%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SWV117+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : 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:11 AM UTC 2026
% Result : Theorem 101.67s 22.71s
% Output : Refutation 104.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 111
% Syntax : Number of formulae : 766 ( 332 unt; 0 typ; 11 def)
% Number of atoms : 2722 ( 780 equ; 0 cnn)
% Maximal formula atoms : 217 ( 3 avg)
% Number of connectives : 8191 ( 972 ~;1087 |; 372 &;5590 @)
% ( 5 <=>; 165 =>; 0 <=; 0 <~>)
% Maximal formula depth : 57 ( 5 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 53 ( 50 usr; 27 con; 0-4 aty)
% Number of variables : 869 ( 8 ^; 849 !; 1 ?; 869 :)
% ( 0 !>; 0 ?*; 0 @-; 11 @+)
% Comments :
%------------------------------------------------------------------------------
thf(leq_decl,type,
leq: $i > $i > $o ).
thf(n0_decl,type,
n0: $i ).
thf(pv5_decl,type,
pv5: $i ).
thf(minus_decl,type,
minus: $i > $i > $i ).
thf(n999_decl,type,
n999: $i ).
thf(n1_decl,type,
n1: $i ).
thf(n6_decl,type,
n6: $i ).
thf(a_select3_decl,type,
a_select3: $i > $i > $i > $i ).
thf(q_ds1_filter_decl,type,
q_ds1_filter: $i ).
thf(n3_decl,type,
n3: $i ).
thf(r_ds1_filter_decl,type,
r_ds1_filter: $i ).
thf(pminus_ds1_filter_decl,type,
pminus_ds1_filter: $i ).
thf(plus_decl,type,
plus: $i > $i > $i ).
thf(id_ds1_filter_decl,type,
id_ds1_filter: $i ).
thf(a_select2_decl,type,
a_select2: $i > $i > $i ).
thf(tptp_update2_decl,type,
tptp_update2: $i > $i > $i > $i ).
thf(gt_decl,type,
gt: $i > $i > $o ).
thf(n2_decl,type,
n2: $i ).
thf(tptp_minus_1_decl,type,
tptp_minus_1: $i ).
thf(succ_decl,type,
succ: $i > $i ).
thf(n5_decl,type,
n5: $i ).
thf(n4_decl,type,
n4: $i ).
thf(pred_decl,type,
pred: $i > $i ).
thf(lt_decl,type,
lt: $i > $i > $o ).
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(tptp_madd_decl,type,
tptp_madd: $i > $i > $i ).
thf(geq_decl,type,
geq: $i > $i > $o ).
thf(tptp_msub_decl,type,
tptp_msub: $i > $i > $i ).
thf(tptp_float_0_0_decl,type,
tptp_float_0_0: $i ).
thf(tptp_const_array1_decl,type,
tptp_const_array1: $i > $i > $i ).
thf(uniform_int_rnd_decl,type,
uniform_int_rnd: $i > $i > $i ).
thf(inv_decl,type,
inv: $i > $i ).
thf(sk1_decl,type,
sk1: $o ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $o ).
thf(sk5_decl,type,
sk5: $i ).
thf(sk6_decl,type,
sk6: $i ).
thf(sk7_decl,type,
sk7: $i ).
thf(sk8_decl,type,
sk8: $i ).
thf(sk9_decl,type,
sk9: $i ).
thf(sk10_decl,type,
sk10: $i ).
thf(sk11_decl,type,
sk11: $i > $i > $i > $i > $i ).
thf(sk14_decl,type,
sk14: $i > $i > $i ).
thf(sk15_decl,type,
sk15: $i > $i > $i ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ! [B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( q_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( q_ds1_filter @ a_select3 ) ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ( ( ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( n1 @ ( n6 @ minus ) @ ( sk2 @ leq ) )
& ( A @ ( n0 @ leq ) )
& ( sk2 @ ( n0 @ leq ) ) )
=> ( ( A @ ( sk2 @ ( q_ds1_filter @ a_select3 ) ) )
= ( sk2 @ ( A @ ( q_ds1_filter @ a_select3 ) ) ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: $i] :
~ ! [B: $i] :
( ( ( n1 @ ( n3 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n3 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( r_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( r_ds1_filter @ a_select3 ) ) ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( @+[A: $i] :
~ ( ( ( n1 @ ( n3 @ minus ) @ ( A @ leq ) )
& ( n1 @ ( n3 @ minus ) @ ( sk5 @ leq ) )
& ( A @ ( n0 @ leq ) )
& ( sk5 @ ( n0 @ leq ) ) )
=> ( ( A @ ( sk5 @ ( r_ds1_filter @ a_select3 ) ) )
= ( sk5 @ ( A @ ( r_ds1_filter @ a_select3 ) ) ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( @+[A: $i] :
~ ! [B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( pminus_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( @+[A: $i] :
~ ( ( ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( n1 @ ( n6 @ minus ) @ ( sk7 @ leq ) )
& ( A @ ( n0 @ leq ) )
& ( sk7 @ ( n0 @ leq ) ) )
=> ( ( A @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) )
= ( sk7 @ ( A @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( @+[A: $i] :
~ ( ( ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ! [B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( B @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( id_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( id_ds1_filter @ a_select3 ) ) ) ) ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( @+[A: $i] :
~ ( ( ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) )
= ( sk9 @ ( A @ ( id_ds1_filter @ a_select3 ) ) ) ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( ^ [A: $i,B: $i,C: $i,D: $i] :
@+[E: $i] :
~ ( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) ) )
=> ( ( E @ ( B @ a_select2 ) )
= A ) ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( ^ [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(sk15_def,definition,
( sk15
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( ( A @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) )
& ( A @ ( B @ ( A @ sk14 ) @ leq ) )
& ( B @ ( A @ sk14 ) @ ( n0 @ leq ) ) )
=> ( ( C @ ( B @ ( A @ sk14 ) @ ( B @ a_select3 ) ) )
= ( B @ ( A @ sk14 ) @ ( C @ ( B @ a_select3 ) ) ) ) ) ) ) ).
thf(84,axiom,
( ( n0 @ succ @ succ )
= n2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_2) ).
thf(604,plain,
( ( n0 @ succ @ succ )
= n2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(605,plain,
( ( n0 @ succ @ succ )
= n2 ),
inference(lifteq,[status(thm)],[604]) ).
thf(23,axiom,
( ( n0 @ succ )
= n1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_1) ).
thf(205,plain,
( ( n0 @ succ )
= n1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(206,plain,
( ( n0 @ succ )
= n1 ),
inference(lifteq,[status(thm)],[205]) ).
thf(3158,plain,
( ( n1 @ succ )
= n2 ),
inference(rewrite,[status(thm)],[605,206]) ).
thf(69,axiom,
( ( n0 @ succ @ succ @ succ )
= n3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_3) ).
thf(554,plain,
( ( n0 @ succ @ succ @ succ )
= n3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(555,plain,
( ( n0 @ succ @ succ @ succ )
= n3 ),
inference(lifteq,[status(thm)],[554]) ).
thf(3297,plain,
( ( n1 @ succ @ succ )
= n3 ),
inference(rewrite,[status(thm)],[555,206]) ).
thf(3304,plain,
( ( ( n1 @ succ )
!= ( n1 @ succ ) )
| ( ( n2 @ succ )
= n3 ) ),
inference(paramod_ordered,[status(thm)],[3158,3297]) ).
thf(3305,plain,
( ( n2 @ succ )
= n3 ),
inference(pattern_uni,[status(thm)],[3304:[]]) ).
thf(10,axiom,
! [A: $i] :
( ( A @ succ @ pred )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',pred_succ) ).
thf(179,plain,
! [A: $i] :
( ( A @ succ @ pred )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(180,plain,
! [A: $i] :
( ( A @ succ @ pred )
= A ),
inference(cnf,[status(esa)],[179]) ).
thf(181,plain,
! [A: $i] :
( ( A @ succ @ pred )
= A ),
inference(lifteq,[status(thm)],[180]) ).
thf(5228,plain,
! [A: $i] :
( ( ( n2 @ succ )
!= ( A @ succ ) )
| ( ( n3 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[3305,181]) ).
thf(5229,plain,
( ( n3 @ pred )
= n2 ),
inference(pattern_uni,[status(thm)],[5228:[bind(A,$thf( n2 ))]]) ).
thf(85,axiom,
n5 @ ( n999 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_999_5) ).
thf(606,plain,
n5 @ ( n999 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(14,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ lt ) )
<=> ( A @ ( B @ gt ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lt_gt) ).
thf(189,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)],[14]) ).
thf(190,plain,
( ! [A: $i,B: $i] :
( ( A @ ( B @ gt ) )
=> ( B @ ( A @ lt ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ lt ) )
=> ( A @ ( B @ gt ) ) ) ),
inference(miniscope,[status(thm)],[189]) ).
thf(191,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ lt ) )
| ~ ( C @ ( D @ gt ) ) )
& ( ( A @ ( B @ gt ) )
| ~ ( B @ ( A @ lt ) ) ) ),
inference(cnf,[status(esa)],[190]) ).
thf(193,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ lt ) )
| ~ ( A @ ( B @ gt ) ) ),
inference(cnfConj,[status(thm)],[191]) ).
thf(194,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ lt ) )
| ~ ( A @ ( B @ gt ) ) ),
inference(simp,[status(thm)],[193]) ).
thf(13264,plain,
! [B: $i,A: $i] :
( ( ( n5 @ ( n999 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[606,194]) ).
thf(13265,plain,
! [B: $i,A: $i] :
( ( ( n5 @ ( n999 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13264]) ).
thf(13266,plain,
n999 @ ( n5 @ lt ),
inference(pattern_uni,[status(thm)],[13265:[bind(A,$thf( n5 )),bind(B,$thf( n999 ))]]) ).
thf(97,axiom,
! [A: $i] :
( ( ( n5 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n5 )
| ( A = n4 )
| ( A = n3 )
| ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_5) ).
thf(629,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)],[97]) ).
thf(1,conjecture,
( ( ! [A: $i] :
( ( ( n1 @ ( n1 @ ( n6 @ minus ) @ ( n1 @ plus ) @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ! [B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( B @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( id_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( id_ds1_filter @ a_select3 ) ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( pminus_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( pminus_ds1_filter @ a_select3 ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n3 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n3 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( r_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( r_ds1_filter @ a_select3 ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( q_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( q_ds1_filter @ a_select3 ) ) ) ) )
& ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
& ( pv5 @ ( n0 @ leq ) ) )
=> ( ! [A: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ! [B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( B @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( id_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( id_ds1_filter @ a_select3 ) ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( pminus_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( pminus_ds1_filter @ a_select3 ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n3 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n3 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( r_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( r_ds1_filter @ a_select3 ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( q_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( q_ds1_filter @ a_select3 ) ) ) ) )
& ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
& ( pv5 @ ( n0 @ leq ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quaternion_ds1_symm_0010) ).
thf(2,negated_conjecture,
~ ( ( ! [A: $i] :
( ( ( n1 @ ( n1 @ ( n6 @ minus ) @ ( n1 @ plus ) @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ! [B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( B @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( id_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( id_ds1_filter @ a_select3 ) ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( pminus_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( pminus_ds1_filter @ a_select3 ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n3 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n3 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( r_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( r_ds1_filter @ a_select3 ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( q_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( q_ds1_filter @ a_select3 ) ) ) ) )
& ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
& ( pv5 @ ( n0 @ leq ) ) )
=> ( ! [A: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ! [B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( B @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( id_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( id_ds1_filter @ a_select3 ) ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( pminus_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( pminus_ds1_filter @ a_select3 ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n3 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n3 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( r_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( r_ds1_filter @ a_select3 ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( q_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( q_ds1_filter @ a_select3 ) ) ) ) )
& ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
& ( pv5 @ ( n0 @ leq ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(102,plain,
~ ( ( ! [A: $i] :
( ( ( n1 @ ( n1 @ ( n6 @ minus ) @ ( n1 @ plus ) @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ! [B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( B @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( id_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( id_ds1_filter @ a_select3 ) ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( pminus_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( pminus_ds1_filter @ a_select3 ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n3 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n3 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( r_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( r_ds1_filter @ a_select3 ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( q_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( q_ds1_filter @ a_select3 ) ) ) ) )
& ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
& ( pv5 @ ( n0 @ leq ) ) )
=> ( ! [A: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ! [B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( B @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( id_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( id_ds1_filter @ a_select3 ) ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( pminus_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( pminus_ds1_filter @ a_select3 ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n3 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n3 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( r_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( r_ds1_filter @ a_select3 ) ) ) ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
& ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( q_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( q_ds1_filter @ a_select3 ) ) ) ) )
& ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
& ( pv5 @ ( n0 @ leq ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(103,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) ) )
| ( ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( n1 @ ( n6 @ minus ) @ ( sk10 @ leq ) )
| ( ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( sk10 @ ( n0 @ leq ) )
| ( ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( n1 @ ( n6 @ minus ) @ ( sk9 @ leq ) )
| ( ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( sk9 @ ( n0 @ leq ) )
| ( ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) ) )
| ( n1 @ ( n6 @ minus ) @ ( sk8 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( n1 @ ( n6 @ minus ) @ ( sk10 @ leq ) )
| ( n1 @ ( n6 @ minus ) @ ( sk8 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( sk10 @ ( n0 @ leq ) )
| ( n1 @ ( n6 @ minus ) @ ( sk8 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( n1 @ ( n6 @ minus ) @ ( sk9 @ leq ) )
| ( n1 @ ( n6 @ minus ) @ ( sk8 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( sk9 @ ( n0 @ leq ) )
| ( n1 @ ( n6 @ minus ) @ ( sk8 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) ) )
| ( n1 @ ( n6 @ minus ) @ ( sk7 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( n1 @ ( n6 @ minus ) @ ( sk10 @ leq ) )
| ( n1 @ ( n6 @ minus ) @ ( sk7 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( sk10 @ ( n0 @ leq ) )
| ( n1 @ ( n6 @ minus ) @ ( sk7 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( n1 @ ( n6 @ minus ) @ ( sk9 @ leq ) )
| ( n1 @ ( n6 @ minus ) @ ( sk7 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( sk9 @ ( n0 @ leq ) )
| ( n1 @ ( n6 @ minus ) @ ( sk7 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( n1 @ ( n6 @ minus ) @ ( sk10 @ leq ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( sk10 @ ( n0 @ leq ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( n1 @ ( n6 @ minus ) @ ( sk9 @ leq ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( sk9 @ ( n0 @ leq ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( n1 @ ( n6 @ minus ) @ ( sk10 @ leq ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( sk10 @ ( n0 @ leq ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( n1 @ ( n6 @ minus ) @ ( sk9 @ leq ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( sk9 @ ( n0 @ leq ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ~ sk4
| ( ( sk6 @ ( sk5 @ ( r_ds1_filter @ a_select3 ) ) )
!= ( sk5 @ ( sk6 @ ( r_ds1_filter @ a_select3 ) ) ) )
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ~ sk4
| ( n1 @ ( n3 @ minus ) @ ( sk6 @ leq ) )
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ~ sk4
| ( n1 @ ( n3 @ minus ) @ ( sk5 @ leq ) )
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ~ sk4
| ( sk6 @ ( n0 @ leq ) )
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ~ sk4
| ( sk5 @ ( n0 @ leq ) )
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ~ sk1
| ( ( sk3 @ ( sk2 @ ( q_ds1_filter @ a_select3 ) ) )
!= ( sk2 @ ( sk3 @ ( q_ds1_filter @ a_select3 ) ) ) )
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ~ sk1
| ( n1 @ ( n6 @ minus ) @ ( sk3 @ leq ) )
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ~ sk1
| ( n1 @ ( n6 @ minus ) @ ( sk2 @ leq ) )
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ~ sk1
| ( sk3 @ ( n0 @ leq ) )
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ~ sk1
| ( sk2 @ ( n0 @ leq ) )
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) )
& ( ( ( H @ ( G @ ( id_ds1_filter @ a_select3 ) ) )
= ( G @ ( H @ ( id_ds1_filter @ a_select3 ) ) ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( H @ leq ) )
| ~ ( H @ ( n0 @ leq ) )
| ~ ( n1 @ ( n1 @ ( n6 @ minus ) @ ( n1 @ plus ) @ minus ) @ ( G @ leq ) )
| ~ ( G @ ( n0 @ leq ) ) )
& ( ( ( F @ ( E @ ( pminus_ds1_filter @ a_select3 ) ) )
= ( E @ ( F @ ( pminus_ds1_filter @ a_select3 ) ) ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( F @ leq ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( E @ leq ) )
| ~ ( F @ ( n0 @ leq ) )
| ~ ( E @ ( n0 @ leq ) ) )
& ( ( ( D @ ( C @ ( r_ds1_filter @ a_select3 ) ) )
= ( C @ ( D @ ( r_ds1_filter @ a_select3 ) ) ) )
| ~ ( n1 @ ( n3 @ minus ) @ ( D @ leq ) )
| ~ ( n1 @ ( n3 @ minus ) @ ( C @ leq ) )
| ~ ( D @ ( n0 @ leq ) )
| ~ ( C @ ( n0 @ leq ) ) )
& ( ( ( B @ ( A @ ( q_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( q_ds1_filter @ a_select3 ) ) ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) )
& ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
& ( pv5 @ ( n0 @ leq ) ) ),
inference(cnf,[status(esa)],[102]) ).
thf(115,plain,
( ~ sk4
| ( ( sk6 @ ( sk5 @ ( r_ds1_filter @ a_select3 ) ) )
!= ( sk5 @ ( sk6 @ ( r_ds1_filter @ a_select3 ) ) ) )
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(147,plain,
( ~ sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) )
| ( ( sk5 @ ( sk6 @ ( r_ds1_filter @ a_select3 ) ) )
!= ( sk6 @ ( sk5 @ ( r_ds1_filter @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[115]) ).
thf(128,plain,
pv5 @ ( n0 @ leq ),
inference(cnfConj,[status(thm)],[103]) ).
thf(105,plain,
n1 @ ( n999 @ minus ) @ ( pv5 @ leq ),
inference(cnfConj,[status(thm)],[103]) ).
thf(5400,plain,
( ~ sk4
| sk1
| ~ $true
| ~ $true
| ( ( sk5 @ ( sk6 @ ( r_ds1_filter @ a_select3 ) ) )
!= ( sk6 @ ( sk5 @ ( r_ds1_filter @ a_select3 ) ) ) ) ),
inference(rewrite,[status(thm)],[147,128,105]) ).
thf(5401,plain,
( ~ sk4
| sk1
| ( ( sk5 @ ( sk6 @ ( r_ds1_filter @ a_select3 ) ) )
!= ( sk6 @ ( sk5 @ ( r_ds1_filter @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[5400]) ).
thf(5402,plain,
( ~ sk4
| ( sk6 != sk5 )
| ( sk6 != sk5 )
| ( r_ds1_filter != r_ds1_filter )
| sk1 ),
inference(simp,[status(thm)],[5401]) ).
thf(5430,plain,
( ~ sk4
| ( sk6 != sk5 )
| sk1 ),
inference(simp,[status(thm)],[5402]) ).
thf(134,plain,
( ~ sk1
| ( sk2 @ ( n0 @ leq ) )
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(942,plain,
( ~ sk1
| ( sk2 @ ( n0 @ leq ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[134,128,105]) ).
thf(943,plain,
( ~ sk1
| ( sk2 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[942]) ).
thf(125,plain,
( ~ sk1
| ( sk3 @ ( n0 @ leq ) )
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(654,plain,
( ~ sk1
| ( sk3 @ ( n0 @ leq ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[125,128,105]) ).
thf(655,plain,
( ~ sk1
| ( sk3 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[654]) ).
thf(110,plain,
( ~ sk1
| ( n1 @ ( n6 @ minus ) @ ( sk3 @ leq ) )
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(994,plain,
( ~ sk1
| ( n1 @ ( n6 @ minus ) @ ( sk3 @ leq ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[110,128,105]) ).
thf(995,plain,
( ~ sk1
| ( n1 @ ( n6 @ minus ) @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[994]) ).
thf(116,plain,
( ~ sk1
| ( n1 @ ( n6 @ minus ) @ ( sk2 @ leq ) )
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(1348,plain,
( ~ sk1
| ( n1 @ ( n6 @ minus ) @ ( sk2 @ leq ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[116,128,105]) ).
thf(1349,plain,
( ~ sk1
| ( n1 @ ( n6 @ minus ) @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[1348]) ).
thf(120,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( q_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( q_ds1_filter @ a_select3 ) ) ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(148,plain,
! [B: $i,A: $i] :
( ~ ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( B @ ( A @ ( q_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( q_ds1_filter @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[120]) ).
thf(129,plain,
( ~ sk1
| ( ( sk3 @ ( sk2 @ ( q_ds1_filter @ a_select3 ) ) )
!= ( sk2 @ ( sk3 @ ( q_ds1_filter @ a_select3 ) ) ) )
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(146,plain,
( ~ sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) )
| ( ( sk2 @ ( sk3 @ ( q_ds1_filter @ a_select3 ) ) )
!= ( sk3 @ ( sk2 @ ( q_ds1_filter @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[129]) ).
thf(666,plain,
( ~ sk1
| ~ $true
| ~ $true
| ( ( sk2 @ ( sk3 @ ( q_ds1_filter @ a_select3 ) ) )
!= ( sk3 @ ( sk2 @ ( q_ds1_filter @ a_select3 ) ) ) ) ),
inference(rewrite,[status(thm)],[146,128,105]) ).
thf(667,plain,
( ~ sk1
| ( ( sk2 @ ( sk3 @ ( q_ds1_filter @ a_select3 ) ) )
!= ( sk3 @ ( sk2 @ ( q_ds1_filter @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[666]) ).
thf(5949,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( q_ds1_filter @ a_select3 ) ) )
!= ( sk2 @ ( sk3 @ ( q_ds1_filter @ a_select3 ) ) ) )
| ~ sk1
| ( ( A @ ( B @ ( q_ds1_filter @ a_select3 ) ) )
!= ( sk3 @ ( sk2 @ ( q_ds1_filter @ a_select3 ) ) ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[148,667]) ).
thf(5950,plain,
( ~ sk1
| ( ( sk3 @ ( sk2 @ ( q_ds1_filter @ a_select3 ) ) )
!= ( sk3 @ ( sk2 @ ( q_ds1_filter @ a_select3 ) ) ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( sk2 @ leq ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( sk3 @ leq ) )
| ~ ( sk2 @ ( n0 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[5949:[bind(A,$thf( sk3 )),bind(B,$thf( sk2 ))]]) ).
thf(6127,plain,
( ~ sk1
| ~ ( n1 @ ( n6 @ minus ) @ ( sk2 @ leq ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( sk3 @ leq ) )
| ~ ( sk2 @ ( n0 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[5950]) ).
thf(6499,plain,
( ( ( n1 @ ( n6 @ minus ) @ ( sk2 @ leq ) )
!= ( n1 @ ( n6 @ minus ) @ ( sk2 @ leq ) ) )
| ~ sk1
| ~ $true
| ~ ( n1 @ ( n6 @ minus ) @ ( sk3 @ leq ) )
| ~ ( sk2 @ ( n0 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[1349,6127]) ).
thf(6500,plain,
( ( ( n1 @ ( n6 @ minus ) @ ( sk2 @ leq ) )
!= ( n1 @ ( n6 @ minus ) @ ( sk2 @ leq ) ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( sk3 @ leq ) )
| ~ ( sk2 @ ( n0 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) )
| ~ sk1 ),
inference(simp,[status(thm)],[6499]) ).
thf(6501,plain,
( ~ ( n1 @ ( n6 @ minus ) @ ( sk3 @ leq ) )
| ~ ( sk2 @ ( n0 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) )
| ~ sk1 ),
inference(pattern_uni,[status(thm)],[6500:[]]) ).
thf(6832,plain,
( ( ( n1 @ ( n6 @ minus ) @ ( sk3 @ leq ) )
!= ( n1 @ ( n6 @ minus ) @ ( sk3 @ leq ) ) )
| ~ $true
| ~ ( sk2 @ ( n0 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) )
| ~ sk1
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[995,6501]) ).
thf(6833,plain,
( ( ( n1 @ ( n6 @ minus ) @ ( sk3 @ leq ) )
!= ( n1 @ ( n6 @ minus ) @ ( sk3 @ leq ) ) )
| ~ ( sk2 @ ( n0 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) )
| ~ sk1 ),
inference(simp,[status(thm)],[6832]) ).
thf(6834,plain,
( ~ ( sk2 @ ( n0 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) )
| ~ sk1 ),
inference(pattern_uni,[status(thm)],[6833:[]]) ).
thf(6879,plain,
( ( ( sk3 @ ( n0 @ leq ) )
!= ( sk3 @ ( n0 @ leq ) ) )
| ~ ( sk2 @ ( n0 @ leq ) )
| ~ $true
| ~ sk1
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[655,6834]) ).
thf(6880,plain,
( ( ( sk3 @ ( n0 @ leq ) )
!= ( sk3 @ ( n0 @ leq ) ) )
| ~ ( sk2 @ ( n0 @ leq ) )
| ~ sk1 ),
inference(simp,[status(thm)],[6879]) ).
thf(6881,plain,
( ~ ( sk2 @ ( n0 @ leq ) )
| ~ sk1 ),
inference(pattern_uni,[status(thm)],[6880:[]]) ).
thf(7089,plain,
( ( ( sk2 @ ( n0 @ leq ) )
!= ( sk2 @ ( n0 @ leq ) ) )
| ~ $true
| ~ sk1
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[943,6881]) ).
thf(7090,plain,
( ( ( sk2 @ ( n0 @ leq ) )
!= ( sk2 @ ( n0 @ leq ) ) )
| ~ sk1 ),
inference(simp,[status(thm)],[7089]) ).
thf(7091,plain,
~ sk1,
inference(pattern_uni,[status(thm)],[7090:[]]) ).
thf(7271,plain,
( ~ sk4
| ( sk6 != sk5 )
| $false ),
inference(rewrite,[status(thm)],[5430,7091]) ).
thf(7272,plain,
( ~ sk4
| ( sk6 != sk5 ) ),
inference(simp,[status(thm)],[7271]) ).
thf(24,axiom,
( ( n0 @ succ @ succ @ succ @ succ )
= n4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_4) ).
thf(207,plain,
( ( n0 @ succ @ succ @ succ @ succ )
= n4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(208,plain,
( ( n0 @ succ @ succ @ succ @ succ )
= n4 ),
inference(lifteq,[status(thm)],[207]) ).
thf(3336,plain,
( ( n1 @ succ @ succ @ succ )
= n4 ),
inference(rewrite,[status(thm)],[208,206]) ).
thf(3344,plain,
( ( ( n1 @ succ @ succ )
!= ( n1 @ succ @ succ ) )
| ( ( n3 @ succ )
= n4 ) ),
inference(paramod_ordered,[status(thm)],[3297,3336]) ).
thf(3345,plain,
( ( n3 @ succ )
= n4 ),
inference(pattern_uni,[status(thm)],[3344:[]]) ).
thf(33,axiom,
n3 @ ( n4 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_3) ).
thf(226,plain,
n3 @ ( n4 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(12,axiom,
! [A: $i] :
~ ( A @ ( A @ gt ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',irreflexivity_gt) ).
thf(185,plain,
! [A: $i] :
~ ( A @ ( A @ gt ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(186,plain,
~ ? [A: $i] : ( A @ ( A @ gt ) ),
inference(miniscope,[status(thm)],[185]) ).
thf(187,plain,
! [A: $i] :
~ ( A @ ( A @ gt ) ),
inference(cnf,[status(esa)],[186]) ).
thf(1992,plain,
! [A: $i] :
( ( ( n3 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[226,187]) ).
thf(1993,plain,
! [A: $i] :
( ( n3 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1992]) ).
thf(1994,plain,
! [A: $i] :
( ( n3 != A )
| ( n4 != A ) ),
inference(simp,[status(thm)],[1993]) ).
thf(1995,plain,
n4 != n3,
inference(simp,[status(thm)],[1994]) ).
thf(61,axiom,
! [A: $i] :
( ( n4 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_4_r) ).
thf(466,plain,
! [A: $i] :
( ( n4 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(467,plain,
! [A: $i] :
( ( n4 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
inference(cnf,[status(esa)],[466]) ).
thf(468,plain,
! [A: $i] :
( ( n4 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
inference(lifteq,[status(thm)],[467]) ).
thf(65,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/sandbox/benchmark/theBenchmark.p',matrix_symm_add) ).
thf(481,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)],[65]) ).
thf(101,axiom,
n3 @ ( n999 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_999_3) ).
thf(637,plain,
n3 @ ( n999 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[101]) ).
thf(13300,plain,
! [B: $i,A: $i] :
( ( ( n3 @ ( n999 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[637,194]) ).
thf(13301,plain,
! [B: $i,A: $i] :
( ( ( n3 @ ( n999 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13300]) ).
thf(13302,plain,
n999 @ ( n3 @ lt ),
inference(pattern_uni,[status(thm)],[13301:[bind(A,$thf( n3 )),bind(B,$thf( n999 ))]]) ).
thf(21,axiom,
n2 @ ( n6 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_2) ).
thf(203,plain,
n2 @ ( n6 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(938,plain,
! [A: $i] :
( ( ( n2 @ ( n6 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[203,187]) ).
thf(939,plain,
! [A: $i] :
( ( n2 @ ( n6 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[938]) ).
thf(940,plain,
! [A: $i] :
( ( n2 != A )
| ( n6 != A ) ),
inference(simp,[status(thm)],[939]) ).
thf(941,plain,
n2 != n6,
inference(simp,[status(thm)],[940]) ).
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/sandbox/benchmark/theBenchmark.p',sel2_update_2) ).
thf(170,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(5224,plain,
! [A: $i] :
( ( ( n1 @ succ )
!= ( A @ succ ) )
| ( ( n2 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[3158,181]) ).
thf(5225,plain,
( ( n2 @ pred )
= n1 ),
inference(pattern_uni,[status(thm)],[5224:[bind(A,$thf( n1 ))]]) ).
thf(19,axiom,
n1 @ ( n2 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_2_1) ).
thf(200,plain,
n1 @ ( n2 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(680,plain,
! [A: $i] :
( ( ( n1 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[200,187]) ).
thf(681,plain,
! [A: $i] :
( ( n1 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[680]) ).
thf(682,plain,
! [A: $i] :
( ( n1 != A )
| ( n2 != A ) ),
inference(simp,[status(thm)],[681]) ).
thf(683,plain,
n2 != n1,
inference(simp,[status(thm)],[682]) ).
thf(26,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/sandbox/benchmark/theBenchmark.p',sel2_update_3) ).
thf(210,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)],[26]) ).
thf(211,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 @ sk11 ) ) ) @ ( C @ a_select2 ) )
!= D ) )
& ( ( ( A @ ( D @ ( B @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D )
| ~ ( B @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( B @ ( A @ ( B @ ( C @ ( D @ sk11 ) ) ) @ leq ) ) )
& ( ( ( A @ ( D @ ( B @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D )
| ~ ( B @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( A @ ( B @ ( C @ ( D @ sk11 ) ) ) @ ( n0 @ leq ) ) ) ),
inference(cnf,[status(esa)],[210]) ).
thf(214,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 @ sk11 ) ) ) @ ( C @ a_select2 ) )
!= D ) ),
inference(cnfConj,[status(thm)],[211]) ).
thf(217,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 @ sk11 ) ) ) @ ( C @ a_select2 ) )
!= D ) ),
inference(lifteq,[status(thm)],[214]) ).
thf(25,axiom,
tptp_minus_1 @ ( n6 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_tptp_minus_1) ).
thf(209,plain,
tptp_minus_1 @ ( n6 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(13339,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n6 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[209,194]) ).
thf(13340,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n6 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13339]) ).
thf(13341,plain,
n6 @ ( tptp_minus_1 @ lt ),
inference(pattern_uni,[status(thm)],[13340:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n6 ))]]) ).
thf(99,axiom,
n5 @ ( n6 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_5) ).
thf(633,plain,
n5 @ ( n6 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[99]) ).
thf(3150,plain,
! [A: $i] :
( ( ( n5 @ ( n6 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[633,187]) ).
thf(3151,plain,
! [A: $i] :
( ( n5 @ ( n6 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[3150]) ).
thf(3152,plain,
! [A: $i] :
( ( n5 != A )
| ( n6 != A ) ),
inference(simp,[status(thm)],[3151]) ).
thf(3153,plain,
n5 != n6,
inference(simp,[status(thm)],[3152]) ).
thf(89,axiom,
n0 @ ( n6 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_0) ).
thf(614,plain,
n0 @ ( n6 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(20,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ gt ) )
=> ( B @ ( A @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_gt1) ).
thf(201,plain,
! [A: $i,B: $i] :
( ( A @ ( B @ gt ) )
=> ( B @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(202,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ~ ( A @ ( B @ gt ) ) ),
inference(cnf,[status(esa)],[201]) ).
thf(80,axiom,
! [A: $i] : ( A @ ( A @ leq ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_leq) ).
thf(597,plain,
! [A: $i] : ( A @ ( A @ leq ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(66,axiom,
! [A: $i,B: $i] :
( ( A @ ( n0 @ leq ) )
=> ( A @ ( A @ ( B @ uniform_int_rnd ) @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',uniform_int_rand_ranges_hi) ).
thf(533,plain,
! [A: $i,B: $i] :
( ( A @ ( n0 @ leq ) )
=> ( A @ ( A @ ( B @ uniform_int_rnd ) @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(144,plain,
( ~ sk4
| ( n1 @ ( n3 @ minus ) @ ( sk6 @ leq ) )
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(1748,plain,
( ~ sk4
| ( n1 @ ( n3 @ minus ) @ ( sk6 @ leq ) )
| sk1
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[144,128,105]) ).
thf(1749,plain,
( ~ sk4
| ( n1 @ ( n3 @ minus ) @ ( sk6 @ leq ) )
| sk1 ),
inference(simp,[status(thm)],[1748]) ).
thf(7259,plain,
( ~ sk4
| ( n1 @ ( n3 @ minus ) @ ( sk6 @ leq ) )
| $false ),
inference(rewrite,[status(thm)],[1749,7091]) ).
thf(7260,plain,
( ~ sk4
| ( n1 @ ( n3 @ minus ) @ ( sk6 @ leq ) ) ),
inference(simp,[status(thm)],[7259]) ).
thf(45,axiom,
! [A: $i] :
( ( n1 @ ( A @ minus ) )
= ( A @ pred ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',pred_minus_1) ).
thf(285,plain,
! [A: $i] :
( ( n1 @ ( A @ minus ) )
= ( A @ pred ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(286,plain,
! [A: $i] :
( ( n1 @ ( A @ minus ) )
= ( A @ pred ) ),
inference(cnf,[status(esa)],[285]) ).
thf(287,plain,
! [A: $i] :
( ( n1 @ ( A @ minus ) )
= ( A @ pred ) ),
inference(lifteq,[status(thm)],[286]) ).
thf(10393,plain,
( ~ sk4
| ( n3 @ pred @ ( sk6 @ leq ) ) ),
inference(rewrite,[status(thm)],[7260,287]) ).
thf(10394,plain,
( ( ( n3 @ pred )
!= ( n3 @ pred ) )
| ~ sk4
| ( n2 @ ( sk6 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[5229,10393]) ).
thf(10395,plain,
( ~ sk4
| ( n2 @ ( sk6 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[10394:[]]) ).
thf(133,plain,
( ~ sk4
| ( sk5 @ ( n0 @ leq ) )
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(968,plain,
( ~ sk4
| ( sk5 @ ( n0 @ leq ) )
| sk1
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[133,128,105]) ).
thf(969,plain,
( ~ sk4
| ( sk5 @ ( n0 @ leq ) )
| sk1 ),
inference(simp,[status(thm)],[968]) ).
thf(7187,plain,
( ~ sk4
| ( sk5 @ ( n0 @ leq ) )
| $false ),
inference(rewrite,[status(thm)],[969,7091]) ).
thf(7188,plain,
( ~ sk4
| ( sk5 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[7187]) ).
thf(79,axiom,
n0 @ ( n2 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_2_0) ).
thf(596,plain,
n0 @ ( n2 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(2683,plain,
! [A: $i] :
( ( ( n0 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[596,187]) ).
thf(2684,plain,
! [A: $i] :
( ( n0 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2683]) ).
thf(2685,plain,
! [A: $i] :
( ( n0 != A )
| ( n2 != A ) ),
inference(simp,[status(thm)],[2684]) ).
thf(2686,plain,
n2 != n0,
inference(simp,[status(thm)],[2685]) ).
thf(22,axiom,
n1 @ ( n3 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_1) ).
thf(204,plain,
n1 @ ( n3 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(13315,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[204,194]) ).
thf(13316,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13315]) ).
thf(13317,plain,
n3 @ ( n1 @ lt ),
inference(pattern_uni,[status(thm)],[13316:[bind(A,$thf( n1 )),bind(B,$thf( n3 ))]]) ).
thf(31,axiom,
n1 @ ( n5 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_1) ).
thf(224,plain,
n1 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(1869,plain,
! [A: $i] :
( ( ( n1 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[224,187]) ).
thf(1870,plain,
! [A: $i] :
( ( n1 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1869]) ).
thf(1871,plain,
! [A: $i] :
( ( n1 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[1870]) ).
thf(1872,plain,
n5 != n1,
inference(simp,[status(thm)],[1871]) ).
thf(63,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/sandbox/benchmark/theBenchmark.p',sel3_update_2) ).
thf(472,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)],[63]) ).
thf(53,axiom,
( ( tptp_minus_1 @ succ )
= n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_tptp_minus_1) ).
thf(393,plain,
( ( tptp_minus_1 @ succ )
= n0 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(394,plain,
( ( tptp_minus_1 @ succ )
= n0 ),
inference(lifteq,[status(thm)],[393]) ).
thf(5226,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ succ )
!= ( A @ succ ) )
| ( ( n0 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[394,181]) ).
thf(5227,plain,
( ( n0 @ pred )
= tptp_minus_1 ),
inference(pattern_uni,[status(thm)],[5226:[bind(A,$thf( tptp_minus_1 ))]]) ).
thf(46,axiom,
! [A: $i] :
( ( ( n0 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( A = n0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_0) ).
thf(288,plain,
! [A: $i] :
( ( ( n0 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( A = n0 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(13285,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[224,194]) ).
thf(13286,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13285]) ).
thf(13287,plain,
n5 @ ( n1 @ lt ),
inference(pattern_uni,[status(thm)],[13286:[bind(A,$thf( n1 )),bind(B,$thf( n5 ))]]) ).
thf(54,axiom,
! [A: $i] :
( ( A @ ( n5 @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_5_l) ).
thf(395,plain,
! [A: $i] :
( ( A @ ( n5 @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(396,plain,
! [A: $i] :
( ( A @ ( n5 @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
inference(cnf,[status(esa)],[395]) ).
thf(397,plain,
! [A: $i] :
( ( A @ ( n5 @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
inference(lifteq,[status(thm)],[396]) ).
thf(92,axiom,
! [A: $i] :
( ( n2 @ ( A @ plus ) )
= ( A @ succ @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_2_r) ).
thf(619,plain,
! [A: $i] :
( ( n2 @ ( A @ plus ) )
= ( A @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(620,plain,
! [A: $i] :
( ( n2 @ ( A @ plus ) )
= ( A @ succ @ succ ) ),
inference(cnf,[status(esa)],[619]) ).
thf(621,plain,
! [A: $i] :
( ( n2 @ ( A @ plus ) )
= ( A @ succ @ succ ) ),
inference(lifteq,[status(thm)],[620]) ).
thf(10359,plain,
! [B: $i,A: $i] :
( ( ( A @ ( n5 @ plus ) )
!= ( n2 @ ( B @ plus ) ) )
| ( ( A @ succ @ succ @ succ @ succ @ succ )
= ( B @ succ @ succ ) ) ),
inference(paramod_ordered,[status(thm)],[397,621]) ).
thf(10360,plain,
( ( n2 @ succ @ succ @ succ @ succ @ succ )
= ( n5 @ succ @ succ ) ),
inference(pattern_uni,[status(thm)],[10359:[bind(A,$thf( n2 )),bind(B,$thf( n5 ))]]) ).
thf(96,axiom,
( ( n0 @ succ @ succ @ succ @ succ @ succ )
= n5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_5) ).
thf(627,plain,
( ( n0 @ succ @ succ @ succ @ succ @ succ )
= n5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(628,plain,
( ( n0 @ succ @ succ @ succ @ succ @ succ )
= n5 ),
inference(lifteq,[status(thm)],[627]) ).
thf(3671,plain,
( ( n1 @ succ @ succ @ succ @ succ )
= n5 ),
inference(rewrite,[status(thm)],[628,206]) ).
thf(86,axiom,
( ( n0 @ succ @ succ @ succ @ succ @ succ @ succ )
= n6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_6) ).
thf(607,plain,
( ( n0 @ succ @ succ @ succ @ succ @ succ @ succ )
= n6 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(608,plain,
( ( n0 @ succ @ succ @ succ @ succ @ succ @ succ )
= n6 ),
inference(lifteq,[status(thm)],[607]) ).
thf(3934,plain,
( ( n1 @ succ @ succ @ succ @ succ @ succ )
= n6 ),
inference(rewrite,[status(thm)],[608,206]) ).
thf(3971,plain,
( ( ( n1 @ succ @ succ @ succ @ succ )
!= ( n1 @ succ @ succ @ succ @ succ ) )
| ( ( n5 @ succ )
= n6 ) ),
inference(paramod_ordered,[status(thm)],[3671,3934]) ).
thf(3972,plain,
( ( n5 @ succ )
= n6 ),
inference(pattern_uni,[status(thm)],[3971:[]]) ).
thf(10799,plain,
( ( n3 @ succ @ succ @ succ @ succ )
= ( n6 @ succ ) ),
inference(rewrite,[status(thm)],[10360,3972,3305]) ).
thf(10802,plain,
( ( ( n3 @ succ )
!= ( n3 @ succ ) )
| ( ( n4 @ succ @ succ @ succ )
= ( n6 @ succ ) ) ),
inference(paramod_ordered,[status(thm)],[3345,10799]) ).
thf(10803,plain,
( ( n4 @ succ @ succ @ succ )
= ( n6 @ succ ) ),
inference(pattern_uni,[status(thm)],[10802:[]]) ).
thf(3714,plain,
( ( ( n1 @ succ @ succ @ succ )
!= ( n1 @ succ @ succ @ succ ) )
| ( ( n4 @ succ )
= n5 ) ),
inference(paramod_ordered,[status(thm)],[3336,3671]) ).
thf(3715,plain,
( ( n4 @ succ )
= n5 ),
inference(pattern_uni,[status(thm)],[3714:[]]) ).
thf(10982,plain,
( ( n5 @ succ @ succ )
= ( n6 @ succ ) ),
inference(rewrite,[status(thm)],[10803,3715]) ).
thf(7,axiom,
! [A: $i] : ( A @ ( A @ succ @ gt ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_succ) ).
thf(175,plain,
! [A: $i] : ( A @ ( A @ succ @ gt ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(176,plain,
! [A: $i] : ( A @ ( A @ succ @ gt ) ),
inference(cnf,[status(esa)],[175]) ).
thf(11031,plain,
! [A: $i] :
( ( ( n5 @ succ @ succ )
!= ( A @ succ ) )
| ( A @ ( n6 @ succ @ gt ) ) ),
inference(paramod_ordered,[status(thm)],[10982,176]) ).
thf(11032,plain,
n5 @ succ @ ( n6 @ succ @ gt ),
inference(pattern_uni,[status(thm)],[11031:[bind(A,$thf( n5 @ succ ))]]) ).
thf(11151,plain,
n6 @ ( n6 @ succ @ gt ),
inference(rewrite,[status(thm)],[11032,3972]) ).
thf(142,plain,
( ( sk10 @ ( n0 @ leq ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(4545,plain,
( ( sk10 @ ( n0 @ leq ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[142,128,105]) ).
thf(4546,plain,
( ( sk10 @ ( n0 @ leq ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(simp,[status(thm)],[4545]) ).
thf(4612,plain,
( ~ $true
| ( ( sk10 @ ( n0 @ leq ) )
!= ( sk7 @ ( n0 @ leq ) ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(eqfactor_ordered,[status(thm)],[4546]) ).
thf(4614,plain,
( ( sk10 != sk7 )
| ( n0 != n0 )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(simp,[status(thm)],[4612]) ).
thf(4618,plain,
( ( sk10 != sk7 )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(simp,[status(thm)],[4614]) ).
thf(7177,plain,
( ( sk10 != sk7 )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| $false ),
inference(rewrite,[status(thm)],[4618,7091]) ).
thf(7178,plain,
( ( sk10 != sk7 )
| ( sk7 @ ( n0 @ leq ) )
| sk4 ),
inference(simp,[status(thm)],[7177]) ).
thf(171,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)],[170]) ).
thf(172,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)],[171]) ).
thf(173,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)],[172]) ).
thf(174,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)],[173]) ).
thf(56,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/sandbox/benchmark/theBenchmark.p',matrix_symm_sub) ).
thf(404,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)],[56]) ).
thf(71,axiom,
! [A: $i] :
( ( n1 @ ( A @ plus ) )
= ( A @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_1_r) ).
thf(568,plain,
! [A: $i] :
( ( n1 @ ( A @ plus ) )
= ( A @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(569,plain,
! [A: $i] :
( ( n1 @ ( A @ plus ) )
= ( A @ succ ) ),
inference(cnf,[status(esa)],[568]) ).
thf(570,plain,
! [A: $i] :
( ( n1 @ ( A @ plus ) )
= ( A @ succ ) ),
inference(lifteq,[status(thm)],[569]) ).
thf(11,axiom,
! [A: $i] :
( ( A @ pred @ succ )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_pred) ).
thf(182,plain,
! [A: $i] :
( ( A @ pred @ succ )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(183,plain,
! [A: $i] :
( ( A @ pred @ succ )
= A ),
inference(cnf,[status(esa)],[182]) ).
thf(184,plain,
! [A: $i] :
( ( A @ pred @ succ )
= A ),
inference(lifteq,[status(thm)],[183]) ).
thf(41,axiom,
n3 @ ( n5 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_3) ).
thf(265,plain,
n3 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(13273,plain,
! [B: $i,A: $i] :
( ( ( n3 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[265,194]) ).
thf(13274,plain,
! [B: $i,A: $i] :
( ( ( n3 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13273]) ).
thf(13275,plain,
n5 @ ( n3 @ lt ),
inference(pattern_uni,[status(thm)],[13274:[bind(A,$thf( n3 )),bind(B,$thf( n5 ))]]) ).
thf(16,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ gt ) )
& ( B @ ( A @ gt ) ) )
=> ( C @ ( A @ gt ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_gt) ).
thf(196,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ gt ) )
& ( B @ ( A @ gt ) ) )
=> ( C @ ( A @ gt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(5230,plain,
! [A: $i] :
( ( ( n4 @ succ )
!= ( A @ succ ) )
| ( ( n5 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[3715,181]) ).
thf(5231,plain,
( ( n5 @ pred )
= n4 ),
inference(pattern_uni,[status(thm)],[5230:[bind(A,$thf( n4 ))]]) ).
thf(44,axiom,
tptp_minus_1 @ ( n0 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_0_tptp_minus_1) ).
thf(284,plain,
tptp_minus_1 @ ( n0 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(35,axiom,
! [A: $i] :
( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
= n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_plus_base) ).
thf(228,plain,
! [A: $i] :
( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
= n0 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(74,axiom,
tptp_minus_1 @ ( n1 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_1_tptp_minus_1) ).
thf(575,plain,
tptp_minus_1 @ ( n1 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(13363,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n1 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[575,194]) ).
thf(13364,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n1 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13363]) ).
thf(13365,plain,
n1 @ ( tptp_minus_1 @ lt ),
inference(pattern_uni,[status(thm)],[13364:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n1 ))]]) ).
thf(39,axiom,
n0 @ ( n999 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_999_0) ).
thf(261,plain,
n0 @ ( n999 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(13261,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n999 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[261,194]) ).
thf(13262,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n999 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13261]) ).
thf(13263,plain,
n999 @ ( n0 @ lt ),
inference(pattern_uni,[status(thm)],[13262:[bind(A,$thf( n0 )),bind(B,$thf( n999 ))]]) ).
thf(13348,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n6 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[203,194]) ).
thf(13349,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n6 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13348]) ).
thf(13350,plain,
n6 @ ( n2 @ lt ),
inference(pattern_uni,[status(thm)],[13349:[bind(A,$thf( n2 )),bind(B,$thf( n6 ))]]) ).
thf(95,axiom,
n4 @ ( n6 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_4) ).
thf(626,plain,
n4 @ ( n6 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(13330,plain,
! [B: $i,A: $i] :
( ( ( n4 @ ( n6 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[626,194]) ).
thf(13331,plain,
! [B: $i,A: $i] :
( ( ( n4 @ ( n6 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13330]) ).
thf(13332,plain,
n6 @ ( n4 @ lt ),
inference(pattern_uni,[status(thm)],[13331:[bind(A,$thf( n4 )),bind(B,$thf( n6 ))]]) ).
thf(58,axiom,
! [A: $i] :
( tptp_float_0_0
= ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_plus_base_float) ).
thf(459,plain,
! [A: $i] :
( tptp_float_0_0
= ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(460,plain,
! [A: $i] :
( tptp_float_0_0
= ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) ) ),
inference(cnf,[status(esa)],[459]) ).
thf(461,plain,
! [A: $i] :
( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
= tptp_float_0_0 ),
inference(lifteq,[status(thm)],[460]) ).
thf(229,plain,
! [A: $i] :
( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
= n0 ),
inference(cnf,[status(esa)],[228]) ).
thf(230,plain,
! [A: $i] :
( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
= n0 ),
inference(lifteq,[status(thm)],[229]) ).
thf(4622,plain,
tptp_float_0_0 = n0,
inference(rewrite,[status(thm)],[461,230]) ).
thf(1344,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n6 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[209,187]) ).
thf(1345,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n6 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1344]) ).
thf(1346,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n6 != A ) ),
inference(simp,[status(thm)],[1345]) ).
thf(1347,plain,
tptp_minus_1 != n6,
inference(simp,[status(thm)],[1346]) ).
thf(138,plain,
( ( sk9 @ ( n0 @ leq ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(2557,plain,
( ( sk9 @ ( n0 @ leq ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[138,128,105]) ).
thf(2558,plain,
( ( sk9 @ ( n0 @ leq ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(simp,[status(thm)],[2557]) ).
thf(7257,plain,
( ( sk9 @ ( n0 @ leq ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| $false ),
inference(rewrite,[status(thm)],[2558,7091]) ).
thf(7258,plain,
( ( sk9 @ ( n0 @ leq ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4 ),
inference(simp,[status(thm)],[7257]) ).
thf(77,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ succ @ leq ) )
=> ( A @ ( B @ gt ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_succ_gt) ).
thf(591,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ succ @ leq ) )
=> ( A @ ( B @ gt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(13,axiom,
n2 @ ( n5 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_2) ).
thf(188,plain,
n2 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(13288,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[188,194]) ).
thf(13289,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13288]) ).
thf(13290,plain,
n5 @ ( n2 @ lt ),
inference(pattern_uni,[status(thm)],[13289:[bind(A,$thf( n2 )),bind(B,$thf( n5 ))]]) ).
thf(213,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 @ sk11 ) ) ) @ leq ) ) ),
inference(cnfConj,[status(thm)],[211]) ).
thf(216,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( B @ ( A @ ( B @ ( C @ ( D @ sk11 ) ) ) @ leq ) )
| ( ( A @ ( D @ ( B @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D ) ),
inference(lifteq,[status(thm)],[213]) ).
thf(83,axiom,
n2 @ ( n999 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_999_2) ).
thf(603,plain,
n2 @ ( n999 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(13354,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n999 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[603,194]) ).
thf(13355,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n999 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13354]) ).
thf(13356,plain,
n999 @ ( n2 @ lt ),
inference(pattern_uni,[status(thm)],[13355:[bind(A,$thf( n2 )),bind(B,$thf( n999 ))]]) ).
thf(82,axiom,
n0 @ ( n4 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_0) ).
thf(602,plain,
n0 @ ( n4 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(13303,plain,
! [B: $i,A: $i] :
( ( ( n5 @ ( n6 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[633,194]) ).
thf(13304,plain,
! [B: $i,A: $i] :
( ( ( n5 @ ( n6 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13303]) ).
thf(13305,plain,
n6 @ ( n5 @ lt ),
inference(pattern_uni,[status(thm)],[13304:[bind(A,$thf( n5 )),bind(B,$thf( n6 ))]]) ).
thf(100,axiom,
! [A: $i,B: $i] :
( ( A @ ( n0 @ leq ) )
=> ( A @ ( B @ uniform_int_rnd ) @ ( n0 @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',uniform_int_rand_ranges_lo) ).
thf(634,plain,
! [A: $i,B: $i] :
( ( A @ ( n0 @ leq ) )
=> ( A @ ( B @ uniform_int_rnd ) @ ( n0 @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[100]) ).
thf(28,axiom,
n4 @ ( n999 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_999_4) ).
thf(221,plain,
n4 @ ( n999 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(47,axiom,
! [A: $i] :
( ( A @ ( n2 @ plus ) )
= ( A @ succ @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_2_l) ).
thf(291,plain,
! [A: $i] :
( ( A @ ( n2 @ plus ) )
= ( A @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(292,plain,
! [A: $i] :
( ( A @ ( n2 @ plus ) )
= ( A @ succ @ succ ) ),
inference(cnf,[status(esa)],[291]) ).
thf(293,plain,
! [A: $i] :
( ( A @ ( n2 @ plus ) )
= ( A @ succ @ succ ) ),
inference(lifteq,[status(thm)],[292]) ).
thf(3154,plain,
! [A: $i] :
( ( ( n3 @ ( n999 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[637,187]) ).
thf(3155,plain,
! [A: $i] :
( ( n3 @ ( n999 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[3154]) ).
thf(3156,plain,
! [A: $i] :
( ( n3 != A )
| ( n999 != A ) ),
inference(simp,[status(thm)],[3155]) ).
thf(3157,plain,
n3 != n999,
inference(simp,[status(thm)],[3156]) ).
thf(38,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/sandbox/benchmark/theBenchmark.p',matrix_symm_update_diagonal) ).
thf(248,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)],[38]) ).
thf(122,plain,
( ( sk10 @ ( n0 @ leq ) )
| ( ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(162,plain,
( ( sk10 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) )
| ( ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[122]) ).
thf(10597,plain,
( ( sk10 @ ( n0 @ leq ) )
| sk4
| $false
| ~ ( n999 @ pred @ ( pv5 @ leq ) )
| ~ $true
| ( ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ),
inference(rewrite,[status(thm)],[162,128,7091,287]) ).
thf(10598,plain,
( ( sk10 @ ( n0 @ leq ) )
| sk4
| ~ ( n999 @ pred @ ( pv5 @ leq ) )
| ( ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[10597]) ).
thf(118,plain,
( ~ sk4
| ( n1 @ ( n3 @ minus ) @ ( sk5 @ leq ) )
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(1424,plain,
( ~ sk4
| ( n1 @ ( n3 @ minus ) @ ( sk5 @ leq ) )
| sk1
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[118,128,105]) ).
thf(1425,plain,
( ~ sk4
| ( n1 @ ( n3 @ minus ) @ ( sk5 @ leq ) )
| sk1 ),
inference(simp,[status(thm)],[1424]) ).
thf(7219,plain,
( ~ sk4
| ( n1 @ ( n3 @ minus ) @ ( sk5 @ leq ) )
| $false ),
inference(rewrite,[status(thm)],[1425,7091]) ).
thf(7220,plain,
( ~ sk4
| ( n1 @ ( n3 @ minus ) @ ( sk5 @ leq ) ) ),
inference(simp,[status(thm)],[7219]) ).
thf(9164,plain,
( ~ sk4
| ( n3 @ pred @ ( sk5 @ leq ) ) ),
inference(rewrite,[status(thm)],[7220,287]) ).
thf(5,axiom,
! [A: $i,B: $i] :
( ( A = B )
| ( A @ ( B @ gt ) )
| ( B @ ( A @ gt ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',totality) ).
thf(167,plain,
! [A: $i,B: $i] :
( ( A = B )
| ( A @ ( B @ gt ) )
| ( B @ ( A @ gt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(168,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( A @ ( B @ gt ) )
| ( B @ ( A @ gt ) ) ),
inference(cnf,[status(esa)],[167]) ).
thf(169,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ gt ) )
| ( B @ ( A @ gt ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[168]) ).
thf(11308,plain,
! [B: $i,A: $i] :
( ( A != sk6 )
| ~ sk4
| ( B != sk5 )
| ( A @ ( B @ gt ) )
| ( B @ ( A @ gt ) ) ),
inference(paramod_ordered,[status(thm)],[169,7272]) ).
thf(11309,plain,
! [A: $i] :
( ~ sk4
| ( A != sk5 )
| ( sk6 @ ( A @ gt ) )
| ( A @ ( sk6 @ gt ) ) ),
inference(pattern_uni,[status(thm)],[11308:[bind(A,$thf( sk6 ))]]) ).
thf(12705,plain,
( ~ sk4
| ( sk6 @ ( sk5 @ gt ) )
| ( sk5 @ ( sk6 @ gt ) ) ),
inference(simp,[status(thm)],[11309]) ).
thf(27,axiom,
! [A: $i] :
( ( ( n6 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n6 )
| ( A = n5 )
| ( A = n4 )
| ( A = n3 )
| ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_6) ).
thf(218,plain,
! [A: $i] :
( ( ( n6 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n6 )
| ( A = n5 )
| ( A = n4 )
| ( A = n3 )
| ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(219,plain,
! [A: $i] :
( ( A = n6 )
| ( A = n5 )
| ( A = n4 )
| ( A = n3 )
| ( A = n2 )
| ( A = n1 )
| ( A = n0 )
| ~ ( n6 @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(cnf,[status(esa)],[218]) ).
thf(220,plain,
! [A: $i] :
( ~ ( n6 @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( A = n6 )
| ( A = n5 )
| ( A = n4 )
| ( A = n3 )
| ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ),
inference(lifteq,[status(thm)],[219]) ).
thf(13258,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n0 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[284,194]) ).
thf(13259,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n0 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13258]) ).
thf(13260,plain,
n0 @ ( tptp_minus_1 @ lt ),
inference(pattern_uni,[status(thm)],[13259:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n0 ))]]) ).
thf(30,axiom,
tptp_minus_1 @ ( n999 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_999_tptp_minus_1) ).
thf(223,plain,
tptp_minus_1 @ ( n999 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(13333,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n999 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[223,194]) ).
thf(13334,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n999 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13333]) ).
thf(13335,plain,
n999 @ ( tptp_minus_1 @ lt ),
inference(pattern_uni,[status(thm)],[13334:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n999 ))]]) ).
thf(598,plain,
! [A: $i] : ( A @ ( A @ leq ) ),
inference(cnf,[status(esa)],[597]) ).
thf(52,axiom,
n3 @ ( n6 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_3) ).
thf(392,plain,
n3 @ ( n6 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(3,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ ( B @ ( A @ tptp_update2 ) ) @ a_select2 ) )
= C ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sel2_update_1) ).
thf(163,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ ( B @ ( A @ tptp_update2 ) ) @ a_select2 ) )
= C ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(164,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( B @ ( A @ tptp_update2 ) ) @ a_select2 ) )
= C ),
inference(cnf,[status(esa)],[163]) ).
thf(165,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( B @ ( A @ tptp_update2 ) ) @ a_select2 ) )
= C ),
inference(lifteq,[status(thm)],[164]) ).
thf(4714,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ succ @ gt ) )
!= ( B @ ( B @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[176,187]) ).
thf(4715,plain,
! [B: $i,A: $i] :
( ( A @ ( A @ succ @ gt ) )
!= ( B @ ( B @ gt ) ) ),
inference(simp,[status(thm)],[4714]) ).
thf(4726,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ succ )
!= B ) ),
inference(simp,[status(thm)],[4715]) ).
thf(4727,plain,
! [A: $i] :
( ( A @ succ )
!= A ),
inference(simp,[status(thm)],[4726]) ).
thf(10888,plain,
! [A: $i] :
( ( ( n3 @ succ @ succ @ succ @ succ )
!= ( A @ succ ) )
| ( ( n6 @ succ )
!= A ) ),
inference(paramod_ordered,[status(thm)],[10799,4727]) ).
thf(10889,plain,
( ( n3 @ succ @ succ @ succ )
!= ( n6 @ succ ) ),
inference(pattern_uni,[status(thm)],[10888:[bind(A,$thf( n3 @ succ @ succ @ succ ))]]) ).
thf(8344,plain,
! [B: $i,A: $i] :
( ( ( n4 @ ( A @ plus ) )
!= ( B @ ( n2 @ plus ) ) )
| ( ( A @ succ @ succ @ succ @ succ )
= ( B @ succ @ succ ) ) ),
inference(paramod_ordered,[status(thm)],[468,293]) ).
thf(8345,plain,
( ( n2 @ succ @ succ @ succ @ succ )
= ( n4 @ succ @ succ ) ),
inference(pattern_uni,[status(thm)],[8344:[bind(A,$thf( n2 )),bind(B,$thf( n4 ))]]) ).
thf(8581,plain,
( ( n3 @ succ @ succ @ succ )
= ( n5 @ succ ) ),
inference(rewrite,[status(thm)],[8345,3715,3305]) ).
thf(11191,plain,
( ( n5 @ succ )
!= ( n6 @ succ ) ),
inference(rewrite,[status(thm)],[10889,8581]) ).
thf(192,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ gt ) )
| ~ ( B @ ( A @ lt ) ) ),
inference(cnfConj,[status(thm)],[191]) ).
thf(14522,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk6 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ~ sk4
| ( sk6 @ ( sk5 @ gt ) ) ),
inference(paramod_ordered,[status(thm)],[12705,202]) ).
thf(14523,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk6 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ leq ) )
| ~ sk4
| ( sk6 @ ( sk5 @ gt ) ) ),
inference(simp,[status(thm)],[14522]) ).
thf(14524,plain,
( ( sk6 @ ( sk5 @ leq ) )
| ~ sk4
| ( sk6 @ ( sk5 @ gt ) ) ),
inference(pattern_uni,[status(thm)],[14523:[bind(A,$thf( sk5 )),bind(B,$thf( sk6 ))]]) ).
thf(13252,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n6 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[614,194]) ).
thf(13253,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n6 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13252]) ).
thf(13254,plain,
n6 @ ( n0 @ lt ),
inference(pattern_uni,[status(thm)],[13253:[bind(A,$thf( n0 )),bind(B,$thf( n6 ))]]) ).
thf(197,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ gt ) )
| ~ ( C @ ( B @ gt ) )
| ~ ( B @ ( A @ gt ) ) ),
inference(cnf,[status(esa)],[196]) ).
thf(94,axiom,
n0 @ ( n1 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_1_0) ).
thf(625,plain,
n0 @ ( n1 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(15,axiom,
tptp_minus_1 @ ( n4 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_tptp_minus_1) ).
thf(195,plain,
tptp_minus_1 @ ( n4 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(662,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[195,187]) ).
thf(663,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[662]) ).
thf(664,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n4 != A ) ),
inference(simp,[status(thm)],[663]) ).
thf(665,plain,
n4 != tptp_minus_1,
inference(simp,[status(thm)],[664]) ).
thf(13357,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[195,194]) ).
thf(13358,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13357]) ).
thf(13359,plain,
n4 @ ( tptp_minus_1 @ lt ),
inference(pattern_uni,[status(thm)],[13358:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n4 ))]]) ).
thf(2178,plain,
! [A: $i] :
( ( ( n3 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[265,187]) ).
thf(2179,plain,
! [A: $i] :
( ( n3 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2178]) ).
thf(2180,plain,
! [A: $i] :
( ( n3 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[2179]) ).
thf(2181,plain,
n5 != n3,
inference(simp,[status(thm)],[2180]) ).
thf(57,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( C @ ( B @ ( D @ ( C @ ( B @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
= D ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sel3_update_1) ).
thf(456,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)],[57]) ).
thf(13267,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[602,194]) ).
thf(13268,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13267]) ).
thf(13269,plain,
n4 @ ( n0 @ lt ),
inference(pattern_uni,[status(thm)],[13268:[bind(A,$thf( n0 )),bind(B,$thf( n4 ))]]) ).
thf(3695,plain,
( ( ( n1 @ succ )
!= ( n1 @ succ ) )
| ( ( n2 @ succ @ succ @ succ )
= n5 ) ),
inference(paramod_ordered,[status(thm)],[3158,3671]) ).
thf(3696,plain,
( ( n2 @ succ @ succ @ succ )
= n5 ),
inference(pattern_uni,[status(thm)],[3695:[]]) ).
thf(3799,plain,
( ( n3 @ succ @ succ )
= n5 ),
inference(rewrite,[status(thm)],[3696,3305]) ).
thf(18,axiom,
n2 @ ( n3 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_2) ).
thf(199,plain,
n2 @ ( n3 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(13345,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[199,194]) ).
thf(13346,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13345]) ).
thf(13347,plain,
n3 @ ( n2 @ lt ),
inference(pattern_uni,[status(thm)],[13346:[bind(A,$thf( n2 )),bind(B,$thf( n3 ))]]) ).
thf(90,axiom,
! [A: $i] :
( ( ( n4 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n4 )
| ( A = n3 )
| ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_4) ).
thf(615,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)],[90]) ).
thf(111,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( id_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( id_ds1_filter @ a_select3 ) ) ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( n1 @ ( n1 @ ( n6 @ minus ) @ ( n1 @ plus ) @ minus ) @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(160,plain,
! [B: $i,A: $i] :
( ~ ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( n1 @ ( n1 @ ( n6 @ minus ) @ ( n1 @ plus ) @ minus ) @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( B @ ( A @ ( id_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( id_ds1_filter @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[111]) ).
thf(161,plain,
! [B: $i,A: $i] :
( ~ ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( n1 @ ( n1 @ ( n6 @ minus ) @ ( n1 @ plus ) @ minus ) @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( B @ ( A @ ( id_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( id_ds1_filter @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[160]) ).
thf(9889,plain,
! [B: $i,A: $i] :
( ~ ( n6 @ pred @ ( B @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( n1 @ plus ) @ pred @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( B @ ( A @ ( id_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( id_ds1_filter @ a_select3 ) ) ) ) ),
inference(rewrite,[status(thm)],[161,287]) ).
thf(2691,plain,
! [A: $i] :
( ( ( n2 @ ( n999 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[603,187]) ).
thf(2692,plain,
! [A: $i] :
( ( n2 @ ( n999 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2691]) ).
thf(2693,plain,
! [A: $i] :
( ( n2 != A )
| ( n999 != A ) ),
inference(simp,[status(thm)],[2692]) ).
thf(2694,plain,
n2 != n999,
inference(simp,[status(thm)],[2693]) ).
thf(50,axiom,
! [A: $i,B: $i] :
( ( ( A != B )
& ( B @ ( A @ leq ) ) )
=> ( A @ ( B @ gt ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_gt2) ).
thf(388,plain,
! [A: $i,B: $i] :
( ( ( A != B )
& ( B @ ( A @ leq ) ) )
=> ( A @ ( B @ gt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(78,axiom,
! [A: $i] :
( ( A @ ( n4 @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_4_l) ).
thf(593,plain,
! [A: $i] :
( ( A @ ( n4 @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(7203,plain,
( ~ sk4
| $false
| ( ( sk5 @ ( sk6 @ ( r_ds1_filter @ a_select3 ) ) )
!= ( sk6 @ ( sk5 @ ( r_ds1_filter @ a_select3 ) ) ) ) ),
inference(rewrite,[status(thm)],[5401,7091]) ).
thf(7204,plain,
( ~ sk4
| ( ( sk5 @ ( sk6 @ ( r_ds1_filter @ a_select3 ) ) )
!= ( sk6 @ ( sk5 @ ( r_ds1_filter @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[7203]) ).
thf(8,axiom,
n4 @ ( n5 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_4) ).
thf(177,plain,
n4 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(13342,plain,
! [B: $i,A: $i] :
( ( ( n4 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[177,194]) ).
thf(13343,plain,
! [B: $i,A: $i] :
( ( ( n4 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13342]) ).
thf(13344,plain,
n5 @ ( n4 @ lt ),
inference(pattern_uni,[status(thm)],[13343:[bind(A,$thf( n4 )),bind(B,$thf( n5 ))]]) ).
thf(249,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)],[248]) ).
thf(250,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 @ sk15 ) @ ( A @ ( B @ sk14 ) @ ( A @ a_select3 ) ) )
!= ( A @ ( B @ sk14 ) @ ( A @ ( B @ sk15 ) @ ( 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 @ sk15 ) @ 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 @ sk15 ) @ ( 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 @ sk14 ) @ 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 @ sk14 ) @ ( n0 @ leq ) ) ) ),
inference(cnf,[status(esa)],[249]) ).
thf(253,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 @ sk15 ) @ ( A @ ( B @ sk14 ) @ ( A @ a_select3 ) ) )
!= ( A @ ( B @ sk14 ) @ ( A @ ( B @ sk15 ) @ ( A @ a_select3 ) ) ) ) ),
inference(cnfConj,[status(thm)],[250]) ).
thf(256,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 @ sk14 ) @ ( A @ ( B @ sk15 ) @ ( A @ a_select3 ) ) )
!= ( A @ ( B @ sk15 ) @ ( A @ ( B @ sk14 ) @ ( A @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[253]) ).
thf(32,axiom,
n6 @ ( n999 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_999_6) ).
thf(225,plain,
n6 @ ( n999 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(91,axiom,
tptp_minus_1 @ ( n3 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_tptp_minus_1) ).
thf(618,plain,
tptp_minus_1 @ ( n3 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(13306,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[618,194]) ).
thf(13307,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13306]) ).
thf(13308,plain,
n3 @ ( tptp_minus_1 @ lt ),
inference(pattern_uni,[status(thm)],[13307:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n3 ))]]) ).
thf(676,plain,
! [A: $i] :
( ( ( n2 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[199,187]) ).
thf(677,plain,
! [A: $i] :
( ( n2 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[676]) ).
thf(678,plain,
! [A: $i] :
( ( n2 != A )
| ( n3 != A ) ),
inference(simp,[status(thm)],[677]) ).
thf(679,plain,
n2 != n3,
inference(simp,[status(thm)],[678]) ).
thf(93,axiom,
! [A: $i] :
( ( n3 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_3_r) ).
thf(622,plain,
! [A: $i] :
( ( n3 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(4,axiom,
tptp_minus_1 @ ( n2 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_2_tptp_minus_1) ).
thf(166,plain,
tptp_minus_1 @ ( n2 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(638,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[166,187]) ).
thf(639,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[638]) ).
thf(644,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n2 != A ) ),
inference(simp,[status(thm)],[639]) ).
thf(647,plain,
tptp_minus_1 != n2,
inference(simp,[status(thm)],[644]) ).
thf(11199,plain,
( ( ( n3 @ succ @ succ @ succ @ succ )
!= ( n5 @ succ ) )
| ( ( n6 @ succ )
!= ( n6 @ succ ) ) ),
inference(paramod_ordered,[status(thm)],[10799,11191]) ).
thf(11200,plain,
( ( n3 @ succ @ succ @ succ @ succ )
!= ( n5 @ succ ) ),
inference(simp,[status(thm)],[11199]) ).
thf(11221,plain,
( ( n3 @ succ @ succ @ succ )
!= n5 ),
inference(simp,[status(thm)],[11200]) ).
thf(13169,plain,
( ( n5 @ succ )
!= n5 ),
inference(rewrite,[status(thm)],[11221,8581]) ).
thf(107,plain,
( ( ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) ) )
| ( n1 @ ( n6 @ minus ) @ ( sk7 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(156,plain,
( ( n1 @ ( n6 @ minus ) @ ( sk7 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) )
| ( ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[107]) ).
thf(8438,plain,
( ( n6 @ pred @ ( sk7 @ leq ) )
| sk4
| $false
| ~ ( n999 @ pred @ ( pv5 @ leq ) )
| ~ $true
| ( ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) ) ) ),
inference(rewrite,[status(thm)],[156,128,7091,287]) ).
thf(8439,plain,
( ( n6 @ pred @ ( sk7 @ leq ) )
| sk4
| ~ ( n999 @ pred @ ( pv5 @ leq ) )
| ( ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[8438]) ).
thf(5216,plain,
! [A: $i] :
( ( ( n5 @ succ )
!= ( A @ succ ) )
| ( ( n6 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[3972,181]) ).
thf(5217,plain,
( ( n6 @ pred )
= n5 ),
inference(pattern_uni,[status(thm)],[5216:[bind(A,$thf( n5 ))]]) ).
thf(42,axiom,
! [A: $i,B: $i] :
( ( B @ succ @ ( A @ succ @ leq ) )
<=> ( B @ ( A @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_succ_succ) ).
thf(266,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)],[42]) ).
thf(17,axiom,
tptp_minus_1 @ ( n5 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_tptp_minus_1) ).
thf(198,plain,
tptp_minus_1 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(13324,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[198,194]) ).
thf(13325,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13324]) ).
thf(13326,plain,
n5 @ ( tptp_minus_1 @ lt ),
inference(pattern_uni,[status(thm)],[13325:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n5 ))]]) ).
thf(108,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( pminus_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( pminus_ds1_filter @ a_select3 ) ) ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(151,plain,
! [B: $i,A: $i] :
( ~ ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( B @ ( A @ ( pminus_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[108]) ).
thf(152,plain,
! [B: $i,A: $i] :
( ~ ( n1 @ ( n6 @ minus ) @ ( B @ leq ) )
| ~ ( n1 @ ( n6 @ minus ) @ ( A @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( B @ ( A @ ( pminus_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[151]) ).
thf(7646,plain,
! [B: $i,A: $i] :
( ~ ( n6 @ pred @ ( B @ leq ) )
| ~ ( n6 @ pred @ ( A @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( B @ ( A @ ( pminus_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ),
inference(rewrite,[status(thm)],[152,287]) ).
thf(55,axiom,
! [A: $i,B: $i] :
( ( B @ pred @ ( A @ leq ) )
<=> ( A @ ( B @ gt ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_gt_pred) ).
thf(398,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)],[55]) ).
thf(1032,plain,
! [A: $i] :
( ( ( n1 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[204,187]) ).
thf(1033,plain,
! [A: $i] :
( ( n1 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1032]) ).
thf(1034,plain,
! [A: $i] :
( ( n1 != A )
| ( n3 != A ) ),
inference(simp,[status(thm)],[1033]) ).
thf(1035,plain,
n3 != n1,
inference(simp,[status(thm)],[1034]) ).
thf(2272,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n0 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[284,187]) ).
thf(2273,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n0 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2272]) ).
thf(2274,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[2273]) ).
thf(2275,plain,
tptp_minus_1 != n0,
inference(simp,[status(thm)],[2274]) ).
thf(40,axiom,
! [A: $i] :
( ( A @ ( n3 @ plus ) )
= ( A @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_3_l) ).
thf(262,plain,
! [A: $i] :
( ( A @ ( n3 @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(263,plain,
! [A: $i] :
( ( A @ ( n3 @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(cnf,[status(esa)],[262]) ).
thf(264,plain,
! [A: $i] :
( ( A @ ( n3 @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(lifteq,[status(thm)],[263]) ).
thf(73,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ ( A @ minus ) @ leq ) )
=> ( B @ ( n0 @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_minus) ).
thf(573,plain,
! [A: $i,B: $i] :
( ( A @ ( B @ ( A @ minus ) @ leq ) )
=> ( B @ ( n0 @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(126,plain,
( ( n1 @ ( n6 @ minus ) @ ( sk10 @ leq ) )
| ( ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(157,plain,
( ( n1 @ ( n6 @ minus ) @ ( sk10 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) )
| ( ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[126]) ).
thf(8858,plain,
( ( n6 @ pred @ ( sk10 @ leq ) )
| sk4
| $false
| ~ ( n999 @ pred @ ( pv5 @ leq ) )
| ~ $true
| ( ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ),
inference(rewrite,[status(thm)],[157,128,7091,287]) ).
thf(8859,plain,
( ( n6 @ pred @ ( sk10 @ leq ) )
| sk4
| ~ ( n999 @ pred @ ( pv5 @ leq ) )
| ( ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[8858]) ).
thf(81,axiom,
! [A: $i] :
( ( A @ ( n1 @ plus ) )
= ( A @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_1_l) ).
thf(599,plain,
! [A: $i] :
( ( A @ ( n1 @ plus ) )
= ( A @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(600,plain,
! [A: $i] :
( ( A @ ( n1 @ plus ) )
= ( A @ succ ) ),
inference(cnf,[status(esa)],[599]) ).
thf(601,plain,
! [A: $i] :
( ( A @ ( n1 @ plus ) )
= ( A @ succ ) ),
inference(lifteq,[status(thm)],[600]) ).
thf(13336,plain,
! [B: $i,A: $i] :
( ( ( n3 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[226,194]) ).
thf(13337,plain,
! [B: $i,A: $i] :
( ( ( n3 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13336]) ).
thf(13338,plain,
n4 @ ( n3 @ lt ),
inference(pattern_uni,[status(thm)],[13337:[bind(A,$thf( n3 )),bind(B,$thf( n4 ))]]) ).
thf(13366,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n2 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[596,194]) ).
thf(13367,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n2 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13366]) ).
thf(13368,plain,
n2 @ ( n0 @ lt ),
inference(pattern_uni,[status(thm)],[13367:[bind(A,$thf( n0 )),bind(B,$thf( n2 ))]]) ).
thf(59,axiom,
n0 @ ( n3 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_0) ).
thf(462,plain,
n0 @ ( n3 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(2486,plain,
! [A: $i] :
( ( ( n0 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[462,187]) ).
thf(2487,plain,
! [A: $i] :
( ( n0 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2486]) ).
thf(2488,plain,
! [A: $i] :
( ( n0 != A )
| ( n3 != A ) ),
inference(simp,[status(thm)],[2487]) ).
thf(2489,plain,
n3 != n0,
inference(simp,[status(thm)],[2488]) ).
thf(7179,plain,
( ( sk10 @ ( n0 @ leq ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| $false ),
inference(rewrite,[status(thm)],[4546,7091]) ).
thf(7180,plain,
( ( sk10 @ ( n0 @ leq ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4 ),
inference(simp,[status(thm)],[7179]) ).
thf(98,axiom,
n1 @ ( n4 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_1) ).
thf(632,plain,
n1 @ ( n4 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[98]) ).
thf(2956,plain,
! [A: $i] :
( ( ( n1 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[632,187]) ).
thf(2957,plain,
! [A: $i] :
( ( n1 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2956]) ).
thf(2958,plain,
! [A: $i] :
( ( n1 != A )
| ( n4 != A ) ),
inference(simp,[status(thm)],[2957]) ).
thf(2959,plain,
n4 != n1,
inference(simp,[status(thm)],[2958]) ).
thf(76,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/sandbox/benchmark/theBenchmark.p',matrix_symm_inv) ).
thf(579,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)],[76]) ).
thf(51,axiom,
n0 @ ( n5 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_0) ).
thf(391,plain,
n0 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(49,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ geq ) )
<=> ( A @ ( B @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_geq) ).
thf(382,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)],[49]) ).
thf(140,plain,
( ( sk9 @ ( n0 @ leq ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(3600,plain,
( ( sk9 @ ( n0 @ leq ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[140,128,105]) ).
thf(3601,plain,
( ( sk9 @ ( n0 @ leq ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(simp,[status(thm)],[3600]) ).
thf(7269,plain,
( ( sk9 @ ( n0 @ leq ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| $false ),
inference(rewrite,[status(thm)],[3601,7091]) ).
thf(7270,plain,
( ( sk9 @ ( n0 @ leq ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4 ),
inference(simp,[status(thm)],[7269]) ).
thf(136,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( r_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( r_ds1_filter @ a_select3 ) ) ) )
| ~ ( n1 @ ( n3 @ minus ) @ ( B @ leq ) )
| ~ ( n1 @ ( n3 @ minus ) @ ( A @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(158,plain,
! [B: $i,A: $i] :
( ~ ( n1 @ ( n3 @ minus ) @ ( B @ leq ) )
| ~ ( n1 @ ( n3 @ minus ) @ ( A @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( B @ ( A @ ( r_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( r_ds1_filter @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[136]) ).
thf(159,plain,
! [B: $i,A: $i] :
( ~ ( n1 @ ( n3 @ minus ) @ ( B @ leq ) )
| ~ ( n1 @ ( n3 @ minus ) @ ( A @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( B @ ( A @ ( r_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( r_ds1_filter @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[158]) ).
thf(9243,plain,
! [B: $i,A: $i] :
( ~ ( n3 @ pred @ ( B @ leq ) )
| ~ ( n3 @ pred @ ( A @ leq ) )
| ~ ( B @ ( n0 @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( B @ ( A @ ( r_ds1_filter @ a_select3 ) ) )
= ( A @ ( B @ ( r_ds1_filter @ a_select3 ) ) ) ) ),
inference(rewrite,[status(thm)],[159,287]) ).
thf(7514,plain,
n999 @ pred @ ( pv5 @ leq ),
inference(rewrite,[status(thm)],[105,287]) ).
thf(2490,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n1 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[575,187]) ).
thf(2491,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n1 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2490]) ).
thf(2492,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n1 != A ) ),
inference(simp,[status(thm)],[2491]) ).
thf(2493,plain,
tptp_minus_1 != n1,
inference(simp,[status(thm)],[2492]) ).
thf(7314,plain,
! [B: $i,A: $i] :
( ( ( A @ pred @ succ )
!= ( B @ succ ) )
| ( B @ ( A @ gt ) ) ),
inference(paramod_ordered,[status(thm)],[184,176]) ).
thf(7315,plain,
! [A: $i] : ( A @ pred @ ( A @ gt ) ),
inference(pattern_uni,[status(thm)],[7314:[bind(A,$thf( C )),bind(B,$thf( C @ pred ))]]) ).
thf(7379,plain,
! [A: $i] : ( A @ pred @ ( A @ gt ) ),
inference(simp,[status(thm)],[7315]) ).
thf(2952,plain,
! [A: $i] :
( ( ( n4 @ ( n6 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[626,187]) ).
thf(2953,plain,
! [A: $i] :
( ( n4 @ ( n6 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2952]) ).
thf(2954,plain,
! [A: $i] :
( ( n4 != A )
| ( n6 != A ) ),
inference(simp,[status(thm)],[2953]) ).
thf(2955,plain,
n4 != n6,
inference(simp,[status(thm)],[2954]) ).
thf(9,axiom,
n2 @ ( n4 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_2) ).
thf(178,plain,
n2 @ ( n4 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(642,plain,
! [A: $i] :
( ( ( n2 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[178,187]) ).
thf(643,plain,
! [A: $i] :
( ( n2 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[642]) ).
thf(646,plain,
! [A: $i] :
( ( n2 != A )
| ( n4 != A ) ),
inference(simp,[status(thm)],[643]) ).
thf(649,plain,
n4 != n2,
inference(simp,[status(thm)],[646]) ).
thf(1687,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n999 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[223,187]) ).
thf(1688,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n999 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1687]) ).
thf(1689,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n999 != A ) ),
inference(simp,[status(thm)],[1688]) ).
thf(1690,plain,
tptp_minus_1 != n999,
inference(simp,[status(thm)],[1689]) ).
thf(2868,plain,
! [A: $i] :
( ( ( n0 @ ( n6 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[614,187]) ).
thf(2869,plain,
! [A: $i] :
( ( n0 @ ( n6 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2868]) ).
thf(2870,plain,
! [A: $i] :
( ( n0 != A )
| ( n6 != A ) ),
inference(simp,[status(thm)],[2869]) ).
thf(2871,plain,
n6 != n0,
inference(simp,[status(thm)],[2870]) ).
thf(64,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/sandbox/benchmark/theBenchmark.p',const_array1_select) ).
thf(477,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)],[64]) ).
thf(29,axiom,
n1 @ ( n6 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_1) ).
thf(222,plain,
n1 @ ( n6 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(1554,plain,
! [A: $i] :
( ( ( n1 @ ( n6 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[222,187]) ).
thf(1555,plain,
! [A: $i] :
( ( n1 @ ( n6 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1554]) ).
thf(1556,plain,
! [A: $i] :
( ( n1 != A )
| ( n6 != A ) ),
inference(simp,[status(thm)],[1555]) ).
thf(1557,plain,
n6 != n1,
inference(simp,[status(thm)],[1556]) ).
thf(87,axiom,
! [A: $i] :
( ( ( n3 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n3 )
| ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_3) ).
thf(609,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)],[87]) ).
thf(13270,plain,
! [B: $i,A: $i] :
( ( ( n4 @ ( n999 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[221,194]) ).
thf(13271,plain,
! [B: $i,A: $i] :
( ( ( n4 @ ( n999 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13270]) ).
thf(13272,plain,
n999 @ ( n4 @ lt ),
inference(pattern_uni,[status(thm)],[13271:[bind(A,$thf( n4 )),bind(B,$thf( n999 ))]]) ).
thf(137,plain,
( ( ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) ) )
| ( ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(145,plain,
( sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) )
| ( ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) ) )
| ( ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[137]) ).
thf(5049,plain,
( sk4
| sk1
| ~ $true
| ~ $true
| ( ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) ) )
| ( ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ),
inference(rewrite,[status(thm)],[145,128,105]) ).
thf(5050,plain,
( sk4
| sk1
| ( ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) ) )
| ( ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[5049]) ).
thf(5053,plain,
( ( sk10 != sk9 )
| ( sk10 != sk9 )
| ( id_ds1_filter != id_ds1_filter )
| ( sk8 != sk7 )
| ( sk8 != sk7 )
| ( pminus_ds1_filter != pminus_ds1_filter )
| sk4
| sk1 ),
inference(simp,[status(thm)],[5050]) ).
thf(5150,plain,
( ( sk10 != sk9 )
| ( sk8 != sk7 )
| sk4
| sk1 ),
inference(simp,[status(thm)],[5053]) ).
thf(7185,plain,
( ( sk10 != sk9 )
| ( sk8 != sk7 )
| sk4
| $false ),
inference(rewrite,[status(thm)],[5150,7091]) ).
thf(7186,plain,
( ( sk10 != sk9 )
| ( sk8 != sk7 )
| sk4 ),
inference(simp,[status(thm)],[7185]) ).
thf(109,plain,
( ~ sk4
| ( sk6 @ ( n0 @ leq ) )
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(674,plain,
( ~ sk4
| ( sk6 @ ( n0 @ leq ) )
| sk1
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[109,128,105]) ).
thf(675,plain,
( ~ sk4
| ( sk6 @ ( n0 @ leq ) )
| sk1 ),
inference(simp,[status(thm)],[674]) ).
thf(7249,plain,
( ~ sk4
| ( sk6 @ ( n0 @ leq ) )
| $false ),
inference(rewrite,[status(thm)],[675,7091]) ).
thf(7250,plain,
( ~ sk4
| ( sk6 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[7249]) ).
thf(130,plain,
( ( ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) ) )
| ( n1 @ ( n6 @ minus ) @ ( sk8 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(153,plain,
( ( n1 @ ( n6 @ minus ) @ ( sk8 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) )
| ( ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[130]) ).
thf(7868,plain,
( ( n6 @ pred @ ( sk8 @ leq ) )
| sk4
| $false
| ~ ( n999 @ pred @ ( pv5 @ leq ) )
| ~ $true
| ( ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) ) ) ),
inference(rewrite,[status(thm)],[153,128,7091,287]) ).
thf(7869,plain,
( ( n6 @ pred @ ( sk8 @ leq ) )
| sk4
| ~ ( n999 @ pred @ ( pv5 @ leq ) )
| ( ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[7868]) ).
thf(650,plain,
! [A: $i] :
( ( ( n2 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[188,187]) ).
thf(651,plain,
! [A: $i] :
( ( n2 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[650]) ).
thf(652,plain,
! [A: $i] :
( ( n2 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[651]) ).
thf(653,plain,
n5 != n2,
inference(simp,[status(thm)],[652]) ).
thf(2864,plain,
! [A: $i] :
( ( ( n5 @ ( n999 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[606,187]) ).
thf(2865,plain,
! [A: $i] :
( ( n5 @ ( n999 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2864]) ).
thf(2866,plain,
! [A: $i] :
( ( n5 != A )
| ( n999 != A ) ),
inference(simp,[status(thm)],[2865]) ).
thf(2867,plain,
n5 != n999,
inference(simp,[status(thm)],[2866]) ).
thf(13276,plain,
! [B: $i,A: $i] :
( ( ( n3 @ ( n6 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[392,194]) ).
thf(13277,plain,
! [B: $i,A: $i] :
( ( ( n3 @ ( n6 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13276]) ).
thf(13278,plain,
n6 @ ( n3 @ lt ),
inference(pattern_uni,[status(thm)],[13277:[bind(A,$thf( n3 )),bind(B,$thf( n6 ))]]) ).
thf(13369,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n2 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[200,194]) ).
thf(13370,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n2 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13369]) ).
thf(13371,plain,
n2 @ ( n1 @ lt ),
inference(pattern_uni,[status(thm)],[13370:[bind(A,$thf( n1 )),bind(B,$thf( n2 ))]]) ).
thf(68,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
<=> ( A @ ( B @ succ @ gt ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_succ_gt_equiv) ).
thf(548,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)],[68]) ).
thf(640,plain,
! [A: $i] :
( ( ( n4 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[177,187]) ).
thf(641,plain,
! [A: $i] :
( ( n4 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[640]) ).
thf(645,plain,
! [A: $i] :
( ( n4 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[641]) ).
thf(648,plain,
n4 != n5,
inference(simp,[status(thm)],[645]) ).
thf(123,plain,
( ( sk10 @ ( n0 @ leq ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(2214,plain,
( ( sk10 @ ( n0 @ leq ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[123,128,105]) ).
thf(2215,plain,
( ( sk10 @ ( n0 @ leq ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(simp,[status(thm)],[2214]) ).
thf(7263,plain,
( ( sk10 @ ( n0 @ leq ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| $false ),
inference(rewrite,[status(thm)],[2215,7091]) ).
thf(7264,plain,
( ( sk10 @ ( n0 @ leq ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4 ),
inference(simp,[status(thm)],[7263]) ).
thf(60,axiom,
! [A: $i] :
( ( ( n1 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n1 )
| ( A = n0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_1) ).
thf(463,plain,
! [A: $i] :
( ( ( n1 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n1 )
| ( A = n0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(13318,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[391,194]) ).
thf(13319,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13318]) ).
thf(13320,plain,
n5 @ ( n0 @ lt ),
inference(pattern_uni,[status(thm)],[13319:[bind(A,$thf( n0 )),bind(B,$thf( n5 ))]]) ).
thf(75,axiom,
! [A: $i] :
( ( ( n2 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_2) ).
thf(576,plain,
! [A: $i] :
( ( ( n2 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(670,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[198,187]) ).
thf(671,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[670]) ).
thf(672,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[671]) ).
thf(673,plain,
n5 != tptp_minus_1,
inference(simp,[status(thm)],[672]) ).
thf(13297,plain,
! [B: $i,A: $i] :
( ( ( n6 @ ( n999 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[225,194]) ).
thf(13298,plain,
! [B: $i,A: $i] :
( ( ( n6 @ ( n999 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13297]) ).
thf(13299,plain,
n999 @ ( n6 @ lt ),
inference(pattern_uni,[status(thm)],[13298:[bind(A,$thf( n6 )),bind(B,$thf( n999 ))]]) ).
thf(2276,plain,
! [A: $i] :
( ( ( n0 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[391,187]) ).
thf(2277,plain,
! [A: $i] :
( ( n0 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2276]) ).
thf(2278,plain,
! [A: $i] :
( ( n0 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[2277]) ).
thf(2279,plain,
n5 != n0,
inference(simp,[status(thm)],[2278]) ).
thf(112,plain,
( ( ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(154,plain,
( ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) )
| ( ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[112]) ).
thf(8042,plain,
( ( sk7 @ ( n0 @ leq ) )
| sk4
| $false
| ~ ( n999 @ pred @ ( pv5 @ leq ) )
| ~ $true
| ( ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) ) ) ),
inference(rewrite,[status(thm)],[154,128,7091,287]) ).
thf(8043,plain,
( ( sk7 @ ( n0 @ leq ) )
| sk4
| ~ ( n999 @ pred @ ( pv5 @ leq ) )
| ( ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[8042]) ).
thf(72,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
=> ( B @ succ @ ( A @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_succ) ).
thf(571,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
=> ( B @ succ @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(594,plain,
! [A: $i] :
( ( A @ ( n4 @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
inference(cnf,[status(esa)],[593]) ).
thf(595,plain,
! [A: $i] :
( ( A @ ( n4 @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
inference(lifteq,[status(thm)],[594]) ).
thf(88,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ leq ) )
& ( B @ ( A @ leq ) ) )
=> ( C @ ( A @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_leq) ).
thf(612,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ leq ) )
& ( B @ ( A @ leq ) ) )
=> ( C @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(7326,plain,
! [B: $i,A: $i] :
( ( ( A @ pred @ succ )
!= ( B @ succ ) )
| ( A != B ) ),
inference(paramod_ordered,[status(thm)],[184,4727]) ).
thf(7327,plain,
! [A: $i] :
( ( A @ pred )
!= A ),
inference(pattern_uni,[status(thm)],[7326:[bind(A,$thf( C )),bind(B,$thf( C @ pred ))]]) ).
thf(7380,plain,
! [A: $i] :
( ( A @ pred )
!= A ),
inference(simp,[status(thm)],[7327]) ).
thf(13372,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[178,194]) ).
thf(13373,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13372]) ).
thf(13374,plain,
n4 @ ( n2 @ lt ),
inference(pattern_uni,[status(thm)],[13373:[bind(A,$thf( n2 )),bind(B,$thf( n4 ))]]) ).
thf(3661,plain,
( ~ $true
| ( ( sk9 @ ( n0 @ leq ) )
!= ( sk8 @ ( n0 @ leq ) ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(eqfactor_ordered,[status(thm)],[3601]) ).
thf(3663,plain,
( ( sk9 != sk8 )
| ( n0 != n0 )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(simp,[status(thm)],[3661]) ).
thf(3670,plain,
( ( sk9 != sk8 )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(simp,[status(thm)],[3663]) ).
thf(7201,plain,
( ( sk9 != sk8 )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| $false ),
inference(rewrite,[status(thm)],[3670,7091]) ).
thf(7202,plain,
( ( sk9 != sk8 )
| ( sk8 @ ( n0 @ leq ) )
| sk4 ),
inference(simp,[status(thm)],[7201]) ).
thf(2872,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[618,187]) ).
thf(2873,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2872]) ).
thf(2874,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n3 != A ) ),
inference(simp,[status(thm)],[2873]) ).
thf(2875,plain,
tptp_minus_1 != n3,
inference(simp,[status(thm)],[2874]) ).
thf(36,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/sandbox/benchmark/theBenchmark.p',const_array2_select) ).
thf(231,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)],[36]) ).
thf(13282,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n1 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[625,194]) ).
thf(13283,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n1 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13282]) ).
thf(13284,plain,
n1 @ ( n0 @ lt ),
inference(pattern_uni,[status(thm)],[13283:[bind(A,$thf( n0 )),bind(B,$thf( n1 ))]]) ).
thf(70,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/sandbox/benchmark/theBenchmark.p',sel3_update_3) ).
thf(556,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)],[70]) ).
thf(1550,plain,
! [A: $i] :
( ( ( n4 @ ( n999 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[221,187]) ).
thf(1551,plain,
! [A: $i] :
( ( n4 @ ( n999 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1550]) ).
thf(1552,plain,
! [A: $i] :
( ( n4 != A )
| ( n999 != A ) ),
inference(simp,[status(thm)],[1551]) ).
thf(1553,plain,
n4 != n999,
inference(simp,[status(thm)],[1552]) ).
thf(2322,plain,
! [A: $i] :
( ( ( n3 @ ( n6 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[392,187]) ).
thf(2323,plain,
! [A: $i] :
( ( n3 @ ( n6 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2322]) ).
thf(2324,plain,
! [A: $i] :
( ( n3 != A )
| ( n6 != A ) ),
inference(simp,[status(thm)],[2323]) ).
thf(2325,plain,
n3 != n6,
inference(simp,[status(thm)],[2324]) ).
thf(37,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/sandbox/benchmark/theBenchmark.p',matrix_symm_aba2) ).
thf(235,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)],[37]) ).
thf(43,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/sandbox/benchmark/theBenchmark.p',matrix_symm_trans) ).
thf(272,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)],[43]) ).
thf(5210,plain,
! [A: $i] :
( ( ( n3 @ succ )
!= ( A @ succ ) )
| ( ( n4 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[3345,181]) ).
thf(5211,plain,
( ( n4 @ pred )
= n3 ),
inference(pattern_uni,[status(thm)],[5210:[bind(A,$thf( n3 ))]]) ).
thf(2092,plain,
! [A: $i] :
( ( ( n0 @ ( n999 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[261,187]) ).
thf(2093,plain,
! [A: $i] :
( ( n0 @ ( n999 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2092]) ).
thf(2094,plain,
! [A: $i] :
( ( n0 != A )
| ( n999 != A ) ),
inference(simp,[status(thm)],[2093]) ).
thf(2095,plain,
n999 != n0,
inference(simp,[status(thm)],[2094]) ).
thf(67,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/sandbox/benchmark/theBenchmark.p',matrix_symm_aba1) ).
thf(536,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)],[67]) ).
thf(9165,plain,
( ( ( n3 @ pred )
!= ( n3 @ pred ) )
| ~ sk4
| ( n2 @ ( sk5 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[5229,9164]) ).
thf(9166,plain,
( ~ sk4
| ( n2 @ ( sk5 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[9165:[]]) ).
thf(106,plain,
( ( sk9 @ ( n0 @ leq ) )
| ( ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(149,plain,
( ( sk9 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) )
| ( ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[106]) ).
thf(7119,plain,
( ( sk9 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ $true
| ~ $true
| ( ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ),
inference(rewrite,[status(thm)],[149,128,105]) ).
thf(7120,plain,
( ( sk9 @ ( n0 @ leq ) )
| sk4
| sk1
| ( ( sk7 @ ( sk8 @ ( pminus_ds1_filter @ a_select3 ) ) )
!= ( sk8 @ ( sk7 @ ( pminus_ds1_filter @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[7119]) ).
thf(7121,plain,
( ( sk8 != sk7 )
| ( sk8 != sk7 )
| ( pminus_ds1_filter != pminus_ds1_filter )
| ( sk9 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(simp,[status(thm)],[7120]) ).
thf(7156,plain,
( ( sk8 != sk7 )
| ( sk9 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(simp,[status(thm)],[7121]) ).
thf(14385,plain,
( ( sk8 != sk7 )
| ( sk9 @ ( n0 @ leq ) )
| sk4
| $false ),
inference(rewrite,[status(thm)],[7156,7091]) ).
thf(14386,plain,
( ( sk8 != sk7 )
| ( sk9 @ ( n0 @ leq ) )
| sk4 ),
inference(simp,[status(thm)],[14385]) ).
thf(13327,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[462,194]) ).
thf(13328,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13327]) ).
thf(13329,plain,
n3 @ ( n0 @ lt ),
inference(pattern_uni,[status(thm)],[13328:[bind(A,$thf( n0 )),bind(B,$thf( n3 ))]]) ).
thf(2948,plain,
! [A: $i] :
( ( ( n0 @ ( n1 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[625,187]) ).
thf(2949,plain,
! [A: $i] :
( ( n0 @ ( n1 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2948]) ).
thf(2950,plain,
! [A: $i] :
( ( n0 != A )
| ( n1 != A ) ),
inference(simp,[status(thm)],[2949]) ).
thf(2951,plain,
n1 != n0,
inference(simp,[status(thm)],[2950]) ).
thf(1873,plain,
! [A: $i] :
( ( ( n6 @ ( n999 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[225,187]) ).
thf(1874,plain,
! [A: $i] :
( ( n6 @ ( n999 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1873]) ).
thf(1875,plain,
! [A: $i] :
( ( n6 != A )
| ( n999 != A ) ),
inference(simp,[status(thm)],[1874]) ).
thf(1876,plain,
n6 != n999,
inference(simp,[status(thm)],[1875]) ).
thf(48,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/sandbox/benchmark/theBenchmark.p',matrix_symm_joseph_update) ).
thf(294,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)],[48]) ).
thf(10861,plain,
! [A: $i] :
( ( ( n3 @ succ @ succ @ succ @ succ )
!= ( A @ succ ) )
| ( A @ ( n6 @ succ @ gt ) ) ),
inference(paramod_ordered,[status(thm)],[10799,176]) ).
thf(10862,plain,
n3 @ succ @ succ @ succ @ ( n6 @ succ @ gt ),
inference(pattern_uni,[status(thm)],[10861:[bind(A,$thf( n3 @ succ @ succ @ succ ))]]) ).
thf(11231,plain,
n5 @ succ @ ( n6 @ succ @ gt ),
inference(rewrite,[status(thm)],[10862,8581]) ).
thf(34,axiom,
n1 @ ( n999 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_999_1) ).
thf(227,plain,
n1 @ ( n999 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(2088,plain,
! [A: $i] :
( ( ( n1 @ ( n999 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[227,187]) ).
thf(2089,plain,
! [A: $i] :
( ( n1 @ ( n999 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2088]) ).
thf(2090,plain,
! [A: $i] :
( ( n1 != A )
| ( n999 != A ) ),
inference(simp,[status(thm)],[2089]) ).
thf(2091,plain,
n1 != n999,
inference(simp,[status(thm)],[2090]) ).
thf(5214,plain,
! [A: $i] :
( ( ( n0 @ succ )
!= ( A @ succ ) )
| ( ( n1 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[206,181]) ).
thf(5215,plain,
( ( n1 @ pred )
= n0 ),
inference(pattern_uni,[status(thm)],[5214:[bind(A,$thf( n0 ))]]) ).
thf(13375,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n999 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[227,194]) ).
thf(13376,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n999 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13375]) ).
thf(13377,plain,
n999 @ ( n1 @ lt ),
inference(pattern_uni,[status(thm)],[13376:[bind(A,$thf( n1 )),bind(B,$thf( n999 ))]]) ).
thf(11049,plain,
! [A: $i] :
( ( ( n5 @ succ @ succ )
!= ( A @ succ ) )
| ( ( n6 @ succ )
!= A ) ),
inference(paramod_ordered,[status(thm)],[10982,4727]) ).
thf(11050,plain,
( ( n5 @ succ )
!= ( n6 @ succ ) ),
inference(pattern_uni,[status(thm)],[11049:[bind(A,$thf( n5 @ succ ))]]) ).
thf(11114,plain,
( ( n6 @ succ )
!= n6 ),
inference(rewrite,[status(thm)],[11050,3972]) ).
thf(2262,plain,
( ~ $true
| ( ( sk10 @ ( n0 @ leq ) )
!= ( sk8 @ ( n0 @ leq ) ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(eqfactor_ordered,[status(thm)],[2215]) ).
thf(2264,plain,
( ( sk10 != sk8 )
| ( n0 != n0 )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(simp,[status(thm)],[2262]) ).
thf(2269,plain,
( ( sk10 != sk8 )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(simp,[status(thm)],[2264]) ).
thf(7183,plain,
( ( sk10 != sk8 )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| $false ),
inference(rewrite,[status(thm)],[2269,7091]) ).
thf(7184,plain,
( ( sk10 != sk8 )
| ( sk8 @ ( n0 @ leq ) )
| sk4 ),
inference(simp,[status(thm)],[7183]) ).
thf(114,plain,
( ( ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) ) )
| ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(155,plain,
( ( sk8 @ ( n0 @ leq ) )
| sk4
| sk1
| ~ ( n1 @ ( n999 @ minus ) @ ( pv5 @ leq ) )
| ~ ( pv5 @ ( n0 @ leq ) )
| ( ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[114]) ).
thf(8206,plain,
( ( sk8 @ ( n0 @ leq ) )
| sk4
| $false
| ~ ( n999 @ pred @ ( pv5 @ leq ) )
| ~ $true
| ( ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) ) ) ),
inference(rewrite,[status(thm)],[155,128,7091,287]) ).
thf(8207,plain,
( ( sk8 @ ( n0 @ leq ) )
| sk4
| ~ ( n999 @ pred @ ( pv5 @ leq ) )
| ( ( sk9 @ ( sk10 @ ( id_ds1_filter @ a_select3 ) ) )
!= ( sk10 @ ( sk9 @ ( id_ds1_filter @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[8206]) ).
thf(2605,plain,
( ~ $true
| ( ( sk9 @ ( n0 @ leq ) )
!= ( sk7 @ ( n0 @ leq ) ) )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(eqfactor_ordered,[status(thm)],[2558]) ).
thf(2607,plain,
( ( sk9 != sk7 )
| ( n0 != n0 )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(simp,[status(thm)],[2605]) ).
thf(2614,plain,
( ( sk9 != sk7 )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| sk1 ),
inference(simp,[status(thm)],[2607]) ).
thf(7251,plain,
( ( sk9 != sk7 )
| ( sk7 @ ( n0 @ leq ) )
| sk4
| $false ),
inference(rewrite,[status(thm)],[2614,7091]) ).
thf(7252,plain,
( ( sk9 != sk7 )
| ( sk7 @ ( n0 @ leq ) )
| sk4 ),
inference(simp,[status(thm)],[7251]) ).
thf(623,plain,
! [A: $i] :
( ( n3 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(cnf,[status(esa)],[622]) ).
thf(624,plain,
! [A: $i] :
( ( n3 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(lifteq,[status(thm)],[623]) ).
thf(62,axiom,
! [A: $i] :
( ( n5 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_5_r) ).
thf(469,plain,
! [A: $i] :
( ( n5 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(2687,plain,
! [A: $i] :
( ( ( n0 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[602,187]) ).
thf(2688,plain,
! [A: $i] :
( ( n0 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2687]) ).
thf(2689,plain,
! [A: $i] :
( ( n0 != A )
| ( n4 != A ) ),
inference(simp,[status(thm)],[2688]) ).
thf(2690,plain,
n4 != n0,
inference(simp,[status(thm)],[2689]) ).
thf(212,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 @ sk11 ) ) ) @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[211]) ).
thf(215,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( A @ ( B @ ( C @ ( D @ sk11 ) ) ) @ ( n0 @ leq ) )
| ( ( A @ ( D @ ( B @ ( C @ tptp_update2 ) ) @ a_select2 ) )
= D ) ),
inference(lifteq,[status(thm)],[212]) ).
thf(13351,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[632,194]) ).
thf(13352,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13351]) ).
thf(13353,plain,
n4 @ ( n1 @ lt ),
inference(pattern_uni,[status(thm)],[13352:[bind(A,$thf( n1 )),bind(B,$thf( n4 ))]]) ).
thf(13309,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n2 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[166,194]) ).
thf(13310,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n2 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13309]) ).
thf(13311,plain,
n2 @ ( tptp_minus_1 @ lt ),
inference(pattern_uni,[status(thm)],[13310:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n2 ))]]) ).
thf(21106,plain,
$false,
inference(e,[status(thm)],[5229,13266,629,7272,3345,1995,468,481,13302,941,170,5225,683,217,13341,3153,614,202,597,533,10395,7188,2686,13317,1872,472,185,5227,288,13287,11151,7178,174,404,570,184,619,13275,196,5231,189,284,10982,228,13365,13263,13350,13332,261,606,4622,1347,7258,3934,179,591,13290,216,13356,602,13305,634,221,293,3157,265,206,10799,397,248,201,10598,102,9164,12705,220,13260,3972,13335,598,392,165,11191,192,14524,13254,197,625,3297,665,13359,2181,456,13269,3799,285,224,13347,615,9889,2694,188,388,169,593,7204,13344,256,7091,225,13308,554,637,3671,679,622,393,647,13169,8439,5217,128,266,633,205,13326,7646,398,1035,618,2275,166,264,573,8859,3158,601,176,13338,13368,2489,8581,7180,204,2959,579,291,391,382,7270,10393,466,181,604,9243,187,7514,2493,7379,2955,230,649,1690,599,2871,477,1557,609,13272,621,7186,7250,198,462,626,7869,223,394,226,653,167,2867,13278,13371,548,194,648,209,7264,3305,463,13320,576,3715,199,673,177,182,13299,2279,175,8043,571,595,612,7380,13374,7202,2875,231,13284,627,4727,556,1553,203,2325,218,3336,632,568,235,207,272,5211,2095,536,287,9166,14386,262,13329,2951,1876,603,210,294,195,11231,2091,5215,13377,11114,7184,8207,575,596,459,178,7252,607,395,624,163,200,227,469,2690,215,13353,222,13311]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV117+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.12 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.22/0.47 % Computer : n016.cluster.edu
% 0.22/0.47 % Model : x86_64 x86_64
% 0.22/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.47 % Memory : 8046.5625MB
% 0.22/0.47 % OS : Linux 6.8.0-71-generic
% 0.22/0.47 % CPULimit : 300
% 0.22/0.47 % WCLimit : 300
% 0.22/0.47 % DateTime : Sat Sep 26 13:18:15 UTC 2026
% 0.22/0.47 % CPUTime :
% 0.22/0.47 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.10/1.11 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.40/1.52 % [INFO] Parsing done (406ms).
% 2.40/1.54 % [INFO] Running in sequential loop mode.
% 3.53/2.10 % [INFO] eprover registered as external prover.
% 3.53/2.10 % [INFO] Scanning for conjecture ...
% 3.94/2.25 % [INFO] Found a conjecture (or negated_conjecture) and 101 axioms. Running axiom selection ...
% 4.21/2.36 % [INFO] Axiom selection finished. Selected 99 axioms (removed 2 axioms).
% 4.55/2.47 % [INFO] Problem is first-order (TPTP FOF).
% 4.55/2.50 % [INFO] Type checking passed.
% 4.86/2.50 % [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 ...
% 101.67/22.70 % External prover 'e' found a proof!
% 101.67/22.70 % [INFO] Killing All external provers ...
% 101.67/22.71 % Time passed: 22059ms (effective reasoning time: 21152ms)
% 101.67/22.71 % 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)>
% 101.67/22.71 % Axioms used in derivation (99): gt_6_0, gt_999_6, gt_0_tptp_minus_1, leq_minus, gt_999_1, sel3_update_2, gt_6_1, sel2_update_2, succ_plus_5_l, lt_gt, gt_5_tptp_minus_1, succ_plus_3_r, gt_4_3, transitivity_gt, gt_6_4, matrix_symm_inv, matrix_symm_trans, finite_domain_1, gt_5_0, const_array2_select, finite_domain_6, gt_2_tptp_minus_1, gt_6_tptp_minus_1, sel3_update_3, leq_geq, gt_999_5, gt_1_0, leq_gt2, gt_5_4, gt_999_0, succ_plus_1_l, gt_3_2, matrix_symm_add, leq_succ_gt, finite_domain_5, pred_minus_1, gt_6_5, successor_3, gt_3_tptp_minus_1, matrix_symm_update_diagonal, sel2_update_1, gt_4_2, matrix_symm_sub, gt_5_3, gt_999_2, 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, leq_succ_succ, sum_plus_base_float, succ_plus_2_l, gt_999_3, gt_3_1, gt_4_1, gt_2_0, gt_5_2, gt_999_tptp_minus_1, const_array1_select, leq_gt_pred, matrix_symm_joseph_update, succ_pred, totality, successor_6, transitivity_leq, finite_domain_3, uniform_int_rand_ranges_lo, gt_6_3, sel3_update_1, successor_1, sum_plus_base, irreflexivity_gt, successor_5, gt_3_0, sel2_update_3, pred_succ, gt_999_4, succ_plus_1_r, succ_plus_3_l, gt_4_tptp_minus_1, succ_plus_4_r, gt_4_0, succ_plus_2_r, gt_6_2, leq_succ_gt_equiv, gt_5_1, uniform_int_rand_ranges_hi, gt_2_1, finite_domain_0, leq_succ
% 101.67/22.71 % No. of inferences in proof: 755
% 101.67/22.71 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 22059 ms resp. 21152 ms w/o parsing
% 104.17/23.09 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 104.17/23.10 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------