%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET617+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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:39:51 EDT 2024
% Result : Theorem 70.96s 71.20s
% Output : Refutation 70.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 11
% Syntax : Number of formulae : 45 ( 29 unt; 0 def)
% Number of atoms : 63 ( 62 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 41 ( 23 ~; 16 |; 2 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 69 ( 4 sgn 20 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(symmetry,axiom,
( X42 != X41
| X41 = X42 ),
theory(equality) ).
cnf(transitivity,axiom,
( X44 != X43
| X43 != X45
| X44 = X45 ),
theory(equality) ).
fof(commutativity_of_symmetric_difference,axiom,
! [B,C] : symmetric_difference(B,C) = symmetric_difference(C,B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_symmetric_difference) ).
fof(c41,plain,
! [X22,X23] : symmetric_difference(X22,X23) = symmetric_difference(X23,X22),
inference(variable_rename,[status(thm)],[commutativity_of_symmetric_difference]) ).
cnf(c42,plain,
symmetric_difference(X102,X103) = symmetric_difference(X103,X102),
inference(split_conjunct,[status(thm)],[c41]) ).
cnf(c138,plain,
( X457 != symmetric_difference(X458,X459)
| X457 = symmetric_difference(X459,X458) ),
inference(resolution,[status(thm)],[c42,transitivity]) ).
fof(no_difference_with_empty_set1,axiom,
! [B] : difference(B,empty_set) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',no_difference_with_empty_set1) ).
fof(c58,plain,
! [X32] : difference(X32,empty_set) = X32,
inference(variable_rename,[status(thm)],[no_difference_with_empty_set1]) ).
cnf(c59,plain,
difference(X57,empty_set) = X57,
inference(split_conjunct,[status(thm)],[c58]) ).
cnf(c72,plain,
( X185 != difference(X184,empty_set)
| X185 = X184 ),
inference(resolution,[status(thm)],[c59,transitivity]) ).
fof(symmetric_difference_defn,axiom,
! [B,C] : symmetric_difference(B,C) = union(difference(B,C),difference(C,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetric_difference_defn) ).
fof(c62,plain,
! [X34,X35] : symmetric_difference(X34,X35) = union(difference(X34,X35),difference(X35,X34)),
inference(variable_rename,[status(thm)],[symmetric_difference_defn]) ).
cnf(c63,plain,
symmetric_difference(X167,X168) = union(difference(X167,X168),difference(X168,X167)),
inference(split_conjunct,[status(thm)],[c62]) ).
fof(commutativity_of_union,axiom,
! [B,C] : union(B,C) = union(C,B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_union) ).
fof(c43,plain,
! [X24,X25] : union(X24,X25) = union(X25,X24),
inference(variable_rename,[status(thm)],[commutativity_of_union]) ).
cnf(c44,plain,
union(X105,X104) = union(X104,X105),
inference(split_conjunct,[status(thm)],[c43]) ).
fof(union_empty_set,axiom,
! [B] : union(B,empty_set) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',union_empty_set) ).
fof(c60,plain,
! [X33] : union(X33,empty_set) = X33,
inference(variable_rename,[status(thm)],[union_empty_set]) ).
cnf(c61,plain,
union(X58,empty_set) = X58,
inference(split_conjunct,[status(thm)],[c60]) ).
cnf(c77,plain,
( X197 != union(X196,empty_set)
| X197 = X196 ),
inference(resolution,[status(thm)],[c61,transitivity]) ).
cnf(c347,plain,
union(empty_set,X200) = X200,
inference(resolution,[status(thm)],[c77,c44]) ).
cnf(c359,plain,
( X271 != union(empty_set,X270)
| X271 = X270 ),
inference(resolution,[status(thm)],[c347,transitivity]) ).
fof(no_difference_with_empty_set2,axiom,
! [B] : difference(empty_set,B) = empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',no_difference_with_empty_set2) ).
fof(c56,plain,
! [X31] : difference(empty_set,X31) = empty_set,
inference(variable_rename,[status(thm)],[no_difference_with_empty_set2]) ).
cnf(c57,plain,
difference(empty_set,X88) = empty_set,
inference(split_conjunct,[status(thm)],[c56]) ).
cnf(reflexivity,axiom,
X36 = X36,
theory(equality) ).
cnf(c1,axiom,
( X66 != X65
| X63 != X64
| union(X66,X63) = union(X65,X64) ),
theory(equality) ).
cnf(c84,plain,
( X234 != X236
| union(X234,X235) = union(X236,X235) ),
inference(resolution,[status(thm)],[c1,reflexivity]) ).
cnf(c511,plain,
union(difference(empty_set,X2268),X2267) = union(empty_set,X2267),
inference(resolution,[status(thm)],[c84,c57]) ).
cnf(c25271,plain,
union(difference(empty_set,X2270),X2269) = X2269,
inference(resolution,[status(thm)],[c511,c359]) ).
cnf(c25354,plain,
( X5578 != union(difference(empty_set,X5576),X5577)
| X5578 = X5577 ),
inference(resolution,[status(thm)],[c25271,transitivity]) ).
cnf(c98835,plain,
symmetric_difference(empty_set,X5595) = difference(X5595,empty_set),
inference(resolution,[status(thm)],[c25354,c63]) ).
cnf(c99320,plain,
symmetric_difference(empty_set,X5596) = X5596,
inference(resolution,[status(thm)],[c98835,c72]) ).
cnf(c99485,plain,
X5601 = symmetric_difference(empty_set,X5601),
inference(resolution,[status(thm)],[c99320,symmetry]) ).
cnf(c99844,plain,
X5609 = symmetric_difference(X5609,empty_set),
inference(resolution,[status(thm)],[c99485,c138]) ).
cnf(c100150,plain,
symmetric_difference(X5614,empty_set) = X5614,
inference(resolution,[status(thm)],[c99844,symmetry]) ).
fof(prove_th92,conjecture,
! [B] :
( symmetric_difference(B,empty_set) = B
& symmetric_difference(empty_set,B) = B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_th92) ).
fof(c6,negated_conjecture,
~ ! [B] :
( symmetric_difference(B,empty_set) = B
& symmetric_difference(empty_set,B) = B ),
inference(assume_negation,[status(cth)],[prove_th92]) ).
fof(c7,negated_conjecture,
? [B] :
( symmetric_difference(B,empty_set) != B
| symmetric_difference(empty_set,B) != B ),
inference(fof_nnf,[status(thm)],[c6]) ).
fof(c8,negated_conjecture,
( ? [B] : symmetric_difference(B,empty_set) != B
| ? [B] : symmetric_difference(empty_set,B) != B ),
inference(shift_quantors,[status(thm)],[c7]) ).
fof(c9,negated_conjecture,
( ? [X2] : symmetric_difference(X2,empty_set) != X2
| ? [X3] : symmetric_difference(empty_set,X3) != X3 ),
inference(variable_rename,[status(thm)],[c8]) ).
fof(c10,negated_conjecture,
( symmetric_difference(skolem0001,empty_set) != skolem0001
| symmetric_difference(empty_set,skolem0002) != skolem0002 ),
inference(skolemize,[status(esa)],[c9]) ).
cnf(c11,negated_conjecture,
( symmetric_difference(skolem0001,empty_set) != skolem0001
| symmetric_difference(empty_set,skolem0002) != skolem0002 ),
inference(split_conjunct,[status(thm)],[c10]) ).
cnf(c99462,plain,
symmetric_difference(skolem0001,empty_set) != skolem0001,
inference(resolution,[status(thm)],[c99320,c11]) ).
cnf(c100906,plain,
$false,
inference(resolution,[status(thm)],[c99462,c100150]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SET617+3 : TPTP v8.1.2. Released v2.2.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n020.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Wed May 8 18:46:38 EDT 2024
% 0.15/0.37 % CPUTime :
% 70.96/71.20 % Version: 1.5
% 70.96/71.20 % SZS status Theorem
% 70.96/71.20 % SZS output start CNFRefutation
% See solution above
% 70.96/71.20
% 70.96/71.20 % Initial clauses : 30
% 70.96/71.20 % Processed clauses : 1264
% 70.96/71.20 % Factors computed : 45
% 70.96/71.20 % Resolvents computed: 100799
% 70.96/71.20 % Tautologies deleted: 9
% 70.96/71.20 % Forward subsumed : 2904
% 70.96/71.20 % Backward subsumed : 90
% 70.96/71.20 % -------- CPU Time ---------
% 70.96/71.20 % User time : 70.541 s
% 70.96/71.20 % System time : 0.272 s
% 70.96/71.20 % Total time : 70.813 s
%------------------------------------------------------------------------------