%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU356+1 : 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 : n026.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:54 AM UTC 2026
% Result : Theorem 1.05s 0.74s
% Output : CNFRefutation 1.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 3
% Syntax : Number of formulae : 191 ( 11 unt; 0 def)
% Number of atoms : 934 ( 42 equ)
% Maximal formula atoms : 107 ( 4 avg)
% Number of connectives : 1123 ( 380 ~; 651 |; 72 &)
% ( 3 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-3 aty)
% Number of variables : 203 ( 0 sgn 89 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d7_yellow_0,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( ex_sup_of_relstr_set(A,B)
<=> ? [C] :
( ! [D] :
( element(D,the_carrier(A))
=> ( ( ! [E] :
( element(E,the_carrier(A))
=> ( relstr_set_smaller(A,B,E)
=> related(A,D,E) ) )
& relstr_set_smaller(A,B,D) )
=> D = C ) )
& ! [D] :
( element(D,the_carrier(A))
=> ( relstr_set_smaller(A,B,D)
=> related(A,C,D) ) )
& relstr_set_smaller(A,B,C)
& element(C,the_carrier(A)) ) ) ),
file('theBenchmark.p',d7_yellow_0) ).
fof(t25_orders_2,axiom,
! [A] :
( ( rel_str(A)
& antisymmetric_relstr(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ( ( related(A,C,B)
& related(A,B,C) )
=> B = C ) ) ) ),
file('theBenchmark.p',t25_orders_2) ).
fof(t15_yellow_0,conjecture,
! [A] :
( ( rel_str(A)
& antisymmetric_relstr(A) )
=> ! [B] :
( ex_sup_of_relstr_set(A,B)
<=> ? [C] :
( ! [D] :
( element(D,the_carrier(A))
=> ( relstr_set_smaller(A,B,D)
=> related(A,C,D) ) )
& relstr_set_smaller(A,B,C)
& element(C,the_carrier(A)) ) ) ),
file('theBenchmark.p',t15_yellow_0) ).
fof(t15_yellow_0_neg,negated_conjecture,
~ ! [A] :
( ( rel_str(A)
& antisymmetric_relstr(A) )
=> ! [B] :
( ex_sup_of_relstr_set(A,B)
<=> ? [C] :
( ! [D] :
( element(D,the_carrier(A))
=> ( relstr_set_smaller(A,B,D)
=> related(A,C,D) ) )
& relstr_set_smaller(A,B,C)
& element(C,the_carrier(A)) ) ) ),
inference(assume_negation,[status(cth)],[t15_yellow_0]) ).
fof(nnf_1,plain,
! [A] :
( ! [B] :
( ( ! [C] :
( ? [D] :
( D != C
& ! [E] :
( related(A,D,E)
| ~ relstr_set_smaller(A,B,E)
| ~ element(E,the_carrier(A)) )
& relstr_set_smaller(A,B,D)
& element(D,the_carrier(A)) )
| ? [X4] :
( ~ related(A,C,X4)
& relstr_set_smaller(A,B,X4)
& element(X4,the_carrier(A)) )
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A)) )
| ex_sup_of_relstr_set(A,B) )
& ( ? [X0] :
( ! [X2] :
( X2 = X0
| ? [X3] :
( ~ related(A,X2,X3)
& relstr_set_smaller(A,B,X3)
& element(X3,the_carrier(A)) )
| ~ relstr_set_smaller(A,B,X2)
| ~ element(X2,the_carrier(A)) )
& ! [X1] :
( related(A,X0,X1)
| ~ relstr_set_smaller(A,B,X1)
| ~ element(X1,the_carrier(A)) )
& relstr_set_smaller(A,B,X0)
& element(X0,the_carrier(A)) )
| ~ ex_sup_of_relstr_set(A,B) ) )
| ~ rel_str(A) ),
inference(fof_nnf,[status(thm)],[d7_yellow_0]) ).
fof(sk_d7_yellow_0_sk,plain,
! [A] :
( ! [B] :
( ( ! [C] :
( ( sK1(A,B,C) != C
& ! [E] :
( related(A,sK1(A,B,C),E)
| ~ relstr_set_smaller(A,B,E)
| ~ element(E,the_carrier(A)) )
& relstr_set_smaller(A,B,sK1(A,B,C))
& element(sK1(A,B,C),the_carrier(A)) )
| ( ~ related(A,C,sK0(A,B,C))
& relstr_set_smaller(A,B,sK0(A,B,C))
& element(sK0(A,B,C),the_carrier(A)) )
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A)) )
| ex_sup_of_relstr_set(A,B) )
& ( ( ! [X2] :
( X2 = sK2(A,B)
| ( ~ related(A,X2,sK7(A,B,X2))
& relstr_set_smaller(A,B,sK7(A,B,X2))
& element(sK7(A,B,X2),the_carrier(A)) )
| ~ relstr_set_smaller(A,B,X2)
| ~ element(X2,the_carrier(A)) )
& ! [X1] :
( related(A,sK2(A,B),X1)
| ~ relstr_set_smaller(A,B,X1)
| ~ element(X1,the_carrier(A)) )
& relstr_set_smaller(A,B,sK2(A,B))
& element(sK2(A,B),the_carrier(A)) )
| ~ ex_sup_of_relstr_set(A,B) ) )
| ~ rel_str(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK7,sK0,sK1]),skolemize(X0,sK2(A,B)),skolemize(X3,sK7(A,B,X2)),skolemize(X4,sK0(A,B,C)),skolemize(D,sK1(A,B,C))],[nnf_1]) ).
fof(sk_d7_yellow_0,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( sK1(VAR_0,VAR_1,VAR_2) != VAR_2
| ~ related(VAR_0,VAR_2,sK0(VAR_0,VAR_1,VAR_2))
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( related(VAR_0,sK1(VAR_0,VAR_1,VAR_2),VAR_3)
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_3)
| ~ element(VAR_3,the_carrier(VAR_0))
| ~ related(VAR_0,VAR_2,sK0(VAR_0,VAR_1,VAR_2))
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( relstr_set_smaller(VAR_0,VAR_1,sK1(VAR_0,VAR_1,VAR_2))
| ~ related(VAR_0,VAR_2,sK0(VAR_0,VAR_1,VAR_2))
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( element(sK1(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
| ~ related(VAR_0,VAR_2,sK0(VAR_0,VAR_1,VAR_2))
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK1(VAR_0,VAR_1,VAR_2) != VAR_2
| relstr_set_smaller(VAR_0,VAR_1,sK0(VAR_0,VAR_1,VAR_2))
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( related(VAR_0,sK1(VAR_0,VAR_1,VAR_2),VAR_3)
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_3)
| ~ element(VAR_3,the_carrier(VAR_0))
| relstr_set_smaller(VAR_0,VAR_1,sK0(VAR_0,VAR_1,VAR_2))
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( relstr_set_smaller(VAR_0,VAR_1,sK1(VAR_0,VAR_1,VAR_2))
| relstr_set_smaller(VAR_0,VAR_1,sK0(VAR_0,VAR_1,VAR_2))
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( element(sK1(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
| relstr_set_smaller(VAR_0,VAR_1,sK0(VAR_0,VAR_1,VAR_2))
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( sK1(VAR_0,VAR_1,VAR_2) != VAR_2
| element(sK0(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( related(VAR_0,sK1(VAR_0,VAR_1,VAR_2),VAR_3)
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_3)
| ~ element(VAR_3,the_carrier(VAR_0))
| element(sK0(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( relstr_set_smaller(VAR_0,VAR_1,sK1(VAR_0,VAR_1,VAR_2))
| element(sK0(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( element(sK1(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
| element(sK0(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( VAR_2 = sK2(VAR_0,VAR_1)
| ~ related(VAR_0,VAR_2,sK7(VAR_0,VAR_1,VAR_2))
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ~ ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( VAR_2 = sK2(VAR_0,VAR_1)
| relstr_set_smaller(VAR_0,VAR_1,sK7(VAR_0,VAR_1,VAR_2))
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ~ ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( VAR_2 = sK2(VAR_0,VAR_1)
| element(sK7(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ~ ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( related(VAR_0,sK2(VAR_0,VAR_1),VAR_2)
| ~ relstr_set_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ~ ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1] :
( relstr_set_smaller(VAR_0,VAR_1,sK2(VAR_0,VAR_1))
| ~ ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1] :
( element(sK2(VAR_0,VAR_1),the_carrier(VAR_0))
| ~ ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d7_yellow_0_sk]) ).
cnf(c_13,plain,
( sK1(A,B,C) != C
| ~ related(A,C,sK0(A,B,C))
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_sup_of_relstr_set(A,B)
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d7_yellow_0]) ).
cnf(c_14,plain,
( related(A,sK1(A,B,C),D)
| ~ relstr_set_smaller(A,B,D)
| ~ element(D,the_carrier(A))
| ~ related(A,C,sK0(A,B,C))
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_sup_of_relstr_set(A,B)
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d7_yellow_0]) ).
cnf(c_15,plain,
( relstr_set_smaller(A,B,sK1(A,B,C))
| ~ related(A,C,sK0(A,B,C))
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_sup_of_relstr_set(A,B)
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d7_yellow_0]) ).
cnf(c_16,plain,
( element(sK1(A,B,C),the_carrier(A))
| ~ related(A,C,sK0(A,B,C))
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_sup_of_relstr_set(A,B)
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d7_yellow_0]) ).
cnf(c_17,plain,
( sK1(A,B,C) != C
| relstr_set_smaller(A,B,sK0(A,B,C))
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_sup_of_relstr_set(A,B)
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d7_yellow_0]) ).
cnf(c_18,plain,
( related(A,sK1(A,B,C),D)
| ~ relstr_set_smaller(A,B,D)
| ~ element(D,the_carrier(A))
| relstr_set_smaller(A,B,sK0(A,B,C))
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_sup_of_relstr_set(A,B)
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d7_yellow_0]) ).
cnf(c_19,plain,
( relstr_set_smaller(A,B,sK1(A,B,C))
| relstr_set_smaller(A,B,sK0(A,B,C))
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_sup_of_relstr_set(A,B)
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d7_yellow_0]) ).
cnf(c_20,plain,
( element(sK1(A,B,C),the_carrier(A))
| relstr_set_smaller(A,B,sK0(A,B,C))
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_sup_of_relstr_set(A,B)
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d7_yellow_0]) ).
cnf(c_21,plain,
( sK1(A,B,C) != C
| element(sK0(A,B,C),the_carrier(A))
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_sup_of_relstr_set(A,B)
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d7_yellow_0]) ).
cnf(c_22,plain,
( related(A,sK1(A,B,C),D)
| ~ relstr_set_smaller(A,B,D)
| ~ element(D,the_carrier(A))
| element(sK0(A,B,C),the_carrier(A))
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_sup_of_relstr_set(A,B)
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d7_yellow_0]) ).
cnf(c_23,plain,
( relstr_set_smaller(A,B,sK1(A,B,C))
| element(sK0(A,B,C),the_carrier(A))
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_sup_of_relstr_set(A,B)
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d7_yellow_0]) ).
cnf(c_24,plain,
( element(sK1(A,B,C),the_carrier(A))
| element(sK0(A,B,C),the_carrier(A))
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_sup_of_relstr_set(A,B)
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d7_yellow_0]) ).
cnf(c_28,plain,
( related(A,sK2(A,B),C)
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ~ ex_sup_of_relstr_set(A,B)
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d7_yellow_0]) ).
cnf(c_29,plain,
( relstr_set_smaller(A,B,sK2(A,B))
| ~ ex_sup_of_relstr_set(A,B)
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d7_yellow_0]) ).
cnf(c_30,plain,
( element(sK2(A,B),the_carrier(A))
| ~ ex_sup_of_relstr_set(A,B)
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d7_yellow_0]) ).
cnf(c_31,plain,
( C = B
| ~ related(A,C,B)
| ~ related(A,B,C)
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ rel_str(A)
| ~ antisymmetric_relstr(A) ),
inference(clausify,[status(thm)],[t25_orders_2]) ).
fof(nnf_10,plain,
? [A] :
( ? [B] :
( ( ! [C] :
( ? [D] :
( ~ related(A,C,D)
& relstr_set_smaller(A,B,D)
& element(D,the_carrier(A)) )
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A)) )
| ~ ex_sup_of_relstr_set(A,B) )
& ( ? [X4] :
( ! [X0] :
( related(A,X4,X0)
| ~ relstr_set_smaller(A,B,X0)
| ~ element(X0,the_carrier(A)) )
& relstr_set_smaller(A,B,X4)
& element(X4,the_carrier(A)) )
| ex_sup_of_relstr_set(A,B) ) )
& rel_str(A)
& antisymmetric_relstr(A) ),
inference(fof_nnf,[status(thm)],[t15_yellow_0_neg]) ).
fof(sk_t15_yellow_0_neg_sk,plain,
( ( ! [C] :
( ( ~ related(sK3,C,sK6(C))
& relstr_set_smaller(sK3,sK4,sK6(C))
& element(sK6(C),the_carrier(sK3)) )
| ~ relstr_set_smaller(sK3,sK4,C)
| ~ element(C,the_carrier(sK3)) )
| ~ ex_sup_of_relstr_set(sK3,sK4) )
& ( ( ! [X0] :
( related(sK3,sK5,X0)
| ~ relstr_set_smaller(sK3,sK4,X0)
| ~ element(X0,the_carrier(sK3)) )
& relstr_set_smaller(sK3,sK4,sK5)
& element(sK5,the_carrier(sK3)) )
| ex_sup_of_relstr_set(sK3,sK4) )
& rel_str(sK3)
& antisymmetric_relstr(sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6]),skolemize(A,sK3),skolemize(B,sK4),skolemize(X4,sK5),skolemize(D,sK6(C))],[nnf_10]) ).
fof(sk_t15_yellow_0_neg,plain,
( ! [VAR_0] :
( ~ related(sK3,VAR_0,sK6(VAR_0))
| ~ relstr_set_smaller(sK3,sK4,VAR_0)
| ~ element(VAR_0,the_carrier(sK3))
| ~ ex_sup_of_relstr_set(sK3,sK4) )
& ! [VAR_0] :
( relstr_set_smaller(sK3,sK4,sK6(VAR_0))
| ~ relstr_set_smaller(sK3,sK4,VAR_0)
| ~ element(VAR_0,the_carrier(sK3))
| ~ ex_sup_of_relstr_set(sK3,sK4) )
& ! [VAR_0] :
( element(sK6(VAR_0),the_carrier(sK3))
| ~ relstr_set_smaller(sK3,sK4,VAR_0)
| ~ element(VAR_0,the_carrier(sK3))
| ~ ex_sup_of_relstr_set(sK3,sK4) )
& ! [VAR_0] :
( related(sK3,sK5,VAR_0)
| ~ relstr_set_smaller(sK3,sK4,VAR_0)
| ~ element(VAR_0,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) )
& ( relstr_set_smaller(sK3,sK4,sK5)
| ex_sup_of_relstr_set(sK3,sK4) )
& ( element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) )
& rel_str(sK3)
& antisymmetric_relstr(sK3) ),
inference(cnf_transformation,[status(thm)],[sk_t15_yellow_0_neg_sk]) ).
cnf(c_32,negated_conjecture,
rel_str(sK3),
inference(split_conjunct,[status(thm)],[sk_t15_yellow_0_neg]) ).
cnf(c_34,negated_conjecture,
antisymmetric_relstr(sK3),
inference(split_conjunct,[status(thm)],[sk_t15_yellow_0_neg]) ).
cnf(c_35,negated_conjecture,
( element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(split_conjunct,[status(thm)],[sk_t15_yellow_0_neg]) ).
cnf(c_36,negated_conjecture,
( relstr_set_smaller(sK3,sK4,sK5)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(split_conjunct,[status(thm)],[sk_t15_yellow_0_neg]) ).
cnf(c_37,negated_conjecture,
( related(sK3,sK5,A)
| ~ relstr_set_smaller(sK3,sK4,A)
| ~ element(A,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(split_conjunct,[status(thm)],[sk_t15_yellow_0_neg]) ).
cnf(c_38,negated_conjecture,
( element(sK6(A),the_carrier(sK3))
| ~ relstr_set_smaller(sK3,sK4,A)
| ~ element(A,the_carrier(sK3))
| ~ ex_sup_of_relstr_set(sK3,sK4) ),
inference(split_conjunct,[status(thm)],[sk_t15_yellow_0_neg]) ).
cnf(c_39,negated_conjecture,
( relstr_set_smaller(sK3,sK4,sK6(A))
| ~ relstr_set_smaller(sK3,sK4,A)
| ~ element(A,the_carrier(sK3))
| ~ ex_sup_of_relstr_set(sK3,sK4) ),
inference(split_conjunct,[status(thm)],[sk_t15_yellow_0_neg]) ).
cnf(c_40,negated_conjecture,
( ~ related(sK3,A,sK6(A))
| ~ relstr_set_smaller(sK3,sK4,A)
| ~ element(A,the_carrier(sK3))
| ~ ex_sup_of_relstr_set(sK3,sK4) ),
inference(split_conjunct,[status(thm)],[sk_t15_yellow_0_neg]) ).
cnf(c_63,negated_conjecture,
( B = A
| ~ related(sK3,B,A)
| ~ related(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ~ element(A,the_carrier(sK3))
| ~ antisymmetric_relstr(sK3) ),
inference(resolve,[status(thm)],[c_32,c_31]) ).
cnf(c_64,negated_conjecture,
( B = A
| ~ related(sK3,B,A)
| ~ related(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ~ element(A,the_carrier(sK3)) ),
inference(resolve,[status(thm)],[c_34,c_63]) ).
cnf(c_65,negated_conjecture,
( sK1(sK3,A,B) != B
| ~ related(sK3,B,sK0(sK3,A,B))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(resolve,[status(thm)],[c_32,c_13]) ).
cnf(c_66,negated_conjecture,
( related(sK3,sK1(sK3,A,B),C)
| ~ relstr_set_smaller(sK3,A,C)
| ~ element(C,the_carrier(sK3))
| ~ related(sK3,B,sK0(sK3,A,B))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(resolve,[status(thm)],[c_32,c_14]) ).
cnf(c_67,negated_conjecture,
( relstr_set_smaller(sK3,A,sK1(sK3,A,B))
| ~ related(sK3,B,sK0(sK3,A,B))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(resolve,[status(thm)],[c_32,c_15]) ).
cnf(c_68,negated_conjecture,
( element(sK1(sK3,A,B),the_carrier(sK3))
| ~ related(sK3,B,sK0(sK3,A,B))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(resolve,[status(thm)],[c_32,c_16]) ).
cnf(c_69,negated_conjecture,
( sK1(sK3,A,B) != B
| relstr_set_smaller(sK3,A,sK0(sK3,A,B))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(resolve,[status(thm)],[c_32,c_17]) ).
cnf(c_70,negated_conjecture,
( related(sK3,sK1(sK3,A,B),C)
| ~ relstr_set_smaller(sK3,A,C)
| ~ element(C,the_carrier(sK3))
| relstr_set_smaller(sK3,A,sK0(sK3,A,B))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(resolve,[status(thm)],[c_32,c_18]) ).
cnf(c_71,negated_conjecture,
( relstr_set_smaller(sK3,A,sK1(sK3,A,B))
| relstr_set_smaller(sK3,A,sK0(sK3,A,B))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(resolve,[status(thm)],[c_32,c_19]) ).
cnf(c_72,negated_conjecture,
( element(sK1(sK3,A,B),the_carrier(sK3))
| relstr_set_smaller(sK3,A,sK0(sK3,A,B))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(resolve,[status(thm)],[c_32,c_20]) ).
cnf(c_73,negated_conjecture,
( sK1(sK3,A,B) != B
| element(sK0(sK3,A,B),the_carrier(sK3))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(resolve,[status(thm)],[c_32,c_21]) ).
cnf(c_74,negated_conjecture,
( related(sK3,sK1(sK3,A,B),C)
| ~ relstr_set_smaller(sK3,A,C)
| ~ element(C,the_carrier(sK3))
| element(sK0(sK3,A,B),the_carrier(sK3))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(resolve,[status(thm)],[c_32,c_22]) ).
cnf(c_75,negated_conjecture,
( relstr_set_smaller(sK3,A,sK1(sK3,A,B))
| element(sK0(sK3,A,B),the_carrier(sK3))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(resolve,[status(thm)],[c_32,c_23]) ).
cnf(c_76,negated_conjecture,
( element(sK1(sK3,A,B),the_carrier(sK3))
| element(sK0(sK3,A,B),the_carrier(sK3))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(resolve,[status(thm)],[c_32,c_24]) ).
cnf(c_83,negated_conjecture,
( related(sK3,sK2(sK3,A),B)
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ~ ex_sup_of_relstr_set(sK3,A) ),
inference(resolve,[status(thm)],[c_32,c_28]) ).
cnf(c_84,negated_conjecture,
( relstr_set_smaller(sK3,A,sK2(sK3,A))
| ~ ex_sup_of_relstr_set(sK3,A) ),
inference(resolve,[status(thm)],[c_32,c_29]) ).
cnf(c_85,negated_conjecture,
( element(sK2(sK3,A),the_carrier(sK3))
| ~ ex_sup_of_relstr_set(sK3,A) ),
inference(resolve,[status(thm)],[c_32,c_30]) ).
cnf(c_1625,plain,
( related(sK3,sK1(sK3,A,B),B)
| ~ relstr_set_smaller(sK3,A,B)
| ~ related(sK3,B,sK0(sK3,A,B))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(factor,[status(thm)],[c_66]) ).
cnf(c_89,plain,
( related(sK3,sK1(sK3,A,B),B)
| ~ related(sK3,B,sK0(sK3,A,B))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(copy,[status(thm)],[c_1625]) ).
cnf(c_1626,plain,
( related(sK3,sK1(sK3,A,B),B)
| ~ relstr_set_smaller(sK3,A,B)
| relstr_set_smaller(sK3,A,sK0(sK3,A,B))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(factor,[status(thm)],[c_70]) ).
cnf(c_90,plain,
( related(sK3,sK1(sK3,A,B),B)
| relstr_set_smaller(sK3,A,sK0(sK3,A,B))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(copy,[status(thm)],[c_1626]) ).
cnf(c_1627,plain,
( related(sK3,sK1(sK3,A,B),B)
| ~ relstr_set_smaller(sK3,A,B)
| element(sK0(sK3,A,B),the_carrier(sK3))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(factor,[status(thm)],[c_74]) ).
cnf(c_91,plain,
( related(sK3,sK1(sK3,A,B),B)
| element(sK0(sK3,A,B),the_carrier(sK3))
| ~ relstr_set_smaller(sK3,A,B)
| ~ element(B,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,A) ),
inference(copy,[status(thm)],[c_1627]) ).
cnf(c_1628,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| sK1(sK3,sK4,sK5) != sK5
| relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_69,c_36]) ).
cnf(c_93,negated_conjecture,
( sK1(sK3,sK4,sK5) != sK5
| relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1628]) ).
cnf(c_1629,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_71,c_36]) ).
cnf(c_96,negated_conjecture,
( relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1629]) ).
cnf(c_1630,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_72,c_36]) ).
cnf(c_97,negated_conjecture,
( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1630]) ).
cnf(c_1631,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| sK1(sK3,sK4,sK5) != sK5
| element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_73,c_36]) ).
cnf(c_98,negated_conjecture,
( sK1(sK3,sK4,sK5) != sK5
| element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1631]) ).
cnf(c_1632,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_75,c_36]) ).
cnf(c_101,negated_conjecture,
( relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1632]) ).
cnf(c_1633,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_76,c_36]) ).
cnf(c_102,negated_conjecture,
( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1633]) ).
cnf(c_103,plain,
( relstr_set_smaller(sK3,sK4,sK5)
| relstr_set_smaller(sK3,sK4,sK2(sK3,sK4)) ),
inference(resolve,[status(thm)],[c_84,c_36]) ).
cnf(c_105,plain,
( relstr_set_smaller(sK3,sK4,sK5)
| element(sK2(sK3,sK4),the_carrier(sK3)) ),
inference(resolve,[status(thm)],[c_85,c_36]) ).
cnf(c_1634,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| related(sK3,sK1(sK3,sK4,sK5),sK5)
| relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_90,c_36]) ).
cnf(c_107,negated_conjecture,
( related(sK3,sK1(sK3,sK4,sK5),sK5)
| relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1634]) ).
cnf(c_1635,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| related(sK3,sK1(sK3,sK4,sK5),sK5)
| element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_91,c_36]) ).
cnf(c_108,negated_conjecture,
( related(sK3,sK1(sK3,sK4,sK5),sK5)
| element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1635]) ).
cnf(c_1636,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| sK1(sK3,sK4,sK5) != sK5
| relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_93,c_35]) ).
cnf(c_110,negated_conjecture,
( sK1(sK3,sK4,sK5) != sK5
| relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1636]) ).
cnf(c_114,plain,
( relstr_set_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
| ~ element(sK2(sK3,sK4),the_carrier(sK3))
| ~ ex_sup_of_relstr_set(sK3,sK4)
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(resolve,[status(thm)],[c_103,c_39]) ).
cnf(c_115,plain,
( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
| ~ element(sK2(sK3,sK4),the_carrier(sK3))
| ~ ex_sup_of_relstr_set(sK3,sK4)
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(resolve,[status(thm)],[c_103,c_38]) ).
cnf(c_1637,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_96,c_35]) ).
cnf(c_121,negated_conjecture,
( relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1637]) ).
cnf(c_1638,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_97,c_35]) ).
cnf(c_124,negated_conjecture,
( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1638]) ).
cnf(c_1639,negated_conjecture,
( related(sK3,sK5,sK0(sK3,sK4,sK5))
| ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4)
| relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_121,c_37]) ).
cnf(c_143,negated_conjecture,
( related(sK3,sK5,sK0(sK3,sK4,sK5))
| ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1639]) ).
cnf(c_1640,negated_conjecture,
( related(sK3,sK5,sK0(sK3,sK4,sK5))
| ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4)
| element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_124,c_37]) ).
cnf(c_174,negated_conjecture,
( related(sK3,sK5,sK0(sK3,sK4,sK5))
| ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1640]) ).
cnf(c_1641,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| sK1(sK3,sK4,sK5) != sK5
| element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_98,c_35]) ).
cnf(c_177,negated_conjecture,
( sK1(sK3,sK4,sK5) != sK5
| element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1641]) ).
cnf(c_1642,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_101,c_35]) ).
cnf(c_183,negated_conjecture,
( relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1642]) ).
cnf(c_1643,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_102,c_35]) ).
cnf(c_210,negated_conjecture,
( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1643]) ).
cnf(c_1644,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| related(sK3,sK1(sK3,sK4,sK5),sK5)
| relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_107,c_35]) ).
cnf(c_213,negated_conjecture,
( related(sK3,sK1(sK3,sK4,sK5),sK5)
| relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1644]) ).
cnf(c_1645,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| related(sK3,sK1(sK3,sK4,sK5),sK5)
| element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_108,c_35]) ).
cnf(c_216,negated_conjecture,
( related(sK3,sK1(sK3,sK4,sK5),sK5)
| element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1645]) ).
cnf(c_1646,negated_conjecture,
( related(sK3,sK5,sK0(sK3,sK4,sK5))
| ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4)
| related(sK3,sK1(sK3,sK4,sK5),sK5)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_213,c_37]) ).
cnf(c_235,negated_conjecture,
( related(sK3,sK5,sK0(sK3,sK4,sK5))
| ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| related(sK3,sK1(sK3,sK4,sK5),sK5)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1646]) ).
cnf(c_1647,negated_conjecture,
( relstr_set_smaller(sK3,sK4,sK5)
| relstr_set_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
| ~ element(sK2(sK3,sK4),the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(resolve,[status(thm)],[c_114,c_36]) ).
cnf(c_261,negated_conjecture,
( relstr_set_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
| ~ element(sK2(sK3,sK4),the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(copy,[status(thm)],[c_1647]) ).
cnf(c_1648,negated_conjecture,
( relstr_set_smaller(sK3,sK4,sK5)
| element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
| ~ element(sK2(sK3,sK4),the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(resolve,[status(thm)],[c_115,c_36]) ).
cnf(c_269,negated_conjecture,
( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
| ~ element(sK2(sK3,sK4),the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(copy,[status(thm)],[c_1648]) ).
cnf(c_1649,plain,
( relstr_set_smaller(sK3,sK4,sK5)
| relstr_set_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(resolve,[status(thm)],[c_261,c_105]) ).
cnf(c_389,plain,
( relstr_set_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(copy,[status(thm)],[c_1649]) ).
cnf(c_395,plain,
( related(sK3,sK2(sK3,sK4),sK6(sK2(sK3,sK4)))
| ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
| ~ ex_sup_of_relstr_set(sK3,sK4)
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(resolve,[status(thm)],[c_389,c_83]) ).
cnf(c_1650,plain,
( relstr_set_smaller(sK3,sK4,sK5)
| element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(resolve,[status(thm)],[c_269,c_105]) ).
cnf(c_408,plain,
( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(copy,[status(thm)],[c_1650]) ).
cnf(c_1651,plain,
( relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4)
| related(sK3,sK5,sK0(sK3,sK4,sK5))
| relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_143,c_183]) ).
cnf(c_1652,plain,
( relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| related(sK3,sK5,sK0(sK3,sK4,sK5))
| relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1651]) ).
cnf(c_498,plain,
( related(sK3,sK5,sK0(sK3,sK4,sK5))
| relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1652]) ).
cnf(c_1653,negated_conjecture,
( relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| ~ relstr_set_smaller(sK3,sK4,sK5)
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4)
| relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_498,c_67]) ).
cnf(c_1654,negated_conjecture,
( relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| ~ relstr_set_smaller(sK3,sK4,sK5)
| ~ element(sK5,the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1653]) ).
cnf(c_521,negated_conjecture,
( ~ relstr_set_smaller(sK3,sK4,sK5)
| ~ element(sK5,the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1654]) ).
cnf(c_1655,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| ~ element(sK5,the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_521,c_36]) ).
cnf(c_528,negated_conjecture,
( ~ element(sK5,the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1655]) ).
cnf(c_1656,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_528,c_35]) ).
cnf(c_534,negated_conjecture,
( relstr_set_smaller(sK3,sK4,sK1(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1656]) ).
cnf(c_1657,negated_conjecture,
( related(sK3,sK5,sK1(sK3,sK4,sK5))
| ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_534,c_37]) ).
cnf(c_572,negated_conjecture,
( related(sK3,sK5,sK1(sK3,sK4,sK5))
| ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1657]) ).
cnf(c_1658,plain,
( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4)
| related(sK3,sK5,sK0(sK3,sK4,sK5))
| element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_174,c_210]) ).
cnf(c_1659,plain,
( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| related(sK3,sK5,sK0(sK3,sK4,sK5))
| element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1658]) ).
cnf(c_648,plain,
( related(sK3,sK5,sK0(sK3,sK4,sK5))
| element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1659]) ).
cnf(c_1660,negated_conjecture,
( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ~ relstr_set_smaller(sK3,sK4,sK5)
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4)
| element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_648,c_68]) ).
cnf(c_1661,negated_conjecture,
( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ~ relstr_set_smaller(sK3,sK4,sK5)
| ~ element(sK5,the_carrier(sK3))
| element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1660]) ).
cnf(c_656,negated_conjecture,
( ~ relstr_set_smaller(sK3,sK4,sK5)
| ~ element(sK5,the_carrier(sK3))
| element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1661]) ).
cnf(c_1662,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| ~ element(sK5,the_carrier(sK3))
| element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_656,c_36]) ).
cnf(c_691,negated_conjecture,
( ~ element(sK5,the_carrier(sK3))
| element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1662]) ).
cnf(c_1663,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_691,c_35]) ).
cnf(c_697,negated_conjecture,
( element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1663]) ).
cnf(c_1664,plain,
( related(sK3,sK5,sK1(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_697,c_572]) ).
cnf(c_703,plain,
( related(sK3,sK5,sK1(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1664]) ).
cnf(c_1665,negated_conjecture,
( sK5 = sK1(sK3,sK4,sK5)
| ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
| ~ element(sK5,the_carrier(sK3))
| ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_703,c_64]) ).
cnf(c_709,negated_conjecture,
( sK1(sK3,sK4,sK5) = sK5
| ~ related(sK3,sK1(sK3,sK4,sK5),sK5)
| ~ element(sK5,the_carrier(sK3))
| ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1665]) ).
cnf(c_1666,plain,
( related(sK3,sK1(sK3,sK4,sK5),sK5)
| ex_sup_of_relstr_set(sK3,sK4)
| related(sK3,sK5,sK0(sK3,sK4,sK5))
| related(sK3,sK1(sK3,sK4,sK5),sK5)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_235,c_216]) ).
cnf(c_1667,plain,
( related(sK3,sK1(sK3,sK4,sK5),sK5)
| related(sK3,sK5,sK0(sK3,sK4,sK5))
| related(sK3,sK1(sK3,sK4,sK5),sK5)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1666]) ).
cnf(c_726,plain,
( related(sK3,sK5,sK0(sK3,sK4,sK5))
| related(sK3,sK1(sK3,sK4,sK5),sK5)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1667]) ).
cnf(c_1668,plain,
( related(sK3,sK1(sK3,sK4,sK5),sK5)
| ~ relstr_set_smaller(sK3,sK4,sK5)
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4)
| related(sK3,sK1(sK3,sK4,sK5),sK5)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_726,c_89]) ).
cnf(c_1669,plain,
( related(sK3,sK1(sK3,sK4,sK5),sK5)
| ~ relstr_set_smaller(sK3,sK4,sK5)
| ~ element(sK5,the_carrier(sK3))
| related(sK3,sK1(sK3,sK4,sK5),sK5)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1668]) ).
cnf(c_733,plain,
( ~ relstr_set_smaller(sK3,sK4,sK5)
| ~ element(sK5,the_carrier(sK3))
| related(sK3,sK1(sK3,sK4,sK5),sK5)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1669]) ).
cnf(c_1670,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| ~ element(sK5,the_carrier(sK3))
| related(sK3,sK1(sK3,sK4,sK5),sK5)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_733,c_36]) ).
cnf(c_740,negated_conjecture,
( ~ element(sK5,the_carrier(sK3))
| related(sK3,sK1(sK3,sK4,sK5),sK5)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1670]) ).
cnf(c_1671,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| related(sK3,sK1(sK3,sK4,sK5),sK5)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_740,c_35]) ).
cnf(c_755,negated_conjecture,
( related(sK3,sK1(sK3,sK4,sK5),sK5)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1671]) ).
cnf(c_1672,negated_conjecture,
( relstr_set_smaller(sK3,sK4,sK5)
| related(sK3,sK2(sK3,sK4),sK6(sK2(sK3,sK4)))
| ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(resolve,[status(thm)],[c_395,c_36]) ).
cnf(c_847,negated_conjecture,
( related(sK3,sK2(sK3,sK4),sK6(sK2(sK3,sK4)))
| ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(copy,[status(thm)],[c_1672]) ).
cnf(c_1673,plain,
( relstr_set_smaller(sK3,sK4,sK5)
| related(sK3,sK2(sK3,sK4),sK6(sK2(sK3,sK4)))
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(resolve,[status(thm)],[c_847,c_408]) ).
cnf(c_1078,plain,
( related(sK3,sK2(sK3,sK4),sK6(sK2(sK3,sK4)))
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(copy,[status(thm)],[c_1673]) ).
cnf(c_1085,plain,
( ~ relstr_set_smaller(sK3,sK4,sK2(sK3,sK4))
| ~ element(sK2(sK3,sK4),the_carrier(sK3))
| ~ ex_sup_of_relstr_set(sK3,sK4)
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(resolve,[status(thm)],[c_1078,c_40]) ).
cnf(c_1674,plain,
( relstr_set_smaller(sK3,sK4,sK5)
| ~ element(sK2(sK3,sK4),the_carrier(sK3))
| ~ ex_sup_of_relstr_set(sK3,sK4)
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(resolve,[status(thm)],[c_1085,c_103]) ).
cnf(c_1094,plain,
( ~ element(sK2(sK3,sK4),the_carrier(sK3))
| ~ ex_sup_of_relstr_set(sK3,sK4)
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(copy,[status(thm)],[c_1674]) ).
cnf(c_1675,negated_conjecture,
( relstr_set_smaller(sK3,sK4,sK5)
| ~ element(sK2(sK3,sK4),the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(resolve,[status(thm)],[c_1094,c_36]) ).
cnf(c_1102,negated_conjecture,
( ~ element(sK2(sK3,sK4),the_carrier(sK3))
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(copy,[status(thm)],[c_1675]) ).
cnf(c_1676,plain,
( relstr_set_smaller(sK3,sK4,sK5)
| relstr_set_smaller(sK3,sK4,sK5) ),
inference(resolve,[status(thm)],[c_1102,c_105]) ).
cnf(c_1131,plain,
relstr_set_smaller(sK3,sK4,sK5),
inference(copy,[status(thm)],[c_1676]) ).
cnf(c_1677,plain,
( ex_sup_of_relstr_set(sK3,sK4)
| sK1(sK3,sK4,sK5) = sK5
| ~ element(sK5,the_carrier(sK3))
| ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_709,c_755]) ).
cnf(c_1336,plain,
( sK1(sK3,sK4,sK5) = sK5
| ~ element(sK5,the_carrier(sK3))
| ~ element(sK1(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1677]) ).
cnf(c_1678,plain,
( ex_sup_of_relstr_set(sK3,sK4)
| sK1(sK3,sK4,sK5) = sK5
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_1336,c_697]) ).
cnf(c_1340,plain,
( sK1(sK3,sK4,sK5) = sK5
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1678]) ).
cnf(c_1679,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| sK1(sK3,sK4,sK5) = sK5
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_1340,c_35]) ).
cnf(c_1346,negated_conjecture,
( sK1(sK3,sK4,sK5) = sK5
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1679]) ).
cnf(c_1680,plain,
( element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_1346,c_177]) ).
cnf(c_1354,plain,
( element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1680]) ).
cnf(c_1681,plain,
( relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_1346,c_110]) ).
cnf(c_1355,plain,
( relstr_set_smaller(sK3,sK4,sK0(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1681]) ).
cnf(c_1682,negated_conjecture,
( related(sK3,sK5,sK0(sK3,sK4,sK5))
| ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_1355,c_37]) ).
cnf(c_1388,negated_conjecture,
( related(sK3,sK5,sK0(sK3,sK4,sK5))
| ~ element(sK0(sK3,sK4,sK5),the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1682]) ).
cnf(c_1683,plain,
( ex_sup_of_relstr_set(sK3,sK4)
| related(sK3,sK5,sK0(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_1388,c_1354]) ).
cnf(c_1466,plain,
( related(sK3,sK5,sK0(sK3,sK4,sK5))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1683]) ).
cnf(c_1684,negated_conjecture,
( sK1(sK3,sK4,sK5) != sK5
| ~ relstr_set_smaller(sK3,sK4,sK5)
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_1466,c_65]) ).
cnf(c_1685,negated_conjecture,
( sK1(sK3,sK4,sK5) != sK5
| ~ relstr_set_smaller(sK3,sK4,sK5)
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1684]) ).
cnf(c_1477,negated_conjecture,
( sK1(sK3,sK4,sK5) != sK5
| ~ element(sK5,the_carrier(sK3))
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_1131,c_1685]) ).
cnf(c_1686,negated_conjecture,
( ex_sup_of_relstr_set(sK3,sK4)
| sK1(sK3,sK4,sK5) != sK5
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_1477,c_35]) ).
cnf(c_1501,negated_conjecture,
( sK1(sK3,sK4,sK5) != sK5
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(copy,[status(thm)],[c_1686]) ).
cnf(c_1687,plain,
( ex_sup_of_relstr_set(sK3,sK4)
| ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_1501,c_1346]) ).
cnf(c_1504,plain,
ex_sup_of_relstr_set(sK3,sK4),
inference(copy,[status(thm)],[c_1687]) ).
cnf(c_1557,negated_conjecture,
( ~ related(sK3,A,sK6(A))
| ~ relstr_set_smaller(sK3,sK4,A)
| ~ element(A,the_carrier(sK3)) ),
inference(resolve,[status(thm)],[c_1504,c_40]) ).
cnf(c_1558,negated_conjecture,
( relstr_set_smaller(sK3,sK4,sK6(A))
| ~ relstr_set_smaller(sK3,sK4,A)
| ~ element(A,the_carrier(sK3)) ),
inference(resolve,[status(thm)],[c_1504,c_39]) ).
cnf(c_1559,negated_conjecture,
( element(sK6(A),the_carrier(sK3))
| ~ relstr_set_smaller(sK3,sK4,A)
| ~ element(A,the_carrier(sK3)) ),
inference(resolve,[status(thm)],[c_1504,c_38]) ).
cnf(c_1560,plain,
element(sK2(sK3,sK4),the_carrier(sK3)),
inference(resolve,[status(thm)],[c_1504,c_85]) ).
cnf(c_1561,plain,
relstr_set_smaller(sK3,sK4,sK2(sK3,sK4)),
inference(resolve,[status(thm)],[c_1504,c_84]) ).
cnf(c_1688,negated_conjecture,
( ~ related(sK3,sK2(sK3,sK4),sK6(sK2(sK3,sK4)))
| ~ relstr_set_smaller(sK3,sK4,sK2(sK3,sK4)) ),
inference(resolve,[status(thm)],[c_1557,c_1560]) ).
cnf(c_1589,negated_conjecture,
~ related(sK3,sK2(sK3,sK4),sK6(sK2(sK3,sK4))),
inference(resolve,[status(thm)],[c_1688,c_1561]) ).
cnf(c_1689,negated_conjecture,
( relstr_set_smaller(sK3,sK4,sK6(sK2(sK3,sK4)))
| ~ element(sK2(sK3,sK4),the_carrier(sK3)) ),
inference(resolve,[status(thm)],[c_1558,c_1561]) ).
cnf(c_1607,negated_conjecture,
relstr_set_smaller(sK3,sK4,sK6(sK2(sK3,sK4))),
inference(resolve,[status(thm)],[c_1560,c_1689]) ).
cnf(c_1690,negated_conjecture,
( element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
| ~ element(sK2(sK3,sK4),the_carrier(sK3)) ),
inference(resolve,[status(thm)],[c_1559,c_1561]) ).
cnf(c_1609,negated_conjecture,
element(sK6(sK2(sK3,sK4)),the_carrier(sK3)),
inference(resolve,[status(thm)],[c_1560,c_1690]) ).
cnf(c_1691,negated_conjecture,
( related(sK3,sK2(sK3,sK4),sK6(sK2(sK3,sK4)))
| ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3))
| ~ ex_sup_of_relstr_set(sK3,sK4) ),
inference(resolve,[status(thm)],[c_1607,c_83]) ).
cnf(c_1692,negated_conjecture,
( related(sK3,sK2(sK3,sK4),sK6(sK2(sK3,sK4)))
| ~ element(sK6(sK2(sK3,sK4)),the_carrier(sK3)) ),
inference(resolve,[status(thm)],[c_1504,c_1691]) ).
cnf(c_1693,negated_conjecture,
related(sK3,sK2(sK3,sK4),sK6(sK2(sK3,sK4))),
inference(resolve,[status(thm)],[c_1609,c_1692]) ).
cnf(c_1624,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1589,c_1693]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU356+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.05/0.37 % Computer : n026.cluster.edu
% 0.05/0.37 % Model : x86_64 x86_64
% 0.05/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.37 % Memory : 8046.5625MB
% 0.05/0.37 % OS : Linux 6.8.0-71-generic
% 0.05/0.37 % CPULimit : 300
% 0.05/0.37 % WCLimit : 300
% 0.05/0.37 % DateTime : Sat Sep 26 09:21:10 UTC 2026
% 0.05/0.37 % CPUTime :
% 0.05/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.05/0.37 % Process 646712 was started by sandbox on n026,
% 0.05/0.37 % Sat Sep 26 09:21:10 2026
% 0.05/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.05/0.38
% 0.05/0.38 % From the command line: assign(max_seconds, 300).
% 1.05/0.74
% 1.05/0.74 % SZS status Theorem for theBenchmark
% 1.05/0.74
% 1.05/0.74 % Proof 1 at 0.11 (+ 0.03) seconds.
% 1.05/0.74 % Length of proof is 115.
% 1.05/0.74 % Level of proof is 24.
% 1.05/0.74 % Maximum clause weight is 43.000.
% 1.05/0.74 % Given clauses 361.
% 1.05/0.74
% 1.05/0.74 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------