%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU357+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 : n006.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.52s 1.12s
% Output : Proof 4.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 3
% Syntax : Number of formulae : 185 ( 10 unt; 0 def)
% Number of atoms : 837 ( 89 equ)
% Maximal formula atoms : 25 ( 4 avg)
% Number of connectives : 950 ( 298 ~; 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 : 163 ( 0 sgn 35 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f0,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( ex_inf_of_relstr_set(A,B)
<=> ? [C] :
( ! [D] :
( element(D,the_carrier(A))
=> ( ( ! [E] :
( element(E,the_carrier(A))
=> ( relstr_element_smaller(A,B,E)
=> related(A,E,D) ) )
& relstr_element_smaller(A,B,D) )
=> D = C ) )
& ! [D] :
( element(D,the_carrier(A))
=> ( relstr_element_smaller(A,B,D)
=> related(A,D,C) ) )
& relstr_element_smaller(A,B,C)
& element(C,the_carrier(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_yellow_0) ).
fof(f0_nnf,plain,
! [A] :
( ! [B] :
( ( ! [C] :
( ? [D] :
( D != C
& ! [E] :
( related(A,E,D)
| ~ relstr_element_smaller(A,B,E)
| ~ element(E,the_carrier(A)) )
& relstr_element_smaller(A,B,D)
& element(D,the_carrier(A)) )
| ? [D] :
( ~ related(A,D,C)
& relstr_element_smaller(A,B,D)
& element(D,the_carrier(A)) )
| ~ relstr_element_smaller(A,B,C)
| ~ element(C,the_carrier(A)) )
| ex_inf_of_relstr_set(A,B) )
& ( ? [C] :
( ! [D] :
( D = C
| ? [E] :
( ~ related(A,E,D)
& relstr_element_smaller(A,B,E)
& element(E,the_carrier(A)) )
| ~ relstr_element_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& ! [D] :
( related(A,D,C)
| ~ relstr_element_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_element_smaller(A,B,C)
& element(C,the_carrier(A)) )
| ~ ex_inf_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,E,sk3(A,B,C))
| ~ relstr_element_smaller(A,B,E)
| ~ element(E,the_carrier(A)) )
& relstr_element_smaller(A,B,sk3(A,B,C))
& element(sk3(A,B,C),the_carrier(A)) )
| ( ~ related(A,sk2(A,B,C),C)
& relstr_element_smaller(A,B,sk2(A,B,C))
& element(sk2(A,B,C),the_carrier(A)) )
| ~ relstr_element_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_inf_of_relstr_set(A,B) )
& ( ( ( D = sk0(A,B)
| ( ~ related(A,sk1(A,B,D),D)
& relstr_element_smaller(A,B,sk1(A,B,D))
& element(sk1(A,B,D),the_carrier(A)) )
| ~ relstr_element_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& ( related(A,D,sk0(A,B))
| ~ relstr_element_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_element_smaller(A,B,sk0(A,B))
& element(sk0(A,B),the_carrier(A)) )
| ~ ex_inf_of_relstr_set(A,B) ) )
| ~ rel_str(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3])],[f0_nnf]) ).
cnf(c6,plain,
( element(sk3(X0,X1,X2),the_carrier(X0))
| element(sk2(X0,X1,X2),the_carrier(X0))
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_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_inf_of_relstr_set(A,B)
<=> ? [C] :
( ! [D] :
( element(D,the_carrier(A))
=> ( relstr_element_smaller(A,B,D)
=> related(A,D,C) ) )
& relstr_element_smaller(A,B,C)
& element(C,the_carrier(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t16_yellow_0) ).
fof(f8_neg,negated_conjecture,
~ ! [A] :
( ( rel_str(A)
& antisymmetric_relstr(A) )
=> ! [B] :
( ex_inf_of_relstr_set(A,B)
<=> ? [C] :
( ! [D] :
( element(D,the_carrier(A))
=> ( relstr_element_smaller(A,B,D)
=> related(A,D,C) ) )
& relstr_element_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,D,C)
| ~ relstr_element_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_element_smaller(A,B,C)
& element(C,the_carrier(A)) )
& ~ ex_inf_of_relstr_set(A,B) )
| ( ! [C] :
( ? [D] :
( ~ related(A,D,C)
& relstr_element_smaller(A,B,D)
& element(D,the_carrier(A)) )
| ~ relstr_element_smaller(A,B,C)
| ~ element(C,the_carrier(A)) )
& ex_inf_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,D,sk10)
| ~ relstr_element_smaller(sk7,sk8,D)
| ~ element(D,the_carrier(sk7)) )
& relstr_element_smaller(sk7,sk8,sk10)
& element(sk10,the_carrier(sk7))
& ~ ex_inf_of_relstr_set(sk7,sk8) )
| ( ( ( ~ related(sk7,sk9(C),C)
& relstr_element_smaller(sk7,sk8,sk9(C))
& element(sk9(C),the_carrier(sk7)) )
| ~ relstr_element_smaller(sk7,sk8,C)
| ~ element(C,the_carrier(sk7)) )
& ex_inf_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(p66,plain,
( element(sk3(sk7,X0,X1),the_carrier(sk7))
| element(sk2(sk7,X0,X1),the_carrier(sk7))
| ~ relstr_element_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c6,c26]) ).
cnf(c28,plain,
( element(sk10,the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p122,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| element(sk3(sk7,X0,sk10),the_carrier(sk7))
| element(sk2(sk7,X0,sk10),the_carrier(sk7))
| ~ relstr_element_smaller(sk7,X0,sk10)
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p66,c28]) ).
cnf(p123,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ~ relstr_element_smaller(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p122]) ).
cnf(c29,plain,
( relstr_element_smaller(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p127,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p123,c29]) ).
cnf(p128,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p127]) ).
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(p108,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(p109,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)],[p108,c26]) ).
cnf(p113,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| sk10 = X0
| ~ related(sk7,X0,sk10)
| ~ related(sk7,sk10,X0)
| ~ element(X0,the_carrier(sk7)) ),
inference(resolution,[status(thm)],[p109,c28]) ).
cnf(p133,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ related(sk7,sk10,sk3(sk7,sk8,sk10))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p128,p113]) ).
cnf(p269,plain,
( sk10 = sk3(sk7,sk8,sk10)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ related(sk7,sk10,sk3(sk7,sk8,sk10))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p133]) ).
cnf(c8,plain,
( related(X0,X4,sk3(X0,X1,X2))
| ~ relstr_element_smaller(X0,X1,X4)
| ~ element(X4,the_carrier(X0))
| element(sk2(X0,X1,X2),the_carrier(X0))
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p74,plain,
( related(X0,X2,sk3(X0,X1,X2))
| ~ relstr_element_smaller(X0,X1,X2)
| element(sk2(X0,X1,X2),the_carrier(X0))
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(factoring,[status(thm)],[c8]) ).
cnf(p168,plain,
( related(X0,X2,sk3(X0,X1,X2))
| element(sk2(X0,X1,X2),the_carrier(X0))
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(factoring,[status(thm)],[p74]) ).
cnf(p228,plain,
( related(sk7,X1,sk3(sk7,X0,X1))
| element(sk2(sk7,X0,X1),the_carrier(sk7))
| ~ relstr_element_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p168,c26]) ).
cnf(p234,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| related(sk7,sk10,sk3(sk7,X0,sk10))
| element(sk2(sk7,X0,sk10),the_carrier(sk7))
| ~ relstr_element_smaller(sk7,X0,sk10)
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p228,c28]) ).
cnf(p236,plain,
( related(sk7,sk10,sk3(sk7,sk8,sk10))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ~ relstr_element_smaller(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p234]) ).
cnf(p238,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| related(sk7,sk10,sk3(sk7,sk8,sk10))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p236,c29]) ).
cnf(p244,plain,
( related(sk7,sk10,sk3(sk7,sk8,sk10))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p238]) ).
cnf(p280,plain,
( element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p269,p244]) ).
cnf(p307,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p280]) ).
cnf(p308,plain,
( sk10 = sk3(sk7,sk8,sk10)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p307]) ).
cnf(c30,plain,
( related(sk7,X3,sk10)
| ~ relstr_element_smaller(sk7,sk8,X3)
| ~ element(X3,the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p129,plain,
( related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ relstr_element_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p128,c30]) ).
cnf(p220,plain,
( related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ relstr_element_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p129]) ).
cnf(c7,plain,
( relstr_element_smaller(X0,X1,sk3(X0,X1,X2))
| element(sk2(X0,X1,X2),the_carrier(X0))
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p71,plain,
( relstr_element_smaller(sk7,X0,sk3(sk7,X0,X1))
| element(sk2(sk7,X0,X1),the_carrier(sk7))
| ~ relstr_element_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c7,c26]) ).
cnf(p164,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| relstr_element_smaller(sk7,X0,sk3(sk7,X0,sk10))
| element(sk2(sk7,X0,sk10),the_carrier(sk7))
| ~ relstr_element_smaller(sk7,X0,sk10)
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p71,c28]) ).
cnf(p166,plain,
( relstr_element_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ~ relstr_element_smaller(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p164]) ).
cnf(p169,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| relstr_element_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p166,c29]) ).
cnf(p170,plain,
( relstr_element_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p169]) ).
cnf(p221,plain,
( element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8)
| related(sk7,sk3(sk7,sk8,sk10),sk10)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p220,p170]) ).
cnf(p225,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| related(sk7,sk3(sk7,sk8,sk10),sk10)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p221]) ).
cnf(p226,plain,
( related(sk7,sk3(sk7,sk8,sk10),sk10)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p225]) ).
cnf(p309,plain,
( element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p308,p226]) ).
cnf(p314,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p309]) ).
cnf(p315,plain,
( sk10 = sk3(sk7,sk8,sk10)
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p314]) ).
cnf(p316,plain,
( related(sk7,sk2(sk7,sk8,sk10),sk10)
| ~ relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p315,c30]) ).
cnf(p338,plain,
( related(sk7,sk2(sk7,sk8,sk10),sk10)
| ~ relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p316]) ).
cnf(c10,plain,
( element(sk3(X0,X1,X2),the_carrier(X0))
| relstr_element_smaller(X0,X1,sk2(X0,X1,X2))
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p83,plain,
( element(sk3(sk7,X0,X1),the_carrier(sk7))
| relstr_element_smaller(sk7,X0,sk2(sk7,X0,X1))
| ~ relstr_element_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c10,c26]) ).
cnf(p176,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| element(sk3(sk7,X0,sk10),the_carrier(sk7))
| relstr_element_smaller(sk7,X0,sk2(sk7,X0,sk10))
| ~ relstr_element_smaller(sk7,X0,sk10)
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p83,c28]) ).
cnf(p178,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ~ relstr_element_smaller(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p176]) ).
cnf(p180,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p178,c29]) ).
cnf(p181,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p180]) ).
cnf(p342,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8)
| related(sk7,sk2(sk7,sk8,sk10),sk10)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p338,p181]) ).
cnf(p343,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| related(sk7,sk2(sk7,sk8,sk10),sk10)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p342]) ).
cnf(c14,plain,
( element(sk3(X0,X1,X2),the_carrier(X0))
| ~ related(X0,sk2(X0,X1,X2),X2)
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p106,plain,
( element(sk3(sk7,X0,X1),the_carrier(sk7))
| ~ related(sk7,sk2(sk7,X0,X1),X1)
| ~ relstr_element_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c14,c26]) ).
cnf(p197,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| element(sk3(sk7,X0,sk10),the_carrier(sk7))
| ~ related(sk7,sk2(sk7,X0,sk10),sk10)
| ~ relstr_element_smaller(sk7,X0,sk10)
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p106,c28]) ).
cnf(p199,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| ~ related(sk7,sk2(sk7,sk8,sk10),sk10)
| ~ relstr_element_smaller(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p197]) ).
cnf(p201,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| ~ related(sk7,sk2(sk7,sk8,sk10),sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p199,c29]) ).
cnf(p202,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| ~ related(sk7,sk2(sk7,sk8,sk10),sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p201]) ).
cnf(p345,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8)
| element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p343,p202]) ).
cnf(p354,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p345]) ).
cnf(p355,plain,
( element(sk3(sk7,sk8,sk10),the_carrier(sk7))
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p354]) ).
cnf(p360,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ related(sk7,sk10,sk3(sk7,sk8,sk10))
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p355,p113]) ).
cnf(p389,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ related(sk7,sk10,sk3(sk7,sk8,sk10))
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p360]) ).
cnf(p390,plain,
( ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ related(sk7,sk10,sk3(sk7,sk8,sk10))
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p389]) ).
cnf(c12,plain,
( related(X0,X4,sk3(X0,X1,X2))
| ~ relstr_element_smaller(X0,X1,X4)
| ~ element(X4,the_carrier(X0))
| relstr_element_smaller(X0,X1,sk2(X0,X1,X2))
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p89,plain,
( related(X0,X2,sk3(X0,X1,X2))
| ~ relstr_element_smaller(X0,X1,X2)
| relstr_element_smaller(X0,X1,sk2(X0,X1,X2))
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(factoring,[status(thm)],[c12]) ).
cnf(p203,plain,
( related(X0,X2,sk3(X0,X1,X2))
| relstr_element_smaller(X0,X1,sk2(X0,X1,X2))
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(factoring,[status(thm)],[p89]) ).
cnf(p249,plain,
( related(sk7,X1,sk3(sk7,X0,X1))
| relstr_element_smaller(sk7,X0,sk2(sk7,X0,X1))
| ~ relstr_element_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p203,c26]) ).
cnf(p252,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| related(sk7,sk10,sk3(sk7,X0,sk10))
| relstr_element_smaller(sk7,X0,sk2(sk7,X0,sk10))
| ~ relstr_element_smaller(sk7,X0,sk10)
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p249,c28]) ).
cnf(p254,plain,
( related(sk7,sk10,sk3(sk7,sk8,sk10))
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ~ relstr_element_smaller(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p252]) ).
cnf(p259,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| related(sk7,sk10,sk3(sk7,sk8,sk10))
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p254,c29]) ).
cnf(p260,plain,
( related(sk7,sk10,sk3(sk7,sk8,sk10))
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p259]) ).
cnf(p391,plain,
( relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8)
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p390,p260]) ).
cnf(p392,plain,
( relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p391]) ).
cnf(p356,plain,
( related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ relstr_element_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p355,c30]) ).
cnf(p382,plain,
( related(sk7,sk3(sk7,sk8,sk10),sk10)
| ~ relstr_element_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p356]) ).
cnf(c11,plain,
( relstr_element_smaller(X0,X1,sk3(X0,X1,X2))
| relstr_element_smaller(X0,X1,sk2(X0,X1,X2))
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p85,plain,
( relstr_element_smaller(sk7,X0,sk3(sk7,X0,X1))
| relstr_element_smaller(sk7,X0,sk2(sk7,X0,X1))
| ~ relstr_element_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c11,c26]) ).
cnf(p189,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| relstr_element_smaller(sk7,X0,sk3(sk7,X0,sk10))
| relstr_element_smaller(sk7,X0,sk2(sk7,X0,sk10))
| ~ relstr_element_smaller(sk7,X0,sk10)
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p85,c28]) ).
cnf(p191,plain,
( relstr_element_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ~ relstr_element_smaller(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p189]) ).
cnf(p193,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| relstr_element_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p191,c29]) ).
cnf(p194,plain,
( relstr_element_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p193]) ).
cnf(p383,plain,
( relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8)
| related(sk7,sk3(sk7,sk8,sk10),sk10)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p382,p194]) ).
cnf(p384,plain,
( relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| related(sk7,sk3(sk7,sk8,sk10),sk10)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p383]) ).
cnf(p396,plain,
( relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8)
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p392,p384]) ).
cnf(p399,plain,
( sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8)
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p396]) ).
cnf(p401,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p399]) ).
cnf(p402,plain,
( relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p401]) ).
cnf(p403,plain,
( related(sk7,sk2(sk7,sk8,sk10),sk10)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p402,p338]) ).
cnf(p405,plain,
( related(sk7,sk2(sk7,sk8,sk10),sk10)
| ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p403]) ).
cnf(p406,plain,
( related(sk7,sk2(sk7,sk8,sk10),sk10)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p405]) ).
cnf(c16,plain,
( related(X0,X4,sk3(X0,X1,X2))
| ~ relstr_element_smaller(X0,X1,X4)
| ~ element(X4,the_carrier(X0))
| ~ related(X0,sk2(X0,X1,X2),X2)
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p116,plain,
( related(X0,X2,sk3(X0,X1,X2))
| ~ relstr_element_smaller(X0,X1,X2)
| ~ related(X0,sk2(X0,X1,X2),X2)
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(factoring,[status(thm)],[c16]) ).
cnf(p223,plain,
( related(X0,X2,sk3(X0,X1,X2))
| ~ related(X0,sk2(X0,X1,X2),X2)
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(factoring,[status(thm)],[p116]) ).
cnf(p264,plain,
( related(sk7,X1,sk3(sk7,X0,X1))
| ~ related(sk7,sk2(sk7,X0,X1),X1)
| ~ relstr_element_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p223,c26]) ).
cnf(p267,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| related(sk7,sk10,sk3(sk7,X0,sk10))
| ~ related(sk7,sk2(sk7,X0,sk10),sk10)
| ~ relstr_element_smaller(sk7,X0,sk10)
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p264,c28]) ).
cnf(p270,plain,
( related(sk7,sk10,sk3(sk7,sk8,sk10))
| ~ related(sk7,sk2(sk7,sk8,sk10),sk10)
| ~ relstr_element_smaller(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p267]) ).
cnf(p272,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| related(sk7,sk10,sk3(sk7,sk8,sk10))
| ~ related(sk7,sk2(sk7,sk8,sk10),sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p270,c29]) ).
cnf(p273,plain,
( related(sk7,sk10,sk3(sk7,sk8,sk10))
| ~ related(sk7,sk2(sk7,sk8,sk10),sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p272]) ).
cnf(p409,plain,
( related(sk7,sk10,sk3(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p406,p273]) ).
cnf(p417,plain,
( related(sk7,sk10,sk3(sk7,sk8,sk10))
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p409]) ).
cnf(p418,plain,
( ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p417,p390]) ).
cnf(p426,plain,
( ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p418]) ).
cnf(p427,plain,
( ~ related(sk7,sk3(sk7,sk8,sk10),sk10)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p426]) ).
cnf(c15,plain,
( relstr_element_smaller(X0,X1,sk3(X0,X1,X2))
| ~ related(X0,sk2(X0,X1,X2),X2)
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p111,plain,
( relstr_element_smaller(sk7,X0,sk3(sk7,X0,X1))
| ~ related(sk7,sk2(sk7,X0,X1),X1)
| ~ relstr_element_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c15,c26]) ).
cnf(p206,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| relstr_element_smaller(sk7,X0,sk3(sk7,X0,sk10))
| ~ related(sk7,sk2(sk7,X0,sk10),sk10)
| ~ relstr_element_smaller(sk7,X0,sk10)
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p111,c28]) ).
cnf(p208,plain,
( relstr_element_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| ~ related(sk7,sk2(sk7,sk8,sk10),sk10)
| ~ relstr_element_smaller(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p206]) ).
cnf(p213,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| relstr_element_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| ~ related(sk7,sk2(sk7,sk8,sk10),sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p208,c29]) ).
cnf(p214,plain,
( relstr_element_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| ~ related(sk7,sk2(sk7,sk8,sk10),sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p213]) ).
cnf(p408,plain,
( relstr_element_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p406,p214]) ).
cnf(p415,plain,
( relstr_element_smaller(sk7,sk8,sk3(sk7,sk8,sk10))
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p408]) ).
cnf(p416,plain,
( related(sk7,sk3(sk7,sk8,sk10),sk10)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p415,p382]) ).
cnf(p420,plain,
( related(sk7,sk3(sk7,sk8,sk10),sk10)
| ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p416]) ).
cnf(p421,plain,
( related(sk7,sk3(sk7,sk8,sk10),sk10)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p420]) ).
cnf(p428,plain,
( sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p427,p421]) ).
cnf(p432,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p428]) ).
cnf(p433,plain,
( sk10 = sk3(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p432]) ).
cnf(c9,plain,
( sk3(X0,X1,X2) != X2
| element(sk2(X0,X1,X2),the_carrier(X0))
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p81,plain,
( sk3(sk7,X0,X1) != X1
| element(sk2(sk7,X0,X1),the_carrier(sk7))
| ~ relstr_element_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c9,c26]) ).
cnf(p88,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| sk3(sk7,X0,sk10) != sk10
| element(sk2(sk7,X0,sk10),the_carrier(sk7))
| ~ relstr_element_smaller(sk7,X0,sk10)
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p81,c28]) ).
cnf(p93,plain,
( sk3(sk7,sk8,sk10) != sk10
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ~ relstr_element_smaller(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p88]) ).
cnf(p95,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| sk3(sk7,sk8,sk10) != sk10
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p93,c29]) ).
cnf(p96,plain,
( sk3(sk7,sk8,sk10) != sk10
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p95]) ).
cnf(p434,plain,
( sk10 != sk10
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(superposition,[status(thm)],[p433,p96]) ).
cnf(p452,plain,
( sk10 != sk10
| element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p434]) ).
cnf(p457,plain,
( element(sk2(sk7,sk8,sk10),the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(equality_resolution,[status(thm)],[p452]) ).
cnf(p458,plain,
( related(sk7,sk2(sk7,sk8,sk10),sk10)
| ~ relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p457,c30]) ).
cnf(p482,plain,
( related(sk7,sk2(sk7,sk8,sk10),sk10)
| ~ relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p458]) ).
cnf(c13,plain,
( sk3(X0,X1,X2) != X2
| relstr_element_smaller(X0,X1,sk2(X0,X1,X2))
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p98,plain,
( sk3(sk7,X0,X1) != X1
| relstr_element_smaller(sk7,X0,sk2(sk7,X0,X1))
| ~ relstr_element_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c13,c26]) ).
cnf(p101,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| sk3(sk7,X0,sk10) != sk10
| relstr_element_smaller(sk7,X0,sk2(sk7,X0,sk10))
| ~ relstr_element_smaller(sk7,X0,sk10)
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p98,c28]) ).
cnf(p102,plain,
( sk3(sk7,sk8,sk10) != sk10
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ~ relstr_element_smaller(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p101]) ).
cnf(p104,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| sk3(sk7,sk8,sk10) != sk10
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p102,c29]) ).
cnf(p107,plain,
( sk3(sk7,sk8,sk10) != sk10
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p104]) ).
cnf(p435,plain,
( sk10 != sk10
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(superposition,[status(thm)],[p433,p107]) ).
cnf(p480,plain,
( sk10 != sk10
| relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p435]) ).
cnf(p481,plain,
( relstr_element_smaller(sk7,sk8,sk2(sk7,sk8,sk10))
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(equality_resolution,[status(thm)],[p480]) ).
cnf(p483,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| related(sk7,sk2(sk7,sk8,sk10),sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p482,p481]) ).
cnf(p484,plain,
( related(sk7,sk2(sk7,sk8,sk10),sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p483]) ).
cnf(c17,plain,
( sk3(X0,X1,X2) != X2
| ~ related(X0,sk2(X0,X1,X2),X2)
| ~ relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p126,plain,
( sk3(sk7,X0,X1) != X1
| ~ related(sk7,sk2(sk7,X0,X1),X1)
| ~ relstr_element_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c17,c26]) ).
cnf(p144,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| sk3(sk7,X0,sk10) != sk10
| ~ related(sk7,sk2(sk7,X0,sk10),sk10)
| ~ relstr_element_smaller(sk7,X0,sk10)
| ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[p126,c28]) ).
cnf(p152,plain,
( sk3(sk7,sk8,sk10) != sk10
| ~ related(sk7,sk2(sk7,sk8,sk10),sk10)
| ~ relstr_element_smaller(sk7,sk8,sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p144]) ).
cnf(p157,plain,
( ex_inf_of_relstr_set(sk7,sk8)
| sk3(sk7,sk8,sk10) != sk10
| ~ related(sk7,sk2(sk7,sk8,sk10),sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p152,c29]) ).
cnf(p158,plain,
( sk3(sk7,sk8,sk10) != sk10
| ~ related(sk7,sk2(sk7,sk8,sk10),sk10)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p157]) ).
cnf(p485,plain,
( sk3(sk7,sk8,sk10) != sk10
| ex_inf_of_relstr_set(sk7,sk8)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(resolution,[status(thm)],[p484,p158]) ).
cnf(p492,plain,
( sk3(sk7,sk8,sk10) != sk10
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p485]) ).
cnf(p493,plain,
( sk10 != sk10
| ex_inf_of_relstr_set(sk7,sk8)
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(superposition,[status(thm)],[p433,p492]) ).
cnf(p494,plain,
( sk10 != sk10
| ex_inf_of_relstr_set(sk7,sk8) ),
inference(factoring,[status(thm)],[p493]) ).
cnf(p495,plain,
ex_inf_of_relstr_set(sk7,sk8),
inference(equality_resolution,[status(thm)],[p494]) ).
cnf(c0,plain,
( element(sk0(X0,X1),the_carrier(X0))
| ~ ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p45,plain,
( element(sk0(sk7,X0),the_carrier(sk7))
| ~ ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c26,c0]) ).
cnf(p496,plain,
element(sk0(sk7,sk8),the_carrier(sk7)),
inference(resolution,[status(thm)],[p495,p45]) ).
cnf(c39,plain,
( ~ ex_inf_of_relstr_set(sk7,sk8)
| ~ related(sk7,sk9(X2),X2)
| ~ relstr_element_smaller(sk7,sk8,X2)
| ~ element(X2,the_carrier(sk7)) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p504,plain,
( ~ ex_inf_of_relstr_set(sk7,sk8)
| ~ related(sk7,sk9(sk0(sk7,sk8)),sk0(sk7,sk8))
| ~ relstr_element_smaller(sk7,sk8,sk0(sk7,sk8)) ),
inference(resolution,[status(thm)],[p496,c39]) ).
cnf(c1,plain,
( relstr_element_smaller(X0,X1,sk0(X0,X1))
| ~ ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p47,plain,
( relstr_element_smaller(sk7,X0,sk0(sk7,X0))
| ~ ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c1,c26]) ).
cnf(p497,plain,
relstr_element_smaller(sk7,sk8,sk0(sk7,sk8)),
inference(resolution,[status(thm)],[p495,p47]) ).
cnf(p581,plain,
( ~ ex_inf_of_relstr_set(sk7,sk8)
| ~ related(sk7,sk9(sk0(sk7,sk8)),sk0(sk7,sk8)) ),
inference(resolution,[status(thm)],[p504,p497]) ).
cnf(c35,plain,
( ~ ex_inf_of_relstr_set(sk7,sk8)
| relstr_element_smaller(sk7,sk8,sk9(X2))
| ~ relstr_element_smaller(sk7,sk8,X2)
| ~ element(X2,the_carrier(sk7)) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p503,plain,
( ~ ex_inf_of_relstr_set(sk7,sk8)
| relstr_element_smaller(sk7,sk8,sk9(sk0(sk7,sk8)))
| ~ relstr_element_smaller(sk7,sk8,sk0(sk7,sk8)) ),
inference(resolution,[status(thm)],[p496,c35]) ).
cnf(p576,plain,
( ~ ex_inf_of_relstr_set(sk7,sk8)
| relstr_element_smaller(sk7,sk8,sk9(sk0(sk7,sk8))) ),
inference(resolution,[status(thm)],[p503,p497]) ).
cnf(p577,plain,
relstr_element_smaller(sk7,sk8,sk9(sk0(sk7,sk8))),
inference(resolution,[status(thm)],[p576,p495]) ).
cnf(c31,plain,
( ~ ex_inf_of_relstr_set(sk7,sk8)
| element(sk9(X2),the_carrier(sk7))
| ~ relstr_element_smaller(sk7,sk8,X2)
| ~ element(X2,the_carrier(sk7)) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p502,plain,
( ~ ex_inf_of_relstr_set(sk7,sk8)
| element(sk9(sk0(sk7,sk8)),the_carrier(sk7))
| ~ relstr_element_smaller(sk7,sk8,sk0(sk7,sk8)) ),
inference(resolution,[status(thm)],[p496,c31]) ).
cnf(p538,plain,
( ~ ex_inf_of_relstr_set(sk7,sk8)
| element(sk9(sk0(sk7,sk8)),the_carrier(sk7)) ),
inference(resolution,[status(thm)],[p502,p497]) ).
cnf(p539,plain,
element(sk9(sk0(sk7,sk8)),the_carrier(sk7)),
inference(resolution,[status(thm)],[p538,p495]) ).
cnf(c2,plain,
( related(X0,X3,sk0(X0,X1))
| ~ relstr_element_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0))
| ~ ex_inf_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p51,plain,
( related(sk7,X1,sk0(sk7,X0))
| ~ relstr_element_smaller(sk7,X0,X1)
| ~ element(X1,the_carrier(sk7))
| ~ ex_inf_of_relstr_set(sk7,X0) ),
inference(resolution,[status(thm)],[c2,c26]) ).
cnf(p498,plain,
( related(sk7,X0,sk0(sk7,sk8))
| ~ relstr_element_smaller(sk7,sk8,X0)
| ~ element(X0,the_carrier(sk7)) ),
inference(resolution,[status(thm)],[p495,p51]) ).
cnf(p573,plain,
( related(sk7,sk9(sk0(sk7,sk8)),sk0(sk7,sk8))
| ~ relstr_element_smaller(sk7,sk8,sk9(sk0(sk7,sk8))) ),
inference(resolution,[status(thm)],[p539,p498]) ).
cnf(p580,plain,
related(sk7,sk9(sk0(sk7,sk8)),sk0(sk7,sk8)),
inference(resolution,[status(thm)],[p577,p573]) ).
cnf(p582,plain,
~ ex_inf_of_relstr_set(sk7,sk8),
inference(resolution,[status(thm)],[p581,p580]) ).
cnf(p584,plain,
$false,
inference(resolution,[status(thm)],[p582,p495]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU357+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.37 % Computer : n006.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 13:49:27 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 4.52/1.12 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.52/1.12 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------