%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET506-6 : TPTP v8.1.2. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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:40 EDT 2024
% Result : Unsatisfiable 3.69s 3.86s
% Output : Refutation 3.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 8
% Syntax : Number of clauses : 20 ( 10 unt; 3 nHn; 17 RR)
% Number of literals : 32 ( 8 equ; 11 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 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(omega_in_universal,axiom,
member(omega,universal_class),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',omega_in_universal) ).
cnf(complement1,axiom,
( ~ member(X62,complement(X63))
| ~ member(X62,X63) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',complement1) ).
cnf(subclass_members,axiom,
( ~ subclass(X6,X4)
| ~ member(X5,X6)
| member(X5,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',subclass_members) ).
cnf(prove_universal_class_not_null_class_1,negated_conjecture,
universal_class = null_class,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_universal_class_not_null_class_1) ).
cnf(equal_implies_subclass1,axiom,
( X10 != X9
| subclass(X10,X9) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',equal_implies_subclass1) ).
cnf(c46,plain,
subclass(universal_class,null_class),
inference(resolution,[status(thm)],[equal_implies_subclass1,prove_universal_class_not_null_class_1]) ).
cnf(c44,plain,
( ~ subclass(universal_class,X100)
| member(omega,X100) ),
inference(resolution,[status(thm)],[subclass_members,omega_in_universal]) ).
cnf(c137,plain,
member(omega,null_class),
inference(resolution,[status(thm)],[c44,c46]) ).
cnf(c142,plain,
( ~ subclass(null_class,X116)
| member(omega,X116) ),
inference(resolution,[status(thm)],[c137,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(c243,plain,
( complement(X813) = null_class
| ~ member(regular(complement(X813)),X813) ),
inference(resolution,[status(thm)],[regularity1,complement1]) ).
cnf(class_elements_are_sets,axiom,
subclass(X3,universal_class),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',class_elements_are_sets) ).
cnf(c244,plain,
( X819 = null_class
| ~ subclass(X819,X820)
| member(regular(X819),X820) ),
inference(resolution,[status(thm)],[regularity1,subclass_members]) ).
cnf(c10239,plain,
( X822 = null_class
| member(regular(X822),universal_class) ),
inference(resolution,[status(thm)],[c244,class_elements_are_sets]) ).
cnf(c10330,plain,
complement(universal_class) = null_class,
inference(resolution,[status(thm)],[c10239,c243]) ).
cnf(c10337,plain,
subclass(null_class,complement(universal_class)),
inference(resolution,[status(thm)],[c10330,equal_implies_subclass2]) ).
cnf(c10379,plain,
member(omega,complement(universal_class)),
inference(resolution,[status(thm)],[c10337,c142]) ).
cnf(c10496,plain,
~ member(omega,universal_class),
inference(resolution,[status(thm)],[c10379,complement1]) ).
cnf(c10510,plain,
$false,
inference(resolution,[status(thm)],[c10496,omega_in_universal]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SET506-6 : TPTP v8.1.2. Bugfixed v2.1.0.
% 0.15/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n021.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Wed May 8 18:51:08 EDT 2024
% 0.22/0.37 % CPUTime :
% 3.69/3.86 % Version: 1.5
% 3.69/3.86 % SZS status Unsatisfiable
% 3.69/3.86 % SZS output start CNFRefutation
% See solution above
% 3.69/3.86
% 3.69/3.86 % Initial clauses : 160
% 3.69/3.86 % Processed clauses : 790
% 3.69/3.86 % Factors computed : 29
% 3.69/3.86 % Resolvents computed: 10438
% 3.69/3.86 % Tautologies deleted: 9
% 3.69/3.86 % Forward subsumed : 327
% 3.69/3.86 % Backward subsumed : 5
% 3.69/3.86 % -------- CPU Time ---------
% 3.69/3.86 % User time : 3.460 s
% 3.69/3.86 % System time : 0.028 s
% 3.69/3.86 % Total time : 3.488 s
%------------------------------------------------------------------------------