%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET929+1 : TPTP v8.1.2. Released v3.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:40:23 EDT 2024
% Result : Theorem 0.99s 1.16s
% Output : Refutation 0.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : SET929+1 : TPTP v8.1.2. Released v3.2.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n020.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 18:27:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.99/1.16 % Version: 1.5
% 0.99/1.16 % SZS status Theorem
% 0.99/1.16 % SZS output start CNFRefutation
% 0.99/1.16 fof(t38_zfmisc_1,axiom,(![A]:(![B]:(![C]:(subset(unordered_pair(A,B),C)<=>(in(A,C)&in(B,C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t38_zfmisc_1)).
% 0.99/1.16 fof(c13,plain,(![A]:(![B]:(![C]:((~subset(unordered_pair(A,B),C)|(in(A,C)&in(B,C)))&((~in(A,C)|~in(B,C))|subset(unordered_pair(A,B),C)))))),inference(fof_nnf,[status(thm)],[t38_zfmisc_1])).
% 0.99/1.16 fof(c14,plain,((![A]:(![B]:(![C]:(~subset(unordered_pair(A,B),C)|(in(A,C)&in(B,C))))))&(![A]:(![B]:(![C]:((~in(A,C)|~in(B,C))|subset(unordered_pair(A,B),C)))))),inference(shift_quantors,[status(thm)],[c13])).
% 0.99/1.16 fof(c16,plain,(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:((~subset(unordered_pair(X5,X6),X7)|(in(X5,X7)&in(X6,X7)))&((~in(X8,X10)|~in(X9,X10))|subset(unordered_pair(X8,X9),X10))))))))),inference(shift_quantors,[status(thm)],[fof(c15,plain,((![X5]:(![X6]:(![X7]:(~subset(unordered_pair(X5,X6),X7)|(in(X5,X7)&in(X6,X7))))))&(![X8]:(![X9]:(![X10]:((~in(X8,X10)|~in(X9,X10))|subset(unordered_pair(X8,X9),X10)))))),inference(variable_rename,[status(thm)],[c14])).])).
% 0.99/1.16 fof(c17,plain,(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(((~subset(unordered_pair(X5,X6),X7)|in(X5,X7))&(~subset(unordered_pair(X5,X6),X7)|in(X6,X7)))&((~in(X8,X10)|~in(X9,X10))|subset(unordered_pair(X8,X9),X10))))))))),inference(distribute,[status(thm)],[c16])).
% 0.99/1.16 cnf(c18,plain,~subset(unordered_pair(X44,X43),X45)|in(X44,X45),inference(split_conjunct,[status(thm)],[c17])).
% 0.99/1.16 fof(t37_xboole_1,axiom,(![A]:(![B]:(set_difference(A,B)=empty_set<=>subset(A,B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t37_xboole_1)).
% 0.99/1.16 fof(c21,plain,(![A]:(![B]:((set_difference(A,B)!=empty_set|subset(A,B))&(~subset(A,B)|set_difference(A,B)=empty_set)))),inference(fof_nnf,[status(thm)],[t37_xboole_1])).
% 0.99/1.16 fof(c22,plain,((![A]:(![B]:(set_difference(A,B)!=empty_set|subset(A,B))))&(![A]:(![B]:(~subset(A,B)|set_difference(A,B)=empty_set)))),inference(shift_quantors,[status(thm)],[c21])).
% 0.99/1.16 fof(c24,plain,(![X11]:(![X12]:(![X13]:(![X14]:((set_difference(X11,X12)!=empty_set|subset(X11,X12))&(~subset(X13,X14)|set_difference(X13,X14)=empty_set)))))),inference(shift_quantors,[status(thm)],[fof(c23,plain,((![X11]:(![X12]:(set_difference(X11,X12)!=empty_set|subset(X11,X12))))&(![X13]:(![X14]:(~subset(X13,X14)|set_difference(X13,X14)=empty_set)))),inference(variable_rename,[status(thm)],[c22])).])).
% 0.99/1.16 cnf(c25,plain,set_difference(X65,X66)!=empty_set|subset(X65,X66),inference(split_conjunct,[status(thm)],[c24])).
% 0.99/1.16 fof(t73_zfmisc_1,conjecture,(![A]:(![B]:(![C]:(set_difference(unordered_pair(A,B),C)=empty_set<=>(in(A,C)&in(B,C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t73_zfmisc_1)).
% 0.99/1.16 fof(c5,negated_conjecture,(~(![A]:(![B]:(![C]:(set_difference(unordered_pair(A,B),C)=empty_set<=>(in(A,C)&in(B,C))))))),inference(assume_negation,[status(cth)],[t73_zfmisc_1])).
% 0.99/1.16 fof(c6,negated_conjecture,(?[A]:(?[B]:(?[C]:((set_difference(unordered_pair(A,B),C)!=empty_set|(~in(A,C)|~in(B,C)))&(set_difference(unordered_pair(A,B),C)=empty_set|(in(A,C)&in(B,C))))))),inference(fof_nnf,[status(thm)],[c5])).
% 0.99/1.16 fof(c7,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((set_difference(unordered_pair(X2,X3),X4)!=empty_set|(~in(X2,X4)|~in(X3,X4)))&(set_difference(unordered_pair(X2,X3),X4)=empty_set|(in(X2,X4)&in(X3,X4))))))),inference(variable_rename,[status(thm)],[c6])).
% 0.99/1.16 fof(c8,negated_conjecture,((set_difference(unordered_pair(skolem0001,skolem0002),skolem0003)!=empty_set|(~in(skolem0001,skolem0003)|~in(skolem0002,skolem0003)))&(set_difference(unordered_pair(skolem0001,skolem0002),skolem0003)=empty_set|(in(skolem0001,skolem0003)&in(skolem0002,skolem0003)))),inference(skolemize,[status(esa)],[c7])).
% 0.99/1.16 fof(c9,negated_conjecture,((set_difference(unordered_pair(skolem0001,skolem0002),skolem0003)!=empty_set|(~in(skolem0001,skolem0003)|~in(skolem0002,skolem0003)))&((set_difference(unordered_pair(skolem0001,skolem0002),skolem0003)=empty_set|in(skolem0001,skolem0003))&(set_difference(unordered_pair(skolem0001,skolem0002),skolem0003)=empty_set|in(skolem0002,skolem0003)))),inference(distribute,[status(thm)],[c8])).
% 0.99/1.16 cnf(c11,negated_conjecture,set_difference(unordered_pair(skolem0001,skolem0002),skolem0003)=empty_set|in(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c9])).
% 0.99/1.16 cnf(c102,plain,in(skolem0001,skolem0003)|subset(unordered_pair(skolem0001,skolem0002),skolem0003),inference(resolution,[status(thm)],[c11, c25])).
% 0.99/1.16 cnf(c869,plain,in(skolem0001,skolem0003),inference(resolution,[status(thm)],[c102, c18])).
% 0.99/1.16 cnf(c19,plain,~subset(unordered_pair(X55,X54),X56)|in(X54,X56),inference(split_conjunct,[status(thm)],[c17])).
% 0.99/1.16 cnf(c12,negated_conjecture,set_difference(unordered_pair(skolem0001,skolem0002),skolem0003)=empty_set|in(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c9])).
% 0.99/1.16 cnf(c126,plain,in(skolem0002,skolem0003)|subset(unordered_pair(skolem0001,skolem0002),skolem0003),inference(resolution,[status(thm)],[c12, c25])).
% 0.99/1.16 cnf(c1265,plain,in(skolem0002,skolem0003),inference(resolution,[status(thm)],[c126, c19])).
% 0.99/1.16 cnf(c10,negated_conjecture,set_difference(unordered_pair(skolem0001,skolem0002),skolem0003)!=empty_set|~in(skolem0001,skolem0003)|~in(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c9])).
% 0.99/1.16 cnf(c26,plain,~subset(X68,X67)|set_difference(X68,X67)=empty_set,inference(split_conjunct,[status(thm)],[c24])).
% 0.99/1.16 cnf(c20,plain,~in(X119,X121)|~in(X120,X121)|subset(unordered_pair(X119,X120),X121),inference(split_conjunct,[status(thm)],[c17])).
% 0.99/1.16 cnf(c1269,plain,~in(X670,skolem0003)|subset(unordered_pair(X670,skolem0002),skolem0003),inference(resolution,[status(thm)],[c1265, c20])).
% 0.99/1.16 cnf(c1548,plain,subset(unordered_pair(skolem0001,skolem0002),skolem0003),inference(resolution,[status(thm)],[c1269, c869])).
% 0.99/1.16 cnf(c1551,plain,set_difference(unordered_pair(skolem0001,skolem0002),skolem0003)=empty_set,inference(resolution,[status(thm)],[c1548, c26])).
% 0.99/1.16 cnf(c1805,plain,~in(skolem0001,skolem0003)|~in(skolem0002,skolem0003),inference(resolution,[status(thm)],[c1551, c10])).
% 0.99/1.16 cnf(c1811,plain,~in(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1805, c1265])).
% 0.99/1.16 cnf(c1812,plain,$false,inference(resolution,[status(thm)],[c1811, c869])).
% 0.99/1.17 % SZS output end CNFRefutation
% 0.99/1.17
% 0.99/1.17 % Initial clauses : 22
% 0.99/1.17 % Processed clauses : 203
% 0.99/1.17 % Factors computed : 10
% 0.99/1.17 % Resolvents computed: 1759
% 0.99/1.17 % Tautologies deleted: 5
% 0.99/1.17 % Forward subsumed : 234
% 0.99/1.17 % Backward subsumed : 27
% 0.99/1.17 % -------- CPU Time ---------
% 0.99/1.17 % User time : 0.775 s
% 0.99/1.17 % System time : 0.014 s
% 0.99/1.17 % Total time : 0.789 s
%------------------------------------------------------------------------------