%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : COM004-1 : TPTP v8.1.2. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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:17:41 EDT 2024
% Result : Unsatisfiable 15.12s 15.30s
% Output : Refutation 15.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 10
% Syntax : Number of clauses : 20 ( 12 unt; 0 nHn; 18 RR)
% Number of literals : 37 ( 11 equ; 18 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 22 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(goal_is_there_an_empty_node,negated_conjecture,
~ failure_node(X15,or(empty,empty)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_is_there_an_empty_node) ).
cnf(n_left_equals_left_child_of_n,plain,
n_left = left_child_of(n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_left_equals_left_child_of_n) ).
cnf(symmetry,axiom,
( X13 != X12
| X12 = X13 ),
theory(equality) ).
cnf(c9,plain,
left_child_of(n) = n_left,
inference(resolution,[status(thm)],[symmetry,n_left_equals_left_child_of_n]) ).
cnf(n_right_equals_right_child_of_n,plain,
n_right = right_child_of(n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_right_equals_right_child_of_n) ).
cnf(c10,plain,
right_child_of(n) = n_right,
inference(resolution,[status(thm)],[symmetry,n_right_equals_right_child_of_n]) ).
cnf(n_left_and_n_right_are_siblings,axiom,
siblings(left_child_of(X5),right_child_of(X5)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_left_and_n_right_are_siblings) ).
cnf(c7,axiom,
( X51 != X52
| X54 != X53
| ~ siblings(X51,X54)
| siblings(X52,X53) ),
theory(equality) ).
cnf(c61,plain,
( left_child_of(X128) != X127
| right_child_of(X128) != X126
| siblings(X127,X126) ),
inference(resolution,[status(thm)],[c7,n_left_and_n_right_are_siblings]) ).
cnf(c636,plain,
( left_child_of(n) != X129
| siblings(X129,n_right) ),
inference(resolution,[status(thm)],[c61,c10]) ).
cnf(c643,plain,
siblings(n_left,n_right),
inference(resolution,[status(thm)],[c636,c9]) ).
cnf(x_contradicts_not_x,axiom,
contradictory(X4,negate(X4)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_contradicts_not_x) ).
cnf(n_left_is_atom,plain,
failure_node(n_left,or(empty,atom)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_left_is_atom) ).
cnf(make_node,axiom,
( failure_node(parent_of(X7,X6),or(X8,X9))
| ~ failure_node(X7,or(X8,X11))
| ~ failure_node(X6,or(X9,X10))
| ~ contradictory(X11,X10)
| ~ siblings(X7,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',make_node) ).
cnf(n_right_is_not_atom,plain,
failure_node(n_right,or(empty,negate(atom))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_right_is_not_atom) ).
cnf(c15,plain,
( failure_node(parent_of(X63,n_right),or(X62,empty))
| ~ failure_node(X63,or(X62,X61))
| ~ contradictory(X61,negate(atom))
| ~ siblings(X63,n_right) ),
inference(resolution,[status(thm)],[n_right_is_not_atom,make_node]) ).
cnf(c151,plain,
( failure_node(parent_of(n_left,n_right),or(empty,empty))
| ~ contradictory(atom,negate(atom))
| ~ siblings(n_left,n_right) ),
inference(resolution,[status(thm)],[c15,n_left_is_atom]) ).
cnf(c3364,plain,
( failure_node(parent_of(n_left,n_right),or(empty,empty))
| ~ siblings(n_left,n_right) ),
inference(resolution,[status(thm)],[c151,x_contradicts_not_x]) ).
cnf(c32228,plain,
failure_node(parent_of(n_left,n_right),or(empty,empty)),
inference(resolution,[status(thm)],[c3364,c643]) ).
cnf(c32230,plain,
$false,
inference(resolution,[status(thm)],[c32228,goal_is_there_an_empty_node]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : COM004-1 : TPTP v8.1.2. Released v1.1.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n008.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 : Thu May 9 07:11:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 15.12/15.30 % Version: 1.5
% 15.12/15.30 % SZS status Unsatisfiable
% 15.12/15.30 % SZS output start CNFRefutation
% See solution above
% 15.12/15.30
% 15.12/15.30 % Initial clauses : 20
% 15.12/15.30 % Processed clauses : 907
% 15.12/15.30 % Factors computed : 4
% 15.12/15.30 % Resolvents computed: 32223
% 15.12/15.30 % Tautologies deleted: 2
% 15.12/15.30 % Forward subsumed : 589
% 15.12/15.30 % Backward subsumed : 3
% 15.12/15.30 % -------- CPU Time ---------
% 15.12/15.30 % User time : 14.857 s
% 15.12/15.30 % System time : 0.097 s
% 15.12/15.30 % Total time : 14.954 s
%------------------------------------------------------------------------------