summaryrefslogtreecommitdiff
path: root/test/golden/abbr/encoding tasks.golden
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/abbr/encoding tasks.golden')
-rw-r--r--test/golden/abbr/encoding tasks.golden26
1 files changed, 0 insertions, 26 deletions
diff --git a/test/golden/abbr/encoding tasks.golden b/test/golden/abbr/encoding tasks.golden
deleted file mode 100644
index cc4e8d9..0000000
--- a/test/golden/abbr/encoding tasks.golden
+++ /dev/null
@@ -1,26 +0,0 @@
-fof(zf_q0,conjecture,~?[V0]:zf_u0(V0,zf_f0)=>~?[V1]:zf_u0(V1,zf_f0)).
-------------------
-fof(zf_q0,conjecture,![V0]:V0=V0).
-fof(zf_h0,axiom,![V1]:(~?[V2]:zf_u0(V2,V1)=>~?[V3]:zf_u0(V3,V1))).
-------------------
-fof(zf_q0,conjecture,zf_f0=zf_f1=>zf_f0=zf_f1).
-fof(zf_h0,axiom,![V0]:(~?[V1]:zf_u0(V1,V0)=>~?[V2]:zf_u0(V2,V0))).
-fof(zf_h1,axiom,![V3]:V3=V3).
-------------------
-fof(zf_q0,conjecture,~zf_u0(zf_f0,zf_f1)=>~zf_u0(zf_f0,zf_f1)).
-fof(zf_h0,axiom,![V0,V1]:(V0=V1=>V0=V1)).
-fof(zf_h1,axiom,![V2]:(~?[V3]:zf_u0(V3,V2)=>~?[V4]:zf_u0(V4,V2))).
-fof(zf_h2,axiom,![V5]:V5=V5).
-------------------
-fof(zf_q0,conjecture,zf_u0(zf_f0,zf_f1)=>zf_u0(zf_f0,zf_f1)).
-fof(zf_h0,axiom,![V0,V1]:(V0=V1=>V0=V1)).
-fof(zf_h1,axiom,![V2,V3]:(~zf_u0(V2,V3)=>~zf_u0(V2,V3))).
-fof(zf_h2,axiom,![V4]:(~?[V5]:zf_u0(V5,V4)=>~?[V6]:zf_u0(V6,V4))).
-fof(zf_h3,axiom,![V7]:V7=V7).
-------------------
-fof(zf_q0,conjecture,zf_f0=zf_f1=>zf_f0=zf_f1).
-fof(zf_h0,axiom,![V0,V1]:(V0=V1=>V0=V1)).
-fof(zf_h1,axiom,![V2,V3]:(zf_u0(V2,V3)=>zf_u0(V2,V3))).
-fof(zf_h2,axiom,![V4,V5]:(~zf_u0(V4,V5)=>~zf_u0(V4,V5))).
-fof(zf_h3,axiom,![V6]:(~?[V7]:zf_u0(V7,V6)=>~?[V8]:zf_u0(V8,V6))).
-fof(zf_h4,axiom,![V9]:V9=V9). \ No newline at end of file