%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SWV055+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 : n014.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:01 AM UTC 2026
% Result : Theorem 78.76s 28.32s
% Output : Refutation 65.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 96
% Syntax : Number of formulae : 554 ( 238 unt; 0 typ; 6 def)
% Number of atoms : 1888 ( 780 equ; 0 cnn)
% Maximal formula atoms : 41 ( 3 avg)
% Number of connectives : 9706 ( 835 ~; 692 |; 254 &;7783 @)
% ( 5 <=>; 137 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 5 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 47 ( 44 usr; 19 con; 0-4 aty)
% Number of variables : 671 ( 4 ^; 660 !; 1 ?; 671 :)
% ( 0 !>; 0 ?*; 0 @-; 6 @+)
% Comments :
%------------------------------------------------------------------------------
thf(leq_decl,type,
leq: $i > $i > $o ).
thf(n0_decl,type,
n0: $i ).
thf(pv10_decl,type,
pv10: $i ).
thf(minus_decl,type,
minus: $i > $i > $i ).
thf(n135300_decl,type,
n135300: $i ).
thf(n1_decl,type,
n1: $i ).
thf(sum_decl,type,
sum: $i > $i > $i > $i ).
thf(n5_decl,type,
n5: $i ).
thf(a_select3_decl,type,
a_select3: $i > $i > $i > $i ).
thf(q_decl,type,
q: $i ).
thf(divide_decl,type,
divide: $i > $i > $i ).
thf(sqrt_decl,type,
sqrt: $i > $i ).
thf(times_decl,type,
times: $i > $i > $i ).
thf(center_decl,type,
center: $i ).
thf(a_select2_decl,type,
a_select2: $i > $i > $i ).
thf(x_decl,type,
x: $i ).
thf(plus_decl,type,
plus: $i > $i > $i ).
thf(n3_decl,type,
n3: $i ).
thf(succ_decl,type,
succ: $i > $i ).
thf(pred_decl,type,
pred: $i > $i ).
thf(gt_decl,type,
gt: $i > $i > $o ).
thf(tptp_minus_1_decl,type,
tptp_minus_1: $i ).
thf(n2_decl,type,
n2: $i ).
thf(n4_decl,type,
n4: $i ).
thf(lt_decl,type,
lt: $i > $i > $o ).
thf(tptp_update2_decl,type,
tptp_update2: $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(uniform_int_rnd_decl,type,
uniform_int_rnd: $i > $i > $i ).
thf(tptp_msub_decl,type,
tptp_msub: $i > $i > $i ).
thf(tptp_float_0_0_decl,type,
tptp_float_0_0: $i ).
thf(tptp_const_array1_decl,type,
tptp_const_array1: $i > $i > $i ).
thf(inv_decl,type,
inv: $i > $i ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $i ).
thf(sk8_decl,type,
sk8: $i > $i > $i ).
thf(sk9_decl,type,
sk9: $i > $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ( ( ( n1 @ ( n0 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ! [B: $i] :
( ( A @ ( pv10 @ ( q @ a_select3 ) ) )
= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( B @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( B @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( A @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( A @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( A @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( A @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ( ( ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ! [B: $i] :
( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
= n1 ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] :
( ( A @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [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(sk9_def,definition,
( sk9
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( ( A @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) )
& ( A @ ( B @ ( A @ sk8 ) @ leq ) )
& ( B @ ( A @ sk8 ) @ ( n0 @ leq ) ) )
=> ( ( C @ ( B @ ( A @ sk8 ) @ ( B @ a_select3 ) ) )
= ( B @ ( A @ sk8 ) @ ( C @ ( B @ a_select3 ) ) ) ) ) ) ) ).
thf(15,axiom,
! [A: $i] :
( ( A @ ( n2 @ plus ) )
= ( A @ succ @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_2_l) ).
thf(138,plain,
! [A: $i] :
( ( A @ ( n2 @ plus ) )
= ( A @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(48,axiom,
( ( tptp_minus_1 @ succ )
= n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_tptp_minus_1) ).
thf(345,plain,
( ( tptp_minus_1 @ succ )
= n0 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(346,plain,
( ( tptp_minus_1 @ succ )
= n0 ),
inference(lifteq,[status(thm)],[345]) ).
thf(14,axiom,
! [A: $i] :
( ( A @ succ @ pred )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',pred_succ) ).
thf(135,plain,
! [A: $i] :
( ( A @ succ @ pred )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(136,plain,
! [A: $i] :
( ( A @ succ @ pred )
= A ),
inference(cnf,[status(esa)],[135]) ).
thf(137,plain,
! [A: $i] :
( ( A @ succ @ pred )
= A ),
inference(lifteq,[status(thm)],[136]) ).
thf(11444,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ succ )
!= ( A @ succ ) )
| ( ( n0 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[346,137]) ).
thf(11445,plain,
( ( n0 @ pred )
= tptp_minus_1 ),
inference(pattern_uni,[status(thm)],[11444:[bind(A,$thf( tptp_minus_1 ))]]) ).
thf(49,axiom,
! [A: $i,B: $i] :
( ( B @ pred @ ( A @ leq ) )
<=> ( A @ ( B @ gt ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_gt_pred) ).
thf(347,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)],[49]) ).
thf(80,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(555,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ leq ) )
& ( B @ ( A @ leq ) ) )
=> ( C @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(3,axiom,
! [A: $i] :
( ( A @ ( n3 @ plus ) )
= ( A @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_3_l) ).
thf(113,plain,
! [A: $i] :
( ( A @ ( n3 @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(114,plain,
! [A: $i] :
( ( A @ ( n3 @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(cnf,[status(esa)],[113]) ).
thf(115,plain,
! [A: $i] :
( ( A @ ( n3 @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(lifteq,[status(thm)],[114]) ).
thf(31,axiom,
! [A: $i] :
( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
= n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_plus_base) ).
thf(183,plain,
! [A: $i] :
( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
= n0 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(184,plain,
! [A: $i] :
( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
= n0 ),
inference(cnf,[status(esa)],[183]) ).
thf(185,plain,
! [A: $i] :
( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
= n0 ),
inference(lifteq,[status(thm)],[184]) ).
thf(1,conjecture,
( ( ! [A: $i,B: $i] :
( ( ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
= n1 ) )
& ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
& ( pv10 @ ( n0 @ leq ) ) )
=> ( ! [A: $i,B: $i] :
( ( ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
= n1 ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n0 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A @ ( pv10 @ ( q @ a_select3 ) ) )
= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( B @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( B @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( A @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( A @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) )
& ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
& ( pv10 @ ( n0 @ leq ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cl5_nebula_norm_0037) ).
thf(2,negated_conjecture,
~ ( ( ! [A: $i,B: $i] :
( ( ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
= n1 ) )
& ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
& ( pv10 @ ( n0 @ leq ) ) )
=> ( ! [A: $i,B: $i] :
( ( ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
= n1 ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n0 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A @ ( pv10 @ ( q @ a_select3 ) ) )
= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( B @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( B @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( A @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( A @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) )
& ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
& ( pv10 @ ( n0 @ leq ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(92,plain,
~ ( ( ! [A: $i,B: $i] :
( ( ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
= n1 ) )
& ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
& ( pv10 @ ( n0 @ leq ) ) )
=> ( ! [A: $i,B: $i] :
( ( ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
= n1 ) )
& ! [A: $i,B: $i] :
( ( ( n1 @ ( n0 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A @ ( pv10 @ ( q @ a_select3 ) ) )
= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( B @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( B @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( A @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( A @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) )
& ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
& ( pv10 @ ( n0 @ leq ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(93,plain,
~ ( ( ! [A: $i] :
( ( ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ! [B: $i] :
( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
= n1 ) )
& ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
& ( pv10 @ ( n0 @ leq ) ) )
=> ( ! [A: $i] :
( ( ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ! [B: $i] :
( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
= n1 ) )
& ! [A: $i] :
( ( ( n1 @ ( n0 @ minus ) @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ! [B: $i] :
( ( A @ ( pv10 @ ( q @ a_select3 ) ) )
= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( B @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( B @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( A @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( A @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) )
& ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
& ( pv10 @ ( n0 @ leq ) ) ) ),
inference(miniscope,[status(thm)],[92]) ).
thf(94,plain,
! [B: $i,A: $i] :
( ( ( ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) )
& ( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) )
& ( ( sk3 @ ( n0 @ leq ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) )
& ( ( ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) )
& ( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) )
& ( ( sk3 @ ( n0 @ leq ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) )
& ( ( ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( sk1 @ ( n0 @ leq ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) )
& ( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( sk1 @ ( n0 @ leq ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) )
& ( ( sk3 @ ( n0 @ leq ) )
| ( sk1 @ ( n0 @ leq ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) )
& ( ( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
= n1 )
| ~ ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) )
& ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
& ( pv10 @ ( n0 @ leq ) ) ),
inference(cnf,[status(esa)],[93]) ).
thf(97,plain,
pv10 @ ( n0 @ leq ),
inference(cnfConj,[status(thm)],[94]) ).
thf(98,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
= n1 )
| ~ ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[94]) ).
thf(110,plain,
! [B: $i,A: $i] :
( ~ ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) )
| ( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
= n1 ) ),
inference(lifteq,[status(thm)],[98]) ).
thf(105,plain,
( ( ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[94]) ).
thf(109,plain,
( ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) )
| ( ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ),
inference(lifteq,[status(thm)],[105]) ).
thf(96,plain,
n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ),
inference(cnfConj,[status(thm)],[94]) ).
thf(606,plain,
( ~ $true
| ~ $true
| ( ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ),
inference(rewrite,[status(thm)],[109,96,97]) ).
thf(607,plain,
( ( ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ),
inference(simp,[status(thm)],[606]) ).
thf(2319,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) ) )
| ( n1 != n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,607]) ).
thf(2320,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[2319]) ).
thf(2321,plain,
( ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[2320:[bind(A,$thf( sk3 )),bind(B,$thf( sk4 ))]]) ).
thf(2405,plain,
( ( ( sk3 @ ( n0 @ leq ) )
!= ( pv10 @ ( n0 @ leq ) ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[97,2321]) ).
thf(2406,plain,
( ( ( sk3 @ ( n0 @ leq ) )
!= ( pv10 @ ( n0 @ leq ) ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[2405]) ).
thf(2488,plain,
( ( sk3 != pv10 )
| ( n0 != n0 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[2406]) ).
thf(2526,plain,
( ( sk3 != pv10 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[2488]) ).
thf(11215,plain,
! [A: $i] :
( ( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) ) )
| ( sk3 != pv10 )
| ( ( n0 @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) )
!= ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[185,2526]) ).
thf(11224,plain,
! [A: $i] :
( ( A
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt ) )
| ( ( n1 @ ( n5 @ minus ) )
!= tptp_minus_1 )
| ( n0 != n0 )
| ( sk3 != pv10 )
| ( ( n0 @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) )
!= ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[11215]) ).
thf(11256,plain,
( ( ( n1 @ ( n5 @ minus ) )
!= tptp_minus_1 )
| ( sk3 != pv10 )
| ( ( n0 @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) )
!= ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[11224]) ).
thf(78,axiom,
n0 @ ( n4 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_0) ).
thf(551,plain,
n0 @ ( n4 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(16,axiom,
! [A: $i] :
~ ( A @ ( A @ gt ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',irreflexivity_gt) ).
thf(141,plain,
! [A: $i] :
~ ( A @ ( A @ gt ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(142,plain,
~ ? [A: $i] : ( A @ ( A @ gt ) ),
inference(miniscope,[status(thm)],[141]) ).
thf(143,plain,
! [A: $i] :
~ ( A @ ( A @ gt ) ),
inference(cnf,[status(esa)],[142]) ).
thf(3009,plain,
! [A: $i] :
( ( ( n0 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[551,143]) ).
thf(3010,plain,
! [A: $i] :
( ( n0 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[3009]) ).
thf(3011,plain,
! [A: $i] :
( ( n0 != A )
| ( n4 != A ) ),
inference(simp,[status(thm)],[3010]) ).
thf(3012,plain,
n4 != n0,
inference(simp,[status(thm)],[3011]) ).
thf(5,axiom,
! [A: $i] : ( A @ ( A @ succ @ gt ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_succ) ).
thf(119,plain,
! [A: $i] : ( A @ ( A @ succ @ gt ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(120,plain,
! [A: $i] : ( A @ ( A @ succ @ gt ) ),
inference(cnf,[status(esa)],[119]) ).
thf(106,plain,
( ( sk3 @ ( n0 @ leq ) )
| ( sk1 @ ( n0 @ leq ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[94]) ).
thf(591,plain,
( ( sk3 @ ( n0 @ leq ) )
| ( sk1 @ ( n0 @ leq ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[106,96,97]) ).
thf(592,plain,
( ( sk3 @ ( n0 @ leq ) )
| ( sk1 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[591]) ).
thf(593,plain,
( ~ $true
| ( ( sk3 @ ( n0 @ leq ) )
!= ( sk1 @ ( n0 @ leq ) ) )
| ( sk1 @ ( n0 @ leq ) ) ),
inference(eqfactor_ordered,[status(thm)],[592]) ).
thf(595,plain,
( ( sk3 != sk1 )
| ( n0 != n0 )
| ( sk1 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[593]) ).
thf(596,plain,
( ( sk3 != sk1 )
| ( sk1 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[595]) ).
thf(2435,plain,
( ( ( sk3 @ ( n0 @ leq ) )
!= ( sk1 @ ( n0 @ leq ) ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ~ $true
| ( sk3 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[596,2321]) ).
thf(2436,plain,
( ( ( sk3 @ ( n0 @ leq ) )
!= ( sk1 @ ( n0 @ leq ) ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[2435]) ).
thf(2495,plain,
( ( sk3 != sk1 )
| ( n0 != n0 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[2436]) ).
thf(2531,plain,
( ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[2495]) ).
thf(3361,plain,
( ( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
!= ( pv10 @ ( n0 @ leq ) ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ $true
| ( sk3 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[97,2531]) ).
thf(3362,plain,
( ( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
!= ( pv10 @ ( n0 @ leq ) ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[3361]) ).
thf(3429,plain,
( ( ( n1 @ ( pv10 @ minus ) )
!= pv10 )
| ( sk3 != n0 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[3362]) ).
thf(45,axiom,
tptp_minus_1 @ ( n135300 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_135300_tptp_minus_1) ).
thf(340,plain,
tptp_minus_1 @ ( n135300 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(19,axiom,
tptp_minus_1 @ ( n4 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_tptp_minus_1) ).
thf(153,plain,
tptp_minus_1 @ ( n4 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(81,axiom,
n4 @ ( n5 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_4) ).
thf(557,plain,
n4 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(3347,plain,
! [A: $i] :
( ( ( n4 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[557,143]) ).
thf(3348,plain,
! [A: $i] :
( ( n4 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[3347]) ).
thf(3349,plain,
! [A: $i] :
( ( n4 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[3348]) ).
thf(3350,plain,
n4 != n5,
inference(simp,[status(thm)],[3349]) ).
thf(65,axiom,
( ( n0 @ succ @ succ @ succ )
= n3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_3) ).
thf(505,plain,
( ( n0 @ succ @ succ @ succ )
= n3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(506,plain,
( ( n0 @ succ @ succ @ succ )
= n3 ),
inference(lifteq,[status(thm)],[505]) ).
thf(24,axiom,
( ( n0 @ succ )
= n1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_1) ).
thf(161,plain,
( ( n0 @ succ )
= n1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(162,plain,
( ( n0 @ succ )
= n1 ),
inference(lifteq,[status(thm)],[161]) ).
thf(3708,plain,
( ( n1 @ succ @ succ )
= n3 ),
inference(rewrite,[status(thm)],[506,162]) ).
thf(25,axiom,
( ( n0 @ succ @ succ @ succ @ succ )
= n4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_4) ).
thf(163,plain,
( ( n0 @ succ @ succ @ succ @ succ )
= n4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(164,plain,
( ( n0 @ succ @ succ @ succ @ succ )
= n4 ),
inference(lifteq,[status(thm)],[163]) ).
thf(3989,plain,
( ( n1 @ succ @ succ @ succ )
= n4 ),
inference(rewrite,[status(thm)],[164,162]) ).
thf(3993,plain,
( ( ( n1 @ succ @ succ )
!= ( n1 @ succ @ succ ) )
| ( ( n3 @ succ )
= n4 ) ),
inference(paramod_ordered,[status(thm)],[3708,3989]) ).
thf(3994,plain,
( ( n3 @ succ )
= n4 ),
inference(pattern_uni,[status(thm)],[3993:[]]) ).
thf(18,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ lt ) )
<=> ( A @ ( B @ gt ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lt_gt) ).
thf(147,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)],[18]) ).
thf(148,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)],[147]) ).
thf(149,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)],[148]) ).
thf(151,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ lt ) )
| ~ ( A @ ( B @ gt ) ) ),
inference(cnfConj,[status(thm)],[149]) ).
thf(152,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ lt ) )
| ~ ( A @ ( B @ gt ) ) ),
inference(simp,[status(thm)],[151]) ).
thf(13125,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[551,152]) ).
thf(13126,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13125]) ).
thf(13127,plain,
n4 @ ( n0 @ lt ),
inference(pattern_uni,[status(thm)],[13126:[bind(A,$thf( n0 )),bind(B,$thf( n4 ))]]) ).
thf(50,axiom,
n1 @ ( n135300 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_135300_1) ).
thf(353,plain,
n1 @ ( n135300 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(2224,plain,
! [A: $i] :
( ( ( n1 @ ( n135300 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[353,143]) ).
thf(2225,plain,
! [A: $i] :
( ( n1 @ ( n135300 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2224]) ).
thf(2226,plain,
! [A: $i] :
( ( n1 != A )
| ( n135300 != A ) ),
inference(simp,[status(thm)],[2225]) ).
thf(2227,plain,
n1 != n135300,
inference(simp,[status(thm)],[2226]) ).
thf(4130,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ succ @ gt ) )
!= ( B @ ( B @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[120,143]) ).
thf(4131,plain,
! [B: $i,A: $i] :
( ( A @ ( A @ succ @ gt ) )
!= ( B @ ( B @ gt ) ) ),
inference(simp,[status(thm)],[4130]) ).
thf(4136,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ succ )
!= B ) ),
inference(simp,[status(thm)],[4131]) ).
thf(4137,plain,
! [A: $i] :
( ( A @ succ )
!= A ),
inference(simp,[status(thm)],[4136]) ).
thf(88,axiom,
n5 @ ( n135300 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_135300_5) ).
thf(570,plain,
n5 @ ( n135300 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(54,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(412,plain,
! [A: $i] :
( tptp_float_0_0
= ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(413,plain,
! [A: $i] :
( tptp_float_0_0
= ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) ) ),
inference(cnf,[status(esa)],[412]) ).
thf(414,plain,
! [A: $i] :
( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
= tptp_float_0_0 ),
inference(lifteq,[status(thm)],[413]) ).
thf(11289,plain,
tptp_float_0_0 = n0,
inference(rewrite,[status(thm)],[414,185]) ).
thf(8,axiom,
! [A: $i] :
( ( n3 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_3_r) ).
thf(125,plain,
! [A: $i] :
( ( n3 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(52,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(357,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)],[52]) ).
thf(73,axiom,
tptp_minus_1 @ ( n5 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_tptp_minus_1) ).
thf(542,plain,
tptp_minus_1 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(1797,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n135300 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[340,143]) ).
thf(1798,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n135300 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1797]) ).
thf(1799,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n135300 != A ) ),
inference(simp,[status(thm)],[1798]) ).
thf(1800,plain,
tptp_minus_1 != n135300,
inference(simp,[status(thm)],[1799]) ).
thf(103,plain,
( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[94]) ).
thf(625,plain,
( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[103,96,97]) ).
thf(626,plain,
( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[625]) ).
thf(102,plain,
( ( ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[94]) ).
thf(108,plain,
( ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) )
| ( ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 ) ),
inference(lifteq,[status(thm)],[102]) ).
thf(1894,plain,
( ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ~ $true
| ~ $true
| ( ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 ) ),
inference(rewrite,[status(thm)],[108,96,97]) ).
thf(1895,plain,
( ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ( ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 ) ),
inference(simp,[status(thm)],[1894]) ).
thf(2280,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ( n1 != n1 )
| ~ ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,1895]) ).
thf(2281,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[2280]) ).
thf(2282,plain,
( ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[2281:[bind(A,$thf( sk3 )),bind(B,$thf( sk4 ))]]) ).
thf(2574,plain,
( ( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
!= ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ~ $true
| ~ ( sk3 @ ( n0 @ leq ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[626,2282]) ).
thf(2575,plain,
( ( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
!= ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) ) )
| ~ ( sk3 @ ( n0 @ leq ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[2574]) ).
thf(2576,plain,
( ~ ( sk3 @ ( n0 @ leq ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[2575:[]]) ).
thf(2789,plain,
( ( ( sk3 @ ( n0 @ leq ) )
!= ( sk1 @ ( n0 @ leq ) ) )
| ~ $true
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ( sk3 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[596,2576]) ).
thf(2790,plain,
( ( ( sk3 @ ( n0 @ leq ) )
!= ( sk1 @ ( n0 @ leq ) ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[2789]) ).
thf(2837,plain,
( ( sk3 != sk1 )
| ( n0 != n0 )
| ( sk3 != sk1 )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[2790]) ).
thf(2870,plain,
( ( sk3 != sk1 )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[2837]) ).
thf(3372,plain,
( ( ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
!= ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ $true
| ( sk3 != sk1 )
| ( sk3 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[2870,2531]) ).
thf(3373,plain,
( ( ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
!= ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[3372]) ).
thf(3428,plain,
( ( ( n1 @ ( pv10 @ minus ) )
!= ( n1 @ ( n0 @ minus ) ) )
| ( sk3 != sk1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[3373]) ).
thf(3463,plain,
( ( ( n1 @ ( pv10 @ minus ) )
!= ( n1 @ ( n0 @ minus ) ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[3428]) ).
thf(2733,plain,
( ( ( sk3 @ ( n0 @ leq ) )
!= ( pv10 @ ( n0 @ leq ) ) )
| ~ $true
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[97,2576]) ).
thf(2734,plain,
( ( ( sk3 @ ( n0 @ leq ) )
!= ( pv10 @ ( n0 @ leq ) ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[2733]) ).
thf(2819,plain,
( ( sk3 != pv10 )
| ( n0 != n0 )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[2734]) ).
thf(2857,plain,
( ( sk3 != pv10 )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[2819]) ).
thf(57,axiom,
n2 @ ( n5 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_2) ).
thf(419,plain,
n2 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(2400,plain,
! [A: $i] :
( ( ( n2 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[419,143]) ).
thf(2401,plain,
! [A: $i] :
( ( n2 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2400]) ).
thf(2402,plain,
! [A: $i] :
( ( n2 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[2401]) ).
thf(2403,plain,
n2 != n5,
inference(simp,[status(thm)],[2402]) ).
thf(4,axiom,
! [A: $i] :
( ( A @ pred @ succ )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_pred) ).
thf(116,plain,
! [A: $i] :
( ( A @ pred @ succ )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(117,plain,
! [A: $i] :
( ( A @ pred @ succ )
= A ),
inference(cnf,[status(esa)],[116]) ).
thf(118,plain,
! [A: $i] :
( ( A @ pred @ succ )
= A ),
inference(lifteq,[status(thm)],[117]) ).
thf(4184,plain,
! [B: $i,A: $i] :
( ( ( A @ pred @ succ )
!= ( B @ succ ) )
| ( A != B ) ),
inference(paramod_ordered,[status(thm)],[118,4137]) ).
thf(4185,plain,
! [A: $i] :
( ( A @ pred )
!= A ),
inference(pattern_uni,[status(thm)],[4184:[bind(A,$thf( C )),bind(B,$thf( C @ pred ))]]) ).
thf(4194,plain,
! [A: $i] :
( ( A @ pred )
!= A ),
inference(simp,[status(thm)],[4185]) ).
thf(17,axiom,
! [A: $i] :
( ( n4 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_4_r) ).
thf(144,plain,
! [A: $i] :
( ( n4 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(145,plain,
! [A: $i] :
( ( n4 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
inference(cnf,[status(esa)],[144]) ).
thf(146,plain,
! [A: $i] :
( ( n4 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
inference(lifteq,[status(thm)],[145]) ).
thf(139,plain,
! [A: $i] :
( ( A @ ( n2 @ plus ) )
= ( A @ succ @ succ ) ),
inference(cnf,[status(esa)],[138]) ).
thf(140,plain,
! [A: $i] :
( ( A @ ( n2 @ plus ) )
= ( A @ succ @ succ ) ),
inference(lifteq,[status(thm)],[139]) ).
thf(12430,plain,
! [B: $i,A: $i] :
( ( ( n4 @ ( A @ plus ) )
!= ( B @ ( n2 @ plus ) ) )
| ( ( A @ succ @ succ @ succ @ succ )
= ( B @ succ @ succ ) ) ),
inference(paramod_ordered,[status(thm)],[146,140]) ).
thf(12431,plain,
( ( n2 @ succ @ succ @ succ @ succ )
= ( n4 @ succ @ succ ) ),
inference(pattern_uni,[status(thm)],[12430:[bind(A,$thf( n2 )),bind(B,$thf( n4 ))]]) ).
thf(91,axiom,
( ( n0 @ succ @ succ )
= n2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_2) ).
thf(573,plain,
( ( n0 @ succ @ succ )
= n2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(574,plain,
( ( n0 @ succ @ succ )
= n2 ),
inference(lifteq,[status(thm)],[573]) ).
thf(3695,plain,
( ( n1 @ succ )
= n2 ),
inference(rewrite,[status(thm)],[574,162]) ).
thf(3715,plain,
( ( ( n1 @ succ )
!= ( n1 @ succ ) )
| ( ( n2 @ succ )
= n3 ) ),
inference(paramod_ordered,[status(thm)],[3695,3708]) ).
thf(3716,plain,
( ( n2 @ succ )
= n3 ),
inference(pattern_uni,[status(thm)],[3715:[]]) ).
thf(84,axiom,
( ( n0 @ succ @ succ @ succ @ succ @ succ )
= n5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_5) ).
thf(562,plain,
( ( n0 @ succ @ succ @ succ @ succ @ succ )
= n5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(563,plain,
( ( n0 @ succ @ succ @ succ @ succ @ succ )
= n5 ),
inference(lifteq,[status(thm)],[562]) ).
thf(4196,plain,
( ( n1 @ succ @ succ @ succ @ succ )
= n5 ),
inference(rewrite,[status(thm)],[563,162]) ).
thf(4216,plain,
( ( ( n1 @ succ @ succ @ succ )
!= ( n1 @ succ @ succ @ succ ) )
| ( ( n4 @ succ )
= n5 ) ),
inference(paramod_ordered,[status(thm)],[3989,4196]) ).
thf(4217,plain,
( ( n4 @ succ )
= n5 ),
inference(pattern_uni,[status(thm)],[4216:[]]) ).
thf(12909,plain,
( ( n3 @ succ @ succ @ succ )
= ( n5 @ succ ) ),
inference(rewrite,[status(thm)],[12431,3716,4217]) ).
thf(12917,plain,
! [A: $i] :
( ( ( n3 @ succ @ succ @ succ )
!= ( A @ succ ) )
| ( ( n5 @ succ )
!= A ) ),
inference(paramod_ordered,[status(thm)],[12909,4137]) ).
thf(12918,plain,
( ( n3 @ succ @ succ )
!= ( n5 @ succ ) ),
inference(pattern_uni,[status(thm)],[12917:[bind(A,$thf( n3 @ succ @ succ ))]]) ).
thf(4229,plain,
( ( ( n1 @ succ )
!= ( n1 @ succ ) )
| ( ( n2 @ succ @ succ @ succ )
= n5 ) ),
inference(paramod_ordered,[status(thm)],[3695,4196]) ).
thf(4230,plain,
( ( n2 @ succ @ succ @ succ )
= n5 ),
inference(pattern_uni,[status(thm)],[4229:[]]) ).
thf(4589,plain,
( ( n3 @ succ @ succ )
= n5 ),
inference(rewrite,[status(thm)],[4230,3716]) ).
thf(13045,plain,
( ( n5 @ succ )
!= n5 ),
inference(rewrite,[status(thm)],[12918,4589]) ).
thf(95,plain,
( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( sk1 @ ( n0 @ leq ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[94]) ).
thf(597,plain,
( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( sk1 @ ( n0 @ leq ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[95,96,97]) ).
thf(598,plain,
( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( sk1 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[597]) ).
thf(100,plain,
( ( ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( sk1 @ ( n0 @ leq ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[94]) ).
thf(111,plain,
( ( sk1 @ ( n0 @ leq ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) )
| ( ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 ) ),
inference(lifteq,[status(thm)],[100]) ).
thf(2877,plain,
( ( sk1 @ ( n0 @ leq ) )
| ~ $true
| ~ $true
| ( ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 ) ),
inference(rewrite,[status(thm)],[111,96,97]) ).
thf(2878,plain,
( ( sk1 @ ( n0 @ leq ) )
| ( ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 ) ),
inference(simp,[status(thm)],[2877]) ).
thf(2879,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) ) )
| ( sk1 @ ( n0 @ leq ) )
| ( n1 != n1 )
| ~ ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,2878]) ).
thf(2880,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) ) )
| ( sk1 @ ( n0 @ leq ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( A @ leq ) )
| ~ ( A @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[2879]) ).
thf(2881,plain,
( ( sk1 @ ( n0 @ leq ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[2880:[bind(A,$thf( sk3 )),bind(B,$thf( sk4 ))]]) ).
thf(4050,plain,
( ( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
!= ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) ) )
| ( sk1 @ ( n0 @ leq ) )
| ~ $true
| ~ ( sk3 @ ( n0 @ leq ) )
| ( sk1 @ ( n0 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[598,2881]) ).
thf(4051,plain,
( ( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
!= ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) ) )
| ~ ( sk3 @ ( n0 @ leq ) )
| ( sk1 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[4050]) ).
thf(4052,plain,
( ~ ( sk3 @ ( n0 @ leq ) )
| ( sk1 @ ( n0 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[4051:[]]) ).
thf(4315,plain,
( ( ( sk3 @ ( n0 @ leq ) )
!= ( sk3 @ ( n0 @ leq ) ) )
| ~ $true
| ( sk1 @ ( n0 @ leq ) )
| ( sk1 @ ( n0 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[592,4052]) ).
thf(4316,plain,
( ( ( sk3 @ ( n0 @ leq ) )
!= ( sk3 @ ( n0 @ leq ) ) )
| ( sk1 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[4315]) ).
thf(4317,plain,
sk1 @ ( n0 @ leq ),
inference(pattern_uni,[status(thm)],[4316:[]]) ).
thf(56,axiom,
! [A: $i] :
( ( ( n1 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n1 )
| ( A = n0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_1) ).
thf(416,plain,
! [A: $i] :
( ( ( n1 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n1 )
| ( A = n0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(35,axiom,
! [A: $i,B: $i] :
( ( B @ succ @ ( A @ succ @ leq ) )
<=> ( B @ ( A @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_succ_succ) ).
thf(216,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)],[35]) ).
thf(11440,plain,
! [A: $i] :
( ( ( n0 @ succ )
!= ( A @ succ ) )
| ( ( n1 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[162,137]) ).
thf(11441,plain,
( ( n1 @ pred )
= n0 ),
inference(pattern_uni,[status(thm)],[11440:[bind(A,$thf( n0 ))]]) ).
thf(6,axiom,
tptp_minus_1 @ ( n3 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_tptp_minus_1) ).
thf(121,plain,
tptp_minus_1 @ ( n3 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(104,plain,
( ( sk3 @ ( n0 @ leq ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[94]) ).
thf(999,plain,
( ( sk3 @ ( n0 @ leq ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[104,96,97]) ).
thf(1000,plain,
( ( sk3 @ ( n0 @ leq ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[999]) ).
thf(1018,plain,
( ~ $true
| ( ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
!= ( sk3 @ ( n0 @ leq ) ) )
| ( sk3 @ ( n0 @ leq ) ) ),
inference(eqfactor_ordered,[status(thm)],[1000]) ).
thf(1020,plain,
( ( ( n1 @ ( n0 @ minus ) )
!= sk3 )
| ( sk1 != n0 )
| ( sk3 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[1018]) ).
thf(11,axiom,
! [A: $i,B: $i] :
( ( A = B )
| ( A @ ( B @ gt ) )
| ( B @ ( A @ gt ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',totality) ).
thf(130,plain,
! [A: $i,B: $i] :
( ( A = B )
| ( A @ ( B @ gt ) )
| ( B @ ( A @ gt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(131,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( A @ ( B @ gt ) )
| ( B @ ( A @ gt ) ) ),
inference(cnf,[status(esa)],[130]) ).
thf(132,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ gt ) )
| ( B @ ( A @ gt ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[131]) ).
thf(13104,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[121,152]) ).
thf(13105,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n3 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13104]) ).
thf(13106,plain,
n3 @ ( tptp_minus_1 @ lt ),
inference(pattern_uni,[status(thm)],[13105:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n3 ))]]) ).
thf(12,axiom,
n2 @ ( n4 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_2) ).
thf(133,plain,
n2 @ ( n4 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(2910,plain,
( ( ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
!= ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) ) )
| ( sk3 != pv10 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[96,2526]) ).
thf(2911,plain,
( ( ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
!= ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) ) )
| ( sk3 != pv10 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ),
inference(simp,[status(thm)],[2910]) ).
thf(2975,plain,
( ( ( n1 @ ( n135300 @ minus ) )
!= ( n1 @ ( pv10 @ minus ) ) )
| ( sk3 != pv10 )
| ( sk3 != pv10 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ),
inference(simp,[status(thm)],[2911]) ).
thf(3001,plain,
( ( ( n1 @ ( n135300 @ minus ) )
!= ( n1 @ ( pv10 @ minus ) ) )
| ( sk3 != pv10 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ),
inference(simp,[status(thm)],[2975]) ).
thf(11185,plain,
! [A: $i] :
( ( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) ) )
| ( ( n1 @ ( n135300 @ minus ) )
!= ( n1 @ ( pv10 @ minus ) ) )
| ( sk3 != pv10 )
| ( ( n0 @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) )
!= ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[185,3001]) ).
thf(11238,plain,
! [A: $i] :
( ( A
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt ) )
| ( ( n1 @ ( n5 @ minus ) )
!= tptp_minus_1 )
| ( n0 != n0 )
| ( n1 != n1 )
| ( n135300 != pv10 )
| ( sk3 != pv10 )
| ( ( n0 @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) )
!= ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[11185]) ).
thf(11270,plain,
( ( ( n1 @ ( n5 @ minus ) )
!= tptp_minus_1 )
| ( n135300 != pv10 )
| ( sk3 != pv10 )
| ( ( n0 @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) )
!= ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[11238]) ).
thf(60,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(428,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)],[60]) ).
thf(66,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( D @ ( B @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( C @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) )
& ! [G: $i,H: $i] :
( ( ( D @ ( H @ leq ) )
& ( C @ ( G @ leq ) )
& ( H @ ( n0 @ leq ) )
& ( G @ ( n0 @ leq ) ) )
=> ( ( H @ ( G @ ( E @ a_select3 ) ) )
= F ) ) )
=> ( ( B @ ( A @ ( F @ ( D @ ( C @ ( E @ tptp_update3 ) ) ) @ a_select3 ) ) )
= F ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sel3_update_3) ).
thf(507,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( D @ ( B @ leq ) )
& ( B @ ( n0 @ leq ) )
& ( C @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) )
& ! [G: $i,H: $i] :
( ( ( D @ ( H @ leq ) )
& ( C @ ( G @ leq ) )
& ( H @ ( n0 @ leq ) )
& ( G @ ( n0 @ leq ) ) )
=> ( ( H @ ( G @ ( E @ a_select3 ) ) )
= F ) ) )
=> ( ( B @ ( A @ ( F @ ( D @ ( C @ ( E @ tptp_update3 ) ) ) @ a_select3 ) ) )
= F ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(71,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(527,plain,
! [A: $i] :
( ( ( n2 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(76,axiom,
! [A: $i] : ( A @ ( A @ leq ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_leq) ).
thf(546,plain,
! [A: $i] : ( A @ ( A @ leq ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(34,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(203,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)],[34]) ).
thf(204,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)],[203]) ).
thf(205,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 @ sk9 ) @ ( A @ ( B @ sk8 ) @ ( A @ a_select3 ) ) )
!= ( A @ ( B @ sk8 ) @ ( A @ ( B @ sk9 ) @ ( 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 @ sk9 ) @ 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 @ sk9 ) @ ( 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 @ sk8 ) @ 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 @ sk8 ) @ ( n0 @ leq ) ) ) ),
inference(cnf,[status(esa)],[204]) ).
thf(210,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 @ sk9 ) @ ( A @ ( B @ sk8 ) @ ( A @ a_select3 ) ) )
!= ( A @ ( B @ sk8 ) @ ( A @ ( B @ sk9 ) @ ( A @ a_select3 ) ) ) ) ),
inference(cnfConj,[status(thm)],[205]) ).
thf(215,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 @ sk8 ) @ ( A @ ( B @ sk9 ) @ ( A @ a_select3 ) ) )
!= ( A @ ( B @ sk9 ) @ ( A @ ( B @ sk8 ) @ ( A @ a_select3 ) ) ) ) ),
inference(lifteq,[status(thm)],[210]) ).
thf(742,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) )
!= ( sk4 @ ( sk3 @ ( q @ a_select3 ) ) ) )
| ( ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( B @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ~ ( B @ ( D @ leq ) )
| ~ ( D @ ( n0 @ leq ) )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ( ( A @ ( B @ sk8 ) @ ( A @ ( B @ sk9 ) @ ( A @ a_select3 ) ) )
!= ( A @ ( B @ sk9 ) @ ( A @ ( B @ sk8 ) @ ( A @ a_select3 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[215,607]) ).
thf(787,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D != sk4 )
| ( C != sk3 )
| ( ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( C @ ( D @ ( F @ ( E @ ( E @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( B @ ( E @ leq ) )
| ~ ( E @ ( n0 @ leq ) )
| ~ ( B @ ( D @ leq ) )
| ~ ( D @ ( n0 @ leq ) )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ( ( A @ ( B @ sk9 ) )
!= ( A @ ( B @ sk8 ) ) )
| ( ( A @ ( B @ sk9 ) )
!= ( A @ ( B @ sk8 ) ) )
| ( A != A ) ),
inference(simp,[status(thm)],[742]) ).
thf(872,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( C @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( sk3 @ ( sk4 @ ( D @ ( C @ ( C @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( n0 @ leq ) )
| ~ ( B @ ( sk4 @ leq ) )
| ~ ( sk4 @ ( n0 @ leq ) )
| ~ ( B @ ( sk3 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) )
| ( ( A @ ( B @ sk9 ) )
!= ( A @ ( B @ sk8 ) ) ) ),
inference(simp,[status(thm)],[787]) ).
thf(1178,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( B @ ( C @ leq ) )
!= ( C @ ( n0 @ leq ) ) )
| ( ( D @ ( C @ ( C @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( sk3 @ ( sk4 @ ( D @ ( C @ ( C @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( C @ ( n0 @ leq ) )
| ~ ( B @ ( sk4 @ leq ) )
| ~ ( sk4 @ ( n0 @ leq ) )
| ~ ( B @ ( sk3 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) )
| ( ( A @ ( B @ sk9 ) )
!= ( A @ ( B @ sk8 ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[872]) ).
thf(1180,plain,
! [B: $i,A: $i] :
( ( ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( sk3 @ ( sk4 @ ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n0 @ ( n0 @ leq ) )
| ~ ( n0 @ ( sk4 @ leq ) )
| ~ ( sk4 @ ( n0 @ leq ) )
| ~ ( n0 @ ( sk3 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) )
| ( ( A @ ( n0 @ sk9 ) )
!= ( A @ ( n0 @ sk8 ) ) ) ),
inference(pattern_uni,[status(thm)],[1178:[bind(A,$thf( A )),bind(B,$thf( n0 )),bind(C,$thf( n0 ))]]) ).
thf(1248,plain,
! [B: $i,A: $i] :
( ( ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( sk3 @ ( sk4 @ ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n0 @ ( n0 @ leq ) )
| ~ ( n0 @ ( sk4 @ leq ) )
| ~ ( sk4 @ ( n0 @ leq ) )
| ~ ( n0 @ ( sk3 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) )
| ( ( A @ ( n0 @ sk9 ) )
!= ( A @ ( n0 @ sk8 ) ) ) ),
inference(simp,[status(thm)],[1180]) ).
thf(1322,plain,
! [B: $i,A: $i] :
( ( ( pv10 @ ( n0 @ leq ) )
!= ( n0 @ ( n0 @ leq ) ) )
| ( ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( sk3 @ ( sk4 @ ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ $true
| ~ ( n0 @ ( sk4 @ leq ) )
| ~ ( sk4 @ ( n0 @ leq ) )
| ~ ( n0 @ ( sk3 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) )
| ( ( A @ ( n0 @ sk9 ) )
!= ( A @ ( n0 @ sk8 ) ) ) ),
inference(paramod_ordered,[status(thm)],[97,1248]) ).
thf(1323,plain,
! [B: $i,A: $i] :
( ( ( pv10 @ ( n0 @ leq ) )
!= ( n0 @ ( n0 @ leq ) ) )
| ( ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( sk3 @ ( sk4 @ ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n0 @ ( sk4 @ leq ) )
| ~ ( sk4 @ ( n0 @ leq ) )
| ~ ( n0 @ ( sk3 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) )
| ( ( A @ ( n0 @ sk9 ) )
!= ( A @ ( n0 @ sk8 ) ) ) ),
inference(simp,[status(thm)],[1322]) ).
thf(1410,plain,
! [B: $i,A: $i] :
( ( pv10 != n0 )
| ( n0 != n0 )
| ( ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( sk3 @ ( sk4 @ ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n0 @ ( sk4 @ leq ) )
| ~ ( sk4 @ ( n0 @ leq ) )
| ~ ( n0 @ ( sk3 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) )
| ( ( A @ ( n0 @ sk9 ) )
!= ( A @ ( n0 @ sk8 ) ) ) ),
inference(simp,[status(thm)],[1323]) ).
thf(1474,plain,
! [B: $i,A: $i] :
( ( pv10 != n0 )
| ( ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( sk3 @ ( sk4 @ ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n0 @ ( sk4 @ leq ) )
| ~ ( sk4 @ ( n0 @ leq ) )
| ~ ( n0 @ ( sk3 @ leq ) )
| ~ ( sk3 @ ( n0 @ leq ) )
| ( ( A @ ( n0 @ sk9 ) )
!= ( A @ ( n0 @ sk8 ) ) ) ),
inference(simp,[status(thm)],[1410]) ).
thf(1616,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( n0 @ leq ) )
!= ( pv10 @ ( n0 @ leq ) ) )
| ( pv10 != n0 )
| ( ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( sk3 @ ( sk4 @ ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n0 @ ( sk4 @ leq ) )
| ~ ( sk4 @ ( n0 @ leq ) )
| ~ ( n0 @ ( sk3 @ leq ) )
| ~ $true
| ( ( A @ ( n0 @ sk9 ) )
!= ( A @ ( n0 @ sk8 ) ) ) ),
inference(paramod_ordered,[status(thm)],[97,1474]) ).
thf(1617,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( n0 @ leq ) )
!= ( pv10 @ ( n0 @ leq ) ) )
| ( pv10 != n0 )
| ( ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( sk3 @ ( sk4 @ ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n0 @ ( sk4 @ leq ) )
| ~ ( sk4 @ ( n0 @ leq ) )
| ~ ( n0 @ ( sk3 @ leq ) )
| ( ( A @ ( n0 @ sk9 ) )
!= ( A @ ( n0 @ sk8 ) ) ) ),
inference(simp,[status(thm)],[1616]) ).
thf(1710,plain,
! [B: $i,A: $i] :
( ( sk3 != pv10 )
| ( n0 != n0 )
| ( pv10 != n0 )
| ( ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( sk3 @ ( sk4 @ ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n0 @ ( sk4 @ leq ) )
| ~ ( sk4 @ ( n0 @ leq ) )
| ~ ( n0 @ ( sk3 @ leq ) )
| ( ( A @ ( n0 @ sk9 ) )
!= ( A @ ( n0 @ sk8 ) ) ) ),
inference(simp,[status(thm)],[1617]) ).
thf(1768,plain,
! [B: $i,A: $i] :
( ( sk3 != pv10 )
| ( pv10 != n0 )
| ( ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( sk3 @ ( sk4 @ ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n0 @ ( sk4 @ leq ) )
| ~ ( sk4 @ ( n0 @ leq ) )
| ~ ( n0 @ ( sk3 @ leq ) )
| ( ( A @ ( n0 @ sk9 ) )
!= ( A @ ( n0 @ sk8 ) ) ) ),
inference(simp,[status(thm)],[1710]) ).
thf(13107,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n135300 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[353,152]) ).
thf(13108,plain,
! [B: $i,A: $i] :
( ( ( n1 @ ( n135300 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13107]) ).
thf(13109,plain,
n135300 @ ( n1 @ lt ),
inference(pattern_uni,[status(thm)],[13108:[bind(A,$thf( n1 )),bind(B,$thf( n135300 ))]]) ).
thf(23,axiom,
n2 @ ( n135300 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_135300_2) ).
thf(160,plain,
n2 @ ( n135300 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(83,axiom,
n0 @ ( n1 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_1_0) ).
thf(561,plain,
n0 @ ( n1 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(629,plain,
( ~ $true
| ( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
!= ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(eqfactor_ordered,[status(thm)],[626]) ).
thf(630,plain,
( ( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
!= ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[629]) ).
thf(26,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(165,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ ( B @ ( A @ tptp_update2 ) ) @ a_select2 ) )
= C ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(13092,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n135300 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[340,152]) ).
thf(13093,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n135300 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13092]) ).
thf(13094,plain,
n135300 @ ( tptp_minus_1 @ lt ),
inference(pattern_uni,[status(thm)],[13093:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n135300 ))]]) ).
thf(62,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(484,plain,
! [A: $i,B: $i] :
( ( A @ ( n0 @ leq ) )
=> ( A @ ( A @ ( B @ uniform_int_rnd ) @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(68,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
=> ( B @ succ @ ( A @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_succ) ).
thf(522,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
=> ( B @ succ @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(3376,plain,
( ( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
!= ( sk1 @ ( n0 @ leq ) ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ $true
| ( sk3 != sk1 )
| ( sk3 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[596,2531]) ).
thf(3377,plain,
( ( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
!= ( sk1 @ ( n0 @ leq ) ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[3376]) ).
thf(3408,plain,
( ( ( n1 @ ( pv10 @ minus ) )
!= sk1 )
| ( sk3 != n0 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[3377]) ).
thf(67,axiom,
! [A: $i] :
( ( n1 @ ( A @ plus ) )
= ( A @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_1_r) ).
thf(519,plain,
! [A: $i] :
( ( n1 @ ( A @ plus ) )
= ( A @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(21,axiom,
! [A: $i] :
( ( A @ ( n4 @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_4_l) ).
thf(156,plain,
! [A: $i] :
( ( A @ ( n4 @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(28,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(169,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)],[28]) ).
thf(58,axiom,
! [A: $i] :
( ( n5 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_5_r) ).
thf(420,plain,
! [A: $i] :
( ( n5 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(64,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
<=> ( A @ ( B @ succ @ gt ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_succ_gt_equiv) ).
thf(499,plain,
! [A: $i,B: $i] :
( ( ( A @ ( B @ succ @ gt ) )
=> ( B @ ( A @ leq ) ) )
& ( ( B @ ( A @ leq ) )
=> ( A @ ( B @ succ @ gt ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(7,axiom,
! [A: $i] :
( ( n2 @ ( A @ plus ) )
= ( A @ succ @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_2_r) ).
thf(122,plain,
! [A: $i] :
( ( n2 @ ( A @ plus ) )
= ( A @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(123,plain,
! [A: $i] :
( ( n2 @ ( A @ plus ) )
= ( A @ succ @ succ ) ),
inference(cnf,[status(esa)],[122]) ).
thf(124,plain,
! [A: $i] :
( ( n2 @ ( A @ plus ) )
= ( A @ succ @ succ ) ),
inference(lifteq,[status(thm)],[123]) ).
thf(70,axiom,
tptp_minus_1 @ ( n1 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_1_tptp_minus_1) ).
thf(526,plain,
tptp_minus_1 @ ( n1 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(587,plain,
! [A: $i] :
( ( ( n2 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[133,143]) ).
thf(588,plain,
! [A: $i] :
( ( n2 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[587]) ).
thf(589,plain,
! [A: $i] :
( ( n2 != A )
| ( n4 != A ) ),
inference(simp,[status(thm)],[588]) ).
thf(590,plain,
n4 != n2,
inference(simp,[status(thm)],[589]) ).
thf(547,plain,
! [A: $i] : ( A @ ( A @ leq ) ),
inference(cnf,[status(esa)],[546]) ).
thf(2904,plain,
( ( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
!= ( pv10 @ ( n0 @ leq ) ) )
| ( sk3 != pv10 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[97,2526]) ).
thf(2905,plain,
( ( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
!= ( pv10 @ ( n0 @ leq ) ) )
| ( sk3 != pv10 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ),
inference(simp,[status(thm)],[2904]) ).
thf(2968,plain,
( ( ( n1 @ ( pv10 @ minus ) )
!= pv10 )
| ( sk3 != n0 )
| ( sk3 != pv10 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ),
inference(simp,[status(thm)],[2905]) ).
thf(3351,plain,
! [A: $i] :
( ( ( n0 @ ( n1 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[561,143]) ).
thf(3352,plain,
! [A: $i] :
( ( n0 @ ( n1 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[3351]) ).
thf(3353,plain,
! [A: $i] :
( ( n0 != A )
| ( n1 != A ) ),
inference(simp,[status(thm)],[3352]) ).
thf(3354,plain,
n1 != n0,
inference(simp,[status(thm)],[3353]) ).
thf(10,axiom,
tptp_minus_1 @ ( n2 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_2_tptp_minus_1) ).
thf(129,plain,
tptp_minus_1 @ ( n2 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(11187,plain,
! [A: $i] :
( ( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) ) )
| ( ( n0 @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) )
!= ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( sk3 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[185,2531]) ).
thf(11229,plain,
! [A: $i] :
( ( A
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt ) )
| ( ( n1 @ ( n5 @ minus ) )
!= tptp_minus_1 )
| ( n0 != n0 )
| ( ( n0 @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) )
!= ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[11187]) ).
thf(11261,plain,
( ( ( n1 @ ( n5 @ minus ) )
!= tptp_minus_1 )
| ( ( n0 @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) )
!= ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) ) )
| ~ ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[11229]) ).
thf(13,axiom,
n3 @ ( n4 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_3) ).
thf(134,plain,
n3 @ ( n4 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(602,plain,
! [A: $i] :
( ( ( n3 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[134,143]) ).
thf(603,plain,
! [A: $i] :
( ( n3 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[602]) ).
thf(604,plain,
! [A: $i] :
( ( n3 != A )
| ( n4 != A ) ),
inference(simp,[status(thm)],[603]) ).
thf(605,plain,
n4 != n3,
inference(simp,[status(thm)],[604]) ).
thf(9,axiom,
n2 @ ( n3 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_2) ).
thf(128,plain,
n2 @ ( n3 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(13101,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[542,152]) ).
thf(13102,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n5 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13101]) ).
thf(13103,plain,
n5 @ ( tptp_minus_1 @ lt ),
inference(pattern_uni,[status(thm)],[13102:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n5 ))]]) ).
thf(82,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(558,plain,
! [A: $i] :
( ( ( n4 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( ( A = n4 )
| ( A = n3 )
| ( A = n2 )
| ( A = n1 )
| ( A = n0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(72,axiom,
! [A: $i,B: $i] :
( ! [C: $i,D: $i] :
( ( ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( A @ a_select3 ) ) )
= ( C @ ( D @ ( A @ a_select3 ) ) ) ) )
=> ! [C: $i,D: $i] :
( ( ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( A @ inv @ a_select3 ) ) )
= ( C @ ( D @ ( A @ inv @ a_select3 ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',matrix_symm_inv) ).
thf(530,plain,
! [A: $i,B: $i] :
( ! [C: $i,D: $i] :
( ( ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( A @ a_select3 ) ) )
= ( C @ ( D @ ( A @ a_select3 ) ) ) ) )
=> ! [C: $i,D: $i] :
( ( ( B @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) )
& ( B @ ( C @ leq ) )
& ( C @ ( n0 @ leq ) ) )
=> ( ( D @ ( C @ ( A @ inv @ a_select3 ) ) )
= ( C @ ( D @ ( A @ inv @ a_select3 ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(579,plain,
! [A: $i] :
( ( ( n2 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[128,143]) ).
thf(580,plain,
! [A: $i] :
( ( n2 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[579]) ).
thf(583,plain,
! [A: $i] :
( ( n2 != A )
| ( n3 != A ) ),
inference(simp,[status(thm)],[580]) ).
thf(586,plain,
n2 != n3,
inference(simp,[status(thm)],[583]) ).
thf(90,axiom,
n4 @ ( n135300 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_135300_4) ).
thf(572,plain,
n4 @ ( n135300 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).
thf(3683,plain,
! [A: $i] :
( ( ( n4 @ ( n135300 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[572,143]) ).
thf(3684,plain,
! [A: $i] :
( ( n4 @ ( n135300 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[3683]) ).
thf(3685,plain,
! [A: $i] :
( ( n4 != A )
| ( n135300 != A ) ),
inference(simp,[status(thm)],[3684]) ).
thf(3686,plain,
n4 != n135300,
inference(simp,[status(thm)],[3685]) ).
thf(575,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[121,143]) ).
thf(576,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[575]) ).
thf(581,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n3 != A ) ),
inference(simp,[status(thm)],[576]) ).
thf(584,plain,
tptp_minus_1 != n3,
inference(simp,[status(thm)],[581]) ).
thf(59,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(423,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)],[59]) ).
thf(42,axiom,
n0 @ ( n135300 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_135300_0) ).
thf(330,plain,
n0 @ ( n135300 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(1612,plain,
! [A: $i] :
( ( ( n0 @ ( n135300 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[330,143]) ).
thf(1613,plain,
! [A: $i] :
( ( n0 @ ( n135300 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1612]) ).
thf(1614,plain,
! [A: $i] :
( ( n0 != A )
| ( n135300 != A ) ),
inference(simp,[status(thm)],[1613]) ).
thf(1615,plain,
n135300 != n0,
inference(simp,[status(thm)],[1614]) ).
thf(89,axiom,
n1 @ ( n5 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_1) ).
thf(571,plain,
n1 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(3606,plain,
! [A: $i] :
( ( ( n1 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[571,143]) ).
thf(3607,plain,
! [A: $i] :
( ( n1 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[3606]) ).
thf(3608,plain,
! [A: $i] :
( ( n1 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[3607]) ).
thf(3609,plain,
n5 != n1,
inference(simp,[status(thm)],[3608]) ).
thf(36,axiom,
n3 @ ( n5 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_3) ).
thf(222,plain,
n3 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(1517,plain,
! [A: $i] :
( ( ( n3 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[222,143]) ).
thf(1518,plain,
! [A: $i] :
( ( n3 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1517]) ).
thf(1519,plain,
! [A: $i] :
( ( n3 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[1518]) ).
thf(1520,plain,
n3 != n5,
inference(simp,[status(thm)],[1519]) ).
thf(75,axiom,
n0 @ ( n2 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_2_0) ).
thf(545,plain,
n0 @ ( n2 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(608,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[153,143]) ).
thf(609,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[608]) ).
thf(610,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n4 != A ) ),
inference(simp,[status(thm)],[609]) ).
thf(611,plain,
n4 != tptp_minus_1,
inference(simp,[status(thm)],[610]) ).
thf(39,axiom,
! [A: $i] :
( ( n1 @ ( A @ minus ) )
= ( A @ pred ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',pred_minus_1) ).
thf(236,plain,
! [A: $i] :
( ( n1 @ ( A @ minus ) )
= ( A @ pred ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(22,axiom,
n1 @ ( n3 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_1) ).
thf(159,plain,
n1 @ ( n3 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(13098,plain,
! [B: $i,A: $i] :
( ( ( n5 @ ( n135300 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[570,152]) ).
thf(13099,plain,
! [B: $i,A: $i] :
( ( ( n5 @ ( n135300 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13098]) ).
thf(13100,plain,
n135300 @ ( n5 @ lt ),
inference(pattern_uni,[status(thm)],[13099:[bind(A,$thf( n5 )),bind(B,$thf( n135300 ))]]) ).
thf(86,axiom,
n1 @ ( n2 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_2_1) ).
thf(567,plain,
n1 @ ( n2 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(2740,plain,
( ( ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
!= ( sk3 @ ( n0 @ leq ) ) )
| ~ $true
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[96,2576]) ).
thf(2741,plain,
( ( ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
!= ( sk3 @ ( n0 @ leq ) ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[2740]) ).
thf(2839,plain,
( ( ( n1 @ ( n135300 @ minus ) )
!= sk3 )
| ( pv10 != n0 )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[2741]) ).
thf(5855,plain,
! [B: $i,A: $i] :
( ( A != sk3 )
| ( B != pv10 )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ( A @ ( B @ gt ) )
| ( B @ ( A @ gt ) ) ),
inference(paramod_ordered,[status(thm)],[132,2857]) ).
thf(5856,plain,
! [A: $i] :
( ( A != pv10 )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ( sk3 @ ( A @ gt ) )
| ( A @ ( sk3 @ gt ) ) ),
inference(pattern_uni,[status(thm)],[5855:[bind(A,$thf( sk3 ))]]) ).
thf(10265,plain,
( ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
| ( sk3 @ ( pv10 @ gt ) )
| ( pv10 @ ( sk3 @ gt ) ) ),
inference(simp,[status(thm)],[5856]) ).
thf(20,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(154,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ gt ) )
& ( B @ ( A @ gt ) ) )
=> ( C @ ( A @ gt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(155,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ gt ) )
| ~ ( C @ ( B @ gt ) )
| ~ ( B @ ( A @ gt ) ) ),
inference(cnf,[status(esa)],[154]) ).
thf(79,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(552,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)],[79]) ).
thf(37,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(223,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)],[37]) ).
thf(2532,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n1 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[526,143]) ).
thf(2533,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n1 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2532]) ).
thf(2534,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n1 != A ) ),
inference(simp,[status(thm)],[2533]) ).
thf(2535,plain,
tptp_minus_1 != n1,
inference(simp,[status(thm)],[2534]) ).
thf(12268,plain,
! [A: $i] :
( ( ( A @ ( A @ leq ) )
!= ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) ) )
| ( ( n1 @ ( n5 @ minus ) )
!= tptp_minus_1 )
| ( sk3 != pv10 )
| ( ( n0 @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) )
!= ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[547,11256]) ).
thf(12269,plain,
! [A: $i] :
( ( ( A @ ( A @ leq ) )
!= ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) ) )
| ( ( n1 @ ( n5 @ minus ) )
!= tptp_minus_1 )
| ( sk3 != pv10 )
| ( ( n0 @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) )
!= ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[12268]) ).
thf(12295,plain,
! [A: $i] :
( ( A
!= ( n1 @ ( pv10 @ minus ) ) )
| ( A != sk3 )
| ( ( n1 @ ( n5 @ minus ) )
!= tptp_minus_1 )
| ( sk3 != pv10 )
| ( ( n0 @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) )
!= ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[12269]) ).
thf(12326,plain,
( ( ( n1 @ ( pv10 @ minus ) )
!= sk3 )
| ( ( n1 @ ( n5 @ minus ) )
!= tptp_minus_1 )
| ( sk3 != pv10 )
| ( ( n0 @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) )
!= ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) ) ) ),
inference(simp,[status(thm)],[12295]) ).
thf(77,axiom,
! [A: $i] :
( ( A @ ( n1 @ plus ) )
= ( A @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_1_l) ).
thf(548,plain,
! [A: $i] :
( ( A @ ( n1 @ plus ) )
= ( A @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(63,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(487,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)],[63]) ).
thf(47,axiom,
! [A: $i] :
( ( A @ ( n5 @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_5_l) ).
thf(342,plain,
! [A: $i] :
( ( A @ ( n5 @ plus ) )
= ( A @ succ @ succ @ succ @ succ @ succ ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(2896,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[542,143]) ).
thf(2897,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2896]) ).
thf(2898,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[2897]) ).
thf(2899,plain,
tptp_minus_1 != n5,
inference(simp,[status(thm)],[2898]) ).
thf(29,axiom,
n1 @ ( n4 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_1) ).
thf(177,plain,
n1 @ ( n4 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(1046,plain,
! [A: $i] :
( ( ( n1 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[177,143]) ).
thf(1047,plain,
! [A: $i] :
( ( n1 @ ( n4 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1046]) ).
thf(1048,plain,
! [A: $i] :
( ( n1 != A )
| ( n4 != A ) ),
inference(simp,[status(thm)],[1047]) ).
thf(1049,plain,
n4 != n1,
inference(simp,[status(thm)],[1048]) ).
thf(38,axiom,
tptp_minus_1 @ ( n0 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_0_tptp_minus_1) ).
thf(235,plain,
tptp_minus_1 @ ( n0 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(1608,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n0 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[235,143]) ).
thf(1609,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n0 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1608]) ).
thf(1610,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[1609]) ).
thf(1611,plain,
tptp_minus_1 != n0,
inference(simp,[status(thm)],[1610]) ).
thf(150,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ gt ) )
| ~ ( B @ ( A @ lt ) ) ),
inference(cnfConj,[status(thm)],[149]) ).
thf(13119,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n135300 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[160,152]) ).
thf(13120,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n135300 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13119]) ).
thf(13121,plain,
n135300 @ ( n2 @ lt ),
inference(pattern_uni,[status(thm)],[13120:[bind(A,$thf( n2 )),bind(B,$thf( n135300 ))]]) ).
thf(53,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(409,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)],[53]) ).
thf(11442,plain,
! [A: $i] :
( ( ( n4 @ succ )
!= ( A @ succ ) )
| ( ( n5 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[4217,137]) ).
thf(11443,plain,
( ( n5 @ pred )
= n4 ),
inference(pattern_uni,[status(thm)],[11442:[bind(A,$thf( n4 ))]]) ).
thf(99,plain,
( ( sk3 @ ( n0 @ leq ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[94]) ).
thf(112,plain,
( ( sk3 @ ( n0 @ leq ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ),
inference(lifteq,[status(thm)],[99]) ).
thf(3272,plain,
( ( sk3 @ ( n0 @ leq ) )
| ~ $true
| ~ $true
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ),
inference(rewrite,[status(thm)],[112,96,97]) ).
thf(3273,plain,
( ( sk3 @ ( n0 @ leq ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ),
inference(simp,[status(thm)],[3272]) ).
thf(43,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ geq ) )
<=> ( A @ ( B @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_geq) ).
thf(331,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)],[43]) ).
thf(577,plain,
! [A: $i] :
( ( ( tptp_minus_1 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[129,143]) ).
thf(578,plain,
! [A: $i] :
( ( tptp_minus_1 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[577]) ).
thf(582,plain,
! [A: $i] :
( ( tptp_minus_1 != A )
| ( n2 != A ) ),
inference(simp,[status(thm)],[578]) ).
thf(585,plain,
n2 != tptp_minus_1,
inference(simp,[status(thm)],[582]) ).
thf(126,plain,
! [A: $i] :
( ( n3 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(cnf,[status(esa)],[125]) ).
thf(127,plain,
! [A: $i] :
( ( n3 @ ( A @ plus ) )
= ( A @ succ @ succ @ succ ) ),
inference(lifteq,[status(thm)],[126]) ).
thf(2900,plain,
! [A: $i] :
( ( ( n0 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[545,143]) ).
thf(2901,plain,
! [A: $i] :
( ( n0 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2900]) ).
thf(2902,plain,
! [A: $i] :
( ( n0 != A )
| ( n2 != A ) ),
inference(simp,[status(thm)],[2901]) ).
thf(2903,plain,
n2 != n0,
inference(simp,[status(thm)],[2902]) ).
thf(1918,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( sk3 @ leq ) )
!= ( pv10 @ ( n0 @ leq ) ) )
| ( sk3 != pv10 )
| ( pv10 != n0 )
| ( ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( sk3 @ ( sk4 @ ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n0 @ ( sk4 @ leq ) )
| ~ ( sk4 @ ( n0 @ leq ) )
| ~ $true
| ( ( A @ ( n0 @ sk9 ) )
!= ( A @ ( n0 @ sk8 ) ) ) ),
inference(paramod_ordered,[status(thm)],[97,1768]) ).
thf(1919,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( sk3 @ leq ) )
!= ( pv10 @ ( n0 @ leq ) ) )
| ( sk3 != pv10 )
| ( pv10 != n0 )
| ( ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( sk3 @ ( sk4 @ ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n0 @ ( sk4 @ leq ) )
| ~ ( sk4 @ ( n0 @ leq ) )
| ( ( A @ ( n0 @ sk9 ) )
!= ( A @ ( n0 @ sk8 ) ) ) ),
inference(simp,[status(thm)],[1918]) ).
thf(1987,plain,
! [B: $i,A: $i] :
( ( pv10 != n0 )
| ( sk3 != n0 )
| ( sk3 != pv10 )
| ( pv10 != n0 )
| ( ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( sk3 @ ( sk4 @ ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n0 @ ( sk4 @ leq ) )
| ~ ( sk4 @ ( n0 @ leq ) )
| ( ( A @ ( n0 @ sk9 ) )
!= ( A @ ( n0 @ sk8 ) ) ) ),
inference(simp,[status(thm)],[1919]) ).
thf(2045,plain,
! [B: $i,A: $i] :
( ( sk3 != n0 )
| ( sk3 != pv10 )
| ( pv10 != n0 )
| ( ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) )
!= q )
| ( ( sk3 @ ( sk4 @ ( B @ ( n0 @ ( n0 @ ( A @ tptp_update3 ) ) ) @ a_select3 ) ) @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) )
!= n1 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n0 @ ( sk4 @ leq ) )
| ~ ( sk4 @ ( n0 @ leq ) )
| ( ( A @ ( n0 @ sk9 ) )
!= ( A @ ( n0 @ sk8 ) ) ) ),
inference(simp,[status(thm)],[1987]) ).
thf(46,axiom,
n0 @ ( n5 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_0) ).
thf(341,plain,
n0 @ ( n5 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(1910,plain,
! [A: $i] :
( ( ( n0 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[341,143]) ).
thf(1911,plain,
! [A: $i] :
( ( n0 @ ( n5 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1910]) ).
thf(1912,plain,
! [A: $i] :
( ( n0 != A )
| ( n5 != A ) ),
inference(simp,[status(thm)],[1911]) ).
thf(1913,plain,
n5 != n0,
inference(simp,[status(thm)],[1912]) ).
thf(69,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ ( A @ minus ) @ leq ) )
=> ( B @ ( n0 @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_minus) ).
thf(524,plain,
! [A: $i,B: $i] :
( ( A @ ( B @ ( A @ minus ) @ leq ) )
=> ( B @ ( n0 @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(157,plain,
! [A: $i] :
( ( A @ ( n4 @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
inference(cnf,[status(esa)],[156]) ).
thf(158,plain,
! [A: $i] :
( ( A @ ( n4 @ plus ) )
= ( A @ succ @ succ @ succ @ succ ) ),
inference(lifteq,[status(thm)],[157]) ).
thf(32,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(186,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)],[32]) ).
thf(13095,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[153,152]) ).
thf(13096,plain,
! [B: $i,A: $i] :
( ( ( tptp_minus_1 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13095]) ).
thf(13097,plain,
n4 @ ( tptp_minus_1 @ lt ),
inference(pattern_uni,[status(thm)],[13096:[bind(A,$thf( tptp_minus_1 )),bind(B,$thf( n4 ))]]) ).
thf(87,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ gt ) )
=> ( B @ ( A @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_gt1) ).
thf(568,plain,
! [A: $i,B: $i] :
( ( A @ ( B @ gt ) )
=> ( B @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(55,axiom,
n0 @ ( n3 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_0) ).
thf(415,plain,
n0 @ ( n3 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(2396,plain,
! [A: $i] :
( ( ( n0 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[415,143]) ).
thf(2397,plain,
! [A: $i] :
( ( n0 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[2396]) ).
thf(2398,plain,
! [A: $i] :
( ( n0 != A )
| ( n3 != A ) ),
inference(simp,[status(thm)],[2397]) ).
thf(2399,plain,
n3 != n0,
inference(simp,[status(thm)],[2398]) ).
thf(3757,plain,
( ( n1 != n1 )
| ( n135300 != pv10 )
| ( sk3 != pv10 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ),
inference(simp,[status(thm)],[3001]) ).
thf(3844,plain,
( ( n135300 != pv10 )
| ( sk3 != pv10 )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ),
inference(simp,[status(thm)],[3757]) ).
thf(27,axiom,
n3 @ ( n135300 @ gt ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_135300_3) ).
thf(168,plain,
n3 @ ( n135300 @ gt ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(1042,plain,
! [A: $i] :
( ( ( n3 @ ( n135300 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[168,143]) ).
thf(1043,plain,
! [A: $i] :
( ( n3 @ ( n135300 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[1042]) ).
thf(1044,plain,
! [A: $i] :
( ( n3 != A )
| ( n135300 != A ) ),
inference(simp,[status(thm)],[1043]) ).
thf(1045,plain,
n3 != n135300,
inference(simp,[status(thm)],[1044]) ).
thf(11343,plain,
! [A: $i] :
( ( ( A @ ( A @ leq ) )
!= ( sk3 @ ( n0 @ leq ) ) )
| ~ $true
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[547,2576]) ).
thf(11344,plain,
! [A: $i] :
( ( ( A @ ( A @ leq ) )
!= ( sk3 @ ( n0 @ leq ) ) )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[11343]) ).
thf(11377,plain,
! [A: $i] :
( ( A != sk3 )
| ( A != n0 )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[11344]) ).
thf(11405,plain,
( ( sk3 != n0 )
| ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[11377]) ).
thf(13122,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n1 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[561,152]) ).
thf(13123,plain,
! [B: $i,A: $i] :
( ( ( n0 @ ( n1 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13122]) ).
thf(13124,plain,
n1 @ ( n0 @ lt ),
inference(pattern_uni,[status(thm)],[13123:[bind(A,$thf( n0 )),bind(B,$thf( n1 ))]]) ).
thf(61,axiom,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( B @ a_select3 ) ) )
= ( D @ ( E @ ( B @ a_select3 ) ) ) ) )
& ! [D: $i,E: $i] :
( ( ( C @ ( E @ leq ) )
& ( E @ ( n0 @ leq ) )
& ( C @ ( D @ leq ) )
& ( D @ ( n0 @ leq ) ) )
=> ( ( E @ ( D @ ( A @ 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(432,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)],[61]) ).
thf(11436,plain,
! [A: $i] :
( ( ( n1 @ succ )
!= ( A @ succ ) )
| ( ( n2 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[3695,137]) ).
thf(11437,plain,
( ( n2 @ pred )
= n1 ),
inference(pattern_uni,[status(thm)],[11436:[bind(A,$thf( n1 ))]]) ).
thf(33,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(190,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)],[33]) ).
thf(3466,plain,
! [A: $i] :
( ( ( n1 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[567,143]) ).
thf(3467,plain,
! [A: $i] :
( ( n1 @ ( n2 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[3466]) ).
thf(3468,plain,
! [A: $i] :
( ( n1 != A )
| ( n2 != A ) ),
inference(simp,[status(thm)],[3467]) ).
thf(3469,plain,
n2 != n1,
inference(simp,[status(thm)],[3468]) ).
thf(13116,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[133,152]) ).
thf(13117,plain,
! [B: $i,A: $i] :
( ( ( n2 @ ( n4 @ gt ) )
!= ( A @ ( B @ gt ) ) )
| ( B @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[13116]) ).
thf(13118,plain,
n4 @ ( n2 @ lt ),
inference(pattern_uni,[status(thm)],[13117:[bind(A,$thf( n2 )),bind(B,$thf( n4 ))]]) ).
thf(11446,plain,
! [A: $i] :
( ( ( n2 @ succ )
!= ( A @ succ ) )
| ( ( n3 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[3716,137]) ).
thf(11447,plain,
( ( n3 @ pred )
= n2 ),
inference(pattern_uni,[status(thm)],[11446:[bind(A,$thf( n2 ))]]) ).
thf(85,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(564,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)],[85]) ).
thf(11414,plain,
! [A: $i] :
( ( ( n3 @ succ )
!= ( A @ succ ) )
| ( ( n4 @ pred )
= A ) ),
inference(paramod_ordered,[status(thm)],[3994,137]) ).
thf(11415,plain,
( ( n4 @ pred )
= n3 ),
inference(pattern_uni,[status(thm)],[11414:[bind(A,$thf( n3 ))]]) ).
thf(632,plain,
! [A: $i] :
( ( ( n1 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[159,143]) ).
thf(633,plain,
! [A: $i] :
( ( n1 @ ( n3 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[632]) ).
thf(634,plain,
! [A: $i] :
( ( n1 != A )
| ( n3 != A ) ),
inference(simp,[status(thm)],[633]) ).
thf(635,plain,
n3 != n1,
inference(simp,[status(thm)],[634]) ).
thf(40,axiom,
! [A: $i] :
( ( ( n0 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( A = n0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_0) ).
thf(239,plain,
! [A: $i] :
( ( ( n0 @ ( A @ leq ) )
& ( A @ ( n0 @ leq ) ) )
=> ( A = n0 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(41,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(242,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)],[41]) ).
thf(1019,plain,
( ( ( n1 @ ( n0 @ minus ) @ ( sk1 @ leq ) )
!= ( sk3 @ ( n0 @ leq ) ) )
| ( sk3 @ ( n0 @ leq ) ) ),
inference(simp,[status(thm)],[1018]) ).
thf(30,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(178,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)],[30]) ).
thf(3602,plain,
! [A: $i] :
( ( ( n5 @ ( n135300 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[570,143]) ).
thf(3603,plain,
! [A: $i] :
( ( n5 @ ( n135300 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[3602]) ).
thf(3604,plain,
! [A: $i] :
( ( n5 != A )
| ( n135300 != A ) ),
inference(simp,[status(thm)],[3603]) ).
thf(3605,plain,
n5 != n135300,
inference(simp,[status(thm)],[3604]) ).
thf(101,plain,
( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) ) ),
inference(cnfConj,[status(thm)],[94]) ).
thf(107,plain,
( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ~ ( n1 @ ( n135300 @ minus ) @ ( pv10 @ leq ) )
| ~ ( pv10 @ ( n0 @ leq ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ),
inference(lifteq,[status(thm)],[101]) ).
thf(1536,plain,
( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ~ $true
| ~ $true
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ),
inference(rewrite,[status(thm)],[107,96,97]) ).
thf(1537,plain,
( ( n1 @ ( pv10 @ minus ) @ ( sk3 @ leq ) )
| ( ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) ) ) ),
inference(simp,[status(thm)],[1536]) ).
thf(11190,plain,
! [A: $i] :
( ( ( A @ ( tptp_minus_1 @ ( n0 @ sum ) ) )
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ ( n1 @ ( n5 @ minus ) @ ( n0 @ sum ) ) ) )
| ( ( n1 @ ( pv10 @ minus ) )
!= ( n1 @ ( n0 @ minus ) ) )
| ( ( n0 @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) )
!= ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) ) )
| ( sk3 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[185,3463]) ).
thf(11244,plain,
! [A: $i] :
( ( A
!= ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk2 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt ) )
| ( ( n1 @ ( n5 @ minus ) )
!= tptp_minus_1 )
| ( n0 != n0 )
| ( n1 != n1 )
| ( pv10 != n0 )
| ( ( n0 @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) )
!= ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) ) )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[11190]) ).
thf(11276,plain,
( ( ( n1 @ ( n5 @ minus ) )
!= tptp_minus_1 )
| ( pv10 != n0 )
| ( ( n0 @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ ( pv10 @ ( x @ a_select2 ) @ ( n0 @ ( sk1 @ ( center @ a_select3 ) ) @ minus ) @ times ) @ sqrt @ divide ) )
!= ( sk1 @ ( pv10 @ ( q @ a_select3 ) ) ) )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[11244]) ).
thf(51,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(354,plain,
! [A: $i,B: $i] :
( ( A @ ( n0 @ leq ) )
=> ( A @ ( B @ uniform_int_rnd ) @ ( n0 @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(74,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ succ @ leq ) )
=> ( A @ ( B @ gt ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_succ_gt) ).
thf(543,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ succ @ leq ) )
=> ( A @ ( B @ gt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(636,plain,
! [A: $i] :
( ( ( n2 @ ( n135300 @ gt ) )
!= ( A @ ( A @ gt ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[160,143]) ).
thf(637,plain,
! [A: $i] :
( ( n2 @ ( n135300 @ gt ) )
!= ( A @ ( A @ gt ) ) ),
inference(simp,[status(thm)],[636]) ).
thf(638,plain,
! [A: $i] :
( ( n2 != A )
| ( n135300 != A ) ),
inference(simp,[status(thm)],[637]) ).
thf(639,plain,
n2 != n135300,
inference(simp,[status(thm)],[638]) ).
thf(44,axiom,
! [A: $i,B: $i] :
( ( ( A != B )
& ( B @ ( A @ leq ) ) )
=> ( A @ ( B @ gt ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_gt2) ).
thf(337,plain,
! [A: $i,B: $i] :
( ( ( A != B )
& ( B @ ( A @ leq ) ) )
=> ( A @ ( B @ gt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(14528,plain,
$false,
inference(e,[status(thm)],[138,11445,347,555,115,11256,3012,120,3429,340,153,185,3350,3994,13127,2227,4137,2531,570,11289,110,125,357,542,1800,3463,2857,2403,152,3708,4194,13045,4317,416,216,11441,121,1020,353,147,132,13106,133,11270,116,428,507,527,4589,546,1768,13109,160,561,3989,630,137,165,13094,92,484,97,522,551,3408,519,156,169,141,420,499,3001,124,526,590,547,96,2968,3354,129,11261,605,134,128,13103,558,1895,530,586,412,161,573,3686,584,562,423,1615,3609,12909,118,1520,545,572,611,236,159,3695,144,113,13100,419,567,2839,10265,140,626,155,330,345,552,130,1474,223,135,1000,2535,4196,505,12326,162,548,487,342,2899,1049,557,872,1611,150,13121,409,11443,3273,177,331,585,127,2903,154,571,143,4217,2045,1913,524,203,2870,158,186,13097,2526,568,119,235,2399,3844,346,1045,11405,2576,13124,432,168,146,11437,190,183,3469,13118,11447,564,341,11415,3716,635,415,239,242,1019,163,178,3605,1537,11276,607,2321,354,543,215,639,222,337,122]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV055+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.13/10.41 % Computer : n014.cluster.edu
% 0.13/10.41 % Model : x86_64 x86_64
% 0.13/10.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/10.41 % Memory : 8046.5625MB
% 0.13/10.41 % OS : Linux 6.8.0-71-generic
% 0.13/10.41 % CPULimit : 300
% 0.13/10.41 % WCLimit : 300
% 0.13/10.41 % DateTime : Sat Sep 26 13:09:57 UTC 2026
% 0.13/10.41 % CPUTime :
% 0.13/10.41 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.17/10.72 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 0.17/10.86 % [INFO] Parsing done (141ms).
% 0.17/10.87 % [INFO] Running in sequential loop mode.
% 1.72/11.06 % [INFO] eprover registered as external prover.
% 1.72/11.07 % [INFO] Scanning for conjecture ...
% 2.03/11.15 % [INFO] Found a conjecture (or negated_conjecture) and 91 axioms. Running axiom selection ...
% 2.27/11.21 % [INFO] Axiom selection finished. Selected 89 axioms (removed 2 axioms).
% 2.27/11.29 % [INFO] Problem is first-order (TPTP FOF).
% 2.27/11.30 % [INFO] Type checking passed.
% 2.61/11.30 % [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 ...
% 78.76/28.31 % External prover 'e' found a proof!
% 78.76/28.31 % [INFO] Killing All external provers ...
% 78.76/28.32 % Time passed: 17802ms (effective reasoning time: 17447ms)
% 78.76/28.32 % 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)>
% 78.76/28.32 % Axioms used in derivation (89): sel3_update_2, gt_135300_0, gt_0_tptp_minus_1, gt_3_1, leq_minus, sel2_update_2, succ_plus_5_l, lt_gt, gt_5_tptp_minus_1, succ_plus_3_r, gt_4_3, transitivity_gt, matrix_symm_inv, matrix_symm_trans, finite_domain_1, gt_5_0, const_array2_select, gt_2_tptp_minus_1, gt_135300_1, sel3_update_3, leq_geq, gt_1_0, leq_gt2, gt_5_4, gt_135300_5, succ_plus_1_l, gt_3_2, matrix_symm_add, leq_succ_gt, finite_domain_5, pred_minus_1, successor_3, gt_3_tptp_minus_1, matrix_symm_update_diagonal, sel2_update_1, gt_4_2, matrix_symm_sub, gt_135300_4, gt_5_3, successor_4, gt_succ, succ_plus_4_l, reflexivity_leq, successor_2, leq_gt1, gt_1_tptp_minus_1, finite_domain_2, matrix_symm_aba1, finite_domain_4, matrix_symm_aba2, succ_tptp_minus_1, succ_plus_5_r, gt_135300_3, leq_succ_succ, sum_plus_base_float, succ_plus_2_l, gt_4_1, gt_2_0, gt_5_2, const_array1_select, leq_gt_pred, matrix_symm_joseph_update, succ_pred, totality, transitivity_leq, finite_domain_3, uniform_int_rand_ranges_lo, sel3_update_1, successor_1, gt_135300_tptp_minus_1, sum_plus_base, irreflexivity_gt, successor_5, gt_3_0, sel2_update_3, pred_succ, gt_135300_2, succ_plus_1_r, succ_plus_3_l, gt_4_tptp_minus_1, succ_plus_4_r, gt_4_0, succ_plus_2_r, leq_succ_gt_equiv, gt_5_1, uniform_int_rand_ranges_hi, gt_2_1, finite_domain_0, leq_succ
% 78.76/28.32 % No. of inferences in proof: 548
% 78.76/28.32 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 17802 ms resp. 17447 ms w/o parsing
% 65.65/28.55 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 65.65/28.56 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------