%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL908+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:00:58 PM UTC 2026
% Result : Satisfiable 0.09s 0.46s
% Output : Saturation 0.09s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u77,axiom,
op_equiv ).
cnf(u81,axiom,
equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0)) ).
cnf(u85,axiom,
~ op_or ).
cnf(u89,axiom,
or(X0,X1) = not(and(not(X0),not(X1))) ).
cnf(u93,axiom,
cn3 ).
cnf(u97,axiom,
is_a_theorem(implies(implies(not(X0),X0),X0)) ).
cnf(u101,axiom,
cn2 ).
cnf(u105,axiom,
is_a_theorem(implies(X0,implies(not(X0),X1))) ).
cnf(u109,axiom,
~ cn1 ).
cnf(u113,axiom,
is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))) ).
cnf(u117,axiom,
substitution_of_equivalents ).
cnf(u121,axiom,
( ~ is_a_theorem(equiv(X0,X1))
| X0 = X1 ) ).
cnf(u125,axiom,
modus_ponens ).
cnf(u129,axiom,
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ) ).
cnf(u151,axiom,
is_a_theorem(X1) ).
cnf(u66,axiom,
modus_ponens ).
cnf(u73,axiom,
~ op_or ).
cnf(u70,axiom,
substitution_of_equivalents ).
cnf(u176,axiom,
X0 = X1 ).
cnf(u65,axiom,
op_equiv ).
cnf(u69,axiom,
cn3 ).
cnf(u74,axiom,
~ cn1 ).
cnf(u68,axiom,
cn2 ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL908+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.39 % Computer : n015.cluster.edu
% 0.09/0.39 % Model : x86_64 x86_64
% 0.09/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.39 % Memory : 8046.5625MB
% 0.09/0.39 % OS : Linux 6.8.0-71-generic
% 0.09/0.39 % CPULimit : 300
% 0.09/0.39 % WCLimit : 300
% 0.09/0.39 % DateTime : Sun Sep 27 17:09:16 UTC 2026
% 0.09/0.39 % CPUTime :
% 0.09/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.41 Running first-order model finding
% 0.09/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.46 % (1864792)Will run a generic schedule for satisfiability detection.
% 0.09/0.46 % (1864803)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3901252135:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.09/0.46 % (1864798)% WARNING: option uhcvi not known.
% 0.09/0.46 % (1864803) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1864792-1864803"...
% 0.09/0.46 % (1864803)...printing done.
% 0.09/0.46 % SZS status Satisfiable for theBenchmark
% 0.09/0.46 % SZS output start Saturation.
% See solution above
% 0.09/0.46 % SZS output start Definitions and Model Updates.
% 0.09/0.46 globally flip the polarity of every occurrence of predicate "op_implies_or"
% 0.09/0.46 globally flip the polarity of every occurrence of predicate "op_implies_and"
% 0.09/0.46 globally flip the polarity of every occurrence of predicate "op_or"
% 0.09/0.46 globally flip the polarity of every occurrence of predicate "r5"
% 0.09/0.46 globally flip the polarity of every occurrence of predicate "r4"
% 0.09/0.46 globally flip the polarity of every occurrence of predicate "cn1"
% 0.09/0.46 globally flip the polarity of every occurrence of predicate "kn3"
% 0.09/0.46 globally flip the polarity of every occurrence of predicate "kn2"
% 0.09/0.46 globally flip the polarity of every occurrence of predicate "kn1"
% 0.09/0.46 globally flip the polarity of every occurrence of predicate "equivalence_1"
% 0.09/0.46 globally flip the polarity of every occurrence of predicate "or_3"
% 0.09/0.46 globally flip the polarity of every occurrence of predicate "and_3"
% 0.09/0.46 globally flip the polarity of every occurrence of predicate "implies_1"
% 0.09/0.46 globally flip the polarity of every occurrence of predicate "modus_tollens"
% 0.09/0.46 for all inputs,
% 0.09/0.46 define op_and := $false
% 0.09/0.46 for all inputs,
% 0.09/0.46 define op_implies_and := $false
% 0.09/0.46 for all inputs,
% 0.09/0.46 define op_implies_or := $false
% 0.09/0.46 for all inputs,
% 0.09/0.46 define op_implies := $true
% 0.09/0.46 for all groundings,
% 0.09/0.46 whenever ! [X0,X1] : ((is_a_theorem(X0) & is_a_theorem(implies(X0,X1))) => is_a_theorem(X1)) is true, set modus_ponens to true
% 0.09/0.46 for all groundings,
% 0.09/0.46 whenever ! [X0,X1] : (is_a_theorem(equiv(X0,X1)) => X0 = X1) is true, set substitution_of_equivalents to true
% 0.09/0.46 for all inputs,
% 0.09/0.46 define modus_tollens := ! [X0,X1] : is_a_theorem(implies(implies(not(X1),not(X0)),implies(X0,X1)))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define implies_1 := ! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0)))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define implies_2 := ! [X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1)))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define implies_3 := ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define and_1 := ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define and_2 := ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X1))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define and_3 := ! [X0,X1] : is_a_theorem(implies(X0,implies(X1,and(X0,X1))))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define or_1 := ! [X0,X1] : is_a_theorem(implies(X0,or(X0,X1)))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define or_2 := ! [X0,X1] : is_a_theorem(implies(X1,or(X0,X1)))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define or_3 := ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X2),implies(implies(X1,X2),implies(or(X0,X1),X2))))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define equivalence_1 := ! [X0,X1] : is_a_theorem(implies(equiv(X0,X1),implies(X0,X1)))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define equivalence_2 := ! [X0,X1] : is_a_theorem(implies(equiv(X0,X1),implies(X1,X0)))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define equivalence_3 := ! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X0),equiv(X0,X1))))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define kn1 := ! [X0] : is_a_theorem(implies(X0,and(X0,X0)))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define kn2 := ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define kn3 := ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0)))))
% 0.09/0.46 for all groundings,
% 0.09/0.46 whenever ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))) is true, set cn1 to true
% 0.09/0.46 for all groundings,
% 0.09/0.46 whenever ! [X0,X1] : is_a_theorem(implies(X0,implies(not(X0),X1))) is true, set cn2 to true
% 0.09/0.46 for all groundings,
% 0.09/0.46 whenever ! [X0] : is_a_theorem(implies(implies(not(X0),X0),X0)) is true, set cn3 to true
% 0.09/0.46 for all inputs,
% 0.09/0.46 define r1 := ! [X0] : is_a_theorem(implies(or(X0,X0),X0))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define r2 := ! [X0,X1] : is_a_theorem(implies(X1,or(X0,X1)))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define r3 := ! [X0,X1] : is_a_theorem(implies(or(X0,X1),or(X1,X0)))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define r4 := ! [X0,X1,X2] : is_a_theorem(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2))))
% 0.09/0.46 for all inputs,
% 0.09/0.46 define r5 := ! [X0,X1,X2] : is_a_theorem(implies(implies(X1,X2),implies(or(X0,X1),or(X0,X2))))
% 0.09/0.46 % SZS output end Definitions and Model Updates.
% 0.09/0.46 % (1864803)------------------------------
% 0.09/0.46 % (1864803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/0.46 % (1864803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/0.46 % (1864803)CaDiCaL version: 2.1.3
% 0.09/0.46 % (1864803)Termination reason: Satisfiable
% 0.09/0.46 % (1864803)Time elapsed: 0.002 s
% 0.09/0.46 % (1864803)Peak memory usage: 12 MB
% 0.09/0.46 % (1864803)Instructions burned: 3 (million)
% 0.09/0.46 % (1864792)Success in time 0.036 s
% 0.09/0.46 % Vampire exiting
%------------------------------------------------------------------------------