%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : PUZ043-1 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:02:46 PM UTC 2026
% Result : Satisfiable 1.24s 1.71s
% Output : Saturation 1.24s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(marsian_females_are_liars,axiom,
( liar(X1)
| ~ from_mars(X1)
| ~ female(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ001-0.ax',marsian_females_are_liars) ).
cnf(from_mars_or_venus,axiom,
( from_mars(X1)
| from_venus(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ001-0.ax',from_mars_or_venus) ).
cnf(male_or_female,axiom,
( male(X1)
| female(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ001-0.ax',male_or_female) ).
cnf(venusian_female_are_truthtellers,axiom,
( truthteller(X1)
| ~ from_venus(X1)
| ~ female(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ001-0.ax',venusian_female_are_truthtellers) ).
cnf(marsian_males_are_truthtellers,axiom,
( truthteller(X1)
| ~ from_mars(X1)
| ~ male(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ001-0.ax',marsian_males_are_truthtellers) ).
cnf(truthtellers_make_true_statements,axiom,
( a_truth(X2)
| ~ truthteller(X1)
| ~ says(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ001-0.ax',truthtellers_make_true_statements) ).
cnf(venusian_males_are_liars,axiom,
( liar(X1)
| ~ from_venus(X1)
| ~ male(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ001-0.ax',venusian_males_are_liars) ).
cnf(false_statements_made_by_liars,axiom,
( a_truth(statement_by(X1))
| liar(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ001-0.ax',false_statements_made_by_liars) ).
cnf(people_say_their_statements,axiom,
( X2 = statement_by(X1)
| ~ says(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ001-0.ax',people_say_their_statements) ).
cnf(truthteller_or_liar,axiom,
( truthteller(X1)
| liar(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ001-0.ax',truthteller_or_liar) ).
cnf(true_statements_made_by_truthtellers,axiom,
( truthteller(X1)
| ~ a_truth(statement_by(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ001-0.ax',true_statements_made_by_truthtellers) ).
cnf(liars_make_false_statements,axiom,
( ~ liar(X1)
| ~ says(X1,X2)
| ~ a_truth(X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ001-0.ax',liars_make_false_statements) ).
cnf(not_truthteller_and_liar,axiom,
( ~ truthteller(X1)
| ~ liar(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ001-0.ax',not_truthteller_and_liar) ).
cnf(not_male_and_female,axiom,
( ~ male(X1)
| ~ female(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ001-0.ax',not_male_and_female) ).
cnf(not_from_mars_and_venus,axiom,
( ~ from_mars(X1)
| ~ from_venus(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ001-0.ax',not_from_mars_and_venus) ).
cnf(c_0_15,axiom,
( liar(X1)
| ~ from_mars(X1)
| ~ female(X1) ),
marsian_females_are_liars,
[final] ).
cnf(c_0_16,axiom,
( from_mars(X1)
| from_venus(X1) ),
from_mars_or_venus,
[final] ).
cnf(c_0_17,plain,
( liar(X1)
| from_venus(X1)
| ~ female(X1) ),
inference(spm,[status(thm)],[c_0_15,c_0_16]),
[final] ).
cnf(c_0_18,axiom,
( male(X1)
| female(X1) ),
male_or_female,
[final] ).
cnf(c_0_19,axiom,
( truthteller(X1)
| ~ from_venus(X1)
| ~ female(X1) ),
venusian_female_are_truthtellers,
[final] ).
cnf(c_0_20,axiom,
( truthteller(X1)
| ~ from_mars(X1)
| ~ male(X1) ),
marsian_males_are_truthtellers,
[final] ).
cnf(c_0_21,plain,
( liar(X1)
| male(X1)
| from_venus(X1) ),
inference(spm,[status(thm)],[c_0_17,c_0_18]),
[final] ).
cnf(c_0_22,plain,
( truthteller(X1)
| male(X1)
| ~ from_venus(X1) ),
inference(spm,[status(thm)],[c_0_19,c_0_18]),
[final] ).
cnf(c_0_23,plain,
( truthteller(X1)
| from_venus(X1)
| ~ male(X1) ),
inference(spm,[status(thm)],[c_0_20,c_0_16]),
[final] ).
cnf(c_0_24,axiom,
( a_truth(X2)
| ~ truthteller(X1)
| ~ says(X1,X2) ),
truthtellers_make_true_statements,
[final] ).
cnf(c_0_25,axiom,
( liar(X1)
| ~ from_venus(X1)
| ~ male(X1) ),
venusian_males_are_liars,
[final] ).
cnf(c_0_26,axiom,
( a_truth(statement_by(X1))
| liar(X1) ),
false_statements_made_by_liars,
[final] ).
cnf(c_0_27,axiom,
( X2 = statement_by(X1)
| ~ says(X1,X2) ),
people_say_their_statements,
[final] ).
cnf(c_0_28,axiom,
( truthteller(X1)
| liar(X1) ),
truthteller_or_liar,
[final] ).
cnf(c_0_29,axiom,
( truthteller(X1)
| ~ a_truth(statement_by(X1)) ),
true_statements_made_by_truthtellers,
[final] ).
cnf(c_0_30,axiom,
( ~ liar(X1)
| ~ says(X1,X2)
| ~ a_truth(X2) ),
liars_make_false_statements,
[final] ).
cnf(c_0_31,axiom,
( ~ truthteller(X1)
| ~ liar(X1) ),
not_truthteller_and_liar,
[final] ).
cnf(c_0_32,axiom,
( ~ male(X1)
| ~ female(X1) ),
not_male_and_female,
[final] ).
cnf(c_0_33,axiom,
( ~ from_mars(X1)
| ~ from_venus(X1) ),
not_from_mars_and_venus,
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PUZ043-1 : TPTP v9.2.1. Released v2.5.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n013.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 01:33:41 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 1.24/1.71 % Version : CSE_E---1.7
% 1.24/1.71 % Problem : theBenchmark.p
% 1.24/1.71 % SZS status Satisfiable for theBenchmark.p
% 1.24/1.71 % SZS output start Saturation
% See solution above
% 1.24/1.71 % Total time : 1.369s
%------------------------------------------------------------------------------