%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU230+3 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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:54 EDT 2024
% Result : Theorem 3.24s 3.42s
% Output : Refutation 3.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SEU230+3 : TPTP v8.1.2. Released v3.2.0.
% 0.08/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n013.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 11:14:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 3.24/3.42 % Version: 1.5
% 3.24/3.42 % SZS status Theorem
% 3.24/3.42 % SZS output start CNFRefutation
% 3.24/3.42 fof(t10_ordinal1,conjecture,(![A]:in(A,succ(A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t10_ordinal1)).
% 3.24/3.42 fof(c28,negated_conjecture,(~(![A]:in(A,succ(A)))),inference(assume_negation,[status(cth)],[t10_ordinal1])).
% 3.24/3.42 fof(c29,negated_conjecture,(?[A]:~in(A,succ(A))),inference(fof_nnf,[status(thm)],[c28])).
% 3.24/3.42 fof(c30,negated_conjecture,(?[X12]:~in(X12,succ(X12))),inference(variable_rename,[status(thm)],[c29])).
% 3.24/3.42 fof(c31,negated_conjecture,~in(skolem0001,succ(skolem0001)),inference(skolemize,[status(esa)],[c30])).
% 3.24/3.42 cnf(c32,negated_conjecture,~in(skolem0001,succ(skolem0001)),inference(split_conjunct,[status(thm)],[c31])).
% 3.24/3.42 cnf(reflexivity,axiom,X57=X57,theory(equality)).
% 3.24/3.42 fof(d1_tarski,axiom,(![A]:(![B]:(B=singleton(A)<=>(![C]:(in(C,B)<=>C=A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_tarski)).
% 3.24/3.42 fof(c119,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])).
% 3.24/3.42 fof(c120,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)],[c119])).
% 3.24/3.42 fof(c121,plain,((![X42]:(![X43]:(X43!=singleton(X42)|((![X44]:(~in(X44,X43)|X44=X42))&(![X45]:(X45!=X42|in(X45,X43)))))))&(![X46]:(![X47]:((?[X48]:((~in(X48,X47)|X48!=X46)&(in(X48,X47)|X48=X46)))|X47=singleton(X46))))),inference(variable_rename,[status(thm)],[c120])).
% 3.24/3.42 fof(c123,plain,(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:((X43!=singleton(X42)|((~in(X44,X43)|X44=X42)&(X45!=X42|in(X45,X43))))&(((~in(skolem0014(X46,X47),X47)|skolem0014(X46,X47)!=X46)&(in(skolem0014(X46,X47),X47)|skolem0014(X46,X47)=X46))|X47=singleton(X46))))))))),inference(shift_quantors,[status(thm)],[fof(c122,plain,((![X42]:(![X43]:(X43!=singleton(X42)|((![X44]:(~in(X44,X43)|X44=X42))&(![X45]:(X45!=X42|in(X45,X43)))))))&(![X46]:(![X47]:(((~in(skolem0014(X46,X47),X47)|skolem0014(X46,X47)!=X46)&(in(skolem0014(X46,X47),X47)|skolem0014(X46,X47)=X46))|X47=singleton(X46))))),inference(skolemize,[status(esa)],[c121])).])).
% 3.24/3.42 fof(c124,plain,(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:(((X43!=singleton(X42)|(~in(X44,X43)|X44=X42))&(X43!=singleton(X42)|(X45!=X42|in(X45,X43))))&(((~in(skolem0014(X46,X47),X47)|skolem0014(X46,X47)!=X46)|X47=singleton(X46))&((in(skolem0014(X46,X47),X47)|skolem0014(X46,X47)=X46)|X47=singleton(X46)))))))))),inference(distribute,[status(thm)],[c123])).
% 3.24/3.42 cnf(c126,plain,X158!=singleton(X160)|X159!=X160|in(X159,X158),inference(split_conjunct,[status(thm)],[c124])).
% 3.24/3.42 cnf(c436,plain,X354!=X353|in(X354,singleton(X353)),inference(resolution,[status(thm)],[c126, reflexivity])).
% 3.24/3.42 cnf(c4035,plain,in(X357,singleton(X357)),inference(resolution,[status(thm)],[c436, reflexivity])).
% 3.24/3.42 fof(d2_xboole_0,axiom,(![A]:(![B]:(![C]:(C=set_union2(A,B)<=>(![D]:(in(D,C)<=>(in(D,A)|in(D,B)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d2_xboole_0)).
% 3.24/3.42 fof(c107,plain,(![A]:(![B]:(![C]:((C!=set_union2(A,B)|(![D]:((~in(D,C)|(in(D,A)|in(D,B)))&((~in(D,A)&~in(D,B))|in(D,C)))))&((?[D]:((~in(D,C)|(~in(D,A)&~in(D,B)))&(in(D,C)|(in(D,A)|in(D,B)))))|C=set_union2(A,B)))))),inference(fof_nnf,[status(thm)],[d2_xboole_0])).
% 3.24/3.42 fof(c108,plain,((![A]:(![B]:(![C]:(C!=set_union2(A,B)|((![D]:(~in(D,C)|(in(D,A)|in(D,B))))&(![D]:((~in(D,A)&~in(D,B))|in(D,C))))))))&(![A]:(![B]:(![C]:((?[D]:((~in(D,C)|(~in(D,A)&~in(D,B)))&(in(D,C)|(in(D,A)|in(D,B)))))|C=set_union2(A,B)))))),inference(shift_quantors,[status(thm)],[c107])).
% 3.24/3.42 fof(c109,plain,((![X33]:(![X34]:(![X35]:(X35!=set_union2(X33,X34)|((![X36]:(~in(X36,X35)|(in(X36,X33)|in(X36,X34))))&(![X37]:((~in(X37,X33)&~in(X37,X34))|in(X37,X35))))))))&(![X38]:(![X39]:(![X40]:((?[X41]:((~in(X41,X40)|(~in(X41,X38)&~in(X41,X39)))&(in(X41,X40)|(in(X41,X38)|in(X41,X39)))))|X40=set_union2(X38,X39)))))),inference(variable_rename,[status(thm)],[c108])).
% 3.24/3.42 fof(c111,plain,(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:((X35!=set_union2(X33,X34)|((~in(X36,X35)|(in(X36,X33)|in(X36,X34)))&((~in(X37,X33)&~in(X37,X34))|in(X37,X35))))&(((~in(skolem0013(X38,X39,X40),X40)|(~in(skolem0013(X38,X39,X40),X38)&~in(skolem0013(X38,X39,X40),X39)))&(in(skolem0013(X38,X39,X40),X40)|(in(skolem0013(X38,X39,X40),X38)|in(skolem0013(X38,X39,X40),X39))))|X40=set_union2(X38,X39))))))))))),inference(shift_quantors,[status(thm)],[fof(c110,plain,((![X33]:(![X34]:(![X35]:(X35!=set_union2(X33,X34)|((![X36]:(~in(X36,X35)|(in(X36,X33)|in(X36,X34))))&(![X37]:((~in(X37,X33)&~in(X37,X34))|in(X37,X35))))))))&(![X38]:(![X39]:(![X40]:(((~in(skolem0013(X38,X39,X40),X40)|(~in(skolem0013(X38,X39,X40),X38)&~in(skolem0013(X38,X39,X40),X39)))&(in(skolem0013(X38,X39,X40),X40)|(in(skolem0013(X38,X39,X40),X38)|in(skolem0013(X38,X39,X40),X39))))|X40=set_union2(X38,X39)))))),inference(skolemize,[status(esa)],[c109])).])).
% 3.24/3.42 fof(c112,plain,(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:(((X35!=set_union2(X33,X34)|(~in(X36,X35)|(in(X36,X33)|in(X36,X34))))&((X35!=set_union2(X33,X34)|(~in(X37,X33)|in(X37,X35)))&(X35!=set_union2(X33,X34)|(~in(X37,X34)|in(X37,X35)))))&((((~in(skolem0013(X38,X39,X40),X40)|~in(skolem0013(X38,X39,X40),X38))|X40=set_union2(X38,X39))&((~in(skolem0013(X38,X39,X40),X40)|~in(skolem0013(X38,X39,X40),X39))|X40=set_union2(X38,X39)))&((in(skolem0013(X38,X39,X40),X40)|(in(skolem0013(X38,X39,X40),X38)|in(skolem0013(X38,X39,X40),X39)))|X40=set_union2(X38,X39)))))))))))),inference(distribute,[status(thm)],[c111])).
% 3.24/3.42 cnf(c115,plain,X140!=set_union2(X141,X138)|~in(X139,X138)|in(X139,X140),inference(split_conjunct,[status(thm)],[c112])).
% 3.24/3.42 fof(d1_ordinal1,axiom,(![A]:succ(A)=set_union2(A,singleton(A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_ordinal1)).
% 3.24/3.42 fof(c129,plain,(![X49]:succ(X49)=set_union2(X49,singleton(X49))),inference(variable_rename,[status(thm)],[d1_ordinal1])).
% 3.24/3.42 cnf(c130,plain,succ(X175)=set_union2(X175,singleton(X175)),inference(split_conjunct,[status(thm)],[c129])).
% 3.24/3.42 cnf(c480,plain,~in(X658,singleton(X657))|in(X658,succ(X657)),inference(resolution,[status(thm)],[c130, c115])).
% 3.24/3.42 cnf(c10771,plain,in(X659,succ(X659)),inference(resolution,[status(thm)],[c480, c4035])).
% 3.24/3.42 cnf(c10823,plain,$false,inference(resolution,[status(thm)],[c10771, c32])).
% 3.24/3.42 % SZS output end CNFRefutation
% 3.24/3.42
% 3.24/3.42 % Initial clauses : 73
% 3.24/3.42 % Processed clauses : 629
% 3.24/3.42 % Factors computed : 25
% 3.24/3.42 % Resolvents computed: 10654
% 3.24/3.42 % Tautologies deleted: 24
% 3.24/3.42 % Forward subsumed : 446
% 3.24/3.42 % Backward subsumed : 3
% 3.24/3.42 % -------- CPU Time ---------
% 3.24/3.42 % User time : 3.042 s
% 3.24/3.42 % System time : 0.031 s
% 3.24/3.42 % Total time : 3.073 s
%------------------------------------------------------------------------------