%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU244+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 : 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:51:29 PM UTC 2026
% Result : Theorem 1.66s 0.72s
% Output : Proof 1.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 8
% Syntax : Number of formulae : 109 ( 15 unt; 0 def)
% Number of atoms : 354 ( 0 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 417 ( 172 ~; 183 |; 44 &)
% ( 9 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 14 ( 13 usr; 1 prp; 0-2 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-1 aty)
% Number of variables : 61 ( 0 sgn 26 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [A] :
( relation(A)
=> ! [B] :
( well_orders(A,B)
<=> ( is_well_founded_in(A,B)
& is_connected_in(A,B)
& is_antisymmetric_in(A,B)
& is_transitive_in(A,B)
& is_reflexive_in(A,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_wellord1) ).
fof(f5_nnf,plain,
! [A] :
( ! [B] :
( ( ~ is_well_founded_in(A,B)
| ~ is_connected_in(A,B)
| ~ is_antisymmetric_in(A,B)
| ~ is_transitive_in(A,B)
| ~ is_reflexive_in(A,B)
| well_orders(A,B) )
& ( ( is_well_founded_in(A,B)
& is_connected_in(A,B)
& is_antisymmetric_in(A,B)
& is_transitive_in(A,B)
& is_reflexive_in(A,B) )
| ~ well_orders(A,B) ) )
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A,B] :
( ( ( ~ is_well_founded_in(A,B)
| ~ is_connected_in(A,B)
| ~ is_antisymmetric_in(A,B)
| ~ is_transitive_in(A,B)
| ~ is_reflexive_in(A,B)
| well_orders(A,B) )
& ( ( is_well_founded_in(A,B)
& is_connected_in(A,B)
& is_antisymmetric_in(A,B)
& is_transitive_in(A,B)
& is_reflexive_in(A,B) )
| ~ well_orders(A,B) ) )
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c18,plain,
( ~ 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)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
fof(f14,conjecture,
! [A] :
( relation(A)
=> ( well_orders(A,relation_field(A))
<=> well_ordering(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_wellord1) ).
fof(f14_neg,negated_conjecture,
~ ! [A] :
( relation(A)
=> ( well_orders(A,relation_field(A))
<=> well_ordering(A) ) ),
inference(negated_conjecture,[status(cth)],[f14]) ).
fof(f14_nnf,plain,
? [A] :
( ( ( well_ordering(A)
& ~ well_orders(A,relation_field(A)) )
| ( ~ well_ordering(A)
& well_orders(A,relation_field(A)) ) )
& relation(A) ),
inference(nnf_transformation,[status(thm)],[f14_neg]) ).
fof(f14_sk,plain,
( ( ( well_ordering(sk0)
& ~ well_orders(sk0,relation_field(sk0)) )
| ( ~ well_ordering(sk0)
& well_orders(sk0,relation_field(sk0)) ) )
& relation(sk0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f14_nnf]) ).
cnf(c29,plain,
relation(sk0),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p100,plain,
( ~ is_well_founded_in(sk0,X0)
| ~ is_connected_in(sk0,X0)
| ~ is_antisymmetric_in(sk0,X0)
| ~ is_transitive_in(sk0,X0)
| ~ is_reflexive_in(sk0,X0)
| well_orders(sk0,X0) ),
inference(resolution,[status(thm)],[c18,c29]) ).
fof(f4,axiom,
! [A] :
( relation(A)
=> ( well_ordering(A)
<=> ( well_founded_relation(A)
& connected(A)
& antisymmetric(A)
& transitive(A)
& reflexive(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_wellord1) ).
fof(f4_nnf,plain,
! [A] :
( ( ( ~ well_founded_relation(A)
| ~ connected(A)
| ~ antisymmetric(A)
| ~ transitive(A)
| ~ reflexive(A)
| well_ordering(A) )
& ( ( well_founded_relation(A)
& connected(A)
& antisymmetric(A)
& transitive(A)
& reflexive(A) )
| ~ well_ordering(A) ) )
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A] :
( ( ( ~ well_founded_relation(A)
| ~ connected(A)
| ~ antisymmetric(A)
| ~ transitive(A)
| ~ reflexive(A)
| well_ordering(A) )
& ( ( well_founded_relation(A)
& connected(A)
& antisymmetric(A)
& transitive(A)
& reflexive(A) )
| ~ well_ordering(A) ) )
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c12,plain,
( ~ well_founded_relation(X0)
| ~ connected(X0)
| ~ antisymmetric(X0)
| ~ transitive(X0)
| ~ reflexive(X0)
| well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p87,plain,
( ~ well_founded_relation(sk0)
| ~ connected(sk0)
| ~ antisymmetric(sk0)
| ~ transitive(sk0)
| ~ reflexive(sk0)
| well_ordering(sk0) ),
inference(resolution,[status(thm)],[c12,c29]) ).
fof(f7,axiom,
! [A] :
( relation(A)
=> ( reflexive(A)
<=> is_reflexive_in(A,relation_field(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_relat_2) ).
fof(f7_nnf,plain,
! [A] :
( ( ( ~ is_reflexive_in(A,relation_field(A))
| reflexive(A) )
& ( is_reflexive_in(A,relation_field(A))
| ~ reflexive(A) ) )
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A] :
( ( ( ~ is_reflexive_in(A,relation_field(A))
| reflexive(A) )
& ( is_reflexive_in(A,relation_field(A))
| ~ reflexive(A) ) )
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c21,plain,
( ~ is_reflexive_in(X0,relation_field(X0))
| reflexive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p80,plain,
( ~ is_reflexive_in(sk0,relation_field(sk0))
| reflexive(sk0) ),
inference(resolution,[status(thm)],[c21,c29]) ).
cnf(c13,plain,
( is_reflexive_in(X0,X1)
| ~ well_orders(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p45,plain,
( is_reflexive_in(sk0,X0)
| ~ well_orders(sk0,X0) ),
inference(resolution,[status(thm)],[c13,c29]) ).
cnf(c31,plain,
( well_ordering(sk0)
| well_orders(sk0,relation_field(sk0)) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p46,plain,
( well_ordering(sk0)
| is_reflexive_in(sk0,relation_field(sk0)) ),
inference(resolution,[status(thm)],[p45,c31]) ).
cnf(p81,plain,
( well_ordering(sk0)
| reflexive(sk0) ),
inference(resolution,[status(thm)],[p80,p46]) ).
cnf(p88,plain,
( well_ordering(sk0)
| ~ well_founded_relation(sk0)
| ~ connected(sk0)
| ~ antisymmetric(sk0)
| ~ transitive(sk0)
| well_ordering(sk0) ),
inference(resolution,[status(thm)],[p87,p81]) ).
cnf(p89,plain,
( ~ well_founded_relation(sk0)
| ~ connected(sk0)
| ~ antisymmetric(sk0)
| ~ transitive(sk0)
| well_ordering(sk0) ),
inference(factoring,[status(thm)],[p88]) ).
cnf(c14,plain,
( is_transitive_in(X0,X1)
| ~ well_orders(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p47,plain,
( is_transitive_in(sk0,X0)
| ~ well_orders(sk0,X0) ),
inference(resolution,[status(thm)],[c14,c29]) ).
cnf(p48,plain,
( well_ordering(sk0)
| is_transitive_in(sk0,relation_field(sk0)) ),
inference(resolution,[status(thm)],[p47,c31]) ).
fof(f3,axiom,
! [A] :
( relation(A)
=> ( transitive(A)
<=> is_transitive_in(A,relation_field(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d16_relat_2) ).
fof(f3_nnf,plain,
! [A] :
( ( ( ~ is_transitive_in(A,relation_field(A))
| transitive(A) )
& ( is_transitive_in(A,relation_field(A))
| ~ transitive(A) ) )
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A] :
( ( ( ~ is_transitive_in(A,relation_field(A))
| transitive(A) )
& ( is_transitive_in(A,relation_field(A))
| ~ transitive(A) ) )
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c6,plain,
( ~ is_transitive_in(X0,relation_field(X0))
| transitive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p44,plain,
( ~ is_transitive_in(sk0,relation_field(sk0))
| transitive(sk0) ),
inference(resolution,[status(thm)],[c6,c29]) ).
cnf(p49,plain,
( transitive(sk0)
| well_ordering(sk0) ),
inference(resolution,[status(thm)],[p48,p44]) ).
cnf(c8,plain,
( transitive(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p35,plain,
( transitive(sk0)
| ~ well_ordering(sk0) ),
inference(resolution,[status(thm)],[c8,c29]) ).
cnf(p52,plain,
( transitive(sk0)
| transitive(sk0) ),
inference(resolution,[status(thm)],[p49,p35]) ).
cnf(p56,plain,
transitive(sk0),
inference(factoring,[status(thm)],[p52]) ).
cnf(p90,plain,
( ~ well_founded_relation(sk0)
| ~ connected(sk0)
| ~ antisymmetric(sk0)
| well_ordering(sk0) ),
inference(resolution,[status(thm)],[p89,p56]) ).
cnf(c15,plain,
( is_antisymmetric_in(X0,X1)
| ~ well_orders(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p58,plain,
( is_antisymmetric_in(sk0,X0)
| ~ well_orders(sk0,X0) ),
inference(resolution,[status(thm)],[c15,c29]) ).
cnf(p59,plain,
( well_ordering(sk0)
| is_antisymmetric_in(sk0,relation_field(sk0)) ),
inference(resolution,[status(thm)],[p58,c31]) ).
fof(f1,axiom,
! [A] :
( relation(A)
=> ( antisymmetric(A)
<=> is_antisymmetric_in(A,relation_field(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d12_relat_2) ).
fof(f1_nnf,plain,
! [A] :
( ( ( ~ is_antisymmetric_in(A,relation_field(A))
| antisymmetric(A) )
& ( is_antisymmetric_in(A,relation_field(A))
| ~ antisymmetric(A) ) )
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A] :
( ( ( ~ is_antisymmetric_in(A,relation_field(A))
| antisymmetric(A) )
& ( is_antisymmetric_in(A,relation_field(A))
| ~ antisymmetric(A) ) )
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c2,plain,
( ~ is_antisymmetric_in(X0,relation_field(X0))
| antisymmetric(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p40,plain,
( ~ is_antisymmetric_in(sk0,relation_field(sk0))
| antisymmetric(sk0) ),
inference(resolution,[status(thm)],[c2,c29]) ).
cnf(p60,plain,
( antisymmetric(sk0)
| well_ordering(sk0) ),
inference(resolution,[status(thm)],[p59,p40]) ).
cnf(c9,plain,
( antisymmetric(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p36,plain,
( antisymmetric(sk0)
| ~ well_ordering(sk0) ),
inference(resolution,[status(thm)],[c9,c29]) ).
cnf(p63,plain,
( antisymmetric(sk0)
| antisymmetric(sk0) ),
inference(resolution,[status(thm)],[p60,p36]) ).
cnf(p66,plain,
antisymmetric(sk0),
inference(factoring,[status(thm)],[p63]) ).
cnf(p91,plain,
( ~ well_founded_relation(sk0)
| ~ connected(sk0)
| well_ordering(sk0) ),
inference(resolution,[status(thm)],[p90,p66]) ).
cnf(c16,plain,
( is_connected_in(X0,X1)
| ~ well_orders(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p68,plain,
( is_connected_in(sk0,X0)
| ~ well_orders(sk0,X0) ),
inference(resolution,[status(thm)],[c16,c29]) ).
cnf(p69,plain,
( well_ordering(sk0)
| is_connected_in(sk0,relation_field(sk0)) ),
inference(resolution,[status(thm)],[p68,c31]) ).
fof(f2,axiom,
! [A] :
( relation(A)
=> ( connected(A)
<=> is_connected_in(A,relation_field(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d14_relat_2) ).
fof(f2_nnf,plain,
! [A] :
( ( ( ~ is_connected_in(A,relation_field(A))
| connected(A) )
& ( is_connected_in(A,relation_field(A))
| ~ connected(A) ) )
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A] :
( ( ( ~ is_connected_in(A,relation_field(A))
| connected(A) )
& ( is_connected_in(A,relation_field(A))
| ~ connected(A) ) )
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c4,plain,
( ~ is_connected_in(X0,relation_field(X0))
| connected(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p42,plain,
( ~ is_connected_in(sk0,relation_field(sk0))
| connected(sk0) ),
inference(resolution,[status(thm)],[c4,c29]) ).
cnf(p70,plain,
( connected(sk0)
| well_ordering(sk0) ),
inference(resolution,[status(thm)],[p69,p42]) ).
cnf(c10,plain,
( connected(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p37,plain,
( connected(sk0)
| ~ well_ordering(sk0) ),
inference(resolution,[status(thm)],[c10,c29]) ).
cnf(p73,plain,
( connected(sk0)
| connected(sk0) ),
inference(resolution,[status(thm)],[p70,p37]) ).
cnf(p75,plain,
connected(sk0),
inference(factoring,[status(thm)],[p73]) ).
cnf(p92,plain,
( ~ well_founded_relation(sk0)
| well_ordering(sk0) ),
inference(resolution,[status(thm)],[p91,p75]) ).
fof(f13,axiom,
! [A] :
( relation(A)
=> ( well_founded_relation(A)
<=> is_well_founded_in(A,relation_field(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_wellord1) ).
fof(f13_nnf,plain,
! [A] :
( ( ( ~ is_well_founded_in(A,relation_field(A))
| well_founded_relation(A) )
& ( is_well_founded_in(A,relation_field(A))
| ~ well_founded_relation(A) ) )
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [A] :
( ( ( ~ is_well_founded_in(A,relation_field(A))
| well_founded_relation(A) )
& ( is_well_founded_in(A,relation_field(A))
| ~ well_founded_relation(A) ) )
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c28,plain,
( ~ is_well_founded_in(X0,relation_field(X0))
| well_founded_relation(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p83,plain,
( ~ is_well_founded_in(sk0,relation_field(sk0))
| well_founded_relation(sk0) ),
inference(resolution,[status(thm)],[c28,c29]) ).
cnf(c17,plain,
( is_well_founded_in(X0,X1)
| ~ well_orders(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p77,plain,
( is_well_founded_in(sk0,X0)
| ~ well_orders(sk0,X0) ),
inference(resolution,[status(thm)],[c17,c29]) ).
cnf(p78,plain,
( well_ordering(sk0)
| is_well_founded_in(sk0,relation_field(sk0)) ),
inference(resolution,[status(thm)],[p77,c31]) ).
cnf(p84,plain,
( well_ordering(sk0)
| well_founded_relation(sk0) ),
inference(resolution,[status(thm)],[p83,p78]) ).
cnf(p93,plain,
( well_ordering(sk0)
| well_ordering(sk0) ),
inference(resolution,[status(thm)],[p92,p84]) ).
cnf(p94,plain,
well_ordering(sk0),
inference(factoring,[status(thm)],[p93]) ).
cnf(c7,plain,
( reflexive(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p34,plain,
( reflexive(sk0)
| ~ well_ordering(sk0) ),
inference(resolution,[status(thm)],[c7,c29]) ).
cnf(p96,plain,
reflexive(sk0),
inference(resolution,[status(thm)],[p94,p34]) ).
cnf(c20,plain,
( is_reflexive_in(X0,relation_field(X0))
| ~ reflexive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p79,plain,
( is_reflexive_in(sk0,relation_field(sk0))
| ~ reflexive(sk0) ),
inference(resolution,[status(thm)],[c20,c29]) ).
cnf(p98,plain,
is_reflexive_in(sk0,relation_field(sk0)),
inference(resolution,[status(thm)],[p96,p79]) ).
cnf(p101,plain,
( ~ is_well_founded_in(sk0,relation_field(sk0))
| ~ is_connected_in(sk0,relation_field(sk0))
| ~ is_antisymmetric_in(sk0,relation_field(sk0))
| ~ is_transitive_in(sk0,relation_field(sk0))
| well_orders(sk0,relation_field(sk0)) ),
inference(resolution,[status(thm)],[p100,p98]) ).
cnf(c5,plain,
( is_transitive_in(X0,relation_field(X0))
| ~ transitive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p43,plain,
( is_transitive_in(sk0,relation_field(sk0))
| ~ transitive(sk0) ),
inference(resolution,[status(thm)],[c5,c29]) ).
cnf(p57,plain,
is_transitive_in(sk0,relation_field(sk0)),
inference(resolution,[status(thm)],[p56,p43]) ).
cnf(p102,plain,
( ~ is_well_founded_in(sk0,relation_field(sk0))
| ~ is_connected_in(sk0,relation_field(sk0))
| ~ is_antisymmetric_in(sk0,relation_field(sk0))
| well_orders(sk0,relation_field(sk0)) ),
inference(resolution,[status(thm)],[p101,p57]) ).
cnf(c1,plain,
( is_antisymmetric_in(X0,relation_field(X0))
| ~ antisymmetric(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p39,plain,
( is_antisymmetric_in(sk0,relation_field(sk0))
| ~ antisymmetric(sk0) ),
inference(resolution,[status(thm)],[c1,c29]) ).
cnf(p67,plain,
is_antisymmetric_in(sk0,relation_field(sk0)),
inference(resolution,[status(thm)],[p66,p39]) ).
cnf(p103,plain,
( ~ is_well_founded_in(sk0,relation_field(sk0))
| ~ is_connected_in(sk0,relation_field(sk0))
| well_orders(sk0,relation_field(sk0)) ),
inference(resolution,[status(thm)],[p102,p67]) ).
cnf(c3,plain,
( is_connected_in(X0,relation_field(X0))
| ~ connected(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p41,plain,
( is_connected_in(sk0,relation_field(sk0))
| ~ connected(sk0) ),
inference(resolution,[status(thm)],[c3,c29]) ).
cnf(p76,plain,
is_connected_in(sk0,relation_field(sk0)),
inference(resolution,[status(thm)],[p75,p41]) ).
cnf(p104,plain,
( ~ is_well_founded_in(sk0,relation_field(sk0))
| well_orders(sk0,relation_field(sk0)) ),
inference(resolution,[status(thm)],[p103,p76]) ).
cnf(c11,plain,
( well_founded_relation(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p38,plain,
( well_founded_relation(sk0)
| ~ well_ordering(sk0) ),
inference(resolution,[status(thm)],[c11,c29]) ).
cnf(p97,plain,
well_founded_relation(sk0),
inference(resolution,[status(thm)],[p94,p38]) ).
cnf(c27,plain,
( is_well_founded_in(X0,relation_field(X0))
| ~ well_founded_relation(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p82,plain,
( is_well_founded_in(sk0,relation_field(sk0))
| ~ well_founded_relation(sk0) ),
inference(resolution,[status(thm)],[c27,c29]) ).
cnf(p99,plain,
is_well_founded_in(sk0,relation_field(sk0)),
inference(resolution,[status(thm)],[p97,p82]) ).
cnf(p105,plain,
well_orders(sk0,relation_field(sk0)),
inference(resolution,[status(thm)],[p104,p99]) ).
cnf(c32,plain,
( ~ well_orders(sk0,relation_field(sk0))
| ~ well_ordering(sk0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p95,plain,
~ well_orders(sk0,relation_field(sk0)),
inference(resolution,[status(thm)],[p94,c32]) ).
cnf(p106,plain,
$false,
inference(resolution,[status(thm)],[p105,p95]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU244+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Thu Sep 24 13:22:35 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.03/0.29 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 1.66/0.72 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.66/0.72 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------