%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU359+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 : n019.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:50 PM UTC 2026
% Result : Theorem 4.75s 1.15s
% Output : Proof 4.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 4
% Syntax : Number of formulae : 116 ( 14 unt; 0 def)
% Number of atoms : 462 ( 64 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 549 ( 203 ~; 267 |; 52 &)
% ( 2 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 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 : 122 ( 2 sgn 41 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f10,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('/export/starexec/sandbox/benchmark/theBenchmark.p',t30_yellow_0) ).
fof(f10_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(negated_conjecture,[status(cth)],[f10]) ).
fof(f10_nnf,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( ( ~ ex_sup_of_relstr_set(A,C)
| B != join_on_relstr(A,C) )
& ! [D] :
( related(A,B,D)
| ~ relstr_set_smaller(A,C,D)
| ~ element(D,the_carrier(A)) )
& relstr_set_smaller(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) )
& ex_sup_of_relstr_set(A,C)
& B = join_on_relstr(A,C) ) )
& element(B,the_carrier(A)) )
& rel_str(A)
& antisymmetric_relstr(A) ),
inference(nnf_transformation,[status(thm)],[f10_neg]) ).
fof(f10_sk,plain,
! [D] :
( ( ( ( ~ ex_sup_of_relstr_set(sk6,sk8)
| sk7 != join_on_relstr(sk6,sk8) )
& ( related(sk6,sk7,D)
| ~ relstr_set_smaller(sk6,sk8,D)
| ~ element(D,the_carrier(sk6)) )
& relstr_set_smaller(sk6,sk8,sk7) )
| ( ( ( ~ related(sk6,sk7,sk9)
& relstr_set_smaller(sk6,sk8,sk9)
& element(sk9,the_carrier(sk6)) )
| ~ relstr_set_smaller(sk6,sk8,sk7) )
& ex_sup_of_relstr_set(sk6,sk8)
& sk7 = join_on_relstr(sk6,sk8) ) )
& element(sk7,the_carrier(sk6))
& rel_str(sk6)
& antisymmetric_relstr(sk6) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk6,sk7,sk8,sk9])],[f10_nnf]) ).
cnf(c22,plain,
( relstr_set_smaller(sk6,sk8,sk7)
| sk7 = join_on_relstr(sk6,sk8) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
fof(f9,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('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_yellow_0) ).
fof(f9_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)],[f9]) ).
fof(f9_sk,plain,
! [A,B,D,C] :
( ( ( ( ~ related(A,C,sk5(A,B,C))
& relstr_set_smaller(A,B,sk5(A,B,C))
& element(sk5(A,B,C),the_carrier(A)) )
| ~ relstr_set_smaller(A,B,C)
| ~ element(C,the_carrier(A))
| ex_sup_of_relstr_set(A,B) )
& ( ( ( related(A,sk4(A,B),D)
| ~ relstr_set_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_set_smaller(A,B,sk4(A,B))
& element(sk4(A,B),the_carrier(A)) )
| ~ ex_sup_of_relstr_set(A,B) ) )
| ~ rel_str(A)
| ~ antisymmetric_relstr(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk4,sk5])],[f9_nnf]) ).
cnf(c18,plain,
( ~ related(X0,X2,sk5(X0,X1,X2))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0)
| ~ antisymmetric_relstr(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(c19,plain,
antisymmetric_relstr(sk6),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p119,plain,
( ~ related(sk6,X1,sk5(sk6,X0,X1))
| ~ relstr_set_smaller(sk6,X0,X1)
| ~ element(X1,the_carrier(sk6))
| ex_sup_of_relstr_set(sk6,X0)
| ~ rel_str(sk6) ),
inference(resolution,[status(thm)],[c18,c19]) ).
cnf(c20,plain,
rel_str(sk6),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p137,plain,
( ~ related(sk6,X1,sk5(sk6,X0,X1))
| ~ relstr_set_smaller(sk6,X0,X1)
| ~ element(X1,the_carrier(sk6))
| ex_sup_of_relstr_set(sk6,X0) ),
inference(resolution,[status(thm)],[p119,c20]) ).
cnf(c21,plain,
element(sk7,the_carrier(sk6)),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p138,plain,
( ~ related(sk6,sk7,sk5(sk6,X0,sk7))
| ~ relstr_set_smaller(sk6,X0,sk7)
| ex_sup_of_relstr_set(sk6,X0) ),
inference(resolution,[status(thm)],[p137,c21]) ).
cnf(c25,plain,
( relstr_set_smaller(sk6,sk8,sk7)
| ex_sup_of_relstr_set(sk6,sk8) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p142,plain,
( ex_sup_of_relstr_set(sk6,sk8)
| ~ related(sk6,sk7,sk5(sk6,sk8,sk7))
| ex_sup_of_relstr_set(sk6,sk8) ),
inference(resolution,[status(thm)],[p138,c25]) ).
cnf(p143,plain,
( ~ related(sk6,sk7,sk5(sk6,sk8,sk7))
| ex_sup_of_relstr_set(sk6,sk8) ),
inference(factoring,[status(thm)],[p142]) ).
cnf(c17,plain,
( relstr_set_smaller(X0,X1,sk5(X0,X1,X2))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0)
| ~ antisymmetric_relstr(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p104,plain,
( relstr_set_smaller(sk6,X0,sk5(sk6,X0,X1))
| ~ relstr_set_smaller(sk6,X0,X1)
| ~ element(X1,the_carrier(sk6))
| ex_sup_of_relstr_set(sk6,X0)
| ~ rel_str(sk6) ),
inference(resolution,[status(thm)],[c17,c19]) ).
cnf(p123,plain,
( relstr_set_smaller(sk6,X0,sk5(sk6,X0,X1))
| ~ relstr_set_smaller(sk6,X0,X1)
| ~ element(X1,the_carrier(sk6))
| ex_sup_of_relstr_set(sk6,X0) ),
inference(resolution,[status(thm)],[p104,c20]) ).
cnf(p124,plain,
( relstr_set_smaller(sk6,X0,sk5(sk6,X0,sk7))
| ~ relstr_set_smaller(sk6,X0,sk7)
| ex_sup_of_relstr_set(sk6,X0) ),
inference(resolution,[status(thm)],[p123,c21]) ).
cnf(p128,plain,
( ex_sup_of_relstr_set(sk6,sk8)
| relstr_set_smaller(sk6,sk8,sk5(sk6,sk8,sk7))
| ex_sup_of_relstr_set(sk6,sk8) ),
inference(resolution,[status(thm)],[p124,c25]) ).
cnf(p131,plain,
( relstr_set_smaller(sk6,sk8,sk5(sk6,sk8,sk7))
| ex_sup_of_relstr_set(sk6,sk8) ),
inference(factoring,[status(thm)],[p128]) ).
cnf(c16,plain,
( element(sk5(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)
| ~ antisymmetric_relstr(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p101,plain,
( element(sk5(sk6,X0,X1),the_carrier(sk6))
| ~ relstr_set_smaller(sk6,X0,X1)
| ~ element(X1,the_carrier(sk6))
| ex_sup_of_relstr_set(sk6,X0)
| ~ rel_str(sk6) ),
inference(resolution,[status(thm)],[c16,c19]) ).
cnf(p103,plain,
( element(sk5(sk6,X0,X1),the_carrier(sk6))
| ~ relstr_set_smaller(sk6,X0,X1)
| ~ element(X1,the_carrier(sk6))
| ex_sup_of_relstr_set(sk6,X0) ),
inference(resolution,[status(thm)],[p101,c20]) ).
cnf(p105,plain,
( element(sk5(sk6,X0,sk7),the_carrier(sk6))
| ~ relstr_set_smaller(sk6,X0,sk7)
| ex_sup_of_relstr_set(sk6,X0) ),
inference(resolution,[status(thm)],[p103,c21]) ).
cnf(p108,plain,
( ex_sup_of_relstr_set(sk6,sk8)
| element(sk5(sk6,sk8,sk7),the_carrier(sk6))
| ex_sup_of_relstr_set(sk6,sk8) ),
inference(resolution,[status(thm)],[p105,c25]) ).
cnf(p109,plain,
( element(sk5(sk6,sk8,sk7),the_carrier(sk6))
| ex_sup_of_relstr_set(sk6,sk8) ),
inference(factoring,[status(thm)],[p108]) ).
cnf(c26,plain,
( related(sk6,sk7,X3)
| ~ relstr_set_smaller(sk6,sk8,X3)
| ~ element(X3,the_carrier(sk6))
| ex_sup_of_relstr_set(sk6,sk8) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p112,plain,
( related(sk6,sk7,sk5(sk6,sk8,sk7))
| ~ relstr_set_smaller(sk6,sk8,sk5(sk6,sk8,sk7))
| ex_sup_of_relstr_set(sk6,sk8)
| ex_sup_of_relstr_set(sk6,sk8) ),
inference(resolution,[status(thm)],[p109,c26]) ).
cnf(p121,plain,
( related(sk6,sk7,sk5(sk6,sk8,sk7))
| ~ relstr_set_smaller(sk6,sk8,sk5(sk6,sk8,sk7))
| ex_sup_of_relstr_set(sk6,sk8) ),
inference(factoring,[status(thm)],[p112]) ).
cnf(p132,plain,
( related(sk6,sk7,sk5(sk6,sk8,sk7))
| ex_sup_of_relstr_set(sk6,sk8)
| ex_sup_of_relstr_set(sk6,sk8) ),
inference(resolution,[status(thm)],[p131,p121]) ).
cnf(p133,plain,
( related(sk6,sk7,sk5(sk6,sk8,sk7))
| ex_sup_of_relstr_set(sk6,sk8) ),
inference(factoring,[status(thm)],[p132]) ).
cnf(p145,plain,
( ex_sup_of_relstr_set(sk6,sk8)
| ex_sup_of_relstr_set(sk6,sk8) ),
inference(resolution,[status(thm)],[p143,p133]) ).
cnf(p146,plain,
ex_sup_of_relstr_set(sk6,sk8),
inference(factoring,[status(thm)],[p145]) ).
fof(f1,axiom,
! [A,B] :
( rel_str(A)
=> element(join_on_relstr(A,B),the_carrier(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_yellow_0) ).
fof(f1_nnf,plain,
! [A,B] :
( element(join_on_relstr(A,B),the_carrier(A))
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B] :
( element(join_on_relstr(A,B),the_carrier(A))
| ~ rel_str(A) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c5,plain,
( element(join_on_relstr(X0,X1),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p53,plain,
element(join_on_relstr(sk6,X0),the_carrier(sk6)),
inference(resolution,[status(thm)],[c5,c20]) ).
fof(f0,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('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_yellow_0) ).
fof(f0_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)
| C = join_on_relstr(A,B) )
& ( ( ! [D] :
( related(A,C,D)
| ~ relstr_set_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_set_smaller(A,B,C) )
| C != join_on_relstr(A,B) ) )
| ~ ex_sup_of_relstr_set(A,B)
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,C,B,D] :
( ( ( ( ~ 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)
| C = join_on_relstr(A,B) )
& ( ( ( related(A,C,D)
| ~ relstr_set_smaller(A,B,D)
| ~ element(D,the_carrier(A)) )
& relstr_set_smaller(A,B,C) )
| C != join_on_relstr(A,B) ) )
| ~ ex_sup_of_relstr_set(A,B)
| ~ element(C,the_carrier(A))
| ~ rel_str(A) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f0_nnf]) ).
cnf(c0,plain,
( relstr_set_smaller(X0,X1,X2)
| X2 != join_on_relstr(X0,X1)
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p38,plain,
( relstr_set_smaller(sk6,X1,X0)
| X0 != join_on_relstr(sk6,X1)
| ~ ex_sup_of_relstr_set(sk6,X1)
| ~ element(X0,the_carrier(sk6)) ),
inference(resolution,[status(thm)],[c0,c20]) ).
cnf(p39,plain,
( relstr_set_smaller(sk6,X0,join_on_relstr(sk6,X0))
| ~ ex_sup_of_relstr_set(sk6,X0)
| ~ element(join_on_relstr(sk6,X0),the_carrier(sk6)) ),
inference(equality_resolution,[status(thm)],[p38]) ).
cnf(p56,plain,
( relstr_set_smaller(sk6,X0,join_on_relstr(sk6,X0))
| ~ ex_sup_of_relstr_set(sk6,X0) ),
inference(resolution,[status(thm)],[p53,p39]) ).
cnf(p148,plain,
relstr_set_smaller(sk6,sk8,join_on_relstr(sk6,sk8)),
inference(resolution,[status(thm)],[p146,p56]) ).
cnf(p169,plain,
( relstr_set_smaller(sk6,sk8,sk7)
| relstr_set_smaller(sk6,sk8,sk7) ),
inference(superposition,[status(thm)],[c22,p148]) ).
cnf(p182,plain,
relstr_set_smaller(sk6,sk8,sk7),
inference(factoring,[status(thm)],[p169]) ).
cnf(c29,plain,
( related(sk6,sk7,X3)
| ~ relstr_set_smaller(sk6,sk8,X3)
| ~ element(X3,the_carrier(sk6))
| element(sk9,the_carrier(sk6))
| ~ relstr_set_smaller(sk6,sk8,sk7) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p188,plain,
( related(sk6,sk7,X0)
| ~ relstr_set_smaller(sk6,sk8,X0)
| ~ element(X0,the_carrier(sk6))
| element(sk9,the_carrier(sk6)) ),
inference(resolution,[status(thm)],[p182,c29]) ).
cnf(c2,plain,
( element(sk0(X0,X1,X2),the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| X2 = join_on_relstr(X0,X1)
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p46,plain,
( element(sk0(sk6,X1,X0),the_carrier(sk6))
| ~ relstr_set_smaller(sk6,X1,X0)
| X0 = join_on_relstr(sk6,X1)
| ~ ex_sup_of_relstr_set(sk6,X1)
| ~ element(X0,the_carrier(sk6)) ),
inference(resolution,[status(thm)],[c2,c20]) ).
cnf(p60,plain,
( element(sk0(sk6,X0,sk7),the_carrier(sk6))
| ~ relstr_set_smaller(sk6,X0,sk7)
| sk7 = join_on_relstr(sk6,X0)
| ~ ex_sup_of_relstr_set(sk6,X0) ),
inference(resolution,[status(thm)],[p46,c21]) ).
cnf(p150,plain,
( element(sk0(sk6,sk8,sk7),the_carrier(sk6))
| ~ relstr_set_smaller(sk6,sk8,sk7)
| sk7 = join_on_relstr(sk6,sk8) ),
inference(resolution,[status(thm)],[p146,p60]) ).
cnf(p228,plain,
( element(sk0(sk6,sk8,sk7),the_carrier(sk6))
| sk7 = join_on_relstr(sk6,sk8) ),
inference(resolution,[status(thm)],[p150,p182]) ).
cnf(p254,plain,
( sk7 = join_on_relstr(sk6,sk8)
| related(sk6,sk7,sk0(sk6,sk8,sk7))
| ~ relstr_set_smaller(sk6,sk8,sk0(sk6,sk8,sk7))
| element(sk9,the_carrier(sk6)) ),
inference(resolution,[status(thm)],[p188,p228]) ).
cnf(c3,plain,
( relstr_set_smaller(X0,X1,sk0(X0,X1,X2))
| ~ relstr_set_smaller(X0,X1,X2)
| X2 = join_on_relstr(X0,X1)
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p48,plain,
( relstr_set_smaller(sk6,X1,sk0(sk6,X1,X0))
| ~ relstr_set_smaller(sk6,X1,X0)
| X0 = join_on_relstr(sk6,X1)
| ~ ex_sup_of_relstr_set(sk6,X1)
| ~ element(X0,the_carrier(sk6)) ),
inference(resolution,[status(thm)],[c3,c20]) ).
cnf(p62,plain,
( relstr_set_smaller(sk6,X0,sk0(sk6,X0,sk7))
| ~ relstr_set_smaller(sk6,X0,sk7)
| sk7 = join_on_relstr(sk6,X0)
| ~ ex_sup_of_relstr_set(sk6,X0) ),
inference(resolution,[status(thm)],[p48,c21]) ).
cnf(p151,plain,
( relstr_set_smaller(sk6,sk8,sk0(sk6,sk8,sk7))
| ~ relstr_set_smaller(sk6,sk8,sk7)
| sk7 = join_on_relstr(sk6,sk8) ),
inference(resolution,[status(thm)],[p146,p62]) ).
cnf(p242,plain,
( relstr_set_smaller(sk6,sk8,sk0(sk6,sk8,sk7))
| sk7 = join_on_relstr(sk6,sk8) ),
inference(resolution,[status(thm)],[p151,p182]) ).
cnf(p295,plain,
( sk7 = join_on_relstr(sk6,sk8)
| sk7 = join_on_relstr(sk6,sk8)
| related(sk6,sk7,sk0(sk6,sk8,sk7))
| element(sk9,the_carrier(sk6)) ),
inference(resolution,[status(thm)],[p254,p242]) ).
cnf(p296,plain,
( sk7 = join_on_relstr(sk6,sk8)
| related(sk6,sk7,sk0(sk6,sk8,sk7))
| element(sk9,the_carrier(sk6)) ),
inference(factoring,[status(thm)],[p295]) ).
cnf(c4,plain,
( ~ related(X0,X2,sk0(X0,X1,X2))
| ~ relstr_set_smaller(X0,X1,X2)
| X2 = join_on_relstr(X0,X1)
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p51,plain,
( ~ related(sk6,X0,sk0(sk6,X1,X0))
| ~ relstr_set_smaller(sk6,X1,X0)
| X0 = join_on_relstr(sk6,X1)
| ~ ex_sup_of_relstr_set(sk6,X1)
| ~ element(X0,the_carrier(sk6)) ),
inference(resolution,[status(thm)],[c4,c20]) ).
cnf(p64,plain,
( ~ related(sk6,sk7,sk0(sk6,X0,sk7))
| ~ relstr_set_smaller(sk6,X0,sk7)
| sk7 = join_on_relstr(sk6,X0)
| ~ ex_sup_of_relstr_set(sk6,X0) ),
inference(resolution,[status(thm)],[p51,c21]) ).
cnf(p152,plain,
( ~ related(sk6,sk7,sk0(sk6,sk8,sk7))
| ~ relstr_set_smaller(sk6,sk8,sk7)
| sk7 = join_on_relstr(sk6,sk8) ),
inference(resolution,[status(thm)],[p146,p64]) ).
cnf(p243,plain,
( ~ related(sk6,sk7,sk0(sk6,sk8,sk7))
| sk7 = join_on_relstr(sk6,sk8) ),
inference(resolution,[status(thm)],[p152,p182]) ).
cnf(p298,plain,
( sk7 = join_on_relstr(sk6,sk8)
| sk7 = join_on_relstr(sk6,sk8)
| element(sk9,the_carrier(sk6)) ),
inference(resolution,[status(thm)],[p296,p243]) ).
cnf(p299,plain,
( sk7 = join_on_relstr(sk6,sk8)
| element(sk9,the_carrier(sk6)) ),
inference(factoring,[status(thm)],[p298]) ).
cnf(c30,plain,
( ~ ex_sup_of_relstr_set(sk6,sk8)
| sk7 != join_on_relstr(sk6,sk8)
| element(sk9,the_carrier(sk6))
| ~ relstr_set_smaller(sk6,sk8,sk7) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p187,plain,
( ~ ex_sup_of_relstr_set(sk6,sk8)
| sk7 != join_on_relstr(sk6,sk8)
| element(sk9,the_carrier(sk6)) ),
inference(resolution,[status(thm)],[p182,c30]) ).
cnf(p304,plain,
( ~ ex_sup_of_relstr_set(sk6,sk8)
| element(sk9,the_carrier(sk6))
| element(sk9,the_carrier(sk6)) ),
inference(resolution,[status(thm)],[p299,p187]) ).
cnf(p310,plain,
( ~ ex_sup_of_relstr_set(sk6,sk8)
| element(sk9,the_carrier(sk6)) ),
inference(factoring,[status(thm)],[p304]) ).
cnf(p311,plain,
element(sk9,the_carrier(sk6)),
inference(resolution,[status(thm)],[p310,p146]) ).
cnf(c23,plain,
( related(sk6,sk7,X3)
| ~ relstr_set_smaller(sk6,sk8,X3)
| ~ element(X3,the_carrier(sk6))
| sk7 = join_on_relstr(sk6,sk8) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p313,plain,
( related(sk6,sk7,sk9)
| ~ relstr_set_smaller(sk6,sk8,sk9)
| sk7 = join_on_relstr(sk6,sk8) ),
inference(resolution,[status(thm)],[p311,c23]) ).
cnf(c32,plain,
( related(sk6,sk7,X3)
| ~ relstr_set_smaller(sk6,sk8,X3)
| ~ element(X3,the_carrier(sk6))
| relstr_set_smaller(sk6,sk8,sk9)
| ~ relstr_set_smaller(sk6,sk8,sk7) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p185,plain,
( related(sk6,sk7,X0)
| ~ relstr_set_smaller(sk6,sk8,X0)
| ~ element(X0,the_carrier(sk6))
| relstr_set_smaller(sk6,sk8,sk9) ),
inference(resolution,[status(thm)],[p182,c32]) ).
cnf(p248,plain,
( sk7 = join_on_relstr(sk6,sk8)
| related(sk6,sk7,sk0(sk6,sk8,sk7))
| ~ relstr_set_smaller(sk6,sk8,sk0(sk6,sk8,sk7))
| relstr_set_smaller(sk6,sk8,sk9) ),
inference(resolution,[status(thm)],[p185,p228]) ).
cnf(p261,plain,
( sk7 = join_on_relstr(sk6,sk8)
| sk7 = join_on_relstr(sk6,sk8)
| related(sk6,sk7,sk0(sk6,sk8,sk7))
| relstr_set_smaller(sk6,sk8,sk9) ),
inference(resolution,[status(thm)],[p248,p242]) ).
cnf(p262,plain,
( sk7 = join_on_relstr(sk6,sk8)
| related(sk6,sk7,sk0(sk6,sk8,sk7))
| relstr_set_smaller(sk6,sk8,sk9) ),
inference(factoring,[status(thm)],[p261]) ).
cnf(p263,plain,
( sk7 = join_on_relstr(sk6,sk8)
| sk7 = join_on_relstr(sk6,sk8)
| relstr_set_smaller(sk6,sk8,sk9) ),
inference(resolution,[status(thm)],[p262,p243]) ).
cnf(p264,plain,
( sk7 = join_on_relstr(sk6,sk8)
| relstr_set_smaller(sk6,sk8,sk9) ),
inference(factoring,[status(thm)],[p263]) ).
cnf(c33,plain,
( ~ ex_sup_of_relstr_set(sk6,sk8)
| sk7 != join_on_relstr(sk6,sk8)
| relstr_set_smaller(sk6,sk8,sk9)
| ~ relstr_set_smaller(sk6,sk8,sk7) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p184,plain,
( ~ ex_sup_of_relstr_set(sk6,sk8)
| sk7 != join_on_relstr(sk6,sk8)
| relstr_set_smaller(sk6,sk8,sk9) ),
inference(resolution,[status(thm)],[p182,c33]) ).
cnf(p269,plain,
( ~ ex_sup_of_relstr_set(sk6,sk8)
| relstr_set_smaller(sk6,sk8,sk9)
| relstr_set_smaller(sk6,sk8,sk9) ),
inference(resolution,[status(thm)],[p264,p184]) ).
cnf(p276,plain,
( ~ ex_sup_of_relstr_set(sk6,sk8)
| relstr_set_smaller(sk6,sk8,sk9) ),
inference(factoring,[status(thm)],[p269]) ).
cnf(p278,plain,
relstr_set_smaller(sk6,sk8,sk9),
inference(resolution,[status(thm)],[p276,p146]) ).
cnf(p326,plain,
( related(sk6,sk7,sk9)
| sk7 = join_on_relstr(sk6,sk8) ),
inference(resolution,[status(thm)],[p313,p278]) ).
cnf(c1,plain,
( related(X0,X2,X3)
| ~ relstr_set_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0))
| X2 != join_on_relstr(X0,X1)
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p43,plain,
( related(sk6,X0,X2)
| ~ relstr_set_smaller(sk6,X1,X2)
| ~ element(X2,the_carrier(sk6))
| X0 != join_on_relstr(sk6,X1)
| ~ ex_sup_of_relstr_set(sk6,X1)
| ~ element(X0,the_carrier(sk6)) ),
inference(resolution,[status(thm)],[c1,c20]) ).
cnf(p67,plain,
( related(sk6,join_on_relstr(sk6,X0),X1)
| ~ relstr_set_smaller(sk6,X0,X1)
| ~ element(X1,the_carrier(sk6))
| ~ ex_sup_of_relstr_set(sk6,X0)
| ~ element(join_on_relstr(sk6,X0),the_carrier(sk6)) ),
inference(equality_resolution,[status(thm)],[p43]) ).
cnf(p72,plain,
( related(sk6,join_on_relstr(sk6,X0),X1)
| ~ relstr_set_smaller(sk6,X0,X1)
| ~ element(X1,the_carrier(sk6))
| ~ ex_sup_of_relstr_set(sk6,X0) ),
inference(resolution,[status(thm)],[p67,p53]) ).
cnf(p156,plain,
( related(sk6,join_on_relstr(sk6,sk8),X0)
| ~ relstr_set_smaller(sk6,sk8,X0)
| ~ element(X0,the_carrier(sk6)) ),
inference(resolution,[status(thm)],[p146,p72]) ).
cnf(p322,plain,
( related(sk6,join_on_relstr(sk6,sk8),sk9)
| ~ relstr_set_smaller(sk6,sk8,sk9) ),
inference(resolution,[status(thm)],[p311,p156]) ).
cnf(p324,plain,
related(sk6,join_on_relstr(sk6,sk8),sk9),
inference(resolution,[status(thm)],[p322,p278]) ).
cnf(p339,plain,
( related(sk6,sk7,sk9)
| related(sk6,sk7,sk9) ),
inference(superposition,[status(thm)],[p326,p324]) ).
cnf(p340,plain,
related(sk6,sk7,sk9),
inference(factoring,[status(thm)],[p339]) ).
cnf(c35,plain,
( related(sk6,sk7,X3)
| ~ relstr_set_smaller(sk6,sk8,X3)
| ~ element(X3,the_carrier(sk6))
| ~ related(sk6,sk7,sk9)
| ~ relstr_set_smaller(sk6,sk8,sk7) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p189,plain,
( related(sk6,sk7,X0)
| ~ relstr_set_smaller(sk6,sk8,X0)
| ~ element(X0,the_carrier(sk6))
| ~ related(sk6,sk7,sk9) ),
inference(resolution,[status(thm)],[p182,c35]) ).
cnf(p342,plain,
( related(sk6,sk7,X0)
| ~ relstr_set_smaller(sk6,sk8,X0)
| ~ element(X0,the_carrier(sk6)) ),
inference(resolution,[status(thm)],[p340,p189]) ).
cnf(p346,plain,
( sk7 = join_on_relstr(sk6,sk8)
| related(sk6,sk7,sk0(sk6,sk8,sk7))
| ~ relstr_set_smaller(sk6,sk8,sk0(sk6,sk8,sk7)) ),
inference(resolution,[status(thm)],[p342,p228]) ).
cnf(p351,plain,
( sk7 = join_on_relstr(sk6,sk8)
| sk7 = join_on_relstr(sk6,sk8)
| related(sk6,sk7,sk0(sk6,sk8,sk7)) ),
inference(resolution,[status(thm)],[p346,p242]) ).
cnf(p352,plain,
( sk7 = join_on_relstr(sk6,sk8)
| related(sk6,sk7,sk0(sk6,sk8,sk7)) ),
inference(factoring,[status(thm)],[p351]) ).
cnf(p353,plain,
( sk7 = join_on_relstr(sk6,sk8)
| sk7 = join_on_relstr(sk6,sk8) ),
inference(resolution,[status(thm)],[p352,p243]) ).
cnf(p354,plain,
sk7 = join_on_relstr(sk6,sk8),
inference(factoring,[status(thm)],[p353]) ).
cnf(c36,plain,
( ~ ex_sup_of_relstr_set(sk6,sk8)
| sk7 != join_on_relstr(sk6,sk8)
| ~ related(sk6,sk7,sk9)
| ~ relstr_set_smaller(sk6,sk8,sk7) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p183,plain,
( ~ ex_sup_of_relstr_set(sk6,sk8)
| sk7 != join_on_relstr(sk6,sk8)
| ~ related(sk6,sk7,sk9) ),
inference(resolution,[status(thm)],[p182,c36]) ).
cnf(p341,plain,
( ~ ex_sup_of_relstr_set(sk6,sk8)
| sk7 != join_on_relstr(sk6,sk8) ),
inference(resolution,[status(thm)],[p340,p183]) ).
cnf(p364,plain,
~ ex_sup_of_relstr_set(sk6,sk8),
inference(resolution,[status(thm)],[p354,p341]) ).
cnf(p366,plain,
$false,
inference(resolution,[status(thm)],[p364,p146]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU359+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.13/0.39 % Computer : n019.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Thu Sep 24 13:50:03 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 4.75/1.15 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.75/1.15 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------