%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU143+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n032.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:38 EDT 2024
% Result : Theorem 0.16s 0.48s
% Output : Refutation 0.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SEU143+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.11 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.11/0.31 % Computer : n032.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Wed May 8 12:01:37 EDT 2024
% 0.11/0.31 % CPUTime :
% 0.16/0.48 % Version: 1.5
% 0.16/0.48 % SZS status Theorem
% 0.16/0.48 % SZS output start CNFRefutation
% 0.16/0.48 cnf(reflexivity,axiom,X18=X18,theory(equality)).
% 0.16/0.48 fof(d1_xboole_0,axiom,(![A]:(A=empty_set<=>(![B]:(~in(B,A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_xboole_0)).
% 0.16/0.48 fof(c18,plain,(![A]:(A=empty_set<=>(![B]:~in(B,A)))),inference(fof_simplification,[status(thm)],[d1_xboole_0])).
% 0.16/0.48 fof(c19,plain,(![A]:((A!=empty_set|(![B]:~in(B,A)))&((?[B]:in(B,A))|A=empty_set))),inference(fof_nnf,[status(thm)],[c18])).
% 0.16/0.48 fof(c20,plain,((![A]:(A!=empty_set|(![B]:~in(B,A))))&(![A]:((?[B]:in(B,A))|A=empty_set))),inference(shift_quantors,[status(thm)],[c19])).
% 0.16/0.48 fof(c21,plain,((![X5]:(X5!=empty_set|(![X6]:~in(X6,X5))))&(![X7]:((?[X8]:in(X8,X7))|X7=empty_set))),inference(variable_rename,[status(thm)],[c20])).
% 0.16/0.48 fof(c23,plain,(![X5]:(![X6]:(![X7]:((X5!=empty_set|~in(X6,X5))&(in(skolem0004(X7),X7)|X7=empty_set))))),inference(shift_quantors,[status(thm)],[fof(c22,plain,((![X5]:(X5!=empty_set|(![X6]:~in(X6,X5))))&(![X7]:(in(skolem0004(X7),X7)|X7=empty_set))),inference(skolemize,[status(esa)],[c21])).])).
% 0.16/0.48 cnf(c24,plain,X32!=empty_set|~in(X31,X32),inference(split_conjunct,[status(thm)],[c23])).
% 0.16/0.48 cnf(symmetry,axiom,X20!=X19|X19=X20,theory(equality)).
% 0.16/0.48 fof(l1_zfmisc_1,conjecture,(![A]:singleton(A)!=empty_set),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l1_zfmisc_1)).
% 0.16/0.48 fof(c10,negated_conjecture,(~(![A]:singleton(A)!=empty_set)),inference(assume_negation,[status(cth)],[l1_zfmisc_1])).
% 0.16/0.48 fof(c11,negated_conjecture,(?[A]:singleton(A)=empty_set),inference(fof_nnf,[status(thm)],[c10])).
% 0.16/0.48 fof(c12,negated_conjecture,(?[X4]:singleton(X4)=empty_set),inference(variable_rename,[status(thm)],[c11])).
% 0.16/0.48 fof(c13,negated_conjecture,singleton(skolem0003)=empty_set,inference(skolemize,[status(esa)],[c12])).
% 0.16/0.48 cnf(c14,negated_conjecture,singleton(skolem0003)=empty_set,inference(split_conjunct,[status(thm)],[c13])).
% 0.16/0.48 cnf(c41,plain,empty_set=singleton(skolem0003),inference(resolution,[status(thm)],[c14, symmetry])).
% 0.16/0.48 fof(d1_tarski,axiom,(![A]:(![B]:(B=singleton(A)<=>(![C]:(in(C,B)<=>C=A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_tarski)).
% 0.16/0.48 fof(c26,plain,(![A]:(![B]:((B!=singleton(A)|(![C]:((~in(C,B)|C=A)&(C!=A|in(C,B)))))&((?[C]:((~in(C,B)|C!=A)&(in(C,B)|C=A)))|B=singleton(A))))),inference(fof_nnf,[status(thm)],[d1_tarski])).
% 0.16/0.48 fof(c27,plain,((![A]:(![B]:(B!=singleton(A)|((![C]:(~in(C,B)|C=A))&(![C]:(C!=A|in(C,B)))))))&(![A]:(![B]:((?[C]:((~in(C,B)|C!=A)&(in(C,B)|C=A)))|B=singleton(A))))),inference(shift_quantors,[status(thm)],[c26])).
% 0.16/0.48 fof(c28,plain,((![X9]:(![X10]:(X10!=singleton(X9)|((![X11]:(~in(X11,X10)|X11=X9))&(![X12]:(X12!=X9|in(X12,X10)))))))&(![X13]:(![X14]:((?[X15]:((~in(X15,X14)|X15!=X13)&(in(X15,X14)|X15=X13)))|X14=singleton(X13))))),inference(variable_rename,[status(thm)],[c27])).
% 0.16/0.48 fof(c30,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:((X10!=singleton(X9)|((~in(X11,X10)|X11=X9)&(X12!=X9|in(X12,X10))))&(((~in(skolem0005(X13,X14),X14)|skolem0005(X13,X14)!=X13)&(in(skolem0005(X13,X14),X14)|skolem0005(X13,X14)=X13))|X14=singleton(X13))))))))),inference(shift_quantors,[status(thm)],[fof(c29,plain,((![X9]:(![X10]:(X10!=singleton(X9)|((![X11]:(~in(X11,X10)|X11=X9))&(![X12]:(X12!=X9|in(X12,X10)))))))&(![X13]:(![X14]:(((~in(skolem0005(X13,X14),X14)|skolem0005(X13,X14)!=X13)&(in(skolem0005(X13,X14),X14)|skolem0005(X13,X14)=X13))|X14=singleton(X13))))),inference(skolemize,[status(esa)],[c28])).])).
% 0.16/0.48 fof(c31,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(((X10!=singleton(X9)|(~in(X11,X10)|X11=X9))&(X10!=singleton(X9)|(X12!=X9|in(X12,X10))))&(((~in(skolem0005(X13,X14),X14)|skolem0005(X13,X14)!=X13)|X14=singleton(X13))&((in(skolem0005(X13,X14),X14)|skolem0005(X13,X14)=X13)|X14=singleton(X13)))))))))),inference(distribute,[status(thm)],[c30])).
% 0.16/0.48 cnf(c33,plain,X56!=singleton(X58)|X57!=X58|in(X57,X56),inference(split_conjunct,[status(thm)],[c31])).
% 0.16/0.48 cnf(c76,plain,X59!=skolem0003|in(X59,empty_set),inference(resolution,[status(thm)],[c33, c41])).
% 0.16/0.48 cnf(c79,plain,in(skolem0003,empty_set),inference(resolution,[status(thm)],[c76, reflexivity])).
% 0.16/0.48 cnf(c83,plain,empty_set!=empty_set,inference(resolution,[status(thm)],[c79, c24])).
% 0.16/0.48 cnf(c85,plain,$false,inference(resolution,[status(thm)],[c83, reflexivity])).
% 0.16/0.48 % SZS output end CNFRefutation
% 0.16/0.48
% 0.16/0.48 % Initial clauses : 19
% 0.16/0.48 % Processed clauses : 28
% 0.16/0.48 % Factors computed : 2
% 0.16/0.48 % Resolvents computed: 46
% 0.16/0.48 % Tautologies deleted: 4
% 0.16/0.48 % Forward subsumed : 8
% 0.16/0.48 % Backward subsumed : 1
% 0.16/0.48 % -------- CPU Time ---------
% 0.16/0.48 % User time : 0.148 s
% 0.16/0.48 % System time : 0.015 s
% 0.16/0.48 % Total time : 0.163 s
%------------------------------------------------------------------------------