%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET062+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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:02 EDT 2024
% Result : Theorem 0.47s 0.67s
% Output : Refutation 0.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SET062+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n008.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.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 18:57:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.47/0.67 % Version: 1.5
% 0.47/0.67 % SZS status Theorem
% 0.47/0.67 % SZS output start CNFRefutation
% 0.47/0.67 fof(null_class_is_subclass,conjecture,(![X]:subclass(null_class,X)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', null_class_is_subclass)).
% 0.47/0.67 fof(c26,negated_conjecture,(~(![X]:subclass(null_class,X))),inference(assume_negation,[status(cth)],[null_class_is_subclass])).
% 0.47/0.67 fof(c27,negated_conjecture,(?[X]:~subclass(null_class,X)),inference(fof_nnf,[status(thm)],[c26])).
% 0.47/0.67 fof(c28,negated_conjecture,(?[X2]:~subclass(null_class,X2)),inference(variable_rename,[status(thm)],[c27])).
% 0.47/0.67 fof(c29,negated_conjecture,~subclass(null_class,skolem0001),inference(skolemize,[status(esa)],[c28])).
% 0.47/0.67 cnf(c30,negated_conjecture,~subclass(null_class,skolem0001),inference(split_conjunct,[status(thm)],[c29])).
% 0.47/0.67 fof(null_class_defn,axiom,(![X]:(~member(X,null_class))),file('/export/starexec/sandbox/benchmark/Axioms/SET005+0.ax', null_class_defn)).
% 0.47/0.67 fof(c177,plain,(![X]:~member(X,null_class)),inference(fof_simplification,[status(thm)],[null_class_defn])).
% 0.47/0.67 fof(c178,plain,(![X86]:~member(X86,null_class)),inference(variable_rename,[status(thm)],[c177])).
% 0.47/0.67 cnf(c179,plain,~member(X140,null_class),inference(split_conjunct,[status(thm)],[c178])).
% 0.47/0.67 fof(subclass_defn,axiom,(![X]:(![Y]:(subclass(X,Y)<=>(![U]:(member(U,X)=>member(U,Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/SET005+0.ax', subclass_defn)).
% 0.47/0.67 fof(c249,plain,(![X]:(![Y]:((~subclass(X,Y)|(![U]:(~member(U,X)|member(U,Y))))&((?[U]:(member(U,X)&~member(U,Y)))|subclass(X,Y))))),inference(fof_nnf,[status(thm)],[subclass_defn])).
% 0.47/0.67 fof(c250,plain,((![X]:(![Y]:(~subclass(X,Y)|(![U]:(~member(U,X)|member(U,Y))))))&(![X]:(![Y]:((?[U]:(member(U,X)&~member(U,Y)))|subclass(X,Y))))),inference(shift_quantors,[status(thm)],[c249])).
% 0.47/0.67 fof(c251,plain,((![X133]:(![X134]:(~subclass(X133,X134)|(![X135]:(~member(X135,X133)|member(X135,X134))))))&(![X136]:(![X137]:((?[X138]:(member(X138,X136)&~member(X138,X137)))|subclass(X136,X137))))),inference(variable_rename,[status(thm)],[c250])).
% 0.47/0.67 fof(c253,plain,(![X133]:(![X134]:(![X135]:(![X136]:(![X137]:((~subclass(X133,X134)|(~member(X135,X133)|member(X135,X134)))&((member(skolem0008(X136,X137),X136)&~member(skolem0008(X136,X137),X137))|subclass(X136,X137)))))))),inference(shift_quantors,[status(thm)],[fof(c252,plain,((![X133]:(![X134]:(~subclass(X133,X134)|(![X135]:(~member(X135,X133)|member(X135,X134))))))&(![X136]:(![X137]:((member(skolem0008(X136,X137),X136)&~member(skolem0008(X136,X137),X137))|subclass(X136,X137))))),inference(skolemize,[status(esa)],[c251])).])).
% 0.47/0.67 fof(c254,plain,(![X133]:(![X134]:(![X135]:(![X136]:(![X137]:((~subclass(X133,X134)|(~member(X135,X133)|member(X135,X134)))&((member(skolem0008(X136,X137),X136)|subclass(X136,X137))&(~member(skolem0008(X136,X137),X137)|subclass(X136,X137))))))))),inference(distribute,[status(thm)],[c253])).
% 0.47/0.67 cnf(c256,plain,member(skolem0008(X258,X257),X258)|subclass(X258,X257),inference(split_conjunct,[status(thm)],[c254])).
% 0.47/0.67 cnf(c456,plain,subclass(null_class,X259),inference(resolution,[status(thm)],[c256, c179])).
% 0.47/0.67 cnf(c459,plain,$false,inference(resolution,[status(thm)],[c456, c30])).
% 0.47/0.67 % SZS output end CNFRefutation
% 0.47/0.67
% 0.47/0.67 % Initial clauses : 119
% 0.47/0.67 % Processed clauses : 65
% 0.47/0.67 % Factors computed : 7
% 0.47/0.67 % Resolvents computed: 203
% 0.47/0.67 % Tautologies deleted: 4
% 0.47/0.67 % Forward subsumed : 15
% 0.47/0.67 % Backward subsumed : 1
% 0.47/0.67 % -------- CPU Time ---------
% 0.47/0.67 % User time : 0.300 s
% 0.47/0.67 % System time : 0.020 s
% 0.47/0.67 % Total time : 0.320 s
%------------------------------------------------------------------------------