%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : NUM845+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n015.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:10:09 AM UTC 2026
% Result : Theorem 126.61s 30.47s
% Output : Refutation 118.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 66
% Syntax : Number of formulae : 668 ( 215 unt; 0 typ; 8 def)
% Number of atoms : 1683 ( 780 equ; 0 cnn)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 5970 ( 723 ~; 642 |; 41 &;4476 @)
% ( 4 <=>; 84 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 8 ( 8 >; 0 *; 0 +; 0 <<)
% Number of symbols : 21 ( 18 usr; 5 con; 0-2 aty)
% Number of variables : 1141 ( 8 ^;1093 !; 32 ?;1141 :)
% ( 0 !>; 0 ?*; 0 @-; 8 @+)
% Comments :
%------------------------------------------------------------------------------
thf(vmul_decl,type,
vmul: $i > $i > $i ).
thf(vsucc_decl,type,
vsucc: $i > $i ).
thf(vd411_decl,type,
vd411: $i ).
thf(vplus_decl,type,
vplus: $i > $i > $i ).
thf(greater_decl,type,
greater: $i > $i > $o ).
thf(less_decl,type,
less: $i > $i > $o ).
thf(leq_decl,type,
leq: $i > $i > $o ).
thf(geq_decl,type,
geq: $i > $i > $o ).
thf(v1_decl,type,
v1: $i ).
thf(vskolem2_decl,type,
vskolem2: $i > $i ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i > $i > $i ).
thf(sk3_decl,type,
sk3: $i > $i > $i ).
thf(sk4_decl,type,
sk4: $i > $i > $i ).
thf(sk5_decl,type,
sk5: $i > $i > $i ).
thf(sk6_decl,type,
sk6: $i > $i ).
thf(sk7_decl,type,
sk7: $i > $i ).
thf(sk8_decl,type,
sk8: $i > $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( A @ vsucc @ ( vd411 @ vsucc @ vmul ) )
= ( A @ vsucc @ ( A @ vsucc @ ( vd411 @ vmul ) @ vplus ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i > $i > $i] :
! [B: $i,C: $i] :
( ( C @ ( B @ vplus ) @ ( B @ A ) )
= C ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( B
= ( C @ ( A @ vplus ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( A
= ( C @ ( B @ vplus ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( B
= ( C @ ( A @ vplus ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( @+[A: $i > $i] :
! [B: $i] :
( ( B @ vsucc @ A )
= B ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( @+[A: $i > $i] :
! [B: $i] :
( ( B @ vsucc @ A )
= B ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( A
= ( C @ ( B @ vplus ) ) ) ) ) ).
thf(4,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ less ) )
=> ( A @ ( B @ greater ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(147, 0), 0)') ).
thf(68,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ less ) )
=> ( A @ ( B @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(69,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ greater ) )
| ~ ( B @ ( A @ less ) ) ),
inference(cnf,[status(esa)],[68]) ).
thf(13,axiom,
! [A: $i,B: $i] :
( ~ ( B @ ( A @ less ) )
| ~ ( B @ ( A @ greater ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 2)') ).
thf(101,plain,
! [A: $i,B: $i] :
( ~ ( B @ ( A @ less ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(53,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ greater ) )
<=> ? [C: $i] :
( B
= ( C @ ( A @ vplus ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 11), 1)') ).
thf(249,plain,
! [A: $i,B: $i] :
( ( ? [C: $i] :
( B
= ( C @ ( A @ vplus ) ) )
=> ( A @ ( B @ greater ) ) )
& ( ( A @ ( B @ greater ) )
=> ? [C: $i] :
( B
= ( C @ ( A @ vplus ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(29,axiom,
! [A: $i] :
( ( A != v1 )
=> ( A
= ( A @ vskolem2 @ vsucc ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(20, 0), 0)') ).
thf(162,plain,
! [A: $i] :
( ( A != v1 )
=> ( A
= ( A @ vskolem2 @ vsucc ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(163,plain,
! [A: $i] :
( ( A
= ( A @ vskolem2 @ vsucc ) )
| ( A = v1 ) ),
inference(cnf,[status(esa)],[162]) ).
thf(164,plain,
! [A: $i] :
( ( ( A @ vskolem2 @ vsucc )
= A )
| ( A = v1 ) ),
inference(lifteq,[status(thm)],[163]) ).
thf(1,conjecture,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( A @ vsucc @ ( vd411 @ vsucc @ vmul ) )
= ( A @ vsucc @ ( A @ vsucc @ ( vd411 @ vmul ) @ vplus ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(ind(267), imp(267))') ).
thf(2,negated_conjecture,
~ ! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( A @ vsucc @ ( vd411 @ vsucc @ vmul ) )
= ( A @ vsucc @ ( A @ vsucc @ ( vd411 @ vmul ) @ vplus ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(60,plain,
~ ! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( A @ vsucc @ ( vd411 @ vsucc @ vmul ) )
= ( A @ vsucc @ ( A @ vsucc @ ( vd411 @ vmul ) @ vplus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(61,plain,
( ( ( sk1 @ vsucc @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ vsucc @ ( sk1 @ vsucc @ ( vd411 @ vmul ) @ vplus ) ) )
& ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
= ( sk1 @ ( sk1 @ ( vd411 @ vmul ) @ vplus ) ) ) ),
inference(cnf,[status(esa)],[60]) ).
thf(62,plain,
( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
= ( sk1 @ ( sk1 @ ( vd411 @ vmul ) @ vplus ) ) ),
inference(cnfConj,[status(thm)],[61]) ).
thf(64,plain,
( ( sk1 @ ( sk1 @ ( vd411 @ vmul ) @ vplus ) )
= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) ),
inference(lifteq,[status(thm)],[62]) ).
thf(18,axiom,
! [A: $i,B: $i] :
( ~ ? [C: $i] :
( A
= ( C @ ( B @ vplus ) ) )
| ( A != B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 3)') ).
thf(125,plain,
! [A: $i,B: $i] :
( ~ ? [C: $i] :
( A
= ( C @ ( B @ vplus ) ) )
| ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(126,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ vplus ) ) )
| ( A != B ) ),
inference(cnf,[status(esa)],[125]) ).
thf(127,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ vplus ) ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[126]) ).
thf(128,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) )
!= A ),
inference(simp,[status(thm)],[127]) ).
thf(426,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ ( vd411 @ vmul ) @ vplus ) )
!= ( B @ ( A @ vplus ) ) )
| ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= A ) ),
inference(paramod_ordered,[status(thm)],[64,128]) ).
thf(427,plain,
( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[426:[bind(A,$thf( sk1 @ ( vd411 @ vmul ) )),bind(B,$thf( sk1 ))]]) ).
thf(10374,plain,
! [A: $i] :
( ( ( A @ vskolem2 @ vsucc )
!= ( vd411 @ vsucc ) )
| ( ( sk1 @ ( A @ vmul ) )
!= ( sk1 @ ( vd411 @ vmul ) ) )
| ( A = v1 ) ),
inference(paramod_ordered,[status(thm)],[164,427]) ).
thf(10409,plain,
! [A: $i] :
( ( ( A @ vskolem2 )
!= vd411 )
| ( sk1 != sk1 )
| ( A != vd411 )
| ( A = v1 ) ),
inference(simp,[status(thm)],[10374]) ).
thf(10495,plain,
( ( ( vd411 @ vskolem2 )
!= vd411 )
| ( v1 = vd411 ) ),
inference(simp,[status(thm)],[10409]) ).
thf(48,axiom,
! [A: $i,B: $i] :
( B
!= ( B @ ( A @ vplus ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(73, 0), 0)') ).
thf(234,plain,
! [A: $i,B: $i] :
( B
!= ( B @ ( A @ vplus ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(33,axiom,
! [A: $i,B: $i] :
( ( ( v1 @ ( A @ vmul ) )
= A )
& ( ( B @ vsucc @ ( A @ vmul ) )
= ( A @ ( B @ ( A @ vmul ) @ vplus ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0)))') ).
thf(179,plain,
! [A: $i,B: $i] :
( ( ( v1 @ ( A @ vmul ) )
= A )
& ( ( B @ vsucc @ ( A @ vmul ) )
= ( A @ ( B @ ( A @ vmul ) @ vplus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(180,plain,
( ! [A: $i] :
( ( v1 @ ( A @ vmul ) )
= A )
& ! [A: $i,B: $i] :
( ( B @ vsucc @ ( A @ vmul ) )
= ( A @ ( B @ ( A @ vmul ) @ vplus ) ) ) ),
inference(miniscope,[status(thm)],[179]) ).
thf(181,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( C @ vmul ) )
= C )
& ( ( B @ vsucc @ ( A @ vmul ) )
= ( A @ ( B @ ( A @ vmul ) @ vplus ) ) ) ),
inference(cnf,[status(esa)],[180]) ).
thf(183,plain,
! [A: $i] :
( ( v1 @ ( A @ vmul ) )
= A ),
inference(cnfConj,[status(thm)],[181]) ).
thf(185,plain,
! [A: $i] :
( ( v1 @ ( A @ vmul ) )
= A ),
inference(lifteq,[status(thm)],[183]) ).
thf(186,plain,
! [A: $i] :
( ( v1 @ ( A @ vmul ) )
= A ),
inference(simp,[status(thm)],[185]) ).
thf(330,plain,
! [A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( sk1 @ ( vd411 @ vmul ) ) )
| ( ( sk1 @ ( A @ vplus ) )
= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[186,64]) ).
thf(332,plain,
! [A: $i] :
( ( sk1 != v1 )
| ( A != vd411 )
| ( ( sk1 @ ( A @ vplus ) )
= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) ) ),
inference(simp,[status(thm)],[330]) ).
thf(334,plain,
( ( sk1 != v1 )
| ( ( sk1 @ ( vd411 @ vplus ) )
= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) ) ),
inference(simp,[status(thm)],[332]) ).
thf(17,axiom,
! [A: $i,B: $i] :
( ( ( v1 @ ( A @ vplus ) )
= ( A @ vsucc ) )
& ( ( B @ vsucc @ ( A @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))') ).
thf(117,plain,
! [A: $i,B: $i] :
( ( ( v1 @ ( A @ vplus ) )
= ( A @ vsucc ) )
& ( ( B @ vsucc @ ( A @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(118,plain,
( ! [A: $i] :
( ( v1 @ ( A @ vplus ) )
= ( A @ vsucc ) )
& ! [A: $i,B: $i] :
( ( B @ vsucc @ ( A @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ) ),
inference(miniscope,[status(thm)],[117]) ).
thf(119,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( C @ vplus ) )
= ( C @ vsucc ) )
& ( ( B @ vsucc @ ( A @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ) ),
inference(cnf,[status(esa)],[118]) ).
thf(121,plain,
! [A: $i] :
( ( v1 @ ( A @ vplus ) )
= ( A @ vsucc ) ),
inference(cnfConj,[status(thm)],[119]) ).
thf(123,plain,
! [A: $i] :
( ( v1 @ ( A @ vplus ) )
= ( A @ vsucc ) ),
inference(lifteq,[status(thm)],[121]) ).
thf(124,plain,
! [A: $i] :
( ( v1 @ ( A @ vplus ) )
= ( A @ vsucc ) ),
inference(simp,[status(thm)],[123]) ).
thf(366,plain,
! [A: $i] :
( ( ( sk1 @ ( vd411 @ vplus ) )
!= ( v1 @ ( A @ vplus ) ) )
| ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
= ( A @ vsucc ) )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[334,124]) ).
thf(376,plain,
! [A: $i] :
( ( sk1 != v1 )
| ( vd411 != A )
| ( sk1 != v1 )
| ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
= ( A @ vsucc ) ) ),
inference(simp,[status(thm)],[366]) ).
thf(380,plain,
( ( sk1 != v1 )
| ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
= ( vd411 @ vsucc ) ) ),
inference(simp,[status(thm)],[376]) ).
thf(19,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ vplus ) )
= ( B @ ( A @ vplus ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(61, 0), 0)') ).
thf(129,plain,
! [A: $i,B: $i] :
( ( A @ ( B @ vplus ) )
= ( B @ ( A @ vplus ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(130,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) )
= ( B @ ( A @ vplus ) ) ),
inference(cnf,[status(esa)],[129]) ).
thf(131,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) )
= ( B @ ( A @ vplus ) ) ),
inference(lifteq,[status(thm)],[130]) ).
thf(1764,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ vplus ) )
!= ( sk1 @ ( sk1 @ ( vd411 @ vmul ) @ vplus ) ) )
| ( ( B @ ( A @ vplus ) )
= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[131,64]) ).
thf(1765,plain,
( ( sk1 @ ( vd411 @ vmul ) @ ( sk1 @ vplus ) )
= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[1764:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ ( vd411 @ vmul ) ))]]) ).
thf(31,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ less ) )
<=> ? [C: $i] :
( A
= ( C @ ( B @ vplus ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 12), 1)') ).
thf(168,plain,
! [A: $i,B: $i] :
( ( ? [C: $i] :
( A
= ( C @ ( B @ vplus ) ) )
=> ( A @ ( B @ less ) ) )
& ( ( A @ ( B @ less ) )
=> ? [C: $i] :
( A
= ( C @ ( B @ vplus ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(169,plain,
( ! [A: $i,B: $i] :
( ? [C: $i] :
( A
= ( C @ ( B @ vplus ) ) )
=> ( A @ ( B @ less ) ) )
& ! [A: $i,B: $i] :
( ( A @ ( B @ less ) )
=> ? [C: $i] :
( A
= ( C @ ( B @ vplus ) ) ) ) ),
inference(miniscope,[status(thm)],[168]) ).
thf(170,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( D @ less ) )
| ( C
!= ( E @ ( D @ vplus ) ) ) )
& ( ( A
= ( A @ ( B @ sk5 ) @ ( B @ vplus ) ) )
| ~ ( A @ ( B @ less ) ) ) ),
inference(cnf,[status(esa)],[169]) ).
thf(172,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ less ) )
| ( A
!= ( C @ ( B @ vplus ) ) ) ),
inference(cnfConj,[status(thm)],[170]) ).
thf(174,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ less ) )
| ( A
!= ( C @ ( B @ vplus ) ) ) ),
inference(lifteq,[status(thm)],[172]) ).
thf(175,plain,
! [B: $i,A: $i] : ( B @ ( A @ vplus ) @ ( A @ less ) ),
inference(simp,[status(thm)],[174]) ).
thf(1899,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vmul ) @ ( sk1 @ vplus ) )
!= ( B @ ( A @ vplus ) ) )
| ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[1765,175]) ).
thf(1900,plain,
sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ less ),
inference(pattern_uni,[status(thm)],[1899:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ ( vd411 @ vmul ) ))]]) ).
thf(2027,plain,
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ( vd411 @ vsucc @ ( sk1 @ less ) )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[380,1900]) ).
thf(2028,plain,
( ( vd411 @ vsucc @ ( sk1 @ less ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[2027:[]]) ).
thf(21,axiom,
! [A: $i,B: $i] :
( ( v1 @ ( B @ vplus ) @ ( A @ less ) )
=> ( B @ ( A @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(241, 0), 0)') ).
thf(136,plain,
! [A: $i,B: $i] :
( ( v1 @ ( B @ vplus ) @ ( A @ less ) )
=> ( B @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(137,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ~ ( v1 @ ( B @ vplus ) @ ( A @ less ) ) ),
inference(cnf,[status(esa)],[136]) ).
thf(5968,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ~ ( B @ vsucc @ ( A @ less ) ) ),
inference(rewrite,[status(thm)],[137,124]) ).
thf(6005,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ vsucc @ ( sk1 @ less ) )
!= ( B @ vsucc @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[2028,5968]) ).
thf(6006,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ vsucc @ ( sk1 @ less ) )
!= ( B @ vsucc @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( sk1 != v1 ) ),
inference(simp,[status(thm)],[6005]) ).
thf(6007,plain,
( ( vd411 @ ( sk1 @ leq ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[6006:[bind(A,$thf( sk1 )),bind(B,$thf( vd411 ))]]) ).
thf(5,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
=> ( A @ ( B @ geq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(163, 0), 0)') ).
thf(70,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
=> ( A @ ( B @ geq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(71,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ geq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(cnf,[status(esa)],[70]) ).
thf(6325,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ ( sk1 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ~ $true
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[6007,71]) ).
thf(6326,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ ( sk1 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ( sk1 != v1 ) ),
inference(simp,[status(thm)],[6325]) ).
thf(6327,plain,
( ( sk1 @ ( vd411 @ geq ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[6326:[bind(A,$thf( sk1 )),bind(B,$thf( vd411 ))]]) ).
thf(14,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ geq ) )
<=> ( ( B = A )
| ( A @ ( B @ greater ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 16), 1)') ).
thf(103,plain,
! [A: $i,B: $i] :
( ( ( ( B = A )
| ( A @ ( B @ greater ) ) )
=> ( A @ ( B @ geq ) ) )
& ( ( A @ ( B @ geq ) )
=> ( ( B = A )
| ( A @ ( B @ greater ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(104,plain,
( ! [A: $i,B: $i] :
( ( ( B = A )
| ( A @ ( B @ greater ) ) )
=> ( A @ ( B @ geq ) ) )
& ! [A: $i,B: $i] :
( ( A @ ( B @ geq ) )
=> ( ( B = A )
| ( A @ ( B @ greater ) ) ) ) ),
inference(miniscope,[status(thm)],[103]) ).
thf(105,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( D @ geq ) )
| ( D != C ) )
& ( ( C @ ( D @ geq ) )
| ~ ( C @ ( D @ greater ) ) )
& ( ( B = A )
| ( A @ ( B @ greater ) )
| ~ ( A @ ( B @ geq ) ) ) ),
inference(cnf,[status(esa)],[104]) ).
thf(106,plain,
! [B: $i,A: $i] :
( ( B = A )
| ( A @ ( B @ greater ) )
| ~ ( A @ ( B @ geq ) ) ),
inference(cnfConj,[status(thm)],[105]) ).
thf(109,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ greater ) )
| ~ ( A @ ( B @ geq ) )
| ( B = A ) ),
inference(lifteq,[status(thm)],[106]) ).
thf(6372,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ geq ) )
!= ( A @ ( B @ geq ) ) )
| ( A @ ( B @ greater ) )
| ~ $true
| ( B = A )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[6327,109]) ).
thf(6373,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ geq ) )
!= ( A @ ( B @ geq ) ) )
| ( A @ ( B @ greater ) )
| ( B = A )
| ( sk1 != v1 ) ),
inference(simp,[status(thm)],[6372]) ).
thf(6374,plain,
( ( sk1 @ ( vd411 @ greater ) )
| ( sk1 = vd411 )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[6373:[bind(A,$thf( sk1 )),bind(B,$thf( vd411 ))]]) ).
thf(35,axiom,
! [A: $i,B: $i] :
( ( ( A @ vsucc )
= ( B @ vsucc ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(antec(axiom(3)), imp(antec(axiom(3))))') ).
thf(189,plain,
! [A: $i,B: $i] :
( ( ( A @ vsucc )
= ( B @ vsucc ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(190,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( ( A @ vsucc )
!= ( B @ vsucc ) ) ),
inference(cnf,[status(esa)],[189]) ).
thf(191,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( ( A @ vsucc )
!= ( B @ vsucc ) ) ),
inference(lifteq,[status(thm)],[190]) ).
thf(192,plain,
? [A: $i > $i] :
! [B: $i] :
( ( B @ vsucc @ A )
= B ),
inference(detectInverse,[status(thm)],[191]) ).
thf(193,plain,
! [A: $i] :
( ( A @ vsucc @ sk6 )
= A ),
inference(cnf,[status(esa)],[192]) ).
thf(365,plain,
! [A: $i] :
( ( A @ vsucc @ sk6 )
= A ),
inference(lifteq,[status(thm)],[193]) ).
thf(22,axiom,
! [A: $i,B: $i] :
( ( A != B )
=> ! [C: $i] :
( ( A @ ( C @ vplus ) )
!= ( B @ ( C @ vplus ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(81, 0), 0)') ).
thf(138,plain,
! [A: $i,B: $i] :
( ( A != B )
=> ! [C: $i] :
( ( A @ ( C @ vplus ) )
!= ( B @ ( C @ vplus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(1822,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( B @ ( A @ vplus ) @ ( C @ less ) ) ),
inference(paramod_ordered,[status(thm)],[131,175]) ).
thf(1823,plain,
! [B: $i,A: $i] : ( B @ ( A @ vplus ) @ ( B @ less ) ),
inference(pattern_uni,[status(thm)],[1822:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(16,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( B @ ( A @ leq ) )
& ( C @ ( B @ leq ) ) )
=> ( C @ ( A @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(184, 0), 0)') ).
thf(115,plain,
! [A: $i,B: $i,C: $i] :
( ( ( B @ ( A @ leq ) )
& ( C @ ( B @ leq ) ) )
=> ( C @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(102,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ less ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(cnf,[status(esa)],[101]) ).
thf(2806,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ~ $true
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1900,102]) ).
thf(2807,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[2806]) ).
thf(2808,plain,
~ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ greater ) ),
inference(pattern_uni,[status(thm)],[2807:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) ))]]) ).
thf(7,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) )
| ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 0)') ).
thf(76,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) )
| ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(77,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) )
| ( A = B ) ),
inference(cnf,[status(esa)],[76]) ).
thf(78,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[77]) ).
thf(26,axiom,
! [A: $i,B: $i] : ( A @ ( B @ ( A @ vplus ) @ greater ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(189, 0), 0)') ).
thf(153,plain,
! [A: $i,B: $i] : ( A @ ( B @ ( A @ vplus ) @ greater ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(154,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ vplus ) @ greater ) ),
inference(cnf,[status(esa)],[153]) ).
thf(1897,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vmul ) @ ( sk1 @ vplus ) )
!= ( B @ ( A @ vplus ) ) )
| ( A @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1765,154]) ).
thf(1898,plain,
sk1 @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ),
inference(pattern_uni,[status(thm)],[1897:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ ( vd411 @ vmul ) ))]]) ).
thf(1957,plain,
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[380,1898]) ).
thf(1958,plain,
( ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[1957:[]]) ).
thf(2455,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( A != v1 )
| ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[78,1958]) ).
thf(2456,plain,
! [A: $i] :
( ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( A != v1 )
| ( sk1 @ ( A @ less ) )
| ( sk1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[2455:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(2495,plain,
( ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( sk1 @ ( v1 @ less ) )
| ( sk1 @ ( v1 @ greater ) ) ),
inference(simp,[status(thm)],[2456]) ).
thf(51,axiom,
( ( v1 @ ( vd411 @ vsucc @ vmul ) )
= ( vd411 @ vsucc ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(264, 412, 0)') ).
thf(244,plain,
( ( v1 @ ( vd411 @ vsucc @ vmul ) )
= ( vd411 @ vsucc ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(245,plain,
( ( v1 @ ( vd411 @ vsucc @ vmul ) )
= ( vd411 @ vsucc ) ),
inference(lifteq,[status(thm)],[244]) ).
thf(44,axiom,
( ( vd411 @ vsucc )
= ( v1 @ ( vd411 @ vmul ) @ vsucc ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(264, 412, 1)') ).
thf(222,plain,
( ( vd411 @ vsucc )
= ( v1 @ ( vd411 @ vmul ) @ vsucc ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(223,plain,
( ( v1 @ ( vd411 @ vmul ) @ vsucc )
= ( vd411 @ vsucc ) ),
inference(lifteq,[status(thm)],[222]) ).
thf(40,axiom,
! [A: $i] :
( ( A @ vsucc )
!= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(12, 0), 0)') ).
thf(210,plain,
! [A: $i] :
( ( A @ vsucc )
!= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(211,plain,
~ ? [A: $i] :
( ( A @ vsucc )
= A ),
inference(miniscope,[status(thm)],[210]) ).
thf(212,plain,
! [A: $i] :
( ( A @ vsucc )
!= A ),
inference(cnf,[status(esa)],[211]) ).
thf(213,plain,
! [A: $i] :
( ( A @ vsucc )
!= A ),
inference(lifteq,[status(thm)],[212]) ).
thf(303,plain,
! [A: $i] :
( ( ( v1 @ ( vd411 @ vmul ) @ vsucc )
!= ( A @ vsucc ) )
| ( ( vd411 @ vsucc )
!= A ) ),
inference(paramod_ordered,[status(thm)],[223,213]) ).
thf(304,plain,
( ( v1 @ ( vd411 @ vmul ) )
!= ( vd411 @ vsucc ) ),
inference(pattern_uni,[status(thm)],[303:[bind(A,$thf( v1 @ ( vd411 @ vmul ) ))]]) ).
thf(305,plain,
( ( ( v1 @ ( vd411 @ vsucc @ vmul ) )
!= ( v1 @ ( vd411 @ vmul ) ) )
| ( ( vd411 @ vsucc )
!= ( vd411 @ vsucc ) ) ),
inference(paramod_ordered,[status(thm)],[245,304]) ).
thf(306,plain,
( ( v1 @ ( vd411 @ vsucc @ vmul ) )
!= ( v1 @ ( vd411 @ vmul ) ) ),
inference(simp,[status(thm)],[305]) ).
thf(307,plain,
( ( v1 != v1 )
| ( ( vd411 @ vsucc )
!= vd411 ) ),
inference(simp,[status(thm)],[306]) ).
thf(308,plain,
( ( vd411 @ vsucc )
!= vd411 ),
inference(simp,[status(thm)],[307]) ).
thf(34,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ greater ) )
=> ( v1 @ ( B @ vplus ) @ ( A @ geq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(234, 0), 0)') ).
thf(187,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ greater ) )
=> ( v1 @ ( B @ vplus ) @ ( A @ geq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(188,plain,
! [B: $i,A: $i] :
( ( v1 @ ( B @ vplus ) @ ( A @ geq ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(cnf,[status(esa)],[187]) ).
thf(13738,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ geq ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(rewrite,[status(thm)],[188,124]) ).
thf(13780,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( B @ vsucc @ ( A @ geq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1898,13738]) ).
thf(13781,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( B @ vsucc @ ( A @ geq ) ) ),
inference(simp,[status(thm)],[13780]) ).
thf(13782,plain,
sk1 @ vsucc @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ geq ),
inference(pattern_uni,[status(thm)],[13781:[bind(A,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(B,$thf( sk1 ))]]) ).
thf(8,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ geq ) )
=> ( A @ ( B @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(158, 0), 0)') ).
thf(79,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ geq ) )
=> ( A @ ( B @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(80,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ geq ) ) ),
inference(cnf,[status(esa)],[79]) ).
thf(13884,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ vsucc @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ geq ) )
!= ( B @ ( A @ geq ) ) )
| ( A @ ( B @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[13782,80]) ).
thf(13885,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ vsucc @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ geq ) )
!= ( B @ ( A @ geq ) ) )
| ( A @ ( B @ leq ) ) ),
inference(simp,[status(thm)],[13884]) ).
thf(13886,plain,
sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ vsucc @ leq ),
inference(pattern_uni,[status(thm)],[13885:[bind(A,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(B,$thf( sk1 @ vsucc ))]]) ).
thf(42,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( B @ ( A @ geq ) )
& ( D @ ( C @ geq ) ) )
=> ( D @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ geq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(223, 0), 0)') ).
thf(217,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( B @ ( A @ geq ) )
& ( D @ ( C @ geq ) ) )
=> ( D @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ geq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(59,axiom,
! [A: $i] :
( ( A @ ( v1 @ vplus ) )
= ( A @ vsucc ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(43, 0), 0)') ).
thf(274,plain,
! [A: $i] :
( ( A @ ( v1 @ vplus ) )
= ( A @ vsucc ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(275,plain,
! [A: $i] :
( ( A @ ( v1 @ vplus ) )
= ( A @ vsucc ) ),
inference(cnf,[status(esa)],[274]) ).
thf(276,plain,
! [A: $i] :
( ( A @ ( v1 @ vplus ) )
= ( A @ vsucc ) ),
inference(lifteq,[status(thm)],[275]) ).
thf(182,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vmul ) )
= ( A @ ( B @ ( A @ vmul ) @ vplus ) ) ),
inference(cnfConj,[status(thm)],[181]) ).
thf(184,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ vmul ) @ vplus ) )
= ( B @ vsucc @ ( A @ vmul ) ) ),
inference(lifteq,[status(thm)],[182]) ).
thf(120,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ),
inference(cnfConj,[status(thm)],[119]) ).
thf(122,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ),
inference(lifteq,[status(thm)],[120]) ).
thf(2909,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vplus ) @ greater ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ greater ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[154,2808]) ).
thf(2910,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ vplus ) @ greater ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ greater ) ) ),
inference(simp,[status(thm)],[2909]) ).
thf(2913,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ( ( B @ ( A @ vplus ) )
!= sk1 ) ),
inference(simp,[status(thm)],[2910]) ).
thf(2927,plain,
! [A: $i] :
( ( A @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) )
!= sk1 ),
inference(simp,[status(thm)],[2913]) ).
thf(5840,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ vsucc @ ( A @ vplus ) )
!= ( C @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[122,2927]) ).
thf(5841,plain,
! [A: $i] :
( ( A @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) @ vsucc )
!= sk1 ),
inference(pattern_uni,[status(thm)],[5840:[bind(A,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(B,$thf( G )),bind(C,$thf( G @ vsucc ))]]) ).
thf(5860,plain,
! [A: $i] :
( ( A @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) @ vsucc )
!= sk1 ),
inference(simp,[status(thm)],[5841]) ).
thf(8125,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ vplus ) )
!= ( C @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[131,5860]) ).
thf(8126,plain,
! [A: $i] :
( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( A @ vplus ) @ vsucc )
!= sk1 ),
inference(pattern_uni,[status(thm)],[8125:[bind(A,$thf( A )),bind(B,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(C,$thf( A ))]]) ).
thf(13065,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( C @ vplus ) ) )
| ( ( B @ vsucc @ ( A @ vmul ) @ vsucc )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[184,8126]) ).
thf(13066,plain,
! [A: $i] :
( ( A @ vsucc @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vmul ) @ vsucc )
!= sk1 ),
inference(pattern_uni,[status(thm)],[13065:[bind(A,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(B,$thf( E )),bind(C,$thf( E @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vmul ) ))]]) ).
thf(13219,plain,
! [A: $i] :
( ( A @ vsucc @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vmul ) @ vsucc )
!= sk1 ),
inference(simp,[status(thm)],[13066]) ).
thf(28,axiom,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( A @ vsucc @ ( vd411 @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) )
= ( A @ vsucc @ ( vd411 @ ( A @ ( vd411 @ vmul ) @ vplus ) @ vplus ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(conseq(263), 1), 1)') ).
thf(159,plain,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( A @ vsucc @ ( vd411 @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) )
= ( A @ vsucc @ ( vd411 @ ( A @ ( vd411 @ vmul ) @ vplus ) @ vplus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(160,plain,
! [A: $i] :
( ( ( A @ vsucc @ ( vd411 @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) )
= ( A @ vsucc @ ( vd411 @ ( A @ ( vd411 @ vmul ) @ vplus ) @ vplus ) ) )
| ( ( A @ ( vd411 @ vsucc @ vmul ) )
!= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) ) ),
inference(cnf,[status(esa)],[159]) ).
thf(161,plain,
! [A: $i] :
( ( ( A @ vsucc @ ( vd411 @ ( A @ ( vd411 @ vmul ) @ vplus ) @ vplus ) )
= ( A @ vsucc @ ( vd411 @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
| ( ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) )
!= ( A @ ( vd411 @ vsucc @ vmul ) ) ) ),
inference(lifteq,[status(thm)],[160]) ).
thf(24,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ vplus ) @ vplus ) )
= ( C @ ( B @ vplus ) @ ( A @ vplus ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(33, 0), 0)') ).
thf(147,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ vplus ) @ vplus ) )
= ( C @ ( B @ vplus ) @ ( A @ vplus ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(148,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ vplus ) @ vplus ) )
= ( C @ ( B @ vplus ) @ ( A @ vplus ) ) ),
inference(cnf,[status(esa)],[147]) ).
thf(149,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ vplus ) @ vplus ) )
= ( C @ ( B @ vplus ) @ ( A @ vplus ) ) ),
inference(lifteq,[status(thm)],[148]) ).
thf(9565,plain,
! [A: $i] :
( ( ( A @ vsucc @ ( vd411 @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) )
= ( A @ ( vd411 @ vplus ) @ vsucc @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
| ( ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) )
!= ( A @ ( vd411 @ vsucc @ vmul ) ) ) ),
inference(rewrite,[status(thm)],[161,149,122]) ).
thf(13777,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( B @ vsucc @ ( A @ geq ) )
| ~ $true
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[1958,13738]) ).
thf(13778,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( B @ vsucc @ ( A @ geq ) )
| ( sk1 != v1 ) ),
inference(simp,[status(thm)],[13777]) ).
thf(13779,plain,
( ( sk1 @ vsucc @ ( vd411 @ vsucc @ geq ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[13778:[bind(A,$thf( vd411 @ vsucc )),bind(B,$thf( sk1 ))]]) ).
thf(461,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( v1 @ vplus ) )
!= ( C @ ( B @ vplus ) ) )
| ( B @ ( A @ vsucc @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[276,154]) ).
thf(462,plain,
! [A: $i] : ( v1 @ ( A @ vsucc @ greater ) ),
inference(pattern_uni,[status(thm)],[461:[bind(A,$thf( A )),bind(B,$thf( v1 )),bind(C,$thf( A ))]]) ).
thf(2818,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vsucc @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ~ ( C @ ( B @ less ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[462,102]) ).
thf(2819,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vsucc @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ~ ( C @ ( B @ less ) ) ),
inference(simp,[status(thm)],[2818]) ).
thf(2820,plain,
! [A: $i] :
~ ( v1 @ ( A @ vsucc @ less ) ),
inference(pattern_uni,[status(thm)],[2819:[bind(A,$thf( D )),bind(B,$thf( D @ vsucc )),bind(C,$thf( v1 ))]]) ).
thf(2848,plain,
! [A: $i] :
~ ( v1 @ ( A @ vsucc @ less ) ),
inference(simp,[status(thm)],[2820]) ).
thf(4209,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( A @ less ) )
!= ( v1 @ ( C @ vsucc @ less ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[175,2848]) ).
thf(4210,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ ( A @ less ) )
!= ( v1 @ ( C @ vsucc @ less ) ) ),
inference(simp,[status(thm)],[4209]) ).
thf(4217,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) )
!= v1 )
| ( A
!= ( C @ vsucc ) ) ),
inference(simp,[status(thm)],[4210]) ).
thf(4236,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vsucc @ vplus ) )
!= v1 ),
inference(simp,[status(thm)],[4217]) ).
thf(6216,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ vsucc @ ( A @ vplus ) )
!= ( C @ ( D @ vsucc @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[122,4236]) ).
thf(6217,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vplus ) @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[6216:[bind(A,$thf( E @ vsucc )),bind(B,$thf( F )),bind(C,$thf( F @ vsucc )),bind(D,$thf( E ))]]) ).
thf(6227,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vplus ) @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[6217]) ).
thf(9318,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ vsucc @ ( A @ vplus ) )
!= ( D @ ( C @ vsucc @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[122,6227]) ).
thf(9319,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vplus ) @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[9318:[bind(A,$thf( E @ vsucc )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ vsucc ))]]) ).
thf(9344,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vplus ) @ vsucc @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[9319]) ).
thf(41,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ vsucc @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(52, 0), 0)') ).
thf(214,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ vsucc @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(215,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ),
inference(cnf,[status(esa)],[214]) ).
thf(216,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ),
inference(lifteq,[status(thm)],[215]) ).
thf(15883,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ vsucc @ vsucc @ vsucc )
!= v1 ),
inference(rewrite,[status(thm)],[9344,216]) ).
thf(15884,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( v1 @ vplus ) )
!= ( C @ ( B @ vplus ) ) )
| ( ( A @ vsucc @ vsucc @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[276,15883]) ).
thf(15885,plain,
! [A: $i] :
( ( A @ vsucc @ vsucc @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[15884:[bind(A,$thf( A )),bind(B,$thf( v1 )),bind(C,$thf( A ))]]) ).
thf(454,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ ( vd411 @ vmul ) @ vplus ) )
!= ( B @ ( A @ vplus ) ) )
| ( A @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[64,154]) ).
thf(455,plain,
sk1 @ ( vd411 @ vmul ) @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ),
inference(pattern_uni,[status(thm)],[454:[bind(A,$thf( sk1 @ ( vd411 @ vmul ) )),bind(B,$thf( sk1 ))]]) ).
thf(2821,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vmul ) @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[455,102]) ).
thf(2822,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vmul ) @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) ) ),
inference(simp,[status(thm)],[2821]) ).
thf(2823,plain,
~ ( sk1 @ ( vd411 @ vmul ) @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ less ) ),
inference(pattern_uni,[status(thm)],[2822:[bind(A,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(B,$thf( sk1 @ ( vd411 @ vmul ) ))]]) ).
thf(4621,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( A @ less ) )
!= ( sk1 @ ( vd411 @ vmul ) @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ less ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[175,2823]) ).
thf(4622,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ ( A @ less ) )
!= ( sk1 @ ( vd411 @ vmul ) @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ less ) ) ),
inference(simp,[status(thm)],[4621]) ).
thf(4634,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) )
!= ( sk1 @ ( vd411 @ vmul ) ) )
| ( A
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) ) ),
inference(simp,[status(thm)],[4622]) ).
thf(4650,plain,
! [A: $i] :
( ( A @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) )
!= ( sk1 @ ( vd411 @ vmul ) ) ),
inference(simp,[status(thm)],[4634]) ).
thf(50,axiom,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( A @ vsucc @ ( vd411 @ ( A @ ( vd411 @ vmul ) @ vplus ) @ vplus ) )
= ( A @ vsucc @ ( A @ vsucc @ ( vd411 @ vmul ) @ vplus ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(conseq(263), 1), 0)') ).
thf(241,plain,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( A @ vsucc @ ( vd411 @ ( A @ ( vd411 @ vmul ) @ vplus ) @ vplus ) )
= ( A @ vsucc @ ( A @ vsucc @ ( vd411 @ vmul ) @ vplus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(242,plain,
! [A: $i] :
( ( ( A @ vsucc @ ( vd411 @ ( A @ ( vd411 @ vmul ) @ vplus ) @ vplus ) )
= ( A @ vsucc @ ( A @ vsucc @ ( vd411 @ vmul ) @ vplus ) ) )
| ( ( A @ ( vd411 @ vsucc @ vmul ) )
!= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) ) ),
inference(cnf,[status(esa)],[241]) ).
thf(243,plain,
! [A: $i] :
( ( ( A @ vsucc @ ( vd411 @ ( A @ ( vd411 @ vmul ) @ vplus ) @ vplus ) )
= ( A @ vsucc @ ( A @ vsucc @ ( vd411 @ vmul ) @ vplus ) ) )
| ( ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) )
!= ( A @ ( vd411 @ vsucc @ vmul ) ) ) ),
inference(lifteq,[status(thm)],[242]) ).
thf(19455,plain,
! [A: $i] :
( ( ( A @ vsucc @ ( vd411 @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) )
= ( A @ ( A @ vsucc @ ( vd411 @ vmul ) @ vplus ) @ vsucc ) )
| ( ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) )
!= ( A @ ( vd411 @ vsucc @ vmul ) ) ) ),
inference(rewrite,[status(thm)],[243,149,122]) ).
thf(10,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ leq ) )
<=> ( ( B = A )
| ( A @ ( B @ less ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','def(cond(conseq(axiom(3)), 17), 1)') ).
thf(85,plain,
! [A: $i,B: $i] :
( ( ( ( B = A )
| ( A @ ( B @ less ) ) )
=> ( A @ ( B @ leq ) ) )
& ( ( A @ ( B @ leq ) )
=> ( ( B = A )
| ( A @ ( B @ less ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(86,plain,
( ! [A: $i,B: $i] :
( ( ( B = A )
| ( A @ ( B @ less ) ) )
=> ( A @ ( B @ leq ) ) )
& ! [A: $i,B: $i] :
( ( A @ ( B @ leq ) )
=> ( ( B = A )
| ( A @ ( B @ less ) ) ) ) ),
inference(miniscope,[status(thm)],[85]) ).
thf(87,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( D @ leq ) )
| ( D != C ) )
& ( ( C @ ( D @ leq ) )
| ~ ( C @ ( D @ less ) ) )
& ( ( B = A )
| ( A @ ( B @ less ) )
| ~ ( A @ ( B @ leq ) ) ) ),
inference(cnf,[status(esa)],[86]) ).
thf(89,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ leq ) )
| ~ ( A @ ( B @ less ) ) ),
inference(cnfConj,[status(thm)],[87]) ).
thf(92,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ leq ) )
| ~ ( A @ ( B @ less ) ) ),
inference(simp,[status(thm)],[89]) ).
thf(2087,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ less ) )
!= ( A @ ( B @ less ) ) )
| ( A @ ( B @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1900,92]) ).
thf(2088,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ less ) )
!= ( A @ ( B @ less ) ) )
| ( A @ ( B @ leq ) ) ),
inference(simp,[status(thm)],[2087]) ).
thf(2089,plain,
sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ leq ),
inference(pattern_uni,[status(thm)],[2088:[bind(A,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(B,$thf( sk1 ))]]) ).
thf(2145,plain,
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ( vd411 @ vsucc @ ( sk1 @ leq ) )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[380,2089]) ).
thf(2146,plain,
( ( vd411 @ vsucc @ ( sk1 @ leq ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[2145:[]]) ).
thf(6212,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ vplus ) )
!= ( C @ ( D @ vsucc @ vplus ) ) )
| ( ( B @ ( A @ vplus ) )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[131,4236]) ).
thf(6213,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vplus ) )
!= v1 ),
inference(pattern_uni,[status(thm)],[6212:[bind(A,$thf( A )),bind(B,$thf( E @ vsucc )),bind(C,$thf( A )),bind(D,$thf( E ))]]) ).
thf(6224,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vplus ) )
!= v1 ),
inference(simp,[status(thm)],[6213]) ).
thf(6553,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ vsucc )
!= v1 ),
inference(rewrite,[status(thm)],[6224,122]) ).
thf(6590,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( ( A @ ( B @ vplus ) @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[131,6553]) ).
thf(6591,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[6590:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(13078,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( C @ ( D @ vplus ) ) )
| ( ( B @ vsucc @ ( A @ vmul ) @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[184,6591]) ).
thf(13079,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vmul ) @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[13078:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ vmul ) ))]]) ).
thf(13238,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vmul ) @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[13079]) ).
thf(2447,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( B != v1 )
| ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[78,1958]) ).
thf(2448,plain,
! [A: $i] :
( ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( A != v1 )
| ( A @ ( sk1 @ less ) )
| ( A @ ( sk1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[2447:[bind(A,$thf( sk1 ))]]) ).
thf(2490,plain,
( ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( v1 @ ( sk1 @ less ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(simp,[status(thm)],[2448]) ).
thf(4348,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( sk1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( A @ ( B @ greater ) )
| ~ $true
| ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[2490,69]) ).
thf(4349,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( sk1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( A @ ( B @ greater ) )
| ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(simp,[status(thm)],[4348]) ).
thf(4350,plain,
( ( sk1 @ ( v1 @ greater ) )
| ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[4349:[bind(A,$thf( sk1 )),bind(B,$thf( v1 ))]]) ).
thf(3,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ greater ) )
=> ( A @ ( B @ less ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(140, 0), 0)') ).
thf(66,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ greater ) )
=> ( A @ ( B @ less ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(67,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ less ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(cnf,[status(esa)],[66]) ).
thf(5936,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ~ $true
| ( sk1 @ ( v1 @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[4350,67]) ).
thf(5937,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ( sk1 @ ( v1 @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(simp,[status(thm)],[5936]) ).
thf(5938,plain,
( ( vd411 @ vsucc @ ( sk1 @ less ) )
| ( sk1 @ ( v1 @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[5937:[bind(A,$thf( vd411 @ vsucc )),bind(B,$thf( sk1 ))]]) ).
thf(8129,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ vsucc @ ( A @ vplus ) )
!= ( C @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc @ vsucc )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[122,5860]) ).
thf(8130,plain,
! [A: $i] :
( ( A @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) @ vsucc @ vsucc )
!= sk1 ),
inference(pattern_uni,[status(thm)],[8129:[bind(A,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(B,$thf( G )),bind(C,$thf( G @ vsucc ))]]) ).
thf(8165,plain,
! [A: $i] :
( ( A @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) @ vsucc @ vsucc )
!= sk1 ),
inference(simp,[status(thm)],[8130]) ).
thf(54,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ greater ) )
=> ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(193), 0), 2)') ).
thf(257,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ greater ) )
=> ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(452,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( C @ ( B @ vplus ) ) )
| ( B @ ( A @ vsucc @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[124,154]) ).
thf(453,plain,
! [A: $i] : ( A @ ( A @ vsucc @ greater ) ),
inference(pattern_uni,[status(thm)],[452:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( v1 ))]]) ).
thf(966,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( B @ ( C @ less ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[453,67]) ).
thf(967,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( B @ ( C @ less ) ) ),
inference(simp,[status(thm)],[966]) ).
thf(968,plain,
! [A: $i] : ( A @ vsucc @ ( A @ less ) ),
inference(pattern_uni,[status(thm)],[967:[bind(A,$thf( D )),bind(B,$thf( D @ vsucc )),bind(C,$thf( D ))]]) ).
thf(974,plain,
! [A: $i] : ( A @ vsucc @ ( A @ less ) ),
inference(simp,[status(thm)],[968]) ).
thf(4183,plain,
! [B: $i,A: $i] :
( ( ( A @ vsucc @ ( A @ less ) )
!= ( v1 @ ( B @ vsucc @ less ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[974,2848]) ).
thf(4184,plain,
! [B: $i,A: $i] :
( ( A @ vsucc @ ( A @ less ) )
!= ( v1 @ ( B @ vsucc @ less ) ) ),
inference(simp,[status(thm)],[4183]) ).
thf(4218,plain,
! [B: $i,A: $i] :
( ( ( A @ vsucc )
!= v1 )
| ( A
!= ( B @ vsucc ) ) ),
inference(simp,[status(thm)],[4184]) ).
thf(4238,plain,
! [A: $i] :
( ( A @ vsucc @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[4218]) ).
thf(11273,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( B @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) ) )
| ( ( A @ vsucc @ vsucc @ vsucc )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[124,8165]) ).
thf(11274,plain,
( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vsucc @ vsucc @ vsucc )
!= sk1 ),
inference(pattern_uni,[status(thm)],[11273:[bind(A,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(B,$thf( v1 ))]]) ).
thf(11425,plain,
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ( ( vd411 @ vsucc @ vsucc @ vsucc @ vsucc )
!= sk1 )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[380,11274]) ).
thf(11426,plain,
( ( ( vd411 @ vsucc @ vsucc @ vsucc @ vsucc )
!= sk1 )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[11425:[]]) ).
thf(12,axiom,
! [A: $i,B: $i] :
( ~ ( B @ ( A @ less ) )
| ( A != B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 1)') ).
thf(97,plain,
! [A: $i,B: $i] :
( ~ ( B @ ( A @ less ) )
| ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(98,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ less ) )
| ( A != B ) ),
inference(cnf,[status(esa)],[97]) ).
thf(99,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ less ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[98]) ).
thf(100,plain,
! [A: $i] :
~ ( A @ ( A @ less ) ),
inference(simp,[status(thm)],[99]) ).
thf(1175,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( A @ less ) )
!= ( C @ ( C @ less ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[175,100]) ).
thf(1176,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ ( A @ less ) )
!= ( C @ ( C @ less ) ) ),
inference(simp,[status(thm)],[1175]) ).
thf(1177,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) )
!= C )
| ( A != C ) ),
inference(simp,[status(thm)],[1176]) ).
thf(1182,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) )
!= B ),
inference(simp,[status(thm)],[1177]) ).
thf(5364,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ vsucc @ ( A @ vplus ) )
!= ( C @ ( D @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc )
!= D ) ),
inference(paramod_ordered,[status(thm)],[122,1182]) ).
thf(5365,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ vsucc )
!= A ),
inference(pattern_uni,[status(thm)],[5364:[bind(A,$thf( A )),bind(B,$thf( E )),bind(C,$thf( E @ vsucc )),bind(D,$thf( A ))]]) ).
thf(5429,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ vsucc )
!= A ),
inference(simp,[status(thm)],[5365]) ).
thf(107,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ geq ) )
| ~ ( A @ ( B @ greater ) ) ),
inference(cnfConj,[status(thm)],[105]) ).
thf(110,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ geq ) )
| ~ ( A @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[107]) ).
thf(63,plain,
( ( sk1 @ vsucc @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ vsucc @ ( sk1 @ vsucc @ ( vd411 @ vmul ) @ vplus ) ) ),
inference(cnfConj,[status(thm)],[61]) ).
thf(65,plain,
( ( sk1 @ vsucc @ ( sk1 @ vsucc @ ( vd411 @ vmul ) @ vplus ) )
!= ( sk1 @ vsucc @ ( vd411 @ vsucc @ vmul ) ) ),
inference(lifteq,[status(thm)],[63]) ).
thf(5338,plain,
( ( sk1 @ ( sk1 @ vsucc @ ( vd411 @ vmul ) @ vplus ) @ vsucc )
!= ( sk1 @ vsucc @ ( vd411 @ vsucc @ vmul ) ) ),
inference(rewrite,[status(thm)],[65,122]) ).
thf(13768,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vsucc @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( C @ vsucc @ ( B @ geq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[462,13738]) ).
thf(13769,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vsucc @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( C @ vsucc @ ( B @ geq ) ) ),
inference(simp,[status(thm)],[13768]) ).
thf(13770,plain,
! [A: $i] : ( v1 @ vsucc @ ( A @ vsucc @ geq ) ),
inference(pattern_uni,[status(thm)],[13769:[bind(A,$thf( D )),bind(B,$thf( D @ vsucc )),bind(C,$thf( v1 ))]]) ).
thf(13793,plain,
! [A: $i] : ( v1 @ vsucc @ ( A @ vsucc @ geq ) ),
inference(simp,[status(thm)],[13770]) ).
thf(14090,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ vsucc @ ( A @ vsucc @ geq ) )
!= ( C @ ( B @ geq ) ) )
| ( B @ ( C @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[13793,80]) ).
thf(14091,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ vsucc @ ( A @ vsucc @ geq ) )
!= ( C @ ( B @ geq ) ) )
| ( B @ ( C @ leq ) ) ),
inference(simp,[status(thm)],[14090]) ).
thf(14092,plain,
! [A: $i] : ( A @ vsucc @ ( v1 @ vsucc @ leq ) ),
inference(pattern_uni,[status(thm)],[14091:[bind(A,$thf( D )),bind(B,$thf( D @ vsucc )),bind(C,$thf( v1 @ vsucc ))]]) ).
thf(14103,plain,
! [A: $i] : ( A @ vsucc @ ( v1 @ vsucc @ leq ) ),
inference(simp,[status(thm)],[14092]) ).
thf(4550,plain,
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ~ ( sk1 @ ( vd411 @ vmul ) @ ( vd411 @ vsucc @ less ) )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[380,2823]) ).
thf(4551,plain,
( ~ ( sk1 @ ( vd411 @ vmul ) @ ( vd411 @ vsucc @ less ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[4550:[]]) ).
thf(2809,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( A @ less ) )
!= ( C @ ( B @ less ) ) )
| ~ $true
| ~ ( C @ ( B @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[974,102]) ).
thf(2810,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( A @ less ) )
!= ( C @ ( B @ less ) ) )
| ~ ( C @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[2809]) ).
thf(2811,plain,
! [A: $i] :
~ ( A @ vsucc @ ( A @ greater ) ),
inference(pattern_uni,[status(thm)],[2810:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ vsucc ))]]) ).
thf(2852,plain,
! [A: $i] :
~ ( A @ vsucc @ ( A @ greater ) ),
inference(simp,[status(thm)],[2811]) ).
thf(13771,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vmul ) @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( B @ vsucc @ ( A @ geq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[455,13738]) ).
thf(13772,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vmul ) @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( B @ vsucc @ ( A @ geq ) ) ),
inference(simp,[status(thm)],[13771]) ).
thf(13773,plain,
sk1 @ ( vd411 @ vmul ) @ vsucc @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ geq ),
inference(pattern_uni,[status(thm)],[13772:[bind(A,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(B,$thf( sk1 @ ( vd411 @ vmul ) ))]]) ).
thf(14314,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vmul ) @ vsucc @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ geq ) )
!= ( B @ ( A @ geq ) ) )
| ( A @ ( B @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[13773,80]) ).
thf(14315,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vmul ) @ vsucc @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ geq ) )
!= ( B @ ( A @ geq ) ) )
| ( A @ ( B @ leq ) ) ),
inference(simp,[status(thm)],[14314]) ).
thf(14316,plain,
sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ ( vd411 @ vmul ) @ vsucc @ leq ),
inference(pattern_uni,[status(thm)],[14315:[bind(A,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(B,$thf( sk1 @ ( vd411 @ vmul ) @ vsucc ))]]) ).
thf(11313,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ vplus ) )
!= ( C @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc @ vsucc )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[131,8165]) ).
thf(11314,plain,
! [A: $i] :
( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( A @ vplus ) @ vsucc @ vsucc )
!= sk1 ),
inference(pattern_uni,[status(thm)],[11313:[bind(A,$thf( A )),bind(B,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(C,$thf( A ))]]) ).
thf(5890,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ greater ) )
!= ( A @ ( B @ greater ) ) )
| ( A @ ( B @ geq ) )
| ~ $true
| ( sk1 @ ( v1 @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[4350,110]) ).
thf(5891,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ greater ) )
!= ( A @ ( B @ greater ) ) )
| ( A @ ( B @ geq ) )
| ( sk1 @ ( v1 @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(simp,[status(thm)],[5890]) ).
thf(5892,plain,
( ( sk1 @ ( vd411 @ vsucc @ geq ) )
| ( sk1 @ ( v1 @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[5891:[bind(A,$thf( sk1 )),bind(B,$thf( vd411 @ vsucc ))]]) ).
thf(4354,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( sk1 @ less ) )
!= ( A @ ( B @ less ) ) )
| ( A @ ( B @ leq ) )
| ~ $true
| ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[2490,92]) ).
thf(4355,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( sk1 @ less ) )
!= ( A @ ( B @ less ) ) )
| ( A @ ( B @ leq ) )
| ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(simp,[status(thm)],[4354]) ).
thf(4356,plain,
( ( v1 @ ( sk1 @ leq ) )
| ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[4355:[bind(A,$thf( v1 )),bind(B,$thf( sk1 ))]]) ).
thf(10621,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( sk1 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ~ $true
| ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[4356,71]) ).
thf(10622,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( sk1 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(simp,[status(thm)],[10621]) ).
thf(10623,plain,
( ( sk1 @ ( v1 @ geq ) )
| ( sk1 @ ( vd411 @ vsucc @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[10622:[bind(A,$thf( sk1 )),bind(B,$thf( v1 ))]]) ).
thf(139,plain,
! [A: $i,B: $i] :
( ( A != B )
=> ~ ? [C: $i] :
( ( A @ ( C @ vplus ) )
= ( B @ ( C @ vplus ) ) ) ),
inference(miniscope,[status(thm)],[138]) ).
thf(140,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ vplus ) )
!= ( B @ ( C @ vplus ) ) )
| ( A = B ) ),
inference(cnf,[status(esa)],[139]) ).
thf(141,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ vplus ) )
!= ( B @ ( C @ vplus ) ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[140]) ).
thf(142,plain,
? [A: $i > $i > $i] :
! [B: $i,C: $i] :
( ( C @ ( B @ vplus ) @ ( B @ A ) )
= C ),
inference(detectInverse,[status(thm)],[141]) ).
thf(143,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ ( A @ sk2 ) )
= B ),
inference(cnf,[status(esa)],[142]) ).
thf(6743,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ ( A @ sk2 ) )
= B ),
inference(lifteq,[status(thm)],[143]) ).
thf(6744,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( v1 @ vplus ) )
!= ( C @ ( B @ vplus ) ) )
| ( ( A @ vsucc @ ( B @ sk2 ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[276,6743]) ).
thf(6745,plain,
! [A: $i] :
( ( A @ vsucc @ ( v1 @ sk2 ) )
= A ),
inference(pattern_uni,[status(thm)],[6744:[bind(A,$thf( A )),bind(B,$thf( v1 )),bind(C,$thf( A ))]]) ).
thf(49,axiom,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( vd411 @ vsucc @ ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) @ vplus ) )
= ( vd411 @ vsucc @ ( A @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(conseq(263), 1), 5)') ).
thf(238,plain,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( vd411 @ vsucc @ ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) @ vplus ) )
= ( vd411 @ vsucc @ ( A @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(9,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( ( B @ ( A @ less ) )
& ( C @ ( B @ leq ) ) )
| ( ( B @ ( A @ leq ) )
& ( C @ ( B @ less ) ) ) )
=> ( C @ ( A @ less ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(177), 0), 0)') ).
thf(81,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ( B @ ( A @ less ) )
& ( C @ ( B @ leq ) ) )
| ( ( B @ ( A @ leq ) )
& ( C @ ( B @ less ) ) ) )
=> ( C @ ( A @ less ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(82,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ less ) )
| ~ ( B @ ( A @ less ) )
| ~ ( C @ ( B @ leq ) ) )
& ( ( C @ ( A @ less ) )
| ~ ( B @ ( A @ leq ) )
| ~ ( C @ ( B @ less ) ) ) ),
inference(cnf,[status(esa)],[81]) ).
thf(84,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less ) )
| ~ ( B @ ( A @ less ) )
| ~ ( C @ ( B @ leq ) ) ),
inference(cnfConj,[status(thm)],[82]) ).
thf(43,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ less ) )
=> ( B @ ( A @ less ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(202), 0), 0)') ).
thf(219,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ less ) )
=> ( B @ ( A @ less ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(220,plain,
! [A: $i,B: $i] :
( ? [C: $i] : ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ less ) )
=> ( B @ ( A @ less ) ) ),
inference(miniscope,[status(thm)],[219]) ).
thf(221,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ less ) )
| ~ ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ less ) ) ),
inference(cnf,[status(esa)],[220]) ).
thf(20,axiom,
! [A: $i,B: $i] :
( ~ ? [C: $i] :
( B
= ( C @ ( A @ vplus ) ) )
| ~ ? [C: $i] :
( A
= ( C @ ( B @ vplus ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 2)') ).
thf(132,plain,
! [A: $i,B: $i] :
( ~ ? [C: $i] :
( B
= ( C @ ( A @ vplus ) ) )
| ~ ? [C: $i] :
( A
= ( C @ ( B @ vplus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(116,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ leq ) )
| ~ ( B @ ( A @ leq ) )
| ~ ( C @ ( B @ leq ) ) ),
inference(cnf,[status(esa)],[115]) ).
thf(38,axiom,
! [A: $i] :
( ( A @ ( v1 @ vmul ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(253, 0), 0)') ).
thf(204,plain,
! [A: $i] :
( ( A @ ( v1 @ vmul ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(205,plain,
! [A: $i] :
( ( A @ ( v1 @ vmul ) )
= A ),
inference(cnf,[status(esa)],[204]) ).
thf(206,plain,
! [A: $i] :
( ( A @ ( v1 @ vmul ) )
= A ),
inference(lifteq,[status(thm)],[205]) ).
thf(10407,plain,
! [A: $i] :
( ( ( A @ vskolem2 @ vsucc )
!= ( vd411 @ vsucc ) )
| ( sk1 != sk1 )
| ( A != vd411 )
| ( A = v1 ) ),
inference(simp,[status(thm)],[10374]) ).
thf(10494,plain,
( ( ( vd411 @ vskolem2 @ vsucc )
!= ( vd411 @ vsucc ) )
| ( v1 = vd411 ) ),
inference(simp,[status(thm)],[10407]) ).
thf(47,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( ( B @ ( A @ greater ) )
& ( D @ ( C @ geq ) ) )
| ( ( B @ ( A @ geq ) )
& ( D @ ( C @ greater ) ) ) )
=> ( D @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(216), 0), 0)') ).
thf(230,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( ( B @ ( A @ greater ) )
& ( D @ ( C @ geq ) ) )
| ( ( B @ ( A @ geq ) )
& ( D @ ( C @ greater ) ) ) )
=> ( D @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(231,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) )
| ~ ( B @ ( A @ greater ) )
| ~ ( D @ ( C @ geq ) ) )
& ( ( D @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) )
| ~ ( B @ ( A @ geq ) )
| ~ ( D @ ( C @ greater ) ) ) ),
inference(cnf,[status(esa)],[230]) ).
thf(233,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) )
| ~ ( B @ ( A @ greater ) )
| ~ ( D @ ( C @ geq ) ) ),
inference(cnfConj,[status(thm)],[231]) ).
thf(4413,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| ( vd411 @ vsucc @ ( sk1 @ leq ) )
| ( A != v1 )
| ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[78,2146]) ).
thf(4414,plain,
! [A: $i] :
( ( vd411 @ vsucc @ ( sk1 @ leq ) )
| ( A != v1 )
| ( sk1 @ ( A @ less ) )
| ( sk1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[4413:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(4480,plain,
( ( vd411 @ vsucc @ ( sk1 @ leq ) )
| ( sk1 @ ( v1 @ less ) )
| ( sk1 @ ( v1 @ greater ) ) ),
inference(simp,[status(thm)],[4414]) ).
thf(13140,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( C @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) ) )
| ( ( B @ vsucc @ ( A @ vmul ) )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[184,2927]) ).
thf(13141,plain,
( ( sk1 @ vsucc @ ( vd411 @ vsucc @ vmul ) )
!= sk1 ),
inference(pattern_uni,[status(thm)],[13140:[bind(A,$thf( vd411 @ vsucc )),bind(B,$thf( sk1 )),bind(C,$thf( vd411 @ vsucc ))]]) ).
thf(13955,plain,
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ( vd411 @ vsucc @ ( sk1 @ vsucc @ leq ) )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[380,13886]) ).
thf(13956,plain,
( ( vd411 @ vsucc @ ( sk1 @ vsucc @ leq ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[13955:[]]) ).
thf(88,plain,
! [B: $i,A: $i] :
( ( B = A )
| ( A @ ( B @ less ) )
| ~ ( A @ ( B @ leq ) ) ),
inference(cnfConj,[status(thm)],[87]) ).
thf(91,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ less ) )
| ~ ( A @ ( B @ leq ) )
| ( B = A ) ),
inference(lifteq,[status(thm)],[88]) ).
thf(6328,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ ( sk1 @ leq ) )
!= ( A @ ( B @ leq ) ) )
| ( A @ ( B @ less ) )
| ~ $true
| ( B = A )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[6007,91]) ).
thf(6329,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ ( sk1 @ leq ) )
!= ( A @ ( B @ leq ) ) )
| ( A @ ( B @ less ) )
| ( B = A )
| ( sk1 != v1 ) ),
inference(simp,[status(thm)],[6328]) ).
thf(6330,plain,
( ( vd411 @ ( sk1 @ less ) )
| ( sk1 = vd411 )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[6329:[bind(A,$thf( vd411 )),bind(B,$thf( sk1 ))]]) ).
thf(7108,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ ( sk1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ~ $true
| ~ ( B @ ( A @ greater ) )
| ( sk1 = vd411 )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[6330,102]) ).
thf(7109,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ ( sk1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ~ ( B @ ( A @ greater ) )
| ( sk1 = vd411 )
| ( sk1 != v1 ) ),
inference(simp,[status(thm)],[7108]) ).
thf(7110,plain,
( ~ ( vd411 @ ( sk1 @ greater ) )
| ( sk1 = vd411 )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[7109:[bind(A,$thf( sk1 )),bind(B,$thf( vd411 ))]]) ).
thf(5836,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ vplus ) )
!= ( C @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) ) )
| ( ( B @ ( A @ vplus ) )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[131,2927]) ).
thf(5837,plain,
! [A: $i] :
( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( A @ vplus ) )
!= sk1 ),
inference(pattern_uni,[status(thm)],[5836:[bind(A,$thf( A )),bind(B,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(C,$thf( A ))]]) ).
thf(13159,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( C @ vplus ) ) )
| ( ( B @ vsucc @ ( A @ vmul ) )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[184,5837]) ).
thf(13160,plain,
! [A: $i] :
( ( A @ vsucc @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vmul ) )
!= sk1 ),
inference(pattern_uni,[status(thm)],[13159:[bind(A,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(B,$thf( E )),bind(C,$thf( E @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vmul ) ))]]) ).
thf(13265,plain,
! [A: $i] :
( ( A @ vsucc @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vmul ) )
!= sk1 ),
inference(simp,[status(thm)],[13160]) ).
thf(2090,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( A @ less ) )
!= ( B @ ( C @ less ) ) )
| ( B @ ( C @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[974,92]) ).
thf(2091,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( A @ less ) )
!= ( B @ ( C @ less ) ) )
| ( B @ ( C @ leq ) ) ),
inference(simp,[status(thm)],[2090]) ).
thf(2092,plain,
! [A: $i] : ( A @ vsucc @ ( A @ leq ) ),
inference(pattern_uni,[status(thm)],[2091:[bind(A,$thf( D )),bind(B,$thf( D @ vsucc )),bind(C,$thf( D ))]]) ).
thf(2118,plain,
! [A: $i] : ( A @ vsucc @ ( A @ leq ) ),
inference(simp,[status(thm)],[2092]) ).
thf(858,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vmul ) @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[455,67]) ).
thf(859,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vmul ) @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) ) ),
inference(simp,[status(thm)],[858]) ).
thf(860,plain,
sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ ( vd411 @ vmul ) @ less ),
inference(pattern_uni,[status(thm)],[859:[bind(A,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(B,$thf( sk1 @ ( vd411 @ vmul ) ))]]) ).
thf(914,plain,
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ( vd411 @ vsucc @ ( sk1 @ ( vd411 @ vmul ) @ less ) )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[380,860]) ).
thf(915,plain,
( ( vd411 @ vsucc @ ( sk1 @ ( vd411 @ vmul ) @ less ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[914:[]]) ).
thf(17839,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ vsucc @ ( sk1 @ ( vd411 @ vmul ) @ less ) )
!= ( B @ vsucc @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[915,5968]) ).
thf(17840,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ vsucc @ ( sk1 @ ( vd411 @ vmul ) @ less ) )
!= ( B @ vsucc @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( sk1 != v1 ) ),
inference(simp,[status(thm)],[17839]) ).
thf(17841,plain,
( ( vd411 @ ( sk1 @ ( vd411 @ vmul ) @ leq ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[17840:[bind(A,$thf( sk1 @ ( vd411 @ vmul ) )),bind(B,$thf( vd411 ))]]) ).
thf(18607,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ ( sk1 @ ( vd411 @ vmul ) @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ~ $true
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[17841,71]) ).
thf(18608,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ ( sk1 @ ( vd411 @ vmul ) @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ( sk1 != v1 ) ),
inference(simp,[status(thm)],[18607]) ).
thf(18609,plain,
( ( sk1 @ ( vd411 @ vmul ) @ ( vd411 @ geq ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[18608:[bind(A,$thf( sk1 @ ( vd411 @ vmul ) )),bind(B,$thf( vd411 ))]]) ).
thf(8091,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( B @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) ) )
| ( ( A @ vsucc @ vsucc )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[124,5860]) ).
thf(8092,plain,
( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vsucc @ vsucc )
!= sk1 ),
inference(pattern_uni,[status(thm)],[8091:[bind(A,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(B,$thf( v1 ))]]) ).
thf(8210,plain,
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ( ( vd411 @ vsucc @ vsucc @ vsucc )
!= sk1 )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[380,8092]) ).
thf(8211,plain,
( ( ( vd411 @ vsucc @ vsucc @ vsucc )
!= sk1 )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[8210:[]]) ).
thf(15,axiom,
! [A: $i] : ( v1 @ ( A @ geq ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(228, 0), 0)') ).
thf(113,plain,
! [A: $i] : ( v1 @ ( A @ geq ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(114,plain,
! [A: $i] : ( v1 @ ( A @ geq ) ),
inference(cnf,[status(esa)],[113]) ).
thf(950,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ geq ) )
!= ( C @ ( B @ geq ) ) )
| ( B @ ( C @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[114,80]) ).
thf(951,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ geq ) )
!= ( C @ ( B @ geq ) ) )
| ( B @ ( C @ leq ) ) ),
inference(simp,[status(thm)],[950]) ).
thf(952,plain,
! [A: $i] : ( A @ ( v1 @ leq ) ),
inference(pattern_uni,[status(thm)],[951:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( v1 ))]]) ).
thf(55,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( A @ vplus ) )
= ( C @ ( B @ vplus ) ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(202), 0), 1)') ).
thf(260,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( A @ vplus ) )
= ( C @ ( B @ vplus ) ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(2148,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2089,71]) ).
thf(2149,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) ) ),
inference(simp,[status(thm)],[2148]) ).
thf(2150,plain,
sk1 @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ geq ),
inference(pattern_uni,[status(thm)],[2149:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) ))]]) ).
thf(30,axiom,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( A @ ( vd411 @ vplus ) @ vsucc @ ( A @ ( vd411 @ vmul ) @ vplus ) )
= ( A @ vsucc @ ( vd411 @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(conseq(263), 1), 2)') ).
thf(165,plain,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( A @ ( vd411 @ vplus ) @ vsucc @ ( A @ ( vd411 @ vmul ) @ vplus ) )
= ( A @ vsucc @ ( vd411 @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(2685,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( A @ leq ) )
!= ( C @ ( B @ leq ) ) )
| ( B @ ( C @ geq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2118,71]) ).
thf(2686,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( A @ leq ) )
!= ( C @ ( B @ leq ) ) )
| ( B @ ( C @ geq ) ) ),
inference(simp,[status(thm)],[2685]) ).
thf(2687,plain,
! [A: $i] : ( A @ ( A @ vsucc @ geq ) ),
inference(pattern_uni,[status(thm)],[2686:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ vsucc ))]]) ).
thf(2705,plain,
! [A: $i] : ( A @ ( A @ vsucc @ geq ) ),
inference(simp,[status(thm)],[2687]) ).
thf(6592,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ vsucc @ ( A @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[122,6553]) ).
thf(6593,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[6592:[bind(A,$thf( A )),bind(B,$thf( E )),bind(C,$thf( A )),bind(D,$thf( E @ vsucc ))]]) ).
thf(6595,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ vsucc @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[6593]) ).
thf(10015,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( ( A @ ( B @ vplus ) @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[131,6595]) ).
thf(10016,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[10015:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(13142,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( C @ ( D @ vplus ) ) )
| ( ( B @ vsucc @ ( A @ vmul ) @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[184,10016]) ).
thf(13143,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vmul ) @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[13142:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ vmul ) ))]]) ).
thf(13260,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vmul ) @ vsucc @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[13143]) ).
thf(46,axiom,
! [A: $i] :
( ( A @ vsucc )
!= v1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(restrictor(axiom(1)), holds(scope(axiom(1)), 2, 0))') ).
thf(226,plain,
! [A: $i] :
( ( A @ vsucc )
!= v1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(227,plain,
~ ? [A: $i] :
( ( A @ vsucc )
= v1 ),
inference(miniscope,[status(thm)],[226]) ).
thf(228,plain,
! [A: $i] :
( ( A @ vsucc )
!= v1 ),
inference(cnf,[status(esa)],[227]) ).
thf(229,plain,
! [A: $i] :
( ( A @ vsucc )
!= v1 ),
inference(lifteq,[status(thm)],[228]) ).
thf(2824,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ~ $true
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[1958,102]) ).
thf(2825,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ( sk1 != v1 ) ),
inference(simp,[status(thm)],[2824]) ).
thf(2826,plain,
( ~ ( sk1 @ ( vd411 @ vsucc @ less ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[2825:[bind(A,$thf( vd411 @ vsucc )),bind(B,$thf( sk1 ))]]) ).
thf(1818,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( C @ ( B @ ( A @ vplus ) @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[131,154]) ).
thf(1819,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( A @ vplus ) @ greater ) ),
inference(pattern_uni,[status(thm)],[1818:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(235,plain,
~ ? [A: $i,B: $i] :
( B
= ( B @ ( A @ vplus ) ) ),
inference(miniscope,[status(thm)],[234]) ).
thf(236,plain,
! [B: $i,A: $i] :
( B
!= ( B @ ( A @ vplus ) ) ),
inference(cnf,[status(esa)],[235]) ).
thf(237,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) )
!= B ),
inference(lifteq,[status(thm)],[236]) ).
thf(1052,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ ( vd411 @ vmul ) @ vplus ) )
!= ( B @ ( A @ vplus ) ) )
| ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= B ) ),
inference(paramod_ordered,[status(thm)],[64,237]) ).
thf(1053,plain,
( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= sk1 ),
inference(pattern_uni,[status(thm)],[1052:[bind(A,$thf( sk1 @ ( vd411 @ vmul ) )),bind(B,$thf( sk1 ))]]) ).
thf(1078,plain,
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ( ( vd411 @ vsucc )
!= sk1 )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[380,1053]) ).
thf(1079,plain,
( ( ( vd411 @ vsucc )
!= sk1 )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[1078:[]]) ).
thf(45,axiom,
( ( v1 @ ( vd411 @ vmul ) @ vsucc )
= ( v1 @ ( v1 @ ( vd411 @ vmul ) @ vplus ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(264, 412, 2)') ).
thf(224,plain,
( ( v1 @ ( vd411 @ vmul ) @ vsucc )
= ( v1 @ ( v1 @ ( vd411 @ vmul ) @ vplus ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(2839,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ ( vd411 @ vmul ) @ less ) )
!= ( B @ ( A @ less ) ) )
| ~ $true
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[860,102]) ).
thf(2840,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ ( vd411 @ vmul ) @ less ) )
!= ( B @ ( A @ less ) ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[2839]) ).
thf(2841,plain,
~ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ ( vd411 @ vmul ) @ greater ) ),
inference(pattern_uni,[status(thm)],[2840:[bind(A,$thf( sk1 @ ( vd411 @ vmul ) )),bind(B,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) ))]]) ).
thf(9291,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( C @ ( B @ vsucc @ vplus ) ) )
| ( ( A @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[124,6227]) ).
thf(9292,plain,
! [A: $i] :
( ( A @ vsucc @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[9291:[bind(A,$thf( D @ vsucc )),bind(B,$thf( D )),bind(C,$thf( v1 ))]]) ).
thf(9333,plain,
! [A: $i] :
( ( A @ vsucc @ vsucc @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[9292]) ).
thf(7202,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ~ $true
| ( sk1 = vd411 )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[6374,102]) ).
thf(7203,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ( sk1 = vd411 )
| ( sk1 != v1 ) ),
inference(simp,[status(thm)],[7202]) ).
thf(7204,plain,
( ~ ( sk1 @ ( vd411 @ less ) )
| ( sk1 = vd411 )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[7203:[bind(A,$thf( vd411 )),bind(B,$thf( sk1 ))]]) ).
thf(11,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( B @ ( A @ less ) )
& ( C @ ( B @ less ) ) )
=> ( C @ ( A @ less ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(168, 0), 0)') ).
thf(95,plain,
! [A: $i,B: $i,C: $i] :
( ( ( B @ ( A @ less ) )
& ( C @ ( B @ less ) ) )
=> ( C @ ( A @ less ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(96,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less ) )
| ~ ( B @ ( A @ less ) )
| ~ ( C @ ( B @ less ) ) ),
inference(cnf,[status(esa)],[95]) ).
thf(2836,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( A @ less ) )
!= ( D @ ( C @ less ) ) )
| ~ $true
| ~ ( D @ ( C @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[175,102]) ).
thf(2837,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( A @ less ) )
!= ( D @ ( C @ less ) ) )
| ~ ( D @ ( C @ greater ) ) ),
inference(simp,[status(thm)],[2836]) ).
thf(2838,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ vplus ) @ ( A @ greater ) ),
inference(pattern_uni,[status(thm)],[2837:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ vplus ) ))]]) ).
thf(2851,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ vplus ) @ ( A @ greater ) ),
inference(simp,[status(thm)],[2838]) ).
thf(171,plain,
! [B: $i,A: $i] :
( ( A
= ( A @ ( B @ sk5 ) @ ( B @ vplus ) ) )
| ~ ( A @ ( B @ less ) ) ),
inference(cnfConj,[status(thm)],[170]) ).
thf(173,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ less ) )
| ( ( A @ ( B @ sk5 ) @ ( B @ vplus ) )
= A ) ),
inference(lifteq,[status(thm)],[171]) ).
thf(2213,plain,
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ( sk1 @ ( vd411 @ vsucc @ geq ) )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[380,2150]) ).
thf(2214,plain,
( ( sk1 @ ( vd411 @ vsucc @ geq ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[2213:[]]) ).
thf(4899,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| ( sk1 @ ( vd411 @ vsucc @ geq ) )
| ( A != v1 )
| ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[78,2214]) ).
thf(4900,plain,
! [A: $i] :
( ( sk1 @ ( vd411 @ vsucc @ geq ) )
| ( A != v1 )
| ( sk1 @ ( A @ less ) )
| ( sk1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[4899:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(4953,plain,
( ( sk1 @ ( vd411 @ vsucc @ geq ) )
| ( sk1 @ ( v1 @ less ) )
| ( sk1 @ ( v1 @ greater ) ) ),
inference(simp,[status(thm)],[4900]) ).
thf(15933,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ ( vd411 @ vmul ) @ vplus ) )
!= ( B @ ( A @ vplus ) ) )
| ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vsucc @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[64,15883]) ).
thf(15934,plain,
( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vsucc @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[15933:[bind(A,$thf( sk1 @ ( vd411 @ vmul ) )),bind(B,$thf( sk1 ))]]) ).
thf(56,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( B @ ( A @ greater ) )
& ( D @ ( C @ greater ) ) )
=> ( D @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(209, 0), 0)') ).
thf(266,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( B @ ( A @ greater ) )
& ( D @ ( C @ greater ) ) )
=> ( D @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(4405,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( vd411 @ vsucc @ ( sk1 @ leq ) )
| ( B != v1 )
| ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[78,2146]) ).
thf(4406,plain,
! [A: $i] :
( ( vd411 @ vsucc @ ( sk1 @ leq ) )
| ( A != v1 )
| ( A @ ( sk1 @ less ) )
| ( A @ ( sk1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[4405:[bind(A,$thf( sk1 ))]]) ).
thf(4476,plain,
( ( vd411 @ vsucc @ ( sk1 @ leq ) )
| ( v1 @ ( sk1 @ less ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(simp,[status(thm)],[4406]) ).
thf(2736,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| ( vd411 @ vsucc @ ( sk1 @ less ) )
| ( A != v1 )
| ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[78,2028]) ).
thf(2737,plain,
! [A: $i] :
( ( vd411 @ vsucc @ ( sk1 @ less ) )
| ( A != v1 )
| ( sk1 @ ( A @ less ) )
| ( sk1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[2736:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(2788,plain,
( ( vd411 @ vsucc @ ( sk1 @ less ) )
| ( sk1 @ ( v1 @ less ) )
| ( sk1 @ ( v1 @ greater ) ) ),
inference(simp,[status(thm)],[2737]) ).
thf(4707,plain,
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ~ ( vd411 @ vsucc @ ( sk1 @ ( vd411 @ vmul ) @ greater ) )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[380,2841]) ).
thf(4708,plain,
( ~ ( vd411 @ vsucc @ ( sk1 @ ( vd411 @ vmul ) @ greater ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[4707:[]]) ).
thf(4555,plain,
! [A: $i] :
( ( ( A @ vsucc @ ( A @ less ) )
!= ( sk1 @ ( vd411 @ vmul ) @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ less ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[974,2823]) ).
thf(4556,plain,
! [A: $i] :
( ( A @ vsucc @ ( A @ less ) )
!= ( sk1 @ ( vd411 @ vmul ) @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ less ) ) ),
inference(simp,[status(thm)],[4555]) ).
thf(4635,plain,
! [A: $i] :
( ( ( A @ vsucc )
!= ( sk1 @ ( vd411 @ vmul ) ) )
| ( A
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) ) ),
inference(simp,[status(thm)],[4556]) ).
thf(4651,plain,
( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vsucc )
!= ( sk1 @ ( vd411 @ vmul ) ) ),
inference(simp,[status(thm)],[4635]) ).
thf(5134,plain,
! [A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( sk1 @ ( vd411 @ vmul ) ) )
| ( A
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vsucc ) ) ),
inference(paramod_ordered,[status(thm)],[186,4651]) ).
thf(5138,plain,
( ( sk1 != v1 )
| ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vsucc )
!= vd411 ) ),
inference(simp,[status(thm)],[5134]) ).
thf(855,plain,
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ( sk1 @ ( vd411 @ vmul ) @ ( vd411 @ vsucc @ greater ) )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[380,455]) ).
thf(856,plain,
( ( sk1 @ ( vd411 @ vmul ) @ ( vd411 @ vsucc @ greater ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[855:[]]) ).
thf(32,axiom,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( A @ vsucc @ ( vd411 @ vsucc @ vmul ) )
= ( vd411 @ vsucc @ ( A @ ( vd411 @ vsucc @ vmul ) @ vplus ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(conseq(263), 1), 7)') ).
thf(176,plain,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( A @ vsucc @ ( vd411 @ vsucc @ vmul ) )
= ( vd411 @ vsucc @ ( A @ ( vd411 @ vsucc @ vmul ) @ vplus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(422,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vplus ) )
!= ( B @ ( A @ vplus ) ) )
| ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= A )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[334,128]) ).
thf(423,plain,
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= vd411 )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[422:[bind(A,$thf( vd411 )),bind(B,$thf( sk1 ))]]) ).
thf(2833,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vplus ) @ greater ) )
!= ( D @ ( C @ greater ) ) )
| ~ ( D @ ( C @ less ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[154,102]) ).
thf(2834,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vplus ) @ greater ) )
!= ( D @ ( C @ greater ) ) )
| ~ ( D @ ( C @ less ) ) ),
inference(simp,[status(thm)],[2833]) ).
thf(2835,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ ( A @ vplus ) @ less ) ),
inference(pattern_uni,[status(thm)],[2834:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ vplus ) )),bind(D,$thf( E ))]]) ).
thf(2849,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ ( A @ vplus ) @ less ) ),
inference(simp,[status(thm)],[2835]) ).
thf(5066,plain,
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ( ( sk1 @ ( vd411 @ vmul ) )
!= ( vd411 @ vsucc @ vsucc ) )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[380,4651]) ).
thf(5067,plain,
( ( ( sk1 @ ( vd411 @ vmul ) )
!= ( vd411 @ vsucc @ vsucc ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[5066:[]]) ).
thf(6360,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( sk1 @ ( vd411 @ geq ) )
| ( B != v1 )
| ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[78,6327]) ).
thf(6361,plain,
! [A: $i] :
( ( sk1 @ ( vd411 @ geq ) )
| ( A != v1 )
| ( A @ ( sk1 @ less ) )
| ( A @ ( sk1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[6360:[bind(A,$thf( sk1 ))]]) ).
thf(6407,plain,
( ( sk1 @ ( vd411 @ geq ) )
| ( v1 @ ( sk1 @ less ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(simp,[status(thm)],[6361]) ).
thf(2815,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ vsucc @ ( sk1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ~ $true
| ~ ( B @ ( A @ greater ) )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[2028,102]) ).
thf(2816,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ vsucc @ ( sk1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ~ ( B @ ( A @ greater ) )
| ( sk1 != v1 ) ),
inference(simp,[status(thm)],[2815]) ).
thf(2817,plain,
( ~ ( vd411 @ vsucc @ ( sk1 @ greater ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[2816:[bind(A,$thf( sk1 )),bind(B,$thf( vd411 @ vsucc ))]]) ).
thf(258,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ greater ) )
=> ! [C: $i] : ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) ) ),
inference(miniscope,[status(thm)],[257]) ).
thf(259,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(cnf,[status(esa)],[258]) ).
thf(37,axiom,
! [A: $i,B: $i] :
( ( A != B )
=> ( ( A @ vsucc )
!= ( B @ vsucc ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(6, 0), 0)') ).
thf(199,plain,
! [A: $i,B: $i] :
( ( A != B )
=> ( ( A @ vsucc )
!= ( B @ vsucc ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(200,plain,
! [B: $i,A: $i] :
( ( ( A @ vsucc )
!= ( B @ vsucc ) )
| ( A = B ) ),
inference(cnf,[status(esa)],[199]) ).
thf(201,plain,
! [B: $i,A: $i] :
( ( ( A @ vsucc )
!= ( B @ vsucc ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[200]) ).
thf(202,plain,
? [A: $i > $i] :
! [B: $i] :
( ( B @ vsucc @ A )
= B ),
inference(detectInverse,[status(thm)],[201]) ).
thf(203,plain,
! [A: $i] :
( ( A @ vsucc @ sk7 )
= A ),
inference(cnf,[status(esa)],[202]) ).
thf(402,plain,
! [A: $i] :
( ( A @ vsucc @ sk7 )
= A ),
inference(lifteq,[status(thm)],[203]) ).
thf(13053,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( C @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) ) )
| ( ( B @ vsucc @ ( A @ vmul ) @ vsucc @ vsucc )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[184,8165]) ).
thf(13054,plain,
( ( sk1 @ vsucc @ ( vd411 @ vsucc @ vmul ) @ vsucc @ vsucc )
!= sk1 ),
inference(pattern_uni,[status(thm)],[13053:[bind(A,$thf( vd411 @ vsucc )),bind(B,$thf( sk1 )),bind(C,$thf( vd411 @ vsucc ))]]) ).
thf(2876,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ greater ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[453,2808]) ).
thf(2877,plain,
! [A: $i] :
( ( A @ ( A @ vsucc @ greater ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ greater ) ) ),
inference(simp,[status(thm)],[2876]) ).
thf(2914,plain,
! [A: $i] :
( ( A
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ( ( A @ vsucc )
!= sk1 ) ),
inference(simp,[status(thm)],[2877]) ).
thf(2928,plain,
( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vsucc )
!= sk1 ),
inference(simp,[status(thm)],[2914]) ).
thf(3050,plain,
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ( ( vd411 @ vsucc @ vsucc )
!= sk1 )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[380,2928]) ).
thf(3051,plain,
( ( ( vd411 @ vsucc @ vsucc )
!= sk1 )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[3050:[]]) ).
thf(1786,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ vplus ) )
!= ( sk1 @ vsucc @ ( sk1 @ vsucc @ ( vd411 @ vmul ) @ vplus ) ) )
| ( ( B @ ( A @ vplus ) )
!= ( sk1 @ vsucc @ ( vd411 @ vsucc @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[131,65]) ).
thf(1787,plain,
( ( sk1 @ vsucc @ ( vd411 @ vmul ) @ ( sk1 @ vsucc @ vplus ) )
!= ( sk1 @ vsucc @ ( vd411 @ vsucc @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[1786:[bind(A,$thf( sk1 @ vsucc )),bind(B,$thf( sk1 @ vsucc @ ( vd411 @ vmul ) ))]]) ).
thf(17480,plain,
( ( sk1 @ vsucc @ ( vd411 @ vmul ) @ ( sk1 @ vplus ) @ vsucc )
!= ( sk1 @ vsucc @ ( vd411 @ vsucc @ vmul ) ) ),
inference(rewrite,[status(thm)],[1787,216]) ).
thf(23,axiom,
! [A: $i,B: $i] :
( ? [C: $i] :
( B
= ( C @ ( A @ vplus ) ) )
| ? [C: $i] :
( A
= ( C @ ( B @ vplus ) ) )
| ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 0)') ).
thf(144,plain,
! [A: $i,B: $i] :
( ? [C: $i] :
( B
= ( C @ ( A @ vplus ) ) )
| ? [C: $i] :
( A
= ( C @ ( B @ vplus ) ) )
| ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(239,plain,
! [A: $i] :
( ( ( vd411 @ vsucc @ ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) @ vplus ) )
= ( vd411 @ vsucc @ ( A @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
| ( ( A @ ( vd411 @ vsucc @ vmul ) )
!= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) ) ),
inference(cnf,[status(esa)],[238]) ).
thf(240,plain,
! [A: $i] :
( ( ( vd411 @ vsucc @ ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) @ vplus ) )
= ( vd411 @ vsucc @ ( A @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
| ( ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) )
!= ( A @ ( vd411 @ vsucc @ vmul ) ) ) ),
inference(lifteq,[status(thm)],[239]) ).
thf(18665,plain,
! [A: $i] :
( ( ( vd411 @ vsucc @ ( A @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) )
= ( vd411 @ ( A @ vplus ) @ vsucc @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
| ( ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) )
!= ( A @ ( vd411 @ vsucc @ vmul ) ) ) ),
inference(rewrite,[status(thm)],[240,149,122]) ).
thf(2102,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( A @ less ) )
!= ( C @ ( D @ less ) ) )
| ( C @ ( D @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[175,92]) ).
thf(2103,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( A @ less ) )
!= ( C @ ( D @ less ) ) )
| ( C @ ( D @ leq ) ) ),
inference(simp,[status(thm)],[2102]) ).
thf(2104,plain,
! [B: $i,A: $i] : ( B @ ( A @ vplus ) @ ( A @ leq ) ),
inference(pattern_uni,[status(thm)],[2103:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ vplus ) )),bind(D,$thf( E ))]]) ).
thf(2119,plain,
! [B: $i,A: $i] : ( B @ ( A @ vplus ) @ ( A @ leq ) ),
inference(simp,[status(thm)],[2104]) ).
thf(4777,plain,
! [A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( sk1 @ ( vd411 @ vmul ) ) )
| ~ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[186,2841]) ).
thf(4787,plain,
! [A: $i] :
( ( sk1 != v1 )
| ( A != vd411 )
| ~ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[4777]) ).
thf(4805,plain,
( ( sk1 != v1 )
| ~ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( vd411 @ greater ) ) ),
inference(simp,[status(thm)],[4787]) ).
thf(17096,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ vsucc @ ( sk1 @ less ) )
!= ( B @ vsucc @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( sk1 @ ( v1 @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[5938,5968]) ).
thf(17097,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ vsucc @ ( sk1 @ less ) )
!= ( B @ vsucc @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( sk1 @ ( v1 @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(simp,[status(thm)],[17096]) ).
thf(17098,plain,
( ( vd411 @ ( sk1 @ leq ) )
| ( sk1 @ ( v1 @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[17097:[bind(A,$thf( sk1 )),bind(B,$thf( vd411 ))]]) ).
thf(1800,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) )
!= ( C @ ( D @ vplus ) ) )
| ( ( A @ ( B @ vplus ) )
!= D ) ),
inference(paramod_ordered,[status(thm)],[131,1182]) ).
thf(1801,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) )
!= A ),
inference(pattern_uni,[status(thm)],[1800:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(450,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vplus ) )
!= ( B @ ( A @ vplus ) ) )
| ( A @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ) )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[334,154]) ).
thf(451,plain,
( ( vd411 @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[450:[bind(A,$thf( vd411 )),bind(B,$thf( sk1 ))]]) ).
thf(2800,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ~ $true
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[451,102]) ).
thf(2801,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ( sk1 != v1 ) ),
inference(simp,[status(thm)],[2800]) ).
thf(2802,plain,
( ~ ( vd411 @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ less ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[2801:[bind(A,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(B,$thf( vd411 ))]]) ).
thf(58,axiom,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( vd411 @ vsucc @ ( A @ ( vd411 @ vsucc @ vmul ) @ vplus ) )
= ( vd411 @ vsucc @ ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) @ vplus ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(conseq(263), 1), 6)') ).
thf(271,plain,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( vd411 @ vsucc @ ( A @ ( vd411 @ vsucc @ vmul ) @ vplus ) )
= ( vd411 @ vsucc @ ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) @ vplus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(13063,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( C @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) ) )
| ( ( B @ vsucc @ ( A @ vmul ) )
!= ( sk1 @ ( vd411 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[184,4650]) ).
thf(13064,plain,
( ( sk1 @ vsucc @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[13063:[bind(A,$thf( vd411 @ vsucc )),bind(B,$thf( sk1 )),bind(C,$thf( vd411 @ vsucc ))]]) ).
thf(10650,plain,
! [B: $i,A: $i] :
( ( B
!= ( vd411 @ vskolem2 ) )
| ( A != vd411 )
| ( v1 = vd411 )
| ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[78,10495]) ).
thf(10651,plain,
! [A: $i] :
( ( A != vd411 )
| ( v1 = vd411 )
| ( vd411 @ vskolem2 @ ( A @ less ) )
| ( vd411 @ vskolem2 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[10650:[bind(A,$thf( A )),bind(B,$thf( vd411 @ vskolem2 ))]]) ).
thf(10677,plain,
( ( v1 = vd411 )
| ( vd411 @ vskolem2 @ ( vd411 @ less ) )
| ( vd411 @ vskolem2 @ ( vd411 @ greater ) ) ),
inference(simp,[status(thm)],[10651]) ).
thf(10646,plain,
! [B: $i,A: $i] :
( ( A
!= ( vd411 @ vskolem2 ) )
| ( B != vd411 )
| ( v1 = vd411 )
| ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[78,10495]) ).
thf(10647,plain,
! [A: $i] :
( ( A != vd411 )
| ( v1 = vd411 )
| ( A @ ( vd411 @ vskolem2 @ less ) )
| ( A @ ( vd411 @ vskolem2 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[10646:[bind(A,$thf( vd411 @ vskolem2 )),bind(B,$thf( B ))]]) ).
thf(10675,plain,
( ( v1 = vd411 )
| ( vd411 @ ( vd411 @ vskolem2 @ less ) )
| ( vd411 @ ( vd411 @ vskolem2 @ greater ) ) ),
inference(simp,[status(thm)],[10647]) ).
thf(1820,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( C @ ( A @ ( B @ vplus ) @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[131,154]) ).
thf(1821,plain,
! [B: $i,A: $i] : ( A @ ( A @ ( B @ vplus ) @ greater ) ),
inference(pattern_uni,[status(thm)],[1820:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(27,axiom,
! [A: $i,B: $i] :
( ~ ? [C: $i] :
( B
= ( C @ ( A @ vplus ) ) )
| ( A != B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(88), 0), 1)') ).
thf(155,plain,
! [A: $i,B: $i] :
( ~ ? [C: $i] :
( B
= ( C @ ( A @ vplus ) ) )
| ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(6768,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vmul ) @ ( sk1 @ vplus ) )
!= ( B @ ( A @ vplus ) ) )
| ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( A @ sk2 ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[1765,6743]) ).
thf(6769,plain,
( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ sk2 ) )
= ( sk1 @ ( vd411 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[6768:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ ( vd411 @ vmul ) ))]]) ).
thf(6002,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ vsucc @ ( sk1 @ less ) )
!= ( B @ vsucc @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( sk1 @ ( v1 @ less ) )
| ( sk1 @ ( v1 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[2788,5968]) ).
thf(6003,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ vsucc @ ( sk1 @ less ) )
!= ( B @ vsucc @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( sk1 @ ( v1 @ less ) )
| ( sk1 @ ( v1 @ greater ) ) ),
inference(simp,[status(thm)],[6002]) ).
thf(6004,plain,
( ( vd411 @ ( sk1 @ leq ) )
| ( sk1 @ ( v1 @ less ) )
| ( sk1 @ ( v1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[6003:[bind(A,$thf( sk1 )),bind(B,$thf( vd411 ))]]) ).
thf(277,plain,
! [A: $i] :
( ( ( v1 @ ( vd411 @ vmul ) @ vsucc )
!= ( A @ vsucc ) )
| ( ( vd411 @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[223,229]) ).
thf(278,plain,
( ( vd411 @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[277:[bind(A,$thf( v1 @ ( vd411 @ vmul ) ))]]) ).
thf(2728,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( vd411 @ vsucc @ ( sk1 @ less ) )
| ( B != v1 )
| ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[78,2028]) ).
thf(2729,plain,
! [A: $i] :
( ( vd411 @ vsucc @ ( sk1 @ less ) )
| ( A != v1 )
| ( A @ ( sk1 @ less ) )
| ( A @ ( sk1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[2728:[bind(A,$thf( sk1 ))]]) ).
thf(2783,plain,
( ( vd411 @ vsucc @ ( sk1 @ less ) )
| ( v1 @ ( sk1 @ less ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(simp,[status(thm)],[2729]) ).
thf(6025,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ vsucc @ ( sk1 @ less ) )
!= ( B @ vsucc @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( v1 @ ( sk1 @ less ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[2783,5968]) ).
thf(6026,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ vsucc @ ( sk1 @ less ) )
!= ( B @ vsucc @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( v1 @ ( sk1 @ less ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(simp,[status(thm)],[6025]) ).
thf(6027,plain,
( ( vd411 @ ( sk1 @ leq ) )
| ( v1 @ ( sk1 @ less ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[6026:[bind(A,$thf( sk1 )),bind(B,$thf( vd411 ))]]) ).
thf(2105,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ ( vd411 @ vmul ) @ less ) )
!= ( A @ ( B @ less ) ) )
| ( A @ ( B @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[860,92]) ).
thf(2106,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ ( vd411 @ vmul ) @ less ) )
!= ( A @ ( B @ less ) ) )
| ( A @ ( B @ leq ) ) ),
inference(simp,[status(thm)],[2105]) ).
thf(2107,plain,
sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ ( vd411 @ vmul ) @ leq ),
inference(pattern_uni,[status(thm)],[2106:[bind(A,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(B,$thf( sk1 @ ( vd411 @ vmul ) ))]]) ).
thf(39,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) )
=> ( B @ ( A @ greater ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(202), 0), 2)') ).
thf(207,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) )
=> ( B @ ( A @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(208,plain,
! [A: $i,B: $i] :
( ? [C: $i] : ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) )
=> ( B @ ( A @ greater ) ) ),
inference(miniscope,[status(thm)],[207]) ).
thf(209,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ greater ) )
| ~ ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) ) ),
inference(cnf,[status(esa)],[208]) ).
thf(108,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ geq ) )
| ( B != A ) ),
inference(cnfConj,[status(thm)],[105]) ).
thf(111,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ geq ) )
| ( B != A ) ),
inference(lifteq,[status(thm)],[108]) ).
thf(112,plain,
! [A: $i] : ( A @ ( A @ geq ) ),
inference(simp,[status(thm)],[111]) ).
thf(36,axiom,
! [A: $i,B: $i,C: $i] :
( ( A = B )
=> ( ( C @ ( A @ vplus ) )
= ( C @ ( B @ vplus ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(193), 0), 1)') ).
thf(194,plain,
! [A: $i,B: $i,C: $i] :
( ( A = B )
=> ( ( C @ ( A @ vplus ) )
= ( C @ ( B @ vplus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(25,axiom,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( vd411 @ vsucc @ ( A @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) )
= ( A @ ( vd411 @ vsucc @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(conseq(263), 1), 4)') ).
thf(150,plain,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( vd411 @ vsucc @ ( A @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) )
= ( A @ ( vd411 @ vsucc @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(2803,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ~ ( C @ ( B @ less ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[453,102]) ).
thf(2804,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ~ ( C @ ( B @ less ) ) ),
inference(simp,[status(thm)],[2803]) ).
thf(2805,plain,
! [A: $i] :
~ ( A @ ( A @ vsucc @ less ) ),
inference(pattern_uni,[status(thm)],[2804:[bind(A,$thf( D )),bind(B,$thf( D @ vsucc )),bind(C,$thf( D ))]]) ).
thf(2850,plain,
! [A: $i] :
~ ( A @ ( A @ vsucc @ less ) ),
inference(simp,[status(thm)],[2805]) ).
thf(15752,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vsucc @ vplus ) )
!= ( C @ ( D @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[216,10016]) ).
thf(15753,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) @ vsucc @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[15752:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( E @ vsucc ))]]) ).
thf(15817,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) @ vsucc @ vsucc @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[15753]) ).
thf(6576,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ ( vd411 @ vmul ) @ vplus ) )
!= ( B @ ( A @ vplus ) ) )
| ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[64,6553]) ).
thf(6577,plain,
( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[6576:[bind(A,$thf( sk1 @ ( vd411 @ vmul ) )),bind(B,$thf( sk1 ))]]) ).
thf(17775,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ ( sk1 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ~ $true
| ( sk1 @ ( v1 @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[17098,71]) ).
thf(17776,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ ( sk1 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ( sk1 @ ( v1 @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(simp,[status(thm)],[17775]) ).
thf(17777,plain,
( ( sk1 @ ( vd411 @ geq ) )
| ( sk1 @ ( v1 @ greater ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[17776:[bind(A,$thf( sk1 )),bind(B,$thf( vd411 ))]]) ).
thf(4506,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vplus ) @ greater ) )
!= ( C @ ( D @ greater ) ) )
| ( C @ ( D @ geq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[154,110]) ).
thf(4507,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vplus ) @ greater ) )
!= ( C @ ( D @ greater ) ) )
| ( C @ ( D @ geq ) ) ),
inference(simp,[status(thm)],[4506]) ).
thf(4508,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ vplus ) @ geq ) ),
inference(pattern_uni,[status(thm)],[4507:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ vplus ) ))]]) ).
thf(4510,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ vplus ) @ geq ) ),
inference(simp,[status(thm)],[4508]) ).
thf(6,axiom,
! [A: $i,B: $i] :
( ~ ( B @ ( A @ greater ) )
| ( A != B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 3)') ).
thf(72,plain,
! [A: $i,B: $i] :
( ~ ( B @ ( A @ greater ) )
| ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(177,plain,
! [A: $i] :
( ( ( A @ vsucc @ ( vd411 @ vsucc @ vmul ) )
= ( vd411 @ vsucc @ ( A @ ( vd411 @ vsucc @ vmul ) @ vplus ) ) )
| ( ( A @ ( vd411 @ vsucc @ vmul ) )
!= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) ) ),
inference(cnf,[status(esa)],[176]) ).
thf(178,plain,
! [A: $i] :
( ( ( vd411 @ vsucc @ ( A @ ( vd411 @ vsucc @ vmul ) @ vplus ) )
= ( A @ vsucc @ ( vd411 @ vsucc @ vmul ) ) )
| ( ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) )
!= ( A @ ( vd411 @ vsucc @ vmul ) ) ) ),
inference(lifteq,[status(thm)],[177]) ).
thf(11636,plain,
! [A: $i] :
( ( ( vd411 @ ( A @ ( vd411 @ vsucc @ vmul ) @ vplus ) @ vsucc )
= ( A @ vsucc @ ( vd411 @ vsucc @ vmul ) ) )
| ( ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) )
!= ( A @ ( vd411 @ vsucc @ vmul ) ) ) ),
inference(rewrite,[status(thm)],[178,122]) ).
thf(218,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ geq ) )
| ~ ( B @ ( A @ geq ) )
| ~ ( D @ ( C @ geq ) ) ),
inference(cnf,[status(esa)],[217]) ).
thf(793,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vsucc @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( B @ ( C @ less ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[462,67]) ).
thf(794,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vsucc @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( B @ ( C @ less ) ) ),
inference(simp,[status(thm)],[793]) ).
thf(795,plain,
! [A: $i] : ( A @ vsucc @ ( v1 @ less ) ),
inference(pattern_uni,[status(thm)],[794:[bind(A,$thf( D )),bind(B,$thf( D @ vsucc )),bind(C,$thf( v1 ))]]) ).
thf(803,plain,
! [A: $i] : ( A @ vsucc @ ( v1 @ less ) ),
inference(simp,[status(thm)],[795]) ).
thf(2842,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( v1 @ less ) )
!= ( C @ ( B @ less ) ) )
| ~ $true
| ~ ( C @ ( B @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[803,102]) ).
thf(2843,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( v1 @ less ) )
!= ( C @ ( B @ less ) ) )
| ~ ( C @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[2842]) ).
thf(2844,plain,
! [A: $i] :
~ ( A @ vsucc @ ( v1 @ greater ) ),
inference(pattern_uni,[status(thm)],[2843:[bind(A,$thf( D )),bind(B,$thf( v1 )),bind(C,$thf( D @ vsucc ))]]) ).
thf(2853,plain,
! [A: $i] :
~ ( A @ vsucc @ ( v1 @ greater ) ),
inference(simp,[status(thm)],[2844]) ).
thf(5191,plain,
! [B: $i,A: $i] :
( ( ( A @ vsucc @ ( A @ less ) )
!= ( B @ ( B @ vsucc @ less ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[974,2850]) ).
thf(5192,plain,
! [B: $i,A: $i] :
( ( A @ vsucc @ ( A @ less ) )
!= ( B @ ( B @ vsucc @ less ) ) ),
inference(simp,[status(thm)],[5191]) ).
thf(5219,plain,
! [B: $i,A: $i] :
( ( ( A @ vsucc )
!= B )
| ( A
!= ( B @ vsucc ) ) ),
inference(simp,[status(thm)],[5192]) ).
thf(5228,plain,
! [A: $i] :
( ( A @ vsucc @ vsucc )
!= A ),
inference(simp,[status(thm)],[5219]) ).
thf(73,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ greater ) )
| ( A != B ) ),
inference(cnf,[status(esa)],[72]) ).
thf(74,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ greater ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[73]) ).
thf(75,plain,
! [A: $i] :
~ ( A @ ( A @ greater ) ),
inference(simp,[status(thm)],[74]) ).
thf(52,axiom,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( A @ ( vd411 @ vsucc @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) )
= ( A @ ( vd411 @ vplus ) @ vsucc @ ( A @ ( vd411 @ vmul ) @ vplus ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(conseq(263), 1), 3)') ).
thf(246,plain,
! [A: $i] :
( ( ( A @ ( vd411 @ vsucc @ vmul ) )
= ( A @ ( A @ ( vd411 @ vmul ) @ vplus ) ) )
=> ( ( A @ ( vd411 @ vsucc @ vplus ) @ ( A @ ( vd411 @ vmul ) @ vplus ) )
= ( A @ ( vd411 @ vplus ) @ vsucc @ ( A @ ( vd411 @ vmul ) @ vplus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(432,plain,
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) )
!= ( sk1 @ ( vd411 @ vsucc @ vmul ) ) )
| ( ( sk1 @ ( vd411 @ vmul ) )
!= ( vd411 @ vsucc ) )
| ( sk1 != v1 ) ),
inference(paramod_ordered,[status(thm)],[380,427]) ).
thf(433,plain,
( ( ( sk1 @ ( vd411 @ vmul ) )
!= ( vd411 @ vsucc ) )
| ( sk1 != v1 ) ),
inference(pattern_uni,[status(thm)],[432:[]]) ).
thf(2383,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ ( vd411 @ vmul ) @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2107,71]) ).
thf(2384,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ ( vd411 @ vmul ) @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) ) ),
inference(simp,[status(thm)],[2383]) ).
thf(2385,plain,
sk1 @ ( vd411 @ vmul ) @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ geq ),
inference(pattern_uni,[status(thm)],[2384:[bind(A,$thf( sk1 @ ( vd411 @ vmul ) )),bind(B,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) ))]]) ).
thf(145,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ ( B @ sk4 ) @ ( A @ vplus ) ) )
| ( A
= ( A @ ( B @ sk3 ) @ ( B @ vplus ) ) )
| ( A = B ) ),
inference(cnf,[status(esa)],[144]) ).
thf(146,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ sk4 ) @ ( A @ vplus ) )
= B )
| ( ( A @ ( B @ sk3 ) @ ( B @ vplus ) )
= A )
| ( A = B ) ),
inference(lifteq,[status(thm)],[145]) ).
thf(5209,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( A @ less ) )
!= ( C @ ( C @ vsucc @ less ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[175,2850]) ).
thf(5210,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ ( A @ less ) )
!= ( C @ ( C @ vsucc @ less ) ) ),
inference(simp,[status(thm)],[5209]) ).
thf(5221,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) )
!= C )
| ( A
!= ( C @ vsucc ) ) ),
inference(simp,[status(thm)],[5210]) ).
thf(5230,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vsucc @ vplus ) )
!= B ),
inference(simp,[status(thm)],[5221]) ).
thf(21763,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) @ vsucc )
!= B ),
inference(rewrite,[status(thm)],[5230,216]) ).
thf(57,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ less ) )
=> ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ less ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(193), 0), 0)') ).
thf(268,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ less ) )
=> ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ less ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(6764,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( C @ ( B @ vplus ) ) )
| ( ( A @ vsucc @ ( B @ sk2 ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[124,6743]) ).
thf(6765,plain,
! [A: $i] :
( ( A @ vsucc @ ( A @ sk2 ) )
= v1 ),
inference(pattern_uni,[status(thm)],[6764:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( v1 ))]]) ).
thf(90,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ leq ) )
| ( B != A ) ),
inference(cnfConj,[status(thm)],[87]) ).
thf(93,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ leq ) )
| ( B != A ) ),
inference(lifteq,[status(thm)],[90]) ).
thf(94,plain,
! [A: $i] : ( A @ ( A @ leq ) ),
inference(simp,[status(thm)],[93]) ).
thf(6267,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ ( sk1 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ~ $true
| ( sk1 @ ( v1 @ less ) )
| ( sk1 @ ( v1 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[6004,71]) ).
thf(6268,plain,
! [B: $i,A: $i] :
( ( ( vd411 @ ( sk1 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ( sk1 @ ( v1 @ less ) )
| ( sk1 @ ( v1 @ greater ) ) ),
inference(simp,[status(thm)],[6267]) ).
thf(6269,plain,
( ( sk1 @ ( vd411 @ geq ) )
| ( sk1 @ ( v1 @ less ) )
| ( sk1 @ ( v1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[6268:[bind(A,$thf( sk1 )),bind(B,$thf( vd411 ))]]) ).
thf(9991,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ ( vd411 @ vmul ) @ vplus ) )
!= ( B @ ( A @ vplus ) ) )
| ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[64,6595]) ).
thf(9992,plain,
( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[9991:[bind(A,$thf( sk1 @ ( vd411 @ vmul ) )),bind(B,$thf( sk1 ))]]) ).
thf(250,plain,
( ! [A: $i,B: $i] :
( ? [C: $i] :
( B
= ( C @ ( A @ vplus ) ) )
=> ( A @ ( B @ greater ) ) )
& ! [A: $i,B: $i] :
( ( A @ ( B @ greater ) )
=> ? [C: $i] :
( B
= ( C @ ( A @ vplus ) ) ) ) ),
inference(miniscope,[status(thm)],[249]) ).
thf(251,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( D @ greater ) )
| ( D
!= ( E @ ( C @ vplus ) ) ) )
& ( ( B
= ( A @ ( B @ sk8 ) @ ( A @ vplus ) ) )
| ~ ( A @ ( B @ greater ) ) ) ),
inference(cnf,[status(esa)],[250]) ).
thf(252,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ ( B @ sk8 ) @ ( A @ vplus ) ) )
| ~ ( A @ ( B @ greater ) ) ),
inference(cnfConj,[status(thm)],[251]) ).
thf(254,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ greater ) )
| ( ( A @ ( B @ sk8 ) @ ( A @ vplus ) )
= B ) ),
inference(lifteq,[status(thm)],[252]) ).
thf(83,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less ) )
| ~ ( B @ ( A @ leq ) )
| ~ ( C @ ( B @ less ) ) ),
inference(cnfConj,[status(thm)],[82]) ).
thf(13155,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( C @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) ) )
| ( ( B @ vsucc @ ( A @ vmul ) @ vsucc )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[184,5860]) ).
thf(13156,plain,
( ( sk1 @ vsucc @ ( vd411 @ vsucc @ vmul ) @ vsucc )
!= sk1 ),
inference(pattern_uni,[status(thm)],[13155:[bind(A,$thf( vd411 @ vsucc )),bind(B,$thf( sk1 )),bind(C,$thf( vd411 @ vsucc ))]]) ).
thf(4891,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( sk1 @ ( vd411 @ vsucc @ geq ) )
| ( B != v1 )
| ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[78,2214]) ).
thf(4892,plain,
! [A: $i] :
( ( sk1 @ ( vd411 @ vsucc @ geq ) )
| ( A != v1 )
| ( A @ ( sk1 @ less ) )
| ( A @ ( sk1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[4891:[bind(A,$thf( sk1 ))]]) ).
thf(4949,plain,
( ( sk1 @ ( vd411 @ vsucc @ geq ) )
| ( v1 @ ( sk1 @ less ) )
| ( v1 @ ( sk1 @ greater ) ) ),
inference(simp,[status(thm)],[4892]) ).
thf(2830,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1898,102]) ).
thf(2831,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) ) ),
inference(simp,[status(thm)],[2830]) ).
thf(2832,plain,
~ ( sk1 @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ less ) ),
inference(pattern_uni,[status(thm)],[2831:[bind(A,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(B,$thf( sk1 ))]]) ).
thf(6766,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ ( vd411 @ vmul ) @ vplus ) )
!= ( B @ ( A @ vplus ) ) )
| ( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( A @ sk2 ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[64,6743]) ).
thf(6767,plain,
( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( sk1 @ ( vd411 @ vmul ) @ sk2 ) )
= sk1 ),
inference(pattern_uni,[status(thm)],[6766:[bind(A,$thf( sk1 @ ( vd411 @ vmul ) )),bind(B,$thf( sk1 ))]]) ).
thf(232,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) )
| ~ ( B @ ( A @ geq ) )
| ~ ( D @ ( C @ greater ) ) ),
inference(cnfConj,[status(thm)],[231]) ).
thf(10812,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ vplus ) )
!= ( C @ ( sk1 @ ( vd411 @ vsucc @ vmul ) @ vplus ) ) )
| ( ( B @ ( A @ vplus ) )
!= ( sk1 @ ( vd411 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[131,4650]) ).
thf(10813,plain,
! [A: $i] :
( ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( A @ vplus ) )
!= ( sk1 @ ( vd411 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[10812:[bind(A,$thf( A )),bind(B,$thf( sk1 @ ( vd411 @ vsucc @ vmul ) )),bind(C,$thf( A ))]]) ).
thf(921,plain,
! [A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( sk1 @ ( vd411 @ vmul ) ) )
| ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[186,860]) ).
thf(926,plain,
! [A: $i] :
( ( sk1 != v1 )
| ( A != vd411 )
| ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( A @ less ) ) ),
inference(simp,[status(thm)],[921]) ).
thf(940,plain,
( ( sk1 != v1 )
| ( sk1 @ ( vd411 @ vsucc @ vmul ) @ ( vd411 @ less ) ) ),
inference(simp,[status(thm)],[926]) ).
thf(63125,plain,
$false,
inference(e,[status(thm)],[69,101,249,10495,234,6374,365,138,1823,115,2808,2495,308,13886,217,276,13219,9565,13779,15885,4650,19455,153,2146,13238,5938,8165,257,4238,11426,5429,184,110,125,5338,189,14103,4551,8126,2852,14316,78,216,11314,164,5892,179,10623,6745,238,84,221,453,132,116,6327,206,147,6591,10494,233,4480,85,13141,5968,13956,102,7110,60,380,117,13265,2118,18609,334,1900,8211,952,260,70,2150,165,2705,13260,92,229,2826,97,1819,1079,974,224,2841,9333,141,7204,109,13782,124,1182,96,2851,173,129,4953,15934,11274,244,266,4476,2089,128,237,2788,4708,5138,856,64,2028,149,176,423,2849,5067,8092,6407,2817,204,259,191,402,13773,71,13054,3051,17480,144,18665,1765,159,187,2119,113,219,230,4805,17841,17098,1801,2802,271,274,2214,13064,10677,10675,81,451,76,103,1821,213,91,66,915,155,462,6769,6004,2928,6553,278,455,226,6027,241,80,2107,162,209,112,2927,1958,10016,194,150,95,2850,15817,6577,1053,67,199,17777,15883,6330,1898,154,4510,72,175,11636,2848,4651,218,2490,6743,5860,2853,2823,186,5228,114,75,13793,246,433,207,5837,214,2385,6007,4356,168,146,21763,210,136,4350,268,79,13738,6765,94,2783,6269,427,860,131,6595,9992,68,254,803,122,83,13156,4949,2832,6767,222,232,100,10813,940]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM845+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.12 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.22/0.49 % Computer : n015.cluster.edu
% 0.22/0.49 % Model : x86_64 x86_64
% 0.22/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.49 % Memory : 8046.5625MB
% 0.22/0.49 % OS : Linux 6.8.0-71-generic
% 0.22/0.49 % CPULimit : 300
% 0.22/0.49 % WCLimit : 300
% 0.22/0.49 % DateTime : Sat Sep 26 04:15:58 UTC 2026
% 0.22/0.50 % CPUTime :
% 0.22/0.50 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 1.41/1.35 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 2.30/1.70 % [INFO] Parsing done (344ms).
% 2.30/1.72 % [INFO] Running in sequential loop mode.
% 3.31/2.35 % [INFO] eprover registered as external prover.
% 3.31/2.36 % [INFO] Scanning for conjecture ...
% 3.66/2.52 % [INFO] Found a conjecture (or negated_conjecture) and 57 axioms. Running axiom selection ...
% 3.86/2.65 % [INFO] Axiom selection finished. Selected 57 axioms (removed 0 axioms).
% 4.08/2.79 % [INFO] Problem is first-order (TPTP FOF).
% 4.34/2.81 % [INFO] Type checking passed.
% 4.34/2.82 % [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 ...
% 126.61/30.46 % External prover 'e' found a proof!
% 126.61/30.46 % [INFO] Killing All external provers ...
% 126.61/30.47 % Time passed: 29752ms (effective reasoning time: 28731ms)
% 126.61/30.47 % 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)>
% 126.61/30.47 % Axioms used in derivation (57): ass(cond(223, 0), 0), ass(cond(6, 0), 0), ass(cond(conseq(263), 1), 6), def(cond(conseq(axiom(3)), 11), 1), def(cond(conseq(axiom(3)), 16), 1), ass(cond(228, 0), 0), ass(cond(goal(202), 0), 2), ass(cond(241, 0), 0), def(cond(conseq(axiom(3)), 12), 1), ass(cond(81, 0), 0), ass(cond(goal(193), 0), 0), ass(cond(goal(130), 0), 1), ass(cond(conseq(263), 1), 4), ass(cond(163, 0), 0), ass(cond(conseq(263), 1), 7), ass(cond(goal(177), 0), 0), ass(cond(goal(193), 0), 2), ass(cond(goal(88), 0), 1), ass(cond(goal(130), 0), 0), ass(cond(goal(130), 0), 3), ass(cond(goal(193), 0), 1), ass(cond(189, 0), 0), ass(cond(conseq(263), 1), 0), qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0))), ass(cond(goal(88), 0), 3), ass(cond(conseq(263), 1), 1), ass(cond(184, 0), 0), ass(cond(goal(88), 0), 2), ass(cond(147, 0), 0), qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0))), ass(cond(73, 0), 0), ass(cond(goal(88), 0), 0), def(cond(conseq(axiom(3)), 17), 1), holds(264, 412, 1), ass(cond(20, 0), 0), ass(cond(goal(202), 0), 1), ass(cond(goal(216), 0), 0), ass(cond(253, 0), 0), qu(antec(axiom(3)), imp(antec(axiom(3)))), ass(cond(209, 0), 0), ass(cond(52, 0), 0), ass(cond(158, 0), 0), ass(cond(conseq(263), 1), 2), ass(cond(234, 0), 0), ass(cond(33, 0), 0), qu(restrictor(axiom(1)), holds(scope(axiom(1)), 2, 0)), ass(cond(61, 0), 0), ass(cond(goal(130), 0), 2), holds(264, 412, 2), ass(cond(goal(202), 0), 0), holds(264, 412, 0), ass(cond(12, 0), 0), ass(cond(conseq(263), 1), 3), ass(cond(168, 0), 0), ass(cond(43, 0), 0), ass(cond(conseq(263), 1), 5), ass(cond(140, 0), 0)
% 126.61/30.47 % No. of inferences in proof: 660
% 126.61/30.47 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 29752 ms resp. 28731 ms w/o parsing
% 118.59/30.70 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 118.59/30.71 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------