%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU126+2 : TPTP v8.1.2. Released v3.3.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:40:36 EDT 2024
% Result : Theorem 9.90s 10.07s
% Output : Refutation 9.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SEU126+2 : TPTP v8.1.2. Released v3.3.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.36 % Computer : n020.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Wed May 8 12:04:38 EDT 2024
% 0.13/0.36 % CPUTime :
% 9.90/10.07 % Version: 1.5
% 9.90/10.07 % SZS status Theorem
% 9.90/10.07 % SZS output start CNFRefutation
% 9.90/10.07 fof(t12_xboole_1,conjecture,(![A]:(![B]:(subset(A,B)=>set_union2(A,B)=B))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t12_xboole_1)).
% 9.90/10.07 fof(c48,negated_conjecture,(~(![A]:(![B]:(subset(A,B)=>set_union2(A,B)=B)))),inference(assume_negation,[status(cth)],[t12_xboole_1])).
% 9.90/10.07 fof(c49,negated_conjecture,(?[A]:(?[B]:(subset(A,B)&set_union2(A,B)!=B))),inference(fof_nnf,[status(thm)],[c48])).
% 9.90/10.07 fof(c50,negated_conjecture,(?[X30]:(?[X31]:(subset(X30,X31)&set_union2(X30,X31)!=X31))),inference(variable_rename,[status(thm)],[c49])).
% 9.90/10.07 fof(c51,negated_conjecture,(subset(skolem0003,skolem0004)&set_union2(skolem0003,skolem0004)!=skolem0004),inference(skolemize,[status(esa)],[c50])).
% 9.90/10.07 cnf(c53,negated_conjecture,set_union2(skolem0003,skolem0004)!=skolem0004,inference(split_conjunct,[status(thm)],[c51])).
% 9.90/10.07 cnf(symmetry,axiom,X88!=X87|X87=X88,theory(equality)).
% 9.90/10.07 cnf(transitivity,axiom,X92!=X91|X91!=X93|X92=X93,theory(equality)).
% 9.90/10.07 fof(commutativity_k2_xboole_0,axiom,(![A]:(![B]:set_union2(A,B)=set_union2(B,A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', commutativity_k2_xboole_0)).
% 9.90/10.07 fof(c146,plain,(![X81]:(![X82]:set_union2(X81,X82)=set_union2(X82,X81))),inference(variable_rename,[status(thm)],[commutativity_k2_xboole_0])).
% 9.90/10.07 cnf(c147,plain,set_union2(X399,X400)=set_union2(X400,X399),inference(split_conjunct,[status(thm)],[c146])).
% 9.90/10.07 cnf(c738,plain,X3256!=set_union2(X3255,X3254)|X3256=set_union2(X3254,X3255),inference(resolution,[status(thm)],[c147, transitivity])).
% 9.90/10.07 fof(reflexivity_r1_tarski,axiom,(![A]:(![B]:subset(A,A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity_r1_tarski)).
% 9.90/10.07 fof(c57,plain,(![A]:subset(A,A)),inference(fof_simplification,[status(thm)],[reflexivity_r1_tarski])).
% 9.90/10.07 fof(c58,plain,(![X34]:subset(X34,X34)),inference(variable_rename,[status(thm)],[c57])).
% 9.90/10.07 cnf(c59,plain,subset(X86,X86),inference(split_conjunct,[status(thm)],[c58])).
% 9.90/10.07 cnf(c52,negated_conjecture,subset(skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c51])).
% 9.90/10.07 fof(t8_xboole_1,plain,(![A]:(![B]:(![C]:((subset(A,B)&subset(C,B))=>subset(set_union2(A,C),B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t8_xboole_1)).
% 9.90/10.07 fof(c6,plain,(![A]:(![B]:(![C]:((~subset(A,B)|~subset(C,B))|subset(set_union2(A,C),B))))),inference(fof_nnf,[status(thm)],[t8_xboole_1])).
% 9.90/10.07 fof(c7,plain,(![X2]:(![X3]:(![X4]:((~subset(X2,X3)|~subset(X4,X3))|subset(set_union2(X2,X4),X3))))),inference(variable_rename,[status(thm)],[c6])).
% 9.90/10.07 cnf(c8,plain,~subset(X148,X150)|~subset(X149,X150)|subset(set_union2(X148,X149),X150),inference(split_conjunct,[status(thm)],[c7])).
% 9.90/10.07 cnf(c225,plain,~subset(X688,skolem0004)|subset(set_union2(X688,skolem0003),skolem0004),inference(resolution,[status(thm)],[c8, c52])).
% 9.90/10.07 cnf(c1911,plain,subset(set_union2(skolem0004,skolem0003),skolem0004),inference(resolution,[status(thm)],[c225, c59])).
% 9.90/10.07 fof(t7_xboole_1,plain,(![A]:(![B]:subset(A,set_union2(A,B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t7_xboole_1)).
% 9.90/10.07 fof(c12,plain,(![X7]:(![X8]:subset(X7,set_union2(X7,X8)))),inference(variable_rename,[status(thm)],[t7_xboole_1])).
% 9.90/10.07 cnf(c13,plain,subset(X94,set_union2(X94,X95)),inference(split_conjunct,[status(thm)],[c12])).
% 9.90/10.07 fof(d10_xboole_0,axiom,(![A]:(![B]:(A=B<=>(subset(A,B)&subset(B,A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d10_xboole_0)).
% 9.90/10.07 fof(c136,plain,(![A]:(![B]:((A!=B|(subset(A,B)&subset(B,A)))&((~subset(A,B)|~subset(B,A))|A=B)))),inference(fof_nnf,[status(thm)],[d10_xboole_0])).
% 9.90/10.07 fof(c137,plain,((![A]:(![B]:(A!=B|(subset(A,B)&subset(B,A)))))&(![A]:(![B]:((~subset(A,B)|~subset(B,A))|A=B)))),inference(shift_quantors,[status(thm)],[c136])).
% 9.90/10.07 fof(c139,plain,(![X75]:(![X76]:(![X77]:(![X78]:((X75!=X76|(subset(X75,X76)&subset(X76,X75)))&((~subset(X77,X78)|~subset(X78,X77))|X77=X78)))))),inference(shift_quantors,[status(thm)],[fof(c138,plain,((![X75]:(![X76]:(X75!=X76|(subset(X75,X76)&subset(X76,X75)))))&(![X77]:(![X78]:((~subset(X77,X78)|~subset(X78,X77))|X77=X78)))),inference(variable_rename,[status(thm)],[c137])).])).
% 9.90/10.07 fof(c140,plain,(![X75]:(![X76]:(![X77]:(![X78]:(((X75!=X76|subset(X75,X76))&(X75!=X76|subset(X76,X75)))&((~subset(X77,X78)|~subset(X78,X77))|X77=X78)))))),inference(distribute,[status(thm)],[c139])).
% 9.90/10.07 cnf(c143,plain,~subset(X383,X382)|~subset(X382,X383)|X383=X382,inference(split_conjunct,[status(thm)],[c140])).
% 9.90/10.07 cnf(c691,plain,~subset(set_union2(X3077,X3076),X3077)|set_union2(X3077,X3076)=X3077,inference(resolution,[status(thm)],[c143, c13])).
% 9.90/10.07 cnf(c19113,plain,set_union2(skolem0004,skolem0003)=skolem0004,inference(resolution,[status(thm)],[c691, c1911])).
% 9.90/10.07 cnf(c19895,plain,skolem0004=set_union2(skolem0004,skolem0003),inference(resolution,[status(thm)],[c19113, symmetry])).
% 9.90/10.07 cnf(c22883,plain,skolem0004=set_union2(skolem0003,skolem0004),inference(resolution,[status(thm)],[c19895, c738])).
% 9.90/10.07 cnf(c24673,plain,set_union2(skolem0003,skolem0004)=skolem0004,inference(resolution,[status(thm)],[c22883, symmetry])).
% 9.90/10.07 cnf(c25102,plain,$false,inference(resolution,[status(thm)],[c24673, c53])).
% 9.90/10.07 % SZS output end CNFRefutation
% 9.90/10.07
% 9.90/10.07 % Initial clauses : 62
% 9.90/10.07 % Processed clauses : 684
% 9.90/10.07 % Factors computed : 100
% 9.90/10.07 % Resolvents computed: 24978
% 9.90/10.07 % Tautologies deleted: 41
% 9.90/10.07 % Forward subsumed : 1759
% 9.90/10.07 % Backward subsumed : 58
% 9.90/10.07 % -------- CPU Time ---------
% 9.90/10.07 % User time : 9.660 s
% 9.90/10.07 % System time : 0.054 s
% 9.90/10.07 % Total time : 9.715 s
%------------------------------------------------------------------------------