%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU189+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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:40:48 EDT 2024
% Result : Theorem 5.35s 5.51s
% Output : Refutation 5.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 8
% Syntax : Number of formulae : 45 ( 12 unt; 0 def)
% Number of atoms : 113 ( 54 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 111 ( 43 ~; 42 |; 17 &)
% ( 2 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-1 aty)
% Number of variables : 28 ( 0 sgn 17 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t6_boole,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
fof(c20,plain,
! [A] :
( ~ empty(A)
| A = empty_set ),
inference(fof_nnf,[status(thm)],[t6_boole]) ).
fof(c21,plain,
! [X4] :
( ~ empty(X4)
| X4 = empty_set ),
inference(variable_rename,[status(thm)],[c20]) ).
cnf(c22,plain,
( ~ empty(X41)
| X41 = empty_set ),
inference(split_conjunct,[status(thm)],[c21]) ).
fof(fc7_relat_1,axiom,
! [A] :
( empty(A)
=> ( empty(relation_dom(A))
& relation(relation_dom(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc7_relat_1) ).
fof(c47,plain,
! [A] :
( ~ empty(A)
| ( empty(relation_dom(A))
& relation(relation_dom(A)) ) ),
inference(fof_nnf,[status(thm)],[fc7_relat_1]) ).
fof(c48,plain,
! [X12] :
( ~ empty(X12)
| ( empty(relation_dom(X12))
& relation(relation_dom(X12)) ) ),
inference(variable_rename,[status(thm)],[c47]) ).
fof(c49,plain,
! [X12] :
( ( ~ empty(X12)
| empty(relation_dom(X12)) )
& ( ~ empty(X12)
| relation(relation_dom(X12)) ) ),
inference(distribute,[status(thm)],[c48]) ).
cnf(c50,plain,
( ~ empty(X59)
| empty(relation_dom(X59)) ),
inference(split_conjunct,[status(thm)],[c49]) ).
fof(fc1_xboole_0,axiom,
empty(empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_xboole_0) ).
cnf(c23,plain,
empty(empty_set),
inference(split_conjunct,[status(thm)],[fc1_xboole_0]) ).
cnf(c3,axiom,
( X46 != X47
| ~ empty(X46)
| empty(X47) ),
theory(equality) ).
cnf(symmetry,axiom,
( X27 != X28
| X28 = X27 ),
theory(equality) ).
fof(t65_relat_1,conjecture,
! [A] :
( relation(A)
=> ( relation_dom(A) = empty_set
<=> relation_rng(A) = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t65_relat_1) ).
fof(c13,negated_conjecture,
~ ! [A] :
( relation(A)
=> ( relation_dom(A) = empty_set
<=> relation_rng(A) = empty_set ) ),
inference(assume_negation,[status(cth)],[t65_relat_1]) ).
fof(c14,negated_conjecture,
? [A] :
( relation(A)
& ( relation_dom(A) != empty_set
| relation_rng(A) != empty_set )
& ( relation_dom(A) = empty_set
| relation_rng(A) = empty_set ) ),
inference(fof_nnf,[status(thm)],[c13]) ).
fof(c15,negated_conjecture,
? [X3] :
( relation(X3)
& ( relation_dom(X3) != empty_set
| relation_rng(X3) != empty_set )
& ( relation_dom(X3) = empty_set
| relation_rng(X3) = empty_set ) ),
inference(variable_rename,[status(thm)],[c14]) ).
fof(c16,negated_conjecture,
( relation(skolem0001)
& ( relation_dom(skolem0001) != empty_set
| relation_rng(skolem0001) != empty_set )
& ( relation_dom(skolem0001) = empty_set
| relation_rng(skolem0001) = empty_set ) ),
inference(skolemize,[status(esa)],[c15]) ).
cnf(c17,negated_conjecture,
relation(skolem0001),
inference(split_conjunct,[status(thm)],[c16]) ).
fof(t64_relat_1,axiom,
! [A] :
( relation(A)
=> ( ( relation_dom(A) = empty_set
| relation_rng(A) = empty_set )
=> A = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t64_relat_1) ).
fof(c6,plain,
! [A] :
( ~ relation(A)
| ( relation_dom(A) != empty_set
& relation_rng(A) != empty_set )
| A = empty_set ),
inference(fof_nnf,[status(thm)],[t64_relat_1]) ).
fof(c7,plain,
! [X2] :
( ~ relation(X2)
| ( relation_dom(X2) != empty_set
& relation_rng(X2) != empty_set )
| X2 = empty_set ),
inference(variable_rename,[status(thm)],[c6]) ).
fof(c8,plain,
! [X2] :
( ( ~ relation(X2)
| relation_dom(X2) != empty_set
| X2 = empty_set )
& ( ~ relation(X2)
| relation_rng(X2) != empty_set
| X2 = empty_set ) ),
inference(distribute,[status(thm)],[c7]) ).
cnf(c10,plain,
( ~ relation(X60)
| relation_rng(X60) != empty_set
| X60 = empty_set ),
inference(split_conjunct,[status(thm)],[c8]) ).
cnf(c9,plain,
( ~ relation(X58)
| relation_dom(X58) != empty_set
| X58 = empty_set ),
inference(split_conjunct,[status(thm)],[c8]) ).
cnf(c19,negated_conjecture,
( relation_dom(skolem0001) = empty_set
| relation_rng(skolem0001) = empty_set ),
inference(split_conjunct,[status(thm)],[c16]) ).
cnf(c189,plain,
( relation_rng(skolem0001) = empty_set
| ~ relation(skolem0001)
| skolem0001 = empty_set ),
inference(resolution,[status(thm)],[c19,c9]) ).
cnf(c739,plain,
( relation_rng(skolem0001) = empty_set
| skolem0001 = empty_set ),
inference(resolution,[status(thm)],[c189,c17]) ).
cnf(c5373,plain,
( skolem0001 = empty_set
| ~ relation(skolem0001) ),
inference(resolution,[status(thm)],[c739,c10]) ).
cnf(c5391,plain,
skolem0001 = empty_set,
inference(resolution,[status(thm)],[c5373,c17]) ).
cnf(c5392,plain,
empty_set = skolem0001,
inference(resolution,[status(thm)],[c5391,symmetry]) ).
cnf(c5409,plain,
( ~ empty(empty_set)
| empty(skolem0001) ),
inference(resolution,[status(thm)],[c5392,c3]) ).
cnf(c5690,plain,
empty(skolem0001),
inference(resolution,[status(thm)],[c5409,c23]) ).
cnf(c5691,plain,
empty(relation_dom(skolem0001)),
inference(resolution,[status(thm)],[c5690,c50]) ).
cnf(c5748,plain,
relation_dom(skolem0001) = empty_set,
inference(resolution,[status(thm)],[c5691,c22]) ).
cnf(c18,negated_conjecture,
( relation_dom(skolem0001) != empty_set
| relation_rng(skolem0001) != empty_set ),
inference(split_conjunct,[status(thm)],[c16]) ).
fof(fc8_relat_1,axiom,
! [A] :
( empty(A)
=> ( empty(relation_rng(A))
& relation(relation_rng(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc8_relat_1) ).
fof(c42,plain,
! [A] :
( ~ empty(A)
| ( empty(relation_rng(A))
& relation(relation_rng(A)) ) ),
inference(fof_nnf,[status(thm)],[fc8_relat_1]) ).
fof(c43,plain,
! [X11] :
( ~ empty(X11)
| ( empty(relation_rng(X11))
& relation(relation_rng(X11)) ) ),
inference(variable_rename,[status(thm)],[c42]) ).
fof(c44,plain,
! [X11] :
( ( ~ empty(X11)
| empty(relation_rng(X11)) )
& ( ~ empty(X11)
| relation(relation_rng(X11)) ) ),
inference(distribute,[status(thm)],[c43]) ).
cnf(c45,plain,
( ~ empty(X49)
| empty(relation_rng(X49)) ),
inference(split_conjunct,[status(thm)],[c44]) ).
cnf(c5720,plain,
empty(relation_rng(skolem0001)),
inference(resolution,[status(thm)],[c5690,c45]) ).
cnf(c5784,plain,
relation_rng(skolem0001) = empty_set,
inference(resolution,[status(thm)],[c5720,c22]) ).
cnf(c6288,plain,
relation_dom(skolem0001) != empty_set,
inference(resolution,[status(thm)],[c5784,c18]) ).
cnf(c6394,plain,
$false,
inference(resolution,[status(thm)],[c6288,c5748]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SEU189+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n007.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 12:05:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 5.35/5.51 % Version: 1.5
% 5.35/5.51 % SZS status Theorem
% 5.35/5.51 % SZS output start CNFRefutation
% See solution above
% 5.35/5.51
% 5.35/5.51 % Initial clauses : 43
% 5.35/5.51 % Processed clauses : 621
% 5.35/5.51 % Factors computed : 3
% 5.35/5.51 % Resolvents computed: 6307
% 5.35/5.51 % Tautologies deleted: 6
% 5.35/5.51 % Forward subsumed : 1252
% 5.35/5.51 % Backward subsumed : 45
% 5.35/5.51 % -------- CPU Time ---------
% 5.35/5.51 % User time : 5.130 s
% 5.35/5.51 % System time : 0.022 s
% 5.35/5.51 % Total time : 5.152 s
%------------------------------------------------------------------------------