%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ027-1 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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.52s 0.75s
% Output : Refutation 0.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 13
% Syntax : Number of clauses : 34 ( 7 unt; 14 nHn; 30 RR)
% Number of literals : 75 ( 0 equ; 28 neg)
% Maximal clause size : 3 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-1 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-2 aty)
% Number of variables : 16 ( 5 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_there_is_an_answer,negated_conjecture,
~ answer(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_there_is_an_answer) ).
cnf(a_liar_b_truthteller,plain,
( ~ a_truth(liar(a))
| ~ a_truth(truthteller(b))
| answer(a_liar_b_truthteller) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_liar_b_truthteller) ).
cnf(a_and_b_normal,plain,
( ~ a_truth(normal(a))
| ~ a_truth(normal(b))
| answer(a_and_b_normal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_and_b_normal) ).
cnf(person_is_one_type,axiom,
( a_truth(truthteller(X7))
| a_truth(liar(X7))
| a_truth(normal(X7)) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ003-0.ax',person_is_one_type) ).
cnf(b_says_a_not_lower_than_b,plain,
a_truth(says(b,not_lower(a,b))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_says_a_not_lower_than_b) ).
cnf(liars_lie,axiom,
( ~ a_truth(liar(X25))
| ~ a_truth(says(X25,X24))
| ~ a_truth(X24) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ003-0.ax',liars_lie) ).
cnf(c11,plain,
( ~ a_truth(liar(b))
| ~ a_truth(not_lower(a,b)) ),
inference(resolution,[status(thm)],[liars_lie,b_says_a_not_lower_than_b]) ).
cnf(no_one_lower_than_liars,axiom,
( ~ a_truth(lower(X11,X10))
| ~ a_truth(liar(X10)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',no_one_lower_than_liars) ).
cnf(not_lower_or_lower,axiom,
( a_truth(not_lower(X15,X14))
| a_truth(lower(X15,X14)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_lower_or_lower) ).
cnf(c3,plain,
( a_truth(not_lower(X17,X16))
| ~ a_truth(liar(X16)) ),
inference(resolution,[status(thm)],[not_lower_or_lower,no_one_lower_than_liars]) ).
cnf(c6,plain,
( a_truth(not_lower(X44,X43))
| a_truth(truthteller(X43))
| a_truth(normal(X43)) ),
inference(resolution,[status(thm)],[c3,person_is_one_type]) ).
cnf(c38,plain,
( a_truth(truthteller(b))
| a_truth(normal(b))
| ~ a_truth(liar(b)) ),
inference(resolution,[status(thm)],[c6,c11]) ).
cnf(c96,plain,
( a_truth(truthteller(b))
| a_truth(normal(b)) ),
inference(resolution,[status(thm)],[c38,person_is_one_type]) ).
cnf(c105,plain,
( a_truth(truthteller(b))
| ~ a_truth(normal(a))
| answer(a_and_b_normal) ),
inference(resolution,[status(thm)],[c96,a_and_b_normal]) ).
cnf(a_liar_b_normal,plain,
( ~ a_truth(liar(a))
| ~ a_truth(normal(b))
| answer(a_liar_b_normal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_liar_b_normal) ).
cnf(c107,plain,
( a_truth(truthteller(b))
| ~ a_truth(liar(a))
| answer(a_liar_b_normal) ),
inference(resolution,[status(thm)],[c96,a_liar_b_normal]) ).
cnf(truthtellers_lower_than_no_one,axiom,
( ~ a_truth(lower(X9,X8))
| ~ a_truth(truthteller(X9)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',truthtellers_lower_than_no_one) ).
cnf(truthtellers_tell_truth,axiom,
( ~ a_truth(truthteller(X19))
| ~ a_truth(says(X19,X18))
| a_truth(X18) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ003-0.ax',truthtellers_tell_truth) ).
cnf(a_says_a_lower_than_b,plain,
a_truth(says(a,lower(a,b))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_says_a_lower_than_b) ).
cnf(c8,plain,
( ~ a_truth(truthteller(a))
| a_truth(lower(a,b)) ),
inference(resolution,[status(thm)],[a_says_a_lower_than_b,truthtellers_tell_truth]) ).
cnf(c14,plain,
( a_truth(lower(a,b))
| a_truth(liar(a))
| a_truth(normal(a)) ),
inference(resolution,[status(thm)],[c8,person_is_one_type]) ).
cnf(c128,plain,
( a_truth(liar(a))
| a_truth(normal(a))
| ~ a_truth(truthteller(a)) ),
inference(resolution,[status(thm)],[c14,truthtellers_lower_than_no_one]) ).
cnf(c259,plain,
( a_truth(liar(a))
| a_truth(normal(a)) ),
inference(resolution,[status(thm)],[c128,person_is_one_type]) ).
cnf(c260,plain,
( a_truth(normal(a))
| a_truth(truthteller(b))
| answer(a_liar_b_normal) ),
inference(resolution,[status(thm)],[c259,c107]) ).
cnf(c302,plain,
( a_truth(normal(a))
| a_truth(truthteller(b)) ),
inference(resolution,[status(thm)],[c260,prove_there_is_an_answer]) ).
cnf(c306,plain,
( a_truth(truthteller(b))
| answer(a_and_b_normal) ),
inference(resolution,[status(thm)],[c302,c105]) ).
cnf(c318,plain,
a_truth(truthteller(b)),
inference(resolution,[status(thm)],[c306,prove_there_is_an_answer]) ).
cnf(c320,plain,
( ~ a_truth(liar(a))
| answer(a_liar_b_truthteller) ),
inference(resolution,[status(thm)],[c318,a_liar_b_truthteller]) ).
cnf(a_normal_b_truthteller,plain,
( ~ a_truth(normal(a))
| ~ a_truth(truthteller(b))
| answer(a_normal_b_truthteller) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_normal_b_truthteller) ).
cnf(c319,plain,
( ~ a_truth(normal(a))
| answer(a_normal_b_truthteller) ),
inference(resolution,[status(thm)],[c318,a_normal_b_truthteller]) ).
cnf(c327,plain,
( answer(a_normal_b_truthteller)
| a_truth(liar(a)) ),
inference(resolution,[status(thm)],[c319,c259]) ).
cnf(c337,plain,
a_truth(liar(a)),
inference(resolution,[status(thm)],[c327,prove_there_is_an_answer]) ).
cnf(c343,plain,
answer(a_liar_b_truthteller),
inference(resolution,[status(thm)],[c337,c320]) ).
cnf(c344,plain,
$false,
inference(resolution,[status(thm)],[c343,prove_there_is_an_answer]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : PUZ027-1 : TPTP v8.1.2. Released v1.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n027.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 20:37:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.52/0.75 % Version: 1.5
% 0.52/0.75 % SZS status Unsatisfiable
% 0.52/0.75 % SZS output start CNFRefutation
% See solution above
% 0.52/0.75
% 0.52/0.75 % Initial clauses : 32
% 0.52/0.75 % Processed clauses : 87
% 0.52/0.75 % Factors computed : 2
% 0.52/0.75 % Resolvents computed: 343
% 0.52/0.75 % Tautologies deleted: 12
% 0.52/0.75 % Forward subsumed : 36
% 0.52/0.75 % Backward subsumed : 40
% 0.52/0.75 % -------- CPU Time ---------
% 0.52/0.75 % User time : 0.387 s
% 0.52/0.75 % System time : 0.013 s
% 0.52/0.75 % Total time : 0.400 s
%------------------------------------------------------------------------------