diff options
Diffstat (limited to 'test/golden/union/encoding tasks.golden')
| -rw-r--r-- | test/golden/union/encoding tasks.golden | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/test/golden/union/encoding tasks.golden b/test/golden/union/encoding tasks.golden deleted file mode 100644 index 444a277..0000000 --- a/test/golden/union/encoding tasks.golden +++ /dev/null @@ -1,21 +0,0 @@ -fof(zf_q0,conjecture,zf_u0(zf_f0,zf_f1)=zf_u0(zf_f1,zf_f0)). -fof(zf_h0,axiom,![V0,V1,V2]:(zf_u1(V0,zf_u0(V1,V2))<=>(zf_u1(V0,V1)|zf_u1(V0,V2)))). -fof(zf_h1,axiom,![V3,V4]:(![V5]:(zf_u1(V5,V3)<=>zf_u1(V5,V4))=>V3=V4)). ------------------- -fof(zf_q0,conjecture,![V0]:(zf_u1(V0,zf_u0(zf_u0(zf_f0,zf_f1),zf_f2))=>zf_u1(V0,zf_u0(zf_f0,zf_u0(zf_f1,zf_f2))))). -fof(zf_h0,axiom,![V1,V2,V3]:(zf_u1(V1,zf_u0(V2,V3))<=>(zf_u1(V1,V2)|zf_u1(V1,V3)))). -fof(zf_h1,axiom,![V4,V5]:(![V6]:(zf_u1(V6,V4)<=>zf_u1(V6,V5))=>V4=V5)). -fof(zf_h2,axiom,![V7,V8]:zf_u0(V7,V8)=zf_u0(V8,V7)). ------------------- -fof(zf_q0,conjecture,![V0]:(zf_u1(V0,zf_u0(zf_f0,zf_u0(zf_f1,zf_f2)))=>zf_u1(V0,zf_u0(zf_u0(zf_f0,zf_f1),zf_f2)))). -fof(zf_h0,axiom,![V1,V2,V3]:(zf_u1(V1,zf_u0(V2,V3))<=>(zf_u1(V1,V2)|zf_u1(V1,V3)))). -fof(zf_h1,axiom,![V4,V5]:(![V6]:(zf_u1(V6,V4)<=>zf_u1(V6,V5))=>V4=V5)). -fof(zf_h2,axiom,![V7,V8]:zf_u0(V7,V8)=zf_u0(V8,V7)). -fof(zf_h3,axiom,![V9]:(zf_u1(V9,zf_u0(zf_u0(zf_f0,zf_f1),zf_f2))=>zf_u1(V9,zf_u0(zf_f0,zf_u0(zf_f1,zf_f2))))). ------------------- -fof(zf_q0,conjecture,zf_u0(zf_u0(zf_f0,zf_f1),zf_f2)=zf_u0(zf_f0,zf_u0(zf_f1,zf_f2))). -fof(zf_h0,axiom,![V0,V1,V2]:(zf_u1(V0,zf_u0(V1,V2))<=>(zf_u1(V0,V1)|zf_u1(V0,V2)))). -fof(zf_h1,axiom,![V3,V4]:(![V5]:(zf_u1(V5,V3)<=>zf_u1(V5,V4))=>V3=V4)). -fof(zf_h2,axiom,![V6,V7]:zf_u0(V6,V7)=zf_u0(V7,V6)). -fof(zf_h3,axiom,![V8]:(zf_u1(V8,zf_u0(zf_f0,zf_u0(zf_f1,zf_f2)))=>zf_u1(V8,zf_u0(zf_u0(zf_f0,zf_f1),zf_f2)))). -fof(zf_h4,axiom,![V9]:(zf_u1(V9,zf_u0(zf_u0(zf_f0,zf_f1),zf_f2))=>zf_u1(V9,zf_u0(zf_f0,zf_u0(zf_f1,zf_f2))))).
\ No newline at end of file |
