%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU153+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:41 EDT 2024
% Result : Theorem 7.17s 7.34s
% Output : Refutation 7.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SEU153+2 : TPTP v8.1.2. Released v3.3.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n005.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 11:26:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 7.17/7.34 % Version: 1.5
% 7.17/7.34 % SZS status Theorem
% 7.17/7.34 % SZS output start CNFRefutation
% 7.17/7.34 fof(l25_zfmisc_1,conjecture,(![A]:(![B]:(~(disjoint(singleton(A),B)&in(A,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', l25_zfmisc_1)).
% 7.17/7.34 fof(c170,negated_conjecture,(~(![A]:(![B]:(~(disjoint(singleton(A),B)&in(A,B)))))),inference(assume_negation,[status(cth)],[l25_zfmisc_1])).
% 7.17/7.34 fof(c171,negated_conjecture,(?[A]:(?[B]:(disjoint(singleton(A),B)&in(A,B)))),inference(fof_nnf,[status(thm)],[c170])).
% 7.17/7.34 fof(c172,negated_conjecture,(?[X107]:(?[X108]:(disjoint(singleton(X107),X108)&in(X107,X108)))),inference(variable_rename,[status(thm)],[c171])).
% 7.17/7.34 fof(c173,negated_conjecture,(disjoint(singleton(skolem0006),skolem0007)&in(skolem0006,skolem0007)),inference(skolemize,[status(esa)],[c172])).
% 7.17/7.34 cnf(c175,negated_conjecture,in(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c173])).
% 7.17/7.34 fof(reflexivity_r1_tarski,axiom,(![A]:(![B]:subset(A,A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity_r1_tarski)).
% 7.17/7.34 fof(c135,plain,(![A]:subset(A,A)),inference(fof_simplification,[status(thm)],[reflexivity_r1_tarski])).
% 7.17/7.34 fof(c136,plain,(![X89]:subset(X89,X89)),inference(variable_rename,[status(thm)],[c135])).
% 7.17/7.34 cnf(c137,plain,subset(X202,X202),inference(split_conjunct,[status(thm)],[c136])).
% 7.17/7.34 fof(l2_zfmisc_1,plain,(![A]:(![B]:(subset(singleton(A),B)<=>in(A,B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', l2_zfmisc_1)).
% 7.17/7.34 fof(c164,plain,(![A]:(![B]:((~subset(singleton(A),B)|in(A,B))&(~in(A,B)|subset(singleton(A),B))))),inference(fof_nnf,[status(thm)],[l2_zfmisc_1])).
% 7.17/7.34 fof(c165,plain,((![A]:(![B]:(~subset(singleton(A),B)|in(A,B))))&(![A]:(![B]:(~in(A,B)|subset(singleton(A),B))))),inference(shift_quantors,[status(thm)],[c164])).
% 7.17/7.34 fof(c167,plain,(![X103]:(![X104]:(![X105]:(![X106]:((~subset(singleton(X103),X104)|in(X103,X104))&(~in(X105,X106)|subset(singleton(X105),X106))))))),inference(shift_quantors,[status(thm)],[fof(c166,plain,((![X103]:(![X104]:(~subset(singleton(X103),X104)|in(X103,X104))))&(![X105]:(![X106]:(~in(X105,X106)|subset(singleton(X105),X106))))),inference(variable_rename,[status(thm)],[c165])).])).
% 7.17/7.34 cnf(c168,plain,~subset(singleton(X588),X587)|in(X588,X587),inference(split_conjunct,[status(thm)],[c167])).
% 7.17/7.34 cnf(c1196,plain,in(X589,singleton(X589)),inference(resolution,[status(thm)],[c168, c137])).
% 7.17/7.34 cnf(c174,negated_conjecture,disjoint(singleton(skolem0006),skolem0007),inference(split_conjunct,[status(thm)],[c173])).
% 7.17/7.34 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)).
% 7.17/7.34 fof(c70,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])).
% 7.17/7.34 fof(c71,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)],[c70])).
% 7.17/7.34 fof(c72,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)],[c71])).
% 7.17/7.34 fof(c73,plain,((![X44]:(![X45]:(disjoint(X44,X45)|(?[X46]:(in(X46,X44)&in(X46,X45))))))&(![X47]:(![X48]:((![X49]:(~in(X49,X47)|~in(X49,X48)))|~disjoint(X47,X48))))),inference(variable_rename,[status(thm)],[c72])).
% 7.17/7.34 fof(c75,plain,(![X44]:(![X45]:(![X47]:(![X48]:(![X49]:((disjoint(X44,X45)|(in(skolem0002(X44,X45),X44)&in(skolem0002(X44,X45),X45)))&((~in(X49,X47)|~in(X49,X48))|~disjoint(X47,X48)))))))),inference(shift_quantors,[status(thm)],[fof(c74,plain,((![X44]:(![X45]:(disjoint(X44,X45)|(in(skolem0002(X44,X45),X44)&in(skolem0002(X44,X45),X45)))))&(![X47]:(![X48]:((![X49]:(~in(X49,X47)|~in(X49,X48)))|~disjoint(X47,X48))))),inference(skolemize,[status(esa)],[c73])).])).
% 7.17/7.34 fof(c76,plain,(![X44]:(![X45]:(![X47]:(![X48]:(![X49]:(((disjoint(X44,X45)|in(skolem0002(X44,X45),X44))&(disjoint(X44,X45)|in(skolem0002(X44,X45),X45)))&((~in(X49,X47)|~in(X49,X48))|~disjoint(X47,X48)))))))),inference(distribute,[status(thm)],[c75])).
% 7.17/7.34 cnf(c79,plain,~in(X413,X414)|~in(X413,X412)|~disjoint(X414,X412),inference(split_conjunct,[status(thm)],[c76])).
% 7.17/7.34 cnf(c733,plain,~in(X2733,singleton(skolem0006))|~in(X2733,skolem0007),inference(resolution,[status(thm)],[c79, c174])).
% 7.17/7.34 cnf(c22195,plain,~in(skolem0006,skolem0007),inference(resolution,[status(thm)],[c733, c1196])).
% 7.17/7.34 cnf(c22201,plain,$false,inference(resolution,[status(thm)],[c22195, c175])).
% 7.17/7.34 % SZS output end CNFRefutation
% 7.17/7.34
% 7.17/7.34 % Initial clauses : 135
% 7.17/7.34 % Processed clauses : 744
% 7.17/7.34 % Factors computed : 36
% 7.17/7.34 % Resolvents computed: 21834
% 7.17/7.34 % Tautologies deleted: 32
% 7.17/7.34 % Forward subsumed : 1169
% 7.17/7.34 % Backward subsumed : 23
% 7.17/7.34 % -------- CPU Time ---------
% 7.17/7.34 % User time : 6.931 s
% 7.17/7.34 % System time : 0.049 s
% 7.17/7.34 % Total time : 6.980 s
%------------------------------------------------------------------------------