%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU230+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:53 EDT 2024
% Result : Theorem 3.31s 3.53s
% Output : Refutation 3.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU230+1 : 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 : n014.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 10:58:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 3.31/3.53 % Version: 1.5
% 3.31/3.53 % SZS status Theorem
% 3.31/3.53 % SZS output start CNFRefutation
% 3.31/3.53 fof(t10_ordinal1,conjecture,(![A]:in(A,succ(A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t10_ordinal1)).
% 3.31/3.53 fof(c27,negated_conjecture,(~(![A]:in(A,succ(A)))),inference(assume_negation,[status(cth)],[t10_ordinal1])).
% 3.31/3.53 fof(c28,negated_conjecture,(?[A]:~in(A,succ(A))),inference(fof_nnf,[status(thm)],[c27])).
% 3.31/3.53 fof(c29,negated_conjecture,(?[X12]:~in(X12,succ(X12))),inference(variable_rename,[status(thm)],[c28])).
% 3.31/3.53 fof(c30,negated_conjecture,~in(skolem0001,succ(skolem0001)),inference(skolemize,[status(esa)],[c29])).
% 3.31/3.53 cnf(c31,negated_conjecture,~in(skolem0001,succ(skolem0001)),inference(split_conjunct,[status(thm)],[c30])).
% 3.31/3.53 cnf(reflexivity,axiom,X56=X56,theory(equality)).
% 3.31/3.53 fof(d1_tarski,axiom,(![A]:(![B]:(B=singleton(A)<=>(![C]:(in(C,B)<=>C=A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_tarski)).
% 3.31/3.53 fof(c118,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.31/3.53 fof(c119,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)],[c118])).
% 3.31/3.53 fof(c120,plain,((![X41]:(![X42]:(X42!=singleton(X41)|((![X43]:(~in(X43,X42)|X43=X41))&(![X44]:(X44!=X41|in(X44,X42)))))))&(![X45]:(![X46]:((?[X47]:((~in(X47,X46)|X47!=X45)&(in(X47,X46)|X47=X45)))|X46=singleton(X45))))),inference(variable_rename,[status(thm)],[c119])).
% 3.31/3.53 fof(c122,plain,(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:((X42!=singleton(X41)|((~in(X43,X42)|X43=X41)&(X44!=X41|in(X44,X42))))&(((~in(skolem0013(X45,X46),X46)|skolem0013(X45,X46)!=X45)&(in(skolem0013(X45,X46),X46)|skolem0013(X45,X46)=X45))|X46=singleton(X45))))))))),inference(shift_quantors,[status(thm)],[fof(c121,plain,((![X41]:(![X42]:(X42!=singleton(X41)|((![X43]:(~in(X43,X42)|X43=X41))&(![X44]:(X44!=X41|in(X44,X42)))))))&(![X45]:(![X46]:(((~in(skolem0013(X45,X46),X46)|skolem0013(X45,X46)!=X45)&(in(skolem0013(X45,X46),X46)|skolem0013(X45,X46)=X45))|X46=singleton(X45))))),inference(skolemize,[status(esa)],[c120])).])).
% 3.31/3.53 fof(c123,plain,(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(((X42!=singleton(X41)|(~in(X43,X42)|X43=X41))&(X42!=singleton(X41)|(X44!=X41|in(X44,X42))))&(((~in(skolem0013(X45,X46),X46)|skolem0013(X45,X46)!=X45)|X46=singleton(X45))&((in(skolem0013(X45,X46),X46)|skolem0013(X45,X46)=X45)|X46=singleton(X45)))))))))),inference(distribute,[status(thm)],[c122])).
% 3.31/3.53 cnf(c125,plain,X159!=singleton(X158)|X157!=X158|in(X157,X159),inference(split_conjunct,[status(thm)],[c123])).
% 3.31/3.53 cnf(c420,plain,X340!=X341|in(X340,singleton(X341)),inference(resolution,[status(thm)],[c125, reflexivity])).
% 3.31/3.53 cnf(c3446,plain,in(X342,singleton(X342)),inference(resolution,[status(thm)],[c420, reflexivity])).
% 3.31/3.53 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/sandbox/benchmark/theBenchmark.p', d2_xboole_0)).
% 3.31/3.53 fof(c106,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.31/3.53 fof(c107,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)],[c106])).
% 3.31/3.53 fof(c108,plain,((![X32]:(![X33]:(![X34]:(X34!=set_union2(X32,X33)|((![X35]:(~in(X35,X34)|(in(X35,X32)|in(X35,X33))))&(![X36]:((~in(X36,X32)&~in(X36,X33))|in(X36,X34))))))))&(![X37]:(![X38]:(![X39]:((?[X40]:((~in(X40,X39)|(~in(X40,X37)&~in(X40,X38)))&(in(X40,X39)|(in(X40,X37)|in(X40,X38)))))|X39=set_union2(X37,X38)))))),inference(variable_rename,[status(thm)],[c107])).
% 3.31/3.53 fof(c110,plain,(![X32]:(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:((X34!=set_union2(X32,X33)|((~in(X35,X34)|(in(X35,X32)|in(X35,X33)))&((~in(X36,X32)&~in(X36,X33))|in(X36,X34))))&(((~in(skolem0012(X37,X38,X39),X39)|(~in(skolem0012(X37,X38,X39),X37)&~in(skolem0012(X37,X38,X39),X38)))&(in(skolem0012(X37,X38,X39),X39)|(in(skolem0012(X37,X38,X39),X37)|in(skolem0012(X37,X38,X39),X38))))|X39=set_union2(X37,X38))))))))))),inference(shift_quantors,[status(thm)],[fof(c109,plain,((![X32]:(![X33]:(![X34]:(X34!=set_union2(X32,X33)|((![X35]:(~in(X35,X34)|(in(X35,X32)|in(X35,X33))))&(![X36]:((~in(X36,X32)&~in(X36,X33))|in(X36,X34))))))))&(![X37]:(![X38]:(![X39]:(((~in(skolem0012(X37,X38,X39),X39)|(~in(skolem0012(X37,X38,X39),X37)&~in(skolem0012(X37,X38,X39),X38)))&(in(skolem0012(X37,X38,X39),X39)|(in(skolem0012(X37,X38,X39),X37)|in(skolem0012(X37,X38,X39),X38))))|X39=set_union2(X37,X38)))))),inference(skolemize,[status(esa)],[c108])).])).
% 3.31/3.53 fof(c111,plain,(![X32]:(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(((X34!=set_union2(X32,X33)|(~in(X35,X34)|(in(X35,X32)|in(X35,X33))))&((X34!=set_union2(X32,X33)|(~in(X36,X32)|in(X36,X34)))&(X34!=set_union2(X32,X33)|(~in(X36,X33)|in(X36,X34)))))&((((~in(skolem0012(X37,X38,X39),X39)|~in(skolem0012(X37,X38,X39),X37))|X39=set_union2(X37,X38))&((~in(skolem0012(X37,X38,X39),X39)|~in(skolem0012(X37,X38,X39),X38))|X39=set_union2(X37,X38)))&((in(skolem0012(X37,X38,X39),X39)|(in(skolem0012(X37,X38,X39),X37)|in(skolem0012(X37,X38,X39),X38)))|X39=set_union2(X37,X38)))))))))))),inference(distribute,[status(thm)],[c110])).
% 3.31/3.53 cnf(c114,plain,X135!=set_union2(X138,X136)|~in(X137,X136)|in(X137,X135),inference(split_conjunct,[status(thm)],[c111])).
% 3.31/3.53 fof(d1_ordinal1,axiom,(![A]:succ(A)=set_union2(A,singleton(A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_ordinal1)).
% 3.31/3.53 fof(c128,plain,(![X48]:succ(X48)=set_union2(X48,singleton(X48))),inference(variable_rename,[status(thm)],[d1_ordinal1])).
% 3.31/3.53 cnf(c129,plain,succ(X171)=set_union2(X171,singleton(X171)),inference(split_conjunct,[status(thm)],[c128])).
% 3.31/3.53 cnf(c467,plain,~in(X646,singleton(X647))|in(X646,succ(X647)),inference(resolution,[status(thm)],[c129, c114])).
% 3.31/3.53 cnf(c10302,plain,in(X648,succ(X648)),inference(resolution,[status(thm)],[c467, c3446])).
% 3.31/3.53 cnf(c10325,plain,$false,inference(resolution,[status(thm)],[c10302, c31])).
% 3.31/3.53 % SZS output end CNFRefutation
% 3.31/3.53
% 3.31/3.53 % Initial clauses : 74
% 3.31/3.53 % Processed clauses : 585
% 3.31/3.53 % Factors computed : 25
% 3.31/3.53 % Resolvents computed: 10164
% 3.31/3.53 % Tautologies deleted: 23
% 3.31/3.53 % Forward subsumed : 485
% 3.31/3.53 % Backward subsumed : 3
% 3.31/3.53 % -------- CPU Time ---------
% 3.31/3.53 % User time : 3.131 s
% 3.31/3.53 % System time : 0.030 s
% 3.31/3.53 % Total time : 3.161 s
%------------------------------------------------------------------------------