%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU269+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:38 AM UTC 2026
% Result : Theorem 19.98s 3.30s
% Output : CNFRefutation 19.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 8
% Syntax : Number of formulae : 80 ( 14 unt; 0 def)
% Number of atoms : 268 ( 19 equ)
% Maximal formula atoms : 26 ( 3 avg)
% Number of connectives : 294 ( 106 ~; 153 |; 25 &)
% ( 4 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 1 con; 0-2 aty)
% Number of variables : 169 ( 2 sgn 47 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k2_tarski,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
file('theBenchmark.p',commutativity_k2_tarski) ).
fof(d16_relat_2,axiom,
! [A] :
( relation(A)
=> ( transitive(A)
<=> is_transitive_in(A,relation_field(A)) ) ),
file('theBenchmark.p',d16_relat_2) ).
fof(d1_wellord2,axiom,
! [A,B] :
( relation(B)
=> ( B = inclusion_relation(A)
<=> ( ! [C,D] :
( ( in(D,A)
& in(C,A) )
=> ( in(ordered_pair(C,D),B)
<=> subset(C,D) ) )
& relation_field(B) = A ) ) ),
file('theBenchmark.p',d1_wellord2) ).
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_2,axiom,
! [A] :
( relation(A)
=> ! [B] :
( is_transitive_in(A,B)
<=> ! [C,D,E] :
( ( in(ordered_pair(D,E),A)
& in(ordered_pair(C,D),A)
& in(E,B)
& in(D,B)
& in(C,B) )
=> in(ordered_pair(C,E),A) ) ) ),
file('theBenchmark.p',d8_relat_2) ).
fof(dt_k1_wellord2,axiom,
! [A] : relation(inclusion_relation(A)),
file('theBenchmark.p',dt_k1_wellord2) ).
fof(t1_xboole_1,axiom,
! [A,B,C] :
( ( subset(B,C)
& subset(A,B) )
=> subset(A,C) ),
file('theBenchmark.p',t1_xboole_1) ).
fof(t3_wellord2,conjecture,
! [A] : transitive(inclusion_relation(A)),
file('theBenchmark.p',t3_wellord2) ).
fof(t3_wellord2_neg,negated_conjecture,
~ ! [A] : transitive(inclusion_relation(A)),
inference(assume_negation,[status(cth)],[t3_wellord2]) ).
cnf(c_68,plain,
relation(inclusion_relation(A)),
inference(clausify,[status(thm)],[dt_k1_wellord2]) ).
fof(nnf_13,plain,
! [A] :
( ! [B] :
( ( ? [C,D,E] :
( ~ in(ordered_pair(C,E),A)
& in(ordered_pair(D,E),A)
& in(ordered_pair(C,D),A)
& in(E,B)
& in(D,B)
& in(C,B) )
| is_transitive_in(A,B) )
& ( ! [X0,X1,X2] :
( in(ordered_pair(X0,X2),A)
| ~ in(ordered_pair(X1,X2),A)
| ~ in(ordered_pair(X0,X1),A)
| ~ in(X2,B)
| ~ in(X1,B)
| ~ in(X0,B) )
| ~ is_transitive_in(A,B) ) )
| ~ relation(A) ),
inference(fof_nnf,[status(thm)],[d8_relat_2]) ).
fof(sk_d8_relat_2_sk,plain,
! [A] :
( ! [B] :
( ( ( ~ in(ordered_pair(sK0(A,B),sK1(A,B)),A)
& in(ordered_pair(sK2(A,B),sK1(A,B)),A)
& in(ordered_pair(sK0(A,B),sK2(A,B)),A)
& in(sK1(A,B),B)
& in(sK2(A,B),B)
& in(sK0(A,B),B) )
| is_transitive_in(A,B) )
& ( ! [X0,X1,X2] :
( in(ordered_pair(X0,X2),A)
| ~ in(ordered_pair(X1,X2),A)
| ~ in(ordered_pair(X0,X1),A)
| ~ in(X2,B)
| ~ in(X1,B)
| ~ in(X0,B) )
| ~ is_transitive_in(A,B) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK2,sK1]),skolemize(C,sK0(A,B)),skolemize(D,sK2(A,B)),skolemize(E,sK1(A,B))],[nnf_13]) ).
fof(sk_d8_relat_2,plain,
( ! [VAR_0,VAR_1] :
( ~ in(ordered_pair(sK0(VAR_0,VAR_1),sK1(VAR_0,VAR_1)),VAR_0)
| is_transitive_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(ordered_pair(sK2(VAR_0,VAR_1),sK1(VAR_0,VAR_1)),VAR_0)
| is_transitive_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(ordered_pair(sK0(VAR_0,VAR_1),sK2(VAR_0,VAR_1)),VAR_0)
| is_transitive_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(sK1(VAR_0,VAR_1),VAR_1)
| is_transitive_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(sK2(VAR_0,VAR_1),VAR_1)
| is_transitive_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1] :
( in(sK0(VAR_0,VAR_1),VAR_1)
| is_transitive_in(VAR_0,VAR_1)
| ~ relation(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( in(ordered_pair(VAR_2,VAR_4),VAR_0)
| ~ in(ordered_pair(VAR_3,VAR_4),VAR_0)
| ~ in(ordered_pair(VAR_2,VAR_3),VAR_0)
| ~ in(VAR_4,VAR_1)
| ~ in(VAR_3,VAR_1)
| ~ in(VAR_2,VAR_1)
| ~ is_transitive_in(VAR_0,VAR_1)
| ~ relation(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d8_relat_2_sk]) ).
cnf(c_69,plain,
( ~ in(ordered_pair(sK0(A,B),sK1(A,B)),A)
| is_transitive_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d8_relat_2]) ).
cnf(c_70,plain,
( in(ordered_pair(sK2(A,B),sK1(A,B)),A)
| is_transitive_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d8_relat_2]) ).
cnf(c_71,plain,
( in(ordered_pair(sK0(A,B),sK2(A,B)),A)
| is_transitive_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d8_relat_2]) ).
cnf(c_72,plain,
( in(sK1(A,B),B)
| is_transitive_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d8_relat_2]) ).
cnf(c_73,plain,
( in(sK2(A,B),B)
| is_transitive_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d8_relat_2]) ).
cnf(c_74,plain,
( in(sK0(A,B),B)
| is_transitive_in(A,B)
| ~ relation(A) ),
inference(split_conjunct,[status(thm)],[sk_d8_relat_2]) ).
cnf(c_81,plain,
( ~ subset(C,D)
| in(ordered_pair(C,D),A)
| ~ in(D,B)
| ~ in(C,B)
| inclusion_relation(B) != A
| ~ relation(A) ),
inference(clausify,[status(thm)],[d1_wellord2]) ).
cnf(c_82,plain,
( subset(C,D)
| ~ in(ordered_pair(C,D),A)
| ~ in(D,B)
| ~ in(C,B)
| inclusion_relation(B) != A
| ~ relation(A) ),
inference(clausify,[status(thm)],[d1_wellord2]) ).
cnf(c_83,plain,
( relation_field(A) = B
| inclusion_relation(B) != A
| ~ relation(A) ),
inference(clausify,[status(thm)],[d1_wellord2]) ).
cnf(c_84,plain,
( ~ is_transitive_in(A,relation_field(A))
| transitive(A)
| ~ relation(A) ),
inference(clausify,[status(thm)],[d16_relat_2]) ).
cnf(c_202,plain,
( ~ is_transitive_in(inclusion_relation(A),relation_field(inclusion_relation(A)))
| transitive(inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_68,c_84]) ).
cnf(c_203,plain,
( relation_field(inclusion_relation(B)) = A
| inclusion_relation(A) != inclusion_relation(B) ),
inference(resolve,[status(thm)],[c_68,c_83]) ).
cnf(c_204,plain,
( subset(C,D)
| ~ in(ordered_pair(C,D),inclusion_relation(B))
| ~ in(D,A)
| ~ in(C,A)
| inclusion_relation(A) != inclusion_relation(B) ),
inference(resolve,[status(thm)],[c_68,c_82]) ).
cnf(c_205,plain,
( ~ subset(C,D)
| in(ordered_pair(C,D),inclusion_relation(B))
| ~ in(D,A)
| ~ in(C,A)
| inclusion_relation(A) != inclusion_relation(B) ),
inference(resolve,[status(thm)],[c_68,c_81]) ).
cnf(c_213,plain,
( in(sK0(inclusion_relation(A),B),B)
| is_transitive_in(inclusion_relation(A),B) ),
inference(resolve,[status(thm)],[c_68,c_74]) ).
cnf(c_214,plain,
( in(sK2(inclusion_relation(A),B),B)
| is_transitive_in(inclusion_relation(A),B) ),
inference(resolve,[status(thm)],[c_68,c_73]) ).
cnf(c_215,plain,
( in(sK1(inclusion_relation(A),B),B)
| is_transitive_in(inclusion_relation(A),B) ),
inference(resolve,[status(thm)],[c_68,c_72]) ).
cnf(c_216,plain,
( in(ordered_pair(sK0(inclusion_relation(A),B),sK2(inclusion_relation(A),B)),inclusion_relation(A))
| is_transitive_in(inclusion_relation(A),B) ),
inference(resolve,[status(thm)],[c_68,c_71]) ).
cnf(c_217,plain,
( in(ordered_pair(sK2(inclusion_relation(A),B),sK1(inclusion_relation(A),B)),inclusion_relation(A))
| is_transitive_in(inclusion_relation(A),B) ),
inference(resolve,[status(thm)],[c_68,c_70]) ).
cnf(c_218,plain,
( ~ in(ordered_pair(sK0(inclusion_relation(A),B),sK1(inclusion_relation(A),B)),inclusion_relation(A))
| is_transitive_in(inclusion_relation(A),B) ),
inference(resolve,[status(thm)],[c_68,c_69]) ).
fof(nnf_51,plain,
? [A] : ~ transitive(inclusion_relation(A)),
inference(fof_nnf,[status(thm)],[t3_wellord2_neg]) ).
fof(sk_t3_wellord2_neg,plain,
~ transitive(inclusion_relation(sK3)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(A,sK3)],[nnf_51]) ).
cnf(c_219,negated_conjecture,
~ transitive(inclusion_relation(sK3)),
inference(split_conjunct,[status(thm)],[sk_t3_wellord2_neg]) ).
cnf(c_228,plain,
( subset(A,C)
| ~ subset(B,C)
| ~ subset(A,B) ),
inference(clausify,[status(thm)],[t1_xboole_1]) ).
cnf(c_243,plain,
ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
inference(clausify,[status(thm)],[d5_tarski]) ).
cnf(c_245,plain,
unordered_pair(A,B) = unordered_pair(B,A),
inference(clausify,[status(thm)],[commutativity_k2_tarski]) ).
cnf(c_11837,plain,
( ~ in(unordered_pair(unordered_pair(sK0(inclusion_relation(A),B),sK1(inclusion_relation(A),B)),singleton(sK0(inclusion_relation(A),B))),inclusion_relation(A))
| is_transitive_in(inclusion_relation(A),B) ),
inference(paramod,[status(thm)],[c_243,c_218]) ).
cnf(c_276,plain,
( ~ in(unordered_pair(singleton(sK0(inclusion_relation(A),B)),unordered_pair(sK0(inclusion_relation(A),B),sK1(inclusion_relation(A),B))),inclusion_relation(A))
| is_transitive_in(inclusion_relation(A),B) ),
inference(paramod,[status(thm)],[c_245,c_11837]) ).
cnf(c_11838,plain,
( in(unordered_pair(unordered_pair(sK2(inclusion_relation(A),B),sK1(inclusion_relation(A),B)),singleton(sK2(inclusion_relation(A),B))),inclusion_relation(A))
| is_transitive_in(inclusion_relation(A),B) ),
inference(paramod,[status(thm)],[c_243,c_217]) ).
cnf(c_277,plain,
( in(unordered_pair(singleton(sK2(inclusion_relation(A),B)),unordered_pair(sK2(inclusion_relation(A),B),sK1(inclusion_relation(A),B))),inclusion_relation(A))
| is_transitive_in(inclusion_relation(A),B) ),
inference(paramod,[status(thm)],[c_245,c_11838]) ).
cnf(c_11839,plain,
( in(unordered_pair(unordered_pair(sK0(inclusion_relation(A),B),sK2(inclusion_relation(A),B)),singleton(sK0(inclusion_relation(A),B))),inclusion_relation(A))
| is_transitive_in(inclusion_relation(A),B) ),
inference(paramod,[status(thm)],[c_243,c_216]) ).
cnf(c_278,plain,
( in(unordered_pair(singleton(sK0(inclusion_relation(A),B)),unordered_pair(sK0(inclusion_relation(A),B),sK2(inclusion_relation(A),B))),inclusion_relation(A))
| is_transitive_in(inclusion_relation(A),B) ),
inference(paramod,[status(thm)],[c_245,c_11839]) ).
cnf(c_11840,plain,
( ~ subset(C,D)
| in(unordered_pair(unordered_pair(C,D),singleton(C)),inclusion_relation(B))
| ~ in(D,A)
| ~ in(C,A)
| inclusion_relation(A) != inclusion_relation(B) ),
inference(paramod,[status(thm)],[c_243,c_205]) ).
cnf(c_282,plain,
( ~ subset(C,D)
| in(unordered_pair(singleton(C),unordered_pair(C,D)),inclusion_relation(B))
| ~ in(D,A)
| ~ in(C,A)
| inclusion_relation(A) != inclusion_relation(B) ),
inference(paramod,[status(thm)],[c_245,c_11840]) ).
cnf(c_11841,plain,
( subset(C,D)
| ~ in(unordered_pair(unordered_pair(C,D),singleton(C)),inclusion_relation(B))
| ~ in(D,A)
| ~ in(C,A)
| inclusion_relation(A) != inclusion_relation(B) ),
inference(paramod,[status(thm)],[c_243,c_204]) ).
cnf(c_283,plain,
( subset(C,D)
| ~ in(unordered_pair(singleton(C),unordered_pair(C,D)),inclusion_relation(B))
| ~ in(D,A)
| ~ in(C,A)
| inclusion_relation(A) != inclusion_relation(B) ),
inference(paramod,[status(thm)],[c_245,c_11841]) ).
cnf(c_364,plain,
relation_field(inclusion_relation(A)) = A,
inference(xxres,[status(thm)],[c_203]) ).
cnf(c_371,plain,
( ~ is_transitive_in(inclusion_relation(A),A)
| transitive(inclusion_relation(A)) ),
inference(paramod,[status(thm)],[c_364,c_202]) ).
cnf(c_448,plain,
( ~ subset(A,C)
| in(unordered_pair(singleton(A),unordered_pair(A,C)),inclusion_relation(B))
| ~ in(C,B)
| ~ in(A,B) ),
inference(xxres,[status(thm)],[c_282]) ).
cnf(c_449,plain,
( subset(A,C)
| ~ in(unordered_pair(singleton(A),unordered_pair(A,C)),inclusion_relation(B))
| ~ in(C,B)
| ~ in(A,B) ),
inference(xxres,[status(thm)],[c_283]) ).
cnf(c_630,plain,
( in(unordered_pair(singleton(sK0(inclusion_relation(A),A)),unordered_pair(sK0(inclusion_relation(A),A),sK2(inclusion_relation(A),A))),inclusion_relation(A))
| transitive(inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_371,c_278]) ).
cnf(c_631,plain,
( in(unordered_pair(singleton(sK2(inclusion_relation(A),A)),unordered_pair(sK2(inclusion_relation(A),A),sK1(inclusion_relation(A),A))),inclusion_relation(A))
| transitive(inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_371,c_277]) ).
cnf(c_632,plain,
( in(sK1(inclusion_relation(A),A),A)
| transitive(inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_371,c_215]) ).
cnf(c_633,plain,
( in(sK2(inclusion_relation(A),A),A)
| transitive(inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_371,c_214]) ).
cnf(c_634,plain,
( in(sK0(inclusion_relation(A),A),A)
| transitive(inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_371,c_213]) ).
cnf(c_1992,plain,
( transitive(inclusion_relation(B))
| ~ subset(A,sK1(inclusion_relation(B),B))
| in(unordered_pair(singleton(A),unordered_pair(A,sK1(inclusion_relation(B),B))),inclusion_relation(B))
| ~ in(A,B) ),
inference(resolve,[status(thm)],[c_448,c_632]) ).
cnf(c_5777,plain,
( subset(sK0(inclusion_relation(A),A),sK2(inclusion_relation(A),A))
| ~ in(sK2(inclusion_relation(A),A),A)
| ~ in(sK0(inclusion_relation(A),A),A)
| transitive(inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_630,c_449]) ).
cnf(c_11842,plain,
( transitive(inclusion_relation(A))
| subset(sK0(inclusion_relation(A),A),sK2(inclusion_relation(A),A))
| ~ in(sK2(inclusion_relation(A),A),A)
| transitive(inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_5777,c_634]) ).
cnf(c_5891,plain,
( subset(sK0(inclusion_relation(A),A),sK2(inclusion_relation(A),A))
| ~ in(sK2(inclusion_relation(A),A),A)
| transitive(inclusion_relation(A)) ),
inference(copy,[status(thm)],[c_11842]) ).
cnf(c_11843,plain,
( transitive(inclusion_relation(A))
| subset(sK0(inclusion_relation(A),A),sK2(inclusion_relation(A),A))
| transitive(inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_5891,c_633]) ).
cnf(c_5893,plain,
( subset(sK0(inclusion_relation(A),A),sK2(inclusion_relation(A),A))
| transitive(inclusion_relation(A)) ),
inference(copy,[status(thm)],[c_11843]) ).
cnf(c_5920,plain,
( subset(sK0(inclusion_relation(A),A),B)
| ~ subset(sK2(inclusion_relation(A),A),B)
| transitive(inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_5893,c_228]) ).
cnf(c_6270,plain,
( subset(sK2(inclusion_relation(A),A),sK1(inclusion_relation(A),A))
| ~ in(sK1(inclusion_relation(A),A),A)
| ~ in(sK2(inclusion_relation(A),A),A)
| transitive(inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_631,c_449]) ).
cnf(c_11844,plain,
( transitive(inclusion_relation(A))
| subset(sK2(inclusion_relation(A),A),sK1(inclusion_relation(A),A))
| ~ in(sK1(inclusion_relation(A),A),A)
| transitive(inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_6270,c_633]) ).
cnf(c_6297,plain,
( subset(sK2(inclusion_relation(A),A),sK1(inclusion_relation(A),A))
| ~ in(sK1(inclusion_relation(A),A),A)
| transitive(inclusion_relation(A)) ),
inference(copy,[status(thm)],[c_11844]) ).
cnf(c_11845,plain,
( transitive(inclusion_relation(A))
| subset(sK2(inclusion_relation(A),A),sK1(inclusion_relation(A),A))
| transitive(inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_6297,c_632]) ).
cnf(c_6299,plain,
( subset(sK2(inclusion_relation(A),A),sK1(inclusion_relation(A),A))
| transitive(inclusion_relation(A)) ),
inference(copy,[status(thm)],[c_11845]) ).
cnf(c_11846,plain,
( subset(sK0(inclusion_relation(A),A),sK1(inclusion_relation(A),A))
| transitive(inclusion_relation(A))
| transitive(inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_6299,c_5920]) ).
cnf(c_6301,plain,
( subset(sK0(inclusion_relation(A),A),sK1(inclusion_relation(A),A))
| transitive(inclusion_relation(A)) ),
inference(copy,[status(thm)],[c_11846]) ).
cnf(c_11847,plain,
( transitive(inclusion_relation(A))
| transitive(inclusion_relation(A))
| in(unordered_pair(singleton(sK0(inclusion_relation(A),A)),unordered_pair(sK0(inclusion_relation(A),A),sK1(inclusion_relation(A),A))),inclusion_relation(A))
| ~ in(sK0(inclusion_relation(A),A),A) ),
inference(resolve,[status(thm)],[c_1992,c_6301]) ).
cnf(c_8960,plain,
( transitive(inclusion_relation(A))
| in(unordered_pair(singleton(sK0(inclusion_relation(A),A)),unordered_pair(sK0(inclusion_relation(A),A),sK1(inclusion_relation(A),A))),inclusion_relation(A))
| ~ in(sK0(inclusion_relation(A),A),A) ),
inference(copy,[status(thm)],[c_11847]) ).
cnf(c_11848,plain,
( transitive(inclusion_relation(A))
| transitive(inclusion_relation(A))
| in(unordered_pair(singleton(sK0(inclusion_relation(A),A)),unordered_pair(sK0(inclusion_relation(A),A),sK1(inclusion_relation(A),A))),inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_8960,c_634]) ).
cnf(c_11791,plain,
( transitive(inclusion_relation(A))
| in(unordered_pair(singleton(sK0(inclusion_relation(A),A)),unordered_pair(sK0(inclusion_relation(A),A),sK1(inclusion_relation(A),A))),inclusion_relation(A)) ),
inference(copy,[status(thm)],[c_11848]) ).
cnf(c_11822,plain,
( is_transitive_in(inclusion_relation(A),A)
| transitive(inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_11791,c_276]) ).
cnf(c_11849,plain,
( transitive(inclusion_relation(A))
| transitive(inclusion_relation(A)) ),
inference(resolve,[status(thm)],[c_11822,c_371]) ).
cnf(c_11835,plain,
transitive(inclusion_relation(A)),
inference(copy,[status(thm)],[c_11849]) ).
cnf(c_11836,plain,
$false,
inference(resolve,[status(thm)],[c_11835,c_219]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU269+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n003.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 09:03:39 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 2509706 was started by sandbox2 on n003,
% 0.08/0.36 % Sat Sep 26 09:03:39 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.37
% 0.13/0.37 % From the command line: assign(max_seconds, 300).
% 19.98/3.30
% 19.98/3.30 % given #500 (A,wt=87): 441 -in(A,B) | -in(C,B) | -in(D,B) | -in(unordered_pair(singleton(A),unordered_pair(A,C)),inclusion_relation(E)) | -in(unordered_pair(singleton(C),unordered_pair(C,D)),inclusion_relation(E)) | in(unordered_pair(singleton(A),unordered_pair(A,D)),inclusion_relation(E)) | in(unordered_pair(singleton(f3(inclusion_relation(E),B)),unordered_pair(f3(inclusion_relation(E),B),f4(inclusion_relation(E),B))),inclusion_relation(E)). [resolve(279,a,278,a)].
% 19.98/3.30
% 19.98/3.30 % given #1000 (T,wt=51): 1123 transitive(c1) | inclusion_relation(relation_field(c1)) != c9 | in(unordered_pair(singleton(f4(c1,relation_field(c1))),unordered_pair(f4(c1,relation_field(c1)),f4(c1,relation_field(c1)))),c9). [resolve(357,a,247,b)].
% 19.98/3.30
% 19.98/3.30 % SZS status Theorem for theBenchmark
% 19.98/3.30
% 19.98/3.30 % Proof 1 at 2.36 (+ 0.47) seconds.
% 19.98/3.30 % Length of proof is 61.
% 19.98/3.30 % Level of proof is 15.
% 19.98/3.30 % Maximum clause weight is 54.000.
% 19.98/3.30 % Given clauses 1413.
% 19.98/3.30
% 19.98/3.30 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------