%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU122+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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:35 EDT 2024
% Result : Theorem 0.46s 0.67s
% Output : Refutation 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU122+2 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n012.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 : Wed May 8 12:06:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.46/0.67 % Version: 1.5
% 0.46/0.67 % SZS status Theorem
% 0.46/0.67 % SZS output start CNFRefutation
% 0.46/0.67 fof(t2_xboole_1,conjecture,(![A]:subset(empty_set,A)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t2_xboole_1)).
% 0.46/0.67 fof(c32,negated_conjecture,(~(![A]:subset(empty_set,A))),inference(assume_negation,[status(cth)],[t2_xboole_1])).
% 0.46/0.67 fof(c33,negated_conjecture,(?[A]:~subset(empty_set,A)),inference(fof_nnf,[status(thm)],[c32])).
% 0.46/0.67 fof(c34,negated_conjecture,(?[X19]:~subset(empty_set,X19)),inference(variable_rename,[status(thm)],[c33])).
% 0.46/0.67 fof(c35,negated_conjecture,~subset(empty_set,skolem0003),inference(skolemize,[status(esa)],[c34])).
% 0.46/0.67 cnf(c36,negated_conjecture,~subset(empty_set,skolem0003),inference(split_conjunct,[status(thm)],[c35])).
% 0.46/0.67 fof(symmetry_r1_xboole_0,axiom,(![A]:(![B]:(disjoint(A,B)=>disjoint(B,A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', symmetry_r1_xboole_0)).
% 0.46/0.67 fof(c40,plain,(![A]:(![B]:(~disjoint(A,B)|disjoint(B,A)))),inference(fof_nnf,[status(thm)],[symmetry_r1_xboole_0])).
% 0.46/0.67 fof(c41,plain,(![X23]:(![X24]:(~disjoint(X23,X24)|disjoint(X24,X23)))),inference(variable_rename,[status(thm)],[c40])).
% 0.46/0.67 cnf(c42,plain,~disjoint(X74,X75)|disjoint(X75,X74),inference(split_conjunct,[status(thm)],[c41])).
% 0.46/0.67 fof(fc1_xboole_0,axiom,empty(empty_set),file('/export/starexec/sandbox/benchmark/theBenchmark.p', fc1_xboole_0)).
% 0.46/0.67 cnf(c56,plain,empty(empty_set),inference(split_conjunct,[status(thm)],[fc1_xboole_0])).
% 0.46/0.67 fof(t7_boole,axiom,(![A]:(![B]:(~(in(A,B)&empty(B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t7_boole)).
% 0.46/0.67 fof(c8,plain,(![A]:(![B]:(~in(A,B)|~empty(B)))),inference(fof_nnf,[status(thm)],[t7_boole])).
% 0.46/0.67 fof(c9,plain,(![X4]:(![X5]:(~in(X4,X5)|~empty(X5)))),inference(variable_rename,[status(thm)],[c8])).
% 0.46/0.67 cnf(c10,plain,~in(X61,X62)|~empty(X62),inference(split_conjunct,[status(thm)],[c9])).
% 0.46/0.67 fof(t3_xboole_0,plain,(![A]:(![B]:((~((~disjoint(A,B))&(![C]:(~(in(C,A)&in(C,B))))))&(~((?[C]:(in(C,A)&in(C,B)))&disjoint(A,B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t3_xboole_0)).
% 0.46/0.67 fof(c22,plain,(![A]:(![B]:((~(~disjoint(A,B)&(![C]:(~(in(C,A)&in(C,B))))))&(~((?[C]:(in(C,A)&in(C,B)))&disjoint(A,B)))))),inference(fof_simplification,[status(thm)],[t3_xboole_0])).
% 0.46/0.67 fof(c23,plain,(![A]:(![B]:((disjoint(A,B)|(?[C]:(in(C,A)&in(C,B))))&((![C]:(~in(C,A)|~in(C,B)))|~disjoint(A,B))))),inference(fof_nnf,[status(thm)],[c22])).
% 0.46/0.67 fof(c24,plain,((![A]:(![B]:(disjoint(A,B)|(?[C]:(in(C,A)&in(C,B))))))&(![A]:(![B]:((![C]:(~in(C,A)|~in(C,B)))|~disjoint(A,B))))),inference(shift_quantors,[status(thm)],[c23])).
% 0.46/0.67 fof(c25,plain,((![X13]:(![X14]:(disjoint(X13,X14)|(?[X15]:(in(X15,X13)&in(X15,X14))))))&(![X16]:(![X17]:((![X18]:(~in(X18,X16)|~in(X18,X17)))|~disjoint(X16,X17))))),inference(variable_rename,[status(thm)],[c24])).
% 0.46/0.67 fof(c27,plain,(![X13]:(![X14]:(![X16]:(![X17]:(![X18]:((disjoint(X13,X14)|(in(skolem0002(X13,X14),X13)&in(skolem0002(X13,X14),X14)))&((~in(X18,X16)|~in(X18,X17))|~disjoint(X16,X17)))))))),inference(shift_quantors,[status(thm)],[fof(c26,plain,((![X13]:(![X14]:(disjoint(X13,X14)|(in(skolem0002(X13,X14),X13)&in(skolem0002(X13,X14),X14)))))&(![X16]:(![X17]:((![X18]:(~in(X18,X16)|~in(X18,X17)))|~disjoint(X16,X17))))),inference(skolemize,[status(esa)],[c25])).])).
% 0.46/0.67 fof(c28,plain,(![X13]:(![X14]:(![X16]:(![X17]:(![X18]:(((disjoint(X13,X14)|in(skolem0002(X13,X14),X13))&(disjoint(X13,X14)|in(skolem0002(X13,X14),X14)))&((~in(X18,X16)|~in(X18,X17))|~disjoint(X16,X17)))))))),inference(distribute,[status(thm)],[c27])).
% 0.46/0.67 cnf(c29,plain,disjoint(X116,X117)|in(skolem0002(X116,X117),X116),inference(split_conjunct,[status(thm)],[c28])).
% 0.46/0.67 cnf(c161,plain,disjoint(X119,X118)|~empty(X119),inference(resolution,[status(thm)],[c29, c10])).
% 0.46/0.67 cnf(c165,plain,disjoint(empty_set,X120),inference(resolution,[status(thm)],[c161, c56])).
% 0.46/0.67 cnf(c168,plain,disjoint(X122,empty_set),inference(resolution,[status(thm)],[c165, c42])).
% 0.46/0.67 cnf(c31,plain,~in(X134,X132)|~in(X134,X133)|~disjoint(X132,X133),inference(split_conjunct,[status(thm)],[c28])).
% 0.46/0.67 cnf(c189,plain,~in(X162,X163)|~in(X162,empty_set),inference(resolution,[status(thm)],[c31, c168])).
% 0.46/0.67 cnf(c231,plain,~in(X164,empty_set),inference(factor,[status(thm)],[c189])).
% 0.46/0.67 fof(d3_tarski,axiom,(![A]:(![B]:(subset(A,B)<=>(![C]:(in(C,A)=>in(C,B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d3_tarski)).
% 0.46/0.67 fof(c77,plain,(![A]:(![B]:((~subset(A,B)|(![C]:(~in(C,A)|in(C,B))))&((?[C]:(in(C,A)&~in(C,B)))|subset(A,B))))),inference(fof_nnf,[status(thm)],[d3_tarski])).
% 0.46/0.67 fof(c78,plain,((![A]:(![B]:(~subset(A,B)|(![C]:(~in(C,A)|in(C,B))))))&(![A]:(![B]:((?[C]:(in(C,A)&~in(C,B)))|subset(A,B))))),inference(shift_quantors,[status(thm)],[c77])).
% 0.46/0.67 fof(c79,plain,((![X42]:(![X43]:(~subset(X42,X43)|(![X44]:(~in(X44,X42)|in(X44,X43))))))&(![X45]:(![X46]:((?[X47]:(in(X47,X45)&~in(X47,X46)))|subset(X45,X46))))),inference(variable_rename,[status(thm)],[c78])).
% 0.46/0.67 fof(c81,plain,(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:((~subset(X42,X43)|(~in(X44,X42)|in(X44,X43)))&((in(skolem0007(X45,X46),X45)&~in(skolem0007(X45,X46),X46))|subset(X45,X46)))))))),inference(shift_quantors,[status(thm)],[fof(c80,plain,((![X42]:(![X43]:(~subset(X42,X43)|(![X44]:(~in(X44,X42)|in(X44,X43))))))&(![X45]:(![X46]:((in(skolem0007(X45,X46),X45)&~in(skolem0007(X45,X46),X46))|subset(X45,X46))))),inference(skolemize,[status(esa)],[c79])).])).
% 0.46/0.67 fof(c82,plain,(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:((~subset(X42,X43)|(~in(X44,X42)|in(X44,X43)))&((in(skolem0007(X45,X46),X45)|subset(X45,X46))&(~in(skolem0007(X45,X46),X46)|subset(X45,X46))))))))),inference(distribute,[status(thm)],[c81])).
% 0.46/0.67 cnf(c84,plain,in(skolem0007(X247,X246),X247)|subset(X247,X246),inference(split_conjunct,[status(thm)],[c82])).
% 0.46/0.67 cnf(c366,plain,subset(empty_set,X249),inference(resolution,[status(thm)],[c84, c231])).
% 0.46/0.67 cnf(c379,plain,$false,inference(resolution,[status(thm)],[c366, c36])).
% 0.46/0.67 % SZS output end CNFRefutation
% 0.46/0.67
% 0.46/0.67 % Initial clauses : 41
% 0.46/0.67 % Processed clauses : 78
% 0.46/0.67 % Factors computed : 11
% 0.46/0.67 % Resolvents computed: 270
% 0.46/0.67 % Tautologies deleted: 9
% 0.46/0.67 % Forward subsumed : 47
% 0.46/0.67 % Backward subsumed : 6
% 0.46/0.67 % -------- CPU Time ---------
% 0.46/0.67 % User time : 0.299 s
% 0.46/0.67 % System time : 0.020 s
% 0.46/0.67 % Total time : 0.319 s
%------------------------------------------------------------------------------