diff options
Diffstat (limited to 'test/golden/abbr/encoding tasks.golden')
| -rw-r--r-- | test/golden/abbr/encoding tasks.golden | 26 |
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 |
