%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SET016+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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:19 AM UTC 2026
% Result : Theorem 197.71s 31.51s
% Output : CNFRefutation 197.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 7
% Syntax : Number of formulae : 45 ( 27 unt; 0 def)
% Number of atoms : 74 ( 35 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 53 ( 24 ~; 15 |; 8 &)
% ( 3 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 61 ( 15 sgn 21 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(subclass_defn,axiom,
! [X,Y] :
( subclass(X,Y)
<=> ! [U] :
( member(U,X)
=> member(U,Y) ) ),
file('theBenchmark.p',subclass_defn) ).
fof(extensionality,axiom,
! [X,Y] :
( X = Y
<=> ( subclass(Y,X)
& subclass(X,Y) ) ),
file('theBenchmark.p',extensionality) ).
fof(unordered_pair_defn,axiom,
! [U,X,Y] :
( member(U,unordered_pair(X,Y))
<=> ( ( U = Y
| U = X )
& member(U,universal_class) ) ),
file('theBenchmark.p',unordered_pair_defn) ).
fof(unordered_pair,axiom,
! [X,Y] : member(unordered_pair(X,Y),universal_class),
file('theBenchmark.p',unordered_pair) ).
fof(singleton_set_defn,axiom,
! [X] : singleton(X) = unordered_pair(X,X),
file('theBenchmark.p',singleton_set_defn) ).
fof(ordered_pair_defn,axiom,
! [X,Y] : ordered_pair(X,Y) = unordered_pair(singleton(X),unordered_pair(X,singleton(Y))),
file('theBenchmark.p',ordered_pair_defn) ).
fof(ordered_pair_determines_components1,conjecture,
! [W,X,Y,Z] :
( ( member(W,universal_class)
& ordered_pair(W,X) = ordered_pair(Y,Z) )
=> W = Y ),
file('theBenchmark.p',ordered_pair_determines_components1) ).
fof(ordered_pair_determines_components1_neg,negated_conjecture,
~ ! [W,X,Y,Z] :
( ( member(W,universal_class)
& ordered_pair(W,X) = ordered_pair(Y,Z) )
=> W = Y ),
inference(assume_negation,[status(cth)],[ordered_pair_determines_components1]) ).
fof(nnf_42,plain,
? [W,X,Y,Z] :
( W != Y
& member(W,universal_class)
& ordered_pair(W,X) = ordered_pair(Y,Z) ),
inference(fof_nnf,[status(thm)],[ordered_pair_determines_components1_neg]) ).
fof(sk_ordered_pair_determines_components1_neg,plain,
( sK0 != sK1
& member(sK0,universal_class)
& ordered_pair(sK0,sK2) = ordered_pair(sK1,sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK2,sK1,sK3]),skolemize(W,sK0),skolemize(X,sK2),skolemize(Y,sK1),skolemize(Z,sK3)],[nnf_42]) ).
cnf(c_64,negated_conjecture,
sK0 != sK1,
inference(split_conjunct,[status(thm)],[sk_ordered_pair_determines_components1_neg]) ).
cnf(c_65,negated_conjecture,
sK1 != sK0,
inference(copy,[status(thm)],[c_64]) ).
cnf(c_66,negated_conjecture,
member(sK0,universal_class),
inference(split_conjunct,[status(thm)],[sk_ordered_pair_determines_components1_neg]) ).
cnf(c_67,negated_conjecture,
ordered_pair(sK0,sK2) = ordered_pair(sK1,sK3),
inference(split_conjunct,[status(thm)],[sk_ordered_pair_determines_components1_neg]) ).
cnf(c_68,negated_conjecture,
ordered_pair(sK1,sK3) = ordered_pair(sK0,sK2),
inference(copy,[status(thm)],[c_67]) ).
cnf(c_130,plain,
ordered_pair(A,B) = unordered_pair(singleton(A),unordered_pair(A,singleton(B))),
inference(clausify,[status(thm)],[ordered_pair_defn]) ).
cnf(c_131,plain,
singleton(A) = unordered_pair(A,A),
inference(clausify,[status(thm)],[singleton_set_defn]) ).
cnf(c_132,plain,
member(unordered_pair(A,B),universal_class),
inference(clausify,[status(thm)],[unordered_pair]) ).
cnf(c_134,plain,
( A != B
| ~ member(A,universal_class)
| member(A,unordered_pair(B,C)) ),
inference(clausify,[status(thm)],[unordered_pair_defn]) ).
cnf(c_135,plain,
( A = C
| A = B
| ~ member(A,unordered_pair(B,C)) ),
inference(clausify,[status(thm)],[unordered_pair_defn]) ).
cnf(c_139,plain,
( subclass(B,A)
| A != B ),
inference(clausify,[status(thm)],[extensionality]) ).
cnf(c_143,plain,
( member(C,B)
| ~ member(C,A)
| ~ subclass(A,B) ),
inference(clausify,[status(thm)],[subclass_defn]) ).
cnf(c_21405,negated_conjecture,
unordered_pair(singleton(sK1),unordered_pair(sK1,singleton(sK3))) = ordered_pair(sK0,sK2),
inference(paramod,[status(thm)],[c_130,c_68]) ).
cnf(c_21406,negated_conjecture,
unordered_pair(unordered_pair(sK1,sK1),unordered_pair(sK1,singleton(sK3))) = ordered_pair(sK0,sK2),
inference(paramod,[status(thm)],[c_131,c_21405]) ).
cnf(c_21407,negated_conjecture,
unordered_pair(unordered_pair(sK1,sK1),unordered_pair(sK1,unordered_pair(sK3,sK3))) = ordered_pair(sK0,sK2),
inference(paramod,[status(thm)],[c_131,c_21406]) ).
cnf(c_21408,negated_conjecture,
unordered_pair(unordered_pair(sK1,sK1),unordered_pair(sK1,unordered_pair(sK3,sK3))) = unordered_pair(singleton(sK0),unordered_pair(sK0,singleton(sK2))),
inference(paramod,[status(thm)],[c_130,c_21407]) ).
cnf(c_21409,negated_conjecture,
unordered_pair(unordered_pair(sK1,sK1),unordered_pair(sK1,unordered_pair(sK3,sK3))) = unordered_pair(unordered_pair(sK0,sK0),unordered_pair(sK0,singleton(sK2))),
inference(paramod,[status(thm)],[c_131,c_21408]) ).
cnf(c_194,negated_conjecture,
unordered_pair(unordered_pair(sK1,sK1),unordered_pair(sK1,unordered_pair(sK3,sK3))) = unordered_pair(unordered_pair(sK0,sK0),unordered_pair(sK0,unordered_pair(sK2,sK2))),
inference(paramod,[status(thm)],[c_131,c_21409]) ).
cnf(c_323,plain,
( sK0 != A
| member(sK0,unordered_pair(A,B)) ),
inference(resolve,[status(thm)],[c_134,c_66]) ).
cnf(c_21410,plain,
( ~ member(singleton(A),universal_class)
| member(singleton(A),unordered_pair(unordered_pair(A,A),B)) ),
inference(resolve,[status(thm)],[c_134,c_131]) ).
cnf(c_21411,plain,
( ~ member(singleton(A),universal_class)
| member(unordered_pair(A,A),unordered_pair(unordered_pair(A,A),B)) ),
inference(paramod,[status(thm)],[c_131,c_21410]) ).
cnf(c_21412,plain,
( ~ member(unordered_pair(A,A),universal_class)
| member(unordered_pair(A,A),unordered_pair(unordered_pair(A,A),B)) ),
inference(paramod,[status(thm)],[c_131,c_21411]) ).
cnf(c_324,plain,
member(unordered_pair(A,A),unordered_pair(unordered_pair(A,A),B)),
inference(resolve,[status(thm)],[c_132,c_21412]) ).
cnf(c_21413,negated_conjecture,
sK0 != sK1,
inference(copy,[status(thm)],[c_65]) ).
cnf(c_21414,negated_conjecture,
( sK0 = A
| ~ member(sK0,unordered_pair(sK1,A)) ),
inference(resolve,[status(thm)],[c_135,c_21413]) ).
cnf(c_21415,negated_conjecture,
sK0 != sK1,
inference(copy,[status(thm)],[c_65]) ).
cnf(c_334,negated_conjecture,
~ member(sK0,unordered_pair(sK1,sK1)),
inference(resolve,[status(thm)],[c_21414,c_21415]) ).
cnf(c_7338,plain,
member(sK0,unordered_pair(sK0,A)),
inference(xxres,[status(thm)],[c_323]) ).
cnf(c_21416,plain,
( member(sK0,B)
| ~ subclass(unordered_pair(sK0,A),B) ),
inference(resolve,[status(thm)],[c_143,c_7338]) ).
cnf(c_7491,plain,
~ subclass(unordered_pair(sK0,A),unordered_pair(sK1,sK1)),
inference(resolve,[status(thm)],[c_21416,c_334]) ).
cnf(c_11947,plain,
member(unordered_pair(sK1,sK1),unordered_pair(unordered_pair(sK0,sK0),unordered_pair(sK0,unordered_pair(sK2,sK2)))),
inference(paramod,[status(thm)],[c_194,c_324]) ).
cnf(c_15963,plain,
unordered_pair(sK1,sK1) != unordered_pair(sK0,A),
inference(resolve,[status(thm)],[c_139,c_7491]) ).
cnf(c_21417,plain,
( unordered_pair(sK1,sK1) = B
| ~ member(unordered_pair(sK1,sK1),unordered_pair(unordered_pair(sK0,A),B)) ),
inference(resolve,[status(thm)],[c_135,c_15963]) ).
cnf(c_21403,plain,
~ member(unordered_pair(sK1,sK1),unordered_pair(unordered_pair(sK0,A),unordered_pair(sK0,B))),
inference(resolve,[status(thm)],[c_21417,c_15963]) ).
cnf(c_21404,plain,
$false,
inference(resolve,[status(thm)],[c_21403,c_11947]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SET016+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/5.45 % Computer : n017.cluster.edu
% 0.19/5.45 % Model : x86_64 x86_64
% 0.19/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/5.45 % Memory : 8046.5625MB
% 0.19/5.45 % OS : Linux 6.8.0-71-generic
% 0.19/5.45 % CPULimit : 300
% 0.19/5.45 % WCLimit : 300
% 0.19/5.45 % DateTime : Sat Sep 26 06:46:24 UTC 2026
% 0.19/5.45 % CPUTime :
% 0.19/5.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/5.46 % Process 68215 was started by sandbox on n017,
% 0.19/5.46 % Sat Sep 26 06:46:24 2026
% 0.19/5.46 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.19/5.48
% 0.19/5.48 % From the command line: assign(max_seconds, 300).
% 197.71/31.51
% 197.71/31.51 % given #500 (A,wt=35): 262 member(flip(A),power_class(cross_product(cross_product(universal_class,universal_class),universal_class))) | -member(flip(A),universal_class). [resolve(101,a,81,c)].
% 197.71/31.51
% 197.71/31.51 % given #1000 (A,wt=27): 360 subclass(intersection(A,B),C) | member(f1(intersection(A,B),C),B). [resolve(142,b,118,a)].
% 197.71/31.51
% 197.71/31.51 % SZS status Theorem for theBenchmark
% 197.71/31.51
% 197.71/31.51 % Proof 1 at 1.41 (+ 0.44) seconds.
% 197.71/31.51 % Length of proof is 29.
% 197.71/31.51 % Level of proof is 7.
% 197.71/31.51 % Maximum clause weight is 51.000.
% 197.71/31.51 % Given clauses 1143.
% 197.71/31.51
% 197.71/31.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------