summaryrefslogtreecommitdiff
path: root/test/golden/replace/encoding tasks.golden
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/replace/encoding tasks.golden')
-rw-r--r--test/golden/replace/encoding tasks.golden17
1 files changed, 0 insertions, 17 deletions
diff --git a/test/golden/replace/encoding tasks.golden b/test/golden/replace/encoding tasks.golden
deleted file mode 100644
index a359f42..0000000
--- a/test/golden/replace/encoding tasks.golden
+++ /dev/null
@@ -1,17 +0,0 @@
-fof(zf_q0,conjecture,zf_u5(zf_u3(zf_u2,zf_u2),zf_u0(zf_u4,zf_u4))).
-fof(zf_h0,axiom,![V0,V1,V2]:(zf_u5(V0,zf_u1(V1,V2))<=>(V0=V1|zf_u5(V0,V2)))).
-fof(zf_h1,axiom,![V3,V4]:![V5]:(zf_u5(V5,zf_u0(V3,V4))<=>?[V6,V7]:(zf_u5(V6,V3)&zf_u5(V7,V4)&zf_u3(V6,V7)=V5))).
-fof(zf_h2,axiom,![V8]:(zf_u5(V8,zf_u4)<=>(zf_u5(V8,zf_u2)|V8=zf_u2))).
-------------------
-fof(zf_q0,conjecture,![V0]:(zf_u5(V0,zf_f0)=>![V1,V2]:((V1=zf_u1(V0,zf_u2)&V2=zf_u1(V0,zf_u2))=>V1=V2))).
-fof(zf_h0,axiom,![V3,V4,V5]:(zf_u5(V3,zf_u1(V4,V5))<=>(V3=V4|zf_u5(V3,V5)))).
-fof(zf_h1,axiom,![V6,V7]:![V8]:(zf_u5(V8,zf_u0(V6,V7))<=>?[V9,V10]:(zf_u5(V9,V6)&zf_u5(V10,V7)&zf_u3(V9,V10)=V8))).
-fof(zf_h2,axiom,![V11]:(zf_u5(V11,zf_u4)<=>(zf_u5(V11,zf_u2)|V11=zf_u2))).
-fof(zf_h3,axiom,zf_u5(zf_u3(zf_u2,zf_u2),zf_u0(zf_u4,zf_u4))).
-------------------
-fof(zf_q0,conjecture,![V0]:(zf_u6(V0,zf_u0(zf_f0,zf_f1))<=>?[V1,V2]:(zf_u6(V1,zf_f0)&zf_u6(V2,zf_f1)&zf_u3(V1,V2)=V0))).
-fof(zf_h0,axiom,![V3,V4,V5]:(zf_u6(V3,zf_u1(V4,V5))<=>(V3=V4|zf_u6(V3,V5)))).
-fof(zf_h1,axiom,![V6,V7]:![V8]:(zf_u6(V8,zf_u0(V6,V7))<=>?[V9,V10]:(zf_u6(V9,V6)&zf_u6(V10,V7)&zf_u3(V9,V10)=V8))).
-fof(zf_h2,axiom,![V11,V12]:(zf_u6(V11,zf_u4(V12))<=>?[V13]:(zf_u6(V13,V12)&V11=zf_u1(V13,zf_u2)))).
-fof(zf_h3,axiom,![V14]:(zf_u6(V14,zf_u5)<=>(zf_u6(V14,zf_u2)|V14=zf_u2))).
-fof(zf_h4,axiom,zf_u6(zf_u3(zf_u2,zf_u2),zf_u0(zf_u5,zf_u5))). \ No newline at end of file