%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET086+1 : TPTP v8.1.2. Bugfixed v5.4.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:39:09 EDT 2024
% Result : Theorem 0.57s 0.81s
% Output : Refutation 0.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : SET086+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.09/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n013.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 18:54:08 EDT 2024
% 0.15/0.37 % CPUTime :
% 0.57/0.81 % Version: 1.5
% 0.57/0.81 % SZS status Theorem
% 0.57/0.81 % SZS output start CNFRefutation
% 0.57/0.81 cnf(reflexivity,axiom,X142=X142,theory(equality)).
% 0.57/0.81 fof(member_of_substitution,conjecture,(![X]:(?[U]:((member(U,universal_class)&X=singleton(U))|((~(?[Y]:(member(Y,universal_class)&X=singleton(Y))))&U=X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', member_of_substitution)).
% 0.57/0.81 fof(c26,negated_conjecture,(~(![X]:(?[U]:((member(U,universal_class)&X=singleton(U))|((~(?[Y]:(member(Y,universal_class)&X=singleton(Y))))&U=X))))),inference(assume_negation,[status(cth)],[member_of_substitution])).
% 0.57/0.81 fof(c27,negated_conjecture,(?[X]:(![U]:((~member(U,universal_class)|X!=singleton(U))&((?[Y]:(member(Y,universal_class)&X=singleton(Y)))|U!=X)))),inference(fof_nnf,[status(thm)],[c26])).
% 0.57/0.81 fof(c28,negated_conjecture,(?[X]:((![U]:(~member(U,universal_class)|X!=singleton(U)))&((?[Y]:(member(Y,universal_class)&X=singleton(Y)))|(![U]:U!=X)))),inference(shift_quantors,[status(thm)],[c27])).
% 0.57/0.81 fof(c29,negated_conjecture,(?[X2]:((![X3]:(~member(X3,universal_class)|X2!=singleton(X3)))&((?[X4]:(member(X4,universal_class)&X2=singleton(X4)))|(![X5]:X5!=X2)))),inference(variable_rename,[status(thm)],[c28])).
% 0.57/0.81 fof(c31,negated_conjecture,(![X3]:(![X5]:((~member(X3,universal_class)|skolem0001!=singleton(X3))&((member(skolem0002,universal_class)&skolem0001=singleton(skolem0002))|X5!=skolem0001)))),inference(shift_quantors,[status(thm)],[fof(c30,negated_conjecture,((![X3]:(~member(X3,universal_class)|skolem0001!=singleton(X3)))&((member(skolem0002,universal_class)&skolem0001=singleton(skolem0002))|(![X5]:X5!=skolem0001))),inference(skolemize,[status(esa)],[c29])).])).
% 0.57/0.81 fof(c32,negated_conjecture,(![X3]:(![X5]:((~member(X3,universal_class)|skolem0001!=singleton(X3))&((member(skolem0002,universal_class)|X5!=skolem0001)&(skolem0001=singleton(skolem0002)|X5!=skolem0001))))),inference(distribute,[status(thm)],[c31])).
% 0.57/0.81 cnf(c34,negated_conjecture,member(skolem0002,universal_class)|X209!=skolem0001,inference(split_conjunct,[status(thm)],[c32])).
% 0.57/0.81 cnf(c329,plain,member(skolem0002,universal_class),inference(resolution,[status(thm)],[c34, reflexivity])).
% 0.57/0.81 cnf(c33,negated_conjecture,~member(X323,universal_class)|skolem0001!=singleton(X323),inference(split_conjunct,[status(thm)],[c32])).
% 0.57/0.81 cnf(c35,negated_conjecture,skolem0001=singleton(skolem0002)|X368!=skolem0001,inference(split_conjunct,[status(thm)],[c32])).
% 0.57/0.81 cnf(c802,plain,skolem0001=singleton(skolem0002),inference(resolution,[status(thm)],[c35, reflexivity])).
% 0.57/0.81 cnf(c816,plain,~member(skolem0002,universal_class),inference(resolution,[status(thm)],[c802, c33])).
% 0.57/0.81 cnf(c831,plain,$false,inference(resolution,[status(thm)],[c816, c329])).
% 0.57/0.81 % SZS output end CNFRefutation
% 0.57/0.81
% 0.57/0.81 % Initial clauses : 121
% 0.57/0.81 % Processed clauses : 111
% 0.57/0.81 % Factors computed : 12
% 0.57/0.81 % Resolvents computed: 557
% 0.57/0.81 % Tautologies deleted: 4
% 0.57/0.81 % Forward subsumed : 49
% 0.57/0.81 % Backward subsumed : 3
% 0.57/0.81 % -------- CPU Time ---------
% 0.57/0.81 % User time : 0.381 s
% 0.57/0.81 % System time : 0.013 s
% 0.57/0.81 % Total time : 0.394 s
%------------------------------------------------------------------------------