%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SWV174+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n016.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:58:19 AM UTC 2026
% Result : Theorem 81.40s 34.46s
% Output : Refutation 67.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 97
% Syntax : Number of formulae : 700 ( 303 unt; 0 typ; 7 def)
% Number of atoms : 2250 ( 895 equ; 0 cnn)
% Maximal formula atoms : 40 ( 3 avg)
% Number of connectives : 6641 ( 911 ~; 695 |; 272 &;4611 @)
% ( 5 <=>; 147 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 5 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 45 ( 42 usr; 17 con; 0-4 aty)
% Number of variables : 883 ( 14 ^; 860 !; 2 ?; 883 :)
% ( 0 !>; 0 ?*; 0 @-; 7 @+)
% Comments :
%------------------------------------------------------------------------------
thf(leq_decl,type,
leq: $i > $i > $o ).
thf(n0_decl,type,
n0: $i ).
thf(pv10_decl,type,
pv10: $i ).
thf(n135299_decl,type,
n135299: $i ).
thf(pred_decl,type,
pred: $i > $i ).
thf(n4_decl,type,
n4: $i ).
thf(a_select3_decl,type,
a_select3: $i > $i > $i > $i ).
thf(q_init_decl,type,
q_init: $i ).
thf(init_decl,type,
init: $i ).
thf(center_init_decl,type,
center_init: $i ).
thf(gt_decl,type,
gt: $i > $i > $o ).
thf(plus_decl,type,
plus: $i > $i > $i ).
thf(n2_decl,type,
n2: $i ).
thf(succ_decl,type,
succ: $i > $i ).
thf(n3_decl,type,
n3: $i ).
thf(a_select2_decl,type,
a_select2: $i > $i > $i ).
thf(tptp_update2_decl,type,
tptp_update2: $i > $i > $i > $i ).
thf(n5_decl,type,
n5: $i ).
thf(n1_decl,type,
n1: $i ).
thf(tptp_minus_1_decl,type,
tptp_minus_1: $i ).
thf(sum_decl,type,
sum: $i > $i > $i > $i ).
thf(tptp_const_array2_decl,type,
tptp_const_array2: $i > $i > $i > $i ).
thf(dim_decl,type,
dim: $i > $i > $i ).
thf(tptp_mmul_decl,type,
tptp_mmul: $i > $i > $i ).
thf(trans_decl,type,
trans: $i > $i ).
thf(tptp_update3_decl,type,
tptp_update3: $i > $i > $i > $i > $i ).
thf(minus_decl,type,
minus: $i > $i > $i ).
thf(tptp_madd_decl,type,
tptp_madd: $i > $i > $i ).
thf(geq_decl,type,
geq: $i > $i > $o ).
thf(uniform_int_rnd_decl,type,
uniform_int_rnd: $i > $i > $i ).
thf(tptp_msub_decl,type,
tptp_msub: $i > $i > $i ).
thf(tptp_float_0_0_decl,type,
tptp_float_0_0: $i ).
thf(lt_decl,type,
lt: $i > $i > $o ).
thf(tptp_const_array1_decl,type,
tptp_const_array1: $i > $i > $i ).
thf(inv_decl,type,
inv: $i > $i ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $i > $i > $i > $i > $i ).
thf(sk4_decl,type,
sk4: $i > $i > $i > $i ).
thf(sk5_decl,type,
sk5: $i > $i > $i > $i ).
thf(sk6_decl,type,
sk6: $i > $i > $i ).
thf(sk7_decl,type,
sk7: $i > $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ! [B: $i] :
( ( ( n4 @ ( B @ leq ) )
& ( n135299 @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A @ ( pv10 @ gt ) )
=> ( ( B @ ( A @ ( q_init @ a_select3 ) ) )
= init ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ( ( ( n4 @ ( A @ leq ) )
& ( n135299 @ ( sk1 @ leq ) )
& ( A @ ( n0 @ leq ) )
& ( sk1 @ ( n0 @ leq ) ) )
=> ( ( sk1 @ ( pv10 @ gt ) )
=> ( ( A @ ( sk1 @ ( q_init @ a_select3 ) ) )
= init ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: $i,B: $i,C: $i,D: $i] :
@+[E: $i] :
~ ( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) ) )
=> ( ( E @ ( B @ a_select2 ) )
= A ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
~ ! [E: $i] :
( ( ( A @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( A @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( B @ a_select3 ) ) )
= ( D @ ( E @ ( B @ a_select3 ) ) ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
~ ( ( ( A @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( A @ ( C @ ( B @ ( A @ sk4 ) ) @ leq ) )
& ( C @ ( B @ ( A @ sk4 ) ) @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( B @ ( A @ sk4 ) ) @ ( B @ a_select3 ) ) )
= ( C @ ( B @ ( A @ sk4 ) ) @ ( D @ ( B @ a_select3 ) ) ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ! [D: $i] :
( ( ( A @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( A @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( B @ a_select3 ) ) )
= ( C @ ( D @ ( B @ a_select3 ) ) ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( ( A @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) )
& ( A @ ( B @ ( A @ sk6 ) @ leq ) )
& ( B @ ( A @ sk6 ) @ ( n0 @ leq ) ) )
=> ( ( C @ ( B @ ( A @ sk6 ) @ ( B @ a_select3 ) ) )
= ( B @ ( A @ sk6 ) @ ( C @ ( B @ a_select3 ) ) ) ) ) ) ) ).
thf(88,axiom,
n3 @ ( n4 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_4_3) ).
thf(563,plain,
n3 @ ( n4 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(16,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ gt ) )
=> ( B @ ( A @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leq_gt1) ).
thf(143,plain,
! [A: $i,B: $i] :
( ( A @ ( B @ gt ) )
=> ( B @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(144,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ~ ( A @ ( B @ gt ) ) ),
inference(cnf,[status(esa)],[143]) ).
thf(2755,plain,
! [B: $i,A: $i] :
( ( ( n3 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[563,144]) ).
thf(2756,plain,
! [B: $i,A: $i] :
( ( ( n3 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2755]) ).
thf(2757,plain,
n4 @ ( n3 @ leq ),
inference(pattern_uni,[status(thm)],[2756:[bind(A,$thf( n3 )),bind(B,$thf( n4 ))]]) ).
thf(1,conjecture,
( ( ! [A: $i] :
( ( ( n4 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( n0 @ ( A @ ( center_init @ a_select3 ) ) )
= init ) )
& ! [A: $i] :
( ( ( pv10 @ pred @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ! [B: $i] :
( ( ( n4 @ ( B @ leq ) )
& ( B @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( q_init @ a_select3 ) ) )
= init ) ) )
& ( n135299 @ ( pv10 @ leq ) )
& ( pv10 @ ( n0 @ leq ) ) )
=> ! [A: $i,B: $i] :
( ( ( n4 @ ( B @ leq ) )
& ( n135299 @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A @ ( pv10 @ gt ) )
=> ( ( B @ ( A @ ( q_init @ a_select3 ) ) )
= init ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cl5_nebula_init_0046) ).
thf(2,negated_conjecture,
~ ( ( ! [A: $i] :
( ( ( n4 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( n0 @ ( A @ ( center_init @ a_select3 ) ) )
= init ) )
& ! [A: $i] :
( ( ( pv10 @ pred @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ! [B: $i] :
( ( ( n4 @ ( B @ leq ) )
& ( B @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( q_init @ a_select3 ) ) )
= init ) ) )
& ( n135299 @ ( pv10 @ leq ) )
& ( pv10 @ ( n0 @ leq ) ) )
=> ! [A: $i,B: $i] :
( ( ( n4 @ ( B @ leq ) )
& ( n135299 @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A @ ( pv10 @ gt ) )
=> ( ( B @ ( A @ ( q_init @ a_select3 ) ) )
= init ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(92,plain,
~ ( ( ! [A: $i] :
( ( ( n4 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( n0 @ ( A @ ( center_init @ a_select3 ) ) )
= init ) )
& ! [A: $i] :
( ( ( pv10 @ pred @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ! [B: $i] :
( ( ( n4 @ ( B @ leq ) )
& ( B @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( q_init @ a_select3 ) ) )
= init ) ) )
& ( n135299 @ ( pv10 @ leq ) )
& ( pv10 @ ( n0 @ leq ) ) )
=> ! [A: $i,B: $i] :
( ( ( n4 @ ( B @ leq ) )
& ( n135299 @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A @ ( pv10 @ gt ) )
=> ( ( B @ ( A @ ( q_init @ a_select3 ) ) )
= init ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(93,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ ( q_init @ a_select3 ) ) )
!= init )
& ( sk1 @ ( pv10 @ gt ) )
& ( n4 @ ( sk2 @ leq ) )
& ( n135299 @ ( sk1 @ leq ) )
& ( sk2 @ ( n0 @ leq ) )
& ( sk1 @ ( n0 @ leq ) )
& ( ( ( n0 @ ( C @ ( center_init @ a_select3 ) ) )
= init )
| ~ ( n4 @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) ) )
& ( ( ( B @ ( A @ ( q_init @ a_select3 ) ) )
= init )
| ~ ( n4 @ ( B @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( pv10 @ pred @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) )
& ( n135299 @ ( pv10 @ leq ) )
& ( pv10 @ ( n0 @ leq ) ) ),
inference(cnf,[status(esa)],[92]) ).
thf(101,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( q_init @ a_select3 ) ) )
= init )
| ~ ( n4 @ ( B @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( pv10 @ pred @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[93]) ).
thf(104,plain,
! [B: $i,A: $i] :
( ~ ( n4 @ ( B @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( pv10 @ pred @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( B @ ( A @ ( q_init @ a_select3 ) ) )
= init ) ),
inference(lifteq,[status(thm)],[101]) ).
thf(103,plain,
( ( sk2 @ ( sk1 @ ( q_init @ a_select3 ) ) )
!= init ),
inference(cnfConj,[status(thm)],[93]) ).
thf(105,plain,
( ( sk2 @ ( sk1 @ ( q_init @ a_select3 ) ) )
!= init ),
inference(lifteq,[status(thm)],[103]) ).
thf(1092,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( q_init @ a_select3 ) ) )
!= ( sk2 @ ( sk1 @ ( q_init @ a_select3 ) ) ) )
| ( init != init )
| ~ ( n4 @ ( B @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( pv10 @ pred @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[104,105]) ).
thf(1093,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( q_init @ a_select3 ) ) )
!= ( sk2 @ ( sk1 @ ( q_init @ a_select3 ) ) ) )
| ~ ( n4 @ ( B @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( pv10 @ pred @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[1092]) ).
thf(1094,plain,
( ~ ( n4 @ ( sk2 @ leq ) )
| ~ ( sk2 @ ( n0 @ leq ) )
| ~ ( pv10 @ pred @ ( sk1 @ leq ) )
| ~ ( sk1 @ ( n0 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[1093:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(96,plain,
sk1 @ ( n0 @ leq ),
inference(cnfConj,[status(thm)],[93]) ).
thf(102,plain,
sk2 @ ( n0 @ leq ),
inference(cnfConj,[status(thm)],[93]) ).
thf(94,plain,
n4 @ ( sk2 @ leq ),
inference(cnfConj,[status(thm)],[93]) ).
thf(1917,plain,
( ~ $true
| ~ $true
| ~ ( pv10 @ pred @ ( sk1 @ leq ) )
| ~ $true ),
inference(rewrite,[status(thm)],[1094,96,102,94]) ).
thf(1918,plain,
~ ( pv10 @ pred @ ( sk1 @ leq ) ),
inference(simp,[status(thm)],[1917]) ).
thf(5354,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n4 @ ( n3 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2757,1918]) ).
thf(5355,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n4 @ ( n3 @ leq ) ) ),
inference(simp,[status(thm)],[5354]) ).
thf(5385,plain,
( ( ( pv10 @ pred )
!= n4 )
| ( sk1 != n3 ) ),
inference(simp,[status(thm)],[5355]) ).
thf(28,axiom,
n0 @ ( n135299 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_135299_0) ).
thf(169,plain,
n0 @ ( n135299 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(45,axiom,
! [A: $i] :
~ ( A @ ( A @ gt ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',irreflexivity_gt) ).
thf(335,plain,
! [A: $i] :
~ ( A @ ( A @ gt ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(336,plain,
~ ? [A: $i] : ( A @ ( A @ gt ) ),
inference(miniscope,[status(thm)],[335]) ).
thf(337,plain,
! [A: $i] :
~ ( A @ ( A @ gt ) ),
inference(cnf,[status(esa)],[336]) ).
thf(1451,plain,
! [A: $i] :
( ( ( n0 @ ( n135299 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[169,337]) ).
thf(1452,plain,
! [A: $i] :
( ( n0 @ ( n135299 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1451]) ).
thf(1453,plain,
! [A: $i] :
( ( n0 != A )
| ( n135299 != A ) ),
inference(simp,[status(thm)],[1452]) ).
thf(1454,plain,
n135299 != n0,
inference(simp,[status(thm)],[1453]) ).
thf(61,axiom,
! [A: $i,B: $i,C: $i] :
( ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( B @ a_select3 ) ) )
= ( D @ ( E @ ( B @ a_select3 ) ) ) ) )
=> ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( D @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',matrix_symm_aba1) ).
thf(479,plain,
! [A: $i,B: $i,C: $i] :
( ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( B @ a_select3 ) ) )
= ( D @ ( E @ ( B @ a_select3 ) ) ) ) )
=> ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( D @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(83,axiom,
tptp_minus_1 @ ( n3 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_3_tptp_minus_1) ).
thf(555,plain,
tptp_minus_1 @ ( n3 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(18,axiom,
( ( n0 @ succ )
= n1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_1) ).
thf(146,plain,
( ( n0 @ succ )
= n1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(147,plain,
( ( n0 @ succ )
= n1 ),
inference(lifteq,[status(thm)],[146]) ).
thf(89,axiom,
! [A: $i] :
( ( A @ succ @ pred )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pred_succ) ).
thf(564,plain,
! [A: $i] :
( ( A @ succ @ pred )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(565,plain,
! [A: $i] :
( ( A @ succ @ pred )
= A ),
inference(cnf,[status(esa)],[564]) ).
thf(566,plain,
! [A: $i] :
( ( A @ succ @ pred )
= A ),
inference(lifteq,[status(thm)],[565]) ).
thf(19450,plain,
! [A: $i] :
( ( ( n0 @ succ )
!= ( A @ succ ) )
| ( ( n1 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[147,566]) ).
thf(19451,plain,
( ( n1 @ pred )
= n0 ),
inference(pattern_uni,[status(thm)],[19450:[bind(A,$thf( n0 ))]]) ).
thf(51,axiom,
n0 @ ( n3 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_3_0) ).
thf(400,plain,
n0 @ ( n3 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(1630,plain,
! [A: $i] :
( ( ( n0 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[400,337]) ).
thf(1631,plain,
! [A: $i] :
( ( n0 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1630]) ).
thf(1632,plain,
! [A: $i] :
( ( n0 != A )
| ( n3 != A ) ),
inference(simp,[status(thm)],[1631]) ).
thf(1633,plain,
n3 != n0,
inference(simp,[status(thm)],[1632]) ).
thf(2776,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[400,144]) ).
thf(2777,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2776]) ).
thf(2778,plain,
n3 @ ( n0 @ leq ),
inference(pattern_uni,[status(thm)],[2777:[bind(A,$thf( n0 )),bind(B,$thf( n3 ))]]) ).
thf(62,axiom,
tptp_minus_1 @ ( n135299 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_135299_tptp_minus_1) ).
thf(491,plain,
tptp_minus_1 @ ( n135299 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(2785,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n135299 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[491,144]) ).
thf(2786,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n135299 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2785]) ).
thf(2787,plain,
n135299 @ ( tptp_minus_1 @ leq ),
inference(pattern_uni,[status(thm)],[2786:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n135299 ))]]) ).
thf(70,axiom,
! [A: $i] :
( ( ( n2 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_2) ).
thf(518,plain,
! [A: $i] :
( ( ( n2 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(72,axiom,
! [A: $i,B: $i] :
( ! [C: $i,D: $i] :
( ( ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( A @ a_select3 ) ) )
= ( C @ ( D @ ( A @ a_select3 ) ) ) ) )
=> ! [C: $i,D: $i] :
( ( ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( A @ inv @ a_select3 ) ) )
= ( C @ ( D @ ( A @ inv @ a_select3 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',matrix_symm_inv) ).
thf(523,plain,
! [A: $i,B: $i] :
( ! [C: $i,D: $i] :
( ( ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( A @ a_select3 ) ) )
= ( C @ ( D @ ( A @ a_select3 ) ) ) ) )
=> ! [C: $i,D: $i] :
( ( ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( A @ inv @ a_select3 ) ) )
= ( C @ ( D @ ( A @ inv @ a_select3 ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(24,axiom,
n1 @ ( n4 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_4_1) ).
thf(163,plain,
n1 @ ( n4 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(2782,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[163,144]) ).
thf(2783,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2782]) ).
thf(2784,plain,
n4 @ ( n1 @ leq ),
inference(pattern_uni,[status(thm)],[2783:[bind(A,$thf( n1 )),bind(B,$thf( n4 ))]]) ).
thf(8654,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n4 @ ( n1 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2784,1918]) ).
thf(8655,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n4 @ ( n1 @ leq ) ) ),
inference(simp,[status(thm)],[8654]) ).
thf(8695,plain,
( ( ( pv10 @ pred )
!= n4 )
| ( sk1 != n1 ) ),
inference(simp,[status(thm)],[8655]) ).
thf(85,axiom,
( ( n0 @ succ @ succ @ succ @ succ @ succ )
= n5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_5) ).
thf(557,plain,
( ( n0 @ succ @ succ @ succ @ succ @ succ )
= n5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(558,plain,
( ( n0 @ succ @ succ @ succ @ succ @ succ )
= n5 ),
inference(lifteq,[status(thm)],[557]) ).
thf(9818,plain,
( ( n1 @ succ @ succ @ succ @ succ )
= n5 ),
inference(rewrite,[status(thm)],[558,147]) ).
thf(55,axiom,
n2 @ ( n135299 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_135299_2) ).
thf(408,plain,
n2 @ ( n135299 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(29,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i] :
( ( ( F @ ( D @ leq ) )
& ( D @ ( E @ leq ) )
& ( C @ ( A @ leq ) )
& ( A @ ( B @ leq ) ) )
=> ( ( D @ ( A @ ( G @ ( F @ ( E @ dim ) @ ( C @ ( B @ dim ) @ tptp_const_array2 ) ) @ a_select3 ) ) )
= G ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',const_array2_select) ).
thf(170,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i] :
( ( ( F @ ( D @ leq ) )
& ( D @ ( E @ leq ) )
& ( C @ ( A @ leq ) )
& ( A @ ( B @ leq ) ) )
=> ( ( D @ ( A @ ( G @ ( F @ ( E @ dim ) @ ( C @ ( B @ dim ) @ tptp_const_array2 ) ) @ a_select3 ) ) )
= G ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(36,axiom,
tptp_minus_1 @ ( n0 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_0_tptp_minus_1) ).
thf(222,plain,
tptp_minus_1 @ ( n0 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(2788,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n0 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[222,144]) ).
thf(2789,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n0 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2788]) ).
thf(2790,plain,
n0 @ ( tptp_minus_1 @ leq ),
inference(pattern_uni,[status(thm)],[2789:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n0 ))]]) ).
thf(8924,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n0 @ ( tptp_minus_1 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2790,1918]) ).
thf(8925,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n0 @ ( tptp_minus_1 @ leq ) ) ),
inference(simp,[status(thm)],[8924]) ).
thf(8963,plain,
( ( ( pv10 @ pred )
!= n0 )
| ( sk1 != tptp_minus_1 ) ),
inference(simp,[status(thm)],[8925]) ).
thf(80,axiom,
! [A: $i] : ( A @ ( A @ succ @ gt ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_succ) ).
thf(549,plain,
! [A: $i] : ( A @ ( A @ succ @ gt ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(550,plain,
! [A: $i] : ( A @ ( A @ succ @ gt ) ),
inference(cnf,[status(esa)],[549]) ).
thf(15,axiom,
n5 @ ( n135299 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_135299_5) ).
thf(142,plain,
n5 @ ( n135299 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(2710,plain,
! [B: $i,A: $i] :
( ( ( n5 @ ( n135299 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[142,144]) ).
thf(2711,plain,
! [B: $i,A: $i] :
( ( ( n5 @ ( n135299 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2710]) ).
thf(2712,plain,
n135299 @ ( n5 @ leq ),
inference(pattern_uni,[status(thm)],[2711:[bind(A,$thf( n5 )),bind(B,$thf( n135299 ))]]) ).
thf(20,axiom,
tptp_minus_1 @ ( n2 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_2_tptp_minus_1) ).
thf(150,plain,
tptp_minus_1 @ ( n2 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(1230,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[150,337]) ).
thf(1231,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1230]) ).
thf(1232,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n2 != A ) ),
inference(simp,[status(thm)],[1231]) ).
thf(1233,plain,
tptp_minus_1 != n2,
inference(simp,[status(thm)],[1232]) ).
thf(8332,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n3 @ ( n0 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2778,1918]) ).
thf(8333,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n3 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[8332]) ).
thf(8370,plain,
( ( ( pv10 @ pred )
!= n3 )
| ( sk1 != n0 ) ),
inference(simp,[status(thm)],[8333]) ).
thf(75,axiom,
! [A: $i] :
( ( A @ ( n4 @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',succ_plus_4_l) ).
thf(538,plain,
! [A: $i] :
( ( A @ ( n4 @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(98,plain,
pv10 @ ( n0 @ leq ),
inference(cnfConj,[status(thm)],[93]) ).
thf(95,plain,
! [A: $i] :
( ( ( n0 @ ( A @ ( center_init @ a_select3 ) ) )
= init )
| ~ ( n4 @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[93]) ).
thf(106,plain,
! [A: $i] :
( ~ ( n4 @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( n0 @ ( A @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(lifteq,[status(thm)],[95]) ).
thf(107,plain,
! [A: $i] :
( ~ ( n4 @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( n0 @ ( A @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[106]) ).
thf(951,plain,
! [A: $i] :
( ( ( pv10 @ ( n0 @ leq ) )
!= ( A @ ( n0 @ leq ) ) )
| ~ ( n4 @ ( A @ leq ) )
| ~ $true
| ( ( n0 @ ( A @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(paramod_ordered,[status(thm)],[98,107]) ).
thf(952,plain,
! [A: $i] :
( ( ( pv10 @ ( n0 @ leq ) )
!= ( A @ ( n0 @ leq ) ) )
| ~ ( n4 @ ( A @ leq ) )
| ( ( n0 @ ( A @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[951]) ).
thf(953,plain,
( ~ ( n4 @ ( pv10 @ leq ) )
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(pattern_uni,[status(thm)],[952:[bind(A,$thf( pv10 ))]]) ).
thf(1465,plain,
( ( ( n4 @ ( pv10 @ leq ) )
!= ( sk2 @ ( n0 @ leq ) ) )
| ~ $true
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(paramod_ordered,[status(thm)],[102,953]) ).
thf(1466,plain,
( ( ( n4 @ ( pv10 @ leq ) )
!= ( sk2 @ ( n0 @ leq ) ) )
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[1465]) ).
thf(1507,plain,
( ( sk2 != n4 )
| ( pv10 != n0 )
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[1466]) ).
thf(33,axiom,
n3 @ ( n5 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_5_3) ).
thf(206,plain,
n3 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(1455,plain,
! [A: $i] :
( ( ( n3 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[206,337]) ).
thf(1456,plain,
! [A: $i] :
( ( n3 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1455]) ).
thf(1457,plain,
! [A: $i] :
( ( n3 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[1456]) ).
thf(1458,plain,
n5 != n3,
inference(simp,[status(thm)],[1457]) ).
thf(30,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ! [E: $i,F: $i] :
( ( ( D @ ( F @ leq ) )
& ( F @ ( n0 @ leq ) )
& ( D @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) ) )
=> ( ( F @ ( E @ ( B @ a_select3 ) ) )
= ( E @ ( F @ ( B @ a_select3 ) ) ) ) )
=> ! [E: $i,F: $i] :
( ( ( C @ ( F @ leq ) )
& ( F @ ( n0 @ leq ) )
& ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) ) )
=> ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',matrix_symm_aba2) ).
thf(174,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ! [E: $i,F: $i] :
( ( ( D @ ( F @ leq ) )
& ( F @ ( n0 @ leq ) )
& ( D @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) ) )
=> ( ( F @ ( E @ ( B @ a_select3 ) ) )
= ( E @ ( F @ ( B @ a_select3 ) ) ) ) )
=> ! [E: $i,F: $i] :
( ( ( C @ ( F @ leq ) )
& ( F @ ( n0 @ leq ) )
& ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) ) )
=> ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(175,plain,
! [A: $i,B: $i] :
( ? [C: $i] :
! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( B @ a_select3 ) ) )
= ( D @ ( E @ ( B @ a_select3 ) ) ) ) )
=> ! [C: $i,D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( D @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) ) ) ),
inference(miniscope,[status(thm)],[174]) ).
thf(176,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) )
| ~ ( D @ ( F @ leq ) )
| ~ ( F @ ( n0 @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ( ( A @ ( B @ ( C @ sk5 ) ) @ ( A @ ( B @ ( C @ sk4 ) ) @ ( B @ a_select3 ) ) )
!= ( A @ ( B @ ( C @ sk4 ) ) @ ( A @ ( B @ ( C @ sk5 ) ) @ ( B @ a_select3 ) ) ) ) )
& ( ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) )
| ~ ( D @ ( F @ leq ) )
| ~ ( F @ ( n0 @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ( C @ ( A @ ( B @ ( C @ sk5 ) ) @ leq ) ) )
& ( ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) )
| ~ ( D @ ( F @ leq ) )
| ~ ( F @ ( n0 @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ( A @ ( B @ ( C @ sk5 ) ) @ ( n0 @ leq ) ) )
& ( ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) )
| ~ ( D @ ( F @ leq ) )
| ~ ( F @ ( n0 @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ( C @ ( A @ ( B @ ( C @ sk4 ) ) @ leq ) ) )
& ( ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) )
| ~ ( D @ ( F @ leq ) )
| ~ ( F @ ( n0 @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ( A @ ( B @ ( C @ sk4 ) ) @ ( n0 @ leq ) ) ) ),
inference(cnf,[status(esa)],[175]) ).
thf(177,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) )
| ~ ( D @ ( F @ leq ) )
| ~ ( F @ ( n0 @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ( A @ ( B @ ( C @ sk5 ) ) @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[176]) ).
thf(185,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( F @ leq ) )
| ~ ( F @ ( n0 @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ( A @ ( B @ ( C @ sk5 ) ) @ ( n0 @ leq ) )
| ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[177]) ).
thf(81,axiom,
n4 @ ( n5 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_5_4) ).
thf(551,plain,
n4 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(2731,plain,
! [B: $i,A: $i] :
( ( ( n4 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[551,144]) ).
thf(2732,plain,
! [B: $i,A: $i] :
( ( ( n4 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2731]) ).
thf(2733,plain,
n5 @ ( n4 @ leq ),
inference(pattern_uni,[status(thm)],[2732:[bind(A,$thf( n4 )),bind(B,$thf( n5 ))]]) ).
thf(3960,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n5 @ ( n4 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2733,1918]) ).
thf(3961,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n5 @ ( n4 @ leq ) ) ),
inference(simp,[status(thm)],[3960]) ).
thf(3994,plain,
( ( ( pv10 @ pred )
!= n5 )
| ( sk1 != n4 ) ),
inference(simp,[status(thm)],[3961]) ).
thf(2761,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n2 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[150,144]) ).
thf(2762,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n2 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2761]) ).
thf(2763,plain,
n2 @ ( tptp_minus_1 @ leq ),
inference(pattern_uni,[status(thm)],[2762:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n2 ))]]) ).
thf(1484,plain,
( ( ( n4 @ ( pv10 @ leq ) )
!= ( pv10 @ ( n0 @ leq ) ) )
| ~ $true
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(paramod_ordered,[status(thm)],[98,953]) ).
thf(1485,plain,
( ( ( n4 @ ( pv10 @ leq ) )
!= ( pv10 @ ( n0 @ leq ) ) )
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[1484]) ).
thf(1518,plain,
( ( n4 != pv10 )
| ( pv10 != n0 )
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[1485]) ).
thf(53,axiom,
n2 @ ( n5 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_5_2) ).
thf(404,plain,
n2 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(181,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) )
| ~ ( D @ ( F @ leq ) )
| ~ ( F @ ( n0 @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ( C @ ( A @ ( B @ ( C @ sk4 ) ) @ leq ) ) ),
inference(cnfConj,[status(thm)],[176]) ).
thf(184,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( F @ leq ) )
| ~ ( F @ ( n0 @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ( C @ ( A @ ( B @ ( C @ sk4 ) ) @ leq ) )
| ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[181]) ).
thf(3,axiom,
! [A: $i] :
( ( n2 @ ( A @ plus ) )
= ( A @ succ @ succ ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',succ_plus_2_r) ).
thf(108,plain,
! [A: $i] :
( ( n2 @ ( A @ plus ) )
= ( A @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(109,plain,
! [A: $i] :
( ( n2 @ ( A @ plus ) )
= ( A @ succ @ succ ) ),
inference(cnf,[status(esa)],[108]) ).
thf(110,plain,
! [A: $i] :
( ( n2 @ ( A @ plus ) )
= ( A @ succ @ succ ) ),
inference(lifteq,[status(thm)],[109]) ).
thf(2713,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[404,144]) ).
thf(2714,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2713]) ).
thf(2715,plain,
n5 @ ( n2 @ leq ),
inference(pattern_uni,[status(thm)],[2714:[bind(A,$thf( n2 )),bind(B,$thf( n5 ))]]) ).
thf(3121,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n5 @ ( n2 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2715,1918]) ).
thf(3122,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n5 @ ( n2 @ leq ) ) ),
inference(simp,[status(thm)],[3121]) ).
thf(3148,plain,
( ( ( pv10 @ pred )
!= n5 )
| ( sk1 != n2 ) ),
inference(simp,[status(thm)],[3122]) ).
thf(8,axiom,
! [A: $i] :
( ( A @ ( n2 @ plus ) )
= ( A @ succ @ succ ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',succ_plus_2_l) ).
thf(125,plain,
! [A: $i] :
( ( A @ ( n2 @ plus ) )
= ( A @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(1310,plain,
! [A: $i] :
( ( ( n1 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[163,337]) ).
thf(1311,plain,
! [A: $i] :
( ( n1 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1310]) ).
thf(1312,plain,
! [A: $i] :
( ( n1 != A )
| ( n4 != A ) ),
inference(simp,[status(thm)],[1311]) ).
thf(1313,plain,
n1 != n4,
inference(simp,[status(thm)],[1312]) ).
thf(31,axiom,
! [A: $i,B: $i] :
( ! [C: $i,D: $i] :
( ( ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( A @ a_select3 ) ) )
= ( C @ ( D @ ( A @ a_select3 ) ) ) ) )
=> ! [C: $i,D: $i,E: $i,F: $i] :
( ( ( B @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',matrix_symm_update_diagonal) ).
thf(187,plain,
! [A: $i,B: $i] :
( ! [C: $i,D: $i] :
( ( ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( A @ a_select3 ) ) )
= ( C @ ( D @ ( A @ a_select3 ) ) ) ) )
=> ! [C: $i,D: $i,E: $i,F: $i] :
( ( ( B @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(188,plain,
! [A: $i,B: $i] :
( ! [C: $i,D: $i] :
( ( ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( A @ a_select3 ) ) )
= ( C @ ( D @ ( A @ a_select3 ) ) ) ) )
=> ! [C: $i,D: $i,E: $i] :
( ( ( B @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ! [F: $i] :
( ( D @ ( C @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) ) ) ) ),
inference(miniscope,[status(thm)],[187]) ).
thf(189,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( ( D @ ( C @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) ) )
| ~ ( B @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ~ ( B @ ( D @ leq ) )
| ~ ( D @ ( n0 @ leq ) )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ( ( A @ ( B @ sk7 ) @ ( A @ ( B @ sk6 ) @ ( A @ a_select3 ) ) )
!= ( A @ ( B @ sk6 ) @ ( A @ ( B @ sk7 ) @ ( A @ a_select3 ) ) ) ) )
& ( ( ( D @ ( C @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) ) )
| ~ ( B @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ~ ( B @ ( D @ leq ) )
| ~ ( D @ ( n0 @ leq ) )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ( B @ ( A @ ( B @ sk7 ) @ leq ) ) )
& ( ( ( D @ ( C @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) ) )
| ~ ( B @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ~ ( B @ ( D @ leq ) )
| ~ ( D @ ( n0 @ leq ) )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ( A @ ( B @ sk7 ) @ ( n0 @ leq ) ) )
& ( ( ( D @ ( C @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) ) )
| ~ ( B @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ~ ( B @ ( D @ leq ) )
| ~ ( D @ ( n0 @ leq ) )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ( B @ ( A @ ( B @ sk6 ) @ leq ) ) )
& ( ( ( D @ ( C @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) ) )
| ~ ( B @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ~ ( B @ ( D @ leq ) )
| ~ ( D @ ( n0 @ leq ) )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ( A @ ( B @ sk6 ) @ ( n0 @ leq ) ) ) ),
inference(cnf,[status(esa)],[188]) ).
thf(193,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) ) )
| ~ ( B @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ~ ( B @ ( D @ leq ) )
| ~ ( D @ ( n0 @ leq ) )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ( A @ ( B @ sk6 ) @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[189]) ).
thf(196,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ~ ( B @ ( D @ leq ) )
| ~ ( D @ ( n0 @ leq ) )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ( A @ ( B @ sk6 ) @ ( n0 @ leq ) )
| ( ( D @ ( C @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[193]) ).
thf(87,axiom,
n1 @ ( n5 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_5_1) ).
thf(562,plain,
n1 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(2743,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[562,144]) ).
thf(2744,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2743]) ).
thf(2745,plain,
n5 @ ( n1 @ leq ),
inference(pattern_uni,[status(thm)],[2744:[bind(A,$thf( n1 )),bind(B,$thf( n5 ))]]) ).
thf(77,axiom,
! [A: $i] : ( A @ ( A @ leq ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_leq) ).
thf(542,plain,
! [A: $i] : ( A @ ( A @ leq ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(22,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( B @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) )
& ! [E: $i] :
( ( ( B @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) ) )
=> ( ( E @ ( C @ a_select2 ) )
= D ) ) )
=> ( ( A @ ( D @ ( B @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sel2_update_3) ).
thf(152,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( B @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) )
& ! [E: $i] :
( ( ( B @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) ) )
=> ( ( E @ ( C @ a_select2 ) )
= D ) ) )
=> ( ( A @ ( D @ ( B @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(153,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( ( A @ ( D @ ( B @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D )
| ~ ( B @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( A @ ( B @ ( C @ ( D @ sk3 ) ) ) @ ( C @ a_select2 ) )
!= D ) )
& ( ( ( A @ ( D @ ( B @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D )
| ~ ( B @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( B @ ( A @ ( B @ ( C @ ( D @ sk3 ) ) ) @ leq ) ) )
& ( ( ( A @ ( D @ ( B @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D )
| ~ ( B @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( A @ ( B @ ( C @ ( D @ sk3 ) ) ) @ ( n0 @ leq ) ) ) ),
inference(cnf,[status(esa)],[152]) ).
thf(154,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( D @ ( B @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D )
| ~ ( B @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( A @ ( B @ ( C @ ( D @ sk3 ) ) ) @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[153]) ).
thf(157,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( A @ ( B @ ( C @ ( D @ sk3 ) ) ) @ ( n0 @ leq ) )
| ( ( A @ ( D @ ( B @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D ) ),
inference(lifteq,[status(thm)],[154]) ).
thf(86,axiom,
! [A: $i] :
( ( ( n5 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n5 )
| ( A = n4 )
| ( A = n3 )
| ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_5) ).
thf(559,plain,
! [A: $i] :
( ( ( n5 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n5 )
| ( A = n4 )
| ( A = n3 )
| ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(17,axiom,
n1 @ ( n3 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_3_1) ).
thf(145,plain,
n1 @ ( n3 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(2758,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[145,144]) ).
thf(2759,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2758]) ).
thf(2760,plain,
n3 @ ( n1 @ leq ),
inference(pattern_uni,[status(thm)],[2759:[bind(A,$thf( n1 )),bind(B,$thf( n3 ))]]) ).
thf(5480,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n3 @ ( n1 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2760,1918]) ).
thf(5481,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n3 @ ( n1 @ leq ) ) ),
inference(simp,[status(thm)],[5480]) ).
thf(5521,plain,
( ( ( pv10 @ pred )
!= n3 )
| ( sk1 != n1 ) ),
inference(simp,[status(thm)],[5481]) ).
thf(65,axiom,
( ( n0 @ succ @ succ @ succ )
= n3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_3) ).
thf(499,plain,
( ( n0 @ succ @ succ @ succ )
= n3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(500,plain,
( ( n0 @ succ @ succ @ succ )
= n3 ),
inference(lifteq,[status(thm)],[499]) ).
thf(2132,plain,
( ( n1 @ succ @ succ )
= n3 ),
inference(rewrite,[status(thm)],[500,147]) ).
thf(19,axiom,
( ( n0 @ succ @ succ @ succ @ succ )
= n4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_4) ).
thf(148,plain,
( ( n0 @ succ @ succ @ succ @ succ )
= n4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(149,plain,
( ( n0 @ succ @ succ @ succ @ succ )
= n4 ),
inference(lifteq,[status(thm)],[148]) ).
thf(2511,plain,
( ( n1 @ succ @ succ @ succ )
= n4 ),
inference(rewrite,[status(thm)],[149,147]) ).
thf(2519,plain,
( ( ( n1 @ succ @ succ )
!= ( n1 @ succ @ succ ) )
| ( ( n3 @ succ )
= n4 ) ),
inference(paramod_ordered,[status(thm)],[2132,2511]) ).
thf(2520,plain,
( ( n3 @ succ )
= n4 ),
inference(pattern_uni,[status(thm)],[2519:[]]) ).
thf(19447,plain,
! [A: $i] :
( ( ( n3 @ succ )
!= ( A @ succ ) )
| ( ( n4 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[2520,566]) ).
thf(19448,plain,
( ( n4 @ pred )
= n3 ),
inference(pattern_uni,[status(thm)],[19447:[bind(A,$thf( n3 ))]]) ).
thf(13,axiom,
n2 @ ( n3 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_3_2) ).
thf(140,plain,
n2 @ ( n3 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(2752,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[140,144]) ).
thf(2753,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2752]) ).
thf(2754,plain,
n3 @ ( n2 @ leq ),
inference(pattern_uni,[status(thm)],[2753:[bind(A,$thf( n2 )),bind(B,$thf( n3 ))]]) ).
thf(5230,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n3 @ ( n2 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2754,1918]) ).
thf(5231,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n3 @ ( n2 @ leq ) ) ),
inference(simp,[status(thm)],[5230]) ).
thf(5271,plain,
( ( ( pv10 @ pred )
!= n3 )
| ( sk1 != n2 ) ),
inference(simp,[status(thm)],[5231]) ).
thf(19581,plain,
( ( ( n4 @ pred )
!= ( pv10 @ pred ) )
| ( n3 != n3 )
| ( sk1 != n2 ) ),
inference(paramod_ordered,[status(thm)],[19448,5271]) ).
thf(19582,plain,
( ( ( n4 @ pred )
!= ( pv10 @ pred ) )
| ( sk1 != n2 ) ),
inference(simp,[status(thm)],[19581]) ).
thf(19604,plain,
( ( n4 != pv10 )
| ( sk1 != n2 ) ),
inference(simp,[status(thm)],[19582]) ).
thf(25,axiom,
n2 @ ( n4 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_4_2) ).
thf(164,plain,
n2 @ ( n4 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(2719,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[164,144]) ).
thf(2720,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2719]) ).
thf(2721,plain,
n4 @ ( n2 @ leq ),
inference(pattern_uni,[status(thm)],[2720:[bind(A,$thf( n2 )),bind(B,$thf( n4 ))]]) ).
thf(3633,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n4 @ ( n2 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2721,1918]) ).
thf(3634,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n4 @ ( n2 @ leq ) ) ),
inference(simp,[status(thm)],[3633]) ).
thf(3657,plain,
( ( ( pv10 @ pred )
!= n4 )
| ( sk1 != n2 ) ),
inference(simp,[status(thm)],[3634]) ).
thf(97,plain,
sk1 @ ( pv10 @ gt ),
inference(cnfConj,[status(thm)],[93]) ).
thf(2728,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( pv10 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[97,144]) ).
thf(2729,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( pv10 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2728]) ).
thf(2730,plain,
pv10 @ ( sk1 @ leq ),
inference(pattern_uni,[status(thm)],[2729:[bind(A,$thf( sk1 )),bind(B,$thf( pv10 ))]]) ).
thf(26,axiom,
n4 @ ( n135299 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_135299_4) ).
thf(165,plain,
n4 @ ( n135299 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(1447,plain,
! [A: $i] :
( ( ( n4 @ ( n135299 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[165,337]) ).
thf(1448,plain,
! [A: $i] :
( ( n4 @ ( n135299 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1447]) ).
thf(1449,plain,
! [A: $i] :
( ( n4 != A )
| ( n135299 != A ) ),
inference(simp,[status(thm)],[1448]) ).
thf(1450,plain,
n4 != n135299,
inference(simp,[status(thm)],[1449]) ).
thf(90,axiom,
n0 @ ( n4 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_4_0) ).
thf(567,plain,
n0 @ ( n4 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).
thf(2746,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[567,144]) ).
thf(2747,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2746]) ).
thf(2748,plain,
n4 @ ( n0 @ leq ),
inference(pattern_uni,[status(thm)],[2747:[bind(A,$thf( n0 )),bind(B,$thf( n4 ))]]) ).
thf(4784,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n4 @ ( n0 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2748,1918]) ).
thf(4785,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n4 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[4784]) ).
thf(4820,plain,
( ( ( pv10 @ pred )
!= n4 )
| ( sk1 != n0 ) ),
inference(simp,[status(thm)],[4785]) ).
thf(6,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( ( B @ ( C @ a_select2 ) )
= D )
& ( A != B ) )
=> ( ( B @ ( E @ ( A @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sel2_update_2) ).
thf(117,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( ( B @ ( C @ a_select2 ) )
= D )
& ( A != B ) )
=> ( ( B @ ( E @ ( A @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(118,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( ( B @ ( C @ a_select2 ) )
= D )
& ( A != B ) )
=> ! [E: $i] :
( ( B @ ( E @ ( A @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D ) ),
inference(miniscope,[status(thm)],[117]) ).
thf(119,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( E @ ( A @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D )
| ( ( B @ ( C @ a_select2 ) )
!= D )
| ( A = B ) ),
inference(cnf,[status(esa)],[118]) ).
thf(120,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( E @ ( A @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D )
| ( ( B @ ( C @ a_select2 ) )
!= D )
| ( A = B ) ),
inference(lifteq,[status(thm)],[119]) ).
thf(121,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( D @ ( A @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= ( B @ ( C @ a_select2 ) ) )
| ( A = B ) ),
inference(simp,[status(thm)],[120]) ).
thf(191,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) ) )
| ~ ( B @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ~ ( B @ ( D @ leq ) )
| ~ ( D @ ( n0 @ leq ) )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ( ( A @ ( B @ sk7 ) @ ( A @ ( B @ sk6 ) @ ( A @ a_select3 ) ) )
!= ( A @ ( B @ sk6 ) @ ( A @ ( B @ sk7 ) @ ( A @ a_select3 ) ) ) ) ),
inference(cnfConj,[status(thm)],[189]) ).
thf(197,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ~ ( B @ ( D @ leq ) )
| ~ ( D @ ( n0 @ leq ) )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ( ( D @ ( C @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) ) )
| ( ( A @ ( B @ sk6 ) @ ( A @ ( B @ sk7 ) @ ( A @ a_select3 ) ) )
!= ( A @ ( B @ sk7 ) @ ( A @ ( B @ sk6 ) @ ( A @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[191]) ).
thf(619,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
!= ( sk2 @ ( sk1 @ ( q_init @ a_select3 ) ) ) )
| ( ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
!= init )
| ~ ( B @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ~ ( B @ ( D @ leq ) )
| ~ ( D @ ( n0 @ leq ) )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ( ( A @ ( B @ sk6 ) @ ( A @ ( B @ sk7 ) @ ( A @ a_select3 ) ) )
!= ( A @ ( B @ sk7 ) @ ( A @ ( B @ sk6 ) @ ( A @ a_select3 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[197,105]) ).
thf(703,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D != sk2 )
| ( C != sk1 )
| ( ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) )
!= q_init )
| ( ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
!= init )
| ~ ( B @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ~ ( B @ ( D @ leq ) )
| ~ ( D @ ( n0 @ leq ) )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ( ( A @ ( B @ sk7 ) )
!= ( A @ ( B @ sk6 ) ) )
| ( ( A @ ( B @ sk7 ) )
!= ( A @ ( B @ sk6 ) ) )
| ( A != A ) ),
inference(simp,[status(thm)],[619]) ).
thf(759,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( C @ ( A @ tptp_update3 ) ) ) )
!= q_init )
| ( ( sk1 @ ( sk2 @ ( D @ ( C @ ( C @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
!= init )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ~ ( B @ ( sk2 @ leq ) )
| ~ ( sk2 @ ( n0 @ leq ) )
| ~ ( B @ ( sk1 @ leq ) )
| ~ ( sk1 @ ( n0 @ leq ) )
| ( ( A @ ( B @ sk7 ) )
!= ( A @ ( B @ sk6 ) ) ) ),
inference(simp,[status(thm)],[703]) ).
thf(820,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( C @ ( A @ tptp_update3 ) ) ) )
!= q_init )
| ( ( sk1 @ ( sk2 @ ( D @ ( C @ ( C @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
!= init )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ~ ( B @ ( sk2 @ leq ) )
| ~ $true
| ~ ( B @ ( sk1 @ leq ) )
| ~ $true
| ( ( A @ ( B @ sk7 ) )
!= ( A @ ( B @ sk6 ) ) ) ),
inference(rewrite,[status(thm)],[759,96,102]) ).
thf(821,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( C @ ( A @ tptp_update3 ) ) ) )
!= q_init )
| ( ( sk1 @ ( sk2 @ ( D @ ( C @ ( C @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
!= init )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ~ ( B @ ( sk2 @ leq ) )
| ~ ( B @ ( sk1 @ leq ) )
| ( ( A @ ( B @ sk7 ) )
!= ( A @ ( B @ sk6 ) ) ) ),
inference(simp,[status(thm)],[820]) ).
thf(63,axiom,
tptp_minus_1 @ ( n4 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_4_tptp_minus_1) ).
thf(492,plain,
tptp_minus_1 @ ( n4 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(50,axiom,
! [A: $i] :
( tptp_float_0_0
= ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_plus_base_float) ).
thf(397,plain,
! [A: $i] :
( tptp_float_0_0
= ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(99,plain,
n135299 @ ( sk1 @ leq ),
inference(cnfConj,[status(thm)],[93]) ).
thf(1925,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n135299 @ ( sk1 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[99,1918]) ).
thf(1926,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n135299 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[1925]) ).
thf(1935,plain,
( ( ( pv10 @ pred )
!= n135299 )
| ( sk1 != sk1 ) ),
inference(simp,[status(thm)],[1926]) ).
thf(1937,plain,
( ( pv10 @ pred )
!= n135299 ),
inference(simp,[status(thm)],[1935]) ).
thf(19462,plain,
! [A: $i] :
( ( ( A @ succ @ pred )
!= ( pv10 @ pred ) )
| ( A != n135299 ) ),
inference(paramod_ordered,[status(thm)],[566,1937]) ).
thf(19512,plain,
( ( n135299 @ succ )
!= pv10 ),
inference(simp,[status(thm)],[19462]) ).
thf(69,axiom,
tptp_minus_1 @ ( n1 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_1_tptp_minus_1) ).
thf(517,plain,
tptp_minus_1 @ ( n1 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(2770,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n1 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[517,144]) ).
thf(2771,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n1 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2770]) ).
thf(2772,plain,
n1 @ ( tptp_minus_1 @ leq ),
inference(pattern_uni,[status(thm)],[2771:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n1 ))]]) ).
thf(10,axiom,
! [A: $i] :
( ( n5 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',succ_plus_5_r) ).
thf(131,plain,
! [A: $i] :
( ( n5 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(132,plain,
! [A: $i] :
( ( n5 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
inference(cnf,[status(esa)],[131]) ).
thf(133,plain,
! [A: $i] :
( ( n5 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
inference(lifteq,[status(thm)],[132]) ).
thf(5,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ ( B @ ( A @ tptp_update2 ) ) @ a_select2 ) )
= C ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sel2_update_1) ).
thf(114,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ ( B @ ( A @ tptp_update2 ) ) @ a_select2 ) )
= C ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(115,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( B @ ( A @ tptp_update2 ) ) @ a_select2 ) )
= C ),
inference(cnf,[status(esa)],[114]) ).
thf(116,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( B @ ( A @ tptp_update2 ) ) @ a_select2 ) )
= C ),
inference(lifteq,[status(thm)],[115]) ).
thf(8058,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n1 @ ( tptp_minus_1 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2772,1918]) ).
thf(8059,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n1 @ ( tptp_minus_1 @ leq ) ) ),
inference(simp,[status(thm)],[8058]) ).
thf(8094,plain,
( ( ( pv10 @ pred )
!= n1 )
| ( sk1 != tptp_minus_1 ) ),
inference(simp,[status(thm)],[8059]) ).
thf(2716,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[492,144]) ).
thf(2717,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2716]) ).
thf(2718,plain,
n4 @ ( tptp_minus_1 @ leq ),
inference(pattern_uni,[status(thm)],[2717:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n4 ))]]) ).
thf(14,axiom,
n1 @ ( n2 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_2_1) ).
thf(141,plain,
n1 @ ( n2 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(2737,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n2 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[141,144]) ).
thf(2738,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n2 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2737]) ).
thf(2739,plain,
n2 @ ( n1 @ leq ),
inference(pattern_uni,[status(thm)],[2738:[bind(A,$thf( n1 )),bind(B,$thf( n2 ))]]) ).
thf(4444,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n2 @ ( n1 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2739,1918]) ).
thf(4445,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n2 @ ( n1 @ leq ) ) ),
inference(simp,[status(thm)],[4444]) ).
thf(4483,plain,
( ( ( pv10 @ pred )
!= n2 )
| ( sk1 != n1 ) ),
inference(simp,[status(thm)],[4445]) ).
thf(3324,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( pv10 @ ( sk1 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2730,1918]) ).
thf(3325,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( pv10 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[3324]) ).
thf(3355,plain,
( ( ( pv10 @ pred )
!= pv10 )
| ( sk1 != sk1 ) ),
inference(simp,[status(thm)],[3325]) ).
thf(3378,plain,
( ( pv10 @ pred )
!= pv10 ),
inference(simp,[status(thm)],[3355]) ).
thf(949,plain,
! [A: $i] :
( ( ( n0 @ ( A @ ( center_init @ a_select3 ) ) )
!= ( sk2 @ ( sk1 @ ( q_init @ a_select3 ) ) ) )
| ( init != init )
| ~ ( n4 @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[107,105]) ).
thf(950,plain,
! [A: $i] :
( ( ( n0 @ ( A @ ( center_init @ a_select3 ) ) )
!= ( sk2 @ ( sk1 @ ( q_init @ a_select3 ) ) ) )
| ~ ( n4 @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[949]) ).
thf(988,plain,
! [A: $i] :
( ( sk2 != n0 )
| ( A != sk1 )
| ( center_init != q_init )
| ~ ( n4 @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[950]) ).
thf(1011,plain,
( ( sk2 != n0 )
| ( center_init != q_init )
| ~ ( n4 @ ( sk1 @ leq ) )
| ~ ( sk1 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[988]) ).
thf(1208,plain,
( ( sk2 != n0 )
| ( center_init != q_init )
| ~ ( n4 @ ( sk1 @ leq ) )
| ~ $true ),
inference(rewrite,[status(thm)],[1011,96]) ).
thf(1209,plain,
( ( sk2 != n0 )
| ( center_init != q_init )
| ~ ( n4 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[1208]) ).
thf(3322,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( pv10 @ ( sk1 @ leq ) ) )
| ( sk2 != n0 )
| ( center_init != q_init )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2730,1209]) ).
thf(3323,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( pv10 @ ( sk1 @ leq ) ) )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[3322]) ).
thf(3366,plain,
( ( n4 != pv10 )
| ( sk1 != sk1 )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[3323]) ).
thf(3389,plain,
( ( n4 != pv10 )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[3366]) ).
thf(9874,plain,
( ( ( n1 @ succ @ succ @ succ )
!= ( n1 @ succ @ succ @ succ ) )
| ( ( n4 @ succ )
= n5 ) ),
inference(paramod_ordered,[status(thm)],[2511,9818]) ).
thf(9875,plain,
( ( n4 @ succ )
= n5 ),
inference(pattern_uni,[status(thm)],[9874:[]]) ).
thf(939,plain,
! [A: $i] :
( ( ( sk2 @ ( n0 @ leq ) )
!= ( A @ ( n0 @ leq ) ) )
| ~ ( n4 @ ( A @ leq ) )
| ~ $true
| ( ( n0 @ ( A @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(paramod_ordered,[status(thm)],[102,107]) ).
thf(940,plain,
! [A: $i] :
( ( ( sk2 @ ( n0 @ leq ) )
!= ( A @ ( n0 @ leq ) ) )
| ~ ( n4 @ ( A @ leq ) )
| ( ( n0 @ ( A @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[939]) ).
thf(941,plain,
( ~ ( n4 @ ( sk2 @ leq ) )
| ( ( n0 @ ( sk2 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(pattern_uni,[status(thm)],[940:[bind(A,$thf( sk2 ))]]) ).
thf(1020,plain,
( ~ $true
| ( ( n0 @ ( sk2 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(rewrite,[status(thm)],[941,94]) ).
thf(1021,plain,
( ( n0 @ ( sk2 @ ( center_init @ a_select3 ) ) )
= init ),
inference(simp,[status(thm)],[1020]) ).
thf(1024,plain,
( ( ( n0 @ ( sk2 @ ( center_init @ a_select3 ) ) )
!= ( sk2 @ ( sk1 @ ( q_init @ a_select3 ) ) ) )
| ( init != init ) ),
inference(paramod_ordered,[status(thm)],[1021,105]) ).
thf(1025,plain,
( ( n0 @ ( sk2 @ ( center_init @ a_select3 ) ) )
!= ( sk2 @ ( sk1 @ ( q_init @ a_select3 ) ) ) ),
inference(simp,[status(thm)],[1024]) ).
thf(1047,plain,
( ( sk2 != n0 )
| ( sk2 != sk1 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[1025]) ).
thf(1727,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[492,337]) ).
thf(1728,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1727]) ).
thf(1729,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n4 != A ) ),
inference(simp,[status(thm)],[1728]) ).
thf(1730,plain,
tptp_minus_1 != n4,
inference(simp,[status(thm)],[1729]) ).
thf(3221,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n4 @ ( tptp_minus_1 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2718,1918]) ).
thf(3222,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n4 @ ( tptp_minus_1 @ leq ) ) ),
inference(simp,[status(thm)],[3221]) ).
thf(3261,plain,
( ( ( pv10 @ pred )
!= n4 )
| ( sk1 != tptp_minus_1 ) ),
inference(simp,[status(thm)],[3222]) ).
thf(1480,plain,
( ( ( n4 @ ( pv10 @ leq ) )
!= ( sk1 @ ( n0 @ leq ) ) )
| ~ $true
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(paramod_ordered,[status(thm)],[96,953]) ).
thf(1481,plain,
( ( ( n4 @ ( pv10 @ leq ) )
!= ( sk1 @ ( n0 @ leq ) ) )
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[1480]) ).
thf(1519,plain,
( ( sk1 != n4 )
| ( pv10 != n0 )
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[1481]) ).
thf(23,axiom,
! [A: $i,B: $i] :
( ( A = B )
| ( A @ ( B @ gt ) )
| ( B @ ( A @ gt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',totality) ).
thf(160,plain,
! [A: $i,B: $i] :
( ( A = B )
| ( A @ ( B @ gt ) )
| ( B @ ( A @ gt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(59,axiom,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( B @ a_select3 ) ) )
= ( D @ ( E @ ( B @ a_select3 ) ) ) ) )
& ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( A @ a_select3 ) ) )
= ( D @ ( E @ ( A @ a_select3 ) ) ) ) ) )
=> ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( B @ ( A @ tptp_madd ) @ a_select3 ) ) )
= ( D @ ( E @ ( B @ ( A @ tptp_madd ) @ a_select3 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',matrix_symm_add) ).
thf(424,plain,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( B @ a_select3 ) ) )
= ( D @ ( E @ ( B @ a_select3 ) ) ) ) )
& ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( A @ a_select3 ) ) )
= ( D @ ( E @ ( A @ a_select3 ) ) ) ) ) )
=> ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( B @ ( A @ tptp_madd ) @ a_select3 ) ) )
= ( D @ ( E @ ( B @ ( A @ tptp_madd ) @ a_select3 ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(944,plain,
! [A: $i] :
( ( ( sk1 @ ( n0 @ leq ) )
!= ( A @ ( n0 @ leq ) ) )
| ~ ( n4 @ ( A @ leq ) )
| ~ $true
| ( ( n0 @ ( A @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(paramod_ordered,[status(thm)],[96,107]) ).
thf(945,plain,
! [A: $i] :
( ( ( sk1 @ ( n0 @ leq ) )
!= ( A @ ( n0 @ leq ) ) )
| ~ ( n4 @ ( A @ leq ) )
| ( ( n0 @ ( A @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[944]) ).
thf(946,plain,
( ~ ( n4 @ ( sk1 @ leq ) )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(pattern_uni,[status(thm)],[945:[bind(A,$thf( sk1 ))]]) ).
thf(3334,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( pv10 @ ( sk1 @ leq ) ) )
| ~ $true
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(paramod_ordered,[status(thm)],[2730,946]) ).
thf(3335,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( pv10 @ ( sk1 @ leq ) ) )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[3334]) ).
thf(3347,plain,
( ( n4 != pv10 )
| ( sk1 != sk1 )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[3335]) ).
thf(3371,plain,
( ( n4 != pv10 )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[3347]) ).
thf(12,axiom,
! [A: $i] :
( ( A @ ( n1 @ plus ) )
= ( A @ succ ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',succ_plus_1_l) ).
thf(137,plain,
! [A: $i] :
( ( A @ ( n1 @ plus ) )
= ( A @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(64,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
<=> ( A @ ( B @ succ @ gt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leq_succ_gt_equiv) ).
thf(493,plain,
! [A: $i,B: $i] :
( ( ( A @ ( B @ succ @ gt ) )
=> ( B @ ( A @ leq ) ) )
& ( ( B @ ( A @ leq ) )
=> ( A @ ( B @ succ @ gt ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(1265,plain,
( ( ( n4 @ ( sk2 @ leq ) )
!= ( n4 @ ( sk1 @ leq ) ) )
| ~ $true
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(paramod_ordered,[status(thm)],[94,946]) ).
thf(1266,plain,
( ( ( n4 @ ( sk2 @ leq ) )
!= ( n4 @ ( sk1 @ leq ) ) )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[1265]) ).
thf(1282,plain,
( ( n4 != n4 )
| ( sk2 != sk1 )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[1266]) ).
thf(1291,plain,
( ( sk2 != sk1 )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[1282]) ).
thf(84,axiom,
n0 @ ( n1 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_1_0) ).
thf(556,plain,
n0 @ ( n1 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(2767,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n1 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[556,144]) ).
thf(2768,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n1 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2767]) ).
thf(2769,plain,
n1 @ ( n0 @ leq ),
inference(pattern_uni,[status(thm)],[2768:[bind(A,$thf( n0 )),bind(B,$thf( n1 ))]]) ).
thf(39,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( ! [I: $i,J: $i] :
( ( ( G @ ( J @ leq ) )
& ( J @ ( n0 @ leq ) )
& ( G @ ( I @ leq ) )
& ( I @ ( n0 @ leq ) ) )
=> ( ( J @ ( I @ ( F @ a_select3 ) ) )
= ( I @ ( J @ ( F @ a_select3 ) ) ) ) )
& ! [I: $i,J: $i] :
( ( ( G @ ( J @ leq ) )
& ( J @ ( n0 @ leq ) )
& ( G @ ( I @ leq ) )
& ( I @ ( n0 @ leq ) ) )
=> ( ( J @ ( I @ ( A @ a_select3 ) ) )
= ( I @ ( J @ ( A @ a_select3 ) ) ) ) )
& ! [I: $i,J: $i] :
( ( ( H @ ( J @ leq ) )
& ( J @ ( n0 @ leq ) )
& ( H @ ( I @ leq ) )
& ( I @ ( n0 @ leq ) ) )
=> ( ( J @ ( I @ ( D @ a_select3 ) ) )
= ( I @ ( J @ ( D @ a_select3 ) ) ) ) ) )
=> ! [I: $i,J: $i] :
( ( ( G @ ( J @ leq ) )
& ( J @ ( n0 @ leq ) )
& ( G @ ( I @ leq ) )
& ( I @ ( n0 @ leq ) ) )
=> ( ( J @ ( I @ ( B @ trans @ ( E @ trans @ ( F @ tptp_mmul ) @ ( E @ tptp_mmul ) @ ( C @ trans @ ( D @ tptp_mmul ) @ ( C @ tptp_mmul ) @ tptp_madd ) @ tptp_mmul ) @ ( B @ tptp_mmul ) @ ( A @ tptp_madd ) @ a_select3 ) ) )
= ( I @ ( J @ ( B @ trans @ ( E @ trans @ ( F @ tptp_mmul ) @ ( E @ tptp_mmul ) @ ( C @ trans @ ( D @ tptp_mmul ) @ ( C @ tptp_mmul ) @ tptp_madd ) @ tptp_mmul ) @ ( B @ tptp_mmul ) @ ( A @ tptp_madd ) @ a_select3 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',matrix_symm_joseph_update) ).
thf(229,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( ! [I: $i,J: $i] :
( ( ( G @ ( J @ leq ) )
& ( J @ ( n0 @ leq ) )
& ( G @ ( I @ leq ) )
& ( I @ ( n0 @ leq ) ) )
=> ( ( J @ ( I @ ( F @ a_select3 ) ) )
= ( I @ ( J @ ( F @ a_select3 ) ) ) ) )
& ! [I: $i,J: $i] :
( ( ( G @ ( J @ leq ) )
& ( J @ ( n0 @ leq ) )
& ( G @ ( I @ leq ) )
& ( I @ ( n0 @ leq ) ) )
=> ( ( J @ ( I @ ( A @ a_select3 ) ) )
= ( I @ ( J @ ( A @ a_select3 ) ) ) ) )
& ! [I: $i,J: $i] :
( ( ( H @ ( J @ leq ) )
& ( J @ ( n0 @ leq ) )
& ( H @ ( I @ leq ) )
& ( I @ ( n0 @ leq ) ) )
=> ( ( J @ ( I @ ( D @ a_select3 ) ) )
= ( I @ ( J @ ( D @ a_select3 ) ) ) ) ) )
=> ! [I: $i,J: $i] :
( ( ( G @ ( J @ leq ) )
& ( J @ ( n0 @ leq ) )
& ( G @ ( I @ leq ) )
& ( I @ ( n0 @ leq ) ) )
=> ( ( J @ ( I @ ( B @ trans @ ( E @ trans @ ( F @ tptp_mmul ) @ ( E @ tptp_mmul ) @ ( C @ trans @ ( D @ tptp_mmul ) @ ( C @ tptp_mmul ) @ tptp_madd ) @ tptp_mmul ) @ ( B @ tptp_mmul ) @ ( A @ tptp_madd ) @ a_select3 ) ) )
= ( I @ ( J @ ( B @ trans @ ( E @ trans @ ( F @ tptp_mmul ) @ ( E @ tptp_mmul ) @ ( C @ trans @ ( D @ tptp_mmul ) @ ( C @ tptp_mmul ) @ tptp_madd ) @ tptp_mmul ) @ ( B @ tptp_mmul ) @ ( A @ tptp_madd ) @ a_select3 ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(398,plain,
! [A: $i] :
( tptp_float_0_0
= ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) ) ),
inference(cnf,[status(esa)],[397]) ).
thf(399,plain,
! [A: $i] :
( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
= tptp_float_0_0 ),
inference(lifteq,[status(thm)],[398]) ).
thf(27,axiom,
! [A: $i] :
( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
= n0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_plus_base) ).
thf(166,plain,
! [A: $i] :
( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
= n0 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(167,plain,
! [A: $i] :
( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
= n0 ),
inference(cnf,[status(esa)],[166]) ).
thf(168,plain,
! [A: $i] :
( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
= n0 ),
inference(lifteq,[status(thm)],[167]) ).
thf(12822,plain,
tptp_float_0_0 = n0,
inference(rewrite,[status(thm)],[399,168]) ).
thf(44,axiom,
! [A: $i,B: $i] :
( ( B @ pred @ ( A @ leq ) )
<=> ( A @ ( B @ gt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leq_gt_pred) ).
thf(329,plain,
! [A: $i,B: $i] :
( ( ( A @ ( B @ gt ) )
=> ( B @ pred @ ( A @ leq ) ) )
& ( ( B @ pred @ ( A @ leq ) )
=> ( A @ ( B @ gt ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(40,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ geq ) )
<=> ( A @ ( B @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leq_geq) ).
thf(317,plain,
! [A: $i,B: $i] :
( ( ( A @ ( B @ leq ) )
=> ( B @ ( A @ geq ) ) )
& ( ( B @ ( A @ geq ) )
=> ( A @ ( B @ leq ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(2707,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[555,144]) ).
thf(2708,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2707]) ).
thf(2709,plain,
n3 @ ( tptp_minus_1 @ leq ),
inference(pattern_uni,[status(thm)],[2708:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n3 ))]]) ).
thf(2722,plain,
! [B: $i,A: $i] :
( ( ( n3 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[206,144]) ).
thf(2723,plain,
! [B: $i,A: $i] :
( ( ( n3 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2722]) ).
thf(2724,plain,
n5 @ ( n3 @ leq ),
inference(pattern_uni,[status(thm)],[2723:[bind(A,$thf( n3 )),bind(B,$thf( n5 ))]]) ).
thf(4782,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( n4 @ ( n0 @ leq ) ) )
| ( sk2 != n0 )
| ( center_init != q_init )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2748,1209]) ).
thf(4783,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( n4 @ ( n0 @ leq ) ) )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[4782]) ).
thf(4826,plain,
( ( n4 != n4 )
| ( sk1 != n0 )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[4783]) ).
thf(4840,plain,
( ( sk1 != n0 )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[4826]) ).
thf(58,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ ( A @ leq ) )
& ( A @ ( B @ leq ) ) )
=> ( ( A @ ( D @ ( C @ ( B @ dim ) @ tptp_const_array1 ) @ a_select2 ) )
= D ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',const_array1_select) ).
thf(420,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ ( A @ leq ) )
& ( A @ ( B @ leq ) ) )
=> ( ( A @ ( D @ ( C @ ( B @ dim ) @ tptp_const_array1 ) @ a_select2 ) )
= D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(43,axiom,
( ( tptp_minus_1 @ succ )
= n0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',succ_tptp_minus_1) ).
thf(327,plain,
( ( tptp_minus_1 @ succ )
= n0 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(328,plain,
( ( tptp_minus_1 @ succ )
= n0 ),
inference(lifteq,[status(thm)],[327]) ).
thf(7,axiom,
! [A: $i] :
( ( A @ ( n3 @ plus ) )
= ( A @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',succ_plus_3_l) ).
thf(122,plain,
! [A: $i] :
( ( A @ ( n3 @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(123,plain,
! [A: $i] :
( ( A @ ( n3 @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(cnf,[status(esa)],[122]) ).
thf(124,plain,
! [A: $i] :
( ( A @ ( n3 @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(lifteq,[status(thm)],[123]) ).
thf(47,axiom,
! [A: $i,B: $i] :
( ( A @ ( n0 @ leq ) )
=> ( A @ ( B @ uniform_int_rnd ) @ ( n0 @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',uniform_int_rand_ranges_lo) ).
thf(339,plain,
! [A: $i,B: $i] :
( ( A @ ( n0 @ leq ) )
=> ( A @ ( B @ uniform_int_rnd ) @ ( n0 @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(60,axiom,
! [A: $i,B: $i] :
( ( A @ ( n0 @ leq ) )
=> ( A @ ( A @ ( B @ uniform_int_rnd ) @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',uniform_int_rand_ranges_hi) ).
thf(476,plain,
! [A: $i,B: $i] :
( ( A @ ( n0 @ leq ) )
=> ( A @ ( A @ ( B @ uniform_int_rnd ) @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(1204,plain,
! [A: $i] :
( ( ( n1 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[145,337]) ).
thf(1205,plain,
! [A: $i] :
( ( n1 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1204]) ).
thf(1206,plain,
! [A: $i] :
( ( n1 != A )
| ( n3 != A ) ),
inference(simp,[status(thm)],[1205]) ).
thf(1207,plain,
n1 != n3,
inference(simp,[status(thm)],[1206]) ).
thf(79,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ leq ) )
& ( B @ ( A @ leq ) ) )
=> ( C @ ( A @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity_leq) ).
thf(547,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ leq ) )
& ( B @ ( A @ leq ) ) )
=> ( C @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(42,axiom,
n0 @ ( n5 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_5_0) ).
thf(326,plain,
n0 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(2779,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[326,144]) ).
thf(2780,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2779]) ).
thf(2781,plain,
n5 @ ( n0 @ leq ),
inference(pattern_uni,[status(thm)],[2780:[bind(A,$thf( n0 )),bind(B,$thf( n5 ))]]) ).
thf(68,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ ( A @ minus ) @ leq ) )
=> ( B @ ( n0 @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leq_minus) ).
thf(515,plain,
! [A: $i,B: $i] :
( ( A @ ( B @ ( A @ minus ) @ leq ) )
=> ( B @ ( n0 @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(171,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( F @ ( D @ leq ) )
& ( D @ ( E @ leq ) )
& ( C @ ( A @ leq ) )
& ( A @ ( B @ leq ) ) )
=> ! [G: $i] :
( ( D @ ( A @ ( G @ ( F @ ( E @ dim ) @ ( C @ ( B @ dim ) @ tptp_const_array2 ) ) @ a_select3 ) ) )
= G ) ),
inference(miniscope,[status(thm)],[170]) ).
thf(172,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( A @ ( G @ ( F @ ( E @ dim ) @ ( C @ ( B @ dim ) @ tptp_const_array2 ) ) @ a_select3 ) ) )
= G )
| ~ ( F @ ( D @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( C @ ( A @ leq ) )
| ~ ( A @ ( B @ leq ) ) ),
inference(cnf,[status(esa)],[171]) ).
thf(173,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( F @ ( D @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( C @ ( A @ leq ) )
| ~ ( A @ ( B @ leq ) )
| ( ( D @ ( A @ ( G @ ( F @ ( E @ dim ) @ ( C @ ( B @ dim ) @ tptp_const_array2 ) ) @ a_select3 ) ) )
= G ) ),
inference(lifteq,[status(thm)],[172]) ).
thf(46,axiom,
n1 @ ( n135299 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_135299_1) ).
thf(338,plain,
n1 @ ( n135299 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(2764,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n135299 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[338,144]) ).
thf(2765,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n135299 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2764]) ).
thf(2766,plain,
n135299 @ ( n1 @ leq ),
inference(pattern_uni,[status(thm)],[2765:[bind(A,$thf( n1 )),bind(B,$thf( n135299 ))]]) ).
thf(91,axiom,
( ( n0 @ succ @ succ )
= n2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_2) ).
thf(568,plain,
( ( n0 @ succ @ succ )
= n2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(569,plain,
( ( n0 @ succ @ succ )
= n2 ),
inference(lifteq,[status(thm)],[568]) ).
thf(2123,plain,
( ( n1 @ succ )
= n2 ),
inference(rewrite,[status(thm)],[569,147]) ).
thf(19497,plain,
! [A: $i] :
( ( ( n1 @ succ )
!= ( A @ succ ) )
| ( ( n2 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[2123,566]) ).
thf(19498,plain,
( ( n2 @ pred )
= n1 ),
inference(pattern_uni,[status(thm)],[19497:[bind(A,$thf( n1 ))]]) ).
thf(11,axiom,
! [A: $i] :
( ( n1 @ ( A @ plus ) )
= ( A @ succ ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',succ_plus_1_r) ).
thf(134,plain,
! [A: $i] :
( ( n1 @ ( A @ plus ) )
= ( A @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(9,axiom,
! [A: $i] :
( ( A @ ( n5 @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',succ_plus_5_l) ).
thf(128,plain,
! [A: $i] :
( ( A @ ( n5 @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(76,axiom,
n0 @ ( n2 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_2_0) ).
thf(541,plain,
n0 @ ( n2 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(1998,plain,
! [A: $i] :
( ( ( n1 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[562,337]) ).
thf(1999,plain,
! [A: $i] :
( ( n1 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1998]) ).
thf(2000,plain,
! [A: $i] :
( ( n1 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[1999]) ).
thf(2001,plain,
n1 != n5,
inference(simp,[status(thm)],[2000]) ).
thf(34,axiom,
! [A: $i] :
( ( A @ pred @ succ )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',succ_pred) ).
thf(207,plain,
! [A: $i] :
( ( A @ pred @ succ )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(208,plain,
! [A: $i] :
( ( A @ pred @ succ )
= A ),
inference(cnf,[status(esa)],[207]) ).
thf(209,plain,
! [A: $i] :
( ( A @ pred @ succ )
= A ),
inference(lifteq,[status(thm)],[208]) ).
thf(15544,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ succ @ gt ) )
!= ( B @ ( B @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[550,337]) ).
thf(15545,plain,
! [B: $i,A: $i] :
( ( A @ ( A @ succ @ gt ) )
!= ( B @ ( B @ gt ) ) ),
inference(simp,[status(thm)],[15544]) ).
thf(15546,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ succ )
!= B ) ),
inference(simp,[status(thm)],[15545]) ).
thf(15551,plain,
! [A: $i] :
( ( A @ succ )
!= A ),
inference(simp,[status(thm)],[15546]) ).
thf(17261,plain,
! [B: $i,A: $i] :
( ( ( A @ pred @ succ )
!= ( B @ succ ) )
| ( A != B ) ),
inference(paramod_ordered,[status(thm)],[209,15551]) ).
thf(17262,plain,
! [A: $i] :
( ( A @ pred )
!= A ),
inference(pattern_uni,[status(thm)],[17261:[bind(A,$thf( C )),bind(B,$thf( C @ pred ))]]) ).
thf(17271,plain,
! [A: $i] :
( ( A @ pred )
!= A ),
inference(simp,[status(thm)],[17262]) ).
thf(73,axiom,
tptp_minus_1 @ ( n5 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_5_tptp_minus_1) ).
thf(535,plain,
tptp_minus_1 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(2749,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[535,144]) ).
thf(2750,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2749]) ).
thf(2751,plain,
n5 @ ( tptp_minus_1 @ leq ),
inference(pattern_uni,[status(thm)],[2750:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n5 ))]]) ).
thf(4884,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n5 @ ( tptp_minus_1 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2751,1918]) ).
thf(4885,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n5 @ ( tptp_minus_1 @ leq ) ) ),
inference(simp,[status(thm)],[4884]) ).
thf(4919,plain,
( ( ( pv10 @ pred )
!= n5 )
| ( sk1 != tptp_minus_1 ) ),
inference(simp,[status(thm)],[4885]) ).
thf(67,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
=> ( B @ succ @ ( A @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leq_succ) ).
thf(513,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
=> ( B @ succ @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(570,plain,
! [A: $i] :
( ( ( sk1 @ ( pv10 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[97,337]) ).
thf(571,plain,
! [A: $i] :
( ( sk1 @ ( pv10 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[570]) ).
thf(572,plain,
! [A: $i] :
( ( sk1 != A )
| ( pv10 != A ) ),
inference(simp,[status(thm)],[571]) ).
thf(573,plain,
sk1 != pv10,
inference(simp,[status(thm)],[572]) ).
thf(2725,plain,
! [B: $i,A: $i] :
( ( ( n4 @ ( n135299 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[165,144]) ).
thf(2726,plain,
! [B: $i,A: $i] :
( ( ( n4 @ ( n135299 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2725]) ).
thf(2727,plain,
n135299 @ ( n4 @ leq ),
inference(pattern_uni,[status(thm)],[2726:[bind(A,$thf( n4 )),bind(B,$thf( n135299 ))]]) ).
thf(1913,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[535,337]) ).
thf(1914,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1913]) ).
thf(1915,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[1914]) ).
thf(1916,plain,
tptp_minus_1 != n5,
inference(simp,[status(thm)],[1915]) ).
thf(9878,plain,
( ( ( n1 @ succ )
!= ( n1 @ succ ) )
| ( ( n2 @ succ @ succ @ succ )
= n5 ) ),
inference(paramod_ordered,[status(thm)],[2123,9818]) ).
thf(9879,plain,
( ( n2 @ succ @ succ @ succ )
= n5 ),
inference(pattern_uni,[status(thm)],[9878:[]]) ).
thf(2142,plain,
( ( ( n1 @ succ )
!= ( n1 @ succ ) )
| ( ( n2 @ succ )
= n3 ) ),
inference(paramod_ordered,[status(thm)],[2123,2132]) ).
thf(2143,plain,
( ( n2 @ succ )
= n3 ),
inference(pattern_uni,[status(thm)],[2142:[]]) ).
thf(11105,plain,
( ( n3 @ succ @ succ )
= n5 ),
inference(rewrite,[status(thm)],[9879,2143]) ).
thf(543,plain,
! [A: $i] : ( A @ ( A @ leq ) ),
inference(cnf,[status(esa)],[542]) ).
thf(12902,plain,
! [A: $i] :
( ( ( A @ ( A @ leq ) )
!= ( pv10 @ pred @ ( sk1 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[543,1918]) ).
thf(12903,plain,
! [A: $i] :
( ( A @ ( A @ leq ) )
!= ( pv10 @ pred @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[12902]) ).
thf(12945,plain,
! [A: $i] :
( ( A
!= ( pv10 @ pred ) )
| ( A != sk1 ) ),
inference(simp,[status(thm)],[12903]) ).
thf(12958,plain,
( ( pv10 @ pred )
!= sk1 ),
inference(simp,[status(thm)],[12945]) ).
thf(3219,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( n4 @ ( tptp_minus_1 @ leq ) ) )
| ( sk2 != n0 )
| ( center_init != q_init )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2718,1209]) ).
thf(3220,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( n4 @ ( tptp_minus_1 @ leq ) ) )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[3219]) ).
thf(3267,plain,
( ( n4 != n4 )
| ( sk1 != tptp_minus_1 )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[3220]) ).
thf(3272,plain,
( ( sk1 != tptp_minus_1 )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[3267]) ).
thf(574,plain,
! [A: $i] :
( ( ( n2 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[140,337]) ).
thf(575,plain,
! [A: $i] :
( ( n2 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[574]) ).
thf(576,plain,
! [A: $i] :
( ( n2 != A )
| ( n3 != A ) ),
inference(simp,[status(thm)],[575]) ).
thf(577,plain,
n3 != n2,
inference(simp,[status(thm)],[576]) ).
thf(2740,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n2 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[541,144]) ).
thf(2741,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n2 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2740]) ).
thf(2742,plain,
n2 @ ( n0 @ leq ),
inference(pattern_uni,[status(thm)],[2741:[bind(A,$thf( n0 )),bind(B,$thf( n2 ))]]) ).
thf(4565,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n2 @ ( n0 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2742,1918]) ).
thf(4566,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n2 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[4565]) ).
thf(4605,plain,
( ( ( pv10 @ pred )
!= n2 )
| ( sk1 != n0 ) ),
inference(simp,[status(thm)],[4566]) ).
thf(1962,plain,
! [A: $i] :
( ( ( n4 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[551,337]) ).
thf(1963,plain,
! [A: $i] :
( ( n4 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1962]) ).
thf(1964,plain,
! [A: $i] :
( ( n4 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[1963]) ).
thf(1965,plain,
n5 != n4,
inference(simp,[status(thm)],[1964]) ).
thf(933,plain,
! [A: $i] :
( ( ( n5 @ ( n135299 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[142,337]) ).
thf(934,plain,
! [A: $i] :
( ( n5 @ ( n135299 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[933]) ).
thf(935,plain,
! [A: $i] :
( ( n5 != A )
| ( n135299 != A ) ),
inference(simp,[status(thm)],[934]) ).
thf(936,plain,
n5 != n135299,
inference(simp,[status(thm)],[935]) ).
thf(156,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( D @ ( B @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D )
| ~ ( B @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( A @ ( B @ ( C @ ( D @ sk3 ) ) ) @ ( C @ a_select2 ) )
!= D ) ),
inference(cnfConj,[status(thm)],[153]) ).
thf(159,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( A @ ( D @ ( B @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D )
| ( ( A @ ( B @ ( C @ ( D @ sk3 ) ) ) @ ( C @ a_select2 ) )
!= D ) ),
inference(lifteq,[status(thm)],[156]) ).
thf(2704,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n135299 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[408,144]) ).
thf(2705,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n135299 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2704]) ).
thf(2706,plain,
n135299 @ ( n2 @ leq ),
inference(pattern_uni,[status(thm)],[2705:[bind(A,$thf( n2 )),bind(B,$thf( n135299 ))]]) ).
thf(4,axiom,
! [A: $i] :
( ( n3 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',succ_plus_3_r) ).
thf(111,plain,
! [A: $i] :
( ( n3 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(112,plain,
! [A: $i] :
( ( n3 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(cnf,[status(esa)],[111]) ).
thf(113,plain,
! [A: $i] :
( ( n3 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(lifteq,[status(thm)],[112]) ).
thf(3644,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( n4 @ ( n2 @ leq ) ) )
| ~ $true
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(paramod_ordered,[status(thm)],[2721,946]) ).
thf(3645,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( n4 @ ( n2 @ leq ) ) )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[3644]) ).
thf(3660,plain,
( ( n4 != n4 )
| ( sk1 != n2 )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[3645]) ).
thf(3683,plain,
( ( sk1 != n2 )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[3660]) ).
thf(1927,plain,
( ( ( n4 @ ( sk2 @ leq ) )
!= ( pv10 @ pred @ ( sk1 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[94,1918]) ).
thf(1928,plain,
( ( n4 @ ( sk2 @ leq ) )
!= ( pv10 @ pred @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[1927]) ).
thf(1933,plain,
( ( ( pv10 @ pred )
!= n4 )
| ( sk2 != sk1 ) ),
inference(simp,[status(thm)],[1928]) ).
thf(1719,plain,
! [A: $i] :
( ( ( n2 @ ( n135299 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[408,337]) ).
thf(1720,plain,
! [A: $i] :
( ( n2 @ ( n135299 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1719]) ).
thf(1721,plain,
! [A: $i] :
( ( n2 != A )
| ( n135299 != A ) ),
inference(simp,[status(thm)],[1720]) ).
thf(1722,plain,
n2 != n135299,
inference(simp,[status(thm)],[1721]) ).
thf(2921,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n3 @ ( tptp_minus_1 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2709,1918]) ).
thf(2922,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n3 @ ( tptp_minus_1 @ leq ) ) ),
inference(simp,[status(thm)],[2921]) ).
thf(2943,plain,
( ( ( pv10 @ pred )
!= n3 )
| ( sk1 != tptp_minus_1 ) ),
inference(simp,[status(thm)],[2922]) ).
thf(1966,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[555,337]) ).
thf(1967,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1966]) ).
thf(1968,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n3 != A ) ),
inference(simp,[status(thm)],[1967]) ).
thf(1969,plain,
tptp_minus_1 != n3,
inference(simp,[status(thm)],[1968]) ).
thf(8644,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( n4 @ ( n1 @ leq ) ) )
| ( sk2 != n0 )
| ( center_init != q_init )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2784,1209]) ).
thf(8645,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( n4 @ ( n1 @ leq ) ) )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[8644]) ).
thf(8698,plain,
( ( n4 != n4 )
| ( sk1 != n1 )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[8645]) ).
thf(8735,plain,
( ( sk1 != n1 )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[8698]) ).
thf(82,axiom,
! [A: $i] :
( ( ( n4 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n4 )
| ( A = n3 )
| ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_4) ).
thf(552,plain,
! [A: $i] :
( ( ( n4 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n4 )
| ( A = n3 )
| ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(41,axiom,
! [A: $i,B: $i] :
( ( ( A != B )
& ( B @ ( A @ leq ) ) )
=> ( A @ ( B @ gt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leq_gt2) ).
thf(323,plain,
! [A: $i,B: $i] :
( ( ( A != B )
& ( B @ ( A @ leq ) ) )
=> ( A @ ( B @ gt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(8487,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n5 @ ( n0 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2781,1918]) ).
thf(8488,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n5 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[8487]) ).
thf(8529,plain,
( ( ( pv10 @ pred )
!= n5 )
| ( sk1 != n0 ) ),
inference(simp,[status(thm)],[8488]) ).
thf(71,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ gt ) )
& ( B @ ( A @ gt ) ) )
=> ( C @ ( A @ gt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity_gt) ).
thf(521,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ gt ) )
& ( B @ ( A @ gt ) ) )
=> ( C @ ( A @ gt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(129,plain,
! [A: $i] :
( ( A @ ( n5 @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
inference(cnf,[status(esa)],[128]) ).
thf(130,plain,
! [A: $i] :
( ( A @ ( n5 @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
inference(lifteq,[status(thm)],[129]) ).
thf(5604,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n2 @ ( tptp_minus_1 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2763,1918]) ).
thf(5605,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n2 @ ( tptp_minus_1 @ leq ) ) ),
inference(simp,[status(thm)],[5604]) ).
thf(5641,plain,
( ( ( pv10 @ pred )
!= n2 )
| ( sk1 != tptp_minus_1 ) ),
inference(simp,[status(thm)],[5605]) ).
thf(37,axiom,
! [A: $i] :
( ( n1 @ ( A @ minus ) )
= ( A @ pred ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pred_minus_1) ).
thf(223,plain,
! [A: $i] :
( ( n1 @ ( A @ minus ) )
= ( A @ pred ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(49,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( C @ ( B @ ( D @ ( C @ ( B @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= D ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sel3_update_1) ).
thf(394,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( C @ ( B @ ( D @ ( C @ ( B @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= D ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(19468,plain,
! [A: $i] :
( ( ( A @ succ @ pred )
!= ( pv10 @ pred ) )
| ( A != sk1 ) ),
inference(paramod_ordered,[status(thm)],[566,12958]) ).
thf(19516,plain,
( ( sk1 @ succ )
!= pv10 ),
inference(simp,[status(thm)],[19468]) ).
thf(4663,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n5 @ ( n1 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2745,1918]) ).
thf(4664,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n5 @ ( n1 @ leq ) ) ),
inference(simp,[status(thm)],[4663]) ).
thf(4703,plain,
( ( ( pv10 @ pred )
!= n5 )
| ( sk1 != n1 ) ),
inference(simp,[status(thm)],[4664]) ).
thf(1970,plain,
! [A: $i] :
( ( ( n0 @ ( n1 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[556,337]) ).
thf(1971,plain,
! [A: $i] :
( ( n0 @ ( n1 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1970]) ).
thf(1972,plain,
! [A: $i] :
( ( n0 != A )
| ( n1 != A ) ),
inference(simp,[status(thm)],[1971]) ).
thf(1973,plain,
n1 != n0,
inference(simp,[status(thm)],[1972]) ).
thf(38,axiom,
! [A: $i] :
( ( ( n0 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( A = n0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_0) ).
thf(226,plain,
! [A: $i] :
( ( ( n0 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( A = n0 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(1723,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n135299 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[491,337]) ).
thf(1724,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n135299 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1723]) ).
thf(1725,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n135299 != A ) ),
inference(simp,[status(thm)],[1724]) ).
thf(1726,plain,
tptp_minus_1 != n135299,
inference(simp,[status(thm)],[1725]) ).
thf(2002,plain,
! [A: $i] :
( ( ( n3 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[563,337]) ).
thf(2003,plain,
! [A: $i] :
( ( n3 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2002]) ).
thf(2004,plain,
! [A: $i] :
( ( n3 != A )
| ( n4 != A ) ),
inference(simp,[status(thm)],[2003]) ).
thf(2005,plain,
n3 != n4,
inference(simp,[status(thm)],[2004]) ).
thf(161,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( A @ ( B @ gt ) )
| ( B @ ( A @ gt ) ) ),
inference(cnf,[status(esa)],[160]) ).
thf(162,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ gt ) )
| ( B @ ( A @ gt ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[161]) ).
thf(48,axiom,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( B @ a_select3 ) ) )
= ( D @ ( E @ ( B @ a_select3 ) ) ) ) )
& ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( A @ a_select3 ) ) )
= ( D @ ( E @ ( A @ a_select3 ) ) ) ) ) )
=> ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( B @ ( A @ tptp_msub ) @ a_select3 ) ) )
= ( D @ ( E @ ( B @ ( A @ tptp_msub ) @ a_select3 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',matrix_symm_sub) ).
thf(342,plain,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( B @ a_select3 ) ) )
= ( D @ ( E @ ( B @ a_select3 ) ) ) ) )
& ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( A @ a_select3 ) ) )
= ( D @ ( E @ ( A @ a_select3 ) ) ) ) ) )
=> ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( B @ ( A @ tptp_msub ) @ a_select3 ) ) )
= ( D @ ( E @ ( B @ ( A @ tptp_msub ) @ a_select3 ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(3217,plain,
( ( ( n4 @ ( tptp_minus_1 @ leq ) )
!= ( n4 @ ( pv10 @ leq ) ) )
| ~ $true
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(paramod_ordered,[status(thm)],[2718,953]) ).
thf(3218,plain,
( ( ( n4 @ ( tptp_minus_1 @ leq ) )
!= ( n4 @ ( pv10 @ leq ) ) )
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[3217]) ).
thf(3246,plain,
( ( n4 != n4 )
| ( tptp_minus_1 != pv10 )
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[3218]) ).
thf(3278,plain,
( ( tptp_minus_1 != pv10 )
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[3246]) ).
thf(1608,plain,
! [A: $i] :
( ( ( n0 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[326,337]) ).
thf(1609,plain,
! [A: $i] :
( ( n0 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1608]) ).
thf(1610,plain,
! [A: $i] :
( ( n0 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[1609]) ).
thf(1611,plain,
n5 != n0,
inference(simp,[status(thm)],[1610]) ).
thf(1938,plain,
! [A: $i] :
( ( ( n0 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[541,337]) ).
thf(1939,plain,
! [A: $i] :
( ( n0 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1938]) ).
thf(1940,plain,
! [A: $i] :
( ( n0 != A )
| ( n2 != A ) ),
inference(simp,[status(thm)],[1939]) ).
thf(1941,plain,
n2 != n0,
inference(simp,[status(thm)],[1940]) ).
thf(56,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ lt ) )
<=> ( A @ ( B @ gt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lt_gt) ).
thf(409,plain,
! [A: $i,B: $i] :
( ( ( A @ ( B @ gt ) )
=> ( B @ ( A @ lt ) ) )
& ( ( B @ ( A @ lt ) )
=> ( A @ ( B @ gt ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(1634,plain,
! [A: $i] :
( ( ( n2 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[404,337]) ).
thf(1635,plain,
! [A: $i] :
( ( n2 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1634]) ).
thf(1636,plain,
! [A: $i] :
( ( n2 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[1635]) ).
thf(1637,plain,
n5 != n2,
inference(simp,[status(thm)],[1636]) ).
thf(179,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) )
| ~ ( D @ ( F @ leq ) )
| ~ ( F @ ( n0 @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ( A @ ( B @ ( C @ sk4 ) ) @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[176]) ).
thf(182,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( F @ leq ) )
| ~ ( F @ ( n0 @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ( A @ ( B @ ( C @ sk4 ) ) @ ( n0 @ leq ) )
| ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[179]) ).
thf(126,plain,
! [A: $i] :
( ( A @ ( n2 @ plus ) )
= ( A @ succ @ succ ) ),
inference(cnf,[status(esa)],[125]) ).
thf(127,plain,
! [A: $i] :
( ( A @ ( n2 @ plus ) )
= ( A @ succ @ succ ) ),
inference(lifteq,[status(thm)],[126]) ).
thf(1314,plain,
! [A: $i] :
( ( ( n2 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[164,337]) ).
thf(1315,plain,
! [A: $i] :
( ( n2 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1314]) ).
thf(1316,plain,
! [A: $i] :
( ( n2 != A )
| ( n4 != A ) ),
inference(simp,[status(thm)],[1315]) ).
thf(1317,plain,
n2 != n4,
inference(simp,[status(thm)],[1316]) ).
thf(3743,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n5 @ ( n3 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2724,1918]) ).
thf(3744,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n5 @ ( n3 @ leq ) ) ),
inference(simp,[status(thm)],[3743]) ).
thf(3769,plain,
( ( ( pv10 @ pred )
!= n5 )
| ( sk1 != n3 ) ),
inference(simp,[status(thm)],[3744]) ).
thf(78,axiom,
! [A: $i] :
( ( ( n3 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n3 )
| ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_3) ).
thf(544,plain,
! [A: $i] :
( ( ( n3 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n3 )
| ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(1919,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( sk2 @ ( n0 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,1918]) ).
thf(1920,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( sk2 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[1919]) ).
thf(1934,plain,
( ( ( pv10 @ pred )
!= sk2 )
| ( sk1 != n0 ) ),
inference(simp,[status(thm)],[1920]) ).
thf(19455,plain,
! [A: $i] :
( ( ( n4 @ succ )
!= ( A @ succ ) )
| ( ( n5 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[9875,566]) ).
thf(19456,plain,
( ( n5 @ pred )
= n4 ),
inference(pattern_uni,[status(thm)],[19455:[bind(A,$thf( n4 ))]]) ).
thf(578,plain,
! [A: $i] :
( ( ( n1 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[141,337]) ).
thf(579,plain,
! [A: $i] :
( ( n1 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[578]) ).
thf(580,plain,
! [A: $i] :
( ( n1 != A )
| ( n2 != A ) ),
inference(simp,[status(thm)],[579]) ).
thf(581,plain,
n1 != n2,
inference(simp,[status(thm)],[580]) ).
thf(1249,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( sk1 @ ( n0 @ leq ) ) )
| ~ $true
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(paramod_ordered,[status(thm)],[96,946]) ).
thf(1250,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( sk1 @ ( n0 @ leq ) ) )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[1249]) ).
thf(1289,plain,
( ( sk1 != n4 )
| ( sk1 != n0 )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[1250]) ).
thf(21,axiom,
n3 @ ( n135299 @ gt ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_135299_3) ).
thf(151,plain,
n3 @ ( n135299 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(2773,plain,
! [B: $i,A: $i] :
( ( ( n3 @ ( n135299 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[151,144]) ).
thf(2774,plain,
! [B: $i,A: $i] :
( ( ( n3 @ ( n135299 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2773]) ).
thf(2775,plain,
n135299 @ ( n3 @ leq ),
inference(pattern_uni,[status(thm)],[2774:[bind(A,$thf( n3 )),bind(B,$thf( n135299 ))]]) ).
thf(12888,plain,
! [A: $i] :
( ( ( A @ ( A @ leq ) )
!= ( n4 @ ( sk1 @ leq ) ) )
| ( sk2 != n0 )
| ( center_init != q_init )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[543,1209]) ).
thf(12889,plain,
! [A: $i] :
( ( ( A @ ( A @ leq ) )
!= ( n4 @ ( sk1 @ leq ) ) )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[12888]) ).
thf(12944,plain,
! [A: $i] :
( ( A != n4 )
| ( A != sk1 )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[12889]) ).
thf(12957,plain,
( ( sk1 != n4 )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[12944]) ).
thf(155,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( D @ ( B @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D )
| ~ ( B @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( B @ ( A @ ( B @ ( C @ ( D @ sk3 ) ) ) @ leq ) ) ),
inference(cnfConj,[status(thm)],[153]) ).
thf(158,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( B @ ( A @ ( B @ ( C @ ( D @ sk3 ) ) ) @ leq ) )
| ( ( A @ ( D @ ( B @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D ) ),
inference(lifteq,[status(thm)],[155]) ).
thf(52,axiom,
! [A: $i] :
( ( ( n1 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n1 )
| ( A = n0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_1) ).
thf(401,plain,
! [A: $i] :
( ( ( n1 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n1 )
| ( A = n0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(138,plain,
! [A: $i] :
( ( A @ ( n1 @ plus ) )
= ( A @ succ ) ),
inference(cnf,[status(esa)],[137]) ).
thf(139,plain,
! [A: $i] :
( ( A @ ( n1 @ plus ) )
= ( A @ succ ) ),
inference(lifteq,[status(thm)],[138]) ).
thf(1626,plain,
! [A: $i] :
( ( ( n1 @ ( n135299 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[338,337]) ).
thf(1627,plain,
! [A: $i] :
( ( n1 @ ( n135299 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1626]) ).
thf(1628,plain,
! [A: $i] :
( ( n1 != A )
| ( n135299 != A ) ),
inference(simp,[status(thm)],[1627]) ).
thf(1629,plain,
n1 != n135299,
inference(simp,[status(thm)],[1628]) ).
thf(178,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) )
| ~ ( D @ ( F @ leq ) )
| ~ ( F @ ( n0 @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ( C @ ( A @ ( B @ ( C @ sk5 ) ) @ leq ) ) ),
inference(cnfConj,[status(thm)],[176]) ).
thf(186,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( F @ leq ) )
| ~ ( F @ ( n0 @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ( C @ ( A @ ( B @ ( C @ sk5 ) ) @ leq ) )
| ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[178]) ).
thf(19460,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ succ )
!= ( A @ succ ) )
| ( ( n0 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[328,566]) ).
thf(19461,plain,
( ( n0 @ pred )
= tptp_minus_1 ),
inference(pattern_uni,[status(thm)],[19460:[bind(A,$thf( tptp_minus_1 ))]]) ).
thf(2006,plain,
! [A: $i] :
( ( ( n0 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[567,337]) ).
thf(2007,plain,
! [A: $i] :
( ( n0 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2006]) ).
thf(2008,plain,
! [A: $i] :
( ( n0 != A )
| ( n4 != A ) ),
inference(simp,[status(thm)],[2007]) ).
thf(2009,plain,
n4 != n0,
inference(simp,[status(thm)],[2008]) ).
thf(19488,plain,
! [A: $i] :
( ( ( n2 @ succ )
!= ( A @ succ ) )
| ( ( n3 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[2143,566]) ).
thf(19489,plain,
( ( n3 @ pred )
= n2 ),
inference(pattern_uni,[status(thm)],[19488:[bind(A,$thf( n2 ))]]) ).
thf(7943,plain,
( ( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n1 @ ( n0 @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2769,1918]) ).
thf(7944,plain,
( ( pv10 @ pred @ ( sk1 @ leq ) )
!= ( n1 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[7943]) ).
thf(7979,plain,
( ( ( pv10 @ pred )
!= n1 )
| ( sk1 != n0 ) ),
inference(simp,[status(thm)],[7944]) ).
thf(1604,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n0 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[222,337]) ).
thf(1605,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n0 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1604]) ).
thf(1606,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[1605]) ).
thf(1607,plain,
tptp_minus_1 != n0,
inference(simp,[status(thm)],[1606]) ).
thf(1306,plain,
! [A: $i] :
( ( ( n3 @ ( n135299 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[151,337]) ).
thf(1307,plain,
! [A: $i] :
( ( n3 @ ( n135299 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1306]) ).
thf(1308,plain,
! [A: $i] :
( ( n3 != A )
| ( n135299 != A ) ),
inference(simp,[status(thm)],[1307]) ).
thf(1309,plain,
n3 != n135299,
inference(simp,[status(thm)],[1308]) ).
thf(74,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ succ @ leq ) )
=> ( A @ ( B @ gt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leq_succ_gt) ).
thf(536,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ succ @ leq ) )
=> ( A @ ( B @ gt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(19454,plain,
! [A: $i] :
( ( ( A @ succ @ pred )
!= ( pv10 @ pred ) )
| ( A != pv10 ) ),
inference(paramod_ordered,[status(thm)],[566,3378]) ).
thf(19505,plain,
( ( pv10 @ succ )
!= pv10 ),
inference(simp,[status(thm)],[19454]) ).
thf(1242,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( sk2 @ ( n0 @ leq ) ) )
| ~ $true
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(paramod_ordered,[status(thm)],[102,946]) ).
thf(1243,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( sk2 @ ( n0 @ leq ) ) )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[1242]) ).
thf(1280,plain,
( ( sk2 != n4 )
| ( sk1 != n0 )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[1243]) ).
thf(54,axiom,
! [A: $i] :
( ( n4 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',succ_plus_4_r) ).
thf(405,plain,
! [A: $i] :
( ( n4 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(2734,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n135299 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[169,144]) ).
thf(2735,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n135299 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2734]) ).
thf(2736,plain,
n135299 @ ( n0 @ leq ),
inference(pattern_uni,[status(thm)],[2735:[bind(A,$thf( n0 )),bind(B,$thf( n135299 ))]]) ).
thf(180,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) )
| ~ ( D @ ( F @ leq ) )
| ~ ( F @ ( n0 @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ( ( A @ ( B @ ( C @ sk5 ) ) @ ( A @ ( B @ ( C @ sk4 ) ) @ ( B @ a_select3 ) ) )
!= ( A @ ( B @ ( C @ sk4 ) ) @ ( A @ ( B @ ( C @ sk5 ) ) @ ( B @ a_select3 ) ) ) ) ),
inference(cnfConj,[status(thm)],[176]) ).
thf(183,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( F @ leq ) )
| ~ ( F @ ( n0 @ leq ) )
| ~ ( D @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ( ( F @ ( E @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) )
= ( E @ ( F @ ( A @ trans @ ( B @ tptp_mmul ) @ ( A @ tptp_mmul ) @ a_select3 ) ) ) )
| ( ( A @ ( B @ ( C @ sk4 ) ) @ ( A @ ( B @ ( C @ sk5 ) ) @ ( B @ a_select3 ) ) )
!= ( A @ ( B @ ( C @ sk5 ) ) @ ( A @ ( B @ ( C @ sk4 ) ) @ ( B @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[180]) ).
thf(3631,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( n4 @ ( n2 @ leq ) ) )
| ( sk2 != n0 )
| ( center_init != q_init )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2721,1209]) ).
thf(3632,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( n4 @ ( n2 @ leq ) ) )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[3631]) ).
thf(3666,plain,
( ( n4 != n4 )
| ( sk1 != n2 )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[3632]) ).
thf(3690,plain,
( ( sk1 != n2 )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[3666]) ).
thf(35,axiom,
! [A: $i,B: $i] :
( ! [C: $i,D: $i] :
( ( ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( A @ a_select3 ) ) )
= ( C @ ( D @ ( A @ a_select3 ) ) ) ) )
=> ! [C: $i,D: $i] :
( ( ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( A @ trans @ a_select3 ) ) )
= ( C @ ( D @ ( A @ trans @ a_select3 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',matrix_symm_trans) ).
thf(210,plain,
! [A: $i,B: $i] :
( ! [C: $i,D: $i] :
( ( ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( A @ a_select3 ) ) )
= ( C @ ( D @ ( A @ a_select3 ) ) ) ) )
=> ! [C: $i,D: $i] :
( ( ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( A @ trans @ a_select3 ) ) )
= ( C @ ( D @ ( A @ trans @ a_select3 ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(135,plain,
! [A: $i] :
( ( n1 @ ( A @ plus ) )
= ( A @ succ ) ),
inference(cnf,[status(esa)],[134]) ).
thf(136,plain,
! [A: $i] :
( ( n1 @ ( A @ plus ) )
= ( A @ succ ) ),
inference(lifteq,[status(thm)],[135]) ).
thf(3232,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( n4 @ ( tptp_minus_1 @ leq ) ) )
| ~ $true
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(paramod_ordered,[status(thm)],[2718,946]) ).
thf(3233,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( n4 @ ( tptp_minus_1 @ leq ) ) )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[3232]) ).
thf(3245,plain,
( ( n4 != n4 )
| ( sk1 != tptp_minus_1 )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[3233]) ).
thf(3277,plain,
( ( sk1 != tptp_minus_1 )
| ( ( n0 @ ( sk1 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[3245]) ).
thf(192,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) ) )
| ~ ( B @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ~ ( B @ ( D @ leq ) )
| ~ ( D @ ( n0 @ leq ) )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ( A @ ( B @ sk7 ) @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[189]) ).
thf(195,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ~ ( B @ ( D @ leq ) )
| ~ ( D @ ( n0 @ leq ) )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ( A @ ( B @ sk7 ) @ ( n0 @ leq ) )
| ( ( D @ ( C @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[192]) ).
thf(5352,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( n4 @ ( n3 @ leq ) ) )
| ( sk2 != n0 )
| ( center_init != q_init )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2757,1209]) ).
thf(5353,plain,
( ( ( n4 @ ( sk1 @ leq ) )
!= ( n4 @ ( n3 @ leq ) ) )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[5352]) ).
thf(5386,plain,
( ( n4 != n4 )
| ( sk1 != n3 )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[5353]) ).
thf(5413,plain,
( ( sk1 != n3 )
| ( sk2 != n0 )
| ( center_init != q_init ) ),
inference(simp,[status(thm)],[5386]) ).
thf(57,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i] :
( ( ( ( D @ ( C @ ( E @ a_select3 ) ) )
= F )
& ( B = D )
& ( A != C ) )
=> ( ( D @ ( C @ ( G @ ( B @ ( A @ ( E @ tptp_update3 ) ) ) @ a_select3 ) ) )
= F ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sel3_update_2) ).
thf(415,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i] :
( ( ( ( D @ ( C @ ( E @ a_select3 ) ) )
= F )
& ( B = D )
& ( A != C ) )
=> ( ( D @ ( C @ ( G @ ( B @ ( A @ ( E @ tptp_update3 ) ) ) @ a_select3 ) ) )
= F ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(1498,plain,
( ( ( n4 @ ( sk2 @ leq ) )
!= ( n4 @ ( pv10 @ leq ) ) )
| ~ $true
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(paramod_ordered,[status(thm)],[94,953]) ).
thf(1499,plain,
( ( ( n4 @ ( sk2 @ leq ) )
!= ( n4 @ ( pv10 @ leq ) ) )
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[1498]) ).
thf(1517,plain,
( ( n4 != n4 )
| ( sk2 != pv10 )
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[1499]) ).
thf(1532,plain,
( ( sk2 != pv10 )
| ( ( n0 @ ( pv10 @ ( center_init @ a_select3 ) ) )
= init ) ),
inference(simp,[status(thm)],[1517]) ).
thf(66,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( D @ ( B @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( C @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) )
& ! [G: $i,H: $i] :
( ( ( D @ ( H @ leq ) )
& ( C @ ( G @ leq ) )
& ( H @ ( n0 @ leq ) )
& ( G @ ( n0 @ leq ) ) )
=> ( ( H @ ( G @ ( E @ a_select3 ) ) )
= F ) ) )
=> ( ( B @ ( A @ ( F @ ( D @ ( C @ ( E @ tptp_update3 ) ) ) @ a_select3 ) ) )
= F ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sel3_update_3) ).
thf(501,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( D @ ( B @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( C @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) )
& ! [G: $i,H: $i] :
( ( ( D @ ( H @ leq ) )
& ( C @ ( G @ leq ) )
& ( H @ ( n0 @ leq ) )
& ( G @ ( n0 @ leq ) ) )
=> ( ( H @ ( G @ ( E @ a_select3 ) ) )
= F ) ) )
=> ( ( B @ ( A @ ( F @ ( D @ ( C @ ( E @ tptp_update3 ) ) ) @ a_select3 ) ) )
= F ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(32,axiom,
! [A: $i,B: $i] :
( ( B @ succ @ ( A @ succ @ leq ) )
<=> ( B @ ( A @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leq_succ_succ) ).
thf(200,plain,
! [A: $i,B: $i] :
( ( ( B @ ( A @ leq ) )
=> ( B @ succ @ ( A @ succ @ leq ) ) )
& ( ( B @ succ @ ( A @ succ @ leq ) )
=> ( B @ ( A @ leq ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(1909,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n1 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[517,337]) ).
thf(1910,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n1 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1909]) ).
thf(1911,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n1 != A ) ),
inference(simp,[status(thm)],[1910]) ).
thf(1912,plain,
tptp_minus_1 != n1,
inference(simp,[status(thm)],[1911]) ).
thf(100,plain,
n135299 @ ( pv10 @ leq ),
inference(cnfConj,[status(thm)],[93]) ).
thf(36724,plain,
$false,
inference(e,[status(thm)],[5385,1454,479,555,19451,1633,2778,2787,518,523,8695,9818,408,170,8963,550,142,2712,1233,8370,538,1507,1458,185,3994,2763,1518,174,404,184,110,3148,125,1313,196,2745,542,157,559,5521,19604,3657,152,2520,2730,1450,4820,121,821,492,164,147,397,19512,2772,133,116,8094,2718,206,4483,3378,3389,9875,117,102,2790,1047,1730,3261,2733,1021,1519,160,424,3371,137,165,2132,92,197,493,551,1291,2769,229,566,12822,97,329,317,2709,2724,169,4840,141,420,499,328,124,339,476,1937,1207,547,2781,96,515,173,2766,19498,134,128,105,541,2748,953,2001,17271,4919,513,166,148,573,562,2727,1916,11105,12958,3272,577,4605,5271,1965,936,144,159,335,2706,187,113,3683,1933,567,1722,2943,98,1969,1209,2721,8735,2742,552,535,323,140,2757,8529,108,521,130,5641,223,394,19516,4703,1973,19448,563,226,1726,2005,162,2784,209,342,3278,145,557,1611,150,2143,327,1941,409,15551,2715,1637,182,127,1317,338,3769,544,1934,2511,143,2760,1918,99,556,19456,581,104,1289,2775,12957,517,946,158,114,401,139,1629,186,19461,2009,568,19489,207,7979,1607,1309,536,19505,2739,549,1280,168,146,405,2736,183,3690,2123,151,564,210,136,3277,195,5413,400,94,415,2751,326,107,1532,131,501,163,200,111,2754,543,491,222,1912,100,337,122]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV174+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.16/15.44 % Computer : n016.cluster.edu
% 0.16/15.44 % Model : x86_64 x86_64
% 0.16/15.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/15.44 % Memory : 8046.5625MB
% 0.16/15.44 % OS : Linux 6.8.0-71-generic
% 0.16/15.44 % CPULimit : 300
% 0.16/15.44 % WCLimit : 300
% 0.16/15.44 % DateTime : Sat Sep 26 13:23:03 UTC 2026
% 0.16/15.44 % CPUTime :
% 0.16/15.44 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.20/16.03 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.28/16.29 % [INFO] Parsing done (257ms).
% 1.69/16.30 % [INFO] Running in sequential loop mode.
% 2.36/16.71 % [INFO] eprover registered as external prover.
% 2.36/16.71 % [INFO] Scanning for conjecture ...
% 2.57/16.86 % [INFO] Found a conjecture (or negated_conjecture) and 91 axioms. Running axiom selection ...
% 2.77/16.97 % [INFO] Axiom selection finished. Selected 89 axioms (removed 2 axioms).
% 3.06/17.09 % [INFO] Problem is first-order (TPTP FOF).
% 3.06/17.10 % [INFO] Type checking passed.
% 3.06/17.11 % [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 ...
% 81.40/34.45 % External prover 'e' found a proof!
% 81.40/34.45 % [INFO] Killing All external provers ...
% 81.40/34.45 % Time passed: 18870ms (effective reasoning time: 18148ms)
% 81.40/34.45 % 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)>
% 81.40/34.46 % Axioms used in derivation (89): sel3_update_2, gt_2_tptp_minus_1, gt_135299_0, gt_3_1, leq_minus, sel2_update_2, succ_plus_5_l, lt_gt, gt_5_tptp_minus_1, succ_plus_3_r, gt_4_3, transitivity_gt, matrix_symm_inv, matrix_symm_trans, finite_domain_1, gt_5_0, const_array2_select, gt_135299_4, sel3_update_3, leq_geq, gt_1_0, leq_gt2, gt_5_4, succ_plus_1_l, gt_3_2, matrix_symm_add, leq_succ_gt, finite_domain_5, pred_minus_1, successor_3, gt_3_tptp_minus_1, matrix_symm_update_diagonal, sel2_update_1, gt_135299_5, gt_4_2, matrix_symm_sub, gt_5_3, successor_4, gt_succ, succ_plus_4_l, reflexivity_leq, successor_2, leq_gt1, gt_1_tptp_minus_1, finite_domain_2, matrix_symm_aba1, finite_domain_4, matrix_symm_aba2, succ_tptp_minus_1, succ_plus_5_r, gt_0_tptp_minus_1, gt_135299_2, leq_succ_succ, sum_plus_base_float, succ_plus_2_l, gt_4_1, gt_2_0, gt_5_2, const_array1_select, leq_gt_pred, matrix_symm_joseph_update, succ_pred, totality, gt_135299_1, transitivity_leq, finite_domain_3, uniform_int_rand_ranges_lo, gt_135299_tptp_minus_1, sel3_update_1, successor_1, sum_plus_base, irreflexivity_gt, successor_5, gt_3_0, sel2_update_3, pred_succ, succ_plus_1_r, succ_plus_3_l, gt_4_tptp_minus_1, succ_plus_4_r, gt_4_0, succ_plus_2_r, leq_succ_gt_equiv, gt_5_1, uniform_int_rand_ranges_hi, gt_2_1, gt_135299_3, finite_domain_0, leq_succ
% 81.40/34.46 % No. of inferences in proof: 693
% 81.40/34.46 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 18870 ms resp. 18148 ms w/o parsing
% 67.51/34.68 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 67.51/34.68 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------