%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : NUM856+2 : 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 : n009.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:13 AM UTC 2026
% Result : Theorem 90.19s 19.55s
% Output : Refutation 77.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 68
% Syntax : Number of formulae : 1020 ( 249 unt; 0 typ; 9 def)
% Number of atoms : 2946 (1537 equ; 0 cnn)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 8357 (1640 ~;1338 |; 49 &;5246 @)
% ( 4 <=>; 80 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 16 ( 16 >; 0 *; 0 +; 0 <<)
% Number of symbols : 25 ( 22 usr; 7 con; 0-2 aty)
% Number of variables : 1584 ( 8 ^;1532 !; 35 ?;1584 :)
% ( 0 !>; 0 ?*; 0 @-; 9 @+)
% Comments :
%------------------------------------------------------------------------------
thf(greater_decl,type,
greater: $i > $i > $o ).
thf(vmul_decl,type,
vmul: $i > $i > $i ).
thf(vd517_decl,type,
vd517: $i ).
thf(vd519_decl,type,
vd519: $i ).
thf(vd518_decl,type,
vd518: $i ).
thf(vd520_decl,type,
vd520: $i ).
thf(leq_decl,type,
leq: $i > $i > $o ).
thf(vplus_decl,type,
vplus: $i > $i > $i ).
thf(vsucc_decl,type,
vsucc: $i > $i ).
thf(v1_decl,type,
v1: $i ).
thf(less_decl,type,
less: $i > $i > $o ).
thf(geq_decl,type,
geq: $i > $i > $o ).
thf(vskolem2_decl,type,
vskolem2: $i > $i ).
thf(sk1_decl,type,
sk1: $i > $i > $i ).
thf(sk2_decl,type,
sk2: $i > $i > $i ).
thf(sk3_decl,type,
sk3: $i > $i > $i ).
thf(sk4_decl,type,
sk4: $i > $i ).
thf(sk5_decl,type,
sk5: $i > $i > $i ).
thf(sk6_decl,type,
sk6: $i > $i ).
thf(sk7_decl,type,
sk7: $i > $i > $i ).
thf(sk8_decl,type,
sk8: $i > $i > $i ).
thf(sk9_decl,type,
sk9: $i > $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i > $i > $i] :
! [B: $i,C: $i] :
( ( C @ ( B @ vplus ) @ ( B @ A ) )
= C ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( B
= ( C @ ( A @ vplus ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( A
= ( C @ ( B @ vplus ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i > $i] :
! [B: $i] :
( ( B @ vsucc @ A )
= B ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: $i > $i > $i] :
! [B: $i,C: $i] :
( ( C @ ( B @ vplus ) @ ( C @ A ) )
= B ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( @+[A: $i > $i] :
! [B: $i] :
( ( B @ vsucc @ A )
= B ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( B
= ( C @ ( A @ vplus ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( A
= ( C @ ( B @ vplus ) ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( @+[A: $i > $i > $i] :
! [B: $i,C: $i] :
( ( C @ ( B @ vmul ) @ ( C @ A ) )
= B ) ) ) ).
thf(4,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(64,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)],[4]) ).
thf(65,plain,
( ! [A: $i] :
( ( v1 @ ( A @ vplus ) )
= ( A @ vsucc ) )
& ! [A: $i,B: $i] :
( ( B @ vsucc @ ( A @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ) ),
inference(miniscope,[status(thm)],[64]) ).
thf(66,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( C @ vplus ) )
= ( C @ vsucc ) )
& ( ( B @ vsucc @ ( A @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ) ),
inference(cnf,[status(esa)],[65]) ).
thf(67,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ),
inference(cnfConj,[status(thm)],[66]) ).
thf(69,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ),
inference(lifteq,[status(thm)],[67]) ).
thf(31,axiom,
! [A: $i] :
( ( A @ ( v1 @ vplus ) )
= ( A @ vsucc ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(43, 0), 0)') ).
thf(176,plain,
! [A: $i] :
( ( A @ ( v1 @ vplus ) )
= ( A @ vsucc ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(177,plain,
! [A: $i] :
( ( A @ ( v1 @ vplus ) )
= ( A @ vsucc ) ),
inference(cnf,[status(esa)],[176]) ).
thf(178,plain,
! [A: $i] :
( ( A @ ( v1 @ vplus ) )
= ( A @ vsucc ) ),
inference(lifteq,[status(thm)],[177]) ).
thf(35,axiom,
! [A: $i,B: $i] : ( A @ ( B @ ( A @ vplus ) @ greater ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(189, 0), 0)') ).
thf(189,plain,
! [A: $i,B: $i] : ( A @ ( B @ ( A @ vplus ) @ greater ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(190,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ vplus ) @ greater ) ),
inference(cnf,[status(esa)],[189]) ).
thf(1021,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( v1 @ vplus ) )
!= ( C @ ( B @ vplus ) ) )
| ( B @ ( A @ vsucc @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[178,190]) ).
thf(1022,plain,
! [A: $i] : ( v1 @ ( A @ vsucc @ greater ) ),
inference(pattern_uni,[status(thm)],[1021:[bind(A,$thf( A )),bind(B,$thf( v1 )),bind(C,$thf( A ))]]) ).
thf(47,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(226,plain,
! [A: $i,B: $i] :
( ~ ( B @ ( A @ less ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(227,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ less ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(cnf,[status(esa)],[226]) ).
thf(19601,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vsucc @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ~ ( C @ ( B @ less ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1022,227]) ).
thf(19602,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vsucc @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ~ ( C @ ( B @ less ) ) ),
inference(simp,[status(thm)],[19601]) ).
thf(19603,plain,
! [A: $i] :
~ ( v1 @ ( A @ vsucc @ less ) ),
inference(pattern_uni,[status(thm)],[19602:[bind(A,$thf( D )),bind(B,$thf( D @ vsucc )),bind(C,$thf( v1 ))]]) ).
thf(19672,plain,
! [A: $i] :
~ ( v1 @ ( A @ vsucc @ less ) ),
inference(simp,[status(thm)],[19603]) ).
thf(6,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ vplus ) )
= ( B @ ( A @ vplus ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(61, 0), 0)') ).
thf(76,plain,
! [A: $i,B: $i] :
( ( A @ ( B @ vplus ) )
= ( B @ ( A @ vplus ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(77,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) )
= ( B @ ( A @ vplus ) ) ),
inference(cnf,[status(esa)],[76]) ).
thf(78,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) )
= ( B @ ( A @ vplus ) ) ),
inference(lifteq,[status(thm)],[77]) ).
thf(26,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(154,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)],[26]) ).
thf(155,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)],[154]) ).
thf(156,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( D @ less ) )
| ( C
!= ( E @ ( D @ vplus ) ) ) )
& ( ( A
= ( A @ ( B @ sk7 ) @ ( B @ vplus ) ) )
| ~ ( A @ ( B @ less ) ) ) ),
inference(cnf,[status(esa)],[155]) ).
thf(158,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ less ) )
| ( A
!= ( C @ ( B @ vplus ) ) ) ),
inference(cnfConj,[status(thm)],[156]) ).
thf(160,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ less ) )
| ( A
!= ( C @ ( B @ vplus ) ) ) ),
inference(lifteq,[status(thm)],[158]) ).
thf(161,plain,
! [B: $i,A: $i] : ( B @ ( A @ vplus ) @ ( A @ less ) ),
inference(simp,[status(thm)],[160]) ).
thf(666,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)],[78,161]) ).
thf(667,plain,
! [B: $i,A: $i] : ( B @ ( A @ vplus ) @ ( B @ less ) ),
inference(pattern_uni,[status(thm)],[666:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(15,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(104,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)],[15]) ).
thf(105,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)],[104]) ).
thf(106,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)],[105]) ).
thf(108,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ leq ) )
| ~ ( A @ ( B @ less ) ) ),
inference(cnfConj,[status(thm)],[106]) ).
thf(111,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ leq ) )
| ~ ( A @ ( B @ less ) ) ),
inference(simp,[status(thm)],[108]) ).
thf(4447,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( B @ less ) )
!= ( C @ ( D @ less ) ) )
| ( C @ ( D @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[667,111]) ).
thf(4448,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( B @ less ) )
!= ( C @ ( D @ less ) ) )
| ( C @ ( D @ leq ) ) ),
inference(simp,[status(thm)],[4447]) ).
thf(4449,plain,
! [B: $i,A: $i] : ( B @ ( A @ vplus ) @ ( B @ leq ) ),
inference(pattern_uni,[status(thm)],[4448:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ vplus ) )),bind(D,$thf( F ))]]) ).
thf(4450,plain,
! [B: $i,A: $i] : ( B @ ( A @ vplus ) @ ( B @ leq ) ),
inference(simp,[status(thm)],[4449]) ).
thf(13,axiom,
! [A: $i] :
( ( A != v1 )
=> ( A
= ( A @ vskolem2 @ vsucc ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(20, 0), 0)') ).
thf(99,plain,
! [A: $i] :
( ( A != v1 )
=> ( A
= ( A @ vskolem2 @ vsucc ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(100,plain,
! [A: $i] :
( ( A
= ( A @ vskolem2 @ vsucc ) )
| ( A = v1 ) ),
inference(cnf,[status(esa)],[99]) ).
thf(101,plain,
! [A: $i] :
( ( ( A @ vskolem2 @ vsucc )
= A )
| ( A = v1 ) ),
inference(lifteq,[status(thm)],[100]) ).
thf(51,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ vsucc @ vmul ) )
= ( B @ ( B @ ( A @ vmul ) @ vplus ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(261, 0), 0)') ).
thf(234,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ vsucc @ vmul ) )
= ( B @ ( B @ ( A @ vmul ) @ vplus ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(68,plain,
! [A: $i] :
( ( v1 @ ( A @ vplus ) )
= ( A @ vsucc ) ),
inference(cnfConj,[status(thm)],[66]) ).
thf(70,plain,
! [A: $i] :
( ( v1 @ ( A @ vplus ) )
= ( A @ vsucc ) ),
inference(lifteq,[status(thm)],[68]) ).
thf(71,plain,
! [A: $i] :
( ( v1 @ ( A @ vplus ) )
= ( A @ vsucc ) ),
inference(simp,[status(thm)],[70]) ).
thf(57,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ vplus ) @ ( A @ vmul ) )
= ( C @ ( A @ vmul ) @ ( B @ ( A @ vmul ) @ vplus ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(281, 0), 0)') ).
thf(260,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ vplus ) @ ( A @ vmul ) )
= ( C @ ( A @ vmul ) @ ( B @ ( A @ vmul ) @ vplus ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(261,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ vplus ) @ ( A @ vmul ) )
= ( C @ ( A @ vmul ) @ ( B @ ( A @ vmul ) @ vplus ) ) ),
inference(cnf,[status(esa)],[260]) ).
thf(262,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ vmul ) @ ( B @ ( A @ vmul ) @ vplus ) )
= ( C @ ( B @ vplus ) @ ( A @ vmul ) ) ),
inference(lifteq,[status(thm)],[261]) ).
thf(1,conjecture,
vd520 @ ( vd518 @ vmul ) @ ( vd519 @ ( vd517 @ vmul ) @ greater ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(conseq(scope(318)), 525, 0)') ).
thf(2,negated_conjecture,
~ ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(61,plain,
~ ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(1007,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vplus ) @ greater ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[190,61]) ).
thf(1008,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ vplus ) @ greater ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) ),
inference(simp,[status(thm)],[1007]) ).
thf(1034,plain,
! [B: $i,A: $i] :
( ( A
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( ( B @ ( A @ vplus ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(simp,[status(thm)],[1008]) ).
thf(1047,plain,
! [A: $i] :
( ( A @ ( vd520 @ ( vd518 @ vmul ) @ vplus ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(simp,[status(thm)],[1034]) ).
thf(27055,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ vmul ) @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( D @ ( vd520 @ ( vd518 @ vmul ) @ vplus ) ) )
| ( ( C @ ( B @ vplus ) @ ( A @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[262,1047]) ).
thf(27056,plain,
! [A: $i] :
( ( A @ ( vd520 @ vplus ) @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[27055:[bind(A,$thf( vd518 )),bind(B,$thf( vd520 )),bind(C,$thf( F )),bind(D,$thf( F @ ( vd518 @ vmul ) ))]]) ).
thf(27272,plain,
! [A: $i] :
( ( A @ ( vd520 @ vplus ) @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(simp,[status(thm)],[27056]) ).
thf(27310,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ vsucc @ ( A @ vplus ) )
!= ( C @ ( vd520 @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[69,27272]) ).
thf(27311,plain,
! [A: $i] :
( ( A @ ( vd520 @ vplus ) @ vsucc @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[27310:[bind(A,$thf( vd520 )),bind(B,$thf( D )),bind(C,$thf( D @ vsucc ))]]) ).
thf(27437,plain,
! [A: $i] :
( ( A @ ( vd520 @ vplus ) @ vsucc @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(simp,[status(thm)],[27311]) ).
thf(33340,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( B @ ( vd520 @ vplus ) ) )
| ( ( A @ vsucc @ vsucc @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[71,27437]) ).
thf(33341,plain,
( ( vd520 @ vsucc @ vsucc @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[33340:[bind(A,$thf( vd520 )),bind(B,$thf( v1 ))]]) ).
thf(9,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(85,plain,
! [A: $i,B: $i] :
( ( A != B )
=> ! [C: $i] :
( ( A @ ( C @ vplus ) )
!= ( B @ ( C @ vplus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(86,plain,
! [A: $i,B: $i] :
( ( A != B )
=> ~ ? [C: $i] :
( ( A @ ( C @ vplus ) )
= ( B @ ( C @ vplus ) ) ) ),
inference(miniscope,[status(thm)],[85]) ).
thf(87,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ vplus ) )
!= ( B @ ( C @ vplus ) ) )
| ( A = B ) ),
inference(cnf,[status(esa)],[86]) ).
thf(88,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ vplus ) )
!= ( B @ ( C @ vplus ) ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[87]) ).
thf(56,axiom,
! [A: $i] :
( ( A @ ( v1 @ vmul ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(253, 0), 0)') ).
thf(257,plain,
! [A: $i] :
( ( A @ ( v1 @ vmul ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(258,plain,
! [A: $i] :
( ( A @ ( v1 @ vmul ) )
= A ),
inference(cnf,[status(esa)],[257]) ).
thf(259,plain,
! [A: $i] :
( ( A @ ( v1 @ vmul ) )
= A ),
inference(lifteq,[status(thm)],[258]) ).
thf(39,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(198,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)],[39]) ).
thf(199,plain,
( ! [A: $i] :
( ( v1 @ ( A @ vmul ) )
= A )
& ! [A: $i,B: $i] :
( ( B @ vsucc @ ( A @ vmul ) )
= ( A @ ( B @ ( A @ vmul ) @ vplus ) ) ) ),
inference(miniscope,[status(thm)],[198]) ).
thf(200,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( C @ vmul ) )
= C )
& ( ( B @ vsucc @ ( A @ vmul ) )
= ( A @ ( B @ ( A @ vmul ) @ vplus ) ) ) ),
inference(cnf,[status(esa)],[199]) ).
thf(202,plain,
! [A: $i] :
( ( v1 @ ( A @ vmul ) )
= A ),
inference(cnfConj,[status(thm)],[200]) ).
thf(204,plain,
! [A: $i] :
( ( v1 @ ( A @ vmul ) )
= A ),
inference(lifteq,[status(thm)],[202]) ).
thf(205,plain,
! [A: $i] :
( ( v1 @ ( A @ vmul ) )
= A ),
inference(simp,[status(thm)],[204]) ).
thf(157,plain,
! [B: $i,A: $i] :
( ( A
= ( A @ ( B @ sk7 ) @ ( B @ vplus ) ) )
| ~ ( A @ ( B @ less ) ) ),
inference(cnfConj,[status(thm)],[156]) ).
thf(159,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ less ) )
| ( ( A @ ( B @ sk7 ) @ ( B @ vplus ) )
= A ) ),
inference(lifteq,[status(thm)],[157]) ).
thf(7684,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ sk7 ) @ ( B @ vplus ) )
!= ( C @ ( vd520 @ ( vd518 @ vmul ) @ vplus ) ) )
| ( A
!= ( vd519 @ ( vd517 @ vmul ) ) )
| ~ ( A @ ( B @ less ) ) ),
inference(paramod_ordered,[status(thm)],[159,1047]) ).
thf(7685,plain,
! [A: $i] :
( ( A
!= ( vd519 @ ( vd517 @ vmul ) ) )
| ~ ( A @ ( vd520 @ ( vd518 @ vmul ) @ less ) ) ),
inference(pattern_uni,[status(thm)],[7684:[bind(A,$thf( G )),bind(B,$thf( vd520 @ ( vd518 @ vmul ) )),bind(C,$thf( G @ ( vd520 @ ( vd518 @ vmul ) @ sk7 ) ))]]) ).
thf(7779,plain,
~ ( vd519 @ ( vd517 @ vmul ) @ ( vd520 @ ( vd518 @ vmul ) @ less ) ),
inference(simp,[status(thm)],[7685]) ).
thf(7863,plain,
! [A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) )
| ~ ( A @ ( vd520 @ ( vd518 @ vmul ) @ less ) ) ),
inference(paramod_ordered,[status(thm)],[205,7779]) ).
thf(7898,plain,
! [A: $i] :
( ( v1 != vd519 )
| ( A != vd517 )
| ~ ( A @ ( vd520 @ ( vd518 @ vmul ) @ less ) ) ),
inference(simp,[status(thm)],[7863]) ).
thf(7908,plain,
( ( v1 != vd519 )
| ~ ( vd517 @ ( vd520 @ ( vd518 @ vmul ) @ less ) ) ),
inference(simp,[status(thm)],[7898]) ).
thf(8151,plain,
! [A: $i] :
( ( ( A @ ( v1 @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( v1 != vd519 )
| ~ ( vd517 @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[259,7908]) ).
thf(8185,plain,
! [A: $i] :
( ( A != vd520 )
| ( v1 != vd518 )
| ( v1 != vd519 )
| ~ ( vd517 @ ( A @ less ) ) ),
inference(simp,[status(thm)],[8151]) ).
thf(8200,plain,
( ( v1 != vd518 )
| ( v1 != vd519 )
| ~ ( vd517 @ ( vd520 @ less ) ) ),
inference(simp,[status(thm)],[8185]) ).
thf(40,axiom,
( ( ( vd518 @ ( vd517 @ greater ) )
& ( vd520 @ ( vd519 @ geq ) ) )
| ( ( vd518 @ ( vd517 @ geq ) )
& ( vd520 @ ( vd519 @ greater ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dis(antec(scope(318)))') ).
thf(206,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
& ( vd520 @ ( vd519 @ geq ) ) )
| ( ( vd518 @ ( vd517 @ geq ) )
& ( vd520 @ ( vd519 @ greater ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(207,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
| ( vd518 @ ( vd517 @ geq ) ) )
& ( ( vd520 @ ( vd519 @ geq ) )
| ( vd518 @ ( vd517 @ geq ) ) )
& ( ( vd518 @ ( vd517 @ greater ) )
| ( vd520 @ ( vd519 @ greater ) ) )
& ( ( vd520 @ ( vd519 @ geq ) )
| ( vd520 @ ( vd519 @ greater ) ) ) ),
inference(cnf,[status(esa)],[206]) ).
thf(211,plain,
( ( vd518 @ ( vd517 @ greater ) )
| ( vd518 @ ( vd517 @ geq ) ) ),
inference(cnfConj,[status(thm)],[207]) ).
thf(14,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ geq ) )
=> ( A @ ( B @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(158, 0), 0)') ).
thf(102,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ geq ) )
=> ( A @ ( B @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(103,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ geq ) ) ),
inference(cnf,[status(esa)],[102]) ).
thf(2415,plain,
! [B: $i,A: $i] :
( ( ( vd518 @ ( vd517 @ geq ) )
!= ( B @ ( A @ geq ) ) )
| ( A @ ( B @ leq ) )
| ~ $true
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[211,103]) ).
thf(2416,plain,
! [B: $i,A: $i] :
( ( ( vd518 @ ( vd517 @ geq ) )
!= ( B @ ( A @ geq ) ) )
| ( A @ ( B @ leq ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[2415]) ).
thf(2417,plain,
( ( vd517 @ ( vd518 @ leq ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[2416:[bind(A,$thf( vd517 )),bind(B,$thf( vd518 ))]]) ).
thf(107,plain,
! [B: $i,A: $i] :
( ( B = A )
| ( A @ ( B @ less ) )
| ~ ( A @ ( B @ leq ) ) ),
inference(cnfConj,[status(thm)],[106]) ).
thf(110,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ less ) )
| ~ ( A @ ( B @ leq ) )
| ( B = A ) ),
inference(lifteq,[status(thm)],[107]) ).
thf(3589,plain,
! [B: $i,A: $i] :
( ( ( vd517 @ ( vd518 @ leq ) )
!= ( A @ ( B @ leq ) ) )
| ( A @ ( B @ less ) )
| ~ $true
| ( B = A )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[2417,110]) ).
thf(3590,plain,
! [B: $i,A: $i] :
( ( ( vd517 @ ( vd518 @ leq ) )
!= ( A @ ( B @ leq ) ) )
| ( A @ ( B @ less ) )
| ( B = A )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[3589]) ).
thf(3591,plain,
( ( vd517 @ ( vd518 @ less ) )
| ( vd518 = vd517 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[3590:[bind(A,$thf( vd517 )),bind(B,$thf( vd518 ))]]) ).
thf(50,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ less ) )
=> ( A @ ( B @ greater ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(147, 0), 0)') ).
thf(232,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ less ) )
=> ( A @ ( B @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(233,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ greater ) )
| ~ ( B @ ( A @ less ) ) ),
inference(cnf,[status(esa)],[232]) ).
thf(21530,plain,
! [B: $i,A: $i] :
( ( ( vd517 @ ( vd518 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( A @ ( B @ greater ) )
| ~ $true
| ( vd518 = vd517 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[3591,233]) ).
thf(21531,plain,
! [B: $i,A: $i] :
( ( ( vd517 @ ( vd518 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( A @ ( B @ greater ) )
| ( vd518 = vd517 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[21530]) ).
thf(21532,plain,
( ( vd518 @ ( vd517 @ greater ) )
| ( vd518 = vd517 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[21531:[bind(A,$thf( vd518 )),bind(B,$thf( vd517 ))]]) ).
thf(21582,plain,
( ( vd518 = vd517 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[21532]) ).
thf(209,plain,
( ( vd518 @ ( vd517 @ greater ) )
| ( vd520 @ ( vd519 @ greater ) ) ),
inference(cnfConj,[status(thm)],[207]) ).
thf(1451,plain,
! [B: $i,A: $i] :
( ( ( A @ vskolem2 @ vsucc )
!= ( B @ vsucc ) )
| ( v1 @ ( A @ greater ) )
| ( A = v1 ) ),
inference(paramod_ordered,[status(thm)],[101,1022]) ).
thf(1452,plain,
! [A: $i] :
( ( v1 @ ( A @ greater ) )
| ( A = v1 ) ),
inference(pattern_uni,[status(thm)],[1451:[bind(A,$thf( C )),bind(B,$thf( C @ vskolem2 ))]]) ).
thf(1505,plain,
! [A: $i] :
( ( v1 @ ( A @ greater ) )
| ( A = v1 ) ),
inference(simp,[status(thm)],[1452]) ).
thf(301,plain,
! [A: $i] :
( ( ( A @ ( v1 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) )
| ~ ( vd520 @ ( vd518 @ vmul ) @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[259,61]) ).
thf(307,plain,
! [A: $i] :
( ( A != vd519 )
| ( v1 != vd517 )
| ~ ( vd520 @ ( vd518 @ vmul ) @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[301]) ).
thf(309,plain,
( ( v1 != vd517 )
| ~ ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ greater ) ) ),
inference(simp,[status(thm)],[307]) ).
thf(340,plain,
! [A: $i] :
( ( ( A @ ( v1 @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( v1 != vd517 )
| ~ ( A @ ( vd519 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[259,309]) ).
thf(344,plain,
! [A: $i] :
( ( A != vd520 )
| ( v1 != vd518 )
| ( v1 != vd517 )
| ~ ( A @ ( vd519 @ greater ) ) ),
inference(simp,[status(thm)],[340]) ).
thf(347,plain,
( ( v1 != vd518 )
| ( v1 != vd517 )
| ~ ( vd520 @ ( vd519 @ greater ) ) ),
inference(simp,[status(thm)],[344]) ).
thf(465,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ( v1 != vd518 )
| ( v1 != vd517 )
| ~ $true
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[209,347]) ).
thf(466,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ( v1 != vd518 )
| ( v1 != vd517 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[465]) ).
thf(467,plain,
( ( v1 != vd518 )
| ( v1 != vd517 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[466:[]]) ).
thf(52,axiom,
! [A: $i,B: $i] :
( ~ ( B @ ( A @ greater ) )
| ( A != B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 3)') ).
thf(237,plain,
! [A: $i,B: $i] :
( ~ ( B @ ( A @ greater ) )
| ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(238,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ greater ) )
| ( A != B ) ),
inference(cnf,[status(esa)],[237]) ).
thf(239,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ greater ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[238]) ).
thf(240,plain,
! [A: $i] :
~ ( A @ ( A @ greater ) ),
inference(simp,[status(thm)],[239]) ).
thf(554,plain,
! [A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ~ $true
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(paramod_ordered,[status(thm)],[467,240]) ).
thf(555,plain,
! [A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[554]) ).
thf(562,plain,
! [A: $i] :
( ( vd518 != A )
| ( vd517 != A )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[555]) ).
thf(571,plain,
( ( vd518 != vd517 )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[562]) ).
thf(2106,plain,
! [A: $i] :
( ( v1 != v1 )
| ( vd518 != vd517 )
| ( v1 != vd518 )
| ( A != vd517 )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,571]) ).
thf(2107,plain,
! [A: $i] :
( ( vd518 != vd517 )
| ( v1 != vd518 )
| ( A != vd517 )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[2106:[]]) ).
thf(2263,plain,
( ( vd518 != vd517 )
| ( v1 != vd518 )
| ( v1 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[2107]) ).
thf(36,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( B @ ( A @ greater ) )
& ( D @ ( C @ greater ) ) )
=> ( D @ ( B @ vmul ) @ ( C @ ( A @ vmul ) @ greater ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(312, 0), 0)') ).
thf(191,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( B @ ( A @ greater ) )
& ( D @ ( C @ greater ) ) )
=> ( D @ ( B @ vmul ) @ ( C @ ( A @ vmul ) @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(192,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ vmul ) @ ( C @ ( A @ vmul ) @ greater ) )
| ~ ( B @ ( A @ greater ) )
| ~ ( D @ ( C @ greater ) ) ),
inference(cnf,[status(esa)],[191]) ).
thf(9983,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( B @ vmul ) @ ( C @ ( A @ vmul ) @ greater ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) )
| ~ $true
| ~ ( B @ ( A @ greater ) )
| ~ ( D @ ( C @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[192,61]) ).
thf(9984,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( B @ vmul ) @ ( C @ ( A @ vmul ) @ greater ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) )
| ~ ( B @ ( A @ greater ) )
| ~ ( D @ ( C @ greater ) ) ),
inference(simp,[status(thm)],[9983]) ).
thf(9985,plain,
( ~ ( vd518 @ ( vd517 @ greater ) )
| ~ ( vd520 @ ( vd519 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[9984:[bind(A,$thf( vd517 )),bind(B,$thf( vd518 )),bind(C,$thf( vd519 )),bind(D,$thf( vd520 ))]]) ).
thf(10354,plain,
( ( ( v1 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ~ $true
| ~ ( vd520 @ ( vd519 @ greater ) )
| ( vd518 != vd517 )
| ( v1 != vd518 ) ),
inference(paramod_ordered,[status(thm)],[2263,9985]) ).
thf(10355,plain,
( ( ( v1 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ~ ( vd520 @ ( vd519 @ greater ) )
| ( vd518 != vd517 )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[10354]) ).
thf(10534,plain,
( ( v1 != vd518 )
| ( vd517 != vd517 )
| ~ ( vd520 @ ( vd519 @ greater ) )
| ( vd518 != vd517 )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[10355]) ).
thf(10554,plain,
( ~ ( vd520 @ ( vd519 @ greater ) )
| ( vd518 != vd517 )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[10534]) ).
thf(15915,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ~ $true
| ( vd518 != vd517 )
| ( v1 != vd518 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[209,10554]) ).
thf(15916,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ( vd518 != vd517 )
| ( v1 != vd518 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[15915]) ).
thf(15917,plain,
( ( vd518 != vd517 )
| ( v1 != vd518 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[15916:[]]) ).
thf(19403,plain,
! [A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ~ $true
| ( vd518 != vd517 )
| ( v1 != vd518 ) ),
inference(paramod_ordered,[status(thm)],[15917,240]) ).
thf(19404,plain,
! [A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ( vd518 != vd517 )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[19403]) ).
thf(19465,plain,
! [A: $i] :
( ( vd518 != A )
| ( vd517 != A )
| ( vd518 != vd517 )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[19404]) ).
thf(19485,plain,
( ( vd518 != vd517 )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[19465]) ).
thf(22912,plain,
( ( vd518 != vd518 )
| ( vd517 != vd517 )
| ( v1 != vd518 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[21582,19485]) ).
thf(22913,plain,
( ( vd518 != vd518 )
| ( v1 != vd518 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[22912]) ).
thf(22914,plain,
( ( v1 != vd518 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[22913:[]]) ).
thf(295,plain,
! [A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) )
| ~ ( vd520 @ ( vd518 @ vmul ) @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[205,61]) ).
thf(297,plain,
! [A: $i] :
( ( v1 != vd519 )
| ( A != vd517 )
| ~ ( vd520 @ ( vd518 @ vmul ) @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[295]) ).
thf(299,plain,
( ( v1 != vd519 )
| ~ ( vd520 @ ( vd518 @ vmul ) @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[297]) ).
thf(313,plain,
! [A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( v1 != vd519 )
| ~ ( A @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[205,299]) ).
thf(315,plain,
! [A: $i] :
( ( v1 != vd520 )
| ( A != vd518 )
| ( v1 != vd519 )
| ~ ( A @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[313]) ).
thf(317,plain,
( ( v1 != vd520 )
| ( v1 != vd519 )
| ~ ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[315]) ).
thf(24263,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( v1 != vd520 )
| ( v1 != vd519 )
| ~ $true
| ( v1 != vd518 ) ),
inference(paramod_ordered,[status(thm)],[22914,317]) ).
thf(24264,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( v1 != vd520 )
| ( v1 != vd519 )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[24263]) ).
thf(24265,plain,
( ( v1 != vd520 )
| ( v1 != vd519 )
| ( v1 != vd518 ) ),
inference(pattern_uni,[status(thm)],[24264:[]]) ).
thf(19530,plain,
! [A: $i] :
( ( v1 != v1 )
| ( vd518 != vd517 )
| ( A != vd518 )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,19485]) ).
thf(19531,plain,
! [A: $i] :
( ( vd518 != vd517 )
| ( A != vd518 )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[19530:[]]) ).
thf(19540,plain,
( ( vd518 != vd517 )
| ( v1 @ ( vd518 @ greater ) ) ),
inference(simp,[status(thm)],[19531]) ).
thf(324,plain,
( ( ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ ( vd517 @ vmul ) @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ~ $true
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[209,61]) ).
thf(325,plain,
( ( ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ ( vd517 @ vmul ) @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[324]) ).
thf(333,plain,
( ( ( vd520 @ ( vd518 @ vmul ) )
!= vd520 )
| ( ( vd519 @ ( vd517 @ vmul ) )
!= vd519 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[325]) ).
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(249,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(29,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(170,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)],[29]) ).
thf(42,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ vmul ) )
= ( A @ ( B @ vmul ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(270, 0), 0)') ).
thf(214,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ vmul ) )
= ( A @ ( B @ vmul ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(215,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vmul ) )
= ( A @ ( B @ vmul ) ) ),
inference(cnf,[status(esa)],[214]) ).
thf(216,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vmul ) )
= ( A @ ( B @ vmul ) ) ),
inference(lifteq,[status(thm)],[215]) ).
thf(235,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vmul ) )
= ( B @ ( B @ ( A @ vmul ) @ vplus ) ) ),
inference(cnf,[status(esa)],[234]) ).
thf(236,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ vmul ) @ vplus ) )
= ( B @ ( A @ vsucc @ vmul ) ) ),
inference(lifteq,[status(thm)],[235]) ).
thf(22265,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( C @ ( vd520 @ ( vd518 @ vmul ) @ vplus ) ) )
| ( ( B @ ( A @ vsucc @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[236,1047]) ).
thf(22266,plain,
( ( vd520 @ ( vd518 @ vsucc @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[22265:[bind(A,$thf( vd518 )),bind(B,$thf( vd520 )),bind(C,$thf( vd520 ))]]) ).
thf(22479,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ vmul ) )
!= ( vd520 @ ( vd518 @ vsucc @ vmul ) ) )
| ( ( A @ ( B @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[216,22266]) ).
thf(22480,plain,
( ( vd518 @ vsucc @ ( vd520 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[22479:[bind(A,$thf( vd518 @ vsucc )),bind(B,$thf( vd520 ))]]) ).
thf(58,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(263,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)],[58]) ).
thf(264,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)],[263]) ).
thf(265,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)],[264]) ).
thf(266,plain,
! [B: $i,A: $i] :
( ( B = A )
| ( A @ ( B @ greater ) )
| ~ ( A @ ( B @ geq ) ) ),
inference(cnfConj,[status(thm)],[265]) ).
thf(269,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ greater ) )
| ~ ( A @ ( B @ geq ) )
| ( B = A ) ),
inference(lifteq,[status(thm)],[266]) ).
thf(43,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(217,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)],[43]) ).
thf(60,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(276,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)],[60]) ).
thf(1011,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( C @ ( B @ vplus ) ) )
| ( B @ ( A @ vsucc @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[71,190]) ).
thf(1012,plain,
! [A: $i] : ( A @ ( A @ vsucc @ greater ) ),
inference(pattern_uni,[status(thm)],[1011:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( v1 ))]]) ).
thf(312,plain,
! [A: $i] :
( ( ( A @ ( v1 @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( v1 != vd519 )
| ~ ( A @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[259,299]) ).
thf(314,plain,
! [A: $i] :
( ( A != vd520 )
| ( v1 != vd518 )
| ( v1 != vd519 )
| ~ ( A @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[312]) ).
thf(316,plain,
( ( v1 != vd518 )
| ( v1 != vd519 )
| ~ ( vd520 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[314]) ).
thf(1238,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd520 @ ( vd517 @ greater ) ) )
| ( v1 != vd518 )
| ( v1 != vd519 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1012,316]) ).
thf(1239,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd520 @ ( vd517 @ greater ) ) )
| ( v1 != vd518 )
| ( v1 != vd519 ) ),
inference(simp,[status(thm)],[1238]) ).
thf(1263,plain,
! [A: $i] :
( ( A != vd520 )
| ( ( A @ vsucc )
!= vd517 )
| ( v1 != vd518 )
| ( v1 != vd519 ) ),
inference(simp,[status(thm)],[1239]) ).
thf(1275,plain,
( ( ( vd520 @ vsucc )
!= vd517 )
| ( v1 != vd518 )
| ( v1 != vd519 ) ),
inference(simp,[status(thm)],[1263]) ).
thf(1305,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ vsucc @ ( A @ vplus ) )
!= ( C @ ( vd520 @ ( vd518 @ vmul ) @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[69,1047]) ).
thf(1306,plain,
! [A: $i] :
( ( A @ ( vd520 @ ( vd518 @ vmul ) @ vplus ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[1305:[bind(A,$thf( vd520 @ ( vd518 @ vmul ) )),bind(B,$thf( F )),bind(C,$thf( F @ vsucc ))]]) ).
thf(1327,plain,
! [A: $i] :
( ( A @ ( vd520 @ ( vd518 @ vmul ) @ vplus ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(simp,[status(thm)],[1306]) ).
thf(19583,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)],[161,227]) ).
thf(19584,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( A @ less ) )
!= ( D @ ( C @ less ) ) )
| ~ ( D @ ( C @ greater ) ) ),
inference(simp,[status(thm)],[19583]) ).
thf(19585,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ vplus ) @ ( A @ greater ) ),
inference(pattern_uni,[status(thm)],[19584:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ vplus ) ))]]) ).
thf(19668,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ vplus ) @ ( A @ greater ) ),
inference(simp,[status(thm)],[19585]) ).
thf(25,axiom,
! [A: $i,B: $i] :
( B
!= ( B @ ( A @ vplus ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(73, 0), 0)') ).
thf(150,plain,
! [A: $i,B: $i] :
( B
!= ( B @ ( A @ vplus ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(151,plain,
~ ? [A: $i,B: $i] :
( B
= ( B @ ( A @ vplus ) ) ),
inference(miniscope,[status(thm)],[150]) ).
thf(152,plain,
! [B: $i,A: $i] :
( B
!= ( B @ ( A @ vplus ) ) ),
inference(cnf,[status(esa)],[151]) ).
thf(153,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) )
!= B ),
inference(lifteq,[status(thm)],[152]) ).
thf(4441,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)],[161,111]) ).
thf(4442,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( A @ less ) )
!= ( C @ ( D @ less ) ) )
| ( C @ ( D @ leq ) ) ),
inference(simp,[status(thm)],[4441]) ).
thf(4443,plain,
! [B: $i,A: $i] : ( B @ ( A @ vplus ) @ ( A @ leq ) ),
inference(pattern_uni,[status(thm)],[4442:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ vplus ) )),bind(D,$thf( E ))]]) ).
thf(4452,plain,
! [B: $i,A: $i] : ( B @ ( A @ vplus ) @ ( A @ leq ) ),
inference(simp,[status(thm)],[4443]) ).
thf(12,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
=> ( A @ ( B @ geq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(163, 0), 0)') ).
thf(97,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
=> ( A @ ( B @ geq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(98,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ geq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(cnf,[status(esa)],[97]) ).
thf(10321,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( A @ leq ) )
!= ( D @ ( C @ leq ) ) )
| ( C @ ( D @ geq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4452,98]) ).
thf(10322,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( A @ leq ) )
!= ( D @ ( C @ leq ) ) )
| ( C @ ( D @ geq ) ) ),
inference(simp,[status(thm)],[10321]) ).
thf(10323,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ vplus ) @ geq ) ),
inference(pattern_uni,[status(thm)],[10322:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ vplus ) ))]]) ).
thf(10341,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ vplus ) @ geq ) ),
inference(simp,[status(thm)],[10323]) ).
thf(55,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( B @ ( A @ vmul ) )
= ( B @ ( C @ vmul ) ) )
=> ( A = C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(conjunct1(conjunct2(307)), 0), 0)') ).
thf(252,plain,
! [A: $i,B: $i,C: $i] :
( ( ( B @ ( A @ vmul ) )
= ( B @ ( C @ vmul ) ) )
=> ( A = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(253,plain,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ( ( B @ ( A @ vmul ) )
!= ( B @ ( C @ vmul ) ) ) ),
inference(cnf,[status(esa)],[252]) ).
thf(254,plain,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ( ( B @ ( A @ vmul ) )
!= ( B @ ( C @ vmul ) ) ) ),
inference(lifteq,[status(thm)],[253]) ).
thf(255,plain,
? [A: $i > $i > $i] :
! [B: $i,C: $i] :
( ( C @ ( B @ vmul ) @ ( C @ A ) )
= B ),
inference(detectInverse,[status(thm)],[254]) ).
thf(256,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vmul ) @ ( B @ sk9 ) )
= A ),
inference(cnf,[status(esa)],[255]) ).
thf(26472,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vmul ) @ ( B @ sk9 ) )
= A ),
inference(lifteq,[status(thm)],[256]) ).
thf(26487,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( C @ ( B @ vmul ) ) )
| ( ( A @ ( C @ sk9 ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[205,26472]) ).
thf(26488,plain,
! [A: $i] :
( ( A @ ( v1 @ sk9 ) )
= A ),
inference(pattern_uni,[status(thm)],[26487:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( v1 ))]]) ).
thf(34,axiom,
! [A: $i,B: $i,C: $i] :
( ( B = C )
=> ( ( A @ ( B @ vmul ) )
= ( A @ ( C @ vmul ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(299, 0), 1)') ).
thf(185,plain,
! [A: $i,B: $i,C: $i] :
( ( B = C )
=> ( ( A @ ( B @ vmul ) )
= ( A @ ( C @ vmul ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(208,plain,
( ( vd520 @ ( vd519 @ geq ) )
| ( vd520 @ ( vd519 @ greater ) ) ),
inference(cnfConj,[status(thm)],[207]) ).
thf(2424,plain,
! [B: $i,A: $i] :
( ( ( vd520 @ ( vd519 @ geq ) )
!= ( B @ ( A @ geq ) ) )
| ( A @ ( B @ leq ) )
| ~ $true
| ( vd520 @ ( vd519 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[208,103]) ).
thf(2425,plain,
! [B: $i,A: $i] :
( ( ( vd520 @ ( vd519 @ geq ) )
!= ( B @ ( A @ geq ) ) )
| ( A @ ( B @ leq ) )
| ( vd520 @ ( vd519 @ greater ) ) ),
inference(simp,[status(thm)],[2424]) ).
thf(2426,plain,
( ( vd519 @ ( vd520 @ leq ) )
| ( vd520 @ ( vd519 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[2425:[bind(A,$thf( vd519 )),bind(B,$thf( vd520 ))]]) ).
thf(4298,plain,
! [B: $i,A: $i] :
( ( ( vd519 @ ( vd520 @ leq ) )
!= ( A @ ( B @ leq ) ) )
| ( A @ ( B @ less ) )
| ~ $true
| ( B = A )
| ( vd520 @ ( vd519 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[2426,110]) ).
thf(4299,plain,
! [B: $i,A: $i] :
( ( ( vd519 @ ( vd520 @ leq ) )
!= ( A @ ( B @ leq ) ) )
| ( A @ ( B @ less ) )
| ( B = A )
| ( vd520 @ ( vd519 @ greater ) ) ),
inference(simp,[status(thm)],[4298]) ).
thf(4300,plain,
( ( vd519 @ ( vd520 @ less ) )
| ( vd520 = vd519 )
| ( vd520 @ ( vd519 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[4299:[bind(A,$thf( vd519 )),bind(B,$thf( vd520 ))]]) ).
thf(21548,plain,
! [B: $i,A: $i] :
( ( ( vd519 @ ( vd520 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( A @ ( B @ greater ) )
| ~ $true
| ( vd520 = vd519 )
| ( vd520 @ ( vd519 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[4300,233]) ).
thf(21549,plain,
! [B: $i,A: $i] :
( ( ( vd519 @ ( vd520 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( A @ ( B @ greater ) )
| ( vd520 = vd519 )
| ( vd520 @ ( vd519 @ greater ) ) ),
inference(simp,[status(thm)],[21548]) ).
thf(21550,plain,
( ( vd520 @ ( vd519 @ greater ) )
| ( vd520 = vd519 )
| ( vd520 @ ( vd519 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[21549:[bind(A,$thf( vd520 )),bind(B,$thf( vd519 ))]]) ).
thf(21578,plain,
( ( vd520 = vd519 )
| ( vd520 @ ( vd519 @ greater ) ) ),
inference(simp,[status(thm)],[21550]) ).
thf(21696,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ~ ( vd518 @ ( vd517 @ greater ) )
| ~ $true
| ( vd520 = vd519 ) ),
inference(paramod_ordered,[status(thm)],[21578,9985]) ).
thf(21697,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ~ ( vd518 @ ( vd517 @ greater ) )
| ( vd520 = vd519 ) ),
inference(simp,[status(thm)],[21696]) ).
thf(21698,plain,
( ~ ( vd518 @ ( vd517 @ greater ) )
| ( vd520 = vd519 ) ),
inference(pattern_uni,[status(thm)],[21697:[]]) ).
thf(24312,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ~ $true
| ( vd520 = vd519 )
| ( v1 != vd518 ) ),
inference(paramod_ordered,[status(thm)],[22914,21698]) ).
thf(24313,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( vd520 = vd519 )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[24312]) ).
thf(24314,plain,
( ( vd520 = vd519 )
| ( v1 != vd518 ) ),
inference(pattern_uni,[status(thm)],[24313:[]]) ).
thf(24403,plain,
! [A: $i] :
( ( v1 != v1 )
| ( vd520 = vd519 )
| ( A != vd518 )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,24314]) ).
thf(24404,plain,
! [A: $i] :
( ( vd520 = vd519 )
| ( A != vd518 )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[24403:[]]) ).
thf(24406,plain,
( ( vd520 = vd519 )
| ( v1 @ ( vd518 @ greater ) ) ),
inference(simp,[status(thm)],[24404]) ).
thf(26962,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( vd518 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ~ $true
| ( vd520 = vd519 ) ),
inference(paramod_ordered,[status(thm)],[24406,227]) ).
thf(26963,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( vd518 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ( vd520 = vd519 ) ),
inference(simp,[status(thm)],[26962]) ).
thf(26964,plain,
( ~ ( v1 @ ( vd518 @ less ) )
| ( vd520 = vd519 ) ),
inference(pattern_uni,[status(thm)],[26963:[bind(A,$thf( vd518 )),bind(B,$thf( v1 ))]]) ).
thf(330,plain,
! [A: $i] :
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ~ $true
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[209,240]) ).
thf(331,plain,
! [A: $i] :
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[330]) ).
thf(336,plain,
! [A: $i] :
( ( vd520 != A )
| ( vd519 != A )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[331]) ).
thf(339,plain,
( ( vd520 != vd519 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[336]) ).
thf(10392,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ~ ( vd518 @ ( vd517 @ greater ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1012,9985]) ).
thf(10393,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ~ ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[10392]) ).
thf(10515,plain,
! [A: $i] :
( ( A != vd520 )
| ( ( A @ vsucc )
!= vd519 )
| ~ ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[10393]) ).
thf(10545,plain,
( ( ( vd520 @ vsucc )
!= vd519 )
| ~ ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[10515]) ).
thf(42164,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( ( vd520 @ vsucc )
!= vd519 )
| ~ $true
| ( vd520 != vd519 ) ),
inference(paramod_ordered,[status(thm)],[339,10545]) ).
thf(42165,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( ( vd520 @ vsucc )
!= vd519 )
| ( vd520 != vd519 ) ),
inference(simp,[status(thm)],[42164]) ).
thf(42166,plain,
( ( ( vd520 @ vsucc )
!= vd519 )
| ( vd520 != vd519 ) ),
inference(pattern_uni,[status(thm)],[42165:[]]) ).
thf(210,plain,
( ( vd520 @ ( vd519 @ geq ) )
| ( vd518 @ ( vd517 @ geq ) ) ),
inference(cnfConj,[status(thm)],[207]) ).
thf(2430,plain,
! [B: $i,A: $i] :
( ( ( vd520 @ ( vd519 @ geq ) )
!= ( B @ ( A @ geq ) ) )
| ( A @ ( B @ leq ) )
| ~ $true
| ( vd518 @ ( vd517 @ geq ) ) ),
inference(paramod_ordered,[status(thm)],[210,103]) ).
thf(2431,plain,
! [B: $i,A: $i] :
( ( ( vd520 @ ( vd519 @ geq ) )
!= ( B @ ( A @ geq ) ) )
| ( A @ ( B @ leq ) )
| ( vd518 @ ( vd517 @ geq ) ) ),
inference(simp,[status(thm)],[2430]) ).
thf(2432,plain,
( ( vd519 @ ( vd520 @ leq ) )
| ( vd518 @ ( vd517 @ geq ) ) ),
inference(pattern_uni,[status(thm)],[2431:[bind(A,$thf( vd519 )),bind(B,$thf( vd520 ))]]) ).
thf(1528,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( B @ ( vd520 @ ( vd518 @ vmul ) @ vplus ) ) )
| ( ( A @ vsucc @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[71,1327]) ).
thf(1529,plain,
( ( vd520 @ ( vd518 @ vmul ) @ vsucc @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[1528:[bind(A,$thf( vd520 @ ( vd518 @ vmul ) )),bind(B,$thf( v1 ))]]) ).
thf(1560,plain,
! [A: $i] :
( ( ( A @ ( v1 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) )
| ( A
!= ( vd520 @ ( vd518 @ vmul ) @ vsucc @ vsucc ) ) ),
inference(paramod_ordered,[status(thm)],[259,1529]) ).
thf(1563,plain,
( ( ( vd520 @ ( vd518 @ vmul ) @ vsucc @ vsucc )
!= vd519 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[1560]) ).
thf(4350,plain,
! [A: $i] :
( ( ( A @ ( v1 @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( ( A @ vsucc @ vsucc )
!= vd519 )
| ( v1 != vd517 ) ),
inference(paramod_ordered,[status(thm)],[259,1563]) ).
thf(4366,plain,
! [A: $i] :
( ( A != vd520 )
| ( v1 != vd518 )
| ( ( A @ vsucc @ vsucc )
!= vd519 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[4350]) ).
thf(4371,plain,
( ( v1 != vd518 )
| ( ( vd520 @ vsucc @ vsucc )
!= vd519 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[4366]) ).
thf(201,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vmul ) )
= ( A @ ( B @ ( A @ vmul ) @ vplus ) ) ),
inference(cnfConj,[status(thm)],[200]) ).
thf(203,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ vmul ) @ vplus ) )
= ( B @ vsucc @ ( A @ vmul ) ) ),
inference(lifteq,[status(thm)],[201]) ).
thf(15445,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( C @ ( vd520 @ ( vd518 @ vmul ) @ vplus ) ) )
| ( ( B @ vsucc @ ( A @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[203,1047]) ).
thf(15446,plain,
( ( vd520 @ vsucc @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[15445:[bind(A,$thf( vd518 )),bind(B,$thf( vd520 )),bind(C,$thf( vd518 ))]]) ).
thf(15621,plain,
! [A: $i] :
( ( ( A @ vskolem2 @ vsucc )
!= ( vd520 @ vsucc ) )
| ( ( A @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) )
| ( A = v1 ) ),
inference(paramod_ordered,[status(thm)],[101,15446]) ).
thf(15676,plain,
! [A: $i] :
( ( ( A @ vskolem2 )
!= vd520 )
| ( A != vd519 )
| ( vd518 != vd517 )
| ( A = v1 ) ),
inference(simp,[status(thm)],[15621]) ).
thf(15688,plain,
( ( ( vd519 @ vskolem2 )
!= vd520 )
| ( vd518 != vd517 )
| ( v1 = vd519 ) ),
inference(simp,[status(thm)],[15676]) ).
thf(49,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ greater ) )
=> ( A @ ( B @ less ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(140, 0), 0)') ).
thf(230,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ greater ) )
=> ( A @ ( B @ less ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(231,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ less ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(cnf,[status(esa)],[230]) ).
thf(24339,plain,
! [B: $i,A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ~ $true
| ( v1 != vd518 ) ),
inference(paramod_ordered,[status(thm)],[22914,227]) ).
thf(24340,plain,
! [B: $i,A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[24339]) ).
thf(24341,plain,
( ~ ( vd518 @ ( vd517 @ less ) )
| ( v1 != vd518 ) ),
inference(pattern_uni,[status(thm)],[24340:[bind(A,$thf( vd517 )),bind(B,$thf( vd518 ))]]) ).
thf(24956,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ less ) )
!= ( vd518 @ ( vd517 @ less ) ) )
| ~ $true
| ( v1 != vd518 )
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[231,24341]) ).
thf(24957,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ less ) )
!= ( vd518 @ ( vd517 @ less ) ) )
| ( v1 != vd518 )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[24956]) ).
thf(24958,plain,
( ( v1 != vd518 )
| ~ ( vd517 @ ( vd518 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[24957:[bind(A,$thf( vd518 )),bind(B,$thf( vd517 ))]]) ).
thf(22,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(141,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ vsucc @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(142,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ),
inference(cnf,[status(esa)],[141]) ).
thf(143,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vplus ) )
= ( B @ ( A @ vplus ) @ vsucc ) ),
inference(lifteq,[status(thm)],[142]) ).
thf(6860,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vsucc @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc )
!= D ) ),
inference(paramod_ordered,[status(thm)],[143,153]) ).
thf(6861,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) @ vsucc )
!= A ),
inference(pattern_uni,[status(thm)],[6860:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ vsucc )),bind(D,$thf( B ))]]) ).
thf(6969,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) @ vsucc )
!= A ),
inference(simp,[status(thm)],[6861]) ).
thf(14007,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ vplus ) ) )
| ( ( v1 @ vsucc )
!= B )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,6969]) ).
thf(14008,plain,
! [B: $i,A: $i] :
( ( ( v1 @ vsucc )
!= B )
| ( v1 @ ( B @ ( A @ vplus ) @ greater ) ) ),
inference(pattern_uni,[status(thm)],[14007:[bind(A,$thf( E @ ( D @ vplus ) )),bind(B,$thf( E )),bind(C,$thf( D ))]]) ).
thf(14023,plain,
! [A: $i] : ( v1 @ ( v1 @ vsucc @ ( A @ vplus ) @ greater ) ),
inference(simp,[status(thm)],[14008]) ).
thf(14030,plain,
! [A: $i] : ( v1 @ ( v1 @ ( A @ vplus ) @ vsucc @ greater ) ),
inference(rewrite,[status(thm)],[14023,69]) ).
thf(41931,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( v1 @ ( A @ vplus ) @ vsucc @ greater ) )
!= ( C @ ( B @ vplus ) @ ( B @ greater ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[14030,19668]) ).
thf(41932,plain,
! [C: $i,B: $i,A: $i] :
( ( v1 @ ( v1 @ ( A @ vplus ) @ vsucc @ greater ) )
!= ( C @ ( B @ vplus ) @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[41931]) ).
thf(41980,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ vplus ) )
!= v1 )
| ( ( v1 @ ( A @ vplus ) @ vsucc )
!= B ) ),
inference(simp,[status(thm)],[41932]) ).
thf(42030,plain,
! [B: $i,A: $i] :
( ( B @ ( v1 @ ( A @ vplus ) @ vsucc @ vplus ) )
!= v1 ),
inference(simp,[status(thm)],[41980]) ).
thf(44588,plain,
! [B: $i,A: $i] :
( ( B @ ( v1 @ ( A @ vplus ) @ vplus ) @ vsucc )
!= v1 ),
inference(rewrite,[status(thm)],[42030,143]) ).
thf(33,axiom,
! [A: $i] :
( ( A @ vsucc )
!= v1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','qu(restrictor(axiom(1)), holds(scope(axiom(1)), 2, 0))') ).
thf(181,plain,
! [A: $i] :
( ( A @ vsucc )
!= v1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(182,plain,
~ ? [A: $i] :
( ( A @ vsucc )
= v1 ),
inference(miniscope,[status(thm)],[181]) ).
thf(183,plain,
! [A: $i] :
( ( A @ vsucc )
!= v1 ),
inference(cnf,[status(esa)],[182]) ).
thf(184,plain,
! [A: $i] :
( ( A @ vsucc )
!= v1 ),
inference(lifteq,[status(thm)],[183]) ).
thf(4582,plain,
! [B: $i,A: $i] :
( ( ( vd518 @ ( vd517 @ geq ) )
!= ( B @ ( A @ geq ) ) )
| ( A @ ( B @ leq ) )
| ~ $true
| ( vd519 @ ( vd520 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2432,103]) ).
thf(4583,plain,
! [B: $i,A: $i] :
( ( ( vd518 @ ( vd517 @ geq ) )
!= ( B @ ( A @ geq ) ) )
| ( A @ ( B @ leq ) )
| ( vd519 @ ( vd520 @ leq ) ) ),
inference(simp,[status(thm)],[4582]) ).
thf(4584,plain,
( ( vd517 @ ( vd518 @ leq ) )
| ( vd519 @ ( vd520 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[4583:[bind(A,$thf( vd517 )),bind(B,$thf( vd518 ))]]) ).
thf(4954,plain,
! [B: $i,A: $i] :
( ( ( vd519 @ ( vd520 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ~ $true
| ( vd517 @ ( vd518 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[4584,98]) ).
thf(4955,plain,
! [B: $i,A: $i] :
( ( ( vd519 @ ( vd520 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ( vd517 @ ( vd518 @ leq ) ) ),
inference(simp,[status(thm)],[4954]) ).
thf(4956,plain,
( ( vd520 @ ( vd519 @ geq ) )
| ( vd517 @ ( vd518 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[4955:[bind(A,$thf( vd520 )),bind(B,$thf( vd519 ))]]) ).
thf(38,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ greater ) )
=> ( A @ ( C @ vmul ) @ ( A @ ( B @ vmul ) @ greater ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(299, 0), 2)') ).
thf(196,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ greater ) )
=> ( A @ ( C @ vmul ) @ ( A @ ( B @ vmul ) @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(7,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(79,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)],[7]) ).
thf(80,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( A @ vplus ) ) )
| ( A
!= ( C @ ( B @ vplus ) ) ) ),
inference(cnf,[status(esa)],[79]) ).
thf(81,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( A @ vplus ) ) )
| ( A
!= ( C @ ( B @ vplus ) ) ) ),
inference(lifteq,[status(thm)],[80]) ).
thf(82,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ vplus ) @ vplus ) )
!= A ),
inference(simp,[status(thm)],[81]) ).
thf(474,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( v1 @ vplus ) )
!= ( D @ ( C @ ( B @ vplus ) @ vplus ) ) )
| ( ( A @ vsucc )
!= B ) ),
inference(paramod_ordered,[status(thm)],[178,82]) ).
thf(488,plain,
! [C: $i,B: $i,A: $i] :
( ( C != A )
| ( ( B @ ( A @ vsucc @ vplus ) )
!= v1 ) ),
inference(simp,[status(thm)],[474]) ).
thf(496,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vplus ) )
!= v1 ),
inference(simp,[status(thm)],[488]) ).
thf(503,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ vsucc @ ( A @ vplus ) )
!= ( D @ ( C @ vsucc @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[69,496]) ).
thf(504,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vplus ) @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[503:[bind(A,$thf( E @ vsucc )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ vsucc ))]]) ).
thf(511,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vplus ) @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[504]) ).
thf(577,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( C @ ( B @ vsucc @ vplus ) ) )
| ( ( A @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[71,511]) ).
thf(578,plain,
! [A: $i] :
( ( A @ vsucc @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[577:[bind(A,$thf( D @ vsucc )),bind(B,$thf( D )),bind(C,$thf( v1 ))]]) ).
thf(587,plain,
! [A: $i] :
( ( A @ vsucc @ vsucc @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[578]) ).
thf(1236,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ( v1 != vd518 )
| ( v1 != vd517 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1012,347]) ).
thf(1237,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[1236]) ).
thf(1256,plain,
! [A: $i] :
( ( A != vd520 )
| ( ( A @ vsucc )
!= vd519 )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[1237]) ).
thf(1268,plain,
( ( ( vd520 @ vsucc )
!= vd519 )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[1256]) ).
thf(2182,plain,
! [A: $i] :
( ( v1 != v1 )
| ( ( vd520 @ vsucc )
!= vd519 )
| ( v1 != vd518 )
| ( A != vd517 )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,1268]) ).
thf(2183,plain,
! [A: $i] :
( ( ( vd520 @ vsucc )
!= vd519 )
| ( v1 != vd518 )
| ( A != vd517 )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[2182:[]]) ).
thf(2303,plain,
( ( ( vd520 @ vsucc )
!= vd519 )
| ( v1 != vd518 )
| ( v1 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[2183]) ).
thf(10611,plain,
( ( ( v1 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( ( vd520 @ vsucc )
!= vd519 )
| ~ $true
| ( ( vd520 @ vsucc )
!= vd519 )
| ( v1 != vd518 ) ),
inference(paramod_ordered,[status(thm)],[2303,10545]) ).
thf(10612,plain,
( ( ( v1 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( ( vd520 @ vsucc )
!= vd519 )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[10611]) ).
thf(10647,plain,
( ( v1 != vd518 )
| ( vd517 != vd517 )
| ( ( vd520 @ vsucc )
!= vd519 )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[10612]) ).
thf(10677,plain,
( ( ( vd520 @ vsucc )
!= vd519 )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[10647]) ).
thf(10710,plain,
! [A: $i] :
( ( v1 != v1 )
| ( ( vd520 @ vsucc )
!= vd519 )
| ( A != vd518 )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,10677]) ).
thf(10711,plain,
! [A: $i] :
( ( ( vd520 @ vsucc )
!= vd519 )
| ( A != vd518 )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[10710:[]]) ).
thf(10719,plain,
( ( ( vd520 @ vsucc )
!= vd519 )
| ( v1 @ ( vd518 @ greater ) ) ),
inference(simp,[status(thm)],[10711]) ).
thf(10,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(91,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)],[10]) ).
thf(92,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ ( B @ sk3 ) @ ( A @ vplus ) ) )
| ( A
= ( A @ ( B @ sk2 ) @ ( B @ vplus ) ) )
| ( A = B ) ),
inference(cnf,[status(esa)],[91]) ).
thf(93,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ sk3 ) @ ( A @ vplus ) )
= B )
| ( ( A @ ( B @ sk2 ) @ ( B @ vplus ) )
= A )
| ( A = B ) ),
inference(lifteq,[status(thm)],[92]) ).
thf(48,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ less ) )
=> ( A @ ( C @ vmul ) @ ( A @ ( B @ vmul ) @ less ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(299, 0), 0)') ).
thf(228,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ less ) )
=> ( A @ ( C @ vmul ) @ ( A @ ( B @ vmul ) @ less ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(42251,plain,
! [A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ~ $true
| ( vd520 != vd519 ) ),
inference(paramod_ordered,[status(thm)],[339,240]) ).
thf(42252,plain,
! [A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ( vd520 != vd519 ) ),
inference(simp,[status(thm)],[42251]) ).
thf(42373,plain,
! [A: $i] :
( ( vd518 != A )
| ( vd517 != A )
| ( vd520 != vd519 ) ),
inference(simp,[status(thm)],[42252]) ).
thf(42379,plain,
( ( vd518 != vd517 )
| ( vd520 != vd519 ) ),
inference(simp,[status(thm)],[42373]) ).
thf(42767,plain,
( ( vd520 != vd520 )
| ( vd518 != vd517 )
| ( vd519 != vd519 )
| ~ ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[21698,42379]) ).
thf(42768,plain,
( ( vd520 != vd520 )
| ( vd518 != vd517 )
| ~ ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[42767]) ).
thf(42769,plain,
( ( vd518 != vd517 )
| ~ ( vd518 @ ( vd517 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[42768:[]]) ).
thf(27,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(162,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)],[27]) ).
thf(163,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)],[162]) ).
thf(164,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less ) )
| ~ ( B @ ( A @ leq ) )
| ~ ( C @ ( B @ less ) ) ),
inference(cnfConj,[status(thm)],[163]) ).
thf(22235,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( C @ ( vd520 @ ( vd518 @ vmul ) @ vplus ) ) )
| ( ( B @ ( A @ vsucc @ vmul ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[236,1327]) ).
thf(22236,plain,
( ( vd520 @ ( vd518 @ vsucc @ vmul ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[22235:[bind(A,$thf( vd518 )),bind(B,$thf( vd520 )),bind(C,$thf( vd520 ))]]) ).
thf(8148,plain,
! [A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( v1 != vd519 )
| ~ ( vd517 @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[205,7908]) ).
thf(8179,plain,
! [A: $i] :
( ( v1 != vd520 )
| ( A != vd518 )
| ( v1 != vd519 )
| ~ ( vd517 @ ( A @ less ) ) ),
inference(simp,[status(thm)],[8148]) ).
thf(8196,plain,
( ( v1 != vd520 )
| ( v1 != vd519 )
| ~ ( vd517 @ ( vd518 @ less ) ) ),
inference(simp,[status(thm)],[8179]) ).
thf(7867,plain,
! [A: $i] :
( ( ( A @ ( v1 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) )
| ~ ( A @ ( vd520 @ ( vd518 @ vmul ) @ less ) ) ),
inference(paramod_ordered,[status(thm)],[259,7779]) ).
thf(7894,plain,
! [A: $i] :
( ( A != vd519 )
| ( v1 != vd517 )
| ~ ( A @ ( vd520 @ ( vd518 @ vmul ) @ less ) ) ),
inference(simp,[status(thm)],[7867]) ).
thf(7906,plain,
( ( v1 != vd517 )
| ~ ( vd519 @ ( vd520 @ ( vd518 @ vmul ) @ less ) ) ),
inference(simp,[status(thm)],[7894]) ).
thf(8067,plain,
! [A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( v1 != vd517 )
| ~ ( vd519 @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[205,7906]) ).
thf(8098,plain,
! [A: $i] :
( ( v1 != vd520 )
| ( A != vd518 )
| ( v1 != vd517 )
| ~ ( vd519 @ ( A @ less ) ) ),
inference(simp,[status(thm)],[8067]) ).
thf(8109,plain,
( ( v1 != vd520 )
| ( v1 != vd517 )
| ~ ( vd519 @ ( vd518 @ less ) ) ),
inference(simp,[status(thm)],[8098]) ).
thf(1311,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ vplus ) )
!= ( C @ ( vd520 @ ( vd518 @ vmul ) @ vplus ) ) )
| ( ( B @ ( A @ vplus ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[78,1047]) ).
thf(1312,plain,
! [A: $i] :
( ( vd520 @ ( vd518 @ vmul ) @ ( A @ vplus ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[1311:[bind(A,$thf( A )),bind(B,$thf( vd520 @ ( vd518 @ vmul ) )),bind(C,$thf( A ))]]) ).
thf(27094,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ vmul ) @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( D @ vplus ) ) )
| ( ( C @ ( B @ vplus ) @ ( A @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[262,1312]) ).
thf(27095,plain,
! [A: $i] :
( ( vd520 @ ( A @ vplus ) @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[27094:[bind(A,$thf( vd518 )),bind(B,$thf( F )),bind(C,$thf( vd520 )),bind(D,$thf( F @ ( vd518 @ vmul ) ))]]) ).
thf(27289,plain,
! [A: $i] :
( ( vd520 @ ( A @ vplus ) @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(simp,[status(thm)],[27095]) ).
thf(27496,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( vd520 @ ( C @ vplus ) ) )
| ( ( B @ ( A @ vsucc @ vmul ) @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[236,27289]) ).
thf(27497,plain,
! [A: $i] :
( ( vd520 @ ( A @ vsucc @ vmul ) @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[27496:[bind(A,$thf( D )),bind(B,$thf( vd520 )),bind(C,$thf( vd520 @ ( D @ vmul ) ))]]) ).
thf(27615,plain,
! [A: $i] :
( ( vd520 @ ( A @ vsucc @ vmul ) @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(simp,[status(thm)],[27497]) ).
thf(32,axiom,
! [A: $i] : ( v1 @ ( A @ geq ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(228, 0), 0)') ).
thf(179,plain,
! [A: $i] : ( v1 @ ( A @ geq ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(341,plain,
( ( ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ( v1 != vd517 )
| ~ $true
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[209,309]) ).
thf(342,plain,
( ( ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ( v1 != vd517 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[341]) ).
thf(345,plain,
( ( ( vd520 @ ( vd518 @ vmul ) )
!= vd520 )
| ( vd519 != vd519 )
| ( v1 != vd517 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[342]) ).
thf(348,plain,
( ( ( vd520 @ ( vd518 @ vmul ) )
!= vd520 )
| ( v1 != vd517 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[345]) ).
thf(296,plain,
! [A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ~ ( A @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[205,61]) ).
thf(298,plain,
! [A: $i] :
( ( v1 != vd520 )
| ( A != vd518 )
| ~ ( A @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) ),
inference(simp,[status(thm)],[296]) ).
thf(300,plain,
( ( v1 != vd520 )
| ~ ( vd518 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) ),
inference(simp,[status(thm)],[298]) ).
thf(545,plain,
( ( ( vd518 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( v1 != vd520 )
| ~ $true
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(paramod_ordered,[status(thm)],[467,300]) ).
thf(546,plain,
( ( ( vd518 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( v1 != vd520 )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[545]) ).
thf(566,plain,
( ( vd518 != vd518 )
| ( ( vd519 @ ( vd517 @ vmul ) )
!= vd517 )
| ( v1 != vd520 )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[546]) ).
thf(574,plain,
( ( ( vd519 @ ( vd517 @ vmul ) )
!= vd517 )
| ( v1 != vd520 )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[566]) ).
thf(505,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ vplus ) )
!= ( D @ ( C @ vsucc @ vplus ) ) )
| ( ( B @ ( A @ vplus ) )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[78,496]) ).
thf(506,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vplus ) )
!= v1 ),
inference(pattern_uni,[status(thm)],[505:[bind(A,$thf( A )),bind(B,$thf( E @ vsucc )),bind(C,$thf( E )),bind(D,$thf( A ))]]) ).
thf(512,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vplus ) )
!= v1 ),
inference(simp,[status(thm)],[506]) ).
thf(515,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ vsucc )
!= v1 ),
inference(rewrite,[status(thm)],[512,69]) ).
thf(520,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)],[69,515]) ).
thf(521,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[520:[bind(A,$thf( A )),bind(B,$thf( E )),bind(C,$thf( A )),bind(D,$thf( E @ vsucc ))]]) ).
thf(526,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ vsucc @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[521]) ).
thf(596,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ vsucc @ ( A @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[69,526]) ).
thf(597,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ vsucc @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[596:[bind(A,$thf( A )),bind(B,$thf( E )),bind(C,$thf( A )),bind(D,$thf( E @ vsucc ))]]) ).
thf(602,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ vsucc @ vsucc @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[597]) ).
thf(318,plain,
! [A: $i] :
( ( ( A @ ( v1 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) )
| ( v1 != vd520 )
| ~ ( vd518 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[259,300]) ).
thf(320,plain,
! [A: $i] :
( ( A != vd519 )
| ( v1 != vd517 )
| ( v1 != vd520 )
| ~ ( vd518 @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[318]) ).
thf(322,plain,
( ( v1 != vd517 )
| ( v1 != vd520 )
| ~ ( vd518 @ ( vd519 @ greater ) ) ),
inference(simp,[status(thm)],[320]) ).
thf(394,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd518 @ ( vd519 @ greater ) ) )
| ( v1 != vd517 )
| ( v1 != vd520 )
| ~ $true
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[209,322]) ).
thf(395,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd518 @ ( vd519 @ greater ) ) )
| ( v1 != vd517 )
| ( v1 != vd520 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[394]) ).
thf(396,plain,
( ( vd520 != vd518 )
| ( vd519 != vd519 )
| ( v1 != vd517 )
| ( v1 != vd520 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[395]) ).
thf(397,plain,
( ( vd520 != vd518 )
| ( v1 != vd517 )
| ( v1 != vd520 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[396]) ).
thf(19544,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( vd518 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ~ $true
| ( ( vd520 @ vsucc )
!= vd519 ) ),
inference(paramod_ordered,[status(thm)],[10719,227]) ).
thf(19545,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( vd518 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ( ( vd520 @ vsucc )
!= vd519 ) ),
inference(simp,[status(thm)],[19544]) ).
thf(19546,plain,
( ~ ( v1 @ ( vd518 @ less ) )
| ( ( vd520 @ vsucc )
!= vd519 ) ),
inference(pattern_uni,[status(thm)],[19545:[bind(A,$thf( vd518 )),bind(B,$thf( v1 ))]]) ).
thf(21781,plain,
! [B: $i,A: $i] :
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ~ $true
| ( vd520 = vd519 ) ),
inference(paramod_ordered,[status(thm)],[21578,231]) ).
thf(21782,plain,
! [B: $i,A: $i] :
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ( vd520 = vd519 ) ),
inference(simp,[status(thm)],[21781]) ).
thf(21783,plain,
( ( vd519 @ ( vd520 @ less ) )
| ( vd520 = vd519 ) ),
inference(pattern_uni,[status(thm)],[21782:[bind(A,$thf( vd519 )),bind(B,$thf( vd520 ))]]) ).
thf(24177,plain,
! [B: $i,A: $i] :
( ( ( vd519 @ ( vd520 @ less ) )
!= ( A @ ( B @ less ) ) )
| ( A @ ( B @ leq ) )
| ~ $true
| ( vd520 = vd519 ) ),
inference(paramod_ordered,[status(thm)],[21783,111]) ).
thf(24178,plain,
! [B: $i,A: $i] :
( ( ( vd519 @ ( vd520 @ less ) )
!= ( A @ ( B @ less ) ) )
| ( A @ ( B @ leq ) )
| ( vd520 = vd519 ) ),
inference(simp,[status(thm)],[24177]) ).
thf(24179,plain,
( ( vd519 @ ( vd520 @ leq ) )
| ( vd520 = vd519 ) ),
inference(pattern_uni,[status(thm)],[24178:[bind(A,$thf( vd519 )),bind(B,$thf( vd520 ))]]) ).
thf(26196,plain,
! [B: $i,A: $i] :
( ( ( vd519 @ ( vd520 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ~ $true
| ( vd520 = vd519 ) ),
inference(paramod_ordered,[status(thm)],[24179,98]) ).
thf(26197,plain,
! [B: $i,A: $i] :
( ( ( vd519 @ ( vd520 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ( vd520 = vd519 ) ),
inference(simp,[status(thm)],[26196]) ).
thf(26198,plain,
( ( vd520 @ ( vd519 @ geq ) )
| ( vd520 = vd519 ) ),
inference(pattern_uni,[status(thm)],[26197:[bind(A,$thf( vd520 )),bind(B,$thf( vd519 ))]]) ).
thf(20,axiom,
! [A: $i,B: $i] :
( ( A != B )
=> ( ( A @ vsucc )
!= ( B @ vsucc ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(6, 0), 0)') ).
thf(132,plain,
! [A: $i,B: $i] :
( ( A != B )
=> ( ( A @ vsucc )
!= ( B @ vsucc ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(670,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( C @ ( B @ vplus ) ) )
| ( A @ vsucc @ ( B @ less ) ) ),
inference(paramod_ordered,[status(thm)],[71,161]) ).
thf(671,plain,
! [A: $i] : ( A @ vsucc @ ( A @ less ) ),
inference(pattern_uni,[status(thm)],[670:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( v1 ))]]) ).
thf(19628,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( A @ less ) )
!= ( C @ ( B @ less ) ) )
| ~ $true
| ~ ( C @ ( B @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[671,227]) ).
thf(19629,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( A @ less ) )
!= ( C @ ( B @ less ) ) )
| ~ ( C @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[19628]) ).
thf(19630,plain,
! [A: $i] :
~ ( A @ vsucc @ ( A @ greater ) ),
inference(pattern_uni,[status(thm)],[19629:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ vsucc ))]]) ).
thf(19676,plain,
! [A: $i] :
~ ( A @ vsucc @ ( A @ greater ) ),
inference(simp,[status(thm)],[19630]) ).
thf(42218,plain,
! [A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( A @ vsucc @ ( A @ greater ) ) )
| ~ $true
| ( vd520 != vd519 ) ),
inference(paramod_ordered,[status(thm)],[339,19676]) ).
thf(42219,plain,
! [A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( A @ vsucc @ ( A @ greater ) ) )
| ( vd520 != vd519 ) ),
inference(simp,[status(thm)],[42218]) ).
thf(42372,plain,
! [A: $i] :
( ( ( A @ vsucc )
!= vd518 )
| ( vd517 != A )
| ( vd520 != vd519 ) ),
inference(simp,[status(thm)],[42219]) ).
thf(42378,plain,
( ( ( vd517 @ vsucc )
!= vd518 )
| ( vd520 != vd519 ) ),
inference(simp,[status(thm)],[42372]) ).
thf(5,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(72,plain,
! [A: $i,B: $i] :
( ~ ? [C: $i] :
( A
= ( C @ ( B @ vplus ) ) )
| ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(73,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ vplus ) ) )
| ( A != B ) ),
inference(cnf,[status(esa)],[72]) ).
thf(74,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ vplus ) ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[73]) ).
thf(75,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) )
!= A ),
inference(simp,[status(thm)],[74]) ).
thf(377,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ vsucc @ ( A @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc )
!= C ) ),
inference(paramod_ordered,[status(thm)],[69,75]) ).
thf(378,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ vsucc )
!= A ),
inference(pattern_uni,[status(thm)],[377:[bind(A,$thf( A )),bind(B,$thf( E )),bind(C,$thf( A )),bind(D,$thf( E @ vsucc ))]]) ).
thf(383,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ vsucc )
!= A ),
inference(simp,[status(thm)],[378]) ).
thf(7752,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ sk7 ) @ ( B @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( ( A @ vsucc )
!= C )
| ~ ( A @ ( B @ less ) ) ),
inference(paramod_ordered,[status(thm)],[159,383]) ).
thf(7753,plain,
! [B: $i,A: $i] :
( ( ( B @ vsucc )
!= A )
| ~ ( B @ ( A @ less ) ) ),
inference(pattern_uni,[status(thm)],[7752:[bind(A,$thf( F )),bind(B,$thf( E )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ sk7 ) ))]]) ).
thf(7805,plain,
! [A: $i] :
~ ( A @ ( A @ vsucc @ less ) ),
inference(simp,[status(thm)],[7753]) ).
thf(8928,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( A @ less ) )
!= ( C @ ( C @ vsucc @ less ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[161,7805]) ).
thf(8929,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ ( A @ less ) )
!= ( C @ ( C @ vsucc @ less ) ) ),
inference(simp,[status(thm)],[8928]) ).
thf(8945,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) )
!= C )
| ( A
!= ( C @ vsucc ) ) ),
inference(simp,[status(thm)],[8929]) ).
thf(8955,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vsucc @ vplus ) )
!= B ),
inference(simp,[status(thm)],[8945]) ).
thf(38780,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) @ vsucc )
!= B ),
inference(rewrite,[status(thm)],[8955,143]) ).
thf(16,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(114,plain,
! [A: $i,B: $i] :
( ( ( A @ vsucc )
= ( B @ vsucc ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(115,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( ( A @ vsucc )
!= ( B @ vsucc ) ) ),
inference(cnf,[status(esa)],[114]) ).
thf(116,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( ( A @ vsucc )
!= ( B @ vsucc ) ) ),
inference(lifteq,[status(thm)],[115]) ).
thf(41,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(212,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ greater ) )
=> ( v1 @ ( B @ vplus ) @ ( A @ geq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(213,plain,
! [B: $i,A: $i] :
( ( v1 @ ( B @ vplus ) @ ( A @ geq ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(cnf,[status(esa)],[212]) ).
thf(16281,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ geq ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(rewrite,[status(thm)],[213,71]) ).
thf(16339,plain,
! [B: $i,A: $i] :
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( B @ vsucc @ ( A @ geq ) )
| ~ $true
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[209,16281]) ).
thf(16340,plain,
! [B: $i,A: $i] :
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( B @ vsucc @ ( A @ geq ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[16339]) ).
thf(16341,plain,
( ( vd520 @ vsucc @ ( vd519 @ geq ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[16340:[bind(A,$thf( vd519 )),bind(B,$thf( vd520 ))]]) ).
thf(16563,plain,
! [B: $i,A: $i] :
( ( ( vd520 @ vsucc @ ( vd519 @ geq ) )
!= ( B @ ( A @ geq ) ) )
| ( A @ ( B @ leq ) )
| ~ $true
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[16341,103]) ).
thf(16564,plain,
! [B: $i,A: $i] :
( ( ( vd520 @ vsucc @ ( vd519 @ geq ) )
!= ( B @ ( A @ geq ) ) )
| ( A @ ( B @ leq ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[16563]) ).
thf(16565,plain,
( ( vd519 @ ( vd520 @ vsucc @ leq ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[16564:[bind(A,$thf( vd519 )),bind(B,$thf( vd520 @ vsucc ))]]) ).
thf(10482,plain,
! [A: $i] :
( ( ( v1 @ ( A @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ~ ( vd518 @ ( vd517 @ greater ) )
| ~ $true
| ( A = v1 ) ),
inference(paramod_ordered,[status(thm)],[1505,9985]) ).
thf(10483,plain,
! [A: $i] :
( ( ( v1 @ ( A @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ~ ( vd518 @ ( vd517 @ greater ) )
| ( A = v1 ) ),
inference(simp,[status(thm)],[10482]) ).
thf(10529,plain,
! [A: $i] :
( ( v1 != vd520 )
| ( A != vd519 )
| ~ ( vd518 @ ( vd517 @ greater ) )
| ( A = v1 ) ),
inference(simp,[status(thm)],[10483]) ).
thf(10551,plain,
( ( v1 != vd520 )
| ~ ( vd518 @ ( vd517 @ greater ) )
| ( v1 = vd519 ) ),
inference(simp,[status(thm)],[10529]) ).
thf(45,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(221,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)],[45]) ).
thf(4435,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( A @ less ) )
!= ( B @ ( C @ less ) ) )
| ( B @ ( C @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[671,111]) ).
thf(4436,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( A @ less ) )
!= ( B @ ( C @ less ) ) )
| ( B @ ( C @ leq ) ) ),
inference(simp,[status(thm)],[4435]) ).
thf(4437,plain,
! [A: $i] : ( A @ vsucc @ ( A @ leq ) ),
inference(pattern_uni,[status(thm)],[4436:[bind(A,$thf( D )),bind(B,$thf( D @ vsucc )),bind(C,$thf( D ))]]) ).
thf(4451,plain,
! [A: $i] : ( A @ vsucc @ ( A @ leq ) ),
inference(simp,[status(thm)],[4437]) ).
thf(4464,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( A @ leq ) )
!= ( C @ ( B @ leq ) ) )
| ( B @ ( C @ geq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4451,98]) ).
thf(4465,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( A @ leq ) )
!= ( C @ ( B @ leq ) ) )
| ( B @ ( C @ geq ) ) ),
inference(simp,[status(thm)],[4464]) ).
thf(4466,plain,
! [A: $i] : ( A @ ( A @ vsucc @ geq ) ),
inference(pattern_uni,[status(thm)],[4465:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ vsucc ))]]) ).
thf(4475,plain,
! [A: $i] : ( A @ ( A @ vsucc @ geq ) ),
inference(simp,[status(thm)],[4466]) ).
thf(27512,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( vd520 @ ( C @ vplus ) ) )
| ( ( B @ vsucc @ ( A @ vmul ) @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[203,27289]) ).
thf(27513,plain,
! [A: $i] :
( ( A @ vsucc @ ( vd520 @ vmul ) @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[27512:[bind(A,$thf( vd520 )),bind(B,$thf( E )),bind(C,$thf( E @ ( vd520 @ vmul ) ))]]) ).
thf(27617,plain,
! [A: $i] :
( ( A @ vsucc @ ( vd520 @ vmul ) @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(simp,[status(thm)],[27513]) ).
thf(267,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ geq ) )
| ~ ( A @ ( B @ greater ) ) ),
inference(cnfConj,[status(thm)],[265]) ).
thf(270,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ geq ) )
| ~ ( A @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[267]) ).
thf(27017,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ vmul ) @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( D @ ( vd520 @ ( vd518 @ vmul ) @ vplus ) ) )
| ( ( C @ ( B @ vplus ) @ ( A @ vmul ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[262,1327]) ).
thf(27018,plain,
! [A: $i] :
( ( A @ ( vd520 @ vplus ) @ ( vd518 @ vmul ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[27017:[bind(A,$thf( vd518 )),bind(B,$thf( vd520 )),bind(C,$thf( F )),bind(D,$thf( F @ ( vd518 @ vmul ) ))]]) ).
thf(27255,plain,
! [A: $i] :
( ( A @ ( vd520 @ vplus ) @ ( vd518 @ vmul ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(simp,[status(thm)],[27018]) ).
thf(44,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ vmul ) @ ( B @ ( A @ vmul ) @ less ) )
=> ( C @ ( A @ less ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(conjunct2(conjunct2(307)), 0), 0)') ).
thf(219,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ vmul ) @ ( B @ ( A @ vmul ) @ less ) )
=> ( C @ ( A @ less ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(220,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less ) )
| ~ ( B @ ( C @ vmul ) @ ( B @ ( A @ vmul ) @ less ) ) ),
inference(cnf,[status(esa)],[219]) ).
thf(133,plain,
! [B: $i,A: $i] :
( ( ( A @ vsucc )
!= ( B @ vsucc ) )
| ( A = B ) ),
inference(cnf,[status(esa)],[132]) ).
thf(134,plain,
! [B: $i,A: $i] :
( ( ( A @ vsucc )
!= ( B @ vsucc ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[133]) ).
thf(135,plain,
? [A: $i > $i] :
! [B: $i] :
( ( B @ vsucc @ A )
= B ),
inference(detectInverse,[status(thm)],[134]) ).
thf(136,plain,
! [A: $i] :
( ( A @ vsucc @ sk6 )
= A ),
inference(cnf,[status(esa)],[135]) ).
thf(366,plain,
! [A: $i] :
( ( A @ vsucc @ sk6 )
= A ),
inference(lifteq,[status(thm)],[136]) ).
thf(1250,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd518 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) )
| ( v1 != vd520 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1012,300]) ).
thf(1251,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd518 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) )
| ( v1 != vd520 ) ),
inference(simp,[status(thm)],[1250]) ).
thf(1262,plain,
! [A: $i] :
( ( A != vd518 )
| ( ( A @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) )
| ( v1 != vd520 ) ),
inference(simp,[status(thm)],[1251]) ).
thf(1274,plain,
( ( ( vd519 @ ( vd517 @ vmul ) )
!= ( vd518 @ vsucc ) )
| ( v1 != vd520 ) ),
inference(simp,[status(thm)],[1262]) ).
thf(328,plain,
( ( ( vd518 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ( v1 != vd520 )
| ~ $true
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[209,300]) ).
thf(329,plain,
( ( ( vd518 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ( v1 != vd520 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[328]) ).
thf(334,plain,
( ( vd520 != vd518 )
| ( ( vd519 @ ( vd517 @ vmul ) )
!= vd519 )
| ( v1 != vd520 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[329]) ).
thf(1557,plain,
! [A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( ( A @ vsucc @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[205,1529]) ).
thf(1568,plain,
! [A: $i] :
( ( v1 != vd520 )
| ( A != vd518 )
| ( ( A @ vsucc @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(simp,[status(thm)],[1557]) ).
thf(1570,plain,
( ( v1 != vd520 )
| ( ( vd519 @ ( vd517 @ vmul ) )
!= ( vd518 @ vsucc @ vsucc ) ) ),
inference(simp,[status(thm)],[1568]) ).
thf(165,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less ) )
| ~ ( B @ ( A @ less ) )
| ~ ( C @ ( B @ leq ) ) ),
inference(cnfConj,[status(thm)],[163]) ).
thf(59,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ vmul ) @ vmul ) )
= ( C @ ( B @ vmul ) @ ( A @ vmul ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(290, 0), 0)') ).
thf(273,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ vmul ) @ vmul ) )
= ( C @ ( B @ vmul ) @ ( A @ vmul ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(274,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ vmul ) @ vmul ) )
= ( C @ ( B @ vmul ) @ ( A @ vmul ) ) ),
inference(cnf,[status(esa)],[273]) ).
thf(275,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ vmul ) @ vmul ) )
= ( C @ ( B @ vmul ) @ ( A @ vmul ) ) ),
inference(lifteq,[status(thm)],[274]) ).
thf(21,axiom,
! [A: $i,B: $i] :
( ~ ( B @ ( A @ less ) )
| ( A != B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(goal(130), 0), 1)') ).
thf(137,plain,
! [A: $i,B: $i] :
( ~ ( B @ ( A @ less ) )
| ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(229,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ vmul ) @ ( A @ ( B @ vmul ) @ less ) )
| ~ ( C @ ( B @ less ) ) ),
inference(cnf,[status(esa)],[228]) ).
thf(197,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ vmul ) @ ( A @ ( B @ vmul ) @ greater ) )
| ~ ( C @ ( B @ greater ) ) ),
inference(cnf,[status(esa)],[196]) ).
thf(1727,plain,
! [A: $i] :
( ( v1 != v1 )
| ( v1 != vd518 )
| ( A != vd519 )
| ~ ( vd520 @ ( vd517 @ greater ) )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,316]) ).
thf(1728,plain,
! [A: $i] :
( ( v1 != vd518 )
| ( A != vd519 )
| ~ ( vd520 @ ( vd517 @ greater ) )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[1727:[]]) ).
thf(2332,plain,
( ( v1 != vd518 )
| ~ ( vd520 @ ( vd517 @ greater ) )
| ( v1 @ ( vd519 @ greater ) ) ),
inference(simp,[status(thm)],[1728]) ).
thf(46,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ vmul ) @ ( B @ ( A @ vmul ) @ greater ) )
=> ( C @ ( A @ greater ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(conjunct1(307), 0), 0)') ).
thf(224,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ vmul ) @ ( B @ ( A @ vmul ) @ greater ) )
=> ( C @ ( A @ greater ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(524,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)],[78,515]) ).
thf(525,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[524:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(15500,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)],[203,525]) ).
thf(15501,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vmul ) @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[15500:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ vmul ) ))]]) ).
thf(15559,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vmul ) @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[15501]) ).
thf(89,plain,
? [A: $i > $i > $i] :
! [B: $i,C: $i] :
( ( C @ ( B @ vplus ) @ ( B @ A ) )
= C ),
inference(detectInverse,[status(thm)],[88]) ).
thf(90,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ ( A @ sk1 ) )
= B ),
inference(cnf,[status(esa)],[89]) ).
thf(695,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ ( A @ sk1 ) )
= B ),
inference(lifteq,[status(thm)],[90]) ).
thf(696,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( v1 @ vplus ) )
!= ( C @ ( B @ vplus ) ) )
| ( ( A @ vsucc @ ( B @ sk1 ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[178,695]) ).
thf(697,plain,
! [A: $i] :
( ( A @ vsucc @ ( v1 @ sk1 ) )
= A ),
inference(pattern_uni,[status(thm)],[696:[bind(A,$thf( A )),bind(B,$thf( v1 )),bind(C,$thf( A ))]]) ).
thf(19646,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)],[190,227]) ).
thf(19647,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vplus ) @ greater ) )
!= ( D @ ( C @ greater ) ) )
| ~ ( D @ ( C @ less ) ) ),
inference(simp,[status(thm)],[19646]) ).
thf(19648,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ ( A @ vplus ) @ less ) ),
inference(pattern_uni,[status(thm)],[19647:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ vplus ) )),bind(D,$thf( E ))]]) ).
thf(19667,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ ( A @ vplus ) @ less ) ),
inference(simp,[status(thm)],[19648]) ).
thf(1005,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)],[78,190]) ).
thf(1006,plain,
! [B: $i,A: $i] : ( A @ ( A @ ( B @ vplus ) @ greater ) ),
inference(pattern_uni,[status(thm)],[1005:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(28,axiom,
! [A: $i] :
( ( A @ vsucc )
!= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(12, 0), 0)') ).
thf(166,plain,
! [A: $i] :
( ( A @ vsucc )
!= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(167,plain,
~ ? [A: $i] :
( ( A @ vsucc )
= A ),
inference(miniscope,[status(thm)],[166]) ).
thf(168,plain,
! [A: $i] :
( ( A @ vsucc )
!= A ),
inference(cnf,[status(esa)],[167]) ).
thf(169,plain,
! [A: $i] :
( ( A @ vsucc )
!= A ),
inference(lifteq,[status(thm)],[168]) ).
thf(21024,plain,
! [B: $i,A: $i] :
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ~ $true
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[209,231]) ).
thf(21025,plain,
! [B: $i,A: $i] :
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[21024]) ).
thf(21026,plain,
( ( vd519 @ ( vd520 @ less ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[21025:[bind(A,$thf( vd519 )),bind(B,$thf( vd520 ))]]) ).
thf(1246,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( vd517 @ greater ) ) )
| ( v1 != vd519 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1012,299]) ).
thf(1247,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( vd517 @ greater ) ) )
| ( v1 != vd519 ) ),
inference(simp,[status(thm)],[1246]) ).
thf(1258,plain,
! [A: $i] :
( ( A
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( ( A @ vsucc )
!= vd517 )
| ( v1 != vd519 ) ),
inference(simp,[status(thm)],[1247]) ).
thf(1270,plain,
( ( ( vd520 @ ( vd518 @ vmul ) @ vsucc )
!= vd517 )
| ( v1 != vd519 ) ),
inference(simp,[status(thm)],[1258]) ).
thf(23115,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ~ $true
| ( vd520 = vd519 )
| ( vd518 = vd517 ) ),
inference(paramod_ordered,[status(thm)],[21582,21698]) ).
thf(23116,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( vd520 = vd519 )
| ( vd518 = vd517 ) ),
inference(simp,[status(thm)],[23115]) ).
thf(23117,plain,
( ( vd520 = vd519 )
| ( vd518 = vd517 ) ),
inference(pattern_uni,[status(thm)],[23116:[]]) ).
thf(42343,plain,
! [B: $i,A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ~ $true
| ( vd520 != vd519 ) ),
inference(paramod_ordered,[status(thm)],[339,227]) ).
thf(42344,plain,
! [B: $i,A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ( vd520 != vd519 ) ),
inference(simp,[status(thm)],[42343]) ).
thf(42345,plain,
( ~ ( vd518 @ ( vd517 @ less ) )
| ( vd520 != vd519 ) ),
inference(pattern_uni,[status(thm)],[42344:[bind(A,$thf( vd517 )),bind(B,$thf( vd518 ))]]) ).
thf(43650,plain,
( ( vd520 != vd520 )
| ~ ( vd518 @ ( vd517 @ less ) )
| ( vd519 != vd519 )
| ( vd518 = vd517 ) ),
inference(paramod_ordered,[status(thm)],[23117,42345]) ).
thf(43651,plain,
( ( vd520 != vd520 )
| ~ ( vd518 @ ( vd517 @ less ) )
| ( vd518 = vd517 ) ),
inference(simp,[status(thm)],[43650]) ).
thf(43652,plain,
( ~ ( vd518 @ ( vd517 @ less ) )
| ( vd518 = vd517 ) ),
inference(pattern_uni,[status(thm)],[43651:[]]) ).
thf(15449,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( ( B @ vsucc @ ( A @ vmul ) @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[203,526]) ).
thf(15450,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vmul ) @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[15449:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ vmul ) )),bind(D,$thf( E ))]]) ).
thf(15606,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vmul ) @ vsucc @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[15450]) ).
thf(1059,plain,
! [A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ~ $true
| ( vd520 != vd518 )
| ( v1 != vd517 )
| ( v1 != vd520 ) ),
inference(paramod_ordered,[status(thm)],[397,240]) ).
thf(1060,plain,
! [A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( A @ ( A @ greater ) ) )
| ( vd520 != vd518 )
| ( v1 != vd517 )
| ( v1 != vd520 ) ),
inference(simp,[status(thm)],[1059]) ).
thf(1075,plain,
! [A: $i] :
( ( vd518 != A )
| ( vd517 != A )
| ( vd520 != vd518 )
| ( v1 != vd517 )
| ( v1 != vd520 ) ),
inference(simp,[status(thm)],[1060]) ).
thf(1082,plain,
( ( vd518 != vd517 )
| ( vd520 != vd518 )
| ( v1 != vd517 )
| ( v1 != vd520 ) ),
inference(simp,[status(thm)],[1075]) ).
thf(2211,plain,
! [A: $i] :
( ( v1 != v1 )
| ( A != vd517 )
| ( v1 != vd520 )
| ~ ( vd518 @ ( vd519 @ greater ) )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,322]) ).
thf(2212,plain,
! [A: $i] :
( ( A != vd517 )
| ( v1 != vd520 )
| ~ ( vd518 @ ( vd519 @ greater ) )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[2211:[]]) ).
thf(2317,plain,
( ( v1 != vd520 )
| ~ ( vd518 @ ( vd519 @ greater ) )
| ( v1 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[2212]) ).
thf(11,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(94,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)],[11]) ).
thf(95,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ vplus ) @ vplus ) )
= ( C @ ( B @ vplus ) @ ( A @ vplus ) ) ),
inference(cnf,[status(esa)],[94]) ).
thf(96,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ vplus ) @ vplus ) )
= ( C @ ( B @ vplus ) @ ( A @ vplus ) ) ),
inference(lifteq,[status(thm)],[95]) ).
thf(1558,plain,
! [A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) )
| ( A
!= ( vd520 @ ( vd518 @ vmul ) @ vsucc @ vsucc ) ) ),
inference(paramod_ordered,[status(thm)],[205,1529]) ).
thf(1567,plain,
( ( v1 != vd519 )
| ( ( vd520 @ ( vd518 @ vmul ) @ vsucc @ vsucc )
!= vd517 ) ),
inference(simp,[status(thm)],[1558]) ).
thf(20173,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( vd518 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( B @ vsucc @ ( A @ geq ) )
| ~ $true
| ( vd518 != vd517 ) ),
inference(paramod_ordered,[status(thm)],[19540,16281]) ).
thf(20174,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( vd518 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( B @ vsucc @ ( A @ geq ) )
| ( vd518 != vd517 ) ),
inference(simp,[status(thm)],[20173]) ).
thf(20175,plain,
( ( v1 @ vsucc @ ( vd518 @ geq ) )
| ( vd518 != vd517 ) ),
inference(pattern_uni,[status(thm)],[20174:[bind(A,$thf( vd518 )),bind(B,$thf( v1 ))]]) ).
thf(18,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(124,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( A @ vplus ) )
= ( C @ ( B @ vplus ) ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(225,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ greater ) )
| ~ ( B @ ( C @ vmul ) @ ( B @ ( A @ vmul ) @ greater ) ) ),
inference(cnf,[status(esa)],[224]) ).
thf(37,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(193,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) )
| ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(4406,plain,
! [A: $i] :
( ( ( A @ ( v1 @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( v1 != vd519 )
| ( ( A @ vsucc @ vsucc )
!= vd517 ) ),
inference(paramod_ordered,[status(thm)],[259,1567]) ).
thf(4421,plain,
! [A: $i] :
( ( A != vd520 )
| ( v1 != vd518 )
| ( v1 != vd519 )
| ( ( A @ vsucc @ vsucc )
!= vd517 ) ),
inference(simp,[status(thm)],[4406]) ).
thf(4425,plain,
( ( v1 != vd518 )
| ( v1 != vd519 )
| ( ( vd520 @ vsucc @ vsucc )
!= vd517 ) ),
inference(simp,[status(thm)],[4421]) ).
thf(23078,plain,
! [B: $i,A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ~ $true
| ( vd518 = vd517 ) ),
inference(paramod_ordered,[status(thm)],[21582,231]) ).
thf(23079,plain,
! [B: $i,A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ( vd518 = vd517 ) ),
inference(simp,[status(thm)],[23078]) ).
thf(23080,plain,
( ( vd517 @ ( vd518 @ less ) )
| ( vd518 = vd517 ) ),
inference(pattern_uni,[status(thm)],[23079:[bind(A,$thf( vd517 )),bind(B,$thf( vd518 ))]]) ).
thf(25304,plain,
! [B: $i,A: $i] :
( ( ( vd517 @ ( vd518 @ less ) )
!= ( A @ ( B @ less ) ) )
| ( A @ ( B @ leq ) )
| ~ $true
| ( vd518 = vd517 ) ),
inference(paramod_ordered,[status(thm)],[23080,111]) ).
thf(25305,plain,
! [B: $i,A: $i] :
( ( ( vd517 @ ( vd518 @ less ) )
!= ( A @ ( B @ less ) ) )
| ( A @ ( B @ leq ) )
| ( vd518 = vd517 ) ),
inference(simp,[status(thm)],[25304]) ).
thf(25306,plain,
( ( vd517 @ ( vd518 @ leq ) )
| ( vd518 = vd517 ) ),
inference(pattern_uni,[status(thm)],[25305:[bind(A,$thf( vd517 )),bind(B,$thf( vd518 ))]]) ).
thf(27961,plain,
! [B: $i,A: $i] :
( ( ( vd517 @ ( vd518 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ~ $true
| ( vd518 = vd517 ) ),
inference(paramod_ordered,[status(thm)],[25306,98]) ).
thf(27962,plain,
! [B: $i,A: $i] :
( ( ( vd517 @ ( vd518 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ( vd518 = vd517 ) ),
inference(simp,[status(thm)],[27961]) ).
thf(27963,plain,
( ( vd518 @ ( vd517 @ geq ) )
| ( vd518 = vd517 ) ),
inference(pattern_uni,[status(thm)],[27962:[bind(A,$thf( vd518 )),bind(B,$thf( vd517 ))]]) ).
thf(984,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( ( A @ ( B @ vplus ) @ vsucc @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[78,602]) ).
thf(985,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) @ vsucc @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[984:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(20212,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( vd518 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ~ $true
| ( vd518 != vd517 ) ),
inference(paramod_ordered,[status(thm)],[19540,227]) ).
thf(20213,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( vd518 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ~ ( B @ ( A @ less ) )
| ( vd518 != vd517 ) ),
inference(simp,[status(thm)],[20212]) ).
thf(20214,plain,
( ~ ( v1 @ ( vd518 @ less ) )
| ( vd518 != vd517 ) ),
inference(pattern_uni,[status(thm)],[20213:[bind(A,$thf( vd518 )),bind(B,$thf( v1 ))]]) ).
thf(21057,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ less ) )
!= ( v1 @ ( vd518 @ less ) ) )
| ~ $true
| ( vd518 != vd517 )
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[231,20214]) ).
thf(21058,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ less ) )
!= ( v1 @ ( vd518 @ less ) ) )
| ( vd518 != vd517 )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[21057]) ).
thf(21059,plain,
( ( vd518 != vd517 )
| ~ ( vd518 @ ( v1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[21058:[bind(A,$thf( v1 )),bind(B,$thf( vd518 ))]]) ).
thf(30,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(173,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)],[30]) ).
thf(24296,plain,
! [B: $i,A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ~ $true
| ( v1 != vd518 ) ),
inference(paramod_ordered,[status(thm)],[22914,231]) ).
thf(24297,plain,
! [B: $i,A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[24296]) ).
thf(24298,plain,
( ( vd517 @ ( vd518 @ less ) )
| ( v1 != vd518 ) ),
inference(pattern_uni,[status(thm)],[24297:[bind(A,$thf( vd517 )),bind(B,$thf( vd518 ))]]) ).
thf(1792,plain,
! [A: $i] :
( ( ( v1 @ ( A @ greater ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) )
| ~ $true
| ( A = v1 ) ),
inference(paramod_ordered,[status(thm)],[1505,61]) ).
thf(1793,plain,
! [A: $i] :
( ( ( v1 @ ( A @ greater ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) )
| ( A = v1 ) ),
inference(simp,[status(thm)],[1792]) ).
thf(2240,plain,
! [A: $i] :
( ( ( vd520 @ ( vd518 @ vmul ) )
!= v1 )
| ( A
!= ( vd519 @ ( vd517 @ vmul ) ) )
| ( A = v1 ) ),
inference(simp,[status(thm)],[1793]) ).
thf(2333,plain,
( ( ( vd520 @ ( vd518 @ vmul ) )
!= v1 )
| ( ( vd519 @ ( vd517 @ vmul ) )
= v1 ) ),
inference(simp,[status(thm)],[2240]) ).
thf(9911,plain,
! [A: $i] :
( ( A
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( v1 != v1 )
| ( ( vd519 @ ( vd517 @ vmul ) )
= v1 )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,2333]) ).
thf(9912,plain,
! [A: $i] :
( ( A
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( ( vd519 @ ( vd517 @ vmul ) )
= v1 )
| ( v1 @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[9911]) ).
thf(9913,plain,
( ( ( vd519 @ ( vd517 @ vmul ) )
= v1 )
| ( v1 @ ( vd520 @ ( vd518 @ vmul ) @ greater ) ) ),
inference(pattern_uni,[status(thm)],[9912:[bind(A,$thf( vd520 @ ( vd518 @ vmul ) ))]]) ).
thf(15421,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( ( B @ vsucc @ ( A @ vmul ) )
!= D ) ),
inference(paramod_ordered,[status(thm)],[203,153]) ).
thf(15422,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vmul ) )
!= A ),
inference(pattern_uni,[status(thm)],[15421:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ vmul ) )),bind(D,$thf( E ))]]) ).
thf(15592,plain,
! [B: $i,A: $i] :
( ( B @ vsucc @ ( A @ vmul ) )
!= A ),
inference(simp,[status(thm)],[15422]) ).
thf(117,plain,
? [A: $i > $i] :
! [B: $i] :
( ( B @ vsucc @ A )
= B ),
inference(detectInverse,[status(thm)],[116]) ).
thf(118,plain,
! [A: $i] :
( ( A @ vsucc @ sk4 )
= A ),
inference(cnf,[status(esa)],[117]) ).
thf(311,plain,
! [A: $i] :
( ( A @ vsucc @ sk4 )
= A ),
inference(lifteq,[status(thm)],[118]) ).
thf(22540,plain,
( ( ( vd518 @ vsucc )
!= vd519 )
| ( vd520 != vd517 ) ),
inference(simp,[status(thm)],[22480]) ).
thf(125,plain,
! [A: $i,B: $i] :
( ? [C: $i] :
( ( C @ ( A @ vplus ) )
= ( C @ ( B @ vplus ) ) )
=> ( A = B ) ),
inference(miniscope,[status(thm)],[124]) ).
thf(126,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( ( C @ ( A @ vplus ) )
!= ( C @ ( B @ vplus ) ) ) ),
inference(cnf,[status(esa)],[125]) ).
thf(127,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( ( C @ ( A @ vplus ) )
!= ( C @ ( B @ vplus ) ) ) ),
inference(lifteq,[status(thm)],[126]) ).
thf(128,plain,
? [A: $i > $i > $i] :
! [B: $i,C: $i] :
( ( C @ ( B @ vplus ) @ ( C @ A ) )
= B ),
inference(detectInverse,[status(thm)],[127]) ).
thf(129,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ ( B @ sk5 ) )
= A ),
inference(cnf,[status(esa)],[128]) ).
thf(5434,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ ( B @ sk5 ) )
= A ),
inference(lifteq,[status(thm)],[129]) ).
thf(424,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( ( A @ ( B @ vplus ) )
!= C ) ),
inference(paramod_ordered,[status(thm)],[78,75]) ).
thf(425,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) )
!= A ),
inference(pattern_uni,[status(thm)],[424:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(1240,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1012,61]) ).
thf(1241,plain,
! [A: $i] :
( ( A @ ( A @ vsucc @ greater ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) ),
inference(simp,[status(thm)],[1240]) ).
thf(1261,plain,
! [A: $i] :
( ( A
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( ( A @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(simp,[status(thm)],[1241]) ).
thf(1273,plain,
( ( vd520 @ ( vd518 @ vmul ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(simp,[status(thm)],[1261]) ).
thf(558,plain,
( ( ( vd518 @ ( vd519 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( v1 != vd517 )
| ( v1 != vd520 )
| ~ $true
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(paramod_ordered,[status(thm)],[467,322]) ).
thf(559,plain,
( ( ( vd518 @ ( vd519 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( v1 != vd520 )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[558]) ).
thf(565,plain,
( ( vd518 != vd518 )
| ( vd519 != vd517 )
| ( v1 != vd520 )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[559]) ).
thf(573,plain,
( ( vd519 != vd517 )
| ( v1 != vd520 )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[565]) ).
thf(7864,plain,
! [A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ~ ( vd519 @ ( vd517 @ vmul ) @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[205,7779]) ).
thf(7900,plain,
! [A: $i] :
( ( v1 != vd520 )
| ( A != vd518 )
| ~ ( vd519 @ ( vd517 @ vmul ) @ ( A @ less ) ) ),
inference(simp,[status(thm)],[7864]) ).
thf(7910,plain,
( ( v1 != vd520 )
| ~ ( vd519 @ ( vd517 @ vmul ) @ ( vd518 @ less ) ) ),
inference(simp,[status(thm)],[7900]) ).
thf(10394,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ~ $true
| ~ ( vd520 @ ( vd519 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1012,9985]) ).
thf(10395,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ~ ( vd520 @ ( vd519 @ greater ) ) ),
inference(simp,[status(thm)],[10394]) ).
thf(10495,plain,
! [A: $i] :
( ( A != vd518 )
| ( ( A @ vsucc )
!= vd517 )
| ~ ( vd520 @ ( vd519 @ greater ) ) ),
inference(simp,[status(thm)],[10395]) ).
thf(10562,plain,
( ( ( vd518 @ vsucc )
!= vd517 )
| ~ ( vd520 @ ( vd519 @ greater ) ) ),
inference(simp,[status(thm)],[10495]) ).
thf(10767,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ( ( vd518 @ vsucc )
!= vd517 )
| ~ $true
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[209,10562]) ).
thf(10768,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ( ( vd518 @ vsucc )
!= vd517 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[10767]) ).
thf(10769,plain,
( ( ( vd518 @ vsucc )
!= vd517 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[10768:[]]) ).
thf(22461,plain,
( ( vd520 != vd519 )
| ( ( vd518 @ vsucc )
!= vd517 ) ),
inference(simp,[status(thm)],[22266]) ).
thf(22778,plain,
( ( vd520 != vd520 )
| ( vd519 != vd519 )
| ( ( vd518 @ vsucc )
!= vd517 )
| ~ ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[21698,22461]) ).
thf(22779,plain,
( ( vd520 != vd520 )
| ( ( vd518 @ vsucc )
!= vd517 )
| ~ ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[22778]) ).
thf(22780,plain,
( ( ( vd518 @ vsucc )
!= vd517 )
| ~ ( vd518 @ ( vd517 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[22779:[]]) ).
thf(36259,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( ( vd518 @ vsucc )
!= vd517 )
| ~ $true
| ( ( vd518 @ vsucc )
!= vd517 ) ),
inference(paramod_ordered,[status(thm)],[10769,22780]) ).
thf(36260,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( ( vd518 @ vsucc )
!= vd517 ) ),
inference(simp,[status(thm)],[36259]) ).
thf(36261,plain,
( ( vd518 @ vsucc )
!= vd517 ),
inference(pattern_uni,[status(thm)],[36260:[]]) ).
thf(8070,plain,
! [A: $i] :
( ( ( A @ ( v1 @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( v1 != vd517 )
| ~ ( vd519 @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[259,7906]) ).
thf(8099,plain,
! [A: $i] :
( ( A != vd520 )
| ( v1 != vd518 )
| ( v1 != vd517 )
| ~ ( vd519 @ ( A @ less ) ) ),
inference(simp,[status(thm)],[8070]) ).
thf(8110,plain,
( ( v1 != vd518 )
| ( v1 != vd517 )
| ~ ( vd519 @ ( vd520 @ less ) ) ),
inference(simp,[status(thm)],[8099]) ).
thf(277,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)],[276]) ).
thf(279,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)],[277]) ).
thf(7369,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ vplus ) ) )
| ( ( v1 @ vsucc )
!= B )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,383]) ).
thf(7370,plain,
! [B: $i,A: $i] :
( ( ( v1 @ vsucc )
!= A )
| ( v1 @ ( B @ ( A @ vplus ) @ greater ) ) ),
inference(pattern_uni,[status(thm)],[7369:[bind(A,$thf( E @ ( D @ vplus ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(7376,plain,
! [A: $i] : ( v1 @ ( A @ ( v1 @ vsucc @ vplus ) @ greater ) ),
inference(simp,[status(thm)],[7370]) ).
thf(7920,plain,
! [A: $i] : ( v1 @ ( A @ ( v1 @ vplus ) @ vsucc @ greater ) ),
inference(rewrite,[status(thm)],[7376,143]) ).
thf(180,plain,
! [A: $i] : ( v1 @ ( A @ geq ) ),
inference(cnf,[status(esa)],[179]) ).
thf(600,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)],[78,526]) ).
thf(601,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[600:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(26873,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( vd518 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ~ $true
| ( vd520 = vd519 ) ),
inference(paramod_ordered,[status(thm)],[24406,231]) ).
thf(26874,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( vd518 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ( vd520 = vd519 ) ),
inference(simp,[status(thm)],[26873]) ).
thf(26875,plain,
( ( vd518 @ ( v1 @ less ) )
| ( vd520 = vd519 ) ),
inference(pattern_uni,[status(thm)],[26874:[bind(A,$thf( vd518 )),bind(B,$thf( v1 ))]]) ).
thf(1519,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ vplus ) )
!= ( C @ ( vd520 @ ( vd518 @ vmul ) @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[78,1327]) ).
thf(1520,plain,
! [A: $i] :
( ( vd520 @ ( vd518 @ vmul ) @ ( A @ vplus ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[1519:[bind(A,$thf( A )),bind(B,$thf( vd520 @ ( vd518 @ vmul ) )),bind(C,$thf( A ))]]) ).
thf(27086,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ vmul ) @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( D @ vplus ) ) )
| ( ( C @ ( B @ vplus ) @ ( A @ vmul ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[262,1520]) ).
thf(27087,plain,
! [A: $i] :
( ( vd520 @ ( A @ vplus ) @ ( vd518 @ vmul ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[27086:[bind(A,$thf( vd518 )),bind(B,$thf( F )),bind(C,$thf( vd520 )),bind(D,$thf( F @ ( vd518 @ vmul ) ))]]) ).
thf(27286,plain,
! [A: $i] :
( ( vd520 @ ( A @ vplus ) @ ( vd518 @ vmul ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(simp,[status(thm)],[27087]) ).
thf(18688,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vmul ) )
!= ( D @ vsucc @ ( C @ vmul ) ) )
| ( ( A @ ( B @ vmul ) @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[216,15606]) ).
thf(18689,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vsucc @ vmul ) @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[18688:[bind(A,$thf( A )),bind(B,$thf( E @ vsucc )),bind(C,$thf( A )),bind(D,$thf( E ))]]) ).
thf(18726,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vsucc @ vmul ) @ vsucc @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[18689]) ).
thf(662,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( v1 @ vplus ) )
!= ( C @ ( B @ vplus ) ) )
| ( A @ vsucc @ ( B @ less ) ) ),
inference(paramod_ordered,[status(thm)],[178,161]) ).
thf(663,plain,
! [A: $i] : ( A @ vsucc @ ( v1 @ less ) ),
inference(pattern_uni,[status(thm)],[662:[bind(A,$thf( A )),bind(B,$thf( v1 )),bind(C,$thf( A ))]]) ).
thf(8,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(83,plain,
! [A: $i,B: $i] :
( ( v1 @ ( B @ vplus ) @ ( A @ less ) )
=> ( B @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(84,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ~ ( v1 @ ( B @ vplus ) @ ( A @ less ) ) ),
inference(cnf,[status(esa)],[83]) ).
thf(576,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ~ ( B @ vsucc @ ( A @ less ) ) ),
inference(rewrite,[status(thm)],[84,71]) ).
thf(709,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( v1 @ less ) )
!= ( C @ vsucc @ ( B @ less ) ) )
| ( C @ ( B @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[663,576]) ).
thf(710,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( v1 @ less ) )
!= ( C @ vsucc @ ( B @ less ) ) )
| ( C @ ( B @ leq ) ) ),
inference(simp,[status(thm)],[709]) ).
thf(711,plain,
! [A: $i] : ( A @ ( v1 @ leq ) ),
inference(pattern_uni,[status(thm)],[710:[bind(A,$thf( A )),bind(B,$thf( v1 )),bind(C,$thf( A ))]]) ).
thf(5455,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( C @ ( B @ vplus ) ) )
| ( ( A @ vsucc @ ( C @ sk5 ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[71,5434]) ).
thf(5456,plain,
! [A: $i] :
( ( A @ vsucc @ ( v1 @ sk5 ) )
= A ),
inference(pattern_uni,[status(thm)],[5455:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( v1 ))]]) ).
thf(10261,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( B @ leq ) )
!= ( D @ ( C @ leq ) ) )
| ( C @ ( D @ geq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4450,98]) ).
thf(10262,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) @ ( B @ leq ) )
!= ( D @ ( C @ leq ) ) )
| ( C @ ( D @ geq ) ) ),
inference(simp,[status(thm)],[10261]) ).
thf(10263,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( A @ vplus ) @ geq ) ),
inference(pattern_uni,[status(thm)],[10262:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ vplus ) ))]]) ).
thf(10284,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( A @ vplus ) @ geq ) ),
inference(simp,[status(thm)],[10263]) ).
thf(20137,plain,
( ( vd518 != vd518 )
| ( vd517 != vd517 )
| ( v1 @ ( vd518 @ greater ) )
| ( vd517 @ ( vd518 @ less ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[3591,19540]) ).
thf(20138,plain,
( ( vd518 != vd518 )
| ( v1 @ ( vd518 @ greater ) )
| ( vd517 @ ( vd518 @ less ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[20137]) ).
thf(20139,plain,
( ( v1 @ ( vd518 @ greater ) )
| ( vd517 @ ( vd518 @ less ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[20138:[]]) ).
thf(21524,plain,
! [B: $i,A: $i] :
( ( ( vd517 @ ( vd518 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( A @ ( B @ greater ) )
| ~ $true
| ( v1 @ ( vd518 @ greater ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[20139,233]) ).
thf(21525,plain,
! [B: $i,A: $i] :
( ( ( vd517 @ ( vd518 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( A @ ( B @ greater ) )
| ( v1 @ ( vd518 @ greater ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[21524]) ).
thf(21526,plain,
( ( vd518 @ ( vd517 @ greater ) )
| ( v1 @ ( vd518 @ greater ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[21525:[bind(A,$thf( vd518 )),bind(B,$thf( vd517 ))]]) ).
thf(21580,plain,
( ( v1 @ ( vd518 @ greater ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[21526]) ).
thf(1254,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ greater ) ) )
| ( v1 != vd517 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1012,309]) ).
thf(1255,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ greater ) ) )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[1254]) ).
thf(1259,plain,
! [A: $i] :
( ( A
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( ( A @ vsucc )
!= vd519 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[1255]) ).
thf(1271,plain,
( ( ( vd520 @ ( vd518 @ vmul ) @ vsucc )
!= vd519 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[1259]) ).
thf(23,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(144,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)],[23]) ).
thf(1056,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( v1 != vd520 )
| ( v1 != vd519 )
| ~ $true
| ( vd520 != vd518 )
| ( v1 != vd517 )
| ( v1 != vd520 ) ),
inference(paramod_ordered,[status(thm)],[397,317]) ).
thf(1057,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( v1 != vd519 )
| ( vd520 != vd518 )
| ( v1 != vd517 )
| ( v1 != vd520 ) ),
inference(simp,[status(thm)],[1056]) ).
thf(1058,plain,
( ( v1 != vd519 )
| ( vd520 != vd518 )
| ( v1 != vd517 )
| ( v1 != vd520 ) ),
inference(pattern_uni,[status(thm)],[1057:[]]) ).
thf(326,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( vd517 @ greater ) ) )
| ( v1 != vd519 )
| ~ $true
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[209,299]) ).
thf(327,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( vd517 @ greater ) ) )
| ( v1 != vd519 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[326]) ).
thf(335,plain,
( ( ( vd520 @ ( vd518 @ vmul ) )
!= vd520 )
| ( vd519 != vd517 )
| ( v1 != vd519 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[327]) ).
thf(23006,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ~ $true
| ~ ( vd520 @ ( vd519 @ greater ) )
| ( vd518 = vd517 ) ),
inference(paramod_ordered,[status(thm)],[21582,9985]) ).
thf(23007,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ~ ( vd520 @ ( vd519 @ greater ) )
| ( vd518 = vd517 ) ),
inference(simp,[status(thm)],[23006]) ).
thf(23008,plain,
( ~ ( vd520 @ ( vd519 @ greater ) )
| ( vd518 = vd517 ) ),
inference(pattern_uni,[status(thm)],[23007:[]]) ).
thf(171,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ less ) )
=> ! [C: $i] : ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ less ) ) ),
inference(miniscope,[status(thm)],[170]) ).
thf(172,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ less ) )
| ~ ( B @ ( A @ less ) ) ),
inference(cnf,[status(esa)],[171]) ).
thf(109,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ leq ) )
| ( B != A ) ),
inference(cnfConj,[status(thm)],[106]) ).
thf(112,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ leq ) )
| ( B != A ) ),
inference(lifteq,[status(thm)],[109]) ).
thf(113,plain,
! [A: $i] : ( A @ ( A @ leq ) ),
inference(simp,[status(thm)],[112]) ).
thf(16333,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vsucc @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( C @ vsucc @ ( B @ geq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1022,16281]) ).
thf(16334,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vsucc @ greater ) )
!= ( C @ ( B @ greater ) ) )
| ( C @ vsucc @ ( B @ geq ) ) ),
inference(simp,[status(thm)],[16333]) ).
thf(16335,plain,
! [A: $i] : ( v1 @ vsucc @ ( A @ vsucc @ geq ) ),
inference(pattern_uni,[status(thm)],[16334:[bind(A,$thf( D )),bind(B,$thf( D @ vsucc )),bind(C,$thf( v1 ))]]) ).
thf(16389,plain,
! [A: $i] : ( v1 @ vsucc @ ( A @ vsucc @ geq ) ),
inference(simp,[status(thm)],[16335]) ).
thf(16421,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ vsucc @ ( A @ vsucc @ geq ) )
!= ( C @ ( B @ geq ) ) )
| ( B @ ( C @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[16389,103]) ).
thf(16422,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ vsucc @ ( A @ vsucc @ geq ) )
!= ( C @ ( B @ geq ) ) )
| ( B @ ( C @ leq ) ) ),
inference(simp,[status(thm)],[16421]) ).
thf(16423,plain,
! [A: $i] : ( A @ vsucc @ ( v1 @ vsucc @ leq ) ),
inference(pattern_uni,[status(thm)],[16422:[bind(A,$thf( D )),bind(B,$thf( D @ vsucc )),bind(C,$thf( v1 @ vsucc ))]]) ).
thf(16454,plain,
! [A: $i] : ( A @ vsucc @ ( v1 @ vsucc @ leq ) ),
inference(simp,[status(thm)],[16423]) ).
thf(15620,plain,
( ( ( vd520 @ vsucc )
!= vd519 )
| ( vd518 != vd517 ) ),
inference(simp,[status(thm)],[15446]) ).
thf(25516,plain,
( ( vd518 != vd518 )
| ( ( vd520 @ vsucc )
!= vd519 )
| ( vd517 != vd517 )
| ~ ( vd520 @ ( vd519 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[23008,15620]) ).
thf(25517,plain,
( ( vd518 != vd518 )
| ( ( vd520 @ vsucc )
!= vd519 )
| ~ ( vd520 @ ( vd519 @ greater ) ) ),
inference(simp,[status(thm)],[25516]) ).
thf(25518,plain,
( ( ( vd520 @ vsucc )
!= vd519 )
| ~ ( vd520 @ ( vd519 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[25517:[]]) ).
thf(1662,plain,
! [A: $i] :
( ( v1 != v1 )
| ( ( vd520 @ vsucc )
!= vd517 )
| ( A != vd518 )
| ( v1 != vd519 )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,1275]) ).
thf(1663,plain,
! [A: $i] :
( ( ( vd520 @ vsucc )
!= vd517 )
| ( A != vd518 )
| ( v1 != vd519 )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[1662:[]]) ).
thf(2299,plain,
( ( ( vd520 @ vsucc )
!= vd517 )
| ( v1 != vd519 )
| ( v1 @ ( vd518 @ greater ) ) ),
inference(simp,[status(thm)],[1663]) ).
thf(1559,plain,
! [A: $i] :
( ( ( A @ ( v1 @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( ( A @ vsucc @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[259,1529]) ).
thf(1561,plain,
! [A: $i] :
( ( A != vd520 )
| ( v1 != vd518 )
| ( ( A @ vsucc @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(simp,[status(thm)],[1559]) ).
thf(1571,plain,
( ( v1 != vd518 )
| ( ( vd519 @ ( vd517 @ vmul ) )
!= ( vd520 @ vsucc @ vsucc ) ) ),
inference(simp,[status(thm)],[1561]) ).
thf(25467,plain,
( ( vd518 != vd518 )
| ( vd517 != vd517 )
| ~ ( vd518 @ ( v1 @ greater ) )
| ~ ( vd520 @ ( vd519 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[23008,21059]) ).
thf(25468,plain,
( ( vd518 != vd518 )
| ~ ( vd518 @ ( v1 @ greater ) )
| ~ ( vd520 @ ( vd519 @ greater ) ) ),
inference(simp,[status(thm)],[25467]) ).
thf(25469,plain,
( ~ ( vd518 @ ( v1 @ greater ) )
| ~ ( vd520 @ ( vd519 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[25468:[]]) ).
thf(10486,plain,
( ~ $true
| ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ~ ( vd518 @ ( vd517 @ greater ) ) ),
inference(eqfactor_ordered,[status(thm)],[9985]) ).
thf(10498,plain,
( ( vd520 != vd518 )
| ( vd519 != vd517 )
| ~ ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[10486]) ).
thf(15315,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( vd520 != vd518 )
| ( vd519 != vd517 )
| ~ $true
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[209,10498]) ).
thf(15316,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( vd520 != vd518 )
| ( vd519 != vd517 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[15315]) ).
thf(15366,plain,
( ( vd520 != vd518 )
| ( vd519 != vd517 )
| ( vd520 != vd518 )
| ( vd519 != vd517 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[15316]) ).
thf(15388,plain,
( ( vd520 != vd518 )
| ( vd519 != vd517 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[15366]) ).
thf(17969,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( vd520 != vd518 )
| ( vd519 != vd517 )
| ~ $true
| ( vd520 != vd518 )
| ( vd519 != vd517 ) ),
inference(paramod_ordered,[status(thm)],[15388,10498]) ).
thf(17970,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( vd520 != vd518 )
| ( vd519 != vd517 ) ),
inference(simp,[status(thm)],[17969]) ).
thf(17971,plain,
( ( vd520 != vd518 )
| ( vd519 != vd517 ) ),
inference(pattern_uni,[status(thm)],[17970:[]]) ).
thf(302,plain,
! [A: $i] :
( ( ( A @ ( v1 @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ~ ( A @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[259,61]) ).
thf(308,plain,
! [A: $i] :
( ( A != vd520 )
| ( v1 != vd518 )
| ~ ( A @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) ),
inference(simp,[status(thm)],[302]) ).
thf(310,plain,
( ( v1 != vd518 )
| ~ ( vd520 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) ),
inference(simp,[status(thm)],[308]) ).
thf(2082,plain,
! [A: $i] :
( ( v1 != v1 )
| ( A != vd518 )
| ~ ( vd520 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,310]) ).
thf(2083,plain,
! [A: $i] :
( ( A != vd518 )
| ~ ( vd520 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[2082:[]]) ).
thf(2257,plain,
( ~ ( vd520 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) )
| ( v1 @ ( vd518 @ greater ) ) ),
inference(simp,[status(thm)],[2083]) ).
thf(39926,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ( ( vd520 @ vsucc )
!= vd519 )
| ~ $true
| ( vd520 = vd519 ) ),
inference(paramod_ordered,[status(thm)],[21578,25518]) ).
thf(39927,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd520 @ ( vd519 @ greater ) ) )
| ( ( vd520 @ vsucc )
!= vd519 )
| ( vd520 = vd519 ) ),
inference(simp,[status(thm)],[39926]) ).
thf(39928,plain,
( ( ( vd520 @ vsucc )
!= vd519 )
| ( vd520 = vd519 ) ),
inference(pattern_uni,[status(thm)],[39927:[]]) ).
thf(560,plain,
( ( ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( v1 != vd517 )
| ~ $true
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(paramod_ordered,[status(thm)],[467,309]) ).
thf(561,plain,
( ( ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[560]) ).
thf(567,plain,
( ( ( vd520 @ ( vd518 @ vmul ) )
!= vd518 )
| ( vd519 != vd517 )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[561]) ).
thf(7361,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( C @ ( B @ vplus ) ) )
| ( ( A @ vsucc @ vsucc )
!= B ) ),
inference(paramod_ordered,[status(thm)],[71,383]) ).
thf(7362,plain,
! [A: $i] :
( ( A @ vsucc @ vsucc )
!= A ),
inference(pattern_uni,[status(thm)],[7361:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( v1 ))]]) ).
thf(24272,plain,
! [A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( A @ vsucc @ ( A @ greater ) ) )
| ~ $true
| ( v1 != vd518 ) ),
inference(paramod_ordered,[status(thm)],[22914,19676]) ).
thf(24273,plain,
! [A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( A @ vsucc @ ( A @ greater ) ) )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[24272]) ).
thf(24355,plain,
! [A: $i] :
( ( ( A @ vsucc )
!= vd518 )
| ( vd517 != A )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[24273]) ).
thf(24380,plain,
( ( ( vd517 @ vsucc )
!= vd518 )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[24355]) ).
thf(15419,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( C @ ( vd520 @ ( vd518 @ vmul ) @ vplus ) ) )
| ( ( B @ vsucc @ ( A @ vmul ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[203,1327]) ).
thf(15420,plain,
( ( vd520 @ vsucc @ ( vd518 @ vmul ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[15419:[bind(A,$thf( vd518 )),bind(B,$thf( vd520 )),bind(C,$thf( vd518 ))]]) ).
thf(138,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ less ) )
| ( A != B ) ),
inference(cnf,[status(esa)],[137]) ).
thf(139,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ less ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[138]) ).
thf(140,plain,
! [A: $i] :
~ ( A @ ( A @ less ) ),
inference(simp,[status(thm)],[139]) ).
thf(33530,plain,
! [A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( vd520 @ vsucc @ vsucc @ ( vd518 @ vmul ) ) )
| ( A
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[205,33341]) ).
thf(33589,plain,
( ( v1 @ ( vd519 @ ( vd517 @ vmul ) @ vmul ) )
!= ( vd520 @ vsucc @ vsucc @ ( vd518 @ vmul ) ) ),
inference(simp,[status(thm)],[33530]) ).
thf(35598,plain,
( ( vd520 @ vsucc @ vsucc @ ( vd518 @ vmul ) )
!= ( v1 @ ( vd519 @ vmul ) @ ( vd517 @ vmul ) ) ),
inference(rewrite,[status(thm)],[33589,275]) ).
thf(25576,plain,
( ( vd518 != vd518 )
| ~ ( v1 @ ( vd518 @ less ) )
| ( vd517 != vd517 )
| ~ ( vd520 @ ( vd519 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[23008,20214]) ).
thf(25577,plain,
( ( vd518 != vd518 )
| ~ ( v1 @ ( vd518 @ less ) )
| ~ ( vd520 @ ( vd519 @ greater ) ) ),
inference(simp,[status(thm)],[25576]) ).
thf(25578,plain,
( ~ ( v1 @ ( vd518 @ less ) )
| ~ ( vd520 @ ( vd519 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[25577:[]]) ).
thf(26424,plain,
! [B: $i,A: $i] :
( ( ( vd517 @ ( vd518 @ less ) )
!= ( A @ ( B @ less ) ) )
| ( A @ ( B @ leq ) )
| ~ $true
| ( v1 != vd518 ) ),
inference(paramod_ordered,[status(thm)],[24298,111]) ).
thf(26425,plain,
! [B: $i,A: $i] :
( ( ( vd517 @ ( vd518 @ less ) )
!= ( A @ ( B @ less ) ) )
| ( A @ ( B @ leq ) )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[26424]) ).
thf(26426,plain,
( ( vd517 @ ( vd518 @ leq ) )
| ( v1 != vd518 ) ),
inference(pattern_uni,[status(thm)],[26425:[bind(A,$thf( vd517 )),bind(B,$thf( vd518 ))]]) ).
thf(28114,plain,
! [B: $i,A: $i] :
( ( ( vd517 @ ( vd518 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ~ $true
| ( v1 != vd518 ) ),
inference(paramod_ordered,[status(thm)],[26426,98]) ).
thf(28115,plain,
! [B: $i,A: $i] :
( ( ( vd517 @ ( vd518 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( A @ ( B @ geq ) )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[28114]) ).
thf(28116,plain,
( ( vd518 @ ( vd517 @ geq ) )
| ( v1 != vd518 ) ),
inference(pattern_uni,[status(thm)],[28115:[bind(A,$thf( vd518 )),bind(B,$thf( vd517 ))]]) ).
thf(250,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ greater ) )
=> ! [C: $i] : ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) ) ),
inference(miniscope,[status(thm)],[249]) ).
thf(251,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) )
| ~ ( B @ ( A @ greater ) ) ),
inference(cnf,[status(esa)],[250]) ).
thf(36362,plain,
! [A: $i] :
( ( ( A @ vskolem2 @ vsucc )
!= ( vd518 @ vsucc ) )
| ( A != vd517 )
| ( A = v1 ) ),
inference(paramod_ordered,[status(thm)],[101,36261]) ).
thf(36401,plain,
( ( ( vd517 @ vskolem2 )
!= vd518 )
| ( v1 = vd517 ) ),
inference(simp,[status(thm)],[36362]) ).
thf(278,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)],[277]) ).
thf(23060,plain,
! [B: $i,A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( B @ vsucc @ ( A @ geq ) )
| ~ $true
| ( vd518 = vd517 ) ),
inference(paramod_ordered,[status(thm)],[21582,16281]) ).
thf(23061,plain,
! [B: $i,A: $i] :
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( B @ vsucc @ ( A @ geq ) )
| ( vd518 = vd517 ) ),
inference(simp,[status(thm)],[23060]) ).
thf(23062,plain,
( ( vd518 @ vsucc @ ( vd517 @ geq ) )
| ( vd518 = vd517 ) ),
inference(pattern_uni,[status(thm)],[23061:[bind(A,$thf( vd517 )),bind(B,$thf( vd518 ))]]) ).
thf(2226,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ vsucc @ vplus ) ) )
| ( v1 != v1 )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,496]) ).
thf(2227,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ vsucc @ vplus ) ) )
| ( v1 @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[2226]) ).
thf(2228,plain,
! [B: $i,A: $i] : ( v1 @ ( A @ ( B @ vsucc @ vplus ) @ greater ) ),
inference(pattern_uni,[status(thm)],[2227:[bind(A,$thf( E @ ( F @ vsucc @ vplus ) )),bind(B,$thf( F )),bind(C,$thf( E ))]]) ).
thf(2324,plain,
! [B: $i,A: $i] : ( v1 @ ( A @ ( B @ vsucc @ vplus ) @ greater ) ),
inference(simp,[status(thm)],[2228]) ).
thf(4793,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ vplus ) )
!= ( C @ ( D @ vsucc @ vplus ) ) )
| ( v1 @ ( B @ ( A @ vplus ) @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[78,2324]) ).
thf(4794,plain,
! [B: $i,A: $i] : ( v1 @ ( B @ vsucc @ ( A @ vplus ) @ greater ) ),
inference(pattern_uni,[status(thm)],[4793:[bind(A,$thf( A )),bind(B,$thf( E @ vsucc )),bind(C,$thf( A )),bind(D,$thf( E ))]]) ).
thf(4854,plain,
! [B: $i,A: $i] : ( v1 @ ( B @ vsucc @ ( A @ vplus ) @ greater ) ),
inference(simp,[status(thm)],[4794]) ).
thf(5139,plain,
! [B: $i,A: $i] : ( v1 @ ( B @ ( A @ vplus ) @ vsucc @ greater ) ),
inference(rewrite,[status(thm)],[4854,69]) ).
thf(19,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(130,plain,
! [A: $i,B: $i,C: $i] :
( ( ( B @ ( A @ less ) )
& ( C @ ( B @ less ) ) )
=> ( C @ ( A @ less ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(7868,plain,
! [A: $i] :
( ( ( A @ ( v1 @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ~ ( vd519 @ ( vd517 @ vmul ) @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[259,7779]) ).
thf(7902,plain,
! [A: $i] :
( ( A != vd520 )
| ( v1 != vd518 )
| ~ ( vd519 @ ( vd517 @ vmul ) @ ( A @ less ) ) ),
inference(simp,[status(thm)],[7868]) ).
thf(7911,plain,
( ( v1 != vd518 )
| ~ ( vd519 @ ( vd517 @ vmul ) @ ( vd520 @ less ) ) ),
inference(simp,[status(thm)],[7902]) ).
thf(222,plain,
! [A: $i,B: $i] :
( ? [C: $i] : ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) )
=> ( B @ ( A @ greater ) ) ),
inference(miniscope,[status(thm)],[221]) ).
thf(223,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ greater ) )
| ~ ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) ) ),
inference(cnf,[status(esa)],[222]) ).
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(241,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(7355,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc )
!= C ) ),
inference(paramod_ordered,[status(thm)],[78,383]) ).
thf(7356,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vplus ) @ vsucc )
!= B ),
inference(pattern_uni,[status(thm)],[7355:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(4405,plain,
! [A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( v1 != vd519 )
| ( ( A @ vsucc @ vsucc )
!= vd517 ) ),
inference(paramod_ordered,[status(thm)],[205,1567]) ).
thf(4423,plain,
! [A: $i] :
( ( v1 != vd520 )
| ( A != vd518 )
| ( v1 != vd519 )
| ( ( A @ vsucc @ vsucc )
!= vd517 ) ),
inference(simp,[status(thm)],[4405]) ).
thf(4426,plain,
( ( v1 != vd520 )
| ( v1 != vd519 )
| ( ( vd518 @ vsucc @ vsucc )
!= vd517 ) ),
inference(simp,[status(thm)],[4423]) ).
thf(1003,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)],[78,190]) ).
thf(1004,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( A @ vplus ) @ greater ) ),
inference(pattern_uni,[status(thm)],[1003:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(9638,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( D @ ( A @ ( B @ vplus ) @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[78,1004]) ).
thf(9639,plain,
! [B: $i,A: $i] : ( B @ ( A @ ( B @ vplus ) @ greater ) ),
inference(pattern_uni,[status(thm)],[9638:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(145,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)],[144]) ).
thf(28464,plain,
! [B: $i,A: $i] :
( ( ( vd518 @ ( v1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ~ $true
| ~ ( B @ ( A @ greater ) )
| ( vd520 = vd519 ) ),
inference(paramod_ordered,[status(thm)],[26875,227]) ).
thf(28465,plain,
! [B: $i,A: $i] :
( ( ( vd518 @ ( v1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ~ ( B @ ( A @ greater ) )
| ( vd520 = vd519 ) ),
inference(simp,[status(thm)],[28464]) ).
thf(28466,plain,
( ~ ( vd518 @ ( v1 @ greater ) )
| ( vd520 = vd519 ) ),
inference(pattern_uni,[status(thm)],[28465:[bind(A,$thf( v1 )),bind(B,$thf( vd518 ))]]) ).
thf(1252,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd518 @ ( vd519 @ greater ) ) )
| ( v1 != vd517 )
| ( v1 != vd520 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1012,322]) ).
thf(1253,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd518 @ ( vd519 @ greater ) ) )
| ( v1 != vd517 )
| ( v1 != vd520 ) ),
inference(simp,[status(thm)],[1252]) ).
thf(1265,plain,
! [A: $i] :
( ( A != vd518 )
| ( ( A @ vsucc )
!= vd519 )
| ( v1 != vd517 )
| ( v1 != vd520 ) ),
inference(simp,[status(thm)],[1253]) ).
thf(1267,plain,
( ( ( vd518 @ vsucc )
!= vd519 )
| ( v1 != vd517 )
| ( v1 != vd520 ) ),
inference(simp,[status(thm)],[1265]) ).
thf(2073,plain,
! [A: $i] :
( ( v1 != v1 )
| ( ( vd518 @ vsucc )
!= vd519 )
| ( A != vd517 )
| ( v1 != vd520 )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,1267]) ).
thf(2074,plain,
! [A: $i] :
( ( ( vd518 @ vsucc )
!= vd519 )
| ( A != vd517 )
| ( v1 != vd520 )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[2073:[]]) ).
thf(2256,plain,
( ( ( vd518 @ vsucc )
!= vd519 )
| ( v1 != vd520 )
| ( v1 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[2074]) ).
thf(3,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(62,plain,
! [A: $i,B: $i,C: $i] :
( ( ( B @ ( A @ leq ) )
& ( C @ ( B @ leq ) ) )
=> ( C @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(63,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ leq ) )
| ~ ( B @ ( A @ leq ) )
| ~ ( C @ ( B @ leq ) ) ),
inference(cnf,[status(esa)],[62]) ).
thf(20925,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( vd518 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ~ $true
| ( vd518 != vd517 ) ),
inference(paramod_ordered,[status(thm)],[19540,231]) ).
thf(20926,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( vd518 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ( vd518 != vd517 ) ),
inference(simp,[status(thm)],[20925]) ).
thf(20927,plain,
( ( vd518 @ ( v1 @ less ) )
| ( vd518 != vd517 ) ),
inference(pattern_uni,[status(thm)],[20926:[bind(A,$thf( vd518 )),bind(B,$thf( v1 ))]]) ).
thf(23104,plain,
( ( vd518 != vd518 )
| ( vd518 @ ( v1 @ less ) )
| ( vd517 != vd517 )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[21582,20927]) ).
thf(23105,plain,
( ( vd518 != vd518 )
| ( vd518 @ ( v1 @ less ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[23104]) ).
thf(23106,plain,
( ( vd518 @ ( v1 @ less ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[23105:[]]) ).
thf(20946,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ less ) )
!= ( v1 @ ( vd518 @ less ) ) )
| ~ $true
| ( ( vd520 @ vsucc )
!= vd519 )
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[231,19546]) ).
thf(20947,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ less ) )
!= ( v1 @ ( vd518 @ less ) ) )
| ( ( vd520 @ vsucc )
!= vd519 )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[20946]) ).
thf(20948,plain,
( ( ( vd520 @ vsucc )
!= vd519 )
| ~ ( vd518 @ ( v1 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[20947:[bind(A,$thf( v1 )),bind(B,$thf( vd518 ))]]) ).
thf(1660,plain,
! [A: $i] :
( ( v1 != v1 )
| ( ( vd520 @ vsucc )
!= vd517 )
| ( v1 != vd518 )
| ( A != vd519 )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,1275]) ).
thf(1661,plain,
! [A: $i] :
( ( ( vd520 @ vsucc )
!= vd517 )
| ( v1 != vd518 )
| ( A != vd519 )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[1660:[]]) ).
thf(2298,plain,
( ( ( vd520 @ vsucc )
!= vd517 )
| ( v1 != vd518 )
| ( v1 @ ( vd519 @ greater ) ) ),
inference(simp,[status(thm)],[1661]) ).
thf(704,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( C @ ( B @ vplus ) ) )
| ( ( A @ vsucc @ ( B @ sk1 ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[71,695]) ).
thf(705,plain,
! [A: $i] :
( ( A @ vsucc @ ( A @ sk1 ) )
= v1 ),
inference(pattern_uni,[status(thm)],[704:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( v1 ))]]) ).
thf(280,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ leq ) )
!= ( F @ ( E @ leq ) ) )
| ( F @ ( D @ leq ) )
| ~ ( E @ ( D @ leq ) )
| ~ $true
| ~ ( B @ ( A @ leq ) )
| ~ ( C @ ( B @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[63,63]) ).
thf(281,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ leq ) )
!= ( F @ ( E @ leq ) ) )
| ( F @ ( D @ leq ) )
| ~ ( E @ ( D @ leq ) )
| ~ ( B @ ( A @ leq ) )
| ~ ( C @ ( B @ leq ) ) ),
inference(simp,[status(thm)],[280]) ).
thf(282,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( D @ leq ) )
| ~ ( A @ ( D @ leq ) )
| ~ ( B @ ( A @ leq ) )
| ~ ( C @ ( B @ leq ) ) ),
inference(pattern_uni,[status(thm)],[281:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( C ))]]) ).
thf(22277,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( ( B @ ( A @ vsucc @ vmul ) @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[236,515]) ).
thf(22278,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vmul ) @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[22277:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ vmul ) )),bind(D,$thf( F ))]]) ).
thf(22391,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vmul ) @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[22278]) ).
thf(21765,plain,
! [B: $i,A: $i] :
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( B @ vsucc @ ( A @ geq ) )
| ~ $true
| ( vd520 = vd519 ) ),
inference(paramod_ordered,[status(thm)],[21578,16281]) ).
thf(21766,plain,
! [B: $i,A: $i] :
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( B @ vsucc @ ( A @ geq ) )
| ( vd520 = vd519 ) ),
inference(simp,[status(thm)],[21765]) ).
thf(21767,plain,
( ( vd520 @ vsucc @ ( vd519 @ geq ) )
| ( vd520 = vd519 ) ),
inference(pattern_uni,[status(thm)],[21766:[bind(A,$thf( vd519 )),bind(B,$thf( vd520 ))]]) ).
thf(440,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vplus ) )
!= ( D @ ( C @ vplus ) ) )
| ( ( A @ ( B @ vplus ) )
!= D ) ),
inference(paramod_ordered,[status(thm)],[78,153]) ).
thf(441,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vplus ) )
!= B ),
inference(pattern_uni,[status(thm)],[440:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(22289,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( C @ ( D @ vplus ) ) )
| ( ( B @ ( A @ vsucc @ vmul ) @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[236,601]) ).
thf(22290,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vmul ) @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[22289:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ vmul ) ))]]) ).
thf(22395,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vmul ) @ vsucc @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[22290]) ).
thf(24241,plain,
( ( ( vd520 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( v1 != vd518 )
| ( v1 != vd519 )
| ~ $true
| ( v1 != vd518 ) ),
inference(paramod_ordered,[status(thm)],[22914,316]) ).
thf(24242,plain,
( ( ( vd520 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( v1 != vd519 )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[24241]) ).
thf(24366,plain,
( ( vd520 != vd518 )
| ( vd517 != vd517 )
| ( v1 != vd519 )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[24242]) ).
thf(24388,plain,
( ( vd520 != vd518 )
| ( v1 != vd519 )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[24366]) ).
thf(2222,plain,
! [A: $i] :
( ( v1 != v1 )
| ( A != vd517 )
| ~ ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ greater ) )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,309]) ).
thf(2223,plain,
! [A: $i] :
( ( A != vd517 )
| ~ ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ greater ) )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[2222:[]]) ).
thf(2322,plain,
( ~ ( vd520 @ ( vd518 @ vmul ) @ ( vd519 @ greater ) )
| ( v1 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[2223]) ).
thf(16706,plain,
! [B: $i,A: $i] :
( ( ( vd519 @ ( vd517 @ vmul ) )
!= ( B @ ( A @ vmul ) ) )
| ( ( A @ ( B @ vmul ) )
= v1 )
| ( v1 @ ( vd520 @ ( vd518 @ vmul ) @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[9913,216]) ).
thf(16707,plain,
( ( ( vd517 @ ( vd519 @ vmul ) )
= v1 )
| ( v1 @ ( vd520 @ ( vd518 @ vmul ) @ greater ) ) ),
inference(pattern_uni,[status(thm)],[16706:[bind(A,$thf( vd517 )),bind(B,$thf( vd519 ))]]) ).
thf(174,plain,
! [A: $i,B: $i] :
( ? [C: $i] : ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ less ) )
=> ( B @ ( A @ less ) ) ),
inference(miniscope,[status(thm)],[173]) ).
thf(175,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ less ) )
| ~ ( C @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ less ) ) ),
inference(cnf,[status(esa)],[174]) ).
thf(1248,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd520 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) )
| ( v1 != vd518 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1012,310]) ).
thf(1249,plain,
! [A: $i] :
( ( ( A @ ( A @ vsucc @ greater ) )
!= ( vd520 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) ) )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[1248]) ).
thf(1260,plain,
! [A: $i] :
( ( A != vd520 )
| ( ( A @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[1249]) ).
thf(1272,plain,
( ( ( vd519 @ ( vd517 @ vmul ) )
!= ( vd520 @ vsucc ) )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[1260]) ).
thf(41882,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ ( v1 @ vplus ) @ vsucc @ greater ) )
!= ( C @ ( B @ vplus ) @ ( B @ greater ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7920,19668]) ).
thf(41883,plain,
! [C: $i,B: $i,A: $i] :
( ( v1 @ ( A @ ( v1 @ vplus ) @ vsucc @ greater ) )
!= ( C @ ( B @ vplus ) @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[41882]) ).
thf(41965,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ vplus ) )
!= v1 )
| ( ( A @ ( v1 @ vplus ) @ vsucc )
!= B ) ),
inference(simp,[status(thm)],[41883]) ).
thf(42009,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( v1 @ vplus ) @ vsucc @ vplus ) )
!= v1 ),
inference(simp,[status(thm)],[41965]) ).
thf(42408,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( v1 @ vplus ) @ vplus ) @ vsucc )
!= v1 ),
inference(rewrite,[status(thm)],[42009,143]) ).
thf(42467,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( B @ ( v1 @ vplus ) ) )
| ( ( C @ ( A @ vsucc @ vplus ) @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[71,42408]) ).
thf(42468,plain,
! [A: $i] :
( ( A @ ( v1 @ vsucc @ vplus ) @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[42467:[bind(A,$thf( v1 )),bind(B,$thf( v1 ))]]) ).
thf(42571,plain,
! [A: $i] :
( ( A @ ( v1 @ vsucc @ vplus ) @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[42468]) ).
thf(42582,plain,
! [A: $i] :
( ( A @ ( v1 @ vplus ) @ vsucc @ vsucc )
!= v1 ),
inference(rewrite,[status(thm)],[42571,143]) ).
thf(42628,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( B @ ( v1 @ vplus ) ) )
| ( ( A @ vsucc @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[71,42582]) ).
thf(42629,plain,
( ( v1 @ vsucc @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[42628:[bind(A,$thf( v1 )),bind(B,$thf( v1 ))]]) ).
thf(218,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ vplus ) @ ( C @ ( A @ vplus ) @ greater ) )
| ~ ( B @ ( A @ greater ) )
| ~ ( D @ ( C @ greater ) ) ),
inference(cnf,[status(esa)],[217]) ).
thf(22651,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ vmul ) )
!= ( vd520 @ ( vd518 @ vsucc @ vmul ) ) )
| ( ( A @ ( B @ vmul ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[216,22236]) ).
thf(22652,plain,
( ( vd518 @ vsucc @ ( vd520 @ vmul ) @ vsucc )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[22651:[bind(A,$thf( vd518 @ vsucc )),bind(B,$thf( vd520 ))]]) ).
thf(16318,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( vd520 @ ( vd518 @ vmul ) @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( B @ vsucc @ ( A @ geq ) )
| ~ $true
| ( ( vd519 @ ( vd517 @ vmul ) )
= v1 ) ),
inference(paramod_ordered,[status(thm)],[9913,16281]) ).
thf(16319,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( vd520 @ ( vd518 @ vmul ) @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( B @ vsucc @ ( A @ geq ) )
| ( ( vd519 @ ( vd517 @ vmul ) )
= v1 ) ),
inference(simp,[status(thm)],[16318]) ).
thf(16320,plain,
( ( v1 @ vsucc @ ( vd520 @ ( vd518 @ vmul ) @ geq ) )
| ( ( vd519 @ ( vd517 @ vmul ) )
= v1 ) ),
inference(pattern_uni,[status(thm)],[16319:[bind(A,$thf( vd520 @ ( vd518 @ vmul ) )),bind(B,$thf( v1 ))]]) ).
thf(1627,plain,
! [A: $i] :
( ( v1 != v1 )
| ( A != vd518 )
| ( v1 != vd517 )
| ~ ( vd520 @ ( vd519 @ greater ) )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,347]) ).
thf(1628,plain,
! [A: $i] :
( ( A != vd518 )
| ( v1 != vd517 )
| ~ ( vd520 @ ( vd519 @ greater ) )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[1627:[]]) ).
thf(2283,plain,
( ( v1 != vd517 )
| ~ ( vd520 @ ( vd519 @ greater ) )
| ( v1 @ ( vd518 @ greater ) ) ),
inference(simp,[status(thm)],[1628]) ).
thf(15480,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ vmul ) @ vplus ) )
!= ( vd520 @ ( vd518 @ vmul ) @ ( C @ vplus ) ) )
| ( ( B @ vsucc @ ( A @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[203,1312]) ).
thf(15481,plain,
! [A: $i] :
( ( A @ vsucc @ ( vd520 @ ( vd518 @ vmul ) @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[15480:[bind(A,$thf( vd520 @ ( vd518 @ vmul ) )),bind(B,$thf( E )),bind(C,$thf( E @ ( vd520 @ ( vd518 @ vmul ) @ vmul ) ))]]) ).
thf(15617,plain,
! [A: $i] :
( ( A @ vsucc @ ( vd520 @ ( vd518 @ vmul ) @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(simp,[status(thm)],[15481]) ).
thf(18221,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vmul ) )
!= ( C @ vsucc @ ( vd520 @ ( vd518 @ vmul ) @ vmul ) ) )
| ( ( A @ ( B @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[216,15617]) ).
thf(18222,plain,
! [A: $i] :
( ( vd520 @ ( vd518 @ vmul ) @ ( A @ vsucc @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[18221:[bind(A,$thf( vd520 @ ( vd518 @ vmul ) )),bind(B,$thf( F @ vsucc )),bind(C,$thf( F ))]]) ).
thf(18298,plain,
! [A: $i] :
( ( vd520 @ ( vd518 @ vmul ) @ ( A @ vsucc @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(simp,[status(thm)],[18222]) ).
thf(1592,plain,
! [A: $i] :
( ( v1 != v1 )
| ( ( vd519 @ ( vd517 @ vmul ) )
!= ( vd518 @ vsucc ) )
| ( A != vd520 )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,1274]) ).
thf(1593,plain,
! [A: $i] :
( ( ( vd519 @ ( vd517 @ vmul ) )
!= ( vd518 @ vsucc ) )
| ( A != vd520 )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[1592:[]]) ).
thf(2262,plain,
( ( ( vd519 @ ( vd517 @ vmul ) )
!= ( vd518 @ vsucc ) )
| ( v1 @ ( vd520 @ greater ) ) ),
inference(simp,[status(thm)],[1593]) ).
thf(556,plain,
( ( ( vd520 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( v1 != vd518 )
| ~ $true
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(paramod_ordered,[status(thm)],[467,310]) ).
thf(557,plain,
( ( ( vd520 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[556]) ).
thf(568,plain,
( ( vd520 != vd518 )
| ( ( vd519 @ ( vd517 @ vmul ) )
!= vd517 )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[557]) ).
thf(17,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(119,plain,
! [A: $i,B: $i,C: $i] :
( ( A = B )
=> ( ( C @ ( A @ vplus ) )
= ( C @ ( B @ vplus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(242,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)],[241]) ).
thf(243,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)],[242]) ).
thf(244,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ ( B @ sk8 ) @ ( A @ vplus ) ) )
| ~ ( A @ ( B @ greater ) ) ),
inference(cnfConj,[status(thm)],[243]) ).
thf(246,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ greater ) )
| ( ( A @ ( B @ sk8 ) @ ( A @ vplus ) )
= B ) ),
inference(lifteq,[status(thm)],[244]) ).
thf(268,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ geq ) )
| ( B != A ) ),
inference(cnfConj,[status(thm)],[265]) ).
thf(271,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ geq ) )
| ( B != A ) ),
inference(lifteq,[status(thm)],[268]) ).
thf(272,plain,
! [A: $i] : ( A @ ( A @ geq ) ),
inference(simp,[status(thm)],[271]) ).
thf(17400,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vmul ) )
!= ( D @ vsucc @ ( C @ vmul ) ) )
| ( ( A @ ( B @ vmul ) @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[216,15559]) ).
thf(17401,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vsucc @ vmul ) @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[17400:[bind(A,$thf( A )),bind(B,$thf( E @ vsucc )),bind(C,$thf( A )),bind(D,$thf( E ))]]) ).
thf(17447,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ vsucc @ vmul ) @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[17401]) ).
thf(2209,plain,
! [A: $i] :
( ( v1 != v1 )
| ( v1 != vd517 )
| ( A != vd520 )
| ~ ( vd518 @ ( vd519 @ greater ) )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,322]) ).
thf(2210,plain,
! [A: $i] :
( ( v1 != vd517 )
| ( A != vd520 )
| ~ ( vd518 @ ( vd519 @ greater ) )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[2209:[]]) ).
thf(2315,plain,
( ( v1 != vd517 )
| ~ ( vd518 @ ( vd519 @ greater ) )
| ( v1 @ ( vd520 @ greater ) ) ),
inference(simp,[status(thm)],[2210]) ).
thf(4349,plain,
! [A: $i] :
( ( ( v1 @ ( A @ vmul ) )
!= ( vd520 @ ( vd518 @ vmul ) ) )
| ( ( A @ vsucc @ vsucc )
!= vd519 )
| ( v1 != vd517 ) ),
inference(paramod_ordered,[status(thm)],[205,1563]) ).
thf(4367,plain,
! [A: $i] :
( ( v1 != vd520 )
| ( A != vd518 )
| ( ( A @ vsucc @ vsucc )
!= vd519 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[4349]) ).
thf(4372,plain,
( ( v1 != vd520 )
| ( ( vd518 @ vsucc @ vsucc )
!= vd519 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[4367]) ).
thf(500,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( C @ ( B @ vsucc @ vplus ) ) )
| ( ( A @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[71,496]) ).
thf(501,plain,
! [A: $i] :
( ( A @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[500:[bind(A,$thf( D @ vsucc )),bind(B,$thf( D )),bind(C,$thf( v1 ))]]) ).
thf(510,plain,
! [A: $i] :
( ( A @ vsucc @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[501]) ).
thf(22877,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( ( vd520 @ vsucc )
!= vd519 )
| ~ $true
| ( vd518 = vd517 ) ),
inference(paramod_ordered,[status(thm)],[21582,10545]) ).
thf(22878,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( ( vd520 @ vsucc )
!= vd519 )
| ( vd518 = vd517 ) ),
inference(simp,[status(thm)],[22877]) ).
thf(22879,plain,
( ( ( vd520 @ vsucc )
!= vd519 )
| ( vd518 = vd517 ) ),
inference(pattern_uni,[status(thm)],[22878:[]]) ).
thf(33482,plain,
( ( ( vd520 @ vsucc @ vsucc )
!= vd519 )
| ( vd518 != vd517 ) ),
inference(simp,[status(thm)],[33341]) ).
thf(2149,plain,
! [A: $i] :
( ( v1 != v1 )
| ( A != vd520 )
| ~ ( vd518 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,300]) ).
thf(2150,plain,
! [A: $i] :
( ( A != vd520 )
| ~ ( vd518 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[2149:[]]) ).
thf(2287,plain,
( ~ ( vd518 @ ( vd519 @ ( vd517 @ vmul ) @ greater ) )
| ( v1 @ ( vd520 @ greater ) ) ),
inference(simp,[status(thm)],[2150]) ).
thf(24,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(146,plain,
! [A: $i,B: $i] :
( ~ ? [C: $i] :
( B
= ( C @ ( A @ vplus ) ) )
| ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(42222,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ~ $true
| ~ ( vd520 @ ( vd519 @ greater ) )
| ( vd520 != vd519 ) ),
inference(paramod_ordered,[status(thm)],[339,9985]) ).
thf(42223,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ~ ( vd520 @ ( vd519 @ greater ) )
| ( vd520 != vd519 ) ),
inference(simp,[status(thm)],[42222]) ).
thf(42224,plain,
( ~ ( vd520 @ ( vd519 @ greater ) )
| ( vd520 != vd519 ) ),
inference(pattern_uni,[status(thm)],[42223:[]]) ).
thf(24276,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ~ $true
| ~ ( vd520 @ ( vd519 @ greater ) )
| ( v1 != vd518 ) ),
inference(paramod_ordered,[status(thm)],[22914,9985]) ).
thf(24277,plain,
( ( ( vd518 @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ~ ( vd520 @ ( vd519 @ greater ) )
| ( v1 != vd518 ) ),
inference(simp,[status(thm)],[24276]) ).
thf(24278,plain,
( ~ ( vd520 @ ( vd519 @ greater ) )
| ( v1 != vd518 ) ),
inference(pattern_uni,[status(thm)],[24277:[]]) ).
thf(2071,plain,
! [A: $i] :
( ( v1 != v1 )
| ( ( vd518 @ vsucc )
!= vd519 )
| ( v1 != vd517 )
| ( A != vd520 )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,1267]) ).
thf(2072,plain,
! [A: $i] :
( ( ( vd518 @ vsucc )
!= vd519 )
| ( v1 != vd517 )
| ( A != vd520 )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[2071:[]]) ).
thf(2255,plain,
( ( ( vd518 @ vsucc )
!= vd519 )
| ( v1 != vd517 )
| ( v1 @ ( vd520 @ greater ) ) ),
inference(simp,[status(thm)],[2072]) ).
thf(43656,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ less ) )
!= ( vd518 @ ( vd517 @ less ) ) )
| ~ $true
| ( vd520 != vd519 )
| ~ ( B @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[231,42345]) ).
thf(43657,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ less ) )
!= ( vd518 @ ( vd517 @ less ) ) )
| ( vd520 != vd519 )
| ~ ( B @ ( A @ greater ) ) ),
inference(simp,[status(thm)],[43656]) ).
thf(43658,plain,
( ( vd520 != vd519 )
| ~ ( vd517 @ ( vd518 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[43657:[bind(A,$thf( vd518 )),bind(B,$thf( vd517 ))]]) ).
thf(283,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ leq ) )
!= ( E @ ( D @ leq ) ) )
| ( F @ ( D @ leq ) )
| ~ $true
| ~ ( F @ ( E @ leq ) )
| ~ ( B @ ( A @ leq ) )
| ~ ( C @ ( B @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[63,63]) ).
thf(284,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ leq ) )
!= ( E @ ( D @ leq ) ) )
| ( F @ ( D @ leq ) )
| ~ ( F @ ( E @ leq ) )
| ~ ( B @ ( A @ leq ) )
| ~ ( C @ ( B @ leq ) ) ),
inference(simp,[status(thm)],[283]) ).
thf(285,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( A @ leq ) )
| ~ ( D @ ( C @ leq ) )
| ~ ( B @ ( A @ leq ) )
| ~ ( C @ ( B @ leq ) ) ),
inference(pattern_uni,[status(thm)],[284:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( C ))]]) ).
thf(294,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( A @ leq ) )
| ~ ( D @ ( C @ leq ) )
| ~ ( B @ ( A @ leq ) )
| ~ ( C @ ( B @ leq ) ) ),
inference(simp,[status(thm)],[285]) ).
thf(19607,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( v1 @ less ) )
!= ( C @ ( B @ less ) ) )
| ~ $true
| ~ ( C @ ( B @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[663,227]) ).
thf(19608,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ vsucc @ ( v1 @ less ) )
!= ( C @ ( B @ less ) ) )
| ~ ( C @ ( B @ greater ) ) ),
inference(simp,[status(thm)],[19607]) ).
thf(19609,plain,
! [A: $i] :
~ ( A @ vsucc @ ( v1 @ greater ) ),
inference(pattern_uni,[status(thm)],[19608:[bind(A,$thf( D )),bind(B,$thf( v1 )),bind(C,$thf( D @ vsucc ))]]) ).
thf(19674,plain,
! [A: $i] :
~ ( A @ vsucc @ ( v1 @ greater ) ),
inference(simp,[status(thm)],[19609]) ).
thf(21342,plain,
! [B: $i,A: $i] :
( ( ( vd519 @ ( vd520 @ less ) )
!= ( A @ ( B @ less ) ) )
| ( A @ ( B @ leq ) )
| ~ $true
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[21026,111]) ).
thf(21343,plain,
! [B: $i,A: $i] :
( ( ( vd519 @ ( vd520 @ less ) )
!= ( A @ ( B @ less ) ) )
| ( A @ ( B @ leq ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[21342]) ).
thf(21344,plain,
( ( vd519 @ ( vd520 @ leq ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(pattern_uni,[status(thm)],[21343:[bind(A,$thf( vd519 )),bind(B,$thf( vd520 ))]]) ).
thf(194,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) )
| ( A = B ) ),
inference(cnf,[status(esa)],[193]) ).
thf(195,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ less ) )
| ( B @ ( A @ greater ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[194]) ).
thf(543,plain,
( ( ( vd520 @ ( vd518 @ vmul ) @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( v1 != vd519 )
| ~ $true
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(paramod_ordered,[status(thm)],[467,299]) ).
thf(544,plain,
( ( ( vd520 @ ( vd518 @ vmul ) @ ( vd517 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( v1 != vd519 )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[543]) ).
thf(569,plain,
( ( ( vd520 @ ( vd518 @ vmul ) )
!= vd518 )
| ( vd517 != vd517 )
| ( v1 != vd519 )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[544]) ).
thf(575,plain,
( ( ( vd520 @ ( vd518 @ vmul ) )
!= vd518 )
| ( v1 != vd519 )
| ( v1 != vd518 )
| ( v1 != vd517 ) ),
inference(simp,[status(thm)],[569]) ).
thf(26489,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( v1 @ vmul ) )
!= ( C @ ( B @ vmul ) ) )
| ( ( A @ ( C @ sk9 ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[259,26472]) ).
thf(26490,plain,
! [A: $i] :
( ( A @ ( A @ sk9 ) )
= v1 ),
inference(pattern_uni,[status(thm)],[26489:[bind(A,$thf( A )),bind(B,$thf( v1 )),bind(C,$thf( A ))]]) ).
thf(10688,plain,
! [A: $i] :
( ( ( A @ vskolem2 @ vsucc )
!= ( vd520 @ vsucc ) )
| ( A != vd519 )
| ( v1 != vd518 )
| ( A = v1 ) ),
inference(paramod_ordered,[status(thm)],[101,10677]) ).
thf(10713,plain,
( ( ( vd519 @ vskolem2 )
!= vd520 )
| ( v1 != vd518 )
| ( v1 = vd519 ) ),
inference(simp,[status(thm)],[10688]) ).
thf(131,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less ) )
| ~ ( B @ ( A @ less ) )
| ~ ( C @ ( B @ less ) ) ),
inference(cnf,[status(esa)],[130]) ).
thf(20931,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( vd518 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ~ $true
| ( ( vd520 @ vsucc )
!= vd519 ) ),
inference(paramod_ordered,[status(thm)],[10719,231]) ).
thf(20932,plain,
! [B: $i,A: $i] :
( ( ( v1 @ ( vd518 @ greater ) )
!= ( B @ ( A @ greater ) ) )
| ( A @ ( B @ less ) )
| ( ( vd520 @ vsucc )
!= vd519 ) ),
inference(simp,[status(thm)],[20931]) ).
thf(20933,plain,
( ( vd518 @ ( v1 @ less ) )
| ( ( vd520 @ vsucc )
!= vd519 ) ),
inference(pattern_uni,[status(thm)],[20932:[bind(A,$thf( vd518 )),bind(B,$thf( v1 ))]]) ).
thf(27510,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ vsucc @ vplus ) )
!= ( vd520 @ ( C @ vplus ) ) )
| ( ( B @ ( A @ vplus ) @ vsucc @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ) ),
inference(paramod_ordered,[status(thm)],[143,27289]) ).
thf(27511,plain,
! [A: $i] :
( ( vd520 @ ( A @ vplus ) @ vsucc @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(pattern_uni,[status(thm)],[27510:[bind(A,$thf( D )),bind(B,$thf( vd520 )),bind(C,$thf( D @ vsucc ))]]) ).
thf(27616,plain,
! [A: $i] :
( ( vd520 @ ( A @ vplus ) @ vsucc @ ( vd518 @ vmul ) )
!= ( vd519 @ ( vd517 @ vmul ) ) ),
inference(simp,[status(thm)],[27511]) ).
thf(2116,plain,
! [A: $i] :
( ( v1 != v1 )
| ( ( vd519 @ ( vd517 @ vmul ) )
!= ( vd520 @ vsucc ) )
| ( A != vd518 )
| ( v1 @ ( A @ greater ) ) ),
inference(paramod_ordered,[status(thm)],[1505,1272]) ).
thf(2117,plain,
! [A: $i] :
( ( ( vd519 @ ( vd517 @ vmul ) )
!= ( vd520 @ vsucc ) )
| ( A != vd518 )
| ( v1 @ ( A @ greater ) ) ),
inference(pattern_uni,[status(thm)],[2116:[]]) ).
thf(2270,plain,
( ( ( vd519 @ ( vd517 @ vmul ) )
!= ( vd520 @ vsucc ) )
| ( v1 @ ( vd518 @ greater ) ) ),
inference(simp,[status(thm)],[2117]) ).
thf(332,plain,
( ~ $true
| ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(eqfactor_ordered,[status(thm)],[209]) ).
thf(337,plain,
( ( ( vd520 @ ( vd519 @ greater ) )
!= ( vd518 @ ( vd517 @ greater ) ) )
| ( vd518 @ ( vd517 @ greater ) ) ),
inference(simp,[status(thm)],[332]) ).
thf(5457,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( v1 @ vplus ) )
!= ( C @ ( B @ vplus ) ) )
| ( ( A @ vsucc @ ( C @ sk5 ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[178,5434]) ).
thf(5458,plain,
! [A: $i] :
( ( A @ vsucc @ ( A @ sk5 ) )
= v1 ),
inference(pattern_uni,[status(thm)],[5457:[bind(A,$thf( A )),bind(B,$thf( v1 )),bind(C,$thf( A ))]]) ).
thf(580,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)],[69,511]) ).
thf(581,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vplus ) @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[580:[bind(A,$thf( E @ vsucc )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ vsucc ))]]) ).
thf(588,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ vsucc @ vplus ) @ vsucc @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[581]) ).
thf(965,plain,
! [C: $i,B: $i,A: $i] :
( ( ( v1 @ ( A @ vplus ) )
!= ( C @ ( B @ vsucc @ vplus ) ) )
| ( ( A @ vsucc @ vsucc @ vsucc )
!= v1 ) ),
inference(paramod_ordered,[status(thm)],[71,588]) ).
thf(966,plain,
! [A: $i] :
( ( A @ vsucc @ vsucc @ vsucc @ vsucc )
!= v1 ),
inference(pattern_uni,[status(thm)],[965:[bind(A,$thf( D @ vsucc )),bind(B,$thf( D )),bind(C,$thf( v1 ))]]) ).
thf(972,plain,
! [A: $i] :
( ( A @ vsucc @ vsucc @ vsucc @ vsucc )
!= v1 ),
inference(simp,[status(thm)],[966]) ).
thf(52175,plain,
$false,
inference(e,[status(thm)],[69,19672,4450,101,234,33341,88,8200,24265,19540,333,249,170,22480,269,217,276,1275,1327,19668,153,10341,26488,185,26964,42166,2432,4371,10545,15688,1529,257,24958,44588,184,4956,110,196,587,10719,189,93,228,316,42769,78,21582,164,22236,19485,211,8196,8109,216,27615,179,348,574,602,397,19546,61,26198,132,42378,38780,116,16565,10551,221,206,4475,27272,233,27617,270,85,27255,102,1047,220,366,1274,334,260,1570,192,165,7906,275,137,229,252,197,2332,97,1012,224,15559,697,19667,1006,169,141,21026,1270,317,43652,15606,1082,339,526,2317,96,1567,20175,124,225,193,4425,27963,212,985,515,21059,173,24298,42379,237,9913,205,15592,311,1563,22540,5434,24341,19676,9985,15446,425,166,1273,161,573,7910,36261,24406,8110,279,64,7920,180,601,26875,191,27286,18726,711,1520,259,176,5456,10284,71,21580,1271,1312,144,1058,335,236,181,23008,21783,159,172,113,219,16454,25518,2299,230,98,1571,25469,17971,10677,2257,39928,76,567,7362,208,6969,24380,103,15420,140,4452,91,35598,25578,1022,198,28116,240,251,36401,695,278,7805,23062,299,226,5139,15620,130,7911,223,241,7356,24314,4426,21578,162,663,27289,209,9639,145,27437,2333,28466,2256,63,23106,150,1267,20948,22266,16389,2298,525,705,282,22391,263,310,21767,23117,441,16281,127,22395,24388,576,2322,7779,2426,16707,154,22914,175,1272,143,7908,26472,42582,72,24179,42629,231,99,671,218,104,203,20214,22652,16320,2283,18298,114,2262,4451,75,568,119,246,667,272,383,17447,42408,20927,2315,4372,214,21698,510,22879,33482,2287,14030,262,146,190,42224,273,16341,24278,300,2255,43658,210,294,79,2417,26426,23080,19674,94,21344,195,575,26490,10713,131,20933,178,27616,1004,25306,62,1505,42345,2270,111,322,337,4584,83,5458,309,232,972,254,227]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM856+2 : 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.24/0.48 % Computer : n009.cluster.edu
% 0.24/0.48 % Model : x86_64 x86_64
% 0.24/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.24/0.48 % Memory : 8046.5625MB
% 0.24/0.48 % OS : Linux 6.8.0-71-generic
% 0.24/0.48 % CPULimit : 300
% 0.24/0.48 % WCLimit : 300
% 0.24/0.48 % DateTime : Sat Sep 26 04:13:44 UTC 2026
% 0.24/0.48 % CPUTime :
% 0.24/0.48 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.33/1.27 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 2.23/1.61 % [INFO] Parsing done (343ms).
% 2.23/1.63 % [INFO] Running in sequential loop mode.
% 3.51/2.22 % [INFO] eprover registered as external prover.
% 3.51/2.23 % [INFO] Scanning for conjecture ...
% 3.67/2.37 % [INFO] Found a conjecture (or negated_conjecture) and 58 axioms. Running axiom selection ...
% 3.84/2.49 % [INFO] Axiom selection finished. Selected 58 axioms (removed 0 axioms).
% 4.28/2.64 % [INFO] Problem is first-order (TPTP FOF).
% 4.28/2.66 % [INFO] Type checking passed.
% 4.28/2.67 % [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 ...
% 90.19/19.54 % External prover 'e' found a proof!
% 90.19/19.54 % [INFO] Killing All external provers ...
% 90.19/19.54 % Time passed: 18854ms (effective reasoning time: 17898ms)
% 90.19/19.54 % 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)>
% 90.19/19.55 % Axioms used in derivation (58): ass(cond(223, 0), 0), ass(cond(6, 0), 0), def(cond(conseq(axiom(3)), 16), 1), ass(cond(228, 0), 0), ass(cond(241, 0), 0), ass(cond(12, 0), 0), ass(cond(140, 0), 0), def(cond(conseq(axiom(3)), 12), 1), ass(cond(81, 0), 0), ass(cond(conjunct2(conjunct2(307)), 0), 0), ass(cond(goal(193), 0), 0), ass(cond(goal(130), 0), 1), ass(cond(163, 0), 0), ass(cond(goal(177), 0), 0), ass(cond(goal(193), 0), 2), def(cond(conseq(axiom(3)), 11), 1), ass(cond(312, 0), 0), ass(cond(299, 0), 0), ass(cond(299, 0), 2), ass(cond(299, 0), 1), 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), 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(goal(202), 0), 2), ass(cond(270, 0), 0), ass(cond(184, 0), 0), ass(cond(goal(88), 0), 2), dis(antec(scope(318))), 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), ass(cond(conjunct1(307), 0), 0), ass(cond(20, 0), 0), ass(cond(goal(202), 0), 1), ass(cond(goal(216), 0), 0), ass(cond(281, 0), 0), ass(cond(253, 0), 0), qu(antec(axiom(3)), imp(antec(axiom(3)))), ass(cond(209, 0), 0), ass(cond(261, 0), 0), ass(cond(52, 0), 0), ass(cond(conjunct1(conjunct2(307)), 0), 0), ass(cond(158, 0), 0), ass(cond(234, 0), 0), ass(cond(33, 0), 0), ass(cond(290, 0), 0), qu(restrictor(axiom(1)), holds(scope(axiom(1)), 2, 0)), ass(cond(61, 0), 0), ass(cond(goal(130), 0), 2), ass(cond(goal(202), 0), 0), ass(cond(168, 0), 0), ass(cond(43, 0), 0)
% 90.19/19.55 % No. of inferences in proof: 1011
% 90.19/19.55 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 18854 ms resp. 17898 ms w/o parsing
% 77.26/19.83 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 77.26/19.84 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------