%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU186+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:45:21 AM UTC 2026
% Result : Theorem 13.79s 2.40s
% Output : CNFRefutation 13.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 7
% Syntax : Number of formulae : 53 ( 22 unt; 0 def)
% Number of atoms : 214 ( 50 equ)
% Maximal formula atoms : 38 ( 4 avg)
% Number of connectives : 268 ( 107 ~; 130 |; 21 &)
% ( 3 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 2 con; 0-5 aty)
% Number of variables : 129 ( 8 sgn 62 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k2_tarski,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
file('theBenchmark.p',commutativity_k2_tarski) ).
fof(d1_xboole_0,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('theBenchmark.p',d1_xboole_0) ).
fof(d5_tarski,axiom,
! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
file('theBenchmark.p',d5_tarski) ).
fof(d8_relat_1,axiom,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ! [C] :
( relation(C)
=> ( C = relation_composition(A,B)
<=> ! [D,E] :
( in(ordered_pair(D,E),C)
<=> ? [F] :
( in(ordered_pair(F,E),B)
& in(ordered_pair(D,F),A) ) ) ) ) ) ),
file('theBenchmark.p',d8_relat_1) ).
fof(fc4_relat_1,axiom,
( relation(empty_set)
& empty(empty_set) ),
file('theBenchmark.p',fc4_relat_1) ).
fof(t69_enumset1,axiom,
! [A] : unordered_pair(A,A) = singleton(A),
file('theBenchmark.p',t69_enumset1) ).
fof(t56_relat_1,conjecture,
! [A] :
( relation(A)
=> ( ! [B,C] : ~ in(ordered_pair(B,C),A)
=> A = empty_set ) ),
file('theBenchmark.p',t56_relat_1) ).
fof(t56_relat_1_neg,negated_conjecture,
~ ! [A] :
( relation(A)
=> ( ! [B,C] : ~ in(ordered_pair(B,C),A)
=> A = empty_set ) ),
inference(assume_negation,[status(cth)],[t56_relat_1]) ).
cnf(c_192,plain,
unordered_pair(A,B) = unordered_pair(B,A),
inference(clausify,[status(thm)],[commutativity_k2_tarski]) ).
cnf(c_214,plain,
( ~ in(B,A)
| empty_set != A ),
inference(clausify,[status(thm)],[d1_xboole_0]) ).
cnf(c_276,plain,
ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
inference(clausify,[status(thm)],[d5_tarski]) ).
cnf(c_277,plain,
ordered_pair(A,B) = unordered_pair(singleton(A),unordered_pair(A,B)),
inference(paramod,[status(thm)],[c_192,c_276]) ).
fof(nnf_26,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ? [D,E] :
( ( ! [F] :
( ~ in(ordered_pair(F,E),B)
| ~ in(ordered_pair(D,F),A) )
| ~ in(ordered_pair(D,E),C) )
& ( ? [X0] :
( in(ordered_pair(X0,E),B)
& in(ordered_pair(D,X0),A) )
| in(ordered_pair(D,E),C) ) )
| relation_composition(A,B) = C )
& ( ! [X1,X2] :
( ( ! [X4] :
( ~ in(ordered_pair(X4,X2),B)
| ~ in(ordered_pair(X1,X4),A) )
| in(ordered_pair(X1,X2),C) )
& ( ? [X3] :
( in(ordered_pair(X3,X2),B)
& in(ordered_pair(X1,X3),A) )
| ~ in(ordered_pair(X1,X2),C) ) )
| relation_composition(A,B) != C ) )
| ~ relation(C) )
| ~ relation(B) )
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[d8_relat_1]) ).
fof(sk_d8_relat_1_sk,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ( ( ! [F] :
( ~ in(ordered_pair(F,sK1(A,B,C)),B)
| ~ in(ordered_pair(sK0(A,B,C),F),A) )
| ~ in(ordered_pair(sK0(A,B,C),sK1(A,B,C)),C) )
& ( ( in(ordered_pair(sK2(A,B,C),sK1(A,B,C)),B)
& in(ordered_pair(sK0(A,B,C),sK2(A,B,C)),A) )
| in(ordered_pair(sK0(A,B,C),sK1(A,B,C)),C) ) )
| relation_composition(A,B) = C )
& ( ! [X1,X2] :
( ( ! [X4] :
( ~ in(ordered_pair(X4,X2),B)
| ~ in(ordered_pair(X1,X4),A) )
| in(ordered_pair(X1,X2),C) )
& ( ( in(ordered_pair(sK5(A,B,C,X1,X2),X2),B)
& in(ordered_pair(X1,sK5(A,B,C,X1,X2)),A) )
| ~ in(ordered_pair(X1,X2),C) ) )
| relation_composition(A,B) != C ) )
| ~ relation(C) )
| ~ relation(B) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK0,sK1,sK2]),skolemize(X3,sK5(A,B,C,X1,X2)),skolemize(D,sK0(A,B,C)),skolemize(E,sK1(A,B,C)),skolemize(X0,sK2(A,B,C))],[nnf_26]) ).
fof(sk_d8_relat_1,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(ordered_pair(VAR_3,sK1(VAR_0,VAR_1,VAR_2)),VAR_1)
| ~ in(ordered_pair(sK0(VAR_0,VAR_1,VAR_2),VAR_3),VAR_0)
| ~ in(ordered_pair(sK0(VAR_0,VAR_1,VAR_2),sK1(VAR_0,VAR_1,VAR_2)),VAR_2)
| relation_composition(VAR_0,VAR_1) = VAR_2
| ~ relation(VAR_2)
| ~ relation(VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(ordered_pair(sK2(VAR_0,VAR_1,VAR_2),sK1(VAR_0,VAR_1,VAR_2)),VAR_1)
| in(ordered_pair(sK0(VAR_0,VAR_1,VAR_2),sK1(VAR_0,VAR_1,VAR_2)),VAR_2)
| relation_composition(VAR_0,VAR_1) = VAR_2
| ~ relation(VAR_2)
| ~ relation(VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(ordered_pair(sK0(VAR_0,VAR_1,VAR_2),sK2(VAR_0,VAR_1,VAR_2)),VAR_0)
| in(ordered_pair(sK0(VAR_0,VAR_1,VAR_2),sK1(VAR_0,VAR_1,VAR_2)),VAR_2)
| relation_composition(VAR_0,VAR_1) = VAR_2
| ~ relation(VAR_2)
| ~ relation(VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ in(ordered_pair(VAR_5,VAR_4),VAR_1)
| ~ in(ordered_pair(VAR_3,VAR_5),VAR_0)
| in(ordered_pair(VAR_3,VAR_4),VAR_2)
| relation_composition(VAR_0,VAR_1) != VAR_2
| ~ relation(VAR_2)
| ~ relation(VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( in(ordered_pair(sK5(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4),VAR_4),VAR_1)
| ~ in(ordered_pair(VAR_3,VAR_4),VAR_2)
| relation_composition(VAR_0,VAR_1) != VAR_2
| ~ relation(VAR_2)
| ~ relation(VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( in(ordered_pair(VAR_3,sK5(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4)),VAR_0)
| ~ in(ordered_pair(VAR_3,VAR_4),VAR_2)
| relation_composition(VAR_0,VAR_1) != VAR_2
| ~ relation(VAR_2)
| ~ relation(VAR_1)
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d8_relat_1_sk]) ).
cnf(c_286,plain,
( in(ordered_pair(sK0(A,B,C),sK2(A,B,C)),A)
| in(ordered_pair(sK0(A,B,C),sK1(A,B,C)),C)
| relation_composition(A,B) = C
| ~ relation(C)
| ~ relation(B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d8_relat_1]) ).
cnf(c_9699,plain,
( in(ordered_pair(sK0(A,B,C),sK2(A,B,C)),A)
| in(unordered_pair(singleton(sK0(A,B,C)),unordered_pair(sK0(A,B,C),sK1(A,B,C))),C)
| relation_composition(A,B) = C
| ~ relation(C)
| ~ relation(B)
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_277,c_286]) ).
cnf(c_287,plain,
( in(unordered_pair(singleton(sK0(A,B,C)),unordered_pair(sK0(A,B,C),sK2(A,B,C))),A)
| in(unordered_pair(singleton(sK0(A,B,C)),unordered_pair(sK0(A,B,C),sK1(A,B,C))),C)
| relation_composition(A,B) = C
| ~ relation(C)
| ~ relation(B)
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_277,c_9699]) ).
cnf(c_288,plain,
( in(ordered_pair(sK2(A,B,C),sK1(A,B,C)),B)
| in(ordered_pair(sK0(A,B,C),sK1(A,B,C)),C)
| relation_composition(A,B) = C
| ~ relation(C)
| ~ relation(B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d8_relat_1]) ).
cnf(c_9700,plain,
( in(ordered_pair(sK2(A,B,C),sK1(A,B,C)),B)
| in(unordered_pair(singleton(sK0(A,B,C)),unordered_pair(sK0(A,B,C),sK1(A,B,C))),C)
| relation_composition(A,B) = C
| ~ relation(C)
| ~ relation(B)
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_277,c_288]) ).
cnf(c_9701,plain,
( in(unordered_pair(singleton(sK2(A,B,C)),unordered_pair(sK2(A,B,C),sK1(A,B,C))),B)
| in(unordered_pair(singleton(sK0(A,B,C)),unordered_pair(sK0(A,B,C),sK1(A,B,C))),C)
| relation_composition(A,B) = C
| ~ relation(C)
| ~ relation(B)
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_277,c_9700]) ).
cnf(c_289,plain,
( in(unordered_pair(singleton(sK2(A,B,C)),unordered_pair(sK1(A,B,C),sK2(A,B,C))),B)
| in(unordered_pair(singleton(sK0(A,B,C)),unordered_pair(sK0(A,B,C),sK1(A,B,C))),C)
| relation_composition(A,B) = C
| ~ relation(C)
| ~ relation(B)
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_192,c_9701]) ).
cnf(c_315,plain,
relation(empty_set),
inference(clausify,[status(thm)],[fc4_relat_1]) ).
cnf(c_429,plain,
singleton(A) = unordered_pair(A,A),
inference(clausify,[status(thm)],[t69_enumset1]) ).
fof(nnf_162,plain,
? [A] :
( empty_set != A
& ! [B,C] : ~ in(ordered_pair(B,C),A)
& relation(A) ),
inference(fof_nnf,[status(thm)],[t56_relat_1_neg]) ).
fof(sk_t56_relat_1_neg,plain,
( empty_set != sK3
& ! [B,C] : ~ in(ordered_pair(B,C),sK3)
& relation(sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(A,sK3)],[nnf_162]) ).
cnf(c_444,negated_conjecture,
relation(sK3),
inference(split_conjunct,[status(thm)],[sk_t56_relat_1_neg]) ).
cnf(c_445,negated_conjecture,
~ in(ordered_pair(A,B),sK3),
inference(split_conjunct,[status(thm)],[sk_t56_relat_1_neg]) ).
cnf(c_9702,negated_conjecture,
~ in(unordered_pair(singleton(A),unordered_pair(A,B)),sK3),
inference(paramod,[status(thm)],[c_277,c_445]) ).
cnf(c_446,negated_conjecture,
~ in(unordered_pair(unordered_pair(A,A),unordered_pair(A,B)),sK3),
inference(paramod,[status(thm)],[c_429,c_9702]) ).
cnf(c_447,negated_conjecture,
empty_set != sK3,
inference(split_conjunct,[status(thm)],[sk_t56_relat_1_neg]) ).
cnf(c_448,negated_conjecture,
sK3 != empty_set,
inference(copy,[status(thm)],[c_447]) ).
cnf(c_9703,plain,
( in(unordered_pair(singleton(sK0(A,B,A)),unordered_pair(sK0(A,B,A),sK2(A,B,A))),A)
| in(unordered_pair(singleton(sK0(A,B,A)),unordered_pair(sK0(A,B,A),sK1(A,B,A))),A)
| relation_composition(A,B) = A
| ~ relation(B)
| ~ relation(A) ),
inference(factor,[status(thm)],[c_287]) ).
cnf(c_9704,plain,
( in(unordered_pair(singleton(sK0(A,B,A)),unordered_pair(sK0(A,B,A),sK2(A,B,A))),A)
| in(unordered_pair(unordered_pair(sK0(A,B,A),sK0(A,B,A)),unordered_pair(sK0(A,B,A),sK1(A,B,A))),A)
| relation_composition(A,B) = A
| ~ relation(B)
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_429,c_9703]) ).
cnf(c_511,plain,
( in(unordered_pair(unordered_pair(sK0(A,B,A),sK0(A,B,A)),unordered_pair(sK0(A,B,A),sK2(A,B,A))),A)
| in(unordered_pair(unordered_pair(sK0(A,B,A),sK0(A,B,A)),unordered_pair(sK0(A,B,A),sK1(A,B,A))),A)
| relation_composition(A,B) = A
| ~ relation(B)
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_429,c_9704]) ).
cnf(c_9705,plain,
( in(unordered_pair(singleton(sK2(A,B,B)),unordered_pair(sK1(A,B,B),sK2(A,B,B))),B)
| in(unordered_pair(singleton(sK0(A,B,B)),unordered_pair(sK0(A,B,B),sK1(A,B,B))),B)
| relation_composition(A,B) = B
| ~ relation(B)
| ~ relation(A) ),
inference(factor,[status(thm)],[c_289]) ).
cnf(c_9706,plain,
( in(unordered_pair(singleton(sK2(A,B,B)),unordered_pair(sK1(A,B,B),sK2(A,B,B))),B)
| in(unordered_pair(unordered_pair(sK0(A,B,B),sK0(A,B,B)),unordered_pair(sK0(A,B,B),sK1(A,B,B))),B)
| relation_composition(A,B) = B
| ~ relation(B)
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_429,c_9705]) ).
cnf(c_9707,plain,
( in(unordered_pair(unordered_pair(sK2(A,B,B),sK2(A,B,B)),unordered_pair(sK1(A,B,B),sK2(A,B,B))),B)
| in(unordered_pair(unordered_pair(sK0(A,B,B),sK0(A,B,B)),unordered_pair(sK0(A,B,B),sK1(A,B,B))),B)
| relation_composition(A,B) = B
| ~ relation(B)
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_429,c_9706]) ).
cnf(c_515,plain,
( in(unordered_pair(unordered_pair(sK1(A,B,B),sK2(A,B,B)),unordered_pair(sK2(A,B,B),sK2(A,B,B))),B)
| in(unordered_pair(unordered_pair(sK0(A,B,B),sK0(A,B,B)),unordered_pair(sK0(A,B,B),sK1(A,B,B))),B)
| relation_composition(A,B) = B
| ~ relation(B)
| ~ relation(A) ),
inference(paramod,[status(thm)],[c_192,c_9707]) ).
cnf(c_595,plain,
~ in(A,empty_set),
inference(xxres,[status(thm)],[c_214]) ).
cnf(c_748,plain,
~ in(unordered_pair(unordered_pair(A,A),unordered_pair(B,A)),sK3),
inference(paramod,[status(thm)],[c_192,c_446]) ).
cnf(c_750,plain,
~ in(unordered_pair(unordered_pair(A,B),unordered_pair(B,B)),sK3),
inference(paramod,[status(thm)],[c_192,c_748]) ).
cnf(c_9708,plain,
( in(unordered_pair(unordered_pair(sK0(empty_set,A,empty_set),sK0(empty_set,A,empty_set)),unordered_pair(sK0(empty_set,A,empty_set),sK2(empty_set,A,empty_set))),empty_set)
| in(unordered_pair(unordered_pair(sK0(empty_set,A,empty_set),sK0(empty_set,A,empty_set)),unordered_pair(sK0(empty_set,A,empty_set),sK1(empty_set,A,empty_set))),empty_set)
| relation_composition(empty_set,A) = empty_set
| ~ relation(A) ),
inference(resolve,[status(thm)],[c_511,c_315]) ).
cnf(c_9709,plain,
( in(unordered_pair(unordered_pair(sK0(empty_set,A,empty_set),sK0(empty_set,A,empty_set)),unordered_pair(sK0(empty_set,A,empty_set),sK2(empty_set,A,empty_set))),empty_set)
| relation_composition(empty_set,A) = empty_set
| ~ relation(A) ),
inference(resolve,[status(thm)],[c_595,c_9708]) ).
cnf(c_9577,plain,
( relation_composition(empty_set,A) = empty_set
| ~ relation(A) ),
inference(resolve,[status(thm)],[c_595,c_9709]) ).
cnf(c_9605,plain,
relation_composition(empty_set,sK3) = empty_set,
inference(resolve,[status(thm)],[c_9577,c_444]) ).
cnf(c_9710,negated_conjecture,
( in(unordered_pair(unordered_pair(sK1(A,sK3,sK3),sK2(A,sK3,sK3)),unordered_pair(sK2(A,sK3,sK3),sK2(A,sK3,sK3))),sK3)
| in(unordered_pair(unordered_pair(sK0(A,sK3,sK3),sK0(A,sK3,sK3)),unordered_pair(sK0(A,sK3,sK3),sK1(A,sK3,sK3))),sK3)
| relation_composition(A,sK3) = sK3
| ~ relation(A) ),
inference(resolve,[status(thm)],[c_515,c_444]) ).
cnf(c_9711,negated_conjecture,
( in(unordered_pair(unordered_pair(sK1(A,sK3,sK3),sK2(A,sK3,sK3)),unordered_pair(sK2(A,sK3,sK3),sK2(A,sK3,sK3))),sK3)
| relation_composition(A,sK3) = sK3
| ~ relation(A) ),
inference(resolve,[status(thm)],[c_446,c_9710]) ).
cnf(c_9688,negated_conjecture,
( relation_composition(A,sK3) = sK3
| ~ relation(A) ),
inference(resolve,[status(thm)],[c_750,c_9711]) ).
cnf(c_9712,plain,
relation_composition(empty_set,sK3) = sK3,
inference(resolve,[status(thm)],[c_9688,c_315]) ).
cnf(c_9713,plain,
empty_set = sK3,
inference(paramod,[status(thm)],[c_9605,c_9712]) ).
cnf(c_9714,plain,
sK3 = empty_set,
inference(copy,[status(thm)],[c_9713]) ).
cnf(c_9698,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_448,c_9714]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU186+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n020.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 08:47:48 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.37 % Process 1131751 was started by sandbox on n020,
% 0.08/0.37 % Sat Sep 26 08:47:48 2026
% 0.08/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.39
% 0.08/0.39 % From the command line: assign(max_seconds, 300).
% 0.08/0.39
% 0.08/0.39 % SInE: 136 to sos, 27 to usable, of 163 axioms (tolerance 2.00, depth 0 fixpoint).
% 13.79/2.40
% 13.79/2.40 % given #500 (F,wt=15): 4985 -disjoint(f44(A),powerset(B)). [resolve(4449,a,898,a)].
% 13.79/2.40
% 13.79/2.40 % SZS status Theorem for theBenchmark
% 13.79/2.40
% 13.79/2.40 % Proof 1 at 1.56 (+ 0.37) seconds.
% 13.79/2.40 % Length of proof is 31.
% 13.79/2.40 % Level of proof is 7.
% 13.79/2.40 % Maximum clause weight is 275.000.
% 13.79/2.40 % Given clauses 840.
% 13.79/2.40
% 13.79/2.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------