%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET507-6 : TPTP v8.1.2. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.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:41 EDT 2024
% Result : Unsatisfiable 3.39s 3.56s
% Output : Refutation 3.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 8
% Syntax : Number of clauses : 22 ( 11 unt; 3 nHn; 19 RR)
% Number of literals : 35 ( 6 equ; 12 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-1 aty)
% Number of variables : 17 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(class_elements_are_sets,axiom,
subclass(X3,universal_class),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',class_elements_are_sets) ).
cnf(subclass_members,axiom,
( ~ subclass(X6,X5)
| ~ member(X4,X6)
| member(X4,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',subclass_members) ).
cnf(omega_is_inductive1,axiom,
inductive(omega),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',omega_is_inductive1) ).
cnf(inductive1,axiom,
( ~ inductive(X19)
| member(null_class,X19) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',inductive1) ).
cnf(c49,plain,
member(null_class,omega),
inference(resolution,[status(thm)],[inductive1,omega_is_inductive1]) ).
cnf(c50,plain,
( ~ subclass(omega,X96)
| member(null_class,X96) ),
inference(resolution,[status(thm)],[c49,subclass_members]) ).
cnf(c126,plain,
member(null_class,universal_class),
inference(resolution,[status(thm)],[c50,class_elements_are_sets]) ).
cnf(complement1,axiom,
( ~ member(X61,complement(X60))
| ~ member(X61,X60) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',complement1) ).
cnf(prove_universal_class_not_subclass_of_null_class_1,negated_conjecture,
subclass(universal_class,null_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_universal_class_not_subclass_of_null_class_1) ).
cnf(c130,plain,
( ~ subclass(universal_class,X120)
| member(null_class,X120) ),
inference(resolution,[status(thm)],[c126,subclass_members]) ).
cnf(c189,plain,
member(null_class,null_class),
inference(resolution,[status(thm)],[c130,prove_universal_class_not_subclass_of_null_class_1]) ).
cnf(c195,plain,
( ~ subclass(null_class,X126)
| member(null_class,X126) ),
inference(resolution,[status(thm)],[c189,subclass_members]) ).
cnf(equal_implies_subclass2,axiom,
( X15 != X14
| subclass(X14,X15) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',equal_implies_subclass2) ).
cnf(regularity1,axiom,
( X133 = null_class
| member(regular(X133),X133) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',regularity1) ).
cnf(c234,plain,
( complement(X756) = null_class
| ~ member(regular(complement(X756)),X756) ),
inference(resolution,[status(thm)],[regularity1,complement1]) ).
cnf(c241,plain,
( X800 = null_class
| ~ subclass(X800,X799)
| member(regular(X800),X799) ),
inference(resolution,[status(thm)],[regularity1,subclass_members]) ).
cnf(c9378,plain,
( X802 = null_class
| member(regular(X802),universal_class) ),
inference(resolution,[status(thm)],[c241,class_elements_are_sets]) ).
cnf(c9507,plain,
complement(universal_class) = null_class,
inference(resolution,[status(thm)],[c9378,c234]) ).
cnf(c9555,plain,
subclass(null_class,complement(universal_class)),
inference(resolution,[status(thm)],[c9507,equal_implies_subclass2]) ).
cnf(c9575,plain,
member(null_class,complement(universal_class)),
inference(resolution,[status(thm)],[c9555,c195]) ).
cnf(c9680,plain,
~ member(null_class,universal_class),
inference(resolution,[status(thm)],[c9575,complement1]) ).
cnf(c9694,plain,
$false,
inference(resolution,[status(thm)],[c9680,c126]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SET507-6 : TPTP v8.1.2. Bugfixed v2.1.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n017.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.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 18:53:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 3.39/3.56 % Version: 1.5
% 3.39/3.56 % SZS status Unsatisfiable
% 3.39/3.56 % SZS output start CNFRefutation
% See solution above
% 3.39/3.56
% 3.39/3.56 % Initial clauses : 160
% 3.39/3.56 % Processed clauses : 773
% 3.39/3.56 % Factors computed : 29
% 3.39/3.56 % Resolvents computed: 9627
% 3.39/3.56 % Tautologies deleted: 9
% 3.39/3.56 % Forward subsumed : 326
% 3.39/3.56 % Backward subsumed : 5
% 3.39/3.56 % -------- CPU Time ---------
% 3.39/3.56 % User time : 3.188 s
% 3.39/3.56 % System time : 0.026 s
% 3.39/3.56 % Total time : 3.214 s
%------------------------------------------------------------------------------