%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU359+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n012.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:57:12 PM UTC 2026
% Result : Theorem 1.65s 1.51s
% Output : CNFRefutation 1.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 7
% Syntax : Number of formulae : 180 ( 17 unt; 3 def)
% Number of atoms : 998 ( 127 equ)
% Maximal formula atoms : 15 ( 5 avg)
% Number of connectives : 1187 ( 497 ~; 543 |; 108 &)
% ( 6 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 14 ( 12 usr; 5 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% Number of variables : 323 ( 0 sgn 296 !; 27 ?; 163 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( rel_str(X0)
=> ! [X1,X2] :
( element(X2,the_carrier(X0))
=> ( ex_sup_of_relstr_set(X0,X1)
=> ( X2 = join_on_relstr(X0,X1)
<=> ( ! [X3] :
( element(X3,the_carrier(X0))
=> ( relstr_set_smaller(X0,X1,X3)
=> related(X0,X2,X3) ) )
& relstr_set_smaller(X0,X1,X2) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_yellow_0) ).
fof(f2,axiom,
! [X0,X1] :
( rel_str(X0)
=> element(join_on_relstr(X0,X1),the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_yellow_0) ).
fof(f10,axiom,
! [X0] :
( ( rel_str(X0)
& antisymmetric_relstr(X0) )
=> ! [X1] :
( ex_sup_of_relstr_set(X0,X1)
<=> ? [X2] :
( ! [X3] :
( element(X3,the_carrier(X0))
=> ( relstr_set_smaller(X0,X1,X3)
=> related(X0,X2,X3) ) )
& relstr_set_smaller(X0,X1,X2)
& element(X2,the_carrier(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_yellow_0) ).
fof(f11,conjecture,
! [X0] :
( ( rel_str(X0)
& antisymmetric_relstr(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( ( ( ! [X3] :
( element(X3,the_carrier(X0))
=> ( relstr_set_smaller(X0,X2,X3)
=> related(X0,X1,X3) ) )
& relstr_set_smaller(X0,X2,X1) )
=> ( ex_sup_of_relstr_set(X0,X2)
& X1 = join_on_relstr(X0,X2) ) )
& ( ( ex_sup_of_relstr_set(X0,X2)
& X1 = join_on_relstr(X0,X2) )
=> ( ! [X3] :
( element(X3,the_carrier(X0))
=> ( relstr_set_smaller(X0,X2,X3)
=> related(X0,X1,X3) ) )
& relstr_set_smaller(X0,X2,X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_yellow_0) ).
fof(f12,negated_conjecture,
~ ! [X0] :
( ( rel_str(X0)
& antisymmetric_relstr(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( ( ( ! [X3] :
( element(X3,the_carrier(X0))
=> ( relstr_set_smaller(X0,X2,X3)
=> related(X0,X1,X3) ) )
& relstr_set_smaller(X0,X2,X1) )
=> ( ex_sup_of_relstr_set(X0,X2)
& X1 = join_on_relstr(X0,X2) ) )
& ( ( ex_sup_of_relstr_set(X0,X2)
& X1 = join_on_relstr(X0,X2) )
=> ( ! [X3] :
( element(X3,the_carrier(X0))
=> ( relstr_set_smaller(X0,X2,X3)
=> related(X0,X1,X3) ) )
& relstr_set_smaller(X0,X2,X1) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f11]) ).
fof(f13,plain,
~ ! [X0] :
( ( rel_str(X0)
& antisymmetric_relstr(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( ( ( ! [X4] :
( element(X4,the_carrier(X0))
=> ( relstr_set_smaller(X0,X2,X4)
=> related(X0,X1,X4) ) )
& relstr_set_smaller(X0,X2,X1) )
=> ( ex_sup_of_relstr_set(X0,X2)
& X1 = join_on_relstr(X0,X2) ) )
& ( ( ex_sup_of_relstr_set(X0,X2)
& X1 = join_on_relstr(X0,X2) )
=> ( ! [X3] :
( element(X3,the_carrier(X0))
=> ( relstr_set_smaller(X0,X2,X3)
=> related(X0,X1,X3) ) )
& relstr_set_smaller(X0,X2,X1) ) ) ) ) ),
inference(rectify,[],[f12]) ).
fof(f16,plain,
! [X0] :
( ~ rel_str(X0)
| ! [X1,X2] :
( ~ element(X2,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| ( X2 = join_on_relstr(X0,X1)
<=> ( ! [X3] :
( ~ element(X3,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X3)
| related(X0,X2,X3) )
& relstr_set_smaller(X0,X1,X2) ) ) ) ),
inference(ennf_transformation,[],[f1]) ).
fof(f17,plain,
! [X0] :
( ~ rel_str(X0)
| ! [X1,X2] :
( ~ element(X2,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| ( X2 = join_on_relstr(X0,X1)
<=> ( ! [X3] :
( ~ element(X3,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X3)
| related(X0,X2,X3) )
& relstr_set_smaller(X0,X1,X2) ) ) ) ),
inference(flattening,[],[f16]) ).
fof(f18,plain,
! [X0,X1] :
( ~ rel_str(X0)
| element(join_on_relstr(X0,X1),the_carrier(X0)) ),
inference(ennf_transformation,[],[f2]) ).
fof(f19,plain,
! [X0] :
( ~ rel_str(X0)
| ~ antisymmetric_relstr(X0)
| ! [X1] :
( ex_sup_of_relstr_set(X0,X1)
<=> ? [X2] :
( ! [X3] :
( ~ element(X3,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X3)
| related(X0,X2,X3) )
& relstr_set_smaller(X0,X1,X2)
& element(X2,the_carrier(X0)) ) ) ),
inference(ennf_transformation,[],[f10]) ).
fof(f20,plain,
! [X0] :
( ~ rel_str(X0)
| ~ antisymmetric_relstr(X0)
| ! [X1] :
( ex_sup_of_relstr_set(X0,X1)
<=> ? [X2] :
( ! [X3] :
( ~ element(X3,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X3)
| related(X0,X2,X3) )
& relstr_set_smaller(X0,X1,X2)
& element(X2,the_carrier(X0)) ) ) ),
inference(flattening,[],[f19]) ).
fof(f21,plain,
? [X0] :
( rel_str(X0)
& antisymmetric_relstr(X0)
& ? [X1] :
( element(X1,the_carrier(X0))
& ? [X2] :
( ( ! [X4] :
( ~ element(X4,the_carrier(X0))
| ~ relstr_set_smaller(X0,X2,X4)
| related(X0,X1,X4) )
& relstr_set_smaller(X0,X2,X1)
& ( ~ ex_sup_of_relstr_set(X0,X2)
| join_on_relstr(X0,X2) != X1 ) )
| ( ex_sup_of_relstr_set(X0,X2)
& X1 = join_on_relstr(X0,X2)
& ( ? [X3] :
( element(X3,the_carrier(X0))
& relstr_set_smaller(X0,X2,X3)
& ~ related(X0,X1,X3) )
| ~ relstr_set_smaller(X0,X2,X1) ) ) ) ) ),
inference(ennf_transformation,[],[f13]) ).
fof(f22,plain,
? [X0] :
( rel_str(X0)
& antisymmetric_relstr(X0)
& ? [X1] :
( element(X1,the_carrier(X0))
& ? [X2] :
( ( ! [X4] :
( ~ element(X4,the_carrier(X0))
| ~ relstr_set_smaller(X0,X2,X4)
| related(X0,X1,X4) )
& relstr_set_smaller(X0,X2,X1)
& ( ~ ex_sup_of_relstr_set(X0,X2)
| join_on_relstr(X0,X2) != X1 ) )
| ( ex_sup_of_relstr_set(X0,X2)
& X1 = join_on_relstr(X0,X2)
& ( ? [X3] :
( element(X3,the_carrier(X0))
& relstr_set_smaller(X0,X2,X3)
& ~ related(X0,X1,X3) )
| ~ relstr_set_smaller(X0,X2,X1) ) ) ) ) ),
inference(flattening,[],[f21]) ).
fof(f25,plain,
! [X0] :
( ~ rel_str(X0)
| ! [X1,X2] :
( ~ element(X2,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| ( ( join_on_relstr(X0,X1) != X2
| ( ! [X3] :
( ~ element(X3,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X3)
| related(X0,X2,X3) )
& relstr_set_smaller(X0,X1,X2) ) )
& ( ? [X3] :
( element(X3,the_carrier(X0))
& relstr_set_smaller(X0,X1,X3)
& ~ related(X0,X2,X3) )
| ~ relstr_set_smaller(X0,X1,X2)
| X2 = join_on_relstr(X0,X1) ) ) ) ),
inference(nnf_transformation,[],[f17]) ).
fof(f26,plain,
! [X0] :
( ~ rel_str(X0)
| ! [X1,X2] :
( ~ element(X2,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| ( ( join_on_relstr(X0,X1) != X2
| ( ! [X3] :
( ~ element(X3,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X3)
| related(X0,X2,X3) )
& relstr_set_smaller(X0,X1,X2) ) )
& ( ? [X3] :
( element(X3,the_carrier(X0))
& relstr_set_smaller(X0,X1,X3)
& ~ related(X0,X2,X3) )
| ~ relstr_set_smaller(X0,X1,X2)
| X2 = join_on_relstr(X0,X1) ) ) ) ),
inference(flattening,[],[f25]) ).
fof(f27,plain,
! [X0] :
( ~ rel_str(X0)
| ! [X1,X2] :
( ~ element(X2,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| ( ( join_on_relstr(X0,X1) != X2
| ( ! [X4] :
( ~ element(X4,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X4)
| related(X0,X2,X4) )
& relstr_set_smaller(X0,X1,X2) ) )
& ( ? [X3] :
( element(X3,the_carrier(X0))
& relstr_set_smaller(X0,X1,X3)
& ~ related(X0,X2,X3) )
| ~ relstr_set_smaller(X0,X1,X2)
| X2 = join_on_relstr(X0,X1) ) ) ) ),
inference(rectify,[],[f26]) ).
fof(f28,plain,
! [X0] :
( ~ rel_str(X0)
| ! [X1,X2] :
( ~ element(X2,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| ( ( join_on_relstr(X0,X1) != X2
| ( ! [X4] :
( ~ element(X4,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X4)
| related(X0,X2,X4) )
& relstr_set_smaller(X0,X1,X2) ) )
& ( ( element(sK1(X0,X1,X2),the_carrier(X0))
& relstr_set_smaller(X0,X1,sK1(X0,X1,X2))
& ~ related(X0,X2,sK1(X0,X1,X2)) )
| ~ relstr_set_smaller(X0,X1,X2)
| X2 = join_on_relstr(X0,X1) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X3,sK1(X0,X1,X2))],[f27]) ).
fof(f31,plain,
! [X0] :
( ~ rel_str(X0)
| ~ antisymmetric_relstr(X0)
| ! [X1] :
( ( ~ ex_sup_of_relstr_set(X0,X1)
| ? [X2] :
( ! [X3] :
( ~ element(X3,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X3)
| related(X0,X2,X3) )
& relstr_set_smaller(X0,X1,X2)
& element(X2,the_carrier(X0)) ) )
& ( ! [X2] :
( ? [X3] :
( element(X3,the_carrier(X0))
& relstr_set_smaller(X0,X1,X3)
& ~ related(X0,X2,X3) )
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0)) )
| ex_sup_of_relstr_set(X0,X1) ) ) ),
inference(nnf_transformation,[],[f20]) ).
fof(f32,plain,
! [X0] :
( ~ rel_str(X0)
| ~ antisymmetric_relstr(X0)
| ! [X1] :
( ( ~ ex_sup_of_relstr_set(X0,X1)
| ? [X4] :
( ! [X5] :
( ~ element(X5,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X5)
| related(X0,X4,X5) )
& relstr_set_smaller(X0,X1,X4)
& element(X4,the_carrier(X0)) ) )
& ( ! [X2] :
( ? [X3] :
( element(X3,the_carrier(X0))
& relstr_set_smaller(X0,X1,X3)
& ~ related(X0,X2,X3) )
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0)) )
| ex_sup_of_relstr_set(X0,X1) ) ) ),
inference(rectify,[],[f31]) ).
fof(f33,plain,
! [X0] :
( ~ rel_str(X0)
| ~ antisymmetric_relstr(X0)
| ! [X1] :
( ( ~ ex_sup_of_relstr_set(X0,X1)
| ( ! [X5] :
( ~ element(X5,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X5)
| related(X0,sK5(X0,X1),X5) )
& relstr_set_smaller(X0,X1,sK5(X0,X1))
& element(sK5(X0,X1),the_carrier(X0)) ) )
& ( ! [X2] :
( ( element(sK4(X0,X1,X2),the_carrier(X0))
& relstr_set_smaller(X0,X1,sK4(X0,X1,X2))
& ~ related(X0,X2,sK4(X0,X1,X2)) )
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0)) )
| ex_sup_of_relstr_set(X0,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X3,sK4(X0,X1,X2)),skolemize(X4,sK5(X0,X1))],[f32]) ).
fof(f37,plain,
? [X0] :
( rel_str(X0)
& antisymmetric_relstr(X0)
& ? [X1] :
( element(X1,the_carrier(X0))
& ? [X2] :
( ( ! [X3] :
( ~ element(X3,the_carrier(X0))
| ~ relstr_set_smaller(X0,X2,X3)
| related(X0,X1,X3) )
& relstr_set_smaller(X0,X2,X1)
& ( ~ ex_sup_of_relstr_set(X0,X2)
| join_on_relstr(X0,X2) != X1 ) )
| sP0(X1,X2,X0) ) ) ),
inference(rectify,[],[f24]) ).
fof(f38,plain,
( rel_str(sK7)
& antisymmetric_relstr(sK7)
& element(sK8,the_carrier(sK7))
& ( ( ! [X3] :
( ~ element(X3,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,sK9,X3)
| related(sK7,sK8,X3) )
& relstr_set_smaller(sK7,sK9,sK8)
& ( ~ ex_sup_of_relstr_set(sK7,sK9)
| sK8 != join_on_relstr(sK7,sK9) ) )
| sP0(sK8,sK9,sK7) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8,sK9]),skolemize(X0,sK7),skolemize(X1,sK8),skolemize(X2,sK9)],[f37]) ).
fof(f39,plain,
! [X2,X0,X1,X4] :
( ~ rel_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| join_on_relstr(X0,X1) != X2
| ~ element(X4,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X4)
| related(X0,X2,X4) ),
inference(cnf_transformation,[],[f28]) ).
fof(f40,plain,
! [X2,X0,X1] :
( ~ rel_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| join_on_relstr(X0,X1) != X2
| relstr_set_smaller(X0,X1,X2) ),
inference(cnf_transformation,[],[f28]) ).
fof(f41,plain,
! [X2,X0,X1] :
( ~ rel_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| element(sK1(X0,X1,X2),the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| join_on_relstr(X0,X1) = X2 ),
inference(cnf_transformation,[],[f28]) ).
fof(f42,plain,
! [X2,X0,X1] :
( ~ rel_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| relstr_set_smaller(X0,X1,sK1(X0,X1,X2))
| ~ relstr_set_smaller(X0,X1,X2)
| join_on_relstr(X0,X1) = X2 ),
inference(cnf_transformation,[],[f28]) ).
fof(f43,plain,
! [X2,X0,X1] :
( ~ rel_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ related(X0,X2,sK1(X0,X1,X2))
| ~ relstr_set_smaller(X0,X1,X2)
| join_on_relstr(X0,X1) = X2 ),
inference(cnf_transformation,[],[f28]) ).
fof(f44,plain,
! [X0,X1] :
( ~ rel_str(X0)
| element(join_on_relstr(X0,X1),the_carrier(X0)) ),
inference(cnf_transformation,[],[f18]) ).
fof(f50,plain,
! [X2,X0,X1] :
( ~ rel_str(X0)
| ~ antisymmetric_relstr(X0)
| element(sK4(X0,X1,X2),the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f51,plain,
! [X2,X0,X1] :
( ~ rel_str(X0)
| ~ antisymmetric_relstr(X0)
| relstr_set_smaller(X0,X1,sK4(X0,X1,X2))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f52,plain,
! [X2,X0,X1] :
( ~ rel_str(X0)
| ~ antisymmetric_relstr(X0)
| ~ related(X0,X2,sK4(X0,X1,X2))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ex_sup_of_relstr_set(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f58,plain,
rel_str(sK7),
inference(cnf_transformation,[],[f38]) ).
fof(f59,plain,
antisymmetric_relstr(sK7),
inference(cnf_transformation,[],[f38]) ).
fof(f60,plain,
element(sK8,the_carrier(sK7)),
inference(cnf_transformation,[],[f38]) ).
fof(f61,plain,
! [X3] :
( ~ element(X3,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,sK9,X3)
| related(sK7,sK8,X3)
| sP0(sK8,sK9,sK7) ),
inference(cnf_transformation,[],[f38]) ).
fof(f62,plain,
( relstr_set_smaller(sK7,sK9,sK8)
| sP0(sK8,sK9,sK7) ),
inference(cnf_transformation,[],[f38]) ).
fof(f63,plain,
( ~ ex_sup_of_relstr_set(sK7,sK9)
| sK8 != join_on_relstr(sK7,sK9)
| sP0(sK8,sK9,sK7) ),
inference(cnf_transformation,[],[f38]) ).
fof(f64,plain,
! [X0,X1] :
( ~ rel_str(X0)
| ~ element(join_on_relstr(X0,X1),the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| relstr_set_smaller(X0,X1,join_on_relstr(X0,X1)) ),
inference(equality_resolution,[],[f40]) ).
fof(f65,plain,
! [X0,X1,X4] :
( ~ rel_str(X0)
| ~ element(join_on_relstr(X0,X1),the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X4,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X4)
| related(X0,join_on_relstr(X0,X1),X4) ),
inference(equality_resolution,[],[f39]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( join_on_relstr(X0,X2) = X1 )
| ~ rel_str(X0)
| ~ ex_sup_of_relstr_set(X0,X2)
| ~ element(X1,the_carrier(X0))
| ~ relstr_set_smaller(X0,X2,X1)
| ~ related(X0,X1,sK1(X0,X2,X1)) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] :
( relstr_set_smaller(X0,X1,sK1(X0,X1,X2))
| ( join_on_relstr(X0,X1) = X2 )
| ~ rel_str(X0)
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i] :
( element(sK1(X0,X1,X2),the_carrier(X0))
| ( join_on_relstr(X0,X1) = X2 )
| ~ rel_str(X0)
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i] :
( relstr_set_smaller(X0,X1,join_on_relstr(X0,X1))
| ~ rel_str(X0)
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(join_on_relstr(X0,X1),the_carrier(X0)) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i] :
( related(X0,join_on_relstr(X0,X1),X2)
| ~ rel_str(X0)
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(join_on_relstr(X0,X1),the_carrier(X0)) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( element(join_on_relstr(X0,X1),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i] :
( ex_sup_of_relstr_set(X0,X2)
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ relstr_set_smaller(X0,X2,X1)
| ~ related(X0,X1,sK4(X0,X2,X1)) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i] :
( ex_sup_of_relstr_set(X0,X1)
| relstr_set_smaller(X0,X1,sK4(X0,X1,X2))
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i,X2: $i] :
( ex_sup_of_relstr_set(X0,X1)
| element(sK4(X0,X1,X2),the_carrier(X0))
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_68,negated_conjecture,
( sP0(sK8,sK9,sK7)
| ~ ex_sup_of_relstr_set(sK7,sK9)
| ( join_on_relstr(sK7,sK9) != sK8 ) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_69,negated_conjecture,
( sP0(sK8,sK9,sK7)
| relstr_set_smaller(sK7,sK9,sK8) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_70,negated_conjecture,
! [X0: $i] :
( sP0(sK8,sK9,sK7)
| related(sK7,sK8,X0)
| ~ element(X0,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,sK9,X0) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_71,negated_conjecture,
element(sK8,the_carrier(sK7)),
inference(cnf_transformation,[],[f60]) ).
tcf(c_72,negated_conjecture,
antisymmetric_relstr(sK7),
inference(cnf_transformation,[],[f59]) ).
tcf(c_73,negated_conjecture,
rel_str(sK7),
inference(cnf_transformation,[],[f58]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i] :
( relstr_set_smaller(X0,X1,join_on_relstr(X0,X1))
| ~ rel_str(X0)
| ~ ex_sup_of_relstr_set(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_52,c_54,c_52]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i] :
( related(X0,join_on_relstr(X0,X1),X2)
| ~ rel_str(X0)
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2) ),
inference(global_subsumption_just,[status(thm)],[c_53,c_54,c_53]) ).
tcf(c_489,plain,
! [X0: $i,X1: $i,X2: $i] :
( ex_sup_of_relstr_set(X0,X1)
| element(sK4(X0,X1,X2),the_carrier(X0))
| ~ rel_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_72]) ).
tcf(c_490,plain,
! [X0: $i,X1: $i] :
( ex_sup_of_relstr_set(sK7,X0)
| element(sK4(sK7,X0,X1),the_carrier(sK7))
| ~ rel_str(sK7)
| ~ element(X1,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,X0,X1) ),
inference(unflattening,[status(thm)],[c_489]) ).
tcf(c_492,plain,
! [X0: $i,X1: $i] :
( ex_sup_of_relstr_set(sK7,X0)
| element(sK4(sK7,X0,X1),the_carrier(sK7))
| ~ relstr_set_smaller(sK7,X0,X1)
| ~ element(X1,the_carrier(sK7)) ),
inference(global_subsumption_just,[status(thm)],[c_490,c_73,c_490]) ).
tcf(c_493,plain,
! [X0: $i,X1: $i] :
( ex_sup_of_relstr_set(sK7,X0)
| element(sK4(sK7,X0,X1),the_carrier(sK7))
| ~ element(X1,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,X0,X1) ),
inference(renaming,[status(thm)],[c_492]) ).
tcf(c_507,plain,
! [X0: $i,X1: $i,X2: $i] :
( ex_sup_of_relstr_set(X0,X1)
| relstr_set_smaller(X0,X1,sK4(X0,X1,X2))
| ~ rel_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_72]) ).
tcf(c_508,plain,
! [X0: $i,X1: $i] :
( ex_sup_of_relstr_set(sK7,X0)
| relstr_set_smaller(sK7,X0,sK4(sK7,X0,X1))
| ~ rel_str(sK7)
| ~ element(X1,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,X0,X1) ),
inference(unflattening,[status(thm)],[c_507]) ).
tcf(c_510,plain,
! [X0: $i,X1: $i] :
( ex_sup_of_relstr_set(sK7,X0)
| relstr_set_smaller(sK7,X0,sK4(sK7,X0,X1))
| ~ relstr_set_smaller(sK7,X0,X1)
| ~ element(X1,the_carrier(sK7)) ),
inference(global_subsumption_just,[status(thm)],[c_508,c_73,c_508]) ).
tcf(c_511,plain,
! [X0: $i,X1: $i] :
( ex_sup_of_relstr_set(sK7,X0)
| relstr_set_smaller(sK7,X0,sK4(sK7,X0,X1))
| ~ element(X1,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,X0,X1) ),
inference(renaming,[status(thm)],[c_510]) ).
tcf(c_525,plain,
! [X0: $i,X1: $i,X2: $i] :
( ex_sup_of_relstr_set(X0,X2)
| ~ rel_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ relstr_set_smaller(X0,X2,X1)
| ~ related(X0,X1,sK4(X0,X2,X1))
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_72]) ).
tcf(c_526,plain,
! [X0: $i,X1: $i] :
( ex_sup_of_relstr_set(sK7,X1)
| ~ rel_str(sK7)
| ~ element(X0,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,X1,X0)
| ~ related(sK7,X0,sK4(sK7,X1,X0)) ),
inference(unflattening,[status(thm)],[c_525]) ).
tcf(c_528,plain,
! [X0: $i,X1: $i] :
( ex_sup_of_relstr_set(sK7,X1)
| ~ related(sK7,X0,sK4(sK7,X1,X0))
| ~ relstr_set_smaller(sK7,X1,X0)
| ~ element(X0,the_carrier(sK7)) ),
inference(global_subsumption_just,[status(thm)],[c_526,c_73,c_526]) ).
tcf(c_529,plain,
! [X0: $i,X1: $i] :
( ex_sup_of_relstr_set(sK7,X1)
| ~ element(X0,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,X1,X0)
| ~ related(sK7,X0,sK4(sK7,X1,X0)) ),
inference(renaming,[status(thm)],[c_528]) ).
tcf(c_647,plain,
! [X0: $i,X1: $i,X2: $i] :
( related(X0,join_on_relstr(X0,X1),X2)
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_96,c_73]) ).
tcf(c_648,plain,
! [X0: $i,X1: $i] :
( related(sK7,join_on_relstr(sK7,X0),X1)
| ~ ex_sup_of_relstr_set(sK7,X0)
| ~ element(X1,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,X0,X1) ),
inference(unflattening,[status(thm)],[c_647]) ).
tcf(c_662,plain,
! [X0: $i,X1: $i] :
( relstr_set_smaller(X0,X1,join_on_relstr(X0,X1))
| ~ ex_sup_of_relstr_set(X0,X1)
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_93,c_73]) ).
tcf(c_663,plain,
! [X0: $i] :
( relstr_set_smaller(sK7,X0,join_on_relstr(sK7,X0))
| ~ ex_sup_of_relstr_set(sK7,X0) ),
inference(unflattening,[status(thm)],[c_662]) ).
tcf(c_677,plain,
! [X0: $i,X1: $i,X2: $i] :
( element(sK1(X0,X1,X2),the_carrier(X0))
| ( join_on_relstr(X0,X1) = X2 )
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_51,c_73]) ).
tcf(c_678,plain,
! [X0: $i,X1: $i] :
( element(sK1(sK7,X0,X1),the_carrier(sK7))
| ( join_on_relstr(sK7,X0) = X1 )
| ~ ex_sup_of_relstr_set(sK7,X0)
| ~ element(X1,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,X0,X1) ),
inference(unflattening,[status(thm)],[c_677]) ).
tcf(c_695,plain,
! [X0: $i,X1: $i,X2: $i] :
( relstr_set_smaller(X0,X1,sK1(X0,X1,X2))
| ( join_on_relstr(X0,X1) = X2 )
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_73]) ).
tcf(c_696,plain,
! [X0: $i,X1: $i] :
( relstr_set_smaller(sK7,X0,sK1(sK7,X0,X1))
| ( join_on_relstr(sK7,X0) = X1 )
| ~ ex_sup_of_relstr_set(sK7,X0)
| ~ element(X1,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,X0,X1) ),
inference(unflattening,[status(thm)],[c_695]) ).
tcf(c_713,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( join_on_relstr(X0,X2) = X1 )
| ~ ex_sup_of_relstr_set(X0,X2)
| ~ element(X1,the_carrier(X0))
| ~ relstr_set_smaller(X0,X2,X1)
| ~ related(X0,X1,sK1(X0,X2,X1))
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_73]) ).
tcf(c_714,plain,
! [X0: $i,X1: $i] :
( ( join_on_relstr(sK7,X1) = X0 )
| ~ ex_sup_of_relstr_set(sK7,X1)
| ~ element(X0,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,X1,X0)
| ~ related(sK7,X0,sK1(sK7,X1,X0)) ),
inference(unflattening,[status(thm)],[c_713]) ).
tcf(c_2926,definition,
iPr_def_11 = join_on_relstr(sK7,sK9),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_2927,definition,
iPr_def_12 = sK6(sK8,sK9,sK7),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_2942,plain,
! [X0: $i,X1: $i] :
( ( join_on_relstr(sK7,X1) = X0 )
| ~ element(X0,iPr_def_13)
| ~ ex_sup_of_relstr_set(sK7,X1)
| ~ relstr_set_smaller(sK7,X1,X0)
| ~ related(sK7,X0,sK1(sK7,X1,X0)) ),
inference(demodulation,[status(thm)],[c_714]) ).
tcf(c_2943,plain,
! [X0: $i,X1: $i] :
( relstr_set_smaller(sK7,X0,sK1(sK7,X0,X1))
| ( join_on_relstr(sK7,X0) = X1 )
| ~ element(X1,iPr_def_13)
| ~ ex_sup_of_relstr_set(sK7,X0)
| ~ relstr_set_smaller(sK7,X0,X1) ),
inference(demodulation,[status(thm)],[c_696]) ).
tcf(c_2944,plain,
! [X0: $i,X1: $i] :
( element(sK1(sK7,X0,X1),iPr_def_13)
| ( join_on_relstr(sK7,X0) = X1 )
| ~ element(X1,iPr_def_13)
| ~ ex_sup_of_relstr_set(sK7,X0)
| ~ relstr_set_smaller(sK7,X0,X1) ),
inference(demodulation,[status(thm)],[c_678]) ).
tcf(c_2946,plain,
! [X0: $i] :
( relstr_set_smaller(sK7,X0,join_on_relstr(sK7,X0))
| ~ ex_sup_of_relstr_set(sK7,X0) ),
inference(demodulation,[status(thm)],[c_663]) ).
tcf(c_2947,plain,
! [X0: $i,X1: $i] :
( related(sK7,join_on_relstr(sK7,X0),X1)
| ~ element(X1,iPr_def_13)
| ~ ex_sup_of_relstr_set(sK7,X0)
| ~ relstr_set_smaller(sK7,X0,X1) ),
inference(demodulation,[status(thm)],[c_648]) ).
tcf(c_2948,plain,
! [X0: $i,X1: $i] :
( ex_sup_of_relstr_set(sK7,X1)
| ~ element(X0,iPr_def_13)
| ~ relstr_set_smaller(sK7,X1,X0)
| ~ related(sK7,X0,sK4(sK7,X1,X0)) ),
inference(demodulation,[status(thm)],[c_529]) ).
tcf(c_2949,plain,
! [X0: $i,X1: $i] :
( ex_sup_of_relstr_set(sK7,X0)
| relstr_set_smaller(sK7,X0,sK4(sK7,X0,X1))
| ~ element(X1,iPr_def_13)
| ~ relstr_set_smaller(sK7,X0,X1) ),
inference(demodulation,[status(thm)],[c_511]) ).
tcf(c_2950,plain,
! [X0: $i,X1: $i] :
( ex_sup_of_relstr_set(sK7,X0)
| element(sK4(sK7,X0,X1),iPr_def_13)
| ~ element(X1,iPr_def_13)
| ~ relstr_set_smaller(sK7,X0,X1) ),
inference(demodulation,[status(thm)],[c_493]) ).
tcf(c_2954,negated_conjecture,
element(sK8,iPr_def_13),
inference(demodulation,[status(thm)],[c_71]) ).
tcf(c_3605,plain,
( relstr_set_smaller(sK7,sK9,iPr_def_11)
| ~ ex_sup_of_relstr_set(sK7,sK9) ),
inference(superposition,[status(thm)],[c_2926,c_2946]) ).
tcf(c_3830,plain,
! [X0: $i] :
( related(sK7,iPr_def_11,X0)
| ~ ex_sup_of_relstr_set(sK7,sK9)
| ~ element(X0,iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,X0) ),
inference(superposition,[status(thm)],[c_2926,c_2947]) ).
fof(f23,definition,
! [X1,X2,X0] :
( ~ sP0(X1,X2,X0)
| ( ex_sup_of_relstr_set(X0,X2)
& X1 = join_on_relstr(X0,X2)
& ( ? [X3] :
( element(X3,the_carrier(X0))
& relstr_set_smaller(X0,X2,X3)
& ~ related(X0,X1,X3) )
| ~ relstr_set_smaller(X0,X2,X1) ) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f24,plain,
? [X0] :
( rel_str(X0)
& antisymmetric_relstr(X0)
& ? [X1] :
( element(X1,the_carrier(X0))
& ? [X2] :
( ( ! [X4] :
( ~ element(X4,the_carrier(X0))
| ~ relstr_set_smaller(X0,X2,X4)
| related(X0,X1,X4) )
& relstr_set_smaller(X0,X2,X1)
& ( ~ ex_sup_of_relstr_set(X0,X2)
| join_on_relstr(X0,X2) != X1 ) )
| sP0(X1,X2,X0) ) ) ),
inference(definition_folding,[],[f22,f23]) ).
fof(f34,plain,
! [X1,X2,X0] :
( ~ sP0(X1,X2,X0)
| ( ex_sup_of_relstr_set(X0,X2)
& X1 = join_on_relstr(X0,X2)
& ( ? [X3] :
( element(X3,the_carrier(X0))
& relstr_set_smaller(X0,X2,X3)
& ~ related(X0,X1,X3) )
| ~ relstr_set_smaller(X0,X2,X1) ) ) ),
inference(nnf_transformation,[],[f23]) ).
fof(f35,plain,
! [X0,X1,X2] :
( ~ sP0(X0,X1,X2)
| ( ex_sup_of_relstr_set(X2,X1)
& join_on_relstr(X2,X1) = X0
& ( ? [X3] :
( element(X3,the_carrier(X2))
& relstr_set_smaller(X2,X1,X3)
& ~ related(X2,X0,X3) )
| ~ relstr_set_smaller(X2,X1,X0) ) ) ),
inference(rectify,[],[f34]) ).
fof(f36,plain,
! [X0,X1,X2] :
( ~ sP0(X0,X1,X2)
| ( ex_sup_of_relstr_set(X2,X1)
& join_on_relstr(X2,X1) = X0
& ( ( element(sK6(X0,X1,X2),the_carrier(X2))
& relstr_set_smaller(X2,X1,sK6(X0,X1,X2))
& ~ related(X2,X0,sK6(X0,X1,X2)) )
| ~ relstr_set_smaller(X2,X1,X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X3,sK6(X0,X1,X2))],[f35]) ).
fof(f53,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| ex_sup_of_relstr_set(X2,X1) ),
inference(cnf_transformation,[],[f36]) ).
fof(f54,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| join_on_relstr(X2,X1) = X0 ),
inference(cnf_transformation,[],[f36]) ).
fof(f55,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| element(sK6(X0,X1,X2),the_carrier(X2))
| ~ relstr_set_smaller(X2,X1,X0) ),
inference(cnf_transformation,[],[f36]) ).
fof(f56,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| relstr_set_smaller(X2,X1,sK6(X0,X1,X2))
| ~ relstr_set_smaller(X2,X1,X0) ),
inference(cnf_transformation,[],[f36]) ).
fof(f57,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| ~ related(X2,X0,sK6(X0,X1,X2))
| ~ relstr_set_smaller(X2,X1,X0) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ sP0(X1,X2,X0)
| ~ relstr_set_smaller(X0,X2,X1)
| ~ related(X0,X1,sK6(X1,X2,X0)) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i] :
( relstr_set_smaller(X0,X1,sK6(X2,X1,X0))
| ~ sP0(X2,X1,X0)
| ~ relstr_set_smaller(X0,X1,X2) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] :
( element(sK6(X2,X1,X0),the_carrier(X0))
| ~ sP0(X2,X1,X0)
| ~ relstr_set_smaller(X0,X1,X2) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( join_on_relstr(X2,X1) = X0 )
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i] :
( ex_sup_of_relstr_set(X2,X1)
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_775,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ex_sup_of_relstr_set(X2,X1)
| related(sK7,sK8,X3)
| ~ element(X3,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,sK9,X3)
| ( X2 != sK7 )
| ( X1 != sK9 )
| ( X0 != sK8 ) ),
inference(resolution_lifted,[status(thm)],[c_67,c_70]) ).
tcf(c_776,plain,
! [X0: $i] :
( ex_sup_of_relstr_set(sK7,sK9)
| related(sK7,sK8,X0)
| ~ element(X0,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,sK9,X0) ),
inference(unflattening,[status(thm)],[c_775]) ).
tcf(c_790,plain,
! [X0: $i,X1: $i,X2: $i] :
( ex_sup_of_relstr_set(X2,X1)
| relstr_set_smaller(sK7,sK9,sK8)
| ( X2 != sK7 )
| ( X1 != sK9 )
| ( X0 != sK8 ) ),
inference(resolution_lifted,[status(thm)],[c_67,c_69]) ).
tcf(c_791,plain,
( ex_sup_of_relstr_set(sK7,sK9)
| relstr_set_smaller(sK7,sK9,sK8) ),
inference(unflattening,[status(thm)],[c_790]) ).
tcf(c_800,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( related(sK7,sK8,X3)
| ( join_on_relstr(X2,X1) = X0 )
| ~ element(X3,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,sK9,X3)
| ( X2 != sK7 )
| ( X1 != sK9 )
| ( X0 != sK8 ) ),
inference(resolution_lifted,[status(thm)],[c_66,c_70]) ).
tcf(c_801,plain,
! [X0: $i] :
( related(sK7,sK8,X0)
| ( join_on_relstr(sK7,sK9) = sK8 )
| ~ element(X0,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,sK9,X0) ),
inference(unflattening,[status(thm)],[c_800]) ).
tcf(c_815,plain,
! [X0: $i,X1: $i,X2: $i] :
( relstr_set_smaller(sK7,sK9,sK8)
| ( join_on_relstr(X2,X1) = X0 )
| ( X2 != sK7 )
| ( X1 != sK9 )
| ( X0 != sK8 ) ),
inference(resolution_lifted,[status(thm)],[c_66,c_69]) ).
tcf(c_816,plain,
( relstr_set_smaller(sK7,sK9,sK8)
| ( join_on_relstr(sK7,sK9) = sK8 ) ),
inference(unflattening,[status(thm)],[c_815]) ).
tcf(c_825,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( related(sK7,sK8,X3)
| ~ element(X3,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,sK9,X3)
| ~ relstr_set_smaller(X0,X2,X1)
| ~ related(X0,X1,sK6(X1,X2,X0))
| ( X2 != sK9 )
| ( X1 != sK8 )
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_70]) ).
tcf(c_826,plain,
! [X0: $i] :
( related(sK7,sK8,X0)
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ~ element(X0,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,sK9,X0)
| ~ related(sK7,sK8,sK6(sK8,sK9,sK7)) ),
inference(unflattening,[status(thm)],[c_825]) ).
tcf(c_845,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ex_sup_of_relstr_set(sK7,sK9)
| ~ relstr_set_smaller(X0,X2,X1)
| ~ related(X0,X1,sK6(X1,X2,X0))
| ( X2 != sK9 )
| ( X1 != sK8 )
| ( X0 != sK7 )
| ( join_on_relstr(sK7,sK9) != sK8 ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_68]) ).
tcf(c_846,plain,
( ~ ex_sup_of_relstr_set(sK7,sK9)
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ~ related(sK7,sK8,sK6(sK8,sK9,sK7))
| ( join_on_relstr(sK7,sK9) != sK8 ) ),
inference(unflattening,[status(thm)],[c_845]) ).
tcf(c_859,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( related(sK7,sK8,X3)
| element(sK6(X2,X1,X0),the_carrier(X0))
| ~ element(X3,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,sK9,X3)
| ~ relstr_set_smaller(X0,X1,X2)
| ( X2 != sK8 )
| ( X1 != sK9 )
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_65,c_70]) ).
tcf(c_860,plain,
! [X0: $i] :
( related(sK7,sK8,X0)
| element(sK6(sK8,sK9,sK7),the_carrier(sK7))
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ~ element(X0,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,sK9,X0) ),
inference(unflattening,[status(thm)],[c_859]) ).
tcf(c_879,plain,
! [X0: $i,X1: $i,X2: $i] :
( element(sK6(X2,X1,X0),the_carrier(X0))
| ~ ex_sup_of_relstr_set(sK7,sK9)
| ~ relstr_set_smaller(X0,X1,X2)
| ( X2 != sK8 )
| ( X1 != sK9 )
| ( X0 != sK7 )
| ( join_on_relstr(sK7,sK9) != sK8 ) ),
inference(resolution_lifted,[status(thm)],[c_65,c_68]) ).
tcf(c_880,plain,
( element(sK6(sK8,sK9,sK7),the_carrier(sK7))
| ~ ex_sup_of_relstr_set(sK7,sK9)
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ( join_on_relstr(sK7,sK9) != sK8 ) ),
inference(unflattening,[status(thm)],[c_879]) ).
tcf(c_893,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( related(sK7,sK8,X3)
| relstr_set_smaller(X0,X1,sK6(X2,X1,X0))
| ~ element(X3,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,sK9,X3)
| ~ relstr_set_smaller(X0,X1,X2)
| ( X2 != sK8 )
| ( X1 != sK9 )
| ( X0 != sK7 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_70]) ).
tcf(c_894,plain,
! [X0: $i] :
( related(sK7,sK8,X0)
| relstr_set_smaller(sK7,sK9,sK6(sK8,sK9,sK7))
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ~ element(X0,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,sK9,X0) ),
inference(unflattening,[status(thm)],[c_893]) ).
tcf(c_913,plain,
! [X0: $i,X1: $i,X2: $i] :
( relstr_set_smaller(X0,X1,sK6(X2,X1,X0))
| ~ ex_sup_of_relstr_set(sK7,sK9)
| ~ relstr_set_smaller(X0,X1,X2)
| ( X2 != sK8 )
| ( X1 != sK9 )
| ( X0 != sK7 )
| ( join_on_relstr(sK7,sK9) != sK8 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_68]) ).
tcf(c_914,plain,
( relstr_set_smaller(sK7,sK9,sK6(sK8,sK9,sK7))
| ~ ex_sup_of_relstr_set(sK7,sK9)
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ( join_on_relstr(sK7,sK9) != sK8 ) ),
inference(unflattening,[status(thm)],[c_913]) ).
tcf(c_2922,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ element(X0,the_carrier(sK7))
| ~ relstr_set_smaller(sK7,sK9,X0)
| related(sK7,sK8,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_894]) ).
tcf(c_2923,plain,
( iPr_def_10
| relstr_set_smaller(sK7,sK9,sK6(sK8,sK9,sK7))
| ~ relstr_set_smaller(sK7,sK9,sK8) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_894]) ).
tcf(c_2924,plain,
( iPr_def_10
| element(sK6(sK8,sK9,sK7),the_carrier(sK7))
| ~ relstr_set_smaller(sK7,sK9,sK8) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_860]) ).
tcf(c_2925,plain,
( iPr_def_10
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ~ related(sK7,sK8,sK6(sK8,sK9,sK7)) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_826]) ).
tcf(c_2929,plain,
( relstr_set_smaller(sK7,sK9,iPr_def_12)
| ~ ex_sup_of_relstr_set(sK7,sK9)
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ( iPr_def_11 != sK8 ) ),
inference(demodulation,[status(thm)],[c_914,c_2927,c_2926]) ).
tcf(c_2930,plain,
( iPr_def_10
| relstr_set_smaller(sK7,sK9,iPr_def_12)
| ~ relstr_set_smaller(sK7,sK9,sK8) ),
inference(demodulation,[status(thm)],[c_2923]) ).
tcf(c_2932,plain,
( element(iPr_def_12,iPr_def_13)
| ~ ex_sup_of_relstr_set(sK7,sK9)
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ( iPr_def_11 != sK8 ) ),
inference(demodulation,[status(thm)],[c_880]) ).
tcf(c_2933,plain,
( iPr_def_10
| element(iPr_def_12,iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,sK8) ),
inference(demodulation,[status(thm)],[c_2924]) ).
tcf(c_2935,plain,
( ~ ex_sup_of_relstr_set(sK7,sK9)
| ~ related(sK7,sK8,iPr_def_12)
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ( iPr_def_11 != sK8 ) ),
inference(demodulation,[status(thm)],[c_846]) ).
tcf(c_2936,plain,
( iPr_def_10
| ~ related(sK7,sK8,iPr_def_12)
| ~ relstr_set_smaller(sK7,sK9,sK8) ),
inference(demodulation,[status(thm)],[c_2925]) ).
tcf(c_2937,plain,
! [X0: $i] :
( related(sK7,sK8,X0)
| ~ iPr_def_10
| ~ element(X0,iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,X0) ),
inference(demodulation,[status(thm)],[c_2922]) ).
tcf(c_2938,plain,
( relstr_set_smaller(sK7,sK9,sK8)
| ( iPr_def_11 = sK8 ) ),
inference(demodulation,[status(thm)],[c_816]) ).
tcf(c_2939,plain,
! [X0: $i] :
( related(sK7,sK8,X0)
| ( iPr_def_11 = sK8 )
| ~ element(X0,iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,X0) ),
inference(demodulation,[status(thm)],[c_801]) ).
tcf(c_2941,plain,
! [X0: $i] :
( ex_sup_of_relstr_set(sK7,sK9)
| related(sK7,sK8,X0)
| ~ element(X0,iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,X0) ),
inference(demodulation,[status(thm)],[c_776]) ).
tcf(c_3575,plain,
( iPr_def_10
| element(iPr_def_12,iPr_def_13)
| ( sK8 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_2938,c_2933]) ).
tcf(c_3593,plain,
( iPr_def_10
| relstr_set_smaller(sK7,sK9,iPr_def_12)
| ( sK8 = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_2938,c_2930]) ).
tcf(c_3637,plain,
( iPr_def_10
| ( sK8 = iPr_def_11 )
| ~ related(sK7,sK8,iPr_def_12) ),
inference(superposition,[status(thm)],[c_2938,c_2936]) ).
tcf(c_3787,plain,
( iPr_def_10
| related(sK7,sK8,iPr_def_12)
| ( sK8 = iPr_def_11 )
| ~ element(iPr_def_12,iPr_def_13) ),
inference(superposition,[status(thm)],[c_3593,c_2939]) ).
tcf(c_3800,plain,
( iPr_def_10
| ( sK8 = iPr_def_11 ) ),
inference(global_subsumption_just,[status(thm)],[c_3637,c_3575,c_3637,c_3787]) ).
tcf(c_3845,plain,
! [X0: $i] :
( ex_sup_of_relstr_set(sK7,sK9)
| related(sK7,sK8,sK4(sK7,sK9,X0))
| ~ element(X0,iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,X0)
| ~ element(sK4(sK7,sK9,X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_2949,c_2941]) ).
tcf(c_3919,plain,
! [X0: $i] :
( related(sK7,sK8,sK1(sK7,sK9,X0))
| ( join_on_relstr(sK7,sK9) = X0 )
| ~ iPr_def_10
| ~ ex_sup_of_relstr_set(sK7,sK9)
| ~ element(X0,iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,X0)
| ~ element(sK1(sK7,sK9,X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_2943,c_2937]) ).
tcf(c_3920,plain,
! [X0: $i] :
( related(sK7,sK8,sK1(sK7,sK9,X0))
| ( X0 = iPr_def_11 )
| ~ iPr_def_10
| ~ ex_sup_of_relstr_set(sK7,sK9)
| ~ element(X0,iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,X0)
| ~ element(sK1(sK7,sK9,X0),iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_3919,c_2926]) ).
tcf(c_4111,plain,
! [X0: $i] :
( ex_sup_of_relstr_set(sK7,sK9)
| related(sK7,sK8,sK4(sK7,sK9,X0))
| ~ element(X0,iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3845,c_2950]) ).
tcf(c_4124,plain,
( ex_sup_of_relstr_set(sK7,sK9)
| ~ element(sK8,iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,sK8) ),
inference(superposition,[status(thm)],[c_4111,c_2948]) ).
tcf(c_4125,plain,
( ex_sup_of_relstr_set(sK7,sK9)
| ~ relstr_set_smaller(sK7,sK9,sK8) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4124,c_2954]) ).
tcf(c_4128,plain,
ex_sup_of_relstr_set(sK7,sK9),
inference(global_subsumption_just,[status(thm)],[c_4125,c_791,c_4125]) ).
tcf(c_4135,plain,
! [X0: $i] :
( related(sK7,iPr_def_11,X0)
| ~ element(X0,iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3830,c_4128]) ).
tcf(c_4138,plain,
relstr_set_smaller(sK7,sK9,iPr_def_11),
inference(backward_subsumption_resolution,[status(thm)],[c_3605,c_4128]) ).
tcf(c_4139,plain,
( ~ related(sK7,sK8,iPr_def_12)
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ( sK8 != iPr_def_11 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2935,c_4128]) ).
tcf(c_4140,plain,
( element(iPr_def_12,iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ( sK8 != iPr_def_11 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2932,c_4128]) ).
tcf(c_4141,plain,
( relstr_set_smaller(sK7,sK9,iPr_def_12)
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ( sK8 != iPr_def_11 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2929,c_4128]) ).
tcf(c_4213,plain,
! [X0: $i] :
( related(sK7,sK8,sK1(sK7,sK9,X0))
| ( X0 = iPr_def_11 )
| ~ iPr_def_10
| ~ element(sK1(sK7,sK9,X0),iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,X0)
| ~ element(X0,iPr_def_13) ),
inference(global_subsumption_just,[status(thm)],[c_3920,c_791,c_3920,c_4125]) ).
tcf(c_4214,plain,
! [X0: $i] :
( related(sK7,sK8,sK1(sK7,sK9,X0))
| ( X0 = iPr_def_11 )
| ~ iPr_def_10
| ~ element(X0,iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,X0)
| ~ element(sK1(sK7,sK9,X0),iPr_def_13) ),
inference(renaming,[status(thm)],[c_4213]) ).
tcf(c_4228,plain,
( ( sK8 = iPr_def_11 )
| ( join_on_relstr(sK7,sK9) = sK8 )
| ~ iPr_def_10
| ~ element(sK8,iPr_def_13)
| ~ ex_sup_of_relstr_set(sK7,sK9)
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ~ element(sK1(sK7,sK9,sK8),iPr_def_13) ),
inference(superposition,[status(thm)],[c_4214,c_2942]) ).
tcf(c_4229,plain,
( ( sK8 = iPr_def_11 )
| ~ iPr_def_10
| ~ element(sK8,iPr_def_13)
| ~ ex_sup_of_relstr_set(sK7,sK9)
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ~ element(sK1(sK7,sK9,sK8),iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_4228,c_2926]) ).
tcf(c_4230,plain,
( ( sK8 = iPr_def_11 )
| ~ iPr_def_10
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ~ element(sK1(sK7,sK9,sK8),iPr_def_13) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4229,c_2954,c_4128]) ).
tcf(c_4241,plain,
( ( sK8 = iPr_def_11 )
| ~ element(sK1(sK7,sK9,sK8),iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,sK8) ),
inference(global_subsumption_just,[status(thm)],[c_4230,c_3800,c_4230]) ).
tcf(c_4242,plain,
( ( sK8 = iPr_def_11 )
| ~ relstr_set_smaller(sK7,sK9,sK8)
| ~ element(sK1(sK7,sK9,sK8),iPr_def_13) ),
inference(renaming,[status(thm)],[c_4241]) ).
tcf(c_4249,plain,
( ( sK8 = iPr_def_11 )
| ( join_on_relstr(sK7,sK9) = sK8 )
| ~ element(sK8,iPr_def_13)
| ~ ex_sup_of_relstr_set(sK7,sK9)
| ~ relstr_set_smaller(sK7,sK9,sK8) ),
inference(superposition,[status(thm)],[c_2944,c_4242]) ).
tcf(c_4250,plain,
( ( sK8 = iPr_def_11 )
| ~ element(sK8,iPr_def_13)
| ~ ex_sup_of_relstr_set(sK7,sK9)
| ~ relstr_set_smaller(sK7,sK9,sK8) ),
inference(light_normalisation,[status(thm)],[c_4249,c_2926]) ).
tcf(c_4251,plain,
( ( sK8 = iPr_def_11 )
| ~ relstr_set_smaller(sK7,sK9,sK8) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4250,c_2954,c_4128]) ).
tcf(c_4260,plain,
sK8 = iPr_def_11,
inference(superposition,[status(thm)],[c_2938,c_4251]) ).
tcf(c_4359,plain,
( element(iPr_def_12,iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,sK8) ),
inference(global_subsumption_just,[status(thm)],[c_4140,c_4140,c_4260]) ).
tcf(c_4361,plain,
( element(iPr_def_12,iPr_def_13)
| ~ relstr_set_smaller(sK7,sK9,iPr_def_11) ),
inference(light_normalisation,[status(thm)],[c_4359,c_4260]) ).
tcf(c_4362,plain,
element(iPr_def_12,iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_4361,c_4138]) ).
tcf(c_4363,plain,
( relstr_set_smaller(sK7,sK9,iPr_def_12)
| ~ relstr_set_smaller(sK7,sK9,sK8) ),
inference(global_subsumption_just,[status(thm)],[c_4141,c_4141,c_4260]) ).
tcf(c_4365,plain,
( relstr_set_smaller(sK7,sK9,iPr_def_12)
| ~ relstr_set_smaller(sK7,sK9,iPr_def_11) ),
inference(light_normalisation,[status(thm)],[c_4363,c_4260]) ).
tcf(c_4366,plain,
relstr_set_smaller(sK7,sK9,iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_4365,c_4138]) ).
tcf(c_4367,plain,
( related(sK7,iPr_def_11,iPr_def_12)
| ~ element(iPr_def_12,iPr_def_13) ),
inference(superposition,[status(thm)],[c_4366,c_4135]) ).
tcf(c_4368,plain,
related(sK7,iPr_def_11,iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_4367,c_4362]) ).
tcf(c_4369,plain,
( ~ related(sK7,sK8,iPr_def_12)
| ~ relstr_set_smaller(sK7,sK9,sK8) ),
inference(global_subsumption_just,[status(thm)],[c_4139,c_4139,c_4260]) ).
tcf(c_4371,plain,
( ~ related(sK7,iPr_def_11,iPr_def_12)
| ~ relstr_set_smaller(sK7,sK9,iPr_def_11) ),
inference(light_normalisation,[status(thm)],[c_4369,c_4260]) ).
tcf(c_4372,plain,
~ related(sK7,iPr_def_11,iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_4371,c_4138]) ).
tcf(c_4456,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_4368,c_4372]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU359+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.05/0.74 % Computer : n012.cluster.edu
% 0.05/0.74 % Model : x86_64 x86_64
% 0.05/0.74 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.74 % Memory : 8046.5625MB
% 0.05/0.74 % OS : Linux 6.8.0-71-generic
% 0.05/0.74 % CPULimit : 300
% 0.05/0.74 % WCLimit : 300
% 0.05/0.74 % DateTime : Thu Sep 24 13:49:22 UTC 2026
% 0.05/0.75 % CPUTime :
% 0.05/0.75 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.05/0.77 Running first-order theorem proving
% 0.05/0.77 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.05/0.77
% 0.05/0.77 % ======== iProver multi-core TPTP/SMT =========
% 0.05/0.77
% 0.05/0.77 % Detected problem language: tptp
% 0.05/0.78 % Proving...
% 1.65/1.51 % SZS status Started for theBenchmark.p
% 1.65/1.51 % SZS status Theorem for theBenchmark.p
% 1.65/1.51
% 1.65/1.51 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.65/1.51
% 1.65/1.51 % ------ iProver source info
% 1.65/1.51
% 1.65/1.51 % git: date: 2026-07-19 20:42:38 +0200
% 1.65/1.51 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.65/1.51 % git: non_committed_changes: false
% 1.65/1.51
% 1.65/1.51 % ------ Parsing...
% 1.65/1.51 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 1.65/1.51
% 1.65/1.51 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe_e %
% 1.65/1.51
% 1.65/1.51 % ------ Preprocessing... gs_s sp: 3 0s gs_e snvd_s sp: 0 0s snvd_e %
% 1.65/1.51
% 1.65/1.51 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 1.65/1.51 % ------ Proving...
% 1.65/1.51 % ------ Problem Properties
% 1.65/1.51
% 1.65/1.51 %
% 1.65/1.51 % clauses 34
% 1.65/1.51 % conjectures 1
% 1.65/1.51 % EPR 12
% 1.65/1.51 % Horn 22
% 1.65/1.51 % unary 7
% 1.65/1.51 % binary 6
% 1.65/1.51 % lits 106
% 1.65/1.51 % lits eq 14
% 1.65/1.51 % fd_pure 0
% 1.65/1.51 % fd_pseudo 0
% 1.65/1.51 % fd_cond 0
% 1.65/1.51 % fd_pseudo_cond 6
% 1.65/1.51 % AC symbols 0
% 1.65/1.51
% 1.65/1.51 % ------ Schedule dynamic 5 is on
% 1.65/1.51
% 1.65/1.51 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 1.65/1.51
% 1.65/1.51
% 1.65/1.51 % ------
% 1.65/1.51 % Current options:
% 1.65/1.51 % ------
% 1.65/1.51
% 1.65/1.51
% 1.65/1.51 %
% 1.65/1.51
% 1.65/1.51 % ------ Proving...
% 1.65/1.51 %
% 1.65/1.51
% 1.65/1.51 % SZS status Theorem for theBenchmark.p
% 1.65/1.51
% 1.65/1.51 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.65/1.51
% 1.65/1.51
%------------------------------------------------------------------------------