diff options
Diffstat (limited to 'test/golden/coord')
| -rw-r--r-- | test/golden/coord/encoding tasks.golden | 53 | ||||
| -rw-r--r-- | test/golden/coord/generating tasks.golden | 3498 | ||||
| -rw-r--r-- | test/golden/coord/glossing.golden | 818 | ||||
| -rw-r--r-- | test/golden/coord/verification.golden | 11 |
4 files changed, 0 insertions, 4380 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 diff --git a/test/golden/coord/generating tasks.golden b/test/golden/coord/generating tasks.golden deleted file mode 100644 index ef6d0a8..0000000 --- a/test/golden/coord/generating tasks.golden +++ /dev/null @@ -1,3498 +0,0 @@ -[ Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "baz" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "baz" ) End - ) - ( Marker "baz" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 10 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "foo" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 5 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 6 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "bar" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 2 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "_local_2" TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 14 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - , Hypothesis Marker "_local_1" TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 14 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ] - , taskConjectureLabel = Marker "nouns" - , taskLocation = Location - { locFile = "test/examples/coord.tex" - , locLine = 13 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 15 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "x" ) - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "nouns" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 14 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 14 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 15 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "baz" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "baz" ) End - ) - ( Marker "baz" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 10 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "foo" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 5 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 6 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "bar" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 2 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "_local_2" Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - , Hypothesis Marker "_local_1" Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ] - , taskConjectureLabel = Marker "adj_nouns" - , taskLocation = Location - { locFile = "test/examples/coord.tex" - , locLine = 18 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 20 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "x" ) - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "adj_nouns" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 20 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "nouns" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 14 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 14 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 15 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "baz" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "baz" ) End - ) - ( Marker "baz" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 10 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "foo" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 5 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 6 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "bar" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 2 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "_local_3" TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - , Hypothesis Marker "_local_2" TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - , Hypothesis Marker "_local_1" Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 56 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "baz" ) End - ) - ( Marker "baz" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - ] - , taskConjectureLabel = Marker "nouns_suchthat" - , taskLocation = Location - { locFile = "test/examples/coord.tex" - , locLine = 24 - , locColumn = 1 - } - , taskConjecture = TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 26 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "x" ) - ] - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "nouns_suchthat" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 56 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "baz" ) End - ) - ( Marker "baz" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 26 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "adj_nouns" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 20 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "nouns" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 14 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 14 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 15 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "baz" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "baz" ) End - ) - ( Marker "baz" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 10 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "foo" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 5 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 6 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "bar" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 2 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "noun_verb" - , taskLocation = Location - { locFile = "test/examples/coord.tex" - , locLine = 30 - , locColumn = 1 - } - , taskConjecture = Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 31 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 31 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "noun_verb" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 31 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 31 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "nouns_suchthat" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 56 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "baz" ) End - ) - ( Marker "baz" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 26 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "adj_nouns" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 20 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "nouns" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 14 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 14 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 15 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "baz" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "baz" ) End - ) - ( Marker "baz" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 10 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "foo" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 5 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 6 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "bar" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 2 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "adjs" - , taskLocation = Location - { locFile = "test/examples/coord.tex" - , locLine = 35 - , locColumn = 1 - } - , taskConjecture = Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 36 - , locColumn = 12 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 36 - , locColumn = 20 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "baz" ) End - ) - ( Marker "baz" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - } -, Task - { taskDirectness = Direct - , taskHypotheses = - [ Hypothesis Marker "adjs" Quantified Universally - ( Scope - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 36 - , locColumn = 12 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 36 - , locColumn = 20 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "baz" ) End - ) - ( Marker "baz" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "noun_verb" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 31 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 31 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - ) - , Hypothesis Marker "nouns_suchthat" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 56 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "baz" ) End - ) - ( Marker "baz" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 26 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "adj_nouns" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 20 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "nouns" Quantified Universally - ( Scope - ( Connected Implication - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 14 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 14 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "y" ) - ) - ] - ) - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 15 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - , Hypothesis Marker "baz" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "baz" ) End - ) - ( Marker "baz" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 10 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "foo" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 5 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 6 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "bar" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 2 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "x" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "_local_2" Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 40 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 40 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - , Hypothesis Marker "_local_1" Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 40 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 40 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ] - , taskConjectureLabel = Marker "are_nouns" - , taskLocation = Location - { locFile = "test/examples/coord.tex" - , locLine = 39 - , locColumn = 1 - } - , taskConjecture = Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 41 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 41 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 41 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 41 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - ) - } -]
\ No newline at end of file diff --git a/test/golden/coord/glossing.golden b/test/golden/coord/glossing.golden deleted file mode 100644 index d1dcd41..0000000 --- a/test/golden/coord/glossing.golden +++ /dev/null @@ -1,818 +0,0 @@ -[ BlockDefn - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( Marker "bar" ) - ( DefnPredicate [] - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ( NamedVar "x" :| [] ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 2 - , locColumn = 25 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "x" ) - ] - ) - ) -, BlockDefn - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 5 - , locColumn = 1 - } - ) - ( Marker "foo" ) - ( DefnPredicate [] - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ( NamedVar "x" :| [] ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 6 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "x" ) - ] - ) - ) -, BlockDefn - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 9 - , locColumn = 1 - } - ) - ( Marker "baz" ) - ( DefnPredicate [] - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "baz" ) End - ) - ( Marker "baz" ) - ) - ) - ( NamedVar "x" :| [] ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 10 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "x" ) - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 13 - , locColumn = 1 - } - ) - ( Marker "nouns" ) - ( Lemma - [ Asm - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 14 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 14 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - ] - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 15 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "x" ) - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 18 - , locColumn = 1 - } - ) - ( Marker "adj_nouns" ) - ( Lemma - [ Asm - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ) - , Asm - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 19 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - ) - ] - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 20 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "x" ) - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 24 - , locColumn = 1 - } - ) - ( Marker "nouns_suchthat" ) - ( Lemma - [ Asm - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 41 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 56 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "baz" ) End - ) - ( Marker "baz" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - , Asm - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 25 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - ] - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 26 - , locColumn = 13 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "x" ) - ] - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 30 - , locColumn = 1 - } - ) - ( Marker "noun_verb" ) - ( Lemma [] - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 31 - , locColumn = 8 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 31 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( ParameterArity 0 ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - , TermVar - ( NamedVar "y" ) - ] - ) - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 35 - , locColumn = 1 - } - ) - ( Marker "adjs" ) - ( Lemma [] - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 36 - , locColumn = 12 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 36 - , locColumn = 20 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "baz" ) End - ) - ( Marker "baz" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 39 - , locColumn = 1 - } - ) - ( Marker "are_nouns" ) - ( Lemma - [ Asm - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 40 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 40 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ) - , Asm - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 40 - , locColumn = 23 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 40 - , locColumn = 19 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - ) - ] - ( Connected Conjunction - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 41 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 41 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( NamedVar "x" ) - ] - ) - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 41 - , locColumn = 30 - } - ) - ( SymbolPredicate - ( PredicateNoun - ( LexicalItemSgPl - ( SgPl - { sg = TokenCons - ( Word "bar" ) End - , pl = TokenCons - ( Word "bars" ) End - } - ) - ( Marker "bar" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/coord.tex" - , locLine = 41 - , locColumn = 26 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "foo" ) End - ) - ( Marker "foo" ) - ) - ) - ) - [ TermVar - ( NamedVar "y" ) - ] - ) - ) - ) - ) -]
\ No newline at end of file diff --git a/test/golden/coord/verification.golden b/test/golden/coord/verification.golden deleted file mode 100644 index 59ecffb..0000000 --- a/test/golden/coord/verification.golden +++ /dev/null @@ -1,11 +0,0 @@ -VerifiedWithTrustedVampire - ( VerificationReport - { verificationRoute = LegacyVerificationRoute - , verificationLegacyDeclaredAssumptionCount = 0 - , verificationTypedDeclaredAssumptionCount = 0 - , verificationTrustedVampireCount = 6 - , verificationExplicitGapLocations = [] - , verificationTrustedLegacyRuleCount = 3 - , verificationKernelProofCount = 0 - } - )
\ No newline at end of file |