%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET062-6 : TPTP v8.1.2. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n002.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 : Unsatisfiable 2.78s 2.98s
% Output : Refutation 2.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 7
% Syntax : Number of clauses : 20 ( 9 unt; 6 nHn; 14 RR)
% Number of literals : 34 ( 6 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 : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 21 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_null_class_is_subclass_1,negated_conjecture,
~ subclass(null_class,x),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_null_class_is_subclass_1) ).
cnf(class_elements_are_sets,axiom,
subclass(X3,universal_class),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',class_elements_are_sets) ).
cnf(subclass_members,axiom,
( ~ subclass(X5,X6)
| ~ member(X4,X5)
| member(X4,X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',subclass_members) ).
cnf(not_subclass_members1,axiom,
( member(not_subclass_element(X12,X13),X12)
| subclass(X12,X13) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',not_subclass_members1) ).
cnf(c41,plain,
( subclass(X557,X556)
| ~ subclass(X557,X558)
| member(not_subclass_element(X557,X556),X558) ),
inference(resolution,[status(thm)],[not_subclass_members1,subclass_members]) ).
cnf(c3607,plain,
( subclass(X561,X562)
| member(not_subclass_element(X561,X562),universal_class) ),
inference(resolution,[status(thm)],[c41,class_elements_are_sets]) ).
cnf(c3625,plain,
member(not_subclass_element(null_class,x),universal_class),
inference(resolution,[status(thm)],[c3607,prove_null_class_is_subclass_1]) ).
cnf(complement1,axiom,
( ~ member(X57,complement(X58))
| ~ member(X57,X58) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',complement1) ).
cnf(c42,plain,
member(not_subclass_element(null_class,x),null_class),
inference(resolution,[status(thm)],[not_subclass_members1,prove_null_class_is_subclass_1]) ).
cnf(c110,plain,
( ~ subclass(null_class,X677)
| member(not_subclass_element(null_class,x),X677) ),
inference(resolution,[status(thm)],[c42,subclass_members]) ).
cnf(equal_implies_subclass2,axiom,
( X14 != X15
| subclass(X15,X14) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',equal_implies_subclass2) ).
cnf(regularity1,axiom,
( X122 = null_class
| member(regular(X122),X122) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',regularity1) ).
cnf(c185,plain,
( X833 = null_class
| ~ subclass(X833,X832)
| member(regular(X833),X832) ),
inference(resolution,[status(thm)],[regularity1,subclass_members]) ).
cnf(c6706,plain,
( X835 = null_class
| member(regular(X835),universal_class) ),
inference(resolution,[status(thm)],[c185,class_elements_are_sets]) ).
cnf(c189,plain,
( complement(X862) = null_class
| ~ member(regular(complement(X862)),X862) ),
inference(resolution,[status(thm)],[regularity1,complement1]) ).
cnf(c7151,plain,
complement(universal_class) = null_class,
inference(resolution,[status(thm)],[c189,c6706]) ).
cnf(c7182,plain,
subclass(null_class,complement(universal_class)),
inference(resolution,[status(thm)],[c7151,equal_implies_subclass2]) ).
cnf(c7237,plain,
member(not_subclass_element(null_class,x),complement(universal_class)),
inference(resolution,[status(thm)],[c7182,c110]) ).
cnf(c8770,plain,
~ member(not_subclass_element(null_class,x),universal_class),
inference(resolution,[status(thm)],[c7237,complement1]) ).
cnf(c8777,plain,
$false,
inference(resolution,[status(thm)],[c8770,c3625]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SET062-6 : TPTP v8.1.2. Bugfixed v2.1.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n002.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 18:32:53 EDT 2024
% 0.14/0.36 % CPUTime :
% 2.78/2.98 % Version: 1.5
% 2.78/2.98 % SZS status Unsatisfiable
% 2.78/2.98 % SZS output start CNFRefutation
% See solution above
% 2.78/2.98
% 2.78/2.98 % Initial clauses : 134
% 2.78/2.98 % Processed clauses : 531
% 2.78/2.98 % Factors computed : 30
% 2.78/2.98 % Resolvents computed: 8709
% 2.78/2.98 % Tautologies deleted: 9
% 2.78/2.98 % Forward subsumed : 313
% 2.78/2.98 % Backward subsumed : 4
% 2.78/2.98 % -------- CPU Time ---------
% 2.78/2.98 % User time : 2.581 s
% 2.78/2.98 % System time : 0.037 s
% 2.78/2.98 % Total time : 2.618 s
%------------------------------------------------------------------------------