diff options
Diffstat (limited to 'test/golden/russell')
| -rw-r--r-- | test/golden/russell/encoding tasks.golden | 16 | ||||
| -rw-r--r-- | test/golden/russell/generating tasks.golden | 864 | ||||
| -rw-r--r-- | test/golden/russell/glossing.golden | 271 | ||||
| -rw-r--r-- | test/golden/russell/verification.golden | 11 |
4 files changed, 0 insertions, 1162 deletions
diff --git a/test/golden/russell/encoding tasks.golden b/test/golden/russell/encoding tasks.golden deleted file mode 100644 index d4ea307..0000000 --- a/test/golden/russell/encoding tasks.golden +++ /dev/null @@ -1,16 +0,0 @@ -fof(zf_q0,conjecture,?[V0]:zf_u0(V0)). -fof(zf_h0,axiom,![V1]:(zf_u0(V1)<=>![V2]:zf_u1(V2,V1))). -fof(zf_h1,axiom,~~?[V3]:zf_u0(V3)). ------------------- -fof(zf_q0,conjecture,zf_u1(zf_f0,zf_f0)<=>~zf_u1(zf_f0,zf_f0)). -fof(zf_h0,axiom,![V0]:(zf_u0(V0)<=>![V1]:zf_u1(V1,V0))). -fof(zf_h1,axiom,![V2]:(zf_u1(V2,zf_f0)<=>(zf_u1(V2,zf_f1)&~zf_u1(V2,V2)))). -fof(zf_h2,axiom,zf_u0(zf_f1)). -fof(zf_h3,axiom,~~?[V3]:zf_u0(V3)). ------------------- -fof(zf_q0,conjecture,$false). -fof(zf_h0,axiom,![V0]:(zf_u0(V0)<=>![V1]:zf_u1(V1,V0))). -fof(zf_h1,axiom,![V2]:(zf_u1(V2,zf_f0)<=>(zf_u1(V2,zf_f1)&~zf_u1(V2,V2)))). -fof(zf_h2,axiom,zf_u0(zf_f1)). -fof(zf_h3,axiom,zf_u1(zf_f0,zf_f0)<=>~zf_u1(zf_f0,zf_f0)). -fof(zf_h4,axiom,~~?[V3]:zf_u0(V3)).
\ No newline at end of file diff --git a/test/golden/russell/generating tasks.golden b/test/golden/russell/generating tasks.golden deleted file mode 100644 index 40c01e6..0000000 --- a/test/golden/russell/generating tasks.golden +++ /dev/null @@ -1,864 +0,0 @@ -[ Task - { taskDirectness = Indirect - ( Not - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 8 - , locColumn = 18 - } - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction ( PropositionalConstant IsTop ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 8 - , locColumn = 21 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "universal" ) End - ) - ( Marker "universal_set" ) - ) - ) - ) - [ TermVar - ( B - ( FreshVar 0 ) - ) - ] - ) - ) - ) - ) - ) - , taskHypotheses = - [ Hypothesis Marker "universal_set" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "universal" ) End - ) - ( Marker "universal_set" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "V" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Quantified Universally - ( Scope - ( Connected Implication ( PropositionalConstant IsTop ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 4 - , locColumn = 32 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( F - ( TermVar - ( B - ( NamedVar "V" ) - ) - ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "_local_1" Not - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 11 - , locColumn = 5 - } - ) - ( Not - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 8 - , locColumn = 18 - } - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction ( PropositionalConstant IsTop ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 8 - , locColumn = 21 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "universal" ) End - ) - ( Marker "universal_set" ) - ) - ) - ) - [ TermVar - ( B - ( FreshVar 0 ) - ) - ] - ) - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "no_universal_set" - , taskLocation = Location - { locFile = "test/examples/russell.tex" - , locLine = 12 - , locColumn = 5 - } - , taskConjecture = Quantified Existentially - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 12 - , locColumn = 12 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "universal" ) End - ) - ( Marker "universal_set" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "V" ) - ) - ] - ) - ) - } -, Task - { taskDirectness = Indirect - ( Not - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 8 - , locColumn = 18 - } - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction ( PropositionalConstant IsTop ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 8 - , locColumn = 21 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "universal" ) End - ) - ( Marker "universal_set" ) - ) - ) - ) - [ TermVar - ( B - ( FreshVar 0 ) - ) - ] - ) - ) - ) - ) - ) - , taskHypotheses = - [ Hypothesis Marker "universal_set" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "universal" ) End - ) - ( Marker "universal_set" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "V" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Quantified Universally - ( Scope - ( Connected Implication ( PropositionalConstant IsTop ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 4 - , locColumn = 32 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( F - ( TermVar - ( B - ( NamedVar "V" ) - ) - ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "_local_3" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "R" ) - ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "V" ) - ) - ) - ] - ) - ( Not - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 13 - , locColumn = 34 - } - ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 13 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "_local_2" Connected Conjunction ( PropositionalConstant IsTop ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 12 - , locColumn = 12 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "universal" ) End - ) - ( Marker "universal_set" ) - ) - ) - ) - [ TermVar - ( NamedVar "V" ) - ] - ) - , Hypothesis Marker "_local_1" Not - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 11 - , locColumn = 5 - } - ) - ( Not - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 8 - , locColumn = 18 - } - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction ( PropositionalConstant IsTop ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 8 - , locColumn = 21 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "universal" ) End - ) - ( Marker "universal_set" ) - ) - ) - ) - [ TermVar - ( B - ( FreshVar 0 ) - ) - ] - ) - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "no_universal_set" - , taskLocation = Location - { locFile = "test/examples/russell.tex" - , locLine = 14 - , locColumn = 5 - } - , taskConjecture = Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 14 - , locColumn = 12 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "R" ) - , TermVar - ( NamedVar "R" ) - ] - ) - ( Not - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 14 - , locColumn = 29 - } - ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 14 - , locColumn = 29 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "R" ) - , TermVar - ( NamedVar "R" ) - ] - ) - ) - } -, Task - { taskDirectness = Indirect - ( Not - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 8 - , locColumn = 18 - } - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction ( PropositionalConstant IsTop ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 8 - , locColumn = 21 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "universal" ) End - ) - ( Marker "universal_set" ) - ) - ) - ) - [ TermVar - ( B - ( FreshVar 0 ) - ) - ] - ) - ) - ) - ) - ) - , taskHypotheses = - [ Hypothesis Marker "universal_set" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "universal" ) End - ) - ( Marker "universal_set" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "V" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( Quantified Universally - ( Scope - ( Connected Implication ( PropositionalConstant IsTop ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 4 - , locColumn = 32 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( F - ( TermVar - ( B - ( NamedVar "V" ) - ) - ) - ) - ) - ) - ] - ) - ) - ) - ) - ) - ) - ) - ) - , Hypothesis Marker "_local_4" Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 14 - , locColumn = 12 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "R" ) - , TermVar - ( NamedVar "R" ) - ] - ) - ( Not - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 14 - , locColumn = 29 - } - ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 14 - , locColumn = 29 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "R" ) - , TermVar - ( NamedVar "R" ) - ] - ) - ) - , Hypothesis Marker "_local_3" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "R" ) - ) - ) - ] - ) - ( Connected Conjunction - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "V" ) - ) - ) - ] - ) - ( Not - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 13 - , locColumn = 34 - } - ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 13 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( B - ( NamedVar "x" ) - ) - ] - ) - ) - ) - ) - ) - , Hypothesis Marker "_local_2" Connected Conjunction ( PropositionalConstant IsTop ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 12 - , locColumn = 12 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "universal" ) End - ) - ( Marker "universal_set" ) - ) - ) - ) - [ TermVar - ( NamedVar "V" ) - ] - ) - , Hypothesis Marker "_local_1" Not - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 11 - , locColumn = 5 - } - ) - ( Not - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 8 - , locColumn = 18 - } - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction ( PropositionalConstant IsTop ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 8 - , locColumn = 21 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "universal" ) End - ) - ( Marker "universal_set" ) - ) - ) - ) - [ TermVar - ( B - ( FreshVar 0 ) - ) - ] - ) - ) - ) - ) - ) - ] - , taskConjectureLabel = Marker "no_universal_set" - , taskLocation = Location - { locFile = "test/examples/russell.tex" - , locLine = 15 - , locColumn = 5 - } - , taskConjecture = PropositionalConstant IsBottom - } -]
\ No newline at end of file diff --git a/test/golden/russell/glossing.golden b/test/golden/russell/glossing.golden deleted file mode 100644 index ab57fdb..0000000 --- a/test/golden/russell/glossing.golden +++ /dev/null @@ -1,271 +0,0 @@ -[ BlockDefn - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 1 - , locColumn = 1 - } - ) - ( Marker "universal_set" ) - ( DefnPredicate [] - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "universal" ) End - ) - ( Marker "universal_set" ) - ) - ) - ( NamedVar "V" :| [] ) - ( Quantified Universally - ( Scope - ( Connected Implication ( PropositionalConstant IsTop ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 4 - , locColumn = 32 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "x" ) - ) - , TermVar - ( F - ( TermVar - ( NamedVar "V" ) - ) - ) - ] - ) - ) - ) - ) - ) -, BlockLemma - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 7 - , locColumn = 1 - } - ) - ( Marker "no_universal_set" ) - ( Lemma [] - ( Not - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 8 - , locColumn = 18 - } - ) - ( Quantified Existentially - ( Scope - ( Connected Conjunction ( PropositionalConstant IsTop ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 8 - , locColumn = 21 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "universal" ) End - ) - ( Marker "universal_set" ) - ) - ) - ) - [ TermVar - ( B - ( FreshVar 0 ) - ) - ] - ) - ) - ) - ) - ) - ) -, BlockProof - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 10 - , locColumn = 1 - } - ) - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 16 - , locColumn = 1 - } - ) - ( ByContradiction - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 11 - , locColumn = 5 - } - ) - ( Take - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 12 - , locColumn = 5 - } - ) - ( NamedVar "V" :| [] ) - ( Connected Conjunction ( PropositionalConstant IsTop ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 12 - , locColumn = 12 - } - ) - ( SymbolPredicate - ( PredicateAdj - ( LexicalItem - ( TokenCons - ( Word "universal" ) End - ) - ( Marker "universal_set" ) - ) - ) - ) - [ TermVar - ( NamedVar "V" ) - ] - ) - ) JustificationEmpty - ( Define - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 13 - , locColumn = 5 - } - ) - ( NamedVar "R" ) - ( TermSep - ( NamedVar "x" ) - ( TermVar - ( NamedVar "V" ) - ) - ( Scope - ( Not - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 13 - , locColumn = 34 - } - ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 13 - , locColumn = 34 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( B () ) - , TermVar - ( B () ) - ] - ) - ) - ) - ) - ( Have - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 14 - , locColumn = 5 - } - ) - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 14 - , locColumn = 12 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "R" ) - , TermVar - ( NamedVar "R" ) - ] - ) - ( Not - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 14 - , locColumn = 29 - } - ) - ( TermSymbol - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 14 - , locColumn = 29 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) - ) - ) - [ TermVar - ( NamedVar "R" ) - , TermVar - ( NamedVar "R" ) - ] - ) - ) - ) JustificationEmpty - ( Contradiction - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 15 - , locColumn = 5 - } - ) JustificationEmpty - ) - ) - ) - ) - ) -]
\ No newline at end of file diff --git a/test/golden/russell/verification.golden b/test/golden/russell/verification.golden deleted file mode 100644 index 7015657..0000000 --- a/test/golden/russell/verification.golden +++ /dev/null @@ -1,11 +0,0 @@ -VerifiedWithTrustedVampire - ( VerificationReport - { verificationRoute = LegacyVerificationRoute - , verificationLegacyDeclaredAssumptionCount = 0 - , verificationTypedDeclaredAssumptionCount = 0 - , verificationTrustedVampireCount = 3 - , verificationExplicitGapLocations = [] - , verificationTrustedLegacyRuleCount = 2 - , verificationKernelProofCount = 0 - } - )
\ No newline at end of file |