%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SET071-6 : 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 : n001.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:35:37 AM UTC 2026
% Result : Unsatisfiable 22.72s 4.21s
% Output : CNFRefutation 22.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 10
% Syntax : Number of formulae : 64 ( 20 unt; 0 def)
% Number of atoms : 122 ( 54 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 93 ( 35 ~; 58 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 57 ( 7 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(prove_null_unordered_pair_3,axiom,
~ member(y,universal_class),
file('theBenchmark.p',prove_null_unordered_pair_3) ).
cnf(c_34,plain,
~ member(y,universal_class),
inference(clausify,[status(thm)],[prove_null_unordered_pair_3]) ).
fof(prove_null_unordered_pair_2,axiom,
~ member(x,universal_class),
file('theBenchmark.p',prove_null_unordered_pair_2) ).
cnf(c_35,plain,
~ member(x,universal_class),
inference(clausify,[status(thm)],[prove_null_unordered_pair_2]) ).
fof(prove_null_unordered_pair_1,axiom,
unordered_pair(x,y) != null_class,
file('theBenchmark.p',prove_null_unordered_pair_1) ).
cnf(c_36,plain,
unordered_pair(x,y) != null_class,
inference(clausify,[status(thm)],[prove_null_unordered_pair_1]) ).
fof(regularity1,axiom,
! [VAR_0] :
( member(regular(VAR_0),VAR_0)
| VAR_0 = null_class ),
file('theBenchmark.p',regularity1) ).
cnf(c_53,plain,
( member(regular(A),A)
| A = null_class ),
inference(clausify,[status(thm)],[regularity1]) ).
cnf(c_54,plain,
( member(regular(A),A)
| null_class = A ),
inference(copy,[status(thm)],[c_53]) ).
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_96,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_97,plain,
( ~ member(A,B)
| ~ member(A,complement(B)) ),
inference(clausify,[status(thm)],[complement1]) ).
fof(unordered_pair_member,axiom,
! [VAR_0,VAR_1,VAR_2] :
( VAR_0 = VAR_2
| VAR_0 = VAR_1
| ~ member(VAR_0,unordered_pair(VAR_1,VAR_2)) ),
file('theBenchmark.p',unordered_pair_member) ).
cnf(c_115,plain,
( A = C
| A = B
| ~ member(A,unordered_pair(B,C)) ),
inference(clausify,[status(thm)],[unordered_pair_member]) ).
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_117,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_119,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_122,plain,
( member(C,B)
| ~ member(C,A)
| ~ subclass(A,B) ),
inference(clausify,[status(thm)],[subclass_members]) ).
cnf(c_206,plain,
( null_class = A
| ~ member(regular(A),complement(A)) ),
inference(resolve,[status(thm)],[c_97,c_54]) ).
cnf(c_29197,plain,
( null_class = unordered_pair(A,B)
| regular(unordered_pair(A,B)) = B
| regular(unordered_pair(A,B)) = A ),
inference(resolve,[status(thm)],[c_115,c_54]) ).
cnf(c_232,plain,
( unordered_pair(A,B) = null_class
| regular(unordered_pair(A,B)) = B
| regular(unordered_pair(A,B)) = A ),
inference(copy,[status(thm)],[c_29197]) ).
cnf(c_235,plain,
( unordered_pair(A,A) = null_class
| regular(unordered_pair(A,A)) = A ),
inference(factor,[status(thm)],[c_232]) ).
cnf(c_251,plain,
subclass(A,A),
inference(xxres,[status(thm)],[c_117]) ).
cnf(c_256,plain,
( member(A,universal_class)
| ~ member(A,B) ),
inference(resolve,[status(thm)],[c_122,c_119]) ).
cnf(c_29198,plain,
( member(A,universal_class)
| ~ member(A,B) ),
inference(resolve,[status(thm)],[c_122,c_119]) ).
cnf(c_266,plain,
~ member(x,A),
inference(resolve,[status(thm)],[c_29198,c_35]) ).
cnf(c_29199,plain,
( member(A,universal_class)
| ~ member(A,B) ),
inference(resolve,[status(thm)],[c_122,c_119]) ).
cnf(c_267,plain,
~ member(y,A),
inference(resolve,[status(thm)],[c_29199,c_34]) ).
cnf(c_397,plain,
( null_class = A
| member(regular(A),universal_class) ),
inference(resolve,[status(thm)],[c_256,c_54]) ).
cnf(c_29200,plain,
null_class != unordered_pair(x,y),
inference(copy,[status(thm)],[c_36]) ).
cnf(c_477,plain,
~ member(regular(unordered_pair(x,y)),complement(unordered_pair(x,y))),
inference(resolve,[status(thm)],[c_206,c_29200]) ).
cnf(c_636,plain,
( member(regular(A),B)
| member(regular(A),complement(B))
| null_class = A ),
inference(resolve,[status(thm)],[c_397,c_96]) ).
cnf(c_29201,plain,
( null_class = unordered_pair(A,A)
| member(A,universal_class)
| unordered_pair(A,A) = null_class ),
inference(paramod,[status(thm)],[c_235,c_397]) ).
cnf(c_29202,plain,
( unordered_pair(A,A) = null_class
| member(A,universal_class)
| unordered_pair(A,A) = null_class ),
inference(copy,[status(thm)],[c_29201]) ).
cnf(c_1142,plain,
( member(A,universal_class)
| unordered_pair(A,A) = null_class ),
inference(copy,[status(thm)],[c_29202]) ).
cnf(c_1781,plain,
unordered_pair(x,x) = null_class,
inference(resolve,[status(thm)],[c_1142,c_266]) ).
cnf(c_29203,plain,
( member(regular(unordered_pair(x,y)),unordered_pair(x,y))
| null_class = unordered_pair(x,y) ),
inference(resolve,[status(thm)],[c_477,c_636]) ).
cnf(c_29204,plain,
( member(regular(unordered_pair(x,y)),unordered_pair(x,y))
| unordered_pair(x,y) = null_class ),
inference(copy,[status(thm)],[c_29203]) ).
cnf(c_10145,plain,
member(regular(unordered_pair(x,y)),unordered_pair(x,y)),
inference(resolve,[status(thm)],[c_36,c_29204]) ).
cnf(c_29187,plain,
( member(regular(unordered_pair(x,y)),A)
| ~ subclass(unordered_pair(x,y),A) ),
inference(resolve,[status(thm)],[c_10145,c_122]) ).
cnf(c_29188,plain,
( regular(unordered_pair(x,y)) = y
| regular(unordered_pair(x,y)) = x ),
inference(resolve,[status(thm)],[c_10145,c_115]) ).
cnf(c_29205,plain,
( member(x,unordered_pair(x,y))
| unordered_pair(x,y) = null_class
| regular(unordered_pair(x,y)) = y ),
inference(paramod,[status(thm)],[c_232,c_10145]) ).
cnf(c_29206,plain,
( member(x,unordered_pair(x,y))
| regular(unordered_pair(x,y)) = y ),
inference(resolve,[status(thm)],[c_36,c_29205]) ).
cnf(c_29191,plain,
regular(unordered_pair(x,y)) = y,
inference(resolve,[status(thm)],[c_266,c_29206]) ).
cnf(c_29207,plain,
( member(y,unordered_pair(x,y))
| unordered_pair(x,y) = null_class
| regular(unordered_pair(x,y)) = x ),
inference(paramod,[status(thm)],[c_232,c_10145]) ).
cnf(c_29208,plain,
( member(y,unordered_pair(x,y))
| unordered_pair(x,y) = null_class
| y = x ),
inference(paramod,[status(thm)],[c_29191,c_29207]) ).
cnf(c_29209,plain,
( member(y,unordered_pair(x,y))
| y = x ),
inference(resolve,[status(thm)],[c_36,c_29208]) ).
cnf(c_29192,plain,
y = x,
inference(resolve,[status(thm)],[c_267,c_29209]) ).
cnf(c_29210,plain,
( regular(unordered_pair(x,y)) = y
| regular(unordered_pair(x,x)) = x ),
inference(paramod,[status(thm)],[c_29192,c_29188]) ).
cnf(c_29211,plain,
( regular(unordered_pair(x,y)) = y
| regular(null_class) = x ),
inference(paramod,[status(thm)],[c_1781,c_29210]) ).
cnf(c_29212,plain,
( regular(unordered_pair(x,x)) = y
| regular(null_class) = x ),
inference(paramod,[status(thm)],[c_29192,c_29211]) ).
cnf(c_29213,plain,
( regular(null_class) = y
| regular(null_class) = x ),
inference(paramod,[status(thm)],[c_1781,c_29212]) ).
cnf(c_29214,plain,
( regular(null_class) = x
| regular(null_class) = x ),
inference(paramod,[status(thm)],[c_29192,c_29213]) ).
cnf(c_29194,plain,
regular(null_class) = x,
inference(copy,[status(thm)],[c_29214]) ).
cnf(c_29215,plain,
( member(regular(unordered_pair(x,y)),A)
| ~ subclass(unordered_pair(x,x),A) ),
inference(paramod,[status(thm)],[c_29192,c_29187]) ).
cnf(c_29216,plain,
( member(regular(unordered_pair(x,y)),A)
| ~ subclass(null_class,A) ),
inference(paramod,[status(thm)],[c_1781,c_29215]) ).
cnf(c_29217,plain,
( member(regular(unordered_pair(x,x)),A)
| ~ subclass(null_class,A) ),
inference(paramod,[status(thm)],[c_29192,c_29216]) ).
cnf(c_29218,plain,
( member(regular(null_class),A)
| ~ subclass(null_class,A) ),
inference(paramod,[status(thm)],[c_1781,c_29217]) ).
cnf(c_29219,plain,
( member(x,A)
| ~ subclass(null_class,A) ),
inference(paramod,[status(thm)],[c_29194,c_29218]) ).
cnf(c_29195,plain,
~ subclass(null_class,A),
inference(resolve,[status(thm)],[c_266,c_29219]) ).
cnf(c_29196,plain,
$false,
inference(resolve,[status(thm)],[c_29195,c_251]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET071-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n001.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 07:08:14 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 1188097 was started by sandbox on n001,
% 0.10/0.37 % Sat Sep 26 07:08:14 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.38
% 0.10/0.38 % From the command line: assign(max_seconds, 300).
% 22.72/4.21
% 22.72/4.21 % given #500 (T,wt=20): 1398 member(null_class,A) | member(not_subclass_element(universal_class,A),intersection(universal_class,universal_class)). [resolve(463,b,184,a)].
% 22.72/4.21
% 22.72/4.21 % given #1000 (F,wt=22): 3867 -member(null_class,unordered_pair(cross_product(universal_class,universal_class),omega)). [ur(115,b,3842,a(flip),c,664,a(flip))].
% 22.72/4.21
% 22.72/4.21 % given #1500 (T,wt=22): 18779 element_relation = null_class | member(not_subclass_element(universal_class,identity_relation),universal_class) | member(regular(element_relation),subset_relation). [resolve(2238,b,324,a)].
% 22.72/4.21
% 22.72/4.21 % SZS status Unsatisfiable for theBenchmark
% 22.72/4.21
% 22.72/4.21 % Proof 1 at 2.97 (+ 0.82) seconds.
% 22.72/4.21 % Length of proof is 31.
% 22.72/4.21 % Level of proof is 9.
% 22.72/4.21 % Maximum clause weight is 32.000.
% 22.72/4.21 % Given clauses 1915.
% 22.72/4.21
% 22.72/4.21 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------