%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SET085-7 : 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 : n007.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:42 AM UTC 2026
% Result : Unsatisfiable 3.23s 0.88s
% Output : CNFRefutation 3.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 12
% Syntax : Number of formulae : 41 ( 20 unt; 0 def)
% Number of atoms : 67 ( 37 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 52 ( 26 ~; 26 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 36 ( 1 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(prove_singleton_in_unordered_pair3_4,axiom,
x != z,
file('theBenchmark.p',prove_singleton_in_unordered_pair3_4) ).
cnf(c_33,plain,
x != z,
inference(clausify,[status(thm)],[prove_singleton_in_unordered_pair3_4]) ).
cnf(c_34,plain,
z != x,
inference(copy,[status(thm)],[c_33]) ).
fof(prove_singleton_in_unordered_pair3_3,axiom,
x != y,
file('theBenchmark.p',prove_singleton_in_unordered_pair3_3) ).
cnf(c_35,plain,
x != y,
inference(clausify,[status(thm)],[prove_singleton_in_unordered_pair3_3]) ).
cnf(c_36,plain,
y != x,
inference(copy,[status(thm)],[c_35]) ).
fof(prove_singleton_in_unordered_pair3_2,axiom,
member(x,universal_class),
file('theBenchmark.p',prove_singleton_in_unordered_pair3_2) ).
cnf(c_37,plain,
member(x,universal_class),
inference(clausify,[status(thm)],[prove_singleton_in_unordered_pair3_2]) ).
fof(prove_singleton_in_unordered_pair3_1,axiom,
unordered_pair(y,z) = singleton(x),
file('theBenchmark.p',prove_singleton_in_unordered_pair3_1) ).
cnf(c_38,plain,
unordered_pair(y,z) = singleton(x),
inference(clausify,[status(thm)],[prove_singleton_in_unordered_pair3_1]) ).
fof(singleton_identified_by_element2,axiom,
! [VAR_0,VAR_1] :
( VAR_0 = VAR_1
| ~ member(VAR_1,universal_class)
| singleton(VAR_0) != singleton(VAR_1) ),
file('theBenchmark.p',singleton_identified_by_element2) ).
cnf(c_39,plain,
( A = B
| ~ member(B,universal_class)
| singleton(A) != singleton(B) ),
inference(clausify,[status(thm)],[singleton_identified_by_element2]) ).
fof(singleton_is_null_class,axiom,
! [VAR_0] :
( singleton(VAR_0) = null_class
| member(VAR_0,universal_class) ),
file('theBenchmark.p',singleton_is_null_class) ).
cnf(c_41,plain,
( singleton(A) = null_class
| member(A,universal_class) ),
inference(clausify,[status(thm)],[singleton_is_null_class]) ).
fof(only_member_in_singleton,axiom,
! [VAR_0,VAR_1] :
( VAR_0 = VAR_1
| ~ member(VAR_0,singleton(VAR_1)) ),
file('theBenchmark.p',only_member_in_singleton) ).
cnf(c_42,plain,
( A = B
| ~ member(A,singleton(B)) ),
inference(clausify,[status(thm)],[only_member_in_singleton]) ).
fof(corollary_to_set_in_its_singleton,axiom,
! [VAR_0] :
( singleton(VAR_0) != null_class
| ~ member(VAR_0,universal_class) ),
file('theBenchmark.p',corollary_to_set_in_its_singleton) ).
cnf(c_44,plain,
( singleton(A) != null_class
| ~ member(A,universal_class) ),
inference(clausify,[status(thm)],[corollary_to_set_in_its_singleton]) ).
fof(set_in_its_singleton,axiom,
! [VAR_0] :
( member(VAR_0,singleton(VAR_0))
| ~ member(VAR_0,universal_class) ),
file('theBenchmark.p',set_in_its_singleton) ).
cnf(c_45,plain,
( member(A,singleton(A))
| ~ member(A,universal_class) ),
inference(clausify,[status(thm)],[set_in_its_singleton]) ).
fof(unordered_pair_equals_singleton1,axiom,
! [VAR_0,VAR_1] :
( unordered_pair(VAR_1,VAR_0) = singleton(VAR_1)
| member(VAR_0,universal_class) ),
file('theBenchmark.p',unordered_pair_equals_singleton1) ).
cnf(c_56,plain,
( unordered_pair(B,A) = singleton(B)
| member(A,universal_class) ),
inference(clausify,[status(thm)],[unordered_pair_equals_singleton1]) ).
fof(singleton_in_unordered_pair2,axiom,
! [VAR_0,VAR_1] : subclass(singleton(VAR_0),unordered_pair(VAR_1,VAR_0)),
file('theBenchmark.p',singleton_in_unordered_pair2) ).
cnf(c_57,plain,
subclass(singleton(A),unordered_pair(B,A)),
inference(clausify,[status(thm)],[singleton_in_unordered_pair2]) ).
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_163,plain,
( member(C,B)
| ~ member(C,A)
| ~ subclass(A,B) ),
inference(clausify,[status(thm)],[subclass_members]) ).
cnf(c_192,plain,
( B = A
| singleton(B) != singleton(A)
| singleton(A) = null_class ),
inference(resolve,[status(thm)],[c_41,c_39]) ).
cnf(c_194,plain,
singleton(x) != null_class,
inference(resolve,[status(thm)],[c_44,c_37]) ).
cnf(c_195,plain,
( singleton(A) = null_class
| member(A,singleton(A)) ),
inference(resolve,[status(thm)],[c_45,c_41]) ).
cnf(c_236,plain,
( singleton(B) != null_class
| unordered_pair(A,B) = singleton(A) ),
inference(resolve,[status(thm)],[c_56,c_44]) ).
cnf(c_240,plain,
subclass(singleton(z),singleton(x)),
inference(paramod,[status(thm)],[c_38,c_57]) ).
cnf(c_971,plain,
( member(A,singleton(x))
| ~ member(A,singleton(z)) ),
inference(resolve,[status(thm)],[c_240,c_163]) ).
cnf(c_2453,plain,
( singleton(z) = null_class
| member(z,singleton(x)) ),
inference(resolve,[status(thm)],[c_971,c_195]) ).
cnf(c_3484,plain,
( z = x
| singleton(z) = null_class ),
inference(resolve,[status(thm)],[c_2453,c_42]) ).
cnf(c_3134,plain,
singleton(z) = null_class,
inference(resolve,[status(thm)],[c_34,c_3484]) ).
cnf(c_3485,plain,
unordered_pair(A,z) = singleton(A),
inference(resolve,[status(thm)],[c_3134,c_236]) ).
cnf(c_3135,plain,
singleton(A) = unordered_pair(A,z),
inference(copy,[status(thm)],[c_3485]) ).
cnf(c_3355,plain,
singleton(y) = singleton(x),
inference(paramod,[status(thm)],[c_38,c_3135]) ).
cnf(c_3486,plain,
( y = x
| singleton(x) = null_class ),
inference(resolve,[status(thm)],[c_3355,c_192]) ).
cnf(c_3487,plain,
y = x,
inference(resolve,[status(thm)],[c_194,c_3486]) ).
cnf(c_3483,plain,
$false,
inference(resolve,[status(thm)],[c_36,c_3487]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET085-7 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 07:02:23 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 3073091 was started by sandbox on n007,
% 0.09/0.36 % Sat Sep 26 07:02:23 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.37
% 0.09/0.37 % From the command line: assign(max_seconds, 300).
% 3.23/0.88
% 3.23/0.88 % given #500 (T,wt=14): 3134 singleton(z) = null_class. [resolve(2453,a,42,a),unit_del(b,34)].
% 3.23/0.88
% 3.23/0.88 % SZS status Unsatisfiable for theBenchmark
% 3.23/0.88
% 3.23/0.88 % Proof 1 at 0.38 (+ 0.12) seconds.
% 3.23/0.88 % Length of proof is 25.
% 3.23/0.88 % Level of proof is 7.
% 3.23/0.88 % Maximum clause weight is 22.000.
% 3.23/0.88 % Given clauses 523.
% 3.23/0.88
% 3.23/0.88 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------