%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ026-1 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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 : Thu May 9 17:37:37 EDT 2024
% Result : Unsatisfiable 0.54s 0.74s
% Output : Refutation 0.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 15
% Syntax : Number of clauses : 58 ( 13 unt; 17 nHn; 46 RR)
% Number of literals : 116 ( 0 equ; 55 neg)
% Maximal clause size : 3 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 39 ( 23 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(not_normal_and_not_normal,axiom,
( ~ a_truth(not_normal(X6))
| ~ a_truth(normal(X6)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_normal_and_not_normal) ).
cnf(person_is_one_type,axiom,
( a_truth(truthteller(X4))
| a_truth(liar(X4))
| a_truth(normal(X4)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ003-0.ax',person_is_one_type) ).
cnf(a_says_a_normal,plain,
a_truth(says(a,normal(a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_says_a_normal) ).
cnf(truthtellers_tell_truth,axiom,
( ~ a_truth(truthteller(X8))
| ~ a_truth(says(X8,X9))
| a_truth(X9) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ003-0.ax',truthtellers_tell_truth) ).
cnf(c8,plain,
( ~ a_truth(truthteller(a))
| a_truth(normal(a)) ),
inference(resolution,[status(thm)],[truthtellers_tell_truth,a_says_a_normal]) ).
cnf(c16,plain,
( a_truth(normal(a))
| a_truth(liar(a)) ),
inference(resolution,[status(thm)],[c8,person_is_one_type]) ).
cnf(c23,plain,
( a_truth(liar(a))
| ~ a_truth(not_normal(a)) ),
inference(resolution,[status(thm)],[c16,not_normal_and_not_normal]) ).
cnf(normal_or_not_normal,axiom,
( a_truth(not_normal(X7))
| a_truth(normal(X7)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',normal_or_not_normal) ).
cnf(a_b_c_are_people,plain,
people(a,b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_b_c_are_people) ).
cnf(not_two_normal2,axiom,
( ~ people(X35,X36,X34)
| ~ a_truth(normal(X35))
| ~ a_truth(normal(X34)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_two_normal2) ).
cnf(c74,plain,
( ~ a_truth(normal(a))
| ~ a_truth(normal(c)) ),
inference(resolution,[status(thm)],[not_two_normal2,a_b_c_are_people]) ).
cnf(c86,plain,
( ~ a_truth(normal(a))
| a_truth(not_normal(c)) ),
inference(resolution,[status(thm)],[c74,normal_or_not_normal]) ).
cnf(c99,plain,
( a_truth(not_normal(c))
| a_truth(liar(a)) ),
inference(resolution,[status(thm)],[c86,c16]) ).
cnf(c_says_c_not_normal,plain,
a_truth(says(c,not_normal(c))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_says_c_not_normal) ).
cnf(liars_lie,axiom,
( ~ a_truth(liar(X13))
| ~ a_truth(says(X13,X14))
| ~ a_truth(X14) ),
file('/export/starexec/sandbox2/benchmark/Axioms/PUZ003-0.ax',liars_lie) ).
cnf(c15,plain,
( ~ a_truth(liar(c))
| ~ a_truth(not_normal(c)) ),
inference(resolution,[status(thm)],[liars_lie,c_says_c_not_normal]) ).
cnf(c19,plain,
( ~ a_truth(liar(c))
| a_truth(normal(c)) ),
inference(resolution,[status(thm)],[c15,normal_or_not_normal]) ).
cnf(c30,plain,
( a_truth(normal(c))
| a_truth(truthteller(c)) ),
inference(resolution,[status(thm)],[c19,person_is_one_type]) ).
cnf(prove_one_of_each,negated_conjecture,
( ~ a_truth(liar(X39))
| ~ a_truth(normal(X38))
| ~ a_truth(truthteller(X37)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_one_of_each) ).
cnf(c84,plain,
( ~ a_truth(liar(X48))
| ~ a_truth(normal(X47))
| a_truth(normal(c)) ),
inference(resolution,[status(thm)],[prove_one_of_each,c30]) ).
cnf(c161,plain,
( ~ a_truth(liar(X57))
| a_truth(normal(c))
| a_truth(not_normal(X56)) ),
inference(resolution,[status(thm)],[c84,normal_or_not_normal]) ).
cnf(b_c_a_are_people,plain,
people(b,c,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_c_a_are_people) ).
cnf(not_two_truthtellers1,axiom,
( ~ people(X20,X21,X19)
| ~ a_truth(truthteller(X20))
| ~ a_truth(truthteller(X21)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_two_truthtellers1) ).
cnf(c41,plain,
( ~ a_truth(truthteller(b))
| ~ a_truth(truthteller(c)) ),
inference(resolution,[status(thm)],[not_two_truthtellers1,b_c_a_are_people]) ).
cnf(c50,plain,
( ~ a_truth(truthteller(b))
| a_truth(normal(c)) ),
inference(resolution,[status(thm)],[c41,c30]) ).
cnf(c3,plain,
( ~ a_truth(not_normal(X43))
| a_truth(truthteller(X43))
| a_truth(liar(X43)) ),
inference(resolution,[status(thm)],[not_normal_and_not_normal,person_is_one_type]) ).
cnf(not_two_normal1,axiom,
( ~ people(X32,X33,X31)
| ~ a_truth(normal(X32))
| ~ a_truth(normal(X33)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_two_normal1) ).
cnf(c65,plain,
( ~ a_truth(normal(a))
| ~ a_truth(normal(b)) ),
inference(resolution,[status(thm)],[not_two_normal1,a_b_c_are_people]) ).
cnf(c72,plain,
( ~ a_truth(normal(a))
| a_truth(not_normal(b)) ),
inference(resolution,[status(thm)],[c65,normal_or_not_normal]) ).
cnf(c82,plain,
( a_truth(not_normal(b))
| a_truth(liar(a)) ),
inference(resolution,[status(thm)],[c72,c16]) ).
cnf(c64,plain,
( ~ a_truth(normal(b))
| ~ a_truth(normal(c)) ),
inference(resolution,[status(thm)],[not_two_normal1,b_c_a_are_people]) ).
cnf(c70,plain,
( ~ a_truth(normal(b))
| a_truth(truthteller(c)) ),
inference(resolution,[status(thm)],[c64,c30]) ).
cnf(c79,plain,
( a_truth(truthteller(c))
| a_truth(not_normal(b)) ),
inference(resolution,[status(thm)],[c70,normal_or_not_normal]) ).
cnf(c90,plain,
( a_truth(not_normal(b))
| ~ a_truth(liar(X50))
| ~ a_truth(normal(X49)) ),
inference(resolution,[status(thm)],[c79,prove_one_of_each]) ).
cnf(c167,plain,
( a_truth(not_normal(b))
| ~ a_truth(liar(X59))
| a_truth(not_normal(X58)) ),
inference(resolution,[status(thm)],[c90,normal_or_not_normal]) ).
cnf(c201,plain,
( a_truth(not_normal(b))
| a_truth(not_normal(X60)) ),
inference(resolution,[status(thm)],[c167,c82]) ).
cnf(c204,plain,
a_truth(not_normal(b)),
inference(factor,[status(thm)],[c201]) ).
cnf(c210,plain,
( a_truth(truthteller(b))
| a_truth(liar(b)) ),
inference(resolution,[status(thm)],[c204,c3]) ).
cnf(c212,plain,
( a_truth(liar(b))
| a_truth(normal(c)) ),
inference(resolution,[status(thm)],[c210,c50]) ).
cnf(c226,plain,
( a_truth(normal(c))
| a_truth(not_normal(X61)) ),
inference(resolution,[status(thm)],[c212,c161]) ).
cnf(c237,plain,
( a_truth(not_normal(X62))
| ~ a_truth(not_normal(c)) ),
inference(resolution,[status(thm)],[c226,not_normal_and_not_normal]) ).
cnf(c249,plain,
( a_truth(not_normal(X68))
| a_truth(liar(a)) ),
inference(resolution,[status(thm)],[c237,c99]) ).
cnf(c283,plain,
a_truth(liar(a)),
inference(resolution,[status(thm)],[c249,c23]) ).
cnf(not_two_liars1,axiom,
( ~ people(X26,X27,X25)
| ~ a_truth(liar(X26))
| ~ a_truth(liar(X27)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_two_liars1) ).
cnf(c53,plain,
( ~ a_truth(liar(a))
| ~ a_truth(liar(b)) ),
inference(resolution,[status(thm)],[not_two_liars1,a_b_c_are_people]) ).
cnf(c37,plain,
( a_truth(truthteller(c))
| ~ a_truth(not_normal(c)) ),
inference(resolution,[status(thm)],[c30,not_normal_and_not_normal]) ).
cnf(c242,plain,
( a_truth(not_normal(X65))
| ~ a_truth(normal(a)) ),
inference(resolution,[status(thm)],[c226,c74]) ).
cnf(b_says_a_normal,plain,
a_truth(says(b,normal(a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_says_a_normal) ).
cnf(c7,plain,
( ~ a_truth(truthteller(b))
| a_truth(normal(a)) ),
inference(resolution,[status(thm)],[truthtellers_tell_truth,b_says_a_normal]) ).
cnf(c217,plain,
( a_truth(liar(b))
| a_truth(normal(a)) ),
inference(resolution,[status(thm)],[c210,c7]) ).
cnf(c297,plain,
( a_truth(liar(b))
| a_truth(not_normal(X81)) ),
inference(resolution,[status(thm)],[c217,c242]) ).
cnf(c305,plain,
( a_truth(not_normal(X83))
| ~ a_truth(liar(a)) ),
inference(resolution,[status(thm)],[c297,c53]) ).
cnf(c311,plain,
a_truth(not_normal(X84)),
inference(resolution,[status(thm)],[c305,c283]) ).
cnf(c313,plain,
a_truth(truthteller(c)),
inference(resolution,[status(thm)],[c311,c37]) ).
cnf(c317,plain,
~ a_truth(truthteller(b)),
inference(resolution,[status(thm)],[c313,c41]) ).
cnf(c319,plain,
a_truth(liar(b)),
inference(resolution,[status(thm)],[c317,c210]) ).
cnf(c321,plain,
~ a_truth(liar(a)),
inference(resolution,[status(thm)],[c319,c53]) ).
cnf(c323,plain,
$false,
inference(resolution,[status(thm)],[c321,c283]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : PUZ026-1 : TPTP v8.1.2. Released v1.0.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n014.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 20:37:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.54/0.74 % Version: 1.5
% 0.54/0.74 % SZS status Unsatisfiable
% 0.54/0.74 % SZS output start CNFRefutation
% See solution above
% 0.54/0.74
% 0.54/0.74 % Initial clauses : 23
% 0.54/0.74 % Processed clauses : 104
% 0.54/0.74 % Factors computed : 1
% 0.54/0.74 % Resolvents computed: 324
% 0.54/0.74 % Tautologies deleted: 7
% 0.54/0.74 % Forward subsumed : 71
% 0.54/0.74 % Backward subsumed : 67
% 0.54/0.74 % -------- CPU Time ---------
% 0.54/0.74 % User time : 0.351 s
% 0.54/0.74 % System time : 0.028 s
% 0.54/0.74 % Total time : 0.380 s
%------------------------------------------------------------------------------