diff options
Diffstat (limited to 'test/golden/datatype/encoding tasks.golden')
| -rw-r--r-- | test/golden/datatype/encoding tasks.golden | 69 |
1 files changed, 0 insertions, 69 deletions
diff --git a/test/golden/datatype/encoding tasks.golden b/test/golden/datatype/encoding tasks.golden deleted file mode 100644 index 5be38a4..0000000 --- a/test/golden/datatype/encoding tasks.golden +++ /dev/null @@ -1,69 +0,0 @@ -fof(zf_q0,conjecture,zf_u6(zf_u3,zf_u4)). -fof(zf_h0,axiom,![V0,V1,V2,V3]:(zf_u0(V0,V1)=zf_u0(V2,V3)=>(V0=V2&V1=V3))). -fof(zf_h1,axiom,![V4,V5,V6]:zf_u5(V4)!=zf_u0(V5,V6)). -fof(zf_h2,axiom,![V7,V8]:((zf_u6(V7,zf_u4)&zf_u6(V8,zf_u4))=>zf_u6(zf_u0(V7,V8),zf_u4))). -fof(zf_h3,axiom,![V9,V10]:(zf_u5(V9)=zf_u5(V10)=>V9=V10)). -fof(zf_h4,axiom,![V11,V12]:zf_u3!=zf_u0(V11,V12)). -fof(zf_h5,axiom,![V13]:((zf_u6(zf_u3,V13)&![V14]:(zf_u6(V14,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V14),V13))&![V15,V16]:((zf_u6(V15,V13)&zf_u6(V16,V13))=>zf_u6(zf_u0(V15,V16),V13)))=>![V17]:(zf_u6(V17,zf_u4)=>zf_u6(V17,V13)))). -fof(zf_h6,axiom,![V18]:(zf_u6(V18,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V18),zf_u4))). -fof(zf_h7,axiom,![V19]:(zf_u6(V19,zf_u4)=>(V19=zf_u3|?[V20]:(zf_u6(V20,zf_u1(zf_u2,zf_u2))&V19=zf_u5(V20))|?[V21,V22]:(zf_u6(V21,zf_u4)&zf_u6(V22,zf_u4)&V19=zf_u0(V21,V22))))). -fof(zf_h8,axiom,![V23]:zf_u3!=zf_u5(V23)). -fof(zf_h9,axiom,zf_u6(zf_u3,zf_u4)). ------------------- -fof(zf_q0,conjecture,zf_u6(zf_u2,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(zf_u2),zf_u4)). -fof(zf_h0,axiom,![V0,V1,V2,V3]:(zf_u0(V0,V1)=zf_u0(V2,V3)=>(V0=V2&V1=V3))). -fof(zf_h1,axiom,![V4,V5,V6]:zf_u5(V4)!=zf_u0(V5,V6)). -fof(zf_h2,axiom,![V7,V8]:((zf_u6(V7,zf_u4)&zf_u6(V8,zf_u4))=>zf_u6(zf_u0(V7,V8),zf_u4))). -fof(zf_h3,axiom,![V9,V10]:(zf_u5(V9)=zf_u5(V10)=>V9=V10)). -fof(zf_h4,axiom,![V11,V12]:zf_u3!=zf_u0(V11,V12)). -fof(zf_h5,axiom,![V13]:((zf_u6(zf_u3,V13)&![V14]:(zf_u6(V14,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V14),V13))&![V15,V16]:((zf_u6(V15,V13)&zf_u6(V16,V13))=>zf_u6(zf_u0(V15,V16),V13)))=>![V17]:(zf_u6(V17,zf_u4)=>zf_u6(V17,V13)))). -fof(zf_h6,axiom,![V18]:(zf_u6(V18,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V18),zf_u4))). -fof(zf_h7,axiom,![V19]:(zf_u6(V19,zf_u4)=>(V19=zf_u3|?[V20]:(zf_u6(V20,zf_u1(zf_u2,zf_u2))&V19=zf_u5(V20))|?[V21,V22]:(zf_u6(V21,zf_u4)&zf_u6(V22,zf_u4)&V19=zf_u0(V21,V22))))). -fof(zf_h8,axiom,![V23]:zf_u3!=zf_u5(V23)). -fof(zf_h9,axiom,zf_u6(zf_u3,zf_u4)). -fof(zf_h10,axiom,zf_u6(zf_u3,zf_u4)). ------------------- -fof(zf_q0,conjecture,zf_u6(zf_u0(zf_u3,zf_u3),zf_u4)). -fof(zf_h0,axiom,![V0,V1,V2,V3]:(zf_u0(V0,V1)=zf_u0(V2,V3)=>(V0=V2&V1=V3))). -fof(zf_h1,axiom,![V4,V5,V6]:zf_u5(V4)!=zf_u0(V5,V6)). -fof(zf_h2,axiom,![V7,V8]:((zf_u6(V7,zf_u4)&zf_u6(V8,zf_u4))=>zf_u6(zf_u0(V7,V8),zf_u4))). -fof(zf_h3,axiom,![V9,V10]:(zf_u5(V9)=zf_u5(V10)=>V9=V10)). -fof(zf_h4,axiom,![V11,V12]:zf_u3!=zf_u0(V11,V12)). -fof(zf_h5,axiom,![V13]:((zf_u6(zf_u3,V13)&![V14]:(zf_u6(V14,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V14),V13))&![V15,V16]:((zf_u6(V15,V13)&zf_u6(V16,V13))=>zf_u6(zf_u0(V15,V16),V13)))=>![V17]:(zf_u6(V17,zf_u4)=>zf_u6(V17,V13)))). -fof(zf_h6,axiom,![V18]:(zf_u6(V18,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V18),zf_u4))). -fof(zf_h7,axiom,![V19]:(zf_u6(V19,zf_u4)=>(V19=zf_u3|?[V20]:(zf_u6(V20,zf_u1(zf_u2,zf_u2))&V19=zf_u5(V20))|?[V21,V22]:(zf_u6(V21,zf_u4)&zf_u6(V22,zf_u4)&V19=zf_u0(V21,V22))))). -fof(zf_h8,axiom,![V23]:zf_u3!=zf_u5(V23)). -fof(zf_h9,axiom,zf_u6(zf_u2,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(zf_u2),zf_u4)). -fof(zf_h10,axiom,zf_u6(zf_u3,zf_u4)). -fof(zf_h11,axiom,zf_u6(zf_u3,zf_u4)). ------------------- -fof(zf_q0,conjecture,zf_u3!=zf_u0(zf_u3,zf_u3)). -fof(zf_h0,axiom,![V0,V1,V2,V3]:(zf_u0(V0,V1)=zf_u0(V2,V3)=>(V0=V2&V1=V3))). -fof(zf_h1,axiom,![V4,V5,V6]:zf_u5(V4)!=zf_u0(V5,V6)). -fof(zf_h2,axiom,![V7,V8]:((zf_u6(V7,zf_u4)&zf_u6(V8,zf_u4))=>zf_u6(zf_u0(V7,V8),zf_u4))). -fof(zf_h3,axiom,![V9,V10]:(zf_u5(V9)=zf_u5(V10)=>V9=V10)). -fof(zf_h4,axiom,![V11,V12]:zf_u3!=zf_u0(V11,V12)). -fof(zf_h5,axiom,![V13]:((zf_u6(zf_u3,V13)&![V14]:(zf_u6(V14,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V14),V13))&![V15,V16]:((zf_u6(V15,V13)&zf_u6(V16,V13))=>zf_u6(zf_u0(V15,V16),V13)))=>![V17]:(zf_u6(V17,zf_u4)=>zf_u6(V17,V13)))). -fof(zf_h6,axiom,![V18]:(zf_u6(V18,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V18),zf_u4))). -fof(zf_h7,axiom,![V19]:(zf_u6(V19,zf_u4)=>(V19=zf_u3|?[V20]:(zf_u6(V20,zf_u1(zf_u2,zf_u2))&V19=zf_u5(V20))|?[V21,V22]:(zf_u6(V21,zf_u4)&zf_u6(V22,zf_u4)&V19=zf_u0(V21,V22))))). -fof(zf_h8,axiom,![V23]:zf_u3!=zf_u5(V23)). -fof(zf_h9,axiom,zf_u6(zf_u0(zf_u3,zf_u3),zf_u4)). -fof(zf_h10,axiom,zf_u6(zf_u2,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(zf_u2),zf_u4)). -fof(zf_h11,axiom,zf_u6(zf_u3,zf_u4)). -fof(zf_h12,axiom,zf_u6(zf_u3,zf_u4)). ------------------- -fof(zf_q0,conjecture,zf_u5(zf_f0)=zf_u5(zf_f1)=>zf_f0=zf_f1). -fof(zf_h0,axiom,![V0,V1,V2,V3]:(zf_u0(V0,V1)=zf_u0(V2,V3)=>(V0=V2&V1=V3))). -fof(zf_h1,axiom,![V4,V5,V6]:zf_u5(V4)!=zf_u0(V5,V6)). -fof(zf_h2,axiom,![V7,V8]:((zf_u6(V7,zf_u4)&zf_u6(V8,zf_u4))=>zf_u6(zf_u0(V7,V8),zf_u4))). -fof(zf_h3,axiom,![V9,V10]:(zf_u5(V9)=zf_u5(V10)=>V9=V10)). -fof(zf_h4,axiom,![V11,V12]:zf_u3!=zf_u0(V11,V12)). -fof(zf_h5,axiom,![V13]:((zf_u6(zf_u3,V13)&![V14]:(zf_u6(V14,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V14),V13))&![V15,V16]:((zf_u6(V15,V13)&zf_u6(V16,V13))=>zf_u6(zf_u0(V15,V16),V13)))=>![V17]:(zf_u6(V17,zf_u4)=>zf_u6(V17,V13)))). -fof(zf_h6,axiom,![V18]:(zf_u6(V18,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(V18),zf_u4))). -fof(zf_h7,axiom,![V19]:(zf_u6(V19,zf_u4)=>(V19=zf_u3|?[V20]:(zf_u6(V20,zf_u1(zf_u2,zf_u2))&V19=zf_u5(V20))|?[V21,V22]:(zf_u6(V21,zf_u4)&zf_u6(V22,zf_u4)&V19=zf_u0(V21,V22))))). -fof(zf_h8,axiom,![V23]:zf_u3!=zf_u5(V23)). -fof(zf_h9,axiom,zf_u3!=zf_u0(zf_u3,zf_u3)). -fof(zf_h10,axiom,zf_u6(zf_u0(zf_u3,zf_u3),zf_u4)). -fof(zf_h11,axiom,zf_u6(zf_u2,zf_u1(zf_u2,zf_u2))=>zf_u6(zf_u5(zf_u2),zf_u4)). -fof(zf_h12,axiom,zf_u6(zf_u3,zf_u4)). -fof(zf_h13,axiom,zf_u6(zf_u3,zf_u4)).
\ No newline at end of file |