%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU356+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.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 : Fri Sep 25 02:51:49 PM UTC 2026
% Result : Theorem 4.61s 1.12s
% Output : Proof 4.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 71
% Number of leaves : 3
% Syntax : Number of formulae : 185 ( 10 unt; 0 def)
% Number of atoms : 837 ( 88 equ)
% Maximal formula atoms : 25 ( 4 avg)
% Number of connectives : 951 ( 299 ~; 582 |; 50 &)
% ( 3 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 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 : 160 ( 0 sgn 35 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f0,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('/export/starexec/sandbox/benchmark/theBenchmark.p',d7_yellow_0) ).
fof(f0_nnf,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)) )
| ? [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) )
& ( ? [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)) )
& ! [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) ) )
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B,D,C,E] :
( ( ( ( sk3(A,B,C) != C
& ( related(A,sk3(A,B,C),E)
| ~ relstr_set_smaller(A,B,E)
| ~ element(E,the_carrier(A)) )
& relstr_set_smaller(A,B,sk3(A,B,C))
& element(sk3(A,B,C),the_carrier(A)) )
| ( ~ related(A,C,sk2(A,B,C))
& relstr_set_smaller(A,B,sk2(A,B,C))
& element(sk2(A,B,C),the_carrier(A)) )
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_sup_of_relstr_set(A,B) )
& ( ( ( D = sk0(A,B)
| ( ~ related(A,D,sk1(A,B,D))
& relstr_set_smaller(A,B,sk1(A,B,D))
& element(sk1(A,B,D),the_carrier(A)) )
| ~ relstr_set_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& ( related(A,sk0(A,B),D)
| ~ relstr_set_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_set_smaller(A,B,sk0(A,B))
& element(sk0(A,B),the_carrier(A)) )
| ~ ex_sup_of_relstr_set(A,B) ) )
| ~ rel_str(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3])],[f0_nnf]) ).
cnf(c16,plain,
( related(X0,sk3(X0,X1,X2),X4)
| ~ relstr_set_smaller(X0,X1,X4)
| ~ element(X4,the_carrier(X0))
| ~ related(X0,X2,sk2(X0,X1,X2))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
fof(f8,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('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_yellow_0) ).
fof(f8_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(negated_conjecture,[status(cth)],[f8]) ).
fof(f8_nnf,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) )
| ( ! [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) ) )
& rel_str(A)
& antisymmetric_relstr(A) ),
inference(nnf_transformation,[status(thm)],[f8_neg]) ).
fof(f8_sk,plain,
! [C,D] :
( ( ( ( related(sk7,sk10,D)
| ~ relstr_set_smaller(sk7,sk8,D)
| ~ element(D,the_carrier(sk7)) )
& relstr_set_smaller(sk7,sk8,sk10)
& element(sk10,the_carrier(sk7))
& ~ ex_sup_of_relstr_set(sk7,sk8) )
| ( ( ( ~ related(sk7,C,sk9(C))
& relstr_set_smaller(sk7,sk8,sk9(C))
& element(sk9(C),the_carrier(sk7)) )
| ~ relstr_set_smaller(sk7,sk8,C)
| ~ element(C,the_carrier(sk7)) )
& ex_sup_of_relstr_set(sk7,sk8) ) )
& rel_str(sk7)
& antisymmetric_relstr(sk7) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk7,sk8,sk9,sk10])],[f8_nnf]) ).
cnf(c26,plain,
rel_str(sk7),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p138,plain,
( related(sk7,sk3(sk7,X0,X1),X2)
| ~ relstr_set_smaller(sk7,X0,X2)
| ~ element(X2,the_carrier(sk7))
| ~ related(sk7,X1,sk2(sk7,X0,X1))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c16,c26]) ).
cnf(p374,plain,
( related(sk7,sk3(sk7,X0,X1),X1)
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ related(sk7,X1,sk2(sk7,X0,X1))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(factoring,[status(thm)],[p138]) ).
cnf(p383,plain,
( related(sk7,sk3(sk7,X0,X1),X1)
| ~ related(sk7,X1,sk2(sk7,X0,X1))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(factoring,[status(thm)],[p374]) ).
cnf(c28,plain,
( element(sk10,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p387,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| related(sk7,sk3(sk7,X0,sk10),sk10)
| ~ related(sk7,sk10,sk2(sk7,X0,sk10))
| ~ relstr_set_smaller(sk7,X0,sk10)
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p383,c28]) ).
cnf(p392,plain,
( related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ related(sk7,sk10,sk2(sk7,sk8,sk10))
| ~ relstr_set_smaller(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p387]) ).
cnf(c29,plain,
( relstr_set_smaller(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p394,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ related(sk7,sk10,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p392,c29]) ).
cnf(p395,plain,
( related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ related(sk7,sk10,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p394]) ).
fof(f9,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('/export/starexec/sandbox/benchmark/theBenchmark.p',t25_orders_2) ).
fof(f9_nnf,plain,
! [A] :
( ! [B] :
( ! [C] :
( B = C
| ~ 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(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A,B,C] :
( B = C
| ~ 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(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c43,plain,
( X1 = X2
| ~ related(X0,X2,X1)
| ~ related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0)
| ~ antisymmetric_relstr(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(c25,plain,
antisymmetric_relstr(sk7),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p179,plain,
( X0 = X1
| ~ related(sk7,X1,X0)
| ~ related(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ~ element(X0,the_carrier(sk7))
| ~ rel_str(sk7) ),
inference(resolution,[status(thm)],[c43,c25]) ).
cnf(p181,plain,
( X0 = X1
| ~ related(sk7,X1,X0)
| ~ related(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ~ element(X0,the_carrier(sk7)) ),
inference(resolution,[status(thm)],[p179,c26]) ).
cnf(p182,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| sk10 = X0
| ~ related(sk7,X0,sk10)
| ~ related(sk7,sk10,X0)
| ~ element(X0,the_carrier(sk7)) ),
inference(resolution,[status(thm)],[p181,c28]) ).
cnf(c6,plain,
( element(sk3(X0,X1,X2),the_carrier(X0))
| element(sk2(X0,X1,X2),the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p78,plain,
( element(sk3(sk7,X0,X1),the_carrier(sk7))
| element(sk2(sk7,X0,X1),the_carrier(sk7))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c26,c6]) ).
cnf(p98,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| element(sk3(sk7,X0,sk10),the_carrier(sk7))
| element(sk2(sk7,X0,sk10),the_carrier(sk7))
| ~ relstr_set_smaller(sk7,X0,sk10)
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p78,c28]) ).
cnf(p103,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ~ relstr_set_smaller(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p98]) ).
cnf(p105,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p103,c29]) ).
cnf(p106,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p105]) ).
cnf(p185,plain,
( element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ related(sk7,sk10,sk3(sk7,sk8,sk10)) ),
inference(resolution,[status(thm)],[p182,p106]) ).
cnf(p229,plain,
( element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ related(sk7,sk10,sk3(sk7,sk8,sk10)) ),
inference(factoring,[status(thm)],[p185]) ).
cnf(c30,plain,
( related(sk7,sk10,X3)
| ~ relstr_set_smaller(sk7,sk8,X3)
| ~ element(X3,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p107,plain,
( related(sk7,sk10,sk3(sk7,sk8,sk10))
| ~ relstr_set_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p106,c30]) ).
cnf(p205,plain,
( related(sk7,sk10,sk3(sk7,sk8,sk10))
| ~ relstr_set_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p107]) ).
cnf(c7,plain,
( relstr_set_smaller(X0,X1,sk3(X0,X1,X2))
| element(sk2(X0,X1,X2),the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p79,plain,
( relstr_set_smaller(sk7,X0,sk3(sk7,X0,X1))
| element(sk2(sk7,X0,X1),the_carrier(sk7))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c26,c7]) ).
cnf(p123,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| relstr_set_smaller(sk7,X0,sk3(sk7,X0,sk10))
| element(sk2(sk7,X0,sk10),the_carrier(sk7))
| ~ relstr_set_smaller(sk7,X0,sk10)
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p79,c28]) ).
cnf(p125,plain,
( relstr_set_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ~ relstr_set_smaller(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p123]) ).
cnf(p127,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| relstr_set_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p125,c29]) ).
cnf(p130,plain,
( relstr_set_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p127]) ).
cnf(p206,plain,
( element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| related(sk7,sk10,sk3(sk7,sk8,sk10))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p205,p130]) ).
cnf(p210,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| related(sk7,sk10,sk3(sk7,sk8,sk10))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p206]) ).
cnf(p211,plain,
( related(sk7,sk10,sk3(sk7,sk8,sk10))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p210]) ).
cnf(p231,plain,
( element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10) ),
inference(resolution,[status(thm)],[p229,p211]) ).
cnf(p240,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10) ),
inference(factoring,[status(thm)],[p231]) ).
cnf(p241,plain,
( element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10) ),
inference(factoring,[status(thm)],[p240]) ).
cnf(c8,plain,
( related(X0,sk3(X0,X1,X2),X4)
| ~ relstr_set_smaller(X0,X1,X4)
| ~ element(X4,the_carrier(X0))
| element(sk2(X0,X1,X2),the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p83,plain,
( related(sk7,sk3(sk7,X0,X1),X2)
| ~ relstr_set_smaller(sk7,X0,X2)
| ~ element(X2,the_carrier(sk7))
| element(sk2(sk7,X0,X1),the_carrier(sk7))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c8,c26]) ).
cnf(p215,plain,
( related(sk7,sk3(sk7,X0,X1),X1)
| ~ relstr_set_smaller(sk7,X0,X1)
| element(sk2(sk7,X0,X1),the_carrier(sk7))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(factoring,[status(thm)],[p83]) ).
cnf(p220,plain,
( related(sk7,sk3(sk7,X0,X1),X1)
| element(sk2(sk7,X0,X1),the_carrier(sk7))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(factoring,[status(thm)],[p215]) ).
cnf(p221,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| related(sk7,sk3(sk7,X0,sk10),sk10)
| element(sk2(sk7,X0,sk10),the_carrier(sk7))
| ~ relstr_set_smaller(sk7,X0,sk10)
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p220,c28]) ).
cnf(p224,plain,
( related(sk7,sk3(sk7,sk8,sk10),sk10)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ~ relstr_set_smaller(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p221]) ).
cnf(p226,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| related(sk7,sk3(sk7,sk8,sk10),sk10)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p224,c29]) ).
cnf(p228,plain,
( related(sk7,sk3(sk7,sk8,sk10),sk10)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p226]) ).
cnf(p243,plain,
( element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(resolution,[status(thm)],[p241,p228]) ).
cnf(p245,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p243]) ).
cnf(p246,plain,
( element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p245]) ).
cnf(p247,plain,
( related(sk7,sk10,sk2(sk7,sk8,sk10))
| ~ relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(resolution,[status(thm)],[p246,c30]) ).
cnf(p268,plain,
( related(sk7,sk10,sk2(sk7,sk8,sk10))
| ~ relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p247]) ).
cnf(c10,plain,
( element(sk3(X0,X1,X2),the_carrier(X0))
| relstr_set_smaller(X0,X1,sk2(X0,X1,X2))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p90,plain,
( element(sk3(sk7,X0,X1),the_carrier(sk7))
| relstr_set_smaller(sk7,X0,sk2(sk7,X0,X1))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c10,c26]) ).
cnf(p131,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| element(sk3(sk7,X0,sk10),the_carrier(sk7))
| relstr_set_smaller(sk7,X0,sk2(sk7,X0,sk10))
| ~ relstr_set_smaller(sk7,X0,sk10)
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p90,c28]) ).
cnf(p133,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ~ relstr_set_smaller(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p131]) ).
cnf(p139,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p133,c29]) ).
cnf(p140,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p139]) ).
cnf(p269,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| related(sk7,sk10,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(resolution,[status(thm)],[p268,p140]) ).
cnf(p270,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| related(sk7,sk10,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p269]) ).
cnf(c14,plain,
( element(sk3(X0,X1,X2),the_carrier(X0))
| ~ related(X0,X2,sk2(X0,X1,X2))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p122,plain,
( element(sk3(sk7,X0,X1),the_carrier(sk7))
| ~ related(sk7,X1,sk2(sk7,X0,X1))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c14,c26]) ).
cnf(p189,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| element(sk3(sk7,X0,sk10),the_carrier(sk7))
| ~ related(sk7,sk10,sk2(sk7,X0,sk10))
| ~ relstr_set_smaller(sk7,X0,sk10)
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p122,c28]) ).
cnf(p192,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| ~ related(sk7,sk10,sk2(sk7,sk8,sk10))
| ~ relstr_set_smaller(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p189]) ).
cnf(p194,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| ~ related(sk7,sk10,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p192,c29]) ).
cnf(p195,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| ~ related(sk7,sk10,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p194]) ).
cnf(p272,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(resolution,[status(thm)],[p270,p195]) ).
cnf(p282,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p272]) ).
cnf(p283,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p282]) ).
cnf(p299,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ related(sk7,sk10,sk3(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(resolution,[status(thm)],[p283,p182]) ).
cnf(p330,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ related(sk7,sk10,sk3(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p299]) ).
cnf(p332,plain,
( ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ related(sk7,sk10,sk3(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p330]) ).
cnf(p287,plain,
( related(sk7,sk10,sk3(sk7,sk8,sk10))
| ~ relstr_set_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(resolution,[status(thm)],[p283,c30]) ).
cnf(p306,plain,
( related(sk7,sk10,sk3(sk7,sk8,sk10))
| ~ relstr_set_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p287]) ).
cnf(c11,plain,
( relstr_set_smaller(X0,X1,sk3(X0,X1,X2))
| relstr_set_smaller(X0,X1,sk2(X0,X1,X2))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p95,plain,
( relstr_set_smaller(sk7,X0,sk3(sk7,X0,X1))
| relstr_set_smaller(sk7,X0,sk2(sk7,X0,X1))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c11,c26]) ).
cnf(p141,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| relstr_set_smaller(sk7,X0,sk3(sk7,X0,sk10))
| relstr_set_smaller(sk7,X0,sk2(sk7,X0,sk10))
| ~ relstr_set_smaller(sk7,X0,sk10)
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p95,c28]) ).
cnf(p145,plain,
( relstr_set_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ~ relstr_set_smaller(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p141]) ).
cnf(p147,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| relstr_set_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p145,c29]) ).
cnf(p148,plain,
( relstr_set_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p147]) ).
cnf(p307,plain,
( relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| related(sk7,sk10,sk3(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(resolution,[status(thm)],[p306,p148]) ).
cnf(p308,plain,
( relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| related(sk7,sk10,sk3(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p307]) ).
cnf(p333,plain,
( relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(resolution,[status(thm)],[p332,p308]) ).
cnf(p334,plain,
( relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p333]) ).
cnf(p339,plain,
( relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p334]) ).
cnf(c12,plain,
( related(X0,sk3(X0,X1,X2),X4)
| ~ relstr_set_smaller(X0,X1,X4)
| ~ element(X4,the_carrier(X0))
| relstr_set_smaller(X0,X1,sk2(X0,X1,X2))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p102,plain,
( related(sk7,sk3(sk7,X0,X1),X2)
| ~ relstr_set_smaller(sk7,X0,X2)
| ~ element(X2,the_carrier(sk7))
| relstr_set_smaller(sk7,X0,sk2(sk7,X0,X1))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c12,c26]) ).
cnf(p274,plain,
( related(sk7,sk3(sk7,X0,X1),X1)
| ~ relstr_set_smaller(sk7,X0,X1)
| relstr_set_smaller(sk7,X0,sk2(sk7,X0,X1))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(factoring,[status(thm)],[p102]) ).
cnf(p312,plain,
( related(sk7,sk3(sk7,X0,X1),X1)
| relstr_set_smaller(sk7,X0,sk2(sk7,X0,X1))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(factoring,[status(thm)],[p274]) ).
cnf(p313,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| related(sk7,sk3(sk7,X0,sk10),sk10)
| relstr_set_smaller(sk7,X0,sk2(sk7,X0,sk10))
| ~ relstr_set_smaller(sk7,X0,sk10)
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p312,c28]) ).
cnf(p318,plain,
( related(sk7,sk3(sk7,sk8,sk10),sk10)
| relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ~ relstr_set_smaller(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p313]) ).
cnf(p321,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| related(sk7,sk3(sk7,sk8,sk10),sk10)
| relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p318,c29]) ).
cnf(p322,plain,
( related(sk7,sk3(sk7,sk8,sk10),sk10)
| relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p321]) ).
cnf(p340,plain,
( relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(resolution,[status(thm)],[p339,p322]) ).
cnf(p342,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p340]) ).
cnf(p343,plain,
( relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p342]) ).
cnf(p345,plain,
( related(sk7,sk10,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(resolution,[status(thm)],[p343,p268]) ).
cnf(p346,plain,
( related(sk7,sk10,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p345]) ).
cnf(p348,plain,
( related(sk7,sk10,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p346]) ).
cnf(p397,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| related(sk7,sk3(sk7,sk8,sk10),sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p395,p348]) ).
cnf(p398,plain,
( sk10 = sk3(sk7,sk8,sk10)
| related(sk7,sk3(sk7,sk8,sk10),sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p397]) ).
cnf(c15,plain,
( relstr_set_smaller(X0,X1,sk3(X0,X1,X2))
| ~ related(X0,X2,sk2(X0,X1,X2))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p129,plain,
( relstr_set_smaller(sk7,X0,sk3(sk7,X0,X1))
| ~ related(sk7,X1,sk2(sk7,X0,X1))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c15,c26]) ).
cnf(p196,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| relstr_set_smaller(sk7,X0,sk3(sk7,X0,sk10))
| ~ related(sk7,sk10,sk2(sk7,X0,sk10))
| ~ relstr_set_smaller(sk7,X0,sk10)
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p129,c28]) ).
cnf(p199,plain,
( relstr_set_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| ~ related(sk7,sk10,sk2(sk7,sk8,sk10))
| ~ relstr_set_smaller(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p196]) ).
cnf(p201,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| relstr_set_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| ~ related(sk7,sk10,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p199,c29]) ).
cnf(p202,plain,
( relstr_set_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| ~ related(sk7,sk10,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p201]) ).
cnf(p350,plain,
( relstr_set_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(resolution,[status(thm)],[p348,p202]) ).
cnf(p358,plain,
( relstr_set_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p350]) ).
cnf(p359,plain,
( related(sk7,sk10,sk3(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(resolution,[status(thm)],[p358,p306]) ).
cnf(p361,plain,
( related(sk7,sk10,sk3(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p359]) ).
cnf(p363,plain,
( related(sk7,sk10,sk3(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p361]) ).
cnf(p364,plain,
( ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(resolution,[status(thm)],[p363,p332]) ).
cnf(p365,plain,
( ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ex_sup_of_relstr_set(sk7,sk8)
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p364]) ).
cnf(p370,plain,
( ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10) ),
inference(factoring,[status(thm)],[p365]) ).
cnf(p399,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| sk10 = sk3(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p398,p370]) ).
cnf(p401,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p399]) ).
cnf(p402,plain,
( sk10 = sk3(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p401]) ).
cnf(c9,plain,
( sk3(X0,X1,X2) != X2
| element(sk2(X0,X1,X2),the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p87,plain,
( sk3(sk7,X0,X1) != X1
| element(sk2(sk7,X0,X1),the_carrier(sk7))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c9,c26]) ).
cnf(p91,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| sk3(sk7,X0,sk10) != sk10
| element(sk2(sk7,X0,sk10),the_carrier(sk7))
| ~ relstr_set_smaller(sk7,X0,sk10)
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p87,c28]) ).
cnf(p92,plain,
( sk3(sk7,sk8,sk10) != sk10
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ~ relstr_set_smaller(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p91]) ).
cnf(p96,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| sk3(sk7,sk8,sk10) != sk10
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p92,c29]) ).
cnf(p97,plain,
( sk3(sk7,sk8,sk10) != sk10
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p96]) ).
cnf(p403,plain,
( sk10 != sk10
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(superposition,[status(thm)],[p402,p97]) ).
cnf(p411,plain,
( sk10 != sk10
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p403]) ).
cnf(p412,plain,
( element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(equality_resolution,[status(thm)],[p411]) ).
cnf(p413,plain,
( related(sk7,sk10,sk2(sk7,sk8,sk10))
| ~ relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p412,c30]) ).
cnf(p437,plain,
( related(sk7,sk10,sk2(sk7,sk8,sk10))
| ~ relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p413]) ).
cnf(c13,plain,
( sk3(X0,X1,X2) != X2
| relstr_set_smaller(X0,X1,sk2(X0,X1,X2))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p114,plain,
( sk3(sk7,X0,X1) != X1
| relstr_set_smaller(sk7,X0,sk2(sk7,X0,X1))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c13,c26]) ).
cnf(p115,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| sk3(sk7,X0,sk10) != sk10
| relstr_set_smaller(sk7,X0,sk2(sk7,X0,sk10))
| ~ relstr_set_smaller(sk7,X0,sk10)
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p114,c28]) ).
cnf(p117,plain,
( sk3(sk7,sk8,sk10) != sk10
| relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ~ relstr_set_smaller(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p115]) ).
cnf(p119,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| sk3(sk7,sk8,sk10) != sk10
| relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p117,c29]) ).
cnf(p120,plain,
( sk3(sk7,sk8,sk10) != sk10
| relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p119]) ).
cnf(p404,plain,
( sk10 != sk10
| relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(superposition,[status(thm)],[p402,p120]) ).
cnf(p435,plain,
( sk10 != sk10
| relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p404]) ).
cnf(p436,plain,
( relstr_set_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(equality_resolution,[status(thm)],[p435]) ).
cnf(p438,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| related(sk7,sk10,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p437,p436]) ).
cnf(p439,plain,
( related(sk7,sk10,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p438]) ).
cnf(c17,plain,
( sk3(X0,X1,X2) != X2
| ~ related(X0,X2,sk2(X0,X1,X2))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p144,plain,
( sk3(sk7,X0,X1) != X1
| ~ related(sk7,X1,sk2(sk7,X0,X1))
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c17,c26]) ).
cnf(p151,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| sk3(sk7,X0,sk10) != sk10
| ~ related(sk7,sk10,sk2(sk7,X0,sk10))
| ~ relstr_set_smaller(sk7,X0,sk10)
| ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p144,c28]) ).
cnf(p153,plain,
( sk3(sk7,sk8,sk10) != sk10
| ~ related(sk7,sk10,sk2(sk7,sk8,sk10))
| ~ relstr_set_smaller(sk7,sk8,sk10)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p151]) ).
cnf(p155,plain,
( ex_sup_of_relstr_set(sk7,sk8)
| sk3(sk7,sk8,sk10) != sk10
| ~ related(sk7,sk10,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p153,c29]) ).
cnf(p180,plain,
( sk3(sk7,sk8,sk10) != sk10
| ~ related(sk7,sk10,sk2(sk7,sk8,sk10))
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p155]) ).
cnf(p440,plain,
( sk3(sk7,sk8,sk10) != sk10
| ex_sup_of_relstr_set(sk7,sk8)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p439,p180]) ).
cnf(p445,plain,
( sk3(sk7,sk8,sk10) != sk10
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p440]) ).
cnf(p446,plain,
( sk10 != sk10
| ex_sup_of_relstr_set(sk7,sk8)
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(superposition,[status(thm)],[p402,p445]) ).
cnf(p447,plain,
( sk10 != sk10
| ex_sup_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p446]) ).
cnf(p448,plain,
ex_sup_of_relstr_set(sk7,sk8),
inference(equality_resolution,[status(thm)],[p447]) ).
cnf(c0,plain,
( element(sk0(X0,X1),the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p72,plain,
( element(sk0(sk7,X0),the_carrier(sk7))
| ~ ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c26,c0]) ).
cnf(p449,plain,
element(sk0(sk7,sk8),the_carrier(sk7)),
inference(resolution,[status(thm)],[p448,p72]) ).
cnf(c39,plain,
( ~ ex_sup_of_relstr_set(sk7,sk8)
| ~ related(sk7,X2,sk9(X2))
| ~ relstr_set_smaller(sk7,sk8,X2)
| ~ element(X2,the_carrier(sk7)) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p457,plain,
( ~ ex_sup_of_relstr_set(sk7,sk8)
| ~ related(sk7,sk0(sk7,sk8),sk9(sk0(sk7,sk8)))
| ~ relstr_set_smaller(sk7,sk8,sk0(sk7,sk8)) ),
inference(resolution,[status(thm)],[p449,c39]) ).
cnf(c1,plain,
( relstr_set_smaller(X0,X1,sk0(X0,X1))
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p73,plain,
( relstr_set_smaller(sk7,X0,sk0(sk7,X0))
| ~ ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c26,c1]) ).
cnf(p450,plain,
relstr_set_smaller(sk7,sk8,sk0(sk7,sk8)),
inference(resolution,[status(thm)],[p448,p73]) ).
cnf(p528,plain,
( ~ ex_sup_of_relstr_set(sk7,sk8)
| ~ related(sk7,sk0(sk7,sk8),sk9(sk0(sk7,sk8))) ),
inference(resolution,[status(thm)],[p457,p450]) ).
cnf(c31,plain,
( ~ ex_sup_of_relstr_set(sk7,sk8)
| element(sk9(X2),the_carrier(sk7))
| ~ relstr_set_smaller(sk7,sk8,X2)
| ~ element(X2,the_carrier(sk7)) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p456,plain,
( ~ ex_sup_of_relstr_set(sk7,sk8)
| element(sk9(sk0(sk7,sk8)),the_carrier(sk7))
| ~ relstr_set_smaller(sk7,sk8,sk0(sk7,sk8)) ),
inference(resolution,[status(thm)],[p449,c31]) ).
cnf(p492,plain,
( ~ ex_sup_of_relstr_set(sk7,sk8)
| element(sk9(sk0(sk7,sk8)),the_carrier(sk7)) ),
inference(resolution,[status(thm)],[p456,p450]) ).
cnf(p493,plain,
element(sk9(sk0(sk7,sk8)),the_carrier(sk7)),
inference(resolution,[status(thm)],[p492,p448]) ).
cnf(c2,plain,
( related(X0,sk0(X0,X1),X3)
| ~ relstr_set_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p74,plain,
( related(sk7,sk0(sk7,X0),X1)
| ~ relstr_set_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ~ ex_sup_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c26,c2]) ).
cnf(p451,plain,
( related(sk7,sk0(sk7,sk8),X0)
| ~ relstr_set_smaller(sk7,sk8,X0)
| ~ element(X0,the_carrier(sk7)) ),
inference(resolution,[status(thm)],[p448,p74]) ).
cnf(p526,plain,
( related(sk7,sk0(sk7,sk8),sk9(sk0(sk7,sk8)))
| ~ relstr_set_smaller(sk7,sk8,sk9(sk0(sk7,sk8))) ),
inference(resolution,[status(thm)],[p493,p451]) ).
cnf(c35,plain,
( ~ ex_sup_of_relstr_set(sk7,sk8)
| relstr_set_smaller(sk7,sk8,sk9(X2))
| ~ relstr_set_smaller(sk7,sk8,X2)
| ~ element(X2,the_carrier(sk7)) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p455,plain,
( ~ ex_sup_of_relstr_set(sk7,sk8)
| relstr_set_smaller(sk7,sk8,sk9(sk0(sk7,sk8)))
| ~ relstr_set_smaller(sk7,sk8,sk0(sk7,sk8)) ),
inference(resolution,[status(thm)],[p449,c35]) ).
cnf(p490,plain,
( ~ ex_sup_of_relstr_set(sk7,sk8)
| relstr_set_smaller(sk7,sk8,sk9(sk0(sk7,sk8))) ),
inference(resolution,[status(thm)],[p455,p450]) ).
cnf(p491,plain,
relstr_set_smaller(sk7,sk8,sk9(sk0(sk7,sk8))),
inference(resolution,[status(thm)],[p490,p448]) ).
cnf(p527,plain,
related(sk7,sk0(sk7,sk8),sk9(sk0(sk7,sk8))),
inference(resolution,[status(thm)],[p526,p491]) ).
cnf(p529,plain,
~ ex_sup_of_relstr_set(sk7,sk8),
inference(resolution,[status(thm)],[p528,p527]) ).
cnf(p530,plain,
$false,
inference(resolution,[status(thm)],[p529,p448]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU356+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n002.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 13:52:04 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 4.61/1.12 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.61/1.12 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------