%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM181-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:16:14 AM UTC 2026
% Result : Unsatisfiable 45.72s 6.38s
% Output : CNFRefutation 45.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 15
% Syntax : Number of formulae : 57 ( 37 unt; 0 def)
% Number of atoms : 83 ( 23 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 56 ( 30 ~; 26 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-3 aty)
% Number of variables : 65 ( 6 sgn 25 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(prove_null_class_is_not_a_limit_ordinal_1,axiom,
member(null_class,limit_ordinals),
file('theBenchmark.p',prove_null_class_is_not_a_limit_ordinal_1) ).
cnf(c_53,plain,
member(null_class,limit_ordinals),
inference(clausify,[status(thm)],[prove_null_class_is_not_a_limit_ordinal_1]) ).
fof(limit_ordinals,axiom,
intersection(complement(kind_1_ordinals),ordinal_numbers) = limit_ordinals,
file('theBenchmark.p',limit_ordinals) ).
cnf(c_75,plain,
intersection(complement(kind_1_ordinals),ordinal_numbers) = limit_ordinals,
inference(clausify,[status(thm)],[limit_ordinals]) ).
cnf(c_76,plain,
limit_ordinals = intersection(complement(kind_1_ordinals),ordinal_numbers),
inference(copy,[status(thm)],[c_75]) ).
fof(kind_1_ordinals,axiom,
union(singleton(null_class),image(successor_relation,ordinal_numbers)) = kind_1_ordinals,
file('theBenchmark.p',kind_1_ordinals) ).
cnf(c_77,plain,
union(singleton(null_class),image(successor_relation,ordinal_numbers)) = kind_1_ordinals,
inference(clausify,[status(thm)],[kind_1_ordinals]) ).
cnf(c_78,plain,
kind_1_ordinals = union(singleton(null_class),image(successor_relation,ordinal_numbers)),
inference(copy,[status(thm)],[c_77]) ).
fof(image,axiom,
! [VAR_0,VAR_1] : range_of(restrict(VAR_0,VAR_1,universal_class)) = image(VAR_0,VAR_1),
file('theBenchmark.p',image) ).
cnf(c_152,plain,
range_of(restrict(A,B,universal_class)) = image(A,B),
inference(clausify,[status(thm)],[image]) ).
cnf(c_153,plain,
image(A,B) = range_of(restrict(A,B,universal_class)),
inference(copy,[status(thm)],[c_152]) ).
fof(union,axiom,
! [VAR_0,VAR_1] : complement(intersection(complement(VAR_0),complement(VAR_1))) = union(VAR_0,VAR_1),
file('theBenchmark.p',union) ).
cnf(c_176,plain,
complement(intersection(complement(A),complement(B))) = union(A,B),
inference(clausify,[status(thm)],[union]) ).
cnf(c_177,plain,
union(A,B) = complement(intersection(complement(A),complement(B))),
inference(copy,[status(thm)],[c_176]) ).
fof(complement2,axiom,
! [VAR_0,VAR_1] :
( member(VAR_0,VAR_1)
| member(VAR_0,complement(VAR_1))
| ~ member(VAR_0,universal_class) ),
file('theBenchmark.p',complement2) ).
cnf(c_178,plain,
( member(A,B)
| member(A,complement(B))
| ~ member(A,universal_class) ),
inference(clausify,[status(thm)],[complement2]) ).
fof(complement1,axiom,
! [VAR_0,VAR_1] :
( ~ member(VAR_0,VAR_1)
| ~ member(VAR_0,complement(VAR_1)) ),
file('theBenchmark.p',complement1) ).
cnf(c_179,plain,
( ~ member(A,B)
| ~ member(A,complement(B)) ),
inference(clausify,[status(thm)],[complement1]) ).
fof(intersection2,axiom,
! [VAR_0,VAR_1,VAR_2] :
( member(VAR_0,VAR_2)
| ~ member(VAR_0,intersection(VAR_1,VAR_2)) ),
file('theBenchmark.p',intersection2) ).
cnf(c_181,plain,
( member(A,C)
| ~ member(A,intersection(B,C)) ),
inference(clausify,[status(thm)],[intersection2]) ).
fof(intersection1,axiom,
! [VAR_0,VAR_1,VAR_2] :
( member(VAR_0,VAR_1)
| ~ member(VAR_0,intersection(VAR_1,VAR_2)) ),
file('theBenchmark.p',intersection1) ).
cnf(c_182,plain,
( member(A,B)
| ~ member(A,intersection(B,C)) ),
inference(clausify,[status(thm)],[intersection1]) ).
fof(singleton_set,axiom,
! [VAR_0] : unordered_pair(VAR_0,VAR_0) = singleton(VAR_0),
file('theBenchmark.p',singleton_set) ).
cnf(c_192,plain,
unordered_pair(A,A) = singleton(A),
inference(clausify,[status(thm)],[singleton_set]) ).
cnf(c_193,plain,
singleton(A) = unordered_pair(A,A),
inference(copy,[status(thm)],[c_192]) ).
fof(unordered_pair2,axiom,
! [VAR_0,VAR_1] :
( member(VAR_0,unordered_pair(VAR_0,VAR_1))
| ~ member(VAR_0,universal_class) ),
file('theBenchmark.p',unordered_pair2) ).
cnf(c_196,plain,
( member(A,unordered_pair(A,B))
| ~ member(A,universal_class) ),
inference(clausify,[status(thm)],[unordered_pair2]) ).
fof(subclass_implies_equal,axiom,
! [VAR_0,VAR_1] :
( VAR_0 = VAR_1
| ~ subclass(VAR_1,VAR_0)
| ~ subclass(VAR_0,VAR_1) ),
file('theBenchmark.p',subclass_implies_equal) ).
cnf(c_198,plain,
( A = B
| ~ subclass(B,A)
| ~ subclass(A,B) ),
inference(clausify,[status(thm)],[subclass_implies_equal]) ).
fof(equal_implies_subclass2,axiom,
! [VAR_0,VAR_1] :
( subclass(VAR_1,VAR_0)
| VAR_0 != VAR_1 ),
file('theBenchmark.p',equal_implies_subclass2) ).
cnf(c_199,plain,
( subclass(B,A)
| A != B ),
inference(clausify,[status(thm)],[equal_implies_subclass2]) ).
fof(class_elements_are_sets,axiom,
! [VAR_0] : subclass(VAR_0,universal_class),
file('theBenchmark.p',class_elements_are_sets) ).
cnf(c_201,plain,
subclass(A,universal_class),
inference(clausify,[status(thm)],[class_elements_are_sets]) ).
fof(subclass_members,axiom,
! [VAR_0,VAR_1,VAR_2] :
( member(VAR_2,VAR_1)
| ~ member(VAR_2,VAR_0)
| ~ subclass(VAR_0,VAR_1) ),
file('theBenchmark.p',subclass_members) ).
cnf(c_204,plain,
( member(C,B)
| ~ member(C,A)
| ~ subclass(A,B) ),
inference(clausify,[status(thm)],[subclass_members]) ).
cnf(c_219,plain,
member(null_class,intersection(complement(kind_1_ordinals),ordinal_numbers)),
inference(paramod,[status(thm)],[c_76,c_53]) ).
cnf(c_406,plain,
subclass(unordered_pair(A,A),singleton(A)),
inference(resolve,[status(thm)],[c_199,c_193]) ).
cnf(c_22432,plain,
unordered_pair(A,A) = singleton(A),
inference(copy,[status(thm)],[c_193]) ).
cnf(c_436,plain,
subclass(singleton(A),unordered_pair(A,A)),
inference(resolve,[status(thm)],[c_199,c_22432]) ).
cnf(c_477,plain,
( member(A,universal_class)
| ~ member(A,B) ),
inference(resolve,[status(thm)],[c_204,c_201]) ).
cnf(c_526,plain,
member(null_class,complement(kind_1_ordinals)),
inference(resolve,[status(thm)],[c_219,c_182]) ).
cnf(c_527,plain,
member(null_class,ordinal_numbers),
inference(resolve,[status(thm)],[c_219,c_181]) ).
cnf(c_546,plain,
member(null_class,universal_class),
inference(resolve,[status(thm)],[c_477,c_527]) ).
cnf(c_581,plain,
member(null_class,unordered_pair(null_class,A)),
inference(resolve,[status(thm)],[c_546,c_196]) ).
cnf(c_587,plain,
( member(null_class,A)
| member(null_class,complement(A)) ),
inference(resolve,[status(thm)],[c_546,c_178]) ).
cnf(c_660,plain,
~ member(null_class,kind_1_ordinals),
inference(resolve,[status(thm)],[c_526,c_179]) ).
cnf(c_700,plain,
~ member(null_class,union(singleton(null_class),image(successor_relation,ordinal_numbers))),
inference(paramod,[status(thm)],[c_78,c_660]) ).
cnf(c_723,plain,
~ member(null_class,union(singleton(null_class),range_of(restrict(successor_relation,ordinal_numbers,universal_class)))),
inference(paramod,[status(thm)],[c_153,c_700]) ).
cnf(c_731,plain,
~ member(null_class,complement(intersection(complement(singleton(null_class)),complement(range_of(restrict(successor_relation,ordinal_numbers,universal_class)))))),
inference(paramod,[status(thm)],[c_177,c_723]) ).
cnf(c_22433,plain,
( singleton(A) = unordered_pair(A,A)
| ~ subclass(singleton(A),unordered_pair(A,A)) ),
inference(resolve,[status(thm)],[c_406,c_198]) ).
cnf(c_22434,plain,
( unordered_pair(A,A) = singleton(A)
| ~ subclass(singleton(A),unordered_pair(A,A)) ),
inference(copy,[status(thm)],[c_22433]) ).
cnf(c_822,plain,
unordered_pair(A,A) = singleton(A),
inference(resolve,[status(thm)],[c_436,c_22434]) ).
cnf(c_884,plain,
member(null_class,singleton(null_class)),
inference(paramod,[status(thm)],[c_822,c_581]) ).
cnf(c_1203,plain,
member(null_class,intersection(complement(singleton(null_class)),complement(range_of(restrict(successor_relation,ordinal_numbers,universal_class))))),
inference(resolve,[status(thm)],[c_587,c_731]) ).
cnf(c_22388,plain,
member(null_class,complement(singleton(null_class))),
inference(resolve,[status(thm)],[c_1203,c_182]) ).
cnf(c_22435,plain,
~ member(null_class,singleton(null_class)),
inference(resolve,[status(thm)],[c_22388,c_179]) ).
cnf(c_22431,plain,
$false,
inference(resolve,[status(thm)],[c_884,c_22435]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM181-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.38 % Computer : n016.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sat Sep 26 02:15:30 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.38 % Process 3982758 was started by sandbox on n016,
% 0.13/0.38 % Sat Sep 26 02:15:30 2026
% 0.13/0.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/0.39
% 0.13/0.39 % From the command line: assign(max_seconds, 300).
% 45.72/6.38
% 45.72/6.38 % given #500 (A,wt=20): 319 -member(A,B) | member(ordered_pair(null_class,A),cross_product(limit_ordinals,B)). [resolve(187,a,53,a)].
% 45.72/6.38
% 45.72/6.38 % given #1000 (T,wt=16): 10437 subclass(range_of(null_class),image(null_class,A)). [para(10414(a,1),416(a,1,1))].
% 45.72/6.38
% 45.72/6.38 % given #1500 (A,wt=26): 657 -member(A,B) | member(ordered_pair(null_class,A),cross_product(complement(kind_1_ordinals),B)). [resolve(526,a,187,a)].
% 45.72/6.38
% 45.72/6.38 % given #2000 (F,wt=65): 7210 -member(A,sum_class(null_class)) | -member(unordered_pair(singleton(A),unordered_pair(A,unordered_pair(least(element_relation,domain_of(restrict(element_relation,universal_class,null_class))),least(element_relation,domain_of(restrict(element_relation,universal_class,null_class)))))),element_relation). [para(372(a,1),794(b,1))].
% 45.72/6.38
% 45.72/6.38 % given #2500 (W,wt=22): 1752 member(null_class,intersection(unordered_pair(null_class,A),universal_class)). [resolve(585,a,581,a)].
% 45.72/6.38
% 45.72/6.38 % given #3000 (F,wt=56): 20772 -member(A,domain_of(restrict(null_class,B,ordered_pair(singleton(ordered_pair(singleton(C),C)),singleton(unordered_pair(unordered_pair(C,C),singleton(C))))))). [para(193(a,1),20757(a,2,1,3,2,1,1))].
% 45.72/6.38
% 45.72/6.38 % SZS status Unsatisfiable for theBenchmark
% 45.72/6.38
% 45.72/6.38 % Proof 1 at 4.26 (+ 1.61) seconds.
% 45.72/6.38 % Length of proof is 38.
% 45.72/6.38 % Level of proof is 10.
% 45.72/6.38 % Maximum clause weight is 43.000.
% 45.72/6.38 % Given clauses 3262.
% 45.72/6.38
% 45.72/6.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------