%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ021-1 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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:36 EDT 2024
% Result : Unsatisfiable 20.82s 21.08s
% Output : Refutation 20.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 12
% Syntax : Number of clauses : 40 ( 9 unt; 19 nHn; 18 RR)
% Number of literals : 83 ( 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-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-2 aty)
% Number of variables : 62 ( 7 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(not_knight_and_knave,axiom,
( ~ a_truth(knight(X8),X9)
| ~ a_truth(knave(X8),X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_knight_and_knave) ).
cnf(conjunction2,axiom,
( ~ a_truth(and(X6,X7),X5)
| a_truth(X7,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjunction2) ).
cnf(knight_or_knave,axiom,
( a_truth(knight(X10),X11)
| a_truth(knave(X10),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knight_or_knave) ).
cnf(knights_tell_truth1,axiom,
( ~ a_truth(knight(X21),X20)
| ~ says(X21,X22)
| a_truth(X22,X20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knights_tell_truth1) ).
cnf(c2,plain,
( ~ says(X40,X41)
| a_truth(X41,X42)
| a_truth(knave(X40),X42) ),
inference(resolution,[status(thm)],[knights_tell_truth1,knight_or_knave]) ).
cnf(knaves_lie2,axiom,
( ~ a_truth(knave(X38),X37)
| says(X38,X39)
| a_truth(X39,X37) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knaves_lie2) ).
cnf(conjunction1,axiom,
( ~ a_truth(and(X3,X4),X2)
| a_truth(X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjunction1) ).
cnf(prove_statement_exists2,negated_conjecture,
( says(me,X72)
| a_truth(and(knave(me),rich(me)),X72) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_statement_exists2) ).
cnf(c77,plain,
( says(me,X74)
| a_truth(knave(me),X74) ),
inference(resolution,[status(thm)],[prove_statement_exists2,conjunction1]) ).
cnf(c87,plain,
( says(me,X94)
| says(me,X95)
| a_truth(X95,X94) ),
inference(resolution,[status(thm)],[c77,knaves_lie2]) ).
cnf(c128,plain,
( says(me,X96)
| a_truth(X96,X96) ),
inference(factor,[status(thm)],[c87]) ).
cnf(c155,plain,
( a_truth(X121,X121)
| a_truth(X121,X122)
| a_truth(knave(me),X122) ),
inference(resolution,[status(thm)],[c128,c2]) ).
cnf(c291,plain,
( a_truth(X126,X126)
| a_truth(knave(me),X126) ),
inference(factor,[status(thm)],[c155]) ).
cnf(c368,plain,
( a_truth(knave(me),and(X2052,X2051))
| a_truth(X2051,and(X2052,X2051)) ),
inference(resolution,[status(thm)],[c291,conjunction2]) ).
cnf(c39573,plain,
a_truth(knave(me),and(X2053,knave(me))),
inference(factor,[status(thm)],[c368]) ).
cnf(c39683,plain,
~ a_truth(knight(me),and(X2057,knave(me))),
inference(resolution,[status(thm)],[c39573,not_knight_and_knave]) ).
cnf(knaves_lie1,axiom,
( ~ a_truth(knave(X29),X28)
| ~ says(X29,X30)
| ~ a_truth(X30,X28) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',knaves_lie1) ).
cnf(c292,plain,
a_truth(knave(me),knave(me)),
inference(factor,[status(thm)],[c155]) ).
cnf(c351,plain,
( ~ says(me,X132)
| ~ a_truth(X132,knave(me)) ),
inference(resolution,[status(thm)],[c292,knaves_lie1]) ).
cnf(c79,plain,
( says(me,X75)
| a_truth(rich(me),X75) ),
inference(resolution,[status(thm)],[prove_statement_exists2,conjunction2]) ).
cnf(c86,plain,
( says(me,X88)
| ~ says(me,X87)
| ~ a_truth(X87,X88) ),
inference(resolution,[status(thm)],[c77,knaves_lie1]) ).
cnf(c107,plain,
( says(me,X89)
| ~ says(me,knave(me)) ),
inference(resolution,[status(thm)],[c86,c77]) ).
cnf(c114,plain,
( says(me,X112)
| a_truth(rich(me),knave(me)) ),
inference(resolution,[status(thm)],[c107,c79]) ).
cnf(c454,plain,
~ says(me,knave(me)),
inference(resolution,[status(thm)],[c351,c292]) ).
cnf(c475,plain,
a_truth(rich(me),knave(me)),
inference(resolution,[status(thm)],[c454,c114]) ).
cnf(c491,plain,
~ says(me,rich(me)),
inference(resolution,[status(thm)],[c475,c351]) ).
cnf(c381,plain,
( a_truth(X181,X181)
| says(me,X182)
| a_truth(X182,X181) ),
inference(resolution,[status(thm)],[c291,knaves_lie2]) ).
cnf(c803,plain,
( a_truth(X188,X188)
| a_truth(rich(me),X188) ),
inference(resolution,[status(thm)],[c381,c491]) ).
cnf(not_rich_and_poor,axiom,
( ~ a_truth(rich(X12),X13)
| ~ a_truth(poor(X12),X13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_rich_and_poor) ).
cnf(prove_statement_exists1,negated_conjecture,
( ~ says(me,X60)
| ~ a_truth(and(knave(me),rich(me)),X60) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_statement_exists1) ).
cnf(rich_or_poor,axiom,
( a_truth(rich(X14),X15)
| a_truth(poor(X14),X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rich_or_poor) ).
cnf(conjunction3,axiom,
( a_truth(and(X44,X45),X43)
| ~ a_truth(X44,X43)
| ~ a_truth(X45,X43) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjunction3) ).
cnf(c15,plain,
( a_truth(and(X101,rich(X100)),X99)
| ~ a_truth(X101,X99)
| a_truth(poor(X100),X99) ),
inference(resolution,[status(thm)],[conjunction3,rich_or_poor]) ).
cnf(c384,plain,
( a_truth(X2109,X2109)
| a_truth(and(knave(me),rich(X2108)),X2109)
| a_truth(poor(X2108),X2109) ),
inference(resolution,[status(thm)],[c291,c15]) ).
cnf(c43483,plain,
( a_truth(X2177,X2177)
| a_truth(poor(me),X2177)
| ~ says(me,X2177) ),
inference(resolution,[status(thm)],[c384,prove_statement_exists1]) ).
cnf(c45361,plain,
( a_truth(X2183,X2183)
| a_truth(poor(me),X2183) ),
inference(resolution,[status(thm)],[c43483,c128]) ).
cnf(c46316,plain,
( a_truth(X2198,X2198)
| ~ a_truth(rich(me),X2198) ),
inference(resolution,[status(thm)],[c45361,not_rich_and_poor]) ).
cnf(c47682,plain,
a_truth(X2199,X2199),
inference(resolution,[status(thm)],[c46316,c803]) ).
cnf(c47729,plain,
a_truth(X2200,and(X2200,X2201)),
inference(resolution,[status(thm)],[c47682,conjunction1]) ).
cnf(c47795,plain,
$false,
inference(resolution,[status(thm)],[c47729,c39683]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : PUZ021-1 : TPTP v8.1.2. Released v1.0.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n012.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 20:39:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 20.82/21.08 % Version: 1.5
% 20.82/21.08 % SZS status Unsatisfiable
% 20.82/21.08 % SZS output start CNFRefutation
% See solution above
% 20.82/21.08
% 20.82/21.08 % Initial clauses : 13
% 20.82/21.08 % Processed clauses : 515
% 20.82/21.08 % Factors computed : 178
% 20.82/21.08 % Resolvents computed: 47649
% 20.82/21.08 % Tautologies deleted: 60
% 20.82/21.08 % Forward subsumed : 1348
% 20.82/21.08 % Backward subsumed : 113
% 20.82/21.08 % -------- CPU Time ---------
% 20.82/21.08 % User time : 20.602 s
% 20.82/21.08 % System time : 0.128 s
% 20.82/21.08 % Total time : 20.730 s
%------------------------------------------------------------------------------