%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEU244+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n013.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 : Sun Sep 27 08:38:11 AM UTC 2026
% Result : Theorem 13.50s 4.25s
% Output : Refutation 13.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 9
% Syntax : Number of formulae : 198 ( 10 unt; 0 typ; 1 def)
% Number of atoms : 950 ( 77 equ; 0 cnn)
% Maximal formula atoms : 22 ( 4 avg)
% Number of connectives : 2457 ( 470 ~; 490 |; 61 &;1388 @)
% ( 9 <=>; 39 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 18 ( 15 usr; 3 con; 0-2 aty)
% Number of variables : 138 ( 0 ^; 137 !; 0 ?; 138 :)
% ( 0 !>; 0 ?*; 0 @-; 1 @+)
% Comments :
%------------------------------------------------------------------------------
thf(relation_decl,type,
relation: $i > $o ).
thf(well_orders_decl,type,
well_orders: $i > $i > $o ).
thf(relation_field_decl,type,
relation_field: $i > $i ).
thf(well_ordering_decl,type,
well_ordering: $i > $o ).
thf(antisymmetric_decl,type,
antisymmetric: $i > $o ).
thf(is_antisymmetric_in_decl,type,
is_antisymmetric_in: $i > $i > $o ).
thf(connected_decl,type,
connected: $i > $o ).
thf(is_connected_in_decl,type,
is_connected_in: $i > $i > $o ).
thf(transitive_decl,type,
transitive: $i > $o ).
thf(is_transitive_in_decl,type,
is_transitive_in: $i > $i > $o ).
thf(reflexive_decl,type,
reflexive: $i > $o ).
thf(well_founded_relation_decl,type,
well_founded_relation: $i > $o ).
thf(is_reflexive_in_decl,type,
is_reflexive_in: $i > $i > $o ).
thf(is_well_founded_in_decl,type,
is_well_founded_in: $i > $i > $o ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ( ( A @ relation )
=> ( ( ( A @ well_ordering )
=> ( A @ relation_field @ ( A @ well_orders ) ) )
& ( ( A @ relation_field @ ( A @ well_orders ) )
=> ( A @ well_ordering ) ) ) ) ) ) ).
thf(1,conjecture,
! [A: $i] :
( ( A @ relation )
=> ( ( A @ relation_field @ ( A @ well_orders ) )
<=> ( A @ well_ordering ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_wellord1) ).
thf(2,negated_conjecture,
~ ! [A: $i] :
( ( A @ relation )
=> ( ( A @ relation_field @ ( A @ well_orders ) )
<=> ( A @ well_ordering ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(17,plain,
~ ! [A: $i] :
( ( A @ relation )
=> ( ( ( A @ well_ordering )
=> ( A @ relation_field @ ( A @ well_orders ) ) )
& ( ( A @ relation_field @ ( A @ well_orders ) )
=> ( A @ well_ordering ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(18,plain,
( ( ~ ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ well_ordering ) )
& ( ( sk1 @ well_ordering )
| ~ ( sk1 @ well_ordering ) )
& ( ~ ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ( sk1 @ relation_field @ ( sk1 @ well_orders ) ) )
& ( ( sk1 @ well_ordering )
| ( sk1 @ relation_field @ ( sk1 @ well_orders ) ) )
& ( sk1 @ relation ) ),
inference(cnf,[status(esa)],[17]) ).
thf(20,plain,
( ( sk1 @ well_ordering )
| ( sk1 @ relation_field @ ( sk1 @ well_orders ) ) ),
inference(cnfConj,[status(thm)],[18]) ).
thf(22,plain,
sk1 @ relation,
inference(cnfConj,[status(thm)],[18]) ).
thf(8,axiom,
! [A: $i] :
( ( A @ relation )
=> ! [B: $i] :
( ( B @ ( A @ well_orders ) )
<=> ( ( B @ ( A @ is_well_founded_in ) )
& ( B @ ( A @ is_connected_in ) )
& ( B @ ( A @ is_antisymmetric_in ) )
& ( B @ ( A @ is_transitive_in ) )
& ( B @ ( A @ is_reflexive_in ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_wellord1) ).
thf(47,plain,
! [A: $i] :
( ( A @ relation )
=> ! [B: $i] :
( ( ( ( B @ ( A @ is_well_founded_in ) )
& ( B @ ( A @ is_connected_in ) )
& ( B @ ( A @ is_antisymmetric_in ) )
& ( B @ ( A @ is_transitive_in ) )
& ( B @ ( A @ is_reflexive_in ) ) )
=> ( B @ ( A @ well_orders ) ) )
& ( ( B @ ( A @ well_orders ) )
=> ( ( B @ ( A @ is_well_founded_in ) )
& ( B @ ( A @ is_connected_in ) )
& ( B @ ( A @ is_antisymmetric_in ) )
& ( B @ ( A @ is_transitive_in ) )
& ( B @ ( A @ is_reflexive_in ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(48,plain,
! [A: $i] :
( ( A @ relation )
=> ( ! [B: $i] :
( ( ( B @ ( A @ is_well_founded_in ) )
& ( B @ ( A @ is_connected_in ) )
& ( B @ ( A @ is_antisymmetric_in ) )
& ( B @ ( A @ is_transitive_in ) )
& ( B @ ( A @ is_reflexive_in ) ) )
=> ( B @ ( A @ well_orders ) ) )
& ! [B: $i] :
( ( B @ ( A @ well_orders ) )
=> ( ( B @ ( A @ is_well_founded_in ) )
& ( B @ ( A @ is_connected_in ) )
& ( B @ ( A @ is_antisymmetric_in ) )
& ( B @ ( A @ is_transitive_in ) )
& ( B @ ( A @ is_reflexive_in ) ) ) ) ) ),
inference(miniscope,[status(thm)],[47]) ).
thf(49,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ well_orders ) )
| ~ ( C @ ( A @ is_well_founded_in ) )
| ~ ( C @ ( A @ is_connected_in ) )
| ~ ( C @ ( A @ is_antisymmetric_in ) )
| ~ ( C @ ( A @ is_transitive_in ) )
| ~ ( C @ ( A @ is_reflexive_in ) )
| ~ ( A @ relation ) )
& ( ( B @ ( A @ is_well_founded_in ) )
| ~ ( B @ ( A @ well_orders ) )
| ~ ( A @ relation ) )
& ( ( B @ ( A @ is_connected_in ) )
| ~ ( B @ ( A @ well_orders ) )
| ~ ( A @ relation ) )
& ( ( B @ ( A @ is_antisymmetric_in ) )
| ~ ( B @ ( A @ well_orders ) )
| ~ ( A @ relation ) )
& ( ( B @ ( A @ is_transitive_in ) )
| ~ ( B @ ( A @ well_orders ) )
| ~ ( A @ relation ) )
& ( ( B @ ( A @ is_reflexive_in ) )
| ~ ( B @ ( A @ well_orders ) )
| ~ ( A @ relation ) ) ),
inference(cnf,[status(esa)],[48]) ).
thf(52,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ is_well_founded_in ) )
| ~ ( B @ ( A @ well_orders ) )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[49]) ).
thf(868,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( B @ ( A @ is_well_founded_in ) )
| ~ ( B @ ( A @ well_orders ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,52]) ).
thf(869,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( B @ ( A @ is_well_founded_in ) )
| ~ ( B @ ( A @ well_orders ) ) ),
inference(simp,[status(thm)],[868]) ).
thf(870,plain,
! [A: $i] :
( ( A @ ( sk1 @ is_well_founded_in ) )
| ~ ( A @ ( sk1 @ well_orders ) ) ),
inference(pattern_uni,[status(thm)],[869:[bind(A,$thf( sk1 ))]]) ).
thf(877,plain,
! [A: $i] :
( ( A @ ( sk1 @ is_well_founded_in ) )
| ~ ( A @ ( sk1 @ well_orders ) ) ),
inference(simp,[status(thm)],[870]) ).
thf(884,plain,
! [A: $i] :
( ( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
!= ( A @ ( sk1 @ well_orders ) ) )
| ( A @ ( sk1 @ is_well_founded_in ) )
| ~ $true
| ( sk1 @ well_ordering ) ),
inference(paramod_ordered,[status(thm)],[20,877]) ).
thf(885,plain,
! [A: $i] :
( ( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
!= ( A @ ( sk1 @ well_orders ) ) )
| ( A @ ( sk1 @ is_well_founded_in ) )
| ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[884]) ).
thf(886,plain,
( ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[885:[bind(A,$thf( sk1 @ relation_field ))]]) ).
thf(7,axiom,
! [A: $i] :
( ( A @ relation )
=> ( ( A @ well_ordering )
<=> ( ( A @ well_founded_relation )
& ( A @ connected )
& ( A @ antisymmetric )
& ( A @ transitive )
& ( A @ reflexive ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_wellord1) ).
thf(39,plain,
! [A: $i] :
( ( A @ relation )
=> ( ( ( ( A @ well_founded_relation )
& ( A @ connected )
& ( A @ antisymmetric )
& ( A @ transitive )
& ( A @ reflexive ) )
=> ( A @ well_ordering ) )
& ( ( A @ well_ordering )
=> ( ( A @ well_founded_relation )
& ( A @ connected )
& ( A @ antisymmetric )
& ( A @ transitive )
& ( A @ reflexive ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(40,plain,
! [A: $i] :
( ( ( A @ well_ordering )
| ~ ( A @ well_founded_relation )
| ~ ( A @ connected )
| ~ ( A @ antisymmetric )
| ~ ( A @ transitive )
| ~ ( A @ reflexive )
| ~ ( A @ relation ) )
& ( ( A @ well_founded_relation )
| ~ ( A @ well_ordering )
| ~ ( A @ relation ) )
& ( ( A @ connected )
| ~ ( A @ well_ordering )
| ~ ( A @ relation ) )
& ( ( A @ antisymmetric )
| ~ ( A @ well_ordering )
| ~ ( A @ relation ) )
& ( ( A @ transitive )
| ~ ( A @ well_ordering )
| ~ ( A @ relation ) )
& ( ( A @ reflexive )
| ~ ( A @ well_ordering )
| ~ ( A @ relation ) ) ),
inference(cnf,[status(esa)],[39]) ).
thf(46,plain,
! [A: $i] :
( ( A @ well_founded_relation )
| ~ ( A @ well_ordering )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[40]) ).
thf(583,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ well_founded_relation )
| ~ ( A @ well_ordering )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,46]) ).
thf(584,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ well_founded_relation )
| ~ ( A @ well_ordering ) ),
inference(simp,[status(thm)],[583]) ).
thf(585,plain,
( ( sk1 @ well_founded_relation )
| ~ ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[584:[bind(A,$thf( sk1 ))]]) ).
thf(16,axiom,
! [A: $i] :
( ( A @ relation )
=> ( ( A @ well_founded_relation )
<=> ( A @ relation_field @ ( A @ is_well_founded_in ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_wellord1) ).
thf(71,plain,
! [A: $i] :
( ( A @ relation )
=> ( ( ( A @ relation_field @ ( A @ is_well_founded_in ) )
=> ( A @ well_founded_relation ) )
& ( ( A @ well_founded_relation )
=> ( A @ relation_field @ ( A @ is_well_founded_in ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(72,plain,
! [A: $i] :
( ( ( A @ well_founded_relation )
| ~ ( A @ relation_field @ ( A @ is_well_founded_in ) )
| ~ ( A @ relation ) )
& ( ( A @ relation_field @ ( A @ is_well_founded_in ) )
| ~ ( A @ well_founded_relation )
| ~ ( A @ relation ) ) ),
inference(cnf,[status(esa)],[71]) ).
thf(73,plain,
! [A: $i] :
( ( A @ relation_field @ ( A @ is_well_founded_in ) )
| ~ ( A @ well_founded_relation )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[72]) ).
thf(1360,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ relation_field @ ( A @ is_well_founded_in ) )
| ~ ( A @ well_founded_relation )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,73]) ).
thf(1361,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ relation_field @ ( A @ is_well_founded_in ) )
| ~ ( A @ well_founded_relation ) ),
inference(simp,[status(thm)],[1360]) ).
thf(1362,plain,
( ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ well_founded_relation ) ),
inference(pattern_uni,[status(thm)],[1361:[bind(A,$thf( sk1 ))]]) ).
thf(1408,plain,
( ( ( sk1 @ well_founded_relation )
!= ( sk1 @ well_founded_relation ) )
| ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ $true
| ~ ( sk1 @ well_ordering ) ),
inference(paramod_ordered,[status(thm)],[585,1362]) ).
thf(1409,plain,
( ( ( sk1 @ well_founded_relation )
!= ( sk1 @ well_founded_relation ) )
| ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[1408]) ).
thf(1410,plain,
( ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[1409:[]]) ).
thf(45,plain,
! [A: $i] :
( ( A @ antisymmetric )
| ~ ( A @ well_ordering )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[40]) ).
thf(377,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ antisymmetric )
| ~ ( A @ well_ordering )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,45]) ).
thf(378,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ antisymmetric )
| ~ ( A @ well_ordering ) ),
inference(simp,[status(thm)],[377]) ).
thf(379,plain,
( ( sk1 @ antisymmetric )
| ~ ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[378:[bind(A,$thf( sk1 ))]]) ).
thf(41,plain,
! [A: $i] :
( ( A @ reflexive )
| ~ ( A @ well_ordering )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[40]) ).
thf(214,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ reflexive )
| ~ ( A @ well_ordering )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,41]) ).
thf(215,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ reflexive )
| ~ ( A @ well_ordering ) ),
inference(simp,[status(thm)],[214]) ).
thf(216,plain,
( ( sk1 @ reflexive )
| ~ ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[215:[bind(A,$thf( sk1 ))]]) ).
thf(10,axiom,
! [A: $i] :
( ( A @ relation )
=> ( ( A @ reflexive )
<=> ( A @ relation_field @ ( A @ is_reflexive_in ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_relat_2) ).
thf(60,plain,
! [A: $i] :
( ( A @ relation )
=> ( ( ( A @ relation_field @ ( A @ is_reflexive_in ) )
=> ( A @ reflexive ) )
& ( ( A @ reflexive )
=> ( A @ relation_field @ ( A @ is_reflexive_in ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(61,plain,
! [A: $i] :
( ( ( A @ reflexive )
| ~ ( A @ relation_field @ ( A @ is_reflexive_in ) )
| ~ ( A @ relation ) )
& ( ( A @ relation_field @ ( A @ is_reflexive_in ) )
| ~ ( A @ reflexive )
| ~ ( A @ relation ) ) ),
inference(cnf,[status(esa)],[60]) ).
thf(62,plain,
! [A: $i] :
( ( A @ relation_field @ ( A @ is_reflexive_in ) )
| ~ ( A @ reflexive )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[61]) ).
thf(640,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ relation_field @ ( A @ is_reflexive_in ) )
| ~ ( A @ reflexive )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,62]) ).
thf(641,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ relation_field @ ( A @ is_reflexive_in ) )
| ~ ( A @ reflexive ) ),
inference(simp,[status(thm)],[640]) ).
thf(642,plain,
( ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ reflexive ) ),
inference(pattern_uni,[status(thm)],[641:[bind(A,$thf( sk1 ))]]) ).
thf(655,plain,
( ( ( sk1 @ reflexive )
!= ( sk1 @ reflexive ) )
| ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ $true
| ~ ( sk1 @ well_ordering ) ),
inference(paramod_ordered,[status(thm)],[216,642]) ).
thf(656,plain,
( ( ( sk1 @ reflexive )
!= ( sk1 @ reflexive ) )
| ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[655]) ).
thf(657,plain,
( ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[656:[]]) ).
thf(42,plain,
! [A: $i] :
( ( A @ transitive )
| ~ ( A @ well_ordering )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[40]) ).
thf(273,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ transitive )
| ~ ( A @ well_ordering )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,42]) ).
thf(274,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ transitive )
| ~ ( A @ well_ordering ) ),
inference(simp,[status(thm)],[273]) ).
thf(275,plain,
( ( sk1 @ transitive )
| ~ ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[274:[bind(A,$thf( sk1 ))]]) ).
thf(6,axiom,
! [A: $i] :
( ( A @ relation )
=> ( ( A @ transitive )
<=> ( A @ relation_field @ ( A @ is_transitive_in ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d16_relat_2) ).
thf(35,plain,
! [A: $i] :
( ( A @ relation )
=> ( ( ( A @ relation_field @ ( A @ is_transitive_in ) )
=> ( A @ transitive ) )
& ( ( A @ transitive )
=> ( A @ relation_field @ ( A @ is_transitive_in ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(36,plain,
! [A: $i] :
( ( ( A @ transitive )
| ~ ( A @ relation_field @ ( A @ is_transitive_in ) )
| ~ ( A @ relation ) )
& ( ( A @ relation_field @ ( A @ is_transitive_in ) )
| ~ ( A @ transitive )
| ~ ( A @ relation ) ) ),
inference(cnf,[status(esa)],[35]) ).
thf(37,plain,
! [A: $i] :
( ( A @ relation_field @ ( A @ is_transitive_in ) )
| ~ ( A @ transitive )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[36]) ).
thf(455,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ relation_field @ ( A @ is_transitive_in ) )
| ~ ( A @ transitive )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,37]) ).
thf(456,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ relation_field @ ( A @ is_transitive_in ) )
| ~ ( A @ transitive ) ),
inference(simp,[status(thm)],[455]) ).
thf(457,plain,
( ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ ( sk1 @ transitive ) ),
inference(pattern_uni,[status(thm)],[456:[bind(A,$thf( sk1 ))]]) ).
thf(482,plain,
( ( ( sk1 @ transitive )
!= ( sk1 @ transitive ) )
| ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ $true
| ~ ( sk1 @ well_ordering ) ),
inference(paramod_ordered,[status(thm)],[275,457]) ).
thf(483,plain,
( ( ( sk1 @ transitive )
!= ( sk1 @ transitive ) )
| ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[482]) ).
thf(484,plain,
( ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[483:[]]) ).
thf(43,plain,
! [A: $i] :
( ( A @ connected )
| ~ ( A @ well_ordering )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[40]) ).
thf(5,axiom,
! [A: $i] :
( ( A @ relation )
=> ( ( A @ connected )
<=> ( A @ relation_field @ ( A @ is_connected_in ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d14_relat_2) ).
thf(31,plain,
! [A: $i] :
( ( A @ relation )
=> ( ( ( A @ relation_field @ ( A @ is_connected_in ) )
=> ( A @ connected ) )
& ( ( A @ connected )
=> ( A @ relation_field @ ( A @ is_connected_in ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(32,plain,
! [A: $i] :
( ( ( A @ connected )
| ~ ( A @ relation_field @ ( A @ is_connected_in ) )
| ~ ( A @ relation ) )
& ( ( A @ relation_field @ ( A @ is_connected_in ) )
| ~ ( A @ connected )
| ~ ( A @ relation ) ) ),
inference(cnf,[status(esa)],[31]) ).
thf(33,plain,
! [A: $i] :
( ( A @ relation_field @ ( A @ is_connected_in ) )
| ~ ( A @ connected )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[32]) ).
thf(4,axiom,
! [A: $i] :
( ( A @ relation )
=> ( ( A @ antisymmetric )
<=> ( A @ relation_field @ ( A @ is_antisymmetric_in ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d12_relat_2) ).
thf(27,plain,
! [A: $i] :
( ( A @ relation )
=> ( ( ( A @ relation_field @ ( A @ is_antisymmetric_in ) )
=> ( A @ antisymmetric ) )
& ( ( A @ antisymmetric )
=> ( A @ relation_field @ ( A @ is_antisymmetric_in ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(28,plain,
! [A: $i] :
( ( ( A @ antisymmetric )
| ~ ( A @ relation_field @ ( A @ is_antisymmetric_in ) )
| ~ ( A @ relation ) )
& ( ( A @ relation_field @ ( A @ is_antisymmetric_in ) )
| ~ ( A @ antisymmetric )
| ~ ( A @ relation ) ) ),
inference(cnf,[status(esa)],[27]) ).
thf(29,plain,
! [A: $i] :
( ( A @ relation_field @ ( A @ is_antisymmetric_in ) )
| ~ ( A @ antisymmetric )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[28]) ).
thf(145,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ relation_field @ ( A @ is_antisymmetric_in ) )
| ~ ( A @ antisymmetric )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,29]) ).
thf(146,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ relation_field @ ( A @ is_antisymmetric_in ) )
| ~ ( A @ antisymmetric ) ),
inference(simp,[status(thm)],[145]) ).
thf(147,plain,
( ( sk1 @ relation_field @ ( sk1 @ is_antisymmetric_in ) )
| ~ ( sk1 @ antisymmetric ) ),
inference(pattern_uni,[status(thm)],[146:[bind(A,$thf( sk1 ))]]) ).
thf(51,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ well_orders ) )
| ~ ( B @ ( A @ is_well_founded_in ) )
| ~ ( B @ ( A @ is_connected_in ) )
| ~ ( B @ ( A @ is_antisymmetric_in ) )
| ~ ( B @ ( A @ is_transitive_in ) )
| ~ ( B @ ( A @ is_reflexive_in ) )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[49]) ).
thf(56,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ well_orders ) )
| ~ ( B @ ( A @ is_well_founded_in ) )
| ~ ( B @ ( A @ is_connected_in ) )
| ~ ( B @ ( A @ is_antisymmetric_in ) )
| ~ ( B @ ( A @ is_transitive_in ) )
| ~ ( B @ ( A @ is_reflexive_in ) )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[51]) ).
thf(150,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation_field @ ( sk1 @ is_antisymmetric_in ) )
!= ( B @ ( A @ is_antisymmetric_in ) ) )
| ( B @ ( A @ well_orders ) )
| ~ ( B @ ( A @ is_well_founded_in ) )
| ~ ( B @ ( A @ is_connected_in ) )
| ~ $true
| ~ ( B @ ( A @ is_transitive_in ) )
| ~ ( B @ ( A @ is_reflexive_in ) )
| ~ ( A @ relation )
| ~ ( sk1 @ antisymmetric ) ),
inference(paramod_ordered,[status(thm)],[147,56]) ).
thf(151,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation_field @ ( sk1 @ is_antisymmetric_in ) )
!= ( B @ ( A @ is_antisymmetric_in ) ) )
| ( B @ ( A @ well_orders ) )
| ~ ( B @ ( A @ is_well_founded_in ) )
| ~ ( B @ ( A @ is_connected_in ) )
| ~ ( B @ ( A @ is_transitive_in ) )
| ~ ( B @ ( A @ is_reflexive_in ) )
| ~ ( A @ relation )
| ~ ( sk1 @ antisymmetric ) ),
inference(simp,[status(thm)],[150]) ).
thf(152,plain,
( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_connected_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ relation )
| ~ ( sk1 @ antisymmetric ) ),
inference(pattern_uni,[status(thm)],[151:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ relation_field ))]]) ).
thf(161,plain,
( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_connected_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ $true
| ~ ( sk1 @ antisymmetric ) ),
inference(rewrite,[status(thm)],[152,22]) ).
thf(162,plain,
( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_connected_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ antisymmetric ) ),
inference(simp,[status(thm)],[161]) ).
thf(247,plain,
! [A: $i] :
( ( ( A @ relation_field @ ( A @ is_connected_in ) )
!= ( sk1 @ relation_field @ ( sk1 @ is_connected_in ) ) )
| ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ $true
| ~ ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ antisymmetric )
| ~ ( A @ connected )
| ~ ( A @ relation ) ),
inference(paramod_ordered,[status(thm)],[33,162]) ).
thf(248,plain,
! [A: $i] :
( ( ( A @ relation_field @ ( A @ is_connected_in ) )
!= ( sk1 @ relation_field @ ( sk1 @ is_connected_in ) ) )
| ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ antisymmetric )
| ~ ( A @ connected )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[247]) ).
thf(249,plain,
( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ antisymmetric )
| ~ ( sk1 @ connected )
| ~ ( sk1 @ relation ) ),
inference(pattern_uni,[status(thm)],[248:[bind(A,$thf( sk1 ))]]) ).
thf(301,plain,
( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ antisymmetric )
| ~ ( sk1 @ connected )
| ~ $true ),
inference(rewrite,[status(thm)],[249,22]) ).
thf(302,plain,
( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ antisymmetric )
| ~ ( sk1 @ connected ) ),
inference(simp,[status(thm)],[301]) ).
thf(303,plain,
! [A: $i] :
( ( ( A @ connected )
!= ( sk1 @ connected ) )
| ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ antisymmetric )
| ~ $true
| ~ ( A @ well_ordering )
| ~ ( A @ relation ) ),
inference(paramod_ordered,[status(thm)],[43,302]) ).
thf(304,plain,
! [A: $i] :
( ( ( A @ connected )
!= ( sk1 @ connected ) )
| ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ antisymmetric )
| ~ ( A @ well_ordering )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[303]) ).
thf(305,plain,
( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ antisymmetric )
| ~ ( sk1 @ well_ordering )
| ~ ( sk1 @ relation ) ),
inference(pattern_uni,[status(thm)],[304:[bind(A,$thf( sk1 ))]]) ).
thf(388,plain,
( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ antisymmetric )
| ~ ( sk1 @ well_ordering )
| ~ $true ),
inference(rewrite,[status(thm)],[305,22]) ).
thf(389,plain,
( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ antisymmetric )
| ~ ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[388]) ).
thf(491,plain,
( ( ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
!= ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) ) )
| ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ $true
| ~ ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ antisymmetric )
| ~ ( sk1 @ well_ordering )
| ~ ( sk1 @ well_ordering ) ),
inference(paramod_ordered,[status(thm)],[484,389]) ).
thf(492,plain,
( ( ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) )
!= ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) ) )
| ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ antisymmetric )
| ~ ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[491]) ).
thf(493,plain,
( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ~ ( sk1 @ antisymmetric )
| ~ ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[492:[]]) ).
thf(697,plain,
( ( ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
!= ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) ) )
| ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ $true
| ~ ( sk1 @ antisymmetric )
| ~ ( sk1 @ well_ordering )
| ~ ( sk1 @ well_ordering ) ),
inference(paramod_ordered,[status(thm)],[657,493]) ).
thf(698,plain,
( ( ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
!= ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) ) )
| ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ antisymmetric )
| ~ ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[697]) ).
thf(699,plain,
( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ antisymmetric )
| ~ ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[698:[]]) ).
thf(840,plain,
( ( ( sk1 @ antisymmetric )
!= ( sk1 @ antisymmetric ) )
| ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ $true
| ~ ( sk1 @ well_ordering )
| ~ ( sk1 @ well_ordering ) ),
inference(paramod_ordered,[status(thm)],[379,699]) ).
thf(841,plain,
( ( ( sk1 @ antisymmetric )
!= ( sk1 @ antisymmetric ) )
| ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[840]) ).
thf(842,plain,
( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| ~ ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[841:[]]) ).
thf(1426,plain,
( ( ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
!= ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) ) )
| ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ $true
| ~ ( sk1 @ well_ordering )
| ~ ( sk1 @ well_ordering ) ),
inference(paramod_ordered,[status(thm)],[1410,842]) ).
thf(1427,plain,
( ( ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
!= ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) ) )
| ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[1426]) ).
thf(1428,plain,
( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[1427:[]]) ).
thf(23,plain,
( ~ ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
| ~ ( sk1 @ well_ordering ) ),
inference(cnfConj,[status(thm)],[18]) ).
thf(1477,plain,
( ( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
!= ( sk1 @ relation_field @ ( sk1 @ well_orders ) ) )
| ~ $true
| ~ ( sk1 @ well_ordering )
| ~ ( sk1 @ well_ordering ) ),
inference(paramod_ordered,[status(thm)],[1428,23]) ).
thf(1478,plain,
( ( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
!= ( sk1 @ relation_field @ ( sk1 @ well_orders ) ) )
| ~ ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[1477]) ).
thf(1479,plain,
~ ( sk1 @ well_ordering ),
inference(pattern_uni,[status(thm)],[1478:[]]) ).
thf(1506,plain,
( ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
| $false ),
inference(rewrite,[status(thm)],[886,1479]) ).
thf(1507,plain,
sk1 @ relation_field @ ( sk1 @ is_well_founded_in ),
inference(simp,[status(thm)],[1506]) ).
thf(74,plain,
! [A: $i] :
( ( A @ well_founded_relation )
| ~ ( A @ relation_field @ ( A @ is_well_founded_in ) )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[72]) ).
thf(1673,plain,
! [A: $i] :
( ( ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
!= ( A @ relation_field @ ( A @ is_well_founded_in ) ) )
| ( A @ well_founded_relation )
| ~ $true
| ~ ( A @ relation ) ),
inference(paramod_ordered,[status(thm)],[1507,74]) ).
thf(1674,plain,
! [A: $i] :
( ( ( sk1 @ relation_field @ ( sk1 @ is_well_founded_in ) )
!= ( A @ relation_field @ ( A @ is_well_founded_in ) ) )
| ( A @ well_founded_relation )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[1673]) ).
thf(1675,plain,
( ( sk1 @ well_founded_relation )
| ~ ( sk1 @ relation ) ),
inference(pattern_uni,[status(thm)],[1674:[bind(A,$thf( sk1 ))]]) ).
thf(44,plain,
! [A: $i] :
( ( A @ well_ordering )
| ~ ( A @ well_founded_relation )
| ~ ( A @ connected )
| ~ ( A @ antisymmetric )
| ~ ( A @ transitive )
| ~ ( A @ reflexive )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[40]) ).
thf(87,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ well_ordering )
| ~ ( A @ well_founded_relation )
| ~ ( A @ connected )
| ~ ( A @ antisymmetric )
| ~ ( A @ transitive )
| ~ ( A @ reflexive )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,44]) ).
thf(88,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ well_ordering )
| ~ ( A @ well_founded_relation )
| ~ ( A @ connected )
| ~ ( A @ antisymmetric )
| ~ ( A @ transitive )
| ~ ( A @ reflexive ) ),
inference(simp,[status(thm)],[87]) ).
thf(89,plain,
( ( sk1 @ well_ordering )
| ~ ( sk1 @ well_founded_relation )
| ~ ( sk1 @ connected )
| ~ ( sk1 @ antisymmetric )
| ~ ( sk1 @ transitive )
| ~ ( sk1 @ reflexive ) ),
inference(pattern_uni,[status(thm)],[88:[bind(A,$thf( sk1 ))]]) ).
thf(1496,plain,
( $false
| ~ ( sk1 @ well_founded_relation )
| ~ ( sk1 @ connected )
| ~ ( sk1 @ antisymmetric )
| ~ ( sk1 @ transitive )
| ~ ( sk1 @ reflexive ) ),
inference(rewrite,[status(thm)],[89,1479]) ).
thf(1497,plain,
( ~ ( sk1 @ well_founded_relation )
| ~ ( sk1 @ connected )
| ~ ( sk1 @ antisymmetric )
| ~ ( sk1 @ transitive )
| ~ ( sk1 @ reflexive ) ),
inference(simp,[status(thm)],[1496]) ).
thf(55,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ is_transitive_in ) )
| ~ ( B @ ( A @ well_orders ) )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[49]) ).
thf(1247,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( B @ ( A @ is_transitive_in ) )
| ~ ( B @ ( A @ well_orders ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,55]) ).
thf(1248,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( B @ ( A @ is_transitive_in ) )
| ~ ( B @ ( A @ well_orders ) ) ),
inference(simp,[status(thm)],[1247]) ).
thf(1249,plain,
! [A: $i] :
( ( A @ ( sk1 @ is_transitive_in ) )
| ~ ( A @ ( sk1 @ well_orders ) ) ),
inference(pattern_uni,[status(thm)],[1248:[bind(A,$thf( sk1 ))]]) ).
thf(1259,plain,
! [A: $i] :
( ( A @ ( sk1 @ is_transitive_in ) )
| ~ ( A @ ( sk1 @ well_orders ) ) ),
inference(simp,[status(thm)],[1249]) ).
thf(38,plain,
! [A: $i] :
( ( A @ transitive )
| ~ ( A @ relation_field @ ( A @ is_transitive_in ) )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[36]) ).
thf(566,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ transitive )
| ~ ( A @ relation_field @ ( A @ is_transitive_in ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,38]) ).
thf(567,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ transitive )
| ~ ( A @ relation_field @ ( A @ is_transitive_in ) ) ),
inference(simp,[status(thm)],[566]) ).
thf(568,plain,
( ( sk1 @ transitive )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) ) ),
inference(pattern_uni,[status(thm)],[567:[bind(A,$thf( sk1 ))]]) ).
thf(1264,plain,
! [A: $i] :
( ( ( A @ ( sk1 @ is_transitive_in ) )
!= ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) ) )
| ( sk1 @ transitive )
| ~ $true
| ~ ( A @ ( sk1 @ well_orders ) ) ),
inference(paramod_ordered,[status(thm)],[1259,568]) ).
thf(1265,plain,
! [A: $i] :
( ( ( A @ ( sk1 @ is_transitive_in ) )
!= ( sk1 @ relation_field @ ( sk1 @ is_transitive_in ) ) )
| ( sk1 @ transitive )
| ~ ( A @ ( sk1 @ well_orders ) ) ),
inference(simp,[status(thm)],[1264]) ).
thf(1266,plain,
( ( sk1 @ transitive )
| ~ ( sk1 @ relation_field @ ( sk1 @ well_orders ) ) ),
inference(pattern_uni,[status(thm)],[1265:[bind(A,$thf( sk1 @ relation_field ))]]) ).
thf(1288,plain,
( ( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
!= ( sk1 @ relation_field @ ( sk1 @ well_orders ) ) )
| ( sk1 @ transitive )
| ~ $true
| ( sk1 @ well_ordering ) ),
inference(paramod_ordered,[status(thm)],[20,1266]) ).
thf(1289,plain,
( ( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
!= ( sk1 @ relation_field @ ( sk1 @ well_orders ) ) )
| ( sk1 @ transitive )
| ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[1288]) ).
thf(1290,plain,
( ( sk1 @ transitive )
| ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[1289:[]]) ).
thf(1486,plain,
( ( sk1 @ transitive )
| $false ),
inference(rewrite,[status(thm)],[1290,1479]) ).
thf(1487,plain,
sk1 @ transitive,
inference(simp,[status(thm)],[1486]) ).
thf(1525,plain,
( ~ ( sk1 @ well_founded_relation )
| ~ ( sk1 @ connected )
| ~ ( sk1 @ antisymmetric )
| ~ $true
| ~ ( sk1 @ reflexive ) ),
inference(rewrite,[status(thm)],[1497,1487]) ).
thf(1526,plain,
( ~ ( sk1 @ well_founded_relation )
| ~ ( sk1 @ connected )
| ~ ( sk1 @ antisymmetric )
| ~ ( sk1 @ reflexive ) ),
inference(simp,[status(thm)],[1525]) ).
thf(53,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ is_antisymmetric_in ) )
| ~ ( B @ ( A @ well_orders ) )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[49]) ).
thf(1004,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( B @ ( A @ is_antisymmetric_in ) )
| ~ ( B @ ( A @ well_orders ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,53]) ).
thf(1005,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( B @ ( A @ is_antisymmetric_in ) )
| ~ ( B @ ( A @ well_orders ) ) ),
inference(simp,[status(thm)],[1004]) ).
thf(1006,plain,
! [A: $i] :
( ( A @ ( sk1 @ is_antisymmetric_in ) )
| ~ ( A @ ( sk1 @ well_orders ) ) ),
inference(pattern_uni,[status(thm)],[1005:[bind(A,$thf( sk1 ))]]) ).
thf(1014,plain,
! [A: $i] :
( ( A @ ( sk1 @ is_antisymmetric_in ) )
| ~ ( A @ ( sk1 @ well_orders ) ) ),
inference(simp,[status(thm)],[1006]) ).
thf(1021,plain,
! [A: $i] :
( ( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
!= ( A @ ( sk1 @ well_orders ) ) )
| ( A @ ( sk1 @ is_antisymmetric_in ) )
| ~ $true
| ( sk1 @ well_ordering ) ),
inference(paramod_ordered,[status(thm)],[20,1014]) ).
thf(1022,plain,
! [A: $i] :
( ( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
!= ( A @ ( sk1 @ well_orders ) ) )
| ( A @ ( sk1 @ is_antisymmetric_in ) )
| ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[1021]) ).
thf(1023,plain,
( ( sk1 @ relation_field @ ( sk1 @ is_antisymmetric_in ) )
| ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[1022:[bind(A,$thf( sk1 @ relation_field ))]]) ).
thf(30,plain,
! [A: $i] :
( ( A @ antisymmetric )
| ~ ( A @ relation_field @ ( A @ is_antisymmetric_in ) )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[28]) ).
thf(169,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ antisymmetric )
| ~ ( A @ relation_field @ ( A @ is_antisymmetric_in ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,30]) ).
thf(170,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ antisymmetric )
| ~ ( A @ relation_field @ ( A @ is_antisymmetric_in ) ) ),
inference(simp,[status(thm)],[169]) ).
thf(171,plain,
( ( sk1 @ antisymmetric )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_antisymmetric_in ) ) ),
inference(pattern_uni,[status(thm)],[170:[bind(A,$thf( sk1 ))]]) ).
thf(1039,plain,
( ( ( sk1 @ relation_field @ ( sk1 @ is_antisymmetric_in ) )
!= ( sk1 @ relation_field @ ( sk1 @ is_antisymmetric_in ) ) )
| ( sk1 @ antisymmetric )
| ~ $true
| ( sk1 @ well_ordering ) ),
inference(paramod_ordered,[status(thm)],[1023,171]) ).
thf(1040,plain,
( ( ( sk1 @ relation_field @ ( sk1 @ is_antisymmetric_in ) )
!= ( sk1 @ relation_field @ ( sk1 @ is_antisymmetric_in ) ) )
| ( sk1 @ antisymmetric )
| ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[1039]) ).
thf(1041,plain,
( ( sk1 @ antisymmetric )
| ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[1040:[]]) ).
thf(1490,plain,
( ( sk1 @ antisymmetric )
| $false ),
inference(rewrite,[status(thm)],[1041,1479]) ).
thf(1491,plain,
sk1 @ antisymmetric,
inference(simp,[status(thm)],[1490]) ).
thf(50,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ is_reflexive_in ) )
| ~ ( B @ ( A @ well_orders ) )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[49]) ).
thf(727,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( B @ ( A @ is_reflexive_in ) )
| ~ ( B @ ( A @ well_orders ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,50]) ).
thf(728,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( B @ ( A @ is_reflexive_in ) )
| ~ ( B @ ( A @ well_orders ) ) ),
inference(simp,[status(thm)],[727]) ).
thf(729,plain,
! [A: $i] :
( ( A @ ( sk1 @ is_reflexive_in ) )
| ~ ( A @ ( sk1 @ well_orders ) ) ),
inference(pattern_uni,[status(thm)],[728:[bind(A,$thf( sk1 ))]]) ).
thf(733,plain,
! [A: $i] :
( ( A @ ( sk1 @ is_reflexive_in ) )
| ~ ( A @ ( sk1 @ well_orders ) ) ),
inference(simp,[status(thm)],[729]) ).
thf(740,plain,
! [A: $i] :
( ( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
!= ( A @ ( sk1 @ well_orders ) ) )
| ( A @ ( sk1 @ is_reflexive_in ) )
| ~ $true
| ( sk1 @ well_ordering ) ),
inference(paramod_ordered,[status(thm)],[20,733]) ).
thf(741,plain,
! [A: $i] :
( ( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
!= ( A @ ( sk1 @ well_orders ) ) )
| ( A @ ( sk1 @ is_reflexive_in ) )
| ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[740]) ).
thf(742,plain,
( ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
| ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[741:[bind(A,$thf( sk1 @ relation_field ))]]) ).
thf(63,plain,
! [A: $i] :
( ( A @ reflexive )
| ~ ( A @ relation_field @ ( A @ is_reflexive_in ) )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[61]) ).
thf(931,plain,
! [A: $i] :
( ( ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
!= ( A @ relation_field @ ( A @ is_reflexive_in ) ) )
| ( A @ reflexive )
| ~ $true
| ~ ( A @ relation )
| ( sk1 @ well_ordering ) ),
inference(paramod_ordered,[status(thm)],[742,63]) ).
thf(932,plain,
! [A: $i] :
( ( ( sk1 @ relation_field @ ( sk1 @ is_reflexive_in ) )
!= ( A @ relation_field @ ( A @ is_reflexive_in ) ) )
| ( A @ reflexive )
| ~ ( A @ relation )
| ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[931]) ).
thf(933,plain,
( ( sk1 @ reflexive )
| ~ ( sk1 @ relation )
| ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[932:[bind(A,$thf( sk1 ))]]) ).
thf(957,plain,
( ( sk1 @ reflexive )
| ~ $true
| ( sk1 @ well_ordering ) ),
inference(rewrite,[status(thm)],[933,22]) ).
thf(958,plain,
( ( sk1 @ reflexive )
| ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[957]) ).
thf(1500,plain,
( ( sk1 @ reflexive )
| $false ),
inference(rewrite,[status(thm)],[958,1479]) ).
thf(1501,plain,
sk1 @ reflexive,
inference(simp,[status(thm)],[1500]) ).
thf(54,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ is_connected_in ) )
| ~ ( B @ ( A @ well_orders ) )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[49]) ).
thf(1096,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( B @ ( A @ is_connected_in ) )
| ~ ( B @ ( A @ well_orders ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,54]) ).
thf(1097,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( B @ ( A @ is_connected_in ) )
| ~ ( B @ ( A @ well_orders ) ) ),
inference(simp,[status(thm)],[1096]) ).
thf(1098,plain,
! [A: $i] :
( ( A @ ( sk1 @ is_connected_in ) )
| ~ ( A @ ( sk1 @ well_orders ) ) ),
inference(pattern_uni,[status(thm)],[1097:[bind(A,$thf( sk1 ))]]) ).
thf(1109,plain,
! [A: $i] :
( ( A @ ( sk1 @ is_connected_in ) )
| ~ ( A @ ( sk1 @ well_orders ) ) ),
inference(simp,[status(thm)],[1098]) ).
thf(1113,plain,
! [A: $i] :
( ( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
!= ( A @ ( sk1 @ well_orders ) ) )
| ( A @ ( sk1 @ is_connected_in ) )
| ~ $true
| ( sk1 @ well_ordering ) ),
inference(paramod_ordered,[status(thm)],[20,1109]) ).
thf(1114,plain,
! [A: $i] :
( ( ( sk1 @ relation_field @ ( sk1 @ well_orders ) )
!= ( A @ ( sk1 @ well_orders ) ) )
| ( A @ ( sk1 @ is_connected_in ) )
| ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[1113]) ).
thf(1115,plain,
( ( sk1 @ relation_field @ ( sk1 @ is_connected_in ) )
| ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[1114:[bind(A,$thf( sk1 @ relation_field ))]]) ).
thf(34,plain,
! [A: $i] :
( ( A @ connected )
| ~ ( A @ relation_field @ ( A @ is_connected_in ) )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[32]) ).
thf(343,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ connected )
| ~ ( A @ relation_field @ ( A @ is_connected_in ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,34]) ).
thf(344,plain,
! [A: $i] :
( ( ( sk1 @ relation )
!= ( A @ relation ) )
| ( A @ connected )
| ~ ( A @ relation_field @ ( A @ is_connected_in ) ) ),
inference(simp,[status(thm)],[343]) ).
thf(345,plain,
( ( sk1 @ connected )
| ~ ( sk1 @ relation_field @ ( sk1 @ is_connected_in ) ) ),
inference(pattern_uni,[status(thm)],[344:[bind(A,$thf( sk1 ))]]) ).
thf(1143,plain,
( ( ( sk1 @ relation_field @ ( sk1 @ is_connected_in ) )
!= ( sk1 @ relation_field @ ( sk1 @ is_connected_in ) ) )
| ( sk1 @ connected )
| ~ $true
| ( sk1 @ well_ordering ) ),
inference(paramod_ordered,[status(thm)],[1115,345]) ).
thf(1144,plain,
( ( ( sk1 @ relation_field @ ( sk1 @ is_connected_in ) )
!= ( sk1 @ relation_field @ ( sk1 @ is_connected_in ) ) )
| ( sk1 @ connected )
| ( sk1 @ well_ordering ) ),
inference(simp,[status(thm)],[1143]) ).
thf(1145,plain,
( ( sk1 @ connected )
| ( sk1 @ well_ordering ) ),
inference(pattern_uni,[status(thm)],[1144:[]]) ).
thf(1502,plain,
( ( sk1 @ connected )
| $false ),
inference(rewrite,[status(thm)],[1145,1479]) ).
thf(1503,plain,
sk1 @ connected,
inference(simp,[status(thm)],[1502]) ).
thf(1642,plain,
( ~ ( sk1 @ well_founded_relation )
| ~ $true
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[1526,1491,1501,1503]) ).
thf(1643,plain,
~ ( sk1 @ well_founded_relation ),
inference(simp,[status(thm)],[1642]) ).
thf(1711,plain,
( $false
| ~ $true ),
inference(rewrite,[status(thm)],[1675,22,1643]) ).
thf(1712,plain,
$false,
inference(simp,[status(thm)],[1711]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU244+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.14/0.39 % Computer : n013.cluster.edu
% 0.14/0.39 % Model : x86_64 x86_64
% 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39 % Memory : 8046.5625MB
% 0.14/0.39 % OS : Linux 6.8.0-71-generic
% 0.14/0.39 % CPULimit : 300
% 0.14/0.39 % WCLimit : 300
% 0.14/0.39 % DateTime : Sat Sep 26 08:57:36 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.14/0.40 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.70/0.70 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 0.70/0.79 % [INFO] Parsing done (94ms).
% 0.96/0.80 % [INFO] Running in sequential loop mode.
% 1.21/0.98 % [INFO] eprover registered as external prover.
% 1.21/0.99 % [INFO] Scanning for conjecture ...
% 1.51/1.03 % [INFO] Found a conjecture (or negated_conjecture) and 14 axioms. Running axiom selection ...
% 1.51/1.05 % [INFO] Axiom selection finished. Selected 14 axioms (removed 0 axioms).
% 1.51/1.07 % [INFO] Problem is first-order (TPTP FOF).
% 1.51/1.07 % [INFO] Type checking passed.
% 1.51/1.08 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 13.50/4.24 % [INFO] Killing All external provers ...
% 13.50/4.25 % Time passed: 3746ms (effective reasoning time: 3438ms)
% 13.50/4.25 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 13.50/4.25 % Axioms used in derivation (7): d9_relat_2, d12_relat_2, d16_relat_2, d4_wellord1, d14_relat_2, d5_wellord1, t5_wellord1
% 13.50/4.25 % No. of inferences in proof: 197
% 13.50/4.25 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 3746 ms resp. 3438 ms w/o parsing
% 13.98/4.34 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 13.98/4.34 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------