%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET093-7 : TPTP v8.1.2. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:10 EDT 2024
% Result : Unsatisfiable 62.94s 63.17s
% Output : Refutation 62.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 11
% Syntax : Number of clauses : 21 ( 12 unt; 1 nHn; 17 RR)
% Number of literals : 34 ( 14 equ; 14 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 4 ( 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 : 23 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(existence_of_null_class,axiom,
~ member(X8,null_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_of_null_class) ).
cnf(subclass_members,axiom,
( ~ subclass(X5,X7)
| ~ member(X6,X5)
| member(X6,X7) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',subclass_members) ).
cnf(singletons_are_sets,axiom,
member(singleton(X15),universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singletons_are_sets) ).
cnf(set_in_its_singleton,axiom,
( ~ member(X171,universal_class)
| member(X171,singleton(X171)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',set_in_its_singleton) ).
cnf(c298,plain,
member(singleton(X174),singleton(singleton(X174))),
inference(resolution,[status(thm)],[set_in_its_singleton,singletons_are_sets]) ).
cnf(c307,plain,
( ~ subclass(singleton(singleton(X1568)),X1569)
| member(singleton(X1568),X1569) ),
inference(resolution,[status(thm)],[c298,subclass_members]) ).
cnf(prove_corollary_2_to_singletons_are_sets_2,negated_conjecture,
~ member(x,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_corollary_2_to_singletons_are_sets_2) ).
cnf(singleton_is_null_class,axiom,
( member(X301,universal_class)
| singleton(X301) = null_class ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_is_null_class) ).
cnf(c793,plain,
singleton(x) = null_class,
inference(resolution,[status(thm)],[singleton_is_null_class,prove_corollary_2_to_singletons_are_sets_2]) ).
cnf(subclass_is_reflexive,axiom,
subclass(X2,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_is_reflexive) ).
cnf(c32,axiom,
( X667 != X666
| X665 != X664
| ~ subclass(X667,X665)
| subclass(X666,X664) ),
theory(equality) ).
cnf(c5239,plain,
( X832 != X831
| X832 != X833
| subclass(X831,X833) ),
inference(resolution,[status(thm)],[c32,subclass_is_reflexive]) ).
cnf(c8470,plain,
( singleton(x) != X1600
| subclass(X1600,null_class) ),
inference(resolution,[status(thm)],[c5239,c793]) ).
cnf(symmetry,axiom,
( X44 != X45
| X45 = X44 ),
theory(equality) ).
cnf(prove_corollary_2_to_singletons_are_sets_1,negated_conjecture,
singleton(member_of(x)) = x,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_corollary_2_to_singletons_are_sets_1) ).
cnf(c120,plain,
x = singleton(member_of(x)),
inference(resolution,[status(thm)],[prove_corollary_2_to_singletons_are_sets_1,symmetry]) ).
cnf(c2,axiom,
( X334 != X333
| singleton(X334) = singleton(X333) ),
theory(equality) ).
cnf(c1023,plain,
singleton(x) = singleton(singleton(member_of(x))),
inference(resolution,[status(thm)],[c2,c120]) ).
cnf(c67676,plain,
subclass(singleton(singleton(member_of(x))),null_class),
inference(resolution,[status(thm)],[c1023,c8470]) ).
cnf(c67705,plain,
member(singleton(member_of(x)),null_class),
inference(resolution,[status(thm)],[c67676,c307]) ).
cnf(c67751,plain,
$false,
inference(resolution,[status(thm)],[c67705,existence_of_null_class]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SET093-7 : TPTP v8.1.2. Bugfixed v2.1.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n003.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 19:23:53 EDT 2024
% 0.14/0.36 % CPUTime :
% 62.94/63.17 % Version: 1.5
% 62.94/63.17 % SZS status Unsatisfiable
% 62.94/63.17 % SZS output start CNFRefutation
% See solution above
% 62.94/63.17
% 62.94/63.17 % Initial clauses : 182
% 62.94/63.17 % Processed clauses : 1896
% 62.94/63.17 % Factors computed : 39
% 62.94/63.17 % Resolvents computed: 67696
% 62.94/63.17 % Tautologies deleted: 15
% 62.94/63.17 % Forward subsumed : 2753
% 62.94/63.17 % Backward subsumed : 39
% 62.94/63.17 % -------- CPU Time ---------
% 62.94/63.17 % User time : 62.658 s
% 62.94/63.17 % System time : 0.158 s
% 62.94/63.17 % Total time : 62.816 s
%------------------------------------------------------------------------------