%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU359+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 : n010.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:46:05 AM UTC 2026
% Result : Theorem 0.15s 5.45s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 76
% Number of leaves : 4
% Syntax : Number of formulae : 169 ( 15 unt; 0 def)
% Number of atoms : 743 ( 128 equ)
% Maximal formula atoms : 42 ( 4 avg)
% Number of connectives : 881 ( 307 ~; 474 |; 73 &)
% ( 2 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-3 aty)
% Number of variables : 162 ( 2 sgn 74 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d9_yellow_0,axiom,
! [A] :
( rel_str(A)
=> ! [B,C] :
( element(C,the_carrier(A))
=> ( ex_sup_of_relstr_set(A,B)
=> ( C = join_on_relstr(A,B)
<=> ( ! [D] :
( element(D,the_carrier(A))
=> ( relstr_set_smaller(A,B,D)
=> related(A,C,D) ) )
& relstr_set_smaller(A,B,C) ) ) ) ) ),
file('theBenchmark.p',d9_yellow_0) ).
fof(dt_k1_yellow_0,axiom,
! [A,B] :
( rel_str(A)
=> element(join_on_relstr(A,B),the_carrier(A)) ),
file('theBenchmark.p',dt_k1_yellow_0) ).
fof(t15_yellow_0,axiom,
! [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(t30_yellow_0,conjecture,
! [A] :
( ( rel_str(A)
& antisymmetric_relstr(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( ( ( ! [D] :
( element(D,the_carrier(A))
=> ( relstr_set_smaller(A,C,D)
=> related(A,B,D) ) )
& relstr_set_smaller(A,C,B) )
=> ( ex_sup_of_relstr_set(A,C)
& B = join_on_relstr(A,C) ) )
& ( ( ex_sup_of_relstr_set(A,C)
& B = join_on_relstr(A,C) )
=> ( ! [D] :
( element(D,the_carrier(A))
=> ( relstr_set_smaller(A,C,D)
=> related(A,B,D) ) )
& relstr_set_smaller(A,C,B) ) ) ) ) ),
file('theBenchmark.p',t30_yellow_0) ).
fof(t30_yellow_0_neg,negated_conjecture,
~ ! [A] :
( ( rel_str(A)
& antisymmetric_relstr(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( ( ( ! [D] :
( element(D,the_carrier(A))
=> ( relstr_set_smaller(A,C,D)
=> related(A,B,D) ) )
& relstr_set_smaller(A,C,B) )
=> ( ex_sup_of_relstr_set(A,C)
& B = join_on_relstr(A,C) ) )
& ( ( ex_sup_of_relstr_set(A,C)
& B = join_on_relstr(A,C) )
=> ( ! [D] :
( element(D,the_carrier(A))
=> ( relstr_set_smaller(A,C,D)
=> related(A,B,D) ) )
& relstr_set_smaller(A,C,B) ) ) ) ) ),
inference(assume_negation,[status(cth)],[t30_yellow_0]) ).
cnf(c_14,plain,
( element(join_on_relstr(A,B),the_carrier(A))
| ~ rel_str(A) ),
inference(clausify,[status(thm)],[dt_k1_yellow_0]) ).
fof(nnf_1,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)
| join_on_relstr(A,B) = C )
& ( ( ! [X0] :
( related(A,C,X0)
| ~ relstr_set_smaller(A,B,X0)
| ~ element(X0,the_carrier(A)) )
& relstr_set_smaller(A,B,C) )
| join_on_relstr(A,B) != C ) )
| ~ ex_sup_of_relstr_set(A,B)
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(fof_nnf,[status(thm)],[d9_yellow_0]) ).
fof(sk_d9_yellow_0_sk,plain,
! [A] :
( ! [B,C] :
( ( ( ( ~ 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)
| join_on_relstr(A,B) = C )
& ( ( ! [X0] :
( related(A,C,X0)
| ~ relstr_set_smaller(A,B,X0)
| ~ element(X0,the_carrier(A)) )
& relstr_set_smaller(A,B,C) )
| join_on_relstr(A,B) != C ) )
| ~ ex_sup_of_relstr_set(A,B)
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(D,sK0(A,B,C))],[nnf_1]) ).
fof(sk_d9_yellow_0,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ related(VAR_0,VAR_1,sK0(VAR_0,VAR_2,VAR_1))
| ~ relstr_set_smaller(VAR_0,VAR_2,VAR_1)
| join_on_relstr(VAR_0,VAR_2) = VAR_1
| ~ ex_sup_of_relstr_set(VAR_0,VAR_2)
| ~ element(VAR_1,the_carrier(VAR_0))
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( relstr_set_smaller(VAR_0,VAR_2,sK0(VAR_0,VAR_2,VAR_1))
| ~ relstr_set_smaller(VAR_0,VAR_2,VAR_1)
| join_on_relstr(VAR_0,VAR_2) = VAR_1
| ~ ex_sup_of_relstr_set(VAR_0,VAR_2)
| ~ element(VAR_1,the_carrier(VAR_0))
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( element(sK0(VAR_0,VAR_2,VAR_1),the_carrier(VAR_0))
| ~ relstr_set_smaller(VAR_0,VAR_2,VAR_1)
| join_on_relstr(VAR_0,VAR_2) = VAR_1
| ~ ex_sup_of_relstr_set(VAR_0,VAR_2)
| ~ element(VAR_1,the_carrier(VAR_0))
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( related(VAR_0,VAR_1,VAR_3)
| ~ relstr_set_smaller(VAR_0,VAR_2,VAR_3)
| ~ element(VAR_3,the_carrier(VAR_0))
| join_on_relstr(VAR_0,VAR_2) != VAR_1
| ~ ex_sup_of_relstr_set(VAR_0,VAR_2)
| ~ element(VAR_1,the_carrier(VAR_0))
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( relstr_set_smaller(VAR_0,VAR_2,VAR_1)
| join_on_relstr(VAR_0,VAR_2) != VAR_1
| ~ ex_sup_of_relstr_set(VAR_0,VAR_2)
| ~ element(VAR_1,the_carrier(VAR_0))
| ~ rel_str(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d9_yellow_0_sk]) ).
cnf(c_15,plain,
( ~ related(A,B,sK0(A,C,B))
| ~ relstr_set_smaller(A,C,B)
| join_on_relstr(A,C) = B
| ~ ex_sup_of_relstr_set(A,C)
| ~ element(B,the_carrier(A))
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d9_yellow_0]) ).
cnf(c_16,plain,
( relstr_set_smaller(A,C,sK0(A,C,B))
| ~ relstr_set_smaller(A,C,B)
| join_on_relstr(A,C) = B
| ~ ex_sup_of_relstr_set(A,C)
| ~ element(B,the_carrier(A))
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d9_yellow_0]) ).
cnf(c_17,plain,
( element(sK0(A,C,B),the_carrier(A))
| ~ relstr_set_smaller(A,C,B)
| join_on_relstr(A,C) = B
| ~ ex_sup_of_relstr_set(A,C)
| ~ element(B,the_carrier(A))
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d9_yellow_0]) ).
cnf(c_18,plain,
( related(A,B,D)
| ~ relstr_set_smaller(A,C,D)
| ~ element(D,the_carrier(A))
| join_on_relstr(A,C) != B
| ~ ex_sup_of_relstr_set(A,C)
| ~ element(B,the_carrier(A))
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d9_yellow_0]) ).
cnf(c_19,plain,
( relstr_set_smaller(A,C,B)
| join_on_relstr(A,C) != B
| ~ ex_sup_of_relstr_set(A,C)
| ~ element(B,the_carrier(A))
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d9_yellow_0]) ).
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) )
& ( ? [X0] :
( ! [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)
| ~ antisymmetric_relstr(A) ),
inference(fof_nnf,[status(thm)],[t15_yellow_0]) ).
fof(sk_t15_yellow_0_sk,plain,
! [A] :
( ! [B] :
( ( ! [C] :
( ( ~ related(A,C,sK1(A,B,C))
& relstr_set_smaller(A,B,sK1(A,B,C))
& element(sK1(A,B,C),the_carrier(A)) )
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A)) )
| ex_sup_of_relstr_set(A,B) )
& ( ( ! [X1] :
( related(A,sK6(A,B),X1)
| ~ relstr_set_smaller(A,B,X1)
| ~ element(X1,the_carrier(A)) )
& relstr_set_smaller(A,B,sK6(A,B))
& element(sK6(A,B),the_carrier(A)) )
| ~ ex_sup_of_relstr_set(A,B) ) )
| ~ rel_str(A)
| ~ antisymmetric_relstr(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK1]),skolemize(X0,sK6(A,B)),skolemize(D,sK1(A,B,C))],[nnf_10]) ).
fof(sk_t15_yellow_0,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ related(VAR_0,VAR_2,sK1(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)
| ~ antisymmetric_relstr(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,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0)
| ~ antisymmetric_relstr(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,VAR_2)
| ~ element(VAR_2,the_carrier(VAR_0))
| ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0)
| ~ antisymmetric_relstr(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( related(VAR_0,sK6(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)
| ~ antisymmetric_relstr(VAR_0) )
& ! [VAR_0,VAR_1] :
( relstr_set_smaller(VAR_0,VAR_1,sK6(VAR_0,VAR_1))
| ~ ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0)
| ~ antisymmetric_relstr(VAR_0) )
& ! [VAR_0,VAR_1] :
( element(sK6(VAR_0,VAR_1),the_carrier(VAR_0))
| ~ ex_sup_of_relstr_set(VAR_0,VAR_1)
| ~ rel_str(VAR_0)
| ~ antisymmetric_relstr(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_t15_yellow_0_sk]) ).
cnf(c_23,plain,
( element(sK1(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)
| ~ antisymmetric_relstr(A) ),
inference(split_conjunct,[status(thm)],[sk_t15_yellow_0]) ).
cnf(c_24,plain,
( relstr_set_smaller(A,B,sK1(A,B,C))
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_sup_of_relstr_set(A,B)
| ~ rel_str(A)
| ~ antisymmetric_relstr(A) ),
inference(split_conjunct,[status(thm)],[sk_t15_yellow_0]) ).
cnf(c_25,plain,
( ~ related(A,C,sK1(A,B,C))
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_sup_of_relstr_set(A,B)
| ~ rel_str(A)
| ~ antisymmetric_relstr(A) ),
inference(split_conjunct,[status(thm)],[sk_t15_yellow_0]) ).
fof(nnf_11,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( ( ~ ex_sup_of_relstr_set(A,C)
| join_on_relstr(A,C) != B )
& ! [D] :
( related(A,B,D)
| ~ relstr_set_smaller(A,C,D)
| ~ element(D,the_carrier(A)) )
& relstr_set_smaller(A,C,B) )
| ( ( ? [X0] :
( ~ related(A,B,X0)
& relstr_set_smaller(A,C,X0)
& element(X0,the_carrier(A)) )
| ~ relstr_set_smaller(A,C,B) )
& ex_sup_of_relstr_set(A,C)
& join_on_relstr(A,C) = B ) )
& element(B,the_carrier(A)) )
& rel_str(A)
& antisymmetric_relstr(A) ),
inference(fof_nnf,[status(thm)],[t30_yellow_0_neg]) ).
fof(sk_t30_yellow_0_neg_sk,plain,
( ( ( ( ~ ex_sup_of_relstr_set(sK2,sK4)
| join_on_relstr(sK2,sK4) != sK3 )
& ! [D] :
( related(sK2,sK3,D)
| ~ relstr_set_smaller(sK2,sK4,D)
| ~ element(D,the_carrier(sK2)) )
& relstr_set_smaller(sK2,sK4,sK3) )
| ( ( ( ~ related(sK2,sK3,sK5)
& relstr_set_smaller(sK2,sK4,sK5)
& element(sK5,the_carrier(sK2)) )
| ~ relstr_set_smaller(sK2,sK4,sK3) )
& ex_sup_of_relstr_set(sK2,sK4)
& join_on_relstr(sK2,sK4) = sK3 ) )
& element(sK3,the_carrier(sK2))
& rel_str(sK2)
& antisymmetric_relstr(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5]),skolemize(A,sK2),skolemize(B,sK3),skolemize(C,sK4),skolemize(X0,sK5)],[nnf_11]) ).
fof(sk_t30_yellow_0_neg,plain,
( ( ~ ex_sup_of_relstr_set(sK2,sK4)
| join_on_relstr(sK2,sK4) != sK3
| ~ related(sK2,sK3,sK5)
| ~ relstr_set_smaller(sK2,sK4,sK3) )
& ! [VAR_0] :
( related(sK2,sK3,VAR_0)
| ~ relstr_set_smaller(sK2,sK4,VAR_0)
| ~ element(VAR_0,the_carrier(sK2))
| ~ related(sK2,sK3,sK5)
| ~ relstr_set_smaller(sK2,sK4,sK3) )
& ( ~ ex_sup_of_relstr_set(sK2,sK4)
| join_on_relstr(sK2,sK4) != sK3
| relstr_set_smaller(sK2,sK4,sK5)
| ~ relstr_set_smaller(sK2,sK4,sK3) )
& ! [VAR_0] :
( related(sK2,sK3,VAR_0)
| ~ relstr_set_smaller(sK2,sK4,VAR_0)
| ~ element(VAR_0,the_carrier(sK2))
| relstr_set_smaller(sK2,sK4,sK5)
| ~ relstr_set_smaller(sK2,sK4,sK3) )
& ( ~ ex_sup_of_relstr_set(sK2,sK4)
| join_on_relstr(sK2,sK4) != sK3
| element(sK5,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK4,sK3) )
& ! [VAR_0] :
( related(sK2,sK3,VAR_0)
| ~ relstr_set_smaller(sK2,sK4,VAR_0)
| ~ element(VAR_0,the_carrier(sK2))
| element(sK5,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK4,sK3) )
& ! [VAR_0] :
( related(sK2,sK3,VAR_0)
| ~ relstr_set_smaller(sK2,sK4,VAR_0)
| ~ element(VAR_0,the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,sK4) )
& ( relstr_set_smaller(sK2,sK4,sK3)
| ex_sup_of_relstr_set(sK2,sK4) )
& ! [VAR_0] :
( related(sK2,sK3,VAR_0)
| ~ relstr_set_smaller(sK2,sK4,VAR_0)
| ~ element(VAR_0,the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3 )
& ( relstr_set_smaller(sK2,sK4,sK3)
| join_on_relstr(sK2,sK4) = sK3 )
& element(sK3,the_carrier(sK2))
& rel_str(sK2)
& antisymmetric_relstr(sK2) ),
inference(cnf_transformation,[status(thm)],[sk_t30_yellow_0_neg_sk]) ).
cnf(c_26,negated_conjecture,
rel_str(sK2),
inference(split_conjunct,[status(thm)],[sk_t30_yellow_0_neg]) ).
cnf(c_28,negated_conjecture,
antisymmetric_relstr(sK2),
inference(split_conjunct,[status(thm)],[sk_t30_yellow_0_neg]) ).
cnf(c_29,negated_conjecture,
element(sK3,the_carrier(sK2)),
inference(split_conjunct,[status(thm)],[sk_t30_yellow_0_neg]) ).
cnf(c_30,negated_conjecture,
( relstr_set_smaller(sK2,sK4,sK3)
| join_on_relstr(sK2,sK4) = sK3 ),
inference(split_conjunct,[status(thm)],[sk_t30_yellow_0_neg]) ).
cnf(c_31,negated_conjecture,
( related(sK2,sK3,A)
| ~ relstr_set_smaller(sK2,sK4,A)
| ~ element(A,the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(split_conjunct,[status(thm)],[sk_t30_yellow_0_neg]) ).
cnf(c_32,negated_conjecture,
( relstr_set_smaller(sK2,sK4,sK3)
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(split_conjunct,[status(thm)],[sk_t30_yellow_0_neg]) ).
cnf(c_33,negated_conjecture,
( related(sK2,sK3,A)
| ~ relstr_set_smaller(sK2,sK4,A)
| ~ element(A,the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(split_conjunct,[status(thm)],[sk_t30_yellow_0_neg]) ).
cnf(c_35,negated_conjecture,
( ~ ex_sup_of_relstr_set(sK2,sK4)
| join_on_relstr(sK2,sK4) != sK3
| element(sK5,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK4,sK3) ),
inference(split_conjunct,[status(thm)],[sk_t30_yellow_0_neg]) ).
cnf(c_37,negated_conjecture,
( ~ ex_sup_of_relstr_set(sK2,sK4)
| join_on_relstr(sK2,sK4) != sK3
| relstr_set_smaller(sK2,sK4,sK5)
| ~ relstr_set_smaller(sK2,sK4,sK3) ),
inference(split_conjunct,[status(thm)],[sk_t30_yellow_0_neg]) ).
cnf(c_39,negated_conjecture,
( ~ ex_sup_of_relstr_set(sK2,sK4)
| join_on_relstr(sK2,sK4) != sK3
| ~ related(sK2,sK3,sK5)
| ~ relstr_set_smaller(sK2,sK4,sK3) ),
inference(split_conjunct,[status(thm)],[sk_t30_yellow_0_neg]) ).
cnf(c_52,negated_conjecture,
( ~ related(sK2,B,sK1(sK2,A,B))
| ~ relstr_set_smaller(sK2,A,B)
| ~ element(B,the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,A)
| ~ antisymmetric_relstr(sK2) ),
inference(resolve,[status(thm)],[c_26,c_25]) ).
cnf(c_53,negated_conjecture,
( ~ related(sK2,B,sK1(sK2,A,B))
| ~ relstr_set_smaller(sK2,A,B)
| ~ element(B,the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,A) ),
inference(resolve,[status(thm)],[c_28,c_52]) ).
cnf(c_54,negated_conjecture,
( relstr_set_smaller(sK2,A,sK1(sK2,A,B))
| ~ relstr_set_smaller(sK2,A,B)
| ~ element(B,the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,A)
| ~ antisymmetric_relstr(sK2) ),
inference(resolve,[status(thm)],[c_26,c_24]) ).
cnf(c_55,negated_conjecture,
( relstr_set_smaller(sK2,A,sK1(sK2,A,B))
| ~ relstr_set_smaller(sK2,A,B)
| ~ element(B,the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,A) ),
inference(resolve,[status(thm)],[c_28,c_54]) ).
cnf(c_56,negated_conjecture,
( element(sK1(sK2,A,B),the_carrier(sK2))
| ~ relstr_set_smaller(sK2,A,B)
| ~ element(B,the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,A)
| ~ antisymmetric_relstr(sK2) ),
inference(resolve,[status(thm)],[c_26,c_23]) ).
cnf(c_57,negated_conjecture,
( element(sK1(sK2,A,B),the_carrier(sK2))
| ~ relstr_set_smaller(sK2,A,B)
| ~ element(B,the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,A) ),
inference(resolve,[status(thm)],[c_28,c_56]) ).
cnf(c_64,negated_conjecture,
element(join_on_relstr(sK2,A),the_carrier(sK2)),
inference(resolve,[status(thm)],[c_26,c_14]) ).
cnf(c_65,negated_conjecture,
( ~ related(sK2,A,sK0(sK2,B,A))
| ~ relstr_set_smaller(sK2,B,A)
| join_on_relstr(sK2,B) = A
| ~ ex_sup_of_relstr_set(sK2,B)
| ~ element(A,the_carrier(sK2)) ),
inference(resolve,[status(thm)],[c_26,c_15]) ).
cnf(c_66,negated_conjecture,
( relstr_set_smaller(sK2,B,sK0(sK2,B,A))
| ~ relstr_set_smaller(sK2,B,A)
| join_on_relstr(sK2,B) = A
| ~ ex_sup_of_relstr_set(sK2,B)
| ~ element(A,the_carrier(sK2)) ),
inference(resolve,[status(thm)],[c_26,c_16]) ).
cnf(c_67,negated_conjecture,
( element(sK0(sK2,B,A),the_carrier(sK2))
| ~ relstr_set_smaller(sK2,B,A)
| join_on_relstr(sK2,B) = A
| ~ ex_sup_of_relstr_set(sK2,B)
| ~ element(A,the_carrier(sK2)) ),
inference(resolve,[status(thm)],[c_26,c_17]) ).
cnf(c_68,negated_conjecture,
( related(sK2,A,C)
| ~ relstr_set_smaller(sK2,B,C)
| ~ element(C,the_carrier(sK2))
| join_on_relstr(sK2,B) != A
| ~ ex_sup_of_relstr_set(sK2,B)
| ~ element(A,the_carrier(sK2)) ),
inference(resolve,[status(thm)],[c_26,c_18]) ).
cnf(c_69,negated_conjecture,
( relstr_set_smaller(sK2,B,A)
| join_on_relstr(sK2,B) != A
| ~ ex_sup_of_relstr_set(sK2,B)
| ~ element(A,the_carrier(sK2)) ),
inference(resolve,[status(thm)],[c_26,c_19]) ).
cnf(c_292,negated_conjecture,
( ex_sup_of_relstr_set(sK2,sK4)
| relstr_set_smaller(sK2,sK4,sK1(sK2,sK4,sK3))
| ~ element(sK3,the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_55,c_32]) ).
cnf(c_293,negated_conjecture,
( relstr_set_smaller(sK2,sK4,sK1(sK2,sK4,sK3))
| ~ element(sK3,the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(copy,[status(thm)],[c_292]) ).
cnf(c_77,negated_conjecture,
( relstr_set_smaller(sK2,sK4,sK1(sK2,sK4,sK3))
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_29,c_293]) ).
cnf(c_294,negated_conjecture,
( ex_sup_of_relstr_set(sK2,sK4)
| element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| ~ element(sK3,the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_57,c_32]) ).
cnf(c_295,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| ~ element(sK3,the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(copy,[status(thm)],[c_294]) ).
cnf(c_78,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_29,c_295]) ).
cnf(c_296,negated_conjecture,
( join_on_relstr(sK2,sK4) = sK3
| relstr_set_smaller(sK2,sK4,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3
| ~ ex_sup_of_relstr_set(sK2,sK4)
| ~ element(sK3,the_carrier(sK2)) ),
inference(resolve,[status(thm)],[c_66,c_30]) ).
cnf(c_297,negated_conjecture,
( relstr_set_smaller(sK2,sK4,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3
| ~ ex_sup_of_relstr_set(sK2,sK4)
| ~ element(sK3,the_carrier(sK2)) ),
inference(copy,[status(thm)],[c_296]) ).
cnf(c_80,negated_conjecture,
( relstr_set_smaller(sK2,sK4,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3
| ~ ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_29,c_297]) ).
cnf(c_298,negated_conjecture,
( join_on_relstr(sK2,sK4) = sK3
| element(sK0(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3
| ~ ex_sup_of_relstr_set(sK2,sK4)
| ~ element(sK3,the_carrier(sK2)) ),
inference(resolve,[status(thm)],[c_67,c_30]) ).
cnf(c_299,negated_conjecture,
( element(sK0(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3
| ~ ex_sup_of_relstr_set(sK2,sK4)
| ~ element(sK3,the_carrier(sK2)) ),
inference(copy,[status(thm)],[c_298]) ).
cnf(c_81,negated_conjecture,
( element(sK0(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3
| ~ ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_29,c_299]) ).
cnf(c_300,negated_conjecture,
( related(sK2,sK3,sK1(sK2,sK4,sK3))
| ~ element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,sK4)
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_77,c_33]) ).
cnf(c_87,negated_conjecture,
( related(sK2,sK3,sK1(sK2,sK4,sK3))
| ~ element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(copy,[status(thm)],[c_300]) ).
cnf(c_88,plain,
( relstr_set_smaller(sK2,sK4,A)
| join_on_relstr(sK2,sK4) != A
| ~ element(A,the_carrier(sK2))
| element(sK1(sK2,sK4,sK3),the_carrier(sK2)) ),
inference(resolve,[status(thm)],[c_78,c_69]) ).
cnf(c_301,negated_conjecture,
( element(sK0(sK2,A,sK3),the_carrier(sK2))
| ~ relstr_set_smaller(sK2,A,sK3)
| join_on_relstr(sK2,A) = sK3
| ~ ex_sup_of_relstr_set(sK2,A) ),
inference(resolve,[status(thm)],[c_67,c_29]) ).
cnf(c_302,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| element(sK0(sK2,sK4,sK3),the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK4,sK3)
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_301,c_78]) ).
cnf(c_303,negated_conjecture,
( join_on_relstr(sK2,sK4) = sK3
| element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| element(sK0(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_302,c_30]) ).
cnf(c_93,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| element(sK0(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(copy,[status(thm)],[c_303]) ).
cnf(c_304,negated_conjecture,
( relstr_set_smaller(sK2,A,sK0(sK2,A,sK3))
| ~ relstr_set_smaller(sK2,A,sK3)
| join_on_relstr(sK2,A) = sK3
| ~ ex_sup_of_relstr_set(sK2,A) ),
inference(resolve,[status(thm)],[c_66,c_29]) ).
cnf(c_305,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| relstr_set_smaller(sK2,sK4,sK0(sK2,sK4,sK3))
| ~ relstr_set_smaller(sK2,sK4,sK3)
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_304,c_78]) ).
cnf(c_306,negated_conjecture,
( join_on_relstr(sK2,sK4) = sK3
| element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| relstr_set_smaller(sK2,sK4,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_305,c_30]) ).
cnf(c_94,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| relstr_set_smaller(sK2,sK4,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(copy,[status(thm)],[c_306]) ).
cnf(c_136,plain,
( related(sK2,sK3,sK1(sK2,sK4,sK3))
| ex_sup_of_relstr_set(sK2,sK4)
| element(sK0(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_93,c_87]) ).
cnf(c_148,plain,
( relstr_set_smaller(sK2,sK4,sK3)
| join_on_relstr(sK2,sK4) != sK3
| element(sK1(sK2,sK4,sK3),the_carrier(sK2)) ),
inference(resolve,[status(thm)],[c_88,c_29]) ).
cnf(c_307,negated_conjecture,
( ~ related(sK2,sK3,sK1(sK2,A,sK3))
| ~ relstr_set_smaller(sK2,A,sK3)
| ex_sup_of_relstr_set(sK2,A) ),
inference(resolve,[status(thm)],[c_53,c_29]) ).
cnf(c_308,negated_conjecture,
( ex_sup_of_relstr_set(sK2,sK4)
| ~ related(sK2,sK3,sK1(sK2,sK4,sK3))
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_307,c_32]) ).
cnf(c_309,negated_conjecture,
( ex_sup_of_relstr_set(sK2,sK4)
| element(sK0(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3
| ex_sup_of_relstr_set(sK2,sK4)
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_308,c_136]) ).
cnf(c_310,negated_conjecture,
( ex_sup_of_relstr_set(sK2,sK4)
| element(sK0(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(copy,[status(thm)],[c_309]) ).
cnf(c_151,negated_conjecture,
( element(sK0(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(copy,[status(thm)],[c_310]) ).
cnf(c_311,plain,
( element(sK0(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3
| element(sK0(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_151,c_81]) ).
cnf(c_312,plain,
( element(sK0(sK2,sK4,sK3),the_carrier(sK2))
| element(sK0(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(copy,[status(thm)],[c_311]) ).
cnf(c_154,plain,
( element(sK0(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(copy,[status(thm)],[c_312]) ).
cnf(c_313,negated_conjecture,
( join_on_relstr(sK2,sK4) = sK3
| related(sK2,sK3,sK0(sK2,sK4,sK3))
| ~ relstr_set_smaller(sK2,sK4,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_31,c_154]) ).
cnf(c_314,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3
| join_on_relstr(sK2,sK4) = sK3
| related(sK2,sK3,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_313,c_94]) ).
cnf(c_315,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3
| related(sK2,sK3,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(copy,[status(thm)],[c_314]) ).
cnf(c_161,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| related(sK2,sK3,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(copy,[status(thm)],[c_315]) ).
cnf(c_316,negated_conjecture,
( ~ related(sK2,sK3,sK0(sK2,A,sK3))
| ~ relstr_set_smaller(sK2,A,sK3)
| join_on_relstr(sK2,A) = sK3
| ~ ex_sup_of_relstr_set(sK2,A) ),
inference(resolve,[status(thm)],[c_65,c_29]) ).
cnf(c_317,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| ~ related(sK2,sK3,sK0(sK2,sK4,sK3))
| ~ relstr_set_smaller(sK2,sK4,sK3)
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_316,c_78]) ).
cnf(c_318,negated_conjecture,
( join_on_relstr(sK2,sK4) = sK3
| element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| ~ related(sK2,sK3,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_317,c_30]) ).
cnf(c_319,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3
| join_on_relstr(sK2,sK4) = sK3
| element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_318,c_161]) ).
cnf(c_320,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3
| element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(copy,[status(thm)],[c_319]) ).
cnf(c_321,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(copy,[status(thm)],[c_320]) ).
cnf(c_163,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(copy,[status(thm)],[c_321]) ).
cnf(c_164,plain,
( related(sK2,sK3,sK1(sK2,sK4,sK3))
| ex_sup_of_relstr_set(sK2,sK4)
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_163,c_87]) ).
cnf(c_322,negated_conjecture,
( ~ related(sK2,sK3,sK1(sK2,A,sK3))
| ~ relstr_set_smaller(sK2,A,sK3)
| ex_sup_of_relstr_set(sK2,A) ),
inference(resolve,[status(thm)],[c_53,c_29]) ).
cnf(c_323,negated_conjecture,
( ex_sup_of_relstr_set(sK2,sK4)
| ~ related(sK2,sK3,sK1(sK2,sK4,sK3))
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_322,c_32]) ).
cnf(c_324,negated_conjecture,
( ex_sup_of_relstr_set(sK2,sK4)
| join_on_relstr(sK2,sK4) = sK3
| ex_sup_of_relstr_set(sK2,sK4)
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_323,c_164]) ).
cnf(c_325,negated_conjecture,
( ex_sup_of_relstr_set(sK2,sK4)
| join_on_relstr(sK2,sK4) = sK3
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(copy,[status(thm)],[c_324]) ).
cnf(c_168,negated_conjecture,
( join_on_relstr(sK2,sK4) = sK3
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(copy,[status(thm)],[c_325]) ).
cnf(c_326,plain,
( relstr_set_smaller(sK2,sK4,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_168,c_80]) ).
cnf(c_170,plain,
( relstr_set_smaller(sK2,sK4,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(copy,[status(thm)],[c_326]) ).
cnf(c_327,negated_conjecture,
( join_on_relstr(sK2,sK4) = sK3
| related(sK2,sK3,sK0(sK2,sK4,sK3))
| ~ relstr_set_smaller(sK2,sK4,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_31,c_154]) ).
cnf(c_328,negated_conjecture,
( join_on_relstr(sK2,sK4) = sK3
| join_on_relstr(sK2,sK4) = sK3
| related(sK2,sK3,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_327,c_170]) ).
cnf(c_329,negated_conjecture,
( join_on_relstr(sK2,sK4) = sK3
| related(sK2,sK3,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(copy,[status(thm)],[c_328]) ).
cnf(c_211,negated_conjecture,
( related(sK2,sK3,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(copy,[status(thm)],[c_329]) ).
cnf(c_330,negated_conjecture,
( ~ related(sK2,sK3,sK0(sK2,A,sK3))
| ~ relstr_set_smaller(sK2,A,sK3)
| join_on_relstr(sK2,A) = sK3
| ~ ex_sup_of_relstr_set(sK2,A) ),
inference(resolve,[status(thm)],[c_65,c_29]) ).
cnf(c_331,negated_conjecture,
( join_on_relstr(sK2,sK4) = sK3
| ~ related(sK2,sK3,sK0(sK2,sK4,sK3))
| ~ relstr_set_smaller(sK2,sK4,sK3)
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_330,c_168]) ).
cnf(c_332,negated_conjecture,
( join_on_relstr(sK2,sK4) = sK3
| join_on_relstr(sK2,sK4) = sK3
| ~ related(sK2,sK3,sK0(sK2,sK4,sK3))
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_331,c_30]) ).
cnf(c_333,negated_conjecture,
( join_on_relstr(sK2,sK4) = sK3
| join_on_relstr(sK2,sK4) = sK3
| join_on_relstr(sK2,sK4) = sK3
| join_on_relstr(sK2,sK4) = sK3 ),
inference(resolve,[status(thm)],[c_332,c_211]) ).
cnf(c_334,negated_conjecture,
( join_on_relstr(sK2,sK4) = sK3
| join_on_relstr(sK2,sK4) = sK3
| join_on_relstr(sK2,sK4) = sK3 ),
inference(copy,[status(thm)],[c_333]) ).
cnf(c_335,negated_conjecture,
( join_on_relstr(sK2,sK4) = sK3
| join_on_relstr(sK2,sK4) = sK3 ),
inference(copy,[status(thm)],[c_334]) ).
cnf(c_213,negated_conjecture,
join_on_relstr(sK2,sK4) = sK3,
inference(copy,[status(thm)],[c_335]) ).
cnf(c_336,plain,
( relstr_set_smaller(sK2,sK4,sK3)
| sK3 != sK3
| element(sK1(sK2,sK4,sK3),the_carrier(sK2)) ),
inference(paramod,[status(thm)],[c_213,c_148]) ).
cnf(c_217,plain,
( relstr_set_smaller(sK2,sK4,sK3)
| element(sK1(sK2,sK4,sK3),the_carrier(sK2)) ),
inference(copy,[status(thm)],[c_336]) ).
cnf(c_337,negated_conjecture,
( ~ ex_sup_of_relstr_set(sK2,sK4)
| sK3 != sK3
| ~ related(sK2,sK3,sK5)
| ~ relstr_set_smaller(sK2,sK4,sK3) ),
inference(paramod,[status(thm)],[c_213,c_39]) ).
cnf(c_225,negated_conjecture,
( ~ ex_sup_of_relstr_set(sK2,sK4)
| ~ related(sK2,sK3,sK5)
| ~ relstr_set_smaller(sK2,sK4,sK3) ),
inference(copy,[status(thm)],[c_337]) ).
cnf(c_338,negated_conjecture,
( ~ ex_sup_of_relstr_set(sK2,sK4)
| sK3 != sK3
| relstr_set_smaller(sK2,sK4,sK5)
| ~ relstr_set_smaller(sK2,sK4,sK3) ),
inference(paramod,[status(thm)],[c_213,c_37]) ).
cnf(c_226,negated_conjecture,
( ~ ex_sup_of_relstr_set(sK2,sK4)
| relstr_set_smaller(sK2,sK4,sK5)
| ~ relstr_set_smaller(sK2,sK4,sK3) ),
inference(copy,[status(thm)],[c_338]) ).
cnf(c_339,negated_conjecture,
( ~ ex_sup_of_relstr_set(sK2,sK4)
| sK3 != sK3
| element(sK5,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK4,sK3) ),
inference(paramod,[status(thm)],[c_213,c_35]) ).
cnf(c_227,negated_conjecture,
( ~ ex_sup_of_relstr_set(sK2,sK4)
| element(sK5,the_carrier(sK2))
| ~ relstr_set_smaller(sK2,sK4,sK3) ),
inference(copy,[status(thm)],[c_339]) ).
cnf(c_340,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| ~ ex_sup_of_relstr_set(sK2,sK4)
| relstr_set_smaller(sK2,sK4,sK5) ),
inference(resolve,[status(thm)],[c_226,c_217]) ).
cnf(c_341,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| relstr_set_smaller(sK2,sK4,sK5) ),
inference(resolve,[status(thm)],[c_340,c_78]) ).
cnf(c_231,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| relstr_set_smaller(sK2,sK4,sK5) ),
inference(copy,[status(thm)],[c_341]) ).
cnf(c_342,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| ~ ex_sup_of_relstr_set(sK2,sK4)
| element(sK5,the_carrier(sK2)) ),
inference(resolve,[status(thm)],[c_227,c_217]) ).
cnf(c_343,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| element(sK5,the_carrier(sK2)) ),
inference(resolve,[status(thm)],[c_342,c_78]) ).
cnf(c_235,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| element(sK5,the_carrier(sK2)) ),
inference(copy,[status(thm)],[c_343]) ).
cnf(c_241,plain,
( related(sK2,sK3,sK1(sK2,sK4,sK3))
| ex_sup_of_relstr_set(sK2,sK4)
| element(sK5,the_carrier(sK2)) ),
inference(resolve,[status(thm)],[c_235,c_87]) ).
cnf(c_344,negated_conjecture,
( ~ related(sK2,sK3,sK1(sK2,A,sK3))
| ~ relstr_set_smaller(sK2,A,sK3)
| ex_sup_of_relstr_set(sK2,A) ),
inference(resolve,[status(thm)],[c_53,c_29]) ).
cnf(c_345,negated_conjecture,
( ex_sup_of_relstr_set(sK2,sK4)
| ~ related(sK2,sK3,sK1(sK2,sK4,sK3))
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_344,c_32]) ).
cnf(c_346,negated_conjecture,
( ex_sup_of_relstr_set(sK2,sK4)
| element(sK5,the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,sK4)
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_345,c_241]) ).
cnf(c_347,negated_conjecture,
( ex_sup_of_relstr_set(sK2,sK4)
| element(sK5,the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(copy,[status(thm)],[c_346]) ).
cnf(c_247,negated_conjecture,
( element(sK5,the_carrier(sK2))
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(copy,[status(thm)],[c_347]) ).
cnf(c_348,negated_conjecture,
( relstr_set_smaller(sK2,A,join_on_relstr(sK2,B))
| join_on_relstr(sK2,A) != join_on_relstr(sK2,B)
| ~ ex_sup_of_relstr_set(sK2,A) ),
inference(resolve,[status(thm)],[c_69,c_64]) ).
cnf(c_349,negated_conjecture,
( element(sK5,the_carrier(sK2))
| relstr_set_smaller(sK2,sK4,join_on_relstr(sK2,A))
| join_on_relstr(sK2,sK4) != join_on_relstr(sK2,A) ),
inference(resolve,[status(thm)],[c_348,c_247]) ).
cnf(c_350,plain,
( element(sK5,the_carrier(sK2))
| relstr_set_smaller(sK2,sK4,join_on_relstr(sK2,sK4)) ),
inference(xxres,[status(thm)],[c_349]) ).
cnf(c_250,plain,
( element(sK5,the_carrier(sK2))
| relstr_set_smaller(sK2,sK4,sK3) ),
inference(paramod,[status(thm)],[c_213,c_350]) ).
cnf(c_351,negated_conjecture,
( element(sK5,the_carrier(sK2))
| ~ ex_sup_of_relstr_set(sK2,sK4)
| element(sK5,the_carrier(sK2)) ),
inference(resolve,[status(thm)],[c_227,c_250]) ).
cnf(c_352,negated_conjecture,
( element(sK5,the_carrier(sK2))
| element(sK5,the_carrier(sK2))
| element(sK5,the_carrier(sK2)) ),
inference(resolve,[status(thm)],[c_351,c_247]) ).
cnf(c_353,negated_conjecture,
( element(sK5,the_carrier(sK2))
| element(sK5,the_carrier(sK2)) ),
inference(copy,[status(thm)],[c_352]) ).
cnf(c_256,negated_conjecture,
element(sK5,the_carrier(sK2)),
inference(copy,[status(thm)],[c_353]) ).
cnf(c_354,negated_conjecture,
( related(sK2,join_on_relstr(sK2,B),C)
| ~ relstr_set_smaller(sK2,A,C)
| ~ element(C,the_carrier(sK2))
| join_on_relstr(sK2,A) != join_on_relstr(sK2,B)
| ~ ex_sup_of_relstr_set(sK2,A) ),
inference(resolve,[status(thm)],[c_68,c_64]) ).
cnf(c_355,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| related(sK2,join_on_relstr(sK2,A),B)
| ~ relstr_set_smaller(sK2,sK4,B)
| ~ element(B,the_carrier(sK2))
| join_on_relstr(sK2,sK4) != join_on_relstr(sK2,A) ),
inference(resolve,[status(thm)],[c_354,c_78]) ).
cnf(c_356,plain,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| related(sK2,join_on_relstr(sK2,sK4),A)
| ~ relstr_set_smaller(sK2,sK4,A)
| ~ element(A,the_carrier(sK2)) ),
inference(xxres,[status(thm)],[c_355]) ).
cnf(c_357,plain,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| related(sK2,join_on_relstr(sK2,sK4),sK5)
| ~ relstr_set_smaller(sK2,sK4,sK5) ),
inference(resolve,[status(thm)],[c_356,c_256]) ).
cnf(c_358,plain,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| related(sK2,join_on_relstr(sK2,sK4),sK5) ),
inference(resolve,[status(thm)],[c_357,c_231]) ).
cnf(c_359,plain,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| related(sK2,sK3,sK5) ),
inference(paramod,[status(thm)],[c_213,c_358]) ).
cnf(c_264,plain,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| related(sK2,sK3,sK5) ),
inference(copy,[status(thm)],[c_359]) ).
cnf(c_360,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| ~ ex_sup_of_relstr_set(sK2,sK4)
| ~ related(sK2,sK3,sK5) ),
inference(resolve,[status(thm)],[c_225,c_217]) ).
cnf(c_361,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| ~ ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_360,c_264]) ).
cnf(c_362,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| element(sK1(sK2,sK4,sK3),the_carrier(sK2)) ),
inference(resolve,[status(thm)],[c_361,c_78]) ).
cnf(c_363,negated_conjecture,
( element(sK1(sK2,sK4,sK3),the_carrier(sK2))
| element(sK1(sK2,sK4,sK3),the_carrier(sK2)) ),
inference(copy,[status(thm)],[c_362]) ).
cnf(c_270,negated_conjecture,
element(sK1(sK2,sK4,sK3),the_carrier(sK2)),
inference(copy,[status(thm)],[c_363]) ).
cnf(c_271,negated_conjecture,
( related(sK2,sK3,sK1(sK2,sK4,sK3))
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_270,c_87]) ).
cnf(c_364,negated_conjecture,
( ~ related(sK2,sK3,sK1(sK2,A,sK3))
| ~ relstr_set_smaller(sK2,A,sK3)
| ex_sup_of_relstr_set(sK2,A) ),
inference(resolve,[status(thm)],[c_53,c_29]) ).
cnf(c_365,negated_conjecture,
( ex_sup_of_relstr_set(sK2,sK4)
| ~ related(sK2,sK3,sK1(sK2,sK4,sK3))
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_364,c_32]) ).
cnf(c_366,negated_conjecture,
( ex_sup_of_relstr_set(sK2,sK4)
| ex_sup_of_relstr_set(sK2,sK4)
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(resolve,[status(thm)],[c_365,c_271]) ).
cnf(c_367,negated_conjecture,
( ex_sup_of_relstr_set(sK2,sK4)
| ex_sup_of_relstr_set(sK2,sK4) ),
inference(copy,[status(thm)],[c_366]) ).
cnf(c_275,negated_conjecture,
ex_sup_of_relstr_set(sK2,sK4),
inference(copy,[status(thm)],[c_367]) ).
cnf(c_276,negated_conjecture,
( relstr_set_smaller(sK2,sK4,sK5)
| ~ relstr_set_smaller(sK2,sK4,sK3) ),
inference(resolve,[status(thm)],[c_275,c_226]) ).
cnf(c_277,negated_conjecture,
( ~ related(sK2,sK3,sK5)
| ~ relstr_set_smaller(sK2,sK4,sK3) ),
inference(resolve,[status(thm)],[c_275,c_225]) ).
cnf(c_368,negated_conjecture,
( relstr_set_smaller(sK2,A,join_on_relstr(sK2,B))
| join_on_relstr(sK2,A) != join_on_relstr(sK2,B)
| ~ ex_sup_of_relstr_set(sK2,A) ),
inference(resolve,[status(thm)],[c_69,c_64]) ).
cnf(c_369,negated_conjecture,
( relstr_set_smaller(sK2,sK4,join_on_relstr(sK2,A))
| join_on_relstr(sK2,sK4) != join_on_relstr(sK2,A) ),
inference(resolve,[status(thm)],[c_368,c_275]) ).
cnf(c_370,plain,
relstr_set_smaller(sK2,sK4,join_on_relstr(sK2,sK4)),
inference(xxres,[status(thm)],[c_369]) ).
cnf(c_280,plain,
relstr_set_smaller(sK2,sK4,sK3),
inference(paramod,[status(thm)],[c_213,c_370]) ).
cnf(c_281,negated_conjecture,
~ related(sK2,sK3,sK5),
inference(resolve,[status(thm)],[c_280,c_277]) ).
cnf(c_282,negated_conjecture,
relstr_set_smaller(sK2,sK4,sK5),
inference(resolve,[status(thm)],[c_280,c_276]) ).
cnf(c_371,negated_conjecture,
( related(sK2,join_on_relstr(sK2,B),C)
| ~ relstr_set_smaller(sK2,A,C)
| ~ element(C,the_carrier(sK2))
| join_on_relstr(sK2,A) != join_on_relstr(sK2,B)
| ~ ex_sup_of_relstr_set(sK2,A) ),
inference(resolve,[status(thm)],[c_68,c_64]) ).
cnf(c_372,negated_conjecture,
( related(sK2,join_on_relstr(sK2,A),B)
| ~ relstr_set_smaller(sK2,sK4,B)
| ~ element(B,the_carrier(sK2))
| join_on_relstr(sK2,sK4) != join_on_relstr(sK2,A) ),
inference(resolve,[status(thm)],[c_371,c_275]) ).
cnf(c_373,plain,
( related(sK2,join_on_relstr(sK2,sK4),A)
| ~ relstr_set_smaller(sK2,sK4,A)
| ~ element(A,the_carrier(sK2)) ),
inference(xxres,[status(thm)],[c_372]) ).
cnf(c_374,plain,
( related(sK2,join_on_relstr(sK2,sK4),sK5)
| ~ relstr_set_smaller(sK2,sK4,sK5) ),
inference(resolve,[status(thm)],[c_373,c_256]) ).
cnf(c_375,negated_conjecture,
related(sK2,join_on_relstr(sK2,sK4),sK5),
inference(resolve,[status(thm)],[c_374,c_282]) ).
cnf(c_376,negated_conjecture,
related(sK2,sK3,sK5),
inference(paramod,[status(thm)],[c_213,c_375]) ).
cnf(c_291,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_281,c_376]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU359+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n010.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Sat Sep 26 09:19:05 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/5.38 % Process 2991636 was started by sandbox2 on n010,
% 0.09/5.38 % Sat Sep 26 09:19:05 2026
% 0.09/5.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/5.38
% 0.09/5.38 % From the command line: assign(max_seconds, 300).
% 0.15/5.45
% 0.15/5.45 % SZS status Theorem for theBenchmark
% 0.15/5.45
% 0.15/5.45 % Proof 1 at 0.04 (+ 0.01) seconds.
% 0.15/5.45 % Length of proof is 74.
% 0.15/5.45 % Level of proof is 28.
% 0.15/5.45 % Maximum clause weight is 34.000.
% 0.15/5.45 % Given clauses 117.
% 0.15/5.45
% 0.15/5.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------