%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU244+2 : 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 : n026.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:56:20 PM UTC 2026
% Result : Theorem 3.27s 1.73s
% Output : CNFRefutation 3.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 9
% Syntax : Number of formulae : 210 ( 9 unt; 0 def)
% Number of atoms : 805 ( 62 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 1043 ( 448 ~; 511 |; 54 &)
% ( 18 <=>; 11 =>; 0 <=; 1 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 16 ( 14 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 1 con; 0-2 aty)
% Number of variables : 164 ( 0 sgn 159 !; 5 ?; 91 :)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [X0] :
( relation(X0)
=> ( antisymmetric(X0)
<=> is_antisymmetric_in(X0,relation_field(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d12_relat_2) ).
fof(f22,axiom,
! [X0] :
( relation(X0)
=> ( connected(X0)
<=> is_connected_in(X0,relation_field(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d14_relat_2) ).
fof(f23,axiom,
! [X0] :
( relation(X0)
=> ( transitive(X0)
<=> is_transitive_in(X0,relation_field(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d16_relat_2) ).
fof(f50,axiom,
! [X0] :
( relation(X0)
=> ( well_ordering(X0)
<=> ( well_founded_relation(X0)
& connected(X0)
& antisymmetric(X0)
& transitive(X0)
& reflexive(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_wellord1) ).
fof(f56,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( well_orders(X0,X1)
<=> ( is_well_founded_in(X0,X1)
& is_connected_in(X0,X1)
& is_antisymmetric_in(X0,X1)
& is_transitive_in(X0,X1)
& is_reflexive_in(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_wellord1) ).
fof(f68,axiom,
! [X0] :
( relation(X0)
=> ( reflexive(X0)
<=> is_reflexive_in(X0,relation_field(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_relat_2) ).
fof(f138,axiom,
! [X0] :
( relation(X0)
=> ( reflexive(X0)
<=> ! [X1] :
( in(X1,relation_field(X0))
=> in(ordered_pair(X1,X1),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1_wellord1) ).
fof(f266,axiom,
! [X0] :
( relation(X0)
=> ( well_founded_relation(X0)
<=> is_well_founded_in(X0,relation_field(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_wellord1) ).
fof(f290,conjecture,
! [X0] :
( relation(X0)
=> ( well_orders(X0,relation_field(X0))
<=> well_ordering(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_wellord1) ).
fof(f291,negated_conjecture,
~ ! [X0] :
( relation(X0)
=> ( well_orders(X0,relation_field(X0))
<=> well_ordering(X0) ) ),
inference(negated_conjecture,[status(cth)],[f290]) ).
fof(f330,plain,
! [X0] :
( ~ relation(X0)
| ( antisymmetric(X0)
<=> is_antisymmetric_in(X0,relation_field(X0)) ) ),
inference(ennf_transformation,[],[f18]) ).
fof(f335,plain,
! [X0] :
( ~ relation(X0)
| ( connected(X0)
<=> is_connected_in(X0,relation_field(X0)) ) ),
inference(ennf_transformation,[],[f22]) ).
fof(f336,plain,
! [X0] :
( ~ relation(X0)
| ( transitive(X0)
<=> is_transitive_in(X0,relation_field(X0)) ) ),
inference(ennf_transformation,[],[f23]) ).
fof(f354,plain,
! [X0] :
( ~ relation(X0)
| ( well_ordering(X0)
<=> ( well_founded_relation(X0)
& connected(X0)
& antisymmetric(X0)
& transitive(X0)
& reflexive(X0) ) ) ),
inference(ennf_transformation,[],[f50]) ).
fof(f359,plain,
! [X0] :
( ~ relation(X0)
| ! [X1] :
( well_orders(X0,X1)
<=> ( is_well_founded_in(X0,X1)
& is_connected_in(X0,X1)
& is_antisymmetric_in(X0,X1)
& is_transitive_in(X0,X1)
& is_reflexive_in(X0,X1) ) ) ),
inference(ennf_transformation,[],[f56]) ).
fof(f373,plain,
! [X0] :
( ~ relation(X0)
| ( reflexive(X0)
<=> is_reflexive_in(X0,relation_field(X0)) ) ),
inference(ennf_transformation,[],[f68]) ).
fof(f421,plain,
! [X0] :
( ~ relation(X0)
| ( reflexive(X0)
<=> ! [X1] :
( ~ in(X1,relation_field(X0))
| in(ordered_pair(X1,X1),X0) ) ) ),
inference(ennf_transformation,[],[f138]) ).
fof(f553,plain,
! [X0] :
( ~ relation(X0)
| ( well_founded_relation(X0)
<=> is_well_founded_in(X0,relation_field(X0)) ) ),
inference(ennf_transformation,[],[f266]) ).
fof(f578,plain,
? [X0] :
( relation(X0)
& ( well_orders(X0,relation_field(X0))
<~> well_ordering(X0) ) ),
inference(ennf_transformation,[],[f291]) ).
fof(f608,plain,
! [X0] :
( ~ relation(X0)
| ( ( ~ antisymmetric(X0)
| is_antisymmetric_in(X0,relation_field(X0)) )
& ( ~ is_antisymmetric_in(X0,relation_field(X0))
| antisymmetric(X0) ) ) ),
inference(nnf_transformation,[],[f330]) ).
fof(f619,plain,
! [X0] :
( ~ relation(X0)
| ( ( ~ connected(X0)
| is_connected_in(X0,relation_field(X0)) )
& ( ~ is_connected_in(X0,relation_field(X0))
| connected(X0) ) ) ),
inference(nnf_transformation,[],[f335]) ).
fof(f620,plain,
! [X0] :
( ~ relation(X0)
| ( ( ~ transitive(X0)
| is_transitive_in(X0,relation_field(X0)) )
& ( ~ is_transitive_in(X0,relation_field(X0))
| transitive(X0) ) ) ),
inference(nnf_transformation,[],[f336]) ).
fof(f692,plain,
! [X0] :
( ~ relation(X0)
| ( ( ~ well_ordering(X0)
| ( well_founded_relation(X0)
& connected(X0)
& antisymmetric(X0)
& transitive(X0)
& reflexive(X0) ) )
& ( ~ well_founded_relation(X0)
| ~ connected(X0)
| ~ antisymmetric(X0)
| ~ transitive(X0)
| ~ reflexive(X0)
| well_ordering(X0) ) ) ),
inference(nnf_transformation,[],[f354]) ).
fof(f693,plain,
! [X0] :
( ~ relation(X0)
| ( ( ~ well_ordering(X0)
| ( well_founded_relation(X0)
& connected(X0)
& antisymmetric(X0)
& transitive(X0)
& reflexive(X0) ) )
& ( ~ well_founded_relation(X0)
| ~ connected(X0)
| ~ antisymmetric(X0)
| ~ transitive(X0)
| ~ reflexive(X0)
| well_ordering(X0) ) ) ),
inference(flattening,[],[f692]) ).
fof(f704,plain,
! [X0] :
( ~ relation(X0)
| ! [X1] :
( ( ~ well_orders(X0,X1)
| ( is_well_founded_in(X0,X1)
& is_connected_in(X0,X1)
& is_antisymmetric_in(X0,X1)
& is_transitive_in(X0,X1)
& is_reflexive_in(X0,X1) ) )
& ( ~ is_well_founded_in(X0,X1)
| ~ is_connected_in(X0,X1)
| ~ is_antisymmetric_in(X0,X1)
| ~ is_transitive_in(X0,X1)
| ~ is_reflexive_in(X0,X1)
| well_orders(X0,X1) ) ) ),
inference(nnf_transformation,[],[f359]) ).
fof(f705,plain,
! [X0] :
( ~ relation(X0)
| ! [X1] :
( ( ~ well_orders(X0,X1)
| ( is_well_founded_in(X0,X1)
& is_connected_in(X0,X1)
& is_antisymmetric_in(X0,X1)
& is_transitive_in(X0,X1)
& is_reflexive_in(X0,X1) ) )
& ( ~ is_well_founded_in(X0,X1)
| ~ is_connected_in(X0,X1)
| ~ is_antisymmetric_in(X0,X1)
| ~ is_transitive_in(X0,X1)
| ~ is_reflexive_in(X0,X1)
| well_orders(X0,X1) ) ) ),
inference(flattening,[],[f704]) ).
fof(f727,plain,
! [X0] :
( ~ relation(X0)
| ( ( ~ reflexive(X0)
| is_reflexive_in(X0,relation_field(X0)) )
& ( ~ is_reflexive_in(X0,relation_field(X0))
| reflexive(X0) ) ) ),
inference(nnf_transformation,[],[f373]) ).
fof(f729,plain,
! [X0] :
( ~ relation(X0)
| ( ( ~ reflexive(X0)
| ! [X1] :
( ~ in(X1,relation_field(X0))
| in(ordered_pair(X1,X1),X0) ) )
& ( ? [X1] :
( in(X1,relation_field(X0))
& ~ in(ordered_pair(X1,X1),X0) )
| reflexive(X0) ) ) ),
inference(nnf_transformation,[],[f421]) ).
fof(f730,plain,
! [X0] :
( ~ relation(X0)
| ( ( ~ reflexive(X0)
| ! [X2] :
( ~ in(X2,relation_field(X0))
| in(ordered_pair(X2,X2),X0) ) )
& ( ? [X1] :
( in(X1,relation_field(X0))
& ~ in(ordered_pair(X1,X1),X0) )
| reflexive(X0) ) ) ),
inference(rectify,[],[f729]) ).
fof(f731,plain,
! [X0] :
( ~ relation(X0)
| ( ( ~ reflexive(X0)
| ! [X2] :
( ~ in(X2,relation_field(X0))
| in(ordered_pair(X2,X2),X0) ) )
& ( ( in(sK78(X0),relation_field(X0))
& ~ in(ordered_pair(sK78(X0),sK78(X0)),X0) )
| reflexive(X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK78]),skolemize(X1,sK78(X0))],[f730]) ).
fof(f809,plain,
! [X0] :
( ~ relation(X0)
| ( ( ~ well_founded_relation(X0)
| is_well_founded_in(X0,relation_field(X0)) )
& ( ~ is_well_founded_in(X0,relation_field(X0))
| well_founded_relation(X0) ) ) ),
inference(nnf_transformation,[],[f553]) ).
fof(f824,plain,
? [X0] :
( relation(X0)
& ( well_orders(X0,relation_field(X0))
| well_ordering(X0) )
& ( ~ well_orders(X0,relation_field(X0))
| ~ well_ordering(X0) ) ),
inference(nnf_transformation,[],[f578]) ).
fof(f825,plain,
? [X0] :
( relation(X0)
& ( well_orders(X0,relation_field(X0))
| well_ordering(X0) )
& ( ~ well_orders(X0,relation_field(X0))
| ~ well_ordering(X0) ) ),
inference(flattening,[],[f824]) ).
fof(f826,plain,
( relation(sK118)
& ( well_orders(sK118,relation_field(sK118))
| well_ordering(sK118) )
& ( ~ well_orders(sK118,relation_field(sK118))
| ~ well_ordering(sK118) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK118]),skolemize(X0,sK118)],[f825]) ).
fof(f874,plain,
! [X0] :
( ~ relation(X0)
| ~ antisymmetric(X0)
| is_antisymmetric_in(X0,relation_field(X0)) ),
inference(cnf_transformation,[],[f608]) ).
fof(f875,plain,
! [X0] :
( ~ relation(X0)
| ~ is_antisymmetric_in(X0,relation_field(X0))
| antisymmetric(X0) ),
inference(cnf_transformation,[],[f608]) ).
fof(f894,plain,
! [X0] :
( ~ relation(X0)
| ~ connected(X0)
| is_connected_in(X0,relation_field(X0)) ),
inference(cnf_transformation,[],[f619]) ).
fof(f895,plain,
! [X0] :
( ~ relation(X0)
| ~ is_connected_in(X0,relation_field(X0))
| connected(X0) ),
inference(cnf_transformation,[],[f619]) ).
fof(f896,plain,
! [X0] :
( ~ relation(X0)
| ~ transitive(X0)
| is_transitive_in(X0,relation_field(X0)) ),
inference(cnf_transformation,[],[f620]) ).
fof(f897,plain,
! [X0] :
( ~ relation(X0)
| ~ is_transitive_in(X0,relation_field(X0))
| transitive(X0) ),
inference(cnf_transformation,[],[f620]) ).
fof(f1014,plain,
! [X0] :
( ~ relation(X0)
| ~ well_ordering(X0)
| well_founded_relation(X0) ),
inference(cnf_transformation,[],[f693]) ).
fof(f1015,plain,
! [X0] :
( ~ relation(X0)
| ~ well_ordering(X0)
| connected(X0) ),
inference(cnf_transformation,[],[f693]) ).
fof(f1016,plain,
! [X0] :
( ~ relation(X0)
| ~ well_ordering(X0)
| antisymmetric(X0) ),
inference(cnf_transformation,[],[f693]) ).
fof(f1017,plain,
! [X0] :
( ~ relation(X0)
| ~ well_ordering(X0)
| transitive(X0) ),
inference(cnf_transformation,[],[f693]) ).
fof(f1018,plain,
! [X0] :
( ~ relation(X0)
| ~ well_ordering(X0)
| reflexive(X0) ),
inference(cnf_transformation,[],[f693]) ).
fof(f1019,plain,
! [X0] :
( ~ relation(X0)
| ~ well_founded_relation(X0)
| ~ connected(X0)
| ~ antisymmetric(X0)
| ~ transitive(X0)
| ~ reflexive(X0)
| well_ordering(X0) ),
inference(cnf_transformation,[],[f693]) ).
fof(f1038,plain,
! [X0,X1] :
( ~ relation(X0)
| ~ well_orders(X0,X1)
| is_well_founded_in(X0,X1) ),
inference(cnf_transformation,[],[f705]) ).
fof(f1039,plain,
! [X0,X1] :
( ~ relation(X0)
| ~ well_orders(X0,X1)
| is_connected_in(X0,X1) ),
inference(cnf_transformation,[],[f705]) ).
fof(f1040,plain,
! [X0,X1] :
( ~ relation(X0)
| ~ well_orders(X0,X1)
| is_antisymmetric_in(X0,X1) ),
inference(cnf_transformation,[],[f705]) ).
fof(f1041,plain,
! [X0,X1] :
( ~ relation(X0)
| ~ well_orders(X0,X1)
| is_transitive_in(X0,X1) ),
inference(cnf_transformation,[],[f705]) ).
fof(f1042,plain,
! [X0,X1] :
( ~ relation(X0)
| ~ well_orders(X0,X1)
| is_reflexive_in(X0,X1) ),
inference(cnf_transformation,[],[f705]) ).
fof(f1043,plain,
! [X0,X1] :
( ~ relation(X0)
| ~ is_well_founded_in(X0,X1)
| ~ is_connected_in(X0,X1)
| ~ is_antisymmetric_in(X0,X1)
| ~ is_transitive_in(X0,X1)
| ~ is_reflexive_in(X0,X1)
| well_orders(X0,X1) ),
inference(cnf_transformation,[],[f705]) ).
fof(f1084,plain,
! [X0] :
( ~ relation(X0)
| ~ reflexive(X0)
| is_reflexive_in(X0,relation_field(X0)) ),
inference(cnf_transformation,[],[f727]) ).
fof(f1085,plain,
! [X0] :
( ~ relation(X0)
| ~ is_reflexive_in(X0,relation_field(X0))
| reflexive(X0) ),
inference(cnf_transformation,[],[f727]) ).
fof(f1161,plain,
! [X0] :
( ~ relation(X0)
| in(sK78(X0),relation_field(X0))
| reflexive(X0) ),
inference(cnf_transformation,[],[f731]) ).
fof(f1391,plain,
! [X0] :
( ~ relation(X0)
| ~ well_founded_relation(X0)
| is_well_founded_in(X0,relation_field(X0)) ),
inference(cnf_transformation,[],[f809]) ).
fof(f1392,plain,
! [X0] :
( ~ relation(X0)
| ~ is_well_founded_in(X0,relation_field(X0))
| well_founded_relation(X0) ),
inference(cnf_transformation,[],[f809]) ).
fof(f1432,plain,
relation(sK118),
inference(cnf_transformation,[],[f826]) ).
fof(f1433,plain,
( well_orders(sK118,relation_field(sK118))
| well_ordering(sK118) ),
inference(cnf_transformation,[],[f826]) ).
fof(f1434,plain,
( ~ well_orders(sK118,relation_field(sK118))
| ~ well_ordering(sK118) ),
inference(cnf_transformation,[],[f826]) ).
tcf(c_93,plain,
! [X0: $i] :
( antisymmetric(X0)
| ~ relation(X0)
| ~ is_antisymmetric_in(X0,relation_field(X0)) ),
inference(cnf_transformation,[],[f875]) ).
tcf(c_94,plain,
! [X0: $i] :
( is_antisymmetric_in(X0,relation_field(X0))
| ~ antisymmetric(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f874]) ).
tcf(c_113,plain,
! [X0: $i] :
( connected(X0)
| ~ relation(X0)
| ~ is_connected_in(X0,relation_field(X0)) ),
inference(cnf_transformation,[],[f895]) ).
tcf(c_114,plain,
! [X0: $i] :
( is_connected_in(X0,relation_field(X0))
| ~ connected(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f894]) ).
tcf(c_115,plain,
! [X0: $i] :
( transitive(X0)
| ~ relation(X0)
| ~ is_transitive_in(X0,relation_field(X0)) ),
inference(cnf_transformation,[],[f897]) ).
tcf(c_116,plain,
! [X0: $i] :
( is_transitive_in(X0,relation_field(X0))
| ~ transitive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f896]) ).
tcf(c_232,plain,
! [X0: $i] :
( well_ordering(X0)
| ~ reflexive(X0)
| ~ well_founded_relation(X0)
| ~ transitive(X0)
| ~ connected(X0)
| ~ antisymmetric(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f1019]) ).
tcf(c_233,plain,
! [X0: $i] :
( reflexive(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f1018]) ).
tcf(c_234,plain,
! [X0: $i] :
( transitive(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f1017]) ).
tcf(c_235,plain,
! [X0: $i] :
( antisymmetric(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f1016]) ).
tcf(c_236,plain,
! [X0: $i] :
( connected(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f1015]) ).
tcf(c_237,plain,
! [X0: $i] :
( well_founded_relation(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f1014]) ).
tcf(c_255,plain,
! [X0: $i,X1: $i] :
( well_orders(X0,X1)
| ~ relation(X0)
| ~ is_well_founded_in(X0,X1)
| ~ is_reflexive_in(X0,X1)
| ~ is_transitive_in(X0,X1)
| ~ is_connected_in(X0,X1)
| ~ is_antisymmetric_in(X0,X1) ),
inference(cnf_transformation,[],[f1043]) ).
tcf(c_256,plain,
! [X0: $i,X1: $i] :
( is_reflexive_in(X0,X1)
| ~ relation(X0)
| ~ well_orders(X0,X1) ),
inference(cnf_transformation,[],[f1042]) ).
tcf(c_257,plain,
! [X0: $i,X1: $i] :
( is_transitive_in(X0,X1)
| ~ relation(X0)
| ~ well_orders(X0,X1) ),
inference(cnf_transformation,[],[f1041]) ).
tcf(c_258,plain,
! [X0: $i,X1: $i] :
( is_antisymmetric_in(X0,X1)
| ~ relation(X0)
| ~ well_orders(X0,X1) ),
inference(cnf_transformation,[],[f1040]) ).
tcf(c_259,plain,
! [X0: $i,X1: $i] :
( is_connected_in(X0,X1)
| ~ relation(X0)
| ~ well_orders(X0,X1) ),
inference(cnf_transformation,[],[f1039]) ).
tcf(c_260,plain,
! [X0: $i,X1: $i] :
( is_well_founded_in(X0,X1)
| ~ relation(X0)
| ~ well_orders(X0,X1) ),
inference(cnf_transformation,[],[f1038]) ).
tcf(c_301,plain,
! [X0: $i] :
( reflexive(X0)
| ~ relation(X0)
| ~ is_reflexive_in(X0,relation_field(X0)) ),
inference(cnf_transformation,[],[f1085]) ).
tcf(c_302,plain,
! [X0: $i] :
( is_reflexive_in(X0,relation_field(X0))
| ~ reflexive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f1084]) ).
tcf(c_378,plain,
! [X0: $i] :
( reflexive(X0)
| in(sK78(X0),relation_field(X0))
| ~ relation(X0) ),
inference(cnf_transformation,[],[f1161]) ).
tcf(c_607,plain,
! [X0: $i] :
( well_founded_relation(X0)
| ~ relation(X0)
| ~ is_well_founded_in(X0,relation_field(X0)) ),
inference(cnf_transformation,[],[f1392]) ).
tcf(c_608,plain,
! [X0: $i] :
( is_well_founded_in(X0,relation_field(X0))
| ~ well_founded_relation(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f1391]) ).
tcf(c_647,negated_conjecture,
( ~ well_ordering(sK118)
| ~ well_orders(sK118,relation_field(sK118)) ),
inference(cnf_transformation,[],[f1434]) ).
tcf(c_648,negated_conjecture,
( well_ordering(sK118)
| well_orders(sK118,relation_field(sK118)) ),
inference(cnf_transformation,[],[f1433]) ).
tcf(c_649,negated_conjecture,
relation(sK118),
inference(cnf_transformation,[],[f1432]) ).
tcf(c_1110,plain,
( ~ well_orders(sK118,relation_field(sK118))
| ~ well_ordering(sK118) ),
inference(prop_impl_just,[status(thm)],[c_647]) ).
tcf(c_1111,plain,
( ~ well_ordering(sK118)
| ~ well_orders(sK118,relation_field(sK118)) ),
inference(renaming,[status(thm)],[c_1110]) ).
tcf(c_1112,plain,
( well_orders(sK118,relation_field(sK118))
| well_ordering(sK118) ),
inference(prop_impl_just,[status(thm)],[c_648]) ).
tcf(c_1113,plain,
( well_ordering(sK118)
| well_orders(sK118,relation_field(sK118)) ),
inference(renaming,[status(thm)],[c_1112]) ).
tcf(c_9290,plain,
! [X0: $i] :
( ~ reflexive(X0)
| ~ well_founded_relation(X0)
| ~ transitive(X0)
| ~ connected(X0)
| ~ antisymmetric(X0)
| ~ relation(X0)
| ~ well_orders(sK118,relation_field(sK118))
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_232,c_1111]) ).
tcf(c_9291,plain,
( ~ reflexive(sK118)
| ~ well_founded_relation(sK118)
| ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118)
| ~ relation(sK118)
| ~ well_orders(sK118,relation_field(sK118)) ),
inference(unflattening,[status(thm)],[c_9290]) ).
tcf(c_9292,plain,
( ~ reflexive(sK118)
| ~ well_founded_relation(sK118)
| ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118)
| ~ well_orders(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_9291,c_649,c_9291]) ).
tcf(c_9312,plain,
! [X0: $i] :
( well_founded_relation(X0)
| well_orders(sK118,relation_field(sK118))
| ~ relation(X0)
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_237,c_1113]) ).
tcf(c_9313,plain,
( well_founded_relation(sK118)
| well_orders(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_9312]) ).
tcf(c_9314,plain,
( well_founded_relation(sK118)
| well_orders(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_9313,c_649,c_9313]) ).
tcf(c_9322,plain,
! [X0: $i] :
( connected(X0)
| well_orders(sK118,relation_field(sK118))
| ~ relation(X0)
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_236,c_1113]) ).
tcf(c_9323,plain,
( connected(sK118)
| well_orders(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_9322]) ).
tcf(c_9324,plain,
( connected(sK118)
| well_orders(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_9323,c_649,c_9323]) ).
tcf(c_9332,plain,
! [X0: $i] :
( antisymmetric(X0)
| well_orders(sK118,relation_field(sK118))
| ~ relation(X0)
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_235,c_1113]) ).
tcf(c_9333,plain,
( antisymmetric(sK118)
| well_orders(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_9332]) ).
tcf(c_9334,plain,
( antisymmetric(sK118)
| well_orders(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_9333,c_649,c_9333]) ).
tcf(c_9342,plain,
! [X0: $i] :
( transitive(X0)
| well_orders(sK118,relation_field(sK118))
| ~ relation(X0)
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_234,c_1113]) ).
tcf(c_9343,plain,
( transitive(sK118)
| well_orders(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_9342]) ).
tcf(c_9344,plain,
( transitive(sK118)
| well_orders(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_9343,c_649,c_9343]) ).
tcf(c_9352,plain,
! [X0: $i] :
( reflexive(X0)
| well_orders(sK118,relation_field(sK118))
| ~ relation(X0)
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_233,c_1113]) ).
tcf(c_9353,plain,
( reflexive(sK118)
| well_orders(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_9352]) ).
tcf(c_9354,plain,
( reflexive(sK118)
| well_orders(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_9353,c_649,c_9353]) ).
tcf(c_9497,plain,
! [X0: $i] :
( ~ well_founded_relation(sK118)
| ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118)
| ~ relation(X0)
| ~ well_orders(sK118,relation_field(sK118))
| ~ is_reflexive_in(X0,relation_field(X0))
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_301,c_9292]) ).
tcf(c_9498,plain,
( ~ well_founded_relation(sK118)
| ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118)
| ~ relation(sK118)
| ~ well_orders(sK118,relation_field(sK118))
| ~ is_reflexive_in(sK118,relation_field(sK118)) ),
inference(unflattening,[status(thm)],[c_9497]) ).
tcf(c_9519,plain,
! [X0: $i] :
( well_orders(sK118,relation_field(sK118))
| is_reflexive_in(X0,relation_field(X0))
| ~ relation(X0)
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_302,c_9354]) ).
tcf(c_9520,plain,
( well_orders(sK118,relation_field(sK118))
| is_reflexive_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_9519]) ).
tcf(c_9521,plain,
( well_orders(sK118,relation_field(sK118))
| is_reflexive_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_9520,c_649,c_9520]) ).
tcf(c_9963,plain,
! [X0: $i] :
( well_orders(sK118,relation_field(sK118))
| is_antisymmetric_in(X0,relation_field(X0))
| ~ relation(X0)
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_94,c_9334]) ).
tcf(c_9964,plain,
( well_orders(sK118,relation_field(sK118))
| is_antisymmetric_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_9963]) ).
tcf(c_9965,plain,
( well_orders(sK118,relation_field(sK118))
| is_antisymmetric_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_9964,c_649,c_9964]) ).
tcf(c_10245,plain,
! [X0: $i] :
( well_orders(sK118,relation_field(sK118))
| is_transitive_in(X0,relation_field(X0))
| ~ relation(X0)
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_116,c_9344]) ).
tcf(c_10246,plain,
( well_orders(sK118,relation_field(sK118))
| is_transitive_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_10245]) ).
tcf(c_10247,plain,
( well_orders(sK118,relation_field(sK118))
| is_transitive_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_10246,c_649,c_10246]) ).
tcf(c_11253,plain,
! [X0: $i] :
( ~ reflexive(sK118)
| ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118)
| ~ relation(X0)
| ~ well_orders(sK118,relation_field(sK118))
| ~ is_well_founded_in(X0,relation_field(X0))
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_607,c_9292]) ).
tcf(c_11254,plain,
( ~ reflexive(sK118)
| ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118)
| ~ relation(sK118)
| ~ well_orders(sK118,relation_field(sK118))
| ~ is_well_founded_in(sK118,relation_field(sK118)) ),
inference(unflattening,[status(thm)],[c_11253]) ).
tcf(c_11255,plain,
( ~ reflexive(sK118)
| ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118)
| ~ is_well_founded_in(sK118,relation_field(sK118))
| ~ well_orders(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_11254,c_649,c_11254]) ).
tcf(c_11256,plain,
( ~ reflexive(sK118)
| ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118)
| ~ well_orders(sK118,relation_field(sK118))
| ~ is_well_founded_in(sK118,relation_field(sK118)) ),
inference(renaming,[status(thm)],[c_11255]) ).
tcf(c_11346,plain,
! [X0: $i] :
( well_orders(sK118,relation_field(sK118))
| is_well_founded_in(X0,relation_field(X0))
| ~ relation(X0)
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_608,c_9314]) ).
tcf(c_11347,plain,
( well_orders(sK118,relation_field(sK118))
| is_well_founded_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_11346]) ).
tcf(c_12211,plain,
! [X0: $i] :
( well_orders(sK118,relation_field(sK118))
| is_connected_in(X0,relation_field(X0))
| ~ relation(X0)
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_114,c_9324]) ).
tcf(c_12212,plain,
( well_orders(sK118,relation_field(sK118))
| is_connected_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_12211]) ).
tcf(c_12213,plain,
( well_orders(sK118,relation_field(sK118))
| is_connected_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_12212,c_649,c_12212]) ).
tcf(c_13536,plain,
! [X0: $i,X1: $i] :
( ~ reflexive(sK118)
| ~ well_founded_relation(sK118)
| ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118)
| ~ relation(X0)
| ~ is_well_founded_in(X0,X1)
| ~ is_reflexive_in(X0,X1)
| ~ is_transitive_in(X0,X1)
| ~ is_connected_in(X0,X1)
| ~ is_antisymmetric_in(X0,X1)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_255,c_9292]) ).
tcf(c_13537,plain,
( ~ reflexive(sK118)
| ~ well_founded_relation(sK118)
| ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118)
| ~ relation(sK118)
| ~ is_well_founded_in(sK118,relation_field(sK118))
| ~ is_reflexive_in(sK118,relation_field(sK118))
| ~ is_transitive_in(sK118,relation_field(sK118))
| ~ is_connected_in(sK118,relation_field(sK118))
| ~ is_antisymmetric_in(sK118,relation_field(sK118)) ),
inference(unflattening,[status(thm)],[c_13536]) ).
tcf(c_13538,plain,
( ~ reflexive(sK118)
| ~ well_founded_relation(sK118)
| ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118) ),
inference(global_subsumption_just,[status(thm)],[c_13537,c_649,c_9291,c_9520,c_9964,c_10246,c_11347,c_12212,c_13537]) ).
tcf(c_13555,plain,
! [X0: $i,X1: $i] :
( reflexive(sK118)
| is_well_founded_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_260,c_9354]) ).
tcf(c_13556,plain,
( reflexive(sK118)
| is_well_founded_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13555]) ).
tcf(c_13557,plain,
( reflexive(sK118)
| is_well_founded_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_13556,c_649,c_13556]) ).
tcf(c_13565,plain,
! [X0: $i,X1: $i] :
( transitive(sK118)
| is_well_founded_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_260,c_9344]) ).
tcf(c_13566,plain,
( transitive(sK118)
| is_well_founded_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13565]) ).
tcf(c_13567,plain,
( transitive(sK118)
| is_well_founded_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_13566,c_649,c_13566]) ).
tcf(c_13575,plain,
! [X0: $i,X1: $i] :
( antisymmetric(sK118)
| is_well_founded_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_260,c_9334]) ).
tcf(c_13576,plain,
( antisymmetric(sK118)
| is_well_founded_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13575]) ).
tcf(c_13577,plain,
( antisymmetric(sK118)
| is_well_founded_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_13576,c_649,c_13576]) ).
tcf(c_13585,plain,
! [X0: $i,X1: $i] :
( connected(sK118)
| is_well_founded_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_260,c_9324]) ).
tcf(c_13586,plain,
( connected(sK118)
| is_well_founded_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13585]) ).
tcf(c_13587,plain,
( connected(sK118)
| is_well_founded_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_13586,c_649,c_13586]) ).
tcf(c_13595,plain,
! [X0: $i,X1: $i] :
( well_founded_relation(sK118)
| is_well_founded_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_260,c_9314]) ).
tcf(c_13596,plain,
( well_founded_relation(sK118)
| is_well_founded_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13595]) ).
tcf(c_13597,plain,
is_well_founded_in(sK118,relation_field(sK118)),
inference(global_subsumption_just,[status(thm)],[c_13596,c_649,c_13538,c_13557,c_13567,c_13577,c_13587,c_13596]) ).
tcf(c_13602,plain,
! [X0: $i,X1: $i] :
( reflexive(sK118)
| is_connected_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_259,c_9354]) ).
tcf(c_13603,plain,
( reflexive(sK118)
| is_connected_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13602]) ).
tcf(c_13604,plain,
( reflexive(sK118)
| is_connected_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_13603,c_649,c_13603]) ).
tcf(c_13612,plain,
! [X0: $i,X1: $i] :
( transitive(sK118)
| is_connected_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_259,c_9344]) ).
tcf(c_13613,plain,
( transitive(sK118)
| is_connected_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13612]) ).
tcf(c_13614,plain,
( transitive(sK118)
| is_connected_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_13613,c_649,c_13613]) ).
tcf(c_13622,plain,
! [X0: $i,X1: $i] :
( antisymmetric(sK118)
| is_connected_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_259,c_9334]) ).
tcf(c_13623,plain,
( antisymmetric(sK118)
| is_connected_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13622]) ).
tcf(c_13624,plain,
( antisymmetric(sK118)
| is_connected_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_13623,c_649,c_13623]) ).
tcf(c_13632,plain,
! [X0: $i,X1: $i] :
( connected(sK118)
| is_connected_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_259,c_9324]) ).
tcf(c_13633,plain,
( connected(sK118)
| is_connected_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13632]) ).
tcf(c_13634,plain,
is_connected_in(sK118,relation_field(sK118)),
inference(global_subsumption_just,[status(thm)],[c_13633,c_649,c_11256,c_12213,c_13538,c_13557,c_13567,c_13577,c_13587,c_13596,c_13604,c_13614,c_13624,c_13633]) ).
tcf(c_13641,plain,
! [X0: $i,X1: $i] :
( reflexive(sK118)
| is_antisymmetric_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_258,c_9354]) ).
tcf(c_13642,plain,
( reflexive(sK118)
| is_antisymmetric_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13641]) ).
tcf(c_13643,plain,
( reflexive(sK118)
| is_antisymmetric_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_13642,c_649,c_13642]) ).
tcf(c_13651,plain,
! [X0: $i,X1: $i] :
( transitive(sK118)
| is_antisymmetric_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_258,c_9344]) ).
tcf(c_13652,plain,
( transitive(sK118)
| is_antisymmetric_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13651]) ).
tcf(c_13653,plain,
( transitive(sK118)
| is_antisymmetric_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_13652,c_649,c_13652]) ).
tcf(c_13661,plain,
! [X0: $i,X1: $i] :
( antisymmetric(sK118)
| is_antisymmetric_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_258,c_9334]) ).
tcf(c_13662,plain,
( antisymmetric(sK118)
| is_antisymmetric_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13661]) ).
tcf(c_13663,plain,
( antisymmetric(sK118)
| is_antisymmetric_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_13662,c_649,c_13662]) ).
tcf(c_13671,plain,
! [X0: $i,X1: $i] :
( connected(sK118)
| is_antisymmetric_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_258,c_9324]) ).
tcf(c_13672,plain,
( connected(sK118)
| is_antisymmetric_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13671]) ).
tcf(c_13673,plain,
is_antisymmetric_in(sK118,relation_field(sK118)),
inference(global_subsumption_just,[status(thm)],[c_13672,c_649,c_9965,c_11256,c_13538,c_13557,c_13567,c_13577,c_13587,c_13596,c_13643,c_13653,c_13663,c_13672]) ).
tcf(c_13680,plain,
! [X0: $i,X1: $i] :
( reflexive(sK118)
| is_transitive_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_257,c_9354]) ).
tcf(c_13681,plain,
( reflexive(sK118)
| is_transitive_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13680]) ).
tcf(c_13682,plain,
( reflexive(sK118)
| is_transitive_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_13681,c_649,c_13681]) ).
tcf(c_13690,plain,
! [X0: $i,X1: $i] :
( transitive(sK118)
| is_transitive_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_257,c_9344]) ).
tcf(c_13691,plain,
( transitive(sK118)
| is_transitive_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13690]) ).
tcf(c_13692,plain,
( transitive(sK118)
| is_transitive_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_13691,c_649,c_13691]) ).
tcf(c_13700,plain,
! [X0: $i,X1: $i] :
( antisymmetric(sK118)
| is_transitive_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_257,c_9334]) ).
tcf(c_13701,plain,
( antisymmetric(sK118)
| is_transitive_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13700]) ).
tcf(c_13702,plain,
( antisymmetric(sK118)
| is_transitive_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_13701,c_649,c_13701]) ).
tcf(c_13710,plain,
! [X0: $i,X1: $i] :
( connected(sK118)
| is_transitive_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_257,c_9324]) ).
tcf(c_13711,plain,
( connected(sK118)
| is_transitive_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13710]) ).
tcf(c_13712,plain,
is_transitive_in(sK118,relation_field(sK118)),
inference(global_subsumption_just,[status(thm)],[c_13711,c_649,c_10247,c_11256,c_13538,c_13557,c_13567,c_13577,c_13587,c_13596,c_13682,c_13692,c_13702,c_13711]) ).
tcf(c_13719,plain,
! [X0: $i,X1: $i] :
( reflexive(sK118)
| is_reflexive_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_256,c_9354]) ).
tcf(c_13720,plain,
( reflexive(sK118)
| is_reflexive_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13719]) ).
tcf(c_13721,plain,
( reflexive(sK118)
| is_reflexive_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_13720,c_649,c_13720]) ).
tcf(c_13729,plain,
! [X0: $i,X1: $i] :
( transitive(sK118)
| is_reflexive_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_256,c_9344]) ).
tcf(c_13730,plain,
( transitive(sK118)
| is_reflexive_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13729]) ).
tcf(c_13731,plain,
( transitive(sK118)
| is_reflexive_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_13730,c_649,c_13730]) ).
tcf(c_13739,plain,
! [X0: $i,X1: $i] :
( antisymmetric(sK118)
| is_reflexive_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_256,c_9334]) ).
tcf(c_13740,plain,
( antisymmetric(sK118)
| is_reflexive_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13739]) ).
tcf(c_13741,plain,
( antisymmetric(sK118)
| is_reflexive_in(sK118,relation_field(sK118)) ),
inference(global_subsumption_just,[status(thm)],[c_13740,c_649,c_13740]) ).
tcf(c_13749,plain,
! [X0: $i,X1: $i] :
( connected(sK118)
| is_reflexive_in(X0,X1)
| ~ relation(X0)
| ( X0 != sK118 )
| ( relation_field(sK118) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_256,c_9324]) ).
tcf(c_13750,plain,
( connected(sK118)
| is_reflexive_in(sK118,relation_field(sK118))
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13749]) ).
tcf(c_13751,plain,
is_reflexive_in(sK118,relation_field(sK118)),
inference(global_subsumption_just,[status(thm)],[c_13750,c_649,c_9521,c_11256,c_13597,c_13721,c_13731,c_13741,c_13750]) ).
tcf(c_13916,plain,
! [X0: $i] :
( in(sK78(X0),relation_field(X0))
| ~ well_founded_relation(sK118)
| ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118)
| ~ relation(X0)
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_378,c_13538]) ).
tcf(c_13917,plain,
( in(sK78(sK118),relation_field(sK118))
| ~ well_founded_relation(sK118)
| ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118)
| ~ relation(sK118) ),
inference(unflattening,[status(thm)],[c_13916]) ).
tcf(c_13918,plain,
( ~ antisymmetric(sK118)
| ~ connected(sK118)
| ~ transitive(sK118)
| ~ well_founded_relation(sK118) ),
inference(global_subsumption_just,[status(thm)],[c_13917,c_649,c_9354,c_9498,c_13538,c_13751]) ).
tcf(c_13919,plain,
( ~ well_founded_relation(sK118)
| ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118) ),
inference(renaming,[status(thm)],[c_13918]) ).
tcf(c_15394,plain,
! [X0: $i] :
( ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118)
| ~ relation(X0)
| ~ is_well_founded_in(X0,relation_field(X0))
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_607,c_13919]) ).
tcf(c_15395,plain,
( ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118)
| ~ relation(sK118)
| ~ is_well_founded_in(sK118,relation_field(sK118)) ),
inference(unflattening,[status(thm)],[c_15394]) ).
tcf(c_15396,plain,
( ~ transitive(sK118)
| ~ connected(sK118)
| ~ antisymmetric(sK118) ),
inference(global_subsumption_just,[status(thm)],[c_15395,c_649,c_13597,c_15395]) ).
tcf(c_15793,plain,
! [X0: $i] :
( ~ connected(sK118)
| ~ antisymmetric(sK118)
| ~ relation(X0)
| ~ is_transitive_in(X0,relation_field(X0))
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_115,c_15396]) ).
tcf(c_15794,plain,
( ~ connected(sK118)
| ~ antisymmetric(sK118)
| ~ relation(sK118)
| ~ is_transitive_in(sK118,relation_field(sK118)) ),
inference(unflattening,[status(thm)],[c_15793]) ).
tcf(c_15795,plain,
( ~ connected(sK118)
| ~ antisymmetric(sK118) ),
inference(global_subsumption_just,[status(thm)],[c_15794,c_649,c_13712,c_15794]) ).
tcf(c_16592,plain,
! [X0: $i] :
( ~ antisymmetric(sK118)
| ~ relation(X0)
| ~ is_connected_in(X0,relation_field(X0))
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_113,c_15795]) ).
tcf(c_16593,plain,
( ~ antisymmetric(sK118)
| ~ relation(sK118)
| ~ is_connected_in(sK118,relation_field(sK118)) ),
inference(unflattening,[status(thm)],[c_16592]) ).
tcf(c_16594,plain,
~ antisymmetric(sK118),
inference(global_subsumption_just,[status(thm)],[c_16593,c_649,c_13634,c_16593]) ).
tcf(c_16774,plain,
! [X0: $i] :
( ~ relation(X0)
| ~ is_antisymmetric_in(X0,relation_field(X0))
| ( X0 != sK118 ) ),
inference(resolution_lifted,[status(thm)],[c_93,c_16594]) ).
tcf(c_16775,plain,
( ~ relation(sK118)
| ~ is_antisymmetric_in(sK118,relation_field(sK118)) ),
inference(unflattening,[status(thm)],[c_16774]) ).
tcf(c_16776,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_16775,c_13673,c_649]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU244+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.37 % Computer : n026.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Thu Sep 24 13:25:39 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 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.11/0.42
% 0.11/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.42
% 0.11/0.42 % Detected problem language: tptp
% 0.11/0.44 % Proving...
% 3.27/1.73 % SZS status Started for theBenchmark.p
% 3.27/1.73 % SZS status Theorem for theBenchmark.p
% 3.27/1.73
% 3.27/1.73 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.27/1.73
% 3.27/1.73 % ------ iProver source info
% 3.27/1.73
% 3.27/1.73 % git: date: 2026-07-19 20:42:38 +0200
% 3.27/1.73 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.27/1.73 % git: non_committed_changes: false
% 3.27/1.73
% 3.27/1.73 % ------ Parsing...
% 3.27/1.73 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.27/1.73
% 3.27/1.73 % ------ Preprocessing... sup_sim: 55 sf_s rm: 6 0s sf_e pe_s pe:1:0s pe:2:0s%
% 3.27/1.73
% 3.27/1.73 % SZS status Theorem for theBenchmark.p
% 3.27/1.73
% 3.27/1.73 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.27/1.73
% 3.27/1.73
%------------------------------------------------------------------------------