summaryrefslogtreecommitdiff
path: root/test/golden/coord/encoding tasks.golden
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/coord/encoding tasks.golden')
-rw-r--r--test/golden/coord/encoding tasks.golden53
1 files changed, 0 insertions, 53 deletions
diff --git a/test/golden/coord/encoding tasks.golden b/test/golden/coord/encoding tasks.golden
deleted file mode 100644
index ec5d906..0000000
--- a/test/golden/coord/encoding tasks.golden
+++ /dev/null
@@ -1,53 +0,0 @@
-fof(zf_q0,conjecture,zf_f0=zf_f0).
-fof(zf_h0,axiom,![V0]:(zf_u0(V0)<=>V0=V0)).
-fof(zf_h1,axiom,![V1]:(zf_u1(V1)<=>V1=V1)).
-fof(zf_h2,axiom,![V2]:(zf_u2(V2)<=>V2=V2)).
-fof(zf_h3,axiom,zf_u2(zf_f0)).
-fof(zf_h4,axiom,zf_u2(zf_f1)).
-------------------
-fof(zf_q0,conjecture,zf_f0=zf_f0).
-fof(zf_h0,axiom,![V0,V1]:((zf_u2(V0)&zf_u2(V1))=>V0=V0)).
-fof(zf_h1,axiom,![V2]:(zf_u0(V2)<=>V2=V2)).
-fof(zf_h2,axiom,![V3]:(zf_u1(V3)<=>V3=V3)).
-fof(zf_h3,axiom,![V4]:(zf_u2(V4)<=>V4=V4)).
-fof(zf_h4,axiom,zf_u2(zf_f0)&zf_u1(zf_f0)).
-fof(zf_h5,axiom,zf_u2(zf_f1)&zf_u1(zf_f1)).
-------------------
-fof(zf_q0,conjecture,zf_f0=zf_f0).
-fof(zf_h0,axiom,![V0,V1]:((zf_u2(V0)&zf_u1(V0)&zf_u2(V1)&zf_u1(V1))=>V0=V0)).
-fof(zf_h1,axiom,![V2,V3]:((zf_u2(V2)&zf_u2(V3))=>V2=V2)).
-fof(zf_h2,axiom,![V4]:(zf_u0(V4)<=>V4=V4)).
-fof(zf_h3,axiom,![V5]:(zf_u1(V5)<=>V5=V5)).
-fof(zf_h4,axiom,![V6]:(zf_u2(V6)<=>V6=V6)).
-fof(zf_h5,axiom,zf_u1(zf_f0)&zf_u0(zf_f1)).
-fof(zf_h6,axiom,zf_u2(zf_f0)).
-fof(zf_h7,axiom,zf_u2(zf_f1)).
-------------------
-fof(zf_q0,conjecture,zf_f0=zf_f1<=>(zf_u2(zf_f0)&zf_f0=zf_f1)).
-fof(zf_h0,axiom,![V0,V1]:((zf_u1(V0)&zf_u0(V1)&zf_u2(V0)&zf_u2(V1))=>V0=V0)).
-fof(zf_h1,axiom,![V2,V3]:((zf_u2(V2)&zf_u1(V2)&zf_u2(V3)&zf_u1(V3))=>V2=V2)).
-fof(zf_h2,axiom,![V4,V5]:((zf_u2(V4)&zf_u2(V5))=>V4=V4)).
-fof(zf_h3,axiom,![V6]:(zf_u0(V6)<=>V6=V6)).
-fof(zf_h4,axiom,![V7]:(zf_u1(V7)<=>V7=V7)).
-fof(zf_h5,axiom,![V8]:(zf_u2(V8)<=>V8=V8)).
-------------------
-fof(zf_q0,conjecture,zf_u1(zf_f0)&zf_u0(zf_f0)).
-fof(zf_h0,axiom,![V0,V1]:((zf_u1(V0)&zf_u0(V1)&zf_u2(V0)&zf_u2(V1))=>V0=V0)).
-fof(zf_h1,axiom,![V2,V3]:((zf_u2(V2)&zf_u1(V2)&zf_u2(V3)&zf_u1(V3))=>V2=V2)).
-fof(zf_h2,axiom,![V4,V5]:((zf_u2(V4)&zf_u2(V5))=>V4=V4)).
-fof(zf_h3,axiom,![V6,V7]:(V6=V7<=>(zf_u2(V6)&V6=V7))).
-fof(zf_h4,axiom,![V8]:(zf_u0(V8)<=>V8=V8)).
-fof(zf_h5,axiom,![V9]:(zf_u1(V9)<=>V9=V9)).
-fof(zf_h6,axiom,![V10]:(zf_u2(V10)<=>V10=V10)).
-------------------
-fof(zf_q0,conjecture,zf_u2(zf_f0)&zf_u1(zf_f0)&zf_u2(zf_f1)&zf_u1(zf_f1)).
-fof(zf_h0,axiom,![V0,V1]:((zf_u1(V0)&zf_u0(V1)&zf_u2(V0)&zf_u2(V1))=>V0=V0)).
-fof(zf_h1,axiom,![V2,V3]:((zf_u2(V2)&zf_u1(V2)&zf_u2(V3)&zf_u1(V3))=>V2=V2)).
-fof(zf_h2,axiom,![V4,V5]:((zf_u2(V4)&zf_u2(V5))=>V4=V4)).
-fof(zf_h3,axiom,![V6,V7]:(V6=V7<=>(zf_u2(V6)&V6=V7))).
-fof(zf_h4,axiom,![V8]:(zf_u0(V8)<=>V8=V8)).
-fof(zf_h5,axiom,![V9]:(zf_u1(V9)&zf_u0(V9))).
-fof(zf_h6,axiom,![V10]:(zf_u1(V10)<=>V10=V10)).
-fof(zf_h7,axiom,![V11]:(zf_u2(V11)<=>V11=V11)).
-fof(zf_h8,axiom,zf_u2(zf_f0)&zf_u1(zf_f0)).
-fof(zf_h9,axiom,zf_u2(zf_f1)&zf_u1(zf_f1)). \ No newline at end of file