%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : KLE170+1.002 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n019.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 07:43:21 AM UTC 2026
% Result : Theorem 99.04s 21.80s
% Output : Refutation 100.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 17
% Syntax : Number of formulae : 400 ( 195 unt; 0 typ; 0 def)
% Number of atoms : 734 ( 488 equ; 0 cnn)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 3389 ( 420 ~; 250 |; 3 &;2707 @)
% ( 1 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 10 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 713 ( 0 ^; 713 !; 0 ?; 713 :)
% Comments :
%------------------------------------------------------------------------------
thf(leq_decl,type,
leq: $i > $i > $o ).
thf(multiplication_decl,type,
multiplication: $i > $i > $i ).
thf(a_decl,type,
a: $i ).
thf(star_decl,type,
star: $i > $i ).
thf(addition_decl,type,
addition: $i > $i > $i ).
thf(zero_decl,type,
zero: $i ).
thf(one_decl,type,
one: $i ).
thf(8,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= ( C @ ( B @ ( A @ multiplication ) @ multiplication ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_associativity) ).
thf(35,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= ( C @ ( B @ ( A @ multiplication ) @ multiplication ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(36,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= ( C @ ( B @ ( A @ multiplication ) @ multiplication ) ) ),
inference(cnf,[status(esa)],[35]) ).
thf(37,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
= ( C @ ( B @ multiplication ) @ ( A @ multiplication ) ) ),
inference(lifteq,[status(thm)],[36]) ).
thf(314,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( E @ ( D @ multiplication ) ) )
| ( ( F @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ multiplication ) )
= ( F @ ( E @ multiplication ) @ ( D @ multiplication ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,37]) ).
thf(315,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ multiplication ) @ ( C @ multiplication ) @ multiplication ) )
= ( B @ ( A @ multiplication ) @ ( D @ ( C @ multiplication ) @ multiplication ) ) ),
inference(pattern_uni,[status(thm)],[314:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ multiplication ) )),bind(E,$thf( C ))]]) ).
thf(343,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ multiplication ) @ ( C @ multiplication ) @ multiplication ) )
= ( B @ ( A @ multiplication ) @ ( D @ ( C @ multiplication ) @ multiplication ) ) ),
inference(simp,[status(thm)],[315]) ).
thf(9516,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ multiplication ) @ multiplication ) @ ( C @ multiplication ) )
= ( B @ ( A @ multiplication ) @ ( D @ multiplication ) @ ( C @ multiplication ) ) ),
inference(rewrite,[status(thm)],[343,37]) ).
thf(12,axiom,
! [A: $i] :
( ( one @ ( A @ multiplication ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_right_identity) ).
thf(46,plain,
! [A: $i] :
( ( one @ ( A @ multiplication ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(47,plain,
! [A: $i] :
( ( one @ ( A @ multiplication ) )
= A ),
inference(cnf,[status(esa)],[46]) ).
thf(48,plain,
! [A: $i] :
( ( one @ ( A @ multiplication ) )
= A ),
inference(lifteq,[status(thm)],[47]) ).
thf(13,axiom,
! [A: $i] : ( A @ star @ ( A @ ( A @ star @ multiplication ) @ ( one @ addition ) @ leq ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',star_unfold_left) ).
thf(49,plain,
! [A: $i] : ( A @ star @ ( A @ ( A @ star @ multiplication ) @ ( one @ addition ) @ leq ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(50,plain,
! [A: $i] : ( A @ star @ ( A @ ( A @ star @ multiplication ) @ ( one @ addition ) @ leq ) ),
inference(cnf,[status(esa)],[49]) ).
thf(453,plain,
! [B: $i,A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( B @ ( B @ star @ multiplication ) ) )
| ( B @ star @ ( A @ ( one @ addition ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[48,50]) ).
thf(454,plain,
one @ star @ ( one @ star @ ( one @ addition ) @ leq ),
inference(pattern_uni,[status(thm)],[453:[bind(A,$thf( one @ star )),bind(B,$thf( one ))]]) ).
thf(18,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
<=> ( ( B @ ( A @ addition ) )
= B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',order) ).
thf(61,plain,
! [A: $i,B: $i] :
( ( ( ( B @ ( A @ addition ) )
= B )
=> ( B @ ( A @ leq ) ) )
& ( ( B @ ( A @ leq ) )
=> ( ( B @ ( A @ addition ) )
= B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(62,plain,
( ! [A: $i,B: $i] :
( ( ( B @ ( A @ addition ) )
= B )
=> ( B @ ( A @ leq ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
=> ( ( B @ ( A @ addition ) )
= B ) ) ),
inference(miniscope,[status(thm)],[61]) ).
thf(63,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ leq ) )
| ( ( D @ ( C @ addition ) )
!= D ) )
& ( ( ( B @ ( A @ addition ) )
= B )
| ~ ( B @ ( A @ leq ) ) ) ),
inference(cnf,[status(esa)],[62]) ).
thf(64,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
= B )
| ~ ( B @ ( A @ leq ) ) ),
inference(cnfConj,[status(thm)],[63]) ).
thf(66,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ leq ) )
| ( ( B @ ( A @ addition ) )
= B ) ),
inference(lifteq,[status(thm)],[64]) ).
thf(1112,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( one @ star @ ( one @ addition ) @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[454,66]) ).
thf(1113,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( one @ star @ ( one @ addition ) @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( ( B @ ( A @ addition ) )
= B ) ),
inference(simp,[status(thm)],[1112]) ).
thf(1114,plain,
( ( one @ star @ ( one @ star @ ( one @ addition ) @ addition ) )
= ( one @ star ) ),
inference(pattern_uni,[status(thm)],[1113:[bind(A,$thf( one @ star @ ( one @ addition ) )),bind(B,$thf( one @ star ))]]) ).
thf(3,axiom,
! [A: $i,B: $i,C: $i] :
( ( A @ ( B @ addition ) @ ( C @ addition ) )
= ( A @ ( B @ ( C @ addition ) @ addition ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_associativity) ).
thf(20,plain,
! [A: $i,B: $i,C: $i] :
( ( A @ ( B @ addition ) @ ( C @ addition ) )
= ( A @ ( B @ ( C @ addition ) @ addition ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(21,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ addition ) @ ( C @ addition ) )
= ( A @ ( B @ ( C @ addition ) @ addition ) ) ),
inference(cnf,[status(esa)],[20]) ).
thf(22,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( C @ addition ) @ addition ) )
= ( A @ ( B @ addition ) @ ( C @ addition ) ) ),
inference(lifteq,[status(thm)],[21]) ).
thf(1250,plain,
( ( one @ star @ ( one @ star @ addition ) @ ( one @ addition ) )
= ( one @ star ) ),
inference(rewrite,[status(thm)],[1114,22]) ).
thf(6,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ addition ) )
= ( A @ ( B @ addition ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_commutativity) ).
thf(29,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ addition ) )
= ( A @ ( B @ addition ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(30,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) )
= ( A @ ( B @ addition ) ) ),
inference(cnf,[status(esa)],[29]) ).
thf(31,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) )
= ( A @ ( B @ addition ) ) ),
inference(lifteq,[status(thm)],[30]) ).
thf(1289,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( one @ star @ addition ) @ ( one @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= ( one @ star ) ) ),
inference(paramod_ordered,[status(thm)],[1250,31]) ).
thf(1290,plain,
( ( one @ ( one @ star @ ( one @ star @ addition ) @ addition ) )
= ( one @ star ) ),
inference(pattern_uni,[status(thm)],[1289:[bind(A,$thf( one )),bind(B,$thf( one @ star @ ( one @ star @ addition ) ))]]) ).
thf(1708,plain,
( ( one @ ( one @ star @ addition ) @ ( one @ star @ addition ) )
= ( one @ star ) ),
inference(rewrite,[status(thm)],[1290,22]) ).
thf(1763,plain,
! [B: $i,A: $i] :
( ( ( one @ ( one @ star @ addition ) @ ( one @ star @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= ( one @ star ) ) ),
inference(paramod_ordered,[status(thm)],[1708,31]) ).
thf(1764,plain,
( ( one @ star @ ( one @ ( one @ star @ addition ) @ addition ) )
= ( one @ star ) ),
inference(pattern_uni,[status(thm)],[1763:[bind(A,$thf( one @ star )),bind(B,$thf( one @ ( one @ star @ addition ) ))]]) ).
thf(1828,plain,
( ( one @ star @ ( one @ addition ) @ ( one @ star @ addition ) )
= ( one @ star ) ),
inference(rewrite,[status(thm)],[1764,22]) ).
thf(17,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ addition ) @ ( A @ multiplication ) )
= ( C @ ( A @ multiplication ) @ ( B @ ( A @ multiplication ) @ addition ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_distributivity) ).
thf(58,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ addition ) @ ( A @ multiplication ) )
= ( C @ ( A @ multiplication ) @ ( B @ ( A @ multiplication ) @ addition ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(59,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ addition ) @ ( A @ multiplication ) )
= ( C @ ( A @ multiplication ) @ ( B @ ( A @ multiplication ) @ addition ) ) ),
inference(cnf,[status(esa)],[58]) ).
thf(60,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ multiplication ) @ ( B @ ( A @ multiplication ) @ addition ) )
= ( C @ ( B @ addition ) @ ( A @ multiplication ) ) ),
inference(lifteq,[status(thm)],[59]) ).
thf(4,axiom,
! [A: $i] :
( ( A @ ( A @ addition ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_idempotence) ).
thf(23,plain,
! [A: $i] :
( ( A @ ( A @ addition ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(24,plain,
! [A: $i] :
( ( A @ ( A @ addition ) )
= A ),
inference(cnf,[status(esa)],[23]) ).
thf(25,plain,
! [A: $i] :
( ( A @ ( A @ addition ) )
= A ),
inference(lifteq,[status(thm)],[24]) ).
thf(186,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ addition ) )
!= ( C @ ( D @ addition ) ) )
| ( ( B @ ( A @ addition ) )
= ( B @ ( C @ addition ) @ ( D @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,22]) ).
thf(187,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) @ ( A @ addition ) )
= ( B @ ( A @ addition ) ) ),
inference(pattern_uni,[status(thm)],[186:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( A ))]]) ).
thf(65,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ( ( B @ ( A @ addition ) )
!= B ) ),
inference(cnfConj,[status(thm)],[63]) ).
thf(67,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ( ( B @ ( A @ addition ) )
!= B ) ),
inference(lifteq,[status(thm)],[65]) ).
thf(68,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ( ( B @ ( A @ addition ) )
!= B ) ),
inference(simp,[status(thm)],[67]) ).
thf(3421,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ addition ) @ ( A @ addition ) )
!= ( D @ ( C @ addition ) ) )
| ( D @ ( C @ leq ) )
| ( ( B @ ( A @ addition ) )
!= D ) ),
inference(paramod_ordered,[status(thm)],[187,68]) ).
thf(3422,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) @ ( A @ leq ) )
| ( ( B @ ( A @ addition ) )
!= ( B @ ( A @ addition ) ) ) ),
inference(pattern_uni,[status(thm)],[3421:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ addition ) ))]]) ).
thf(3474,plain,
! [B: $i,A: $i] : ( B @ ( A @ addition ) @ ( A @ leq ) ),
inference(simp,[status(thm)],[3422]) ).
thf(1,conjecture,
a @ star @ ( a @ ( a @ multiplication ) @ leq ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a) ).
thf(2,negated_conjecture,
~ ( a @ star @ ( a @ ( a @ multiplication ) @ leq ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(19,plain,
~ ( a @ star @ ( a @ ( a @ multiplication ) @ leq ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(5590,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) @ ( A @ leq ) )
!= ( a @ star @ ( a @ ( a @ multiplication ) @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3474,19]) ).
thf(5591,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) @ ( A @ leq ) )
!= ( a @ star @ ( a @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[5590]) ).
thf(5636,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( a @ star ) )
| ( A
!= ( a @ ( a @ multiplication ) ) ) ),
inference(simp,[status(thm)],[5591]) ).
thf(5642,plain,
! [A: $i] :
( ( A @ ( a @ ( a @ multiplication ) @ addition ) )
!= ( a @ star ) ),
inference(simp,[status(thm)],[5636]) ).
thf(5698,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= ( C @ ( a @ ( a @ multiplication ) @ addition ) ) )
| ( ( B @ ( A @ addition ) )
!= ( a @ star ) ) ),
inference(paramod_ordered,[status(thm)],[31,5642]) ).
thf(5699,plain,
! [A: $i] :
( ( a @ ( a @ multiplication ) @ ( A @ addition ) )
!= ( a @ star ) ),
inference(pattern_uni,[status(thm)],[5698:[bind(A,$thf( A )),bind(B,$thf( a @ ( a @ multiplication ) )),bind(C,$thf( A ))]]) ).
thf(5791,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ multiplication ) @ ( B @ ( A @ multiplication ) @ addition ) )
!= ( a @ ( a @ multiplication ) @ ( D @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ multiplication ) )
!= ( a @ star ) ) ),
inference(paramod_ordered,[status(thm)],[60,5699]) ).
thf(5792,plain,
! [A: $i] :
( ( a @ ( A @ addition ) @ ( a @ multiplication ) )
!= ( a @ star ) ),
inference(pattern_uni,[status(thm)],[5791:[bind(A,$thf( a )),bind(B,$thf( F )),bind(C,$thf( a )),bind(D,$thf( F @ ( a @ multiplication ) ))]]) ).
thf(5878,plain,
! [A: $i] :
( ( a @ ( A @ addition ) @ ( a @ multiplication ) )
!= ( a @ star ) ),
inference(simp,[status(thm)],[5792]) ).
thf(14,axiom,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
= zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_annihilation) ).
thf(51,plain,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
= zero ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(52,plain,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
= zero ),
inference(cnf,[status(esa)],[51]) ).
thf(53,plain,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
= zero ),
inference(lifteq,[status(thm)],[52]) ).
thf(444,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( A @ multiplication ) )
!= ( B @ ( B @ star @ multiplication ) ) )
| ( B @ star @ ( zero @ ( one @ addition ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[53,50]) ).
thf(445,plain,
zero @ star @ ( zero @ ( one @ addition ) @ leq ),
inference(pattern_uni,[status(thm)],[444:[bind(A,$thf( zero @ star )),bind(B,$thf( zero ))]]) ).
thf(5,axiom,
! [A: $i] :
( ( zero @ ( A @ addition ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_identity) ).
thf(26,plain,
! [A: $i] :
( ( zero @ ( A @ addition ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(27,plain,
! [A: $i] :
( ( zero @ ( A @ addition ) )
= A ),
inference(cnf,[status(esa)],[26]) ).
thf(28,plain,
! [A: $i] :
( ( zero @ ( A @ addition ) )
= A ),
inference(lifteq,[status(thm)],[27]) ).
thf(499,plain,
zero @ star @ ( one @ leq ),
inference(rewrite,[status(thm)],[445,28]) ).
thf(1069,plain,
! [B: $i,A: $i] :
( ( ( zero @ star @ ( one @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[499,66]) ).
thf(1070,plain,
! [B: $i,A: $i] :
( ( ( zero @ star @ ( one @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( ( B @ ( A @ addition ) )
= B ) ),
inference(simp,[status(thm)],[1069]) ).
thf(1071,plain,
( ( zero @ star @ ( one @ addition ) )
= ( zero @ star ) ),
inference(pattern_uni,[status(thm)],[1070:[bind(A,$thf( one )),bind(B,$thf( zero @ star ))]]) ).
thf(1149,plain,
! [B: $i,A: $i] :
( ( ( zero @ star @ ( one @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= ( zero @ star ) ) ),
inference(paramod_ordered,[status(thm)],[1071,31]) ).
thf(1150,plain,
( ( one @ ( zero @ star @ addition ) )
= ( zero @ star ) ),
inference(pattern_uni,[status(thm)],[1149:[bind(A,$thf( one )),bind(B,$thf( zero @ star ))]]) ).
thf(1196,plain,
! [C: $i,B: $i,A: $i] :
( ( ( one @ ( zero @ star @ addition ) )
!= ( B @ ( C @ addition ) ) )
| ( ( A @ ( zero @ star @ addition ) )
= ( A @ ( B @ addition ) @ ( C @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[1150,22]) ).
thf(1197,plain,
! [A: $i] :
( ( A @ ( one @ addition ) @ ( zero @ star @ addition ) )
= ( A @ ( zero @ star @ addition ) ) ),
inference(pattern_uni,[status(thm)],[1196:[bind(A,$thf( A )),bind(B,$thf( one )),bind(C,$thf( zero @ star ))]]) ).
thf(215,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( D @ ( E @ addition ) ) )
| ( ( C @ ( A @ ( B @ addition ) @ addition ) )
= ( C @ ( D @ addition ) @ ( E @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[31,22]) ).
thf(216,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ addition ) @ addition ) )
= ( C @ ( B @ addition ) @ ( A @ addition ) ) ),
inference(pattern_uni,[status(thm)],[215:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( B )),bind(E,$thf( A ))]]) ).
thf(4102,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ addition ) @ ( B @ addition ) )
= ( C @ ( B @ addition ) @ ( A @ addition ) ) ),
inference(rewrite,[status(thm)],[216,22]) ).
thf(7,axiom,
! [A: $i] :
( ( A @ ( zero @ multiplication ) )
= zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_annihilation) ).
thf(32,plain,
! [A: $i] :
( ( A @ ( zero @ multiplication ) )
= zero ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(33,plain,
! [A: $i] :
( ( A @ ( zero @ multiplication ) )
= zero ),
inference(cnf,[status(esa)],[32]) ).
thf(34,plain,
! [A: $i] :
( ( A @ ( zero @ multiplication ) )
= zero ),
inference(lifteq,[status(thm)],[33]) ).
thf(10,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ addition ) @ multiplication ) )
= ( C @ ( B @ multiplication ) @ ( C @ ( A @ multiplication ) @ addition ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_distributivity) ).
thf(40,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ addition ) @ multiplication ) )
= ( C @ ( B @ multiplication ) @ ( C @ ( A @ multiplication ) @ addition ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(41,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ addition ) @ multiplication ) )
= ( C @ ( B @ multiplication ) @ ( C @ ( A @ multiplication ) @ addition ) ) ),
inference(cnf,[status(esa)],[40]) ).
thf(42,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ multiplication ) @ ( C @ ( A @ multiplication ) @ addition ) )
= ( C @ ( B @ ( A @ addition ) @ multiplication ) ) ),
inference(lifteq,[status(thm)],[41]) ).
thf(201,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( zero @ ( C @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[31,28]) ).
thf(202,plain,
! [A: $i] :
( ( A @ ( zero @ addition ) )
= A ),
inference(pattern_uni,[status(thm)],[201:[bind(A,$thf( A )),bind(B,$thf( zero )),bind(C,$thf( A ))]]) ).
thf(249,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( D @ ( zero @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[22,202]) ).
thf(258,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A != D )
| ( ( B @ ( C @ addition ) )
!= zero )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
= D ) ),
inference(simp,[status(thm)],[249]) ).
thf(261,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= zero )
| ( ( C @ ( A @ addition ) @ ( B @ addition ) )
= C ) ),
inference(simp,[status(thm)],[258]) ).
thf(6523,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ addition ) @ ( B @ addition ) )
!= ( D @ ( a @ ( a @ multiplication ) @ addition ) ) )
| ( C
!= ( a @ star ) )
| ( ( A @ ( B @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[261,5642]) ).
thf(6524,plain,
! [B: $i,A: $i] :
( ( B
!= ( a @ star ) )
| ( ( A @ ( a @ ( a @ multiplication ) @ addition ) )
!= zero ) ),
inference(pattern_uni,[status(thm)],[6523:[bind(A,$thf( G )),bind(B,$thf( a @ ( a @ multiplication ) )),bind(C,$thf( H )),bind(D,$thf( H @ ( G @ addition ) ))]]) ).
thf(6608,plain,
! [A: $i] :
( ( A @ ( a @ ( a @ multiplication ) @ addition ) )
!= zero ),
inference(simp,[status(thm)],[6524]) ).
thf(6696,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ multiplication ) @ ( C @ ( A @ multiplication ) @ addition ) )
!= ( D @ ( a @ ( a @ multiplication ) @ addition ) ) )
| ( ( C @ ( B @ ( A @ addition ) @ multiplication ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[42,6608]) ).
thf(6697,plain,
! [A: $i] :
( ( a @ ( A @ ( a @ addition ) @ multiplication ) )
!= zero ),
inference(pattern_uni,[status(thm)],[6696:[bind(A,$thf( a )),bind(B,$thf( E )),bind(C,$thf( a )),bind(D,$thf( a @ ( E @ multiplication ) ))]]) ).
thf(6773,plain,
! [A: $i] :
( ( a @ ( A @ ( a @ addition ) @ multiplication ) )
!= zero ),
inference(simp,[status(thm)],[6697]) ).
thf(7386,plain,
! [B: $i,A: $i] :
( ( ( A @ ( zero @ multiplication ) )
!= ( a @ ( B @ ( a @ addition ) @ multiplication ) ) )
| ( zero != zero ) ),
inference(paramod_ordered,[status(thm)],[34,6773]) ).
thf(7387,plain,
! [B: $i,A: $i] :
( ( A @ ( zero @ multiplication ) )
!= ( a @ ( B @ ( a @ addition ) @ multiplication ) ) ),
inference(simp,[status(thm)],[7386]) ).
thf(7431,plain,
! [B: $i,A: $i] :
( ( A != a )
| ( ( B @ ( a @ addition ) )
!= zero ) ),
inference(simp,[status(thm)],[7387]) ).
thf(7440,plain,
! [A: $i] :
( ( A @ ( a @ addition ) )
!= zero ),
inference(simp,[status(thm)],[7431]) ).
thf(7500,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ addition ) @ ( B @ addition ) )
!= ( D @ ( a @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[4102,7440]) ).
thf(7501,plain,
! [B: $i,A: $i] :
( ( B @ ( a @ addition ) @ ( A @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[7500:[bind(A,$thf( E )),bind(B,$thf( a )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ addition ) ))]]) ).
thf(7526,plain,
! [B: $i,A: $i] :
( ( B @ ( a @ addition ) @ ( A @ addition ) )
!= zero ),
inference(simp,[status(thm)],[7501]) ).
thf(8578,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= ( D @ ( a @ addition ) @ ( C @ addition ) ) )
| ( ( B @ ( A @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[31,7526]) ).
thf(8579,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( a @ addition ) @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[8578:[bind(A,$thf( F @ ( a @ addition ) )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( F ))]]) ).
thf(8626,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( a @ addition ) @ addition ) )
!= zero ),
inference(simp,[status(thm)],[8579]) ).
thf(9899,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ addition ) @ ( a @ addition ) )
!= zero ),
inference(rewrite,[status(thm)],[8626,22]) ).
thf(9992,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( one @ addition ) @ ( zero @ star @ addition ) )
!= ( B @ ( C @ addition ) ) )
| ( ( A @ ( zero @ star @ addition ) @ ( a @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[1197,9899]) ).
thf(9993,plain,
! [A: $i] :
( ( A @ ( zero @ star @ addition ) @ ( a @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[9992:[bind(A,$thf( F )),bind(B,$thf( F @ ( one @ addition ) )),bind(C,$thf( zero @ star ))]]) ).
thf(10017,plain,
! [A: $i] :
( ( A @ ( zero @ star @ addition ) @ ( a @ addition ) )
!= zero ),
inference(simp,[status(thm)],[9993]) ).
thf(16,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ ( B @ ( A @ multiplication ) @ addition ) @ leq ) )
=> ( B @ ( C @ ( A @ star @ multiplication ) @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',star_induction_left) ).
thf(56,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ ( B @ ( A @ multiplication ) @ addition ) @ leq ) )
=> ( B @ ( C @ ( A @ star @ multiplication ) @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(7494,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( C @ ( a @ addition ) ) )
| ( B != zero )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[66,7440]) ).
thf(7495,plain,
! [A: $i] :
( ( A != zero )
| ~ ( A @ ( a @ leq ) ) ),
inference(pattern_uni,[status(thm)],[7494:[bind(A,$thf( a )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(7524,plain,
~ ( zero @ ( a @ leq ) ),
inference(simp,[status(thm)],[7495]) ).
thf(223,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( D @ ( E @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
= ( E @ ( D @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,31]) ).
thf(224,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ addition ) @ ( B @ addition ) )
= ( C @ ( B @ addition ) @ ( A @ addition ) ) ),
inference(pattern_uni,[status(thm)],[223:[bind(A,$thf( A )),bind(B,$thf( G )),bind(C,$thf( F )),bind(D,$thf( A )),bind(E,$thf( G @ ( F @ addition ) ))]]) ).
thf(225,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ addition ) @ ( B @ addition ) )
= ( C @ ( B @ addition ) @ ( A @ addition ) ) ),
inference(simp,[status(thm)],[224]) ).
thf(1277,plain,
! [A: $i] :
( ( ( A @ ( A @ addition ) )
!= ( one @ star @ ( one @ star @ addition ) ) )
| ( ( A @ ( one @ addition ) )
= ( one @ star ) ) ),
inference(paramod_ordered,[status(thm)],[25,1250]) ).
thf(1278,plain,
( ( one @ star @ ( one @ addition ) )
= ( one @ star ) ),
inference(pattern_uni,[status(thm)],[1277:[bind(A,$thf( one @ star ))]]) ).
thf(1375,plain,
! [C: $i,B: $i,A: $i] :
( ( ( one @ star @ ( one @ addition ) )
!= ( B @ ( C @ addition ) ) )
| ( ( A @ ( one @ star @ addition ) )
= ( A @ ( B @ addition ) @ ( C @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[1278,22]) ).
thf(1376,plain,
! [A: $i] :
( ( A @ ( one @ star @ addition ) @ ( one @ addition ) )
= ( A @ ( one @ star @ addition ) ) ),
inference(pattern_uni,[status(thm)],[1375:[bind(A,$thf( A )),bind(B,$thf( one @ star )),bind(C,$thf( one ))]]) ).
thf(9961,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( one @ star @ addition ) @ ( one @ addition ) )
!= ( B @ ( C @ addition ) ) )
| ( ( A @ ( one @ star @ addition ) @ ( a @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[1376,9899]) ).
thf(9962,plain,
! [A: $i] :
( ( A @ ( one @ star @ addition ) @ ( a @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[9961:[bind(A,$thf( E )),bind(B,$thf( E @ ( one @ star @ addition ) )),bind(C,$thf( one ))]]) ).
thf(10040,plain,
! [A: $i] :
( ( A @ ( one @ star @ addition ) @ ( a @ addition ) )
!= zero ),
inference(simp,[status(thm)],[9962]) ).
thf(10216,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ addition ) @ ( B @ addition ) )
!= ( D @ ( one @ star @ addition ) @ ( a @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[225,10040]) ).
thf(10217,plain,
! [A: $i] :
( ( one @ star @ ( a @ addition ) @ ( A @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[10216:[bind(A,$thf( A )),bind(B,$thf( a )),bind(C,$thf( one @ star )),bind(D,$thf( A ))]]) ).
thf(10654,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ addition ) @ ( B @ addition ) )
!= ( one @ star @ ( a @ addition ) @ ( D @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[225,10217]) ).
thf(10655,plain,
! [A: $i] :
( ( a @ ( A @ addition ) @ ( one @ star @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[10654:[bind(A,$thf( one @ star )),bind(B,$thf( B )),bind(C,$thf( a )),bind(D,$thf( B ))]]) ).
thf(10747,plain,
! [A: $i] :
( ( a @ ( A @ addition ) @ ( one @ star @ addition ) )
!= zero ),
inference(simp,[status(thm)],[10655]) ).
thf(11,axiom,
! [A: $i] :
( ( A @ ( one @ multiplication ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_left_identity) ).
thf(43,plain,
! [A: $i] :
( ( A @ ( one @ multiplication ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(44,plain,
! [A: $i] :
( ( A @ ( one @ multiplication ) )
= A ),
inference(cnf,[status(esa)],[43]) ).
thf(45,plain,
! [A: $i] :
( ( A @ ( one @ multiplication ) )
= A ),
inference(lifteq,[status(thm)],[44]) ).
thf(86,plain,
! [B: $i,A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( B @ ( zero @ multiplication ) ) )
| ( A = zero ) ),
inference(paramod_ordered,[status(thm)],[45,34]) ).
thf(89,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( one != zero )
| ( A = zero ) ),
inference(simp,[status(thm)],[86]) ).
thf(92,plain,
! [A: $i] :
( ( one != zero )
| ( A = zero ) ),
inference(simp,[status(thm)],[89]) ).
thf(121,plain,
! [A: $i] :
( ( A
!= ( a @ ( a @ multiplication ) ) )
| ~ ( a @ star @ ( zero @ leq ) )
| ( one != zero ) ),
inference(paramod_ordered,[status(thm)],[92,19]) ).
thf(122,plain,
( ~ ( a @ star @ ( zero @ leq ) )
| ( one != zero ) ),
inference(pattern_uni,[status(thm)],[121:[bind(A,$thf( a @ ( a @ multiplication ) ))]]) ).
thf(268,plain,
! [A: $i] :
( ( A
!= ( a @ star ) )
| ~ ( zero @ ( zero @ leq ) )
| ( one != zero )
| ( one != zero ) ),
inference(paramod_ordered,[status(thm)],[92,122]) ).
thf(269,plain,
! [A: $i] :
( ( A
!= ( a @ star ) )
| ~ ( zero @ ( zero @ leq ) )
| ( one != zero ) ),
inference(simp,[status(thm)],[268]) ).
thf(270,plain,
( ~ ( zero @ ( zero @ leq ) )
| ( one != zero ) ),
inference(pattern_uni,[status(thm)],[269:[bind(A,$thf( a @ star ))]]) ).
thf(285,plain,
! [A: $i] :
( ( zero != zero )
| ~ ( A @ ( zero @ leq ) )
| ( one != zero )
| ( one != zero ) ),
inference(paramod_ordered,[status(thm)],[92,270]) ).
thf(286,plain,
! [A: $i] :
( ( zero != zero )
| ~ ( A @ ( zero @ leq ) )
| ( one != zero ) ),
inference(simp,[status(thm)],[285]) ).
thf(287,plain,
! [A: $i] :
( ~ ( A @ ( zero @ leq ) )
| ( one != zero ) ),
inference(pattern_uni,[status(thm)],[286:[]]) ).
thf(516,plain,
! [A: $i] :
( ( ( zero @ star @ ( one @ leq ) )
!= ( A @ ( zero @ leq ) ) )
| ~ $true
| ( one != zero ) ),
inference(paramod_ordered,[status(thm)],[499,287]) ).
thf(517,plain,
! [A: $i] :
( ( ( zero @ star @ ( one @ leq ) )
!= ( A @ ( zero @ leq ) ) )
| ( one != zero ) ),
inference(simp,[status(thm)],[516]) ).
thf(527,plain,
! [A: $i] :
( ( ( zero @ star )
!= A )
| ( one != zero )
| ( one != zero ) ),
inference(simp,[status(thm)],[517]) ).
thf(538,plain,
one != zero,
inference(simp,[status(thm)],[527]) ).
thf(7498,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= ( C @ ( a @ addition ) ) )
| ( ( B @ ( A @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[31,7440]) ).
thf(7499,plain,
! [A: $i] :
( ( a @ ( A @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[7498:[bind(A,$thf( A )),bind(B,$thf( a )),bind(C,$thf( A ))]]) ).
thf(1438,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ addition ) )
!= ( C @ ( B @ addition ) ) )
| ( C @ ( B @ leq ) )
| ( A != C ) ),
inference(paramod_ordered,[status(thm)],[202,68]) ).
thf(1439,plain,
! [A: $i] :
( ( A @ ( zero @ leq ) )
| ( A != A ) ),
inference(pattern_uni,[status(thm)],[1438:[bind(A,$thf( A )),bind(B,$thf( zero )),bind(C,$thf( A ))]]) ).
thf(1471,plain,
! [A: $i] : ( A @ ( zero @ leq ) ),
inference(simp,[status(thm)],[1439]) ).
thf(1639,plain,
! [A: $i] :
( ( ( A @ ( zero @ leq ) )
!= ( a @ star @ ( a @ ( a @ multiplication ) @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1471,19]) ).
thf(1640,plain,
! [A: $i] :
( ( A @ ( zero @ leq ) )
!= ( a @ star @ ( a @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[1639]) ).
thf(1646,plain,
! [A: $i] :
( ( A
!= ( a @ star ) )
| ( ( a @ ( a @ multiplication ) )
!= zero ) ),
inference(simp,[status(thm)],[1640]) ).
thf(1650,plain,
( ( a @ ( a @ multiplication ) )
!= zero ),
inference(simp,[status(thm)],[1646]) ).
thf(1133,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ star @ ( one @ addition ) )
!= ( B @ ( C @ addition ) ) )
| ( ( A @ ( zero @ star @ addition ) )
= ( A @ ( B @ addition ) @ ( C @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[1071,22]) ).
thf(1134,plain,
! [A: $i] :
( ( A @ ( zero @ star @ addition ) @ ( one @ addition ) )
= ( A @ ( zero @ star @ addition ) ) ),
inference(pattern_uni,[status(thm)],[1133:[bind(A,$thf( A )),bind(B,$thf( zero @ star )),bind(C,$thf( one ))]]) ).
thf(2034,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ star @ addition ) @ ( one @ addition ) )
!= ( C @ ( B @ addition ) ) )
| ( C @ ( B @ leq ) )
| ( ( A @ ( zero @ star @ addition ) )
!= C ) ),
inference(paramod_ordered,[status(thm)],[1134,68]) ).
thf(2035,plain,
! [A: $i] :
( ( A @ ( zero @ star @ addition ) @ ( one @ leq ) )
| ( ( A @ ( zero @ star @ addition ) )
!= ( A @ ( zero @ star @ addition ) ) ) ),
inference(pattern_uni,[status(thm)],[2034:[bind(A,$thf( E )),bind(B,$thf( one )),bind(C,$thf( E @ ( zero @ star @ addition ) ))]]) ).
thf(2101,plain,
! [A: $i] : ( A @ ( zero @ star @ addition ) @ ( one @ leq ) ),
inference(simp,[status(thm)],[2035]) ).
thf(2181,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= ( C @ ( zero @ star @ addition ) ) )
| ( B @ ( A @ addition ) @ ( one @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[31,2101]) ).
thf(2182,plain,
! [A: $i] : ( zero @ star @ ( A @ addition ) @ ( one @ leq ) ),
inference(pattern_uni,[status(thm)],[2181:[bind(A,$thf( A )),bind(B,$thf( zero @ star )),bind(C,$thf( A ))]]) ).
thf(2222,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( zero @ star @ ( D @ addition ) ) )
| ( A @ ( B @ addition ) @ ( C @ addition ) @ ( one @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[22,2182]) ).
thf(2223,plain,
! [B: $i,A: $i] : ( zero @ star @ ( B @ addition ) @ ( A @ addition ) @ ( one @ leq ) ),
inference(pattern_uni,[status(thm)],[2222:[bind(A,$thf( zero @ star )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ addition ) ))]]) ).
thf(2268,plain,
! [B: $i,A: $i] : ( zero @ star @ ( B @ addition ) @ ( A @ addition ) @ ( one @ leq ) ),
inference(simp,[status(thm)],[2223]) ).
thf(2326,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( zero @ star @ ( D @ addition ) ) )
| ( A @ ( B @ addition ) @ ( C @ addition ) @ ( one @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[31,2268]) ).
thf(2327,plain,
! [B: $i,A: $i] : ( A @ ( zero @ star @ addition ) @ ( B @ addition ) @ ( one @ leq ) ),
inference(pattern_uni,[status(thm)],[2326:[bind(A,$thf( A )),bind(B,$thf( zero @ star )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(2362,plain,
! [B: $i,A: $i] : ( A @ ( zero @ star @ addition ) @ ( B @ addition ) @ ( one @ leq ) ),
inference(simp,[status(thm)],[2327]) ).
thf(2443,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( C @ ( zero @ star @ addition ) @ ( D @ addition ) ) )
| ( A @ ( B @ addition ) @ ( one @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[31,2362]) ).
thf(2444,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( zero @ star @ addition ) @ addition ) @ ( one @ leq ) ),
inference(pattern_uni,[status(thm)],[2443:[bind(A,$thf( A )),bind(B,$thf( F @ ( zero @ star @ addition ) )),bind(C,$thf( F )),bind(D,$thf( A ))]]) ).
thf(2477,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( zero @ star @ addition ) @ addition ) @ ( one @ leq ) ),
inference(simp,[status(thm)],[2444]) ).
thf(2516,plain,
! [B: $i,A: $i] : ( A @ ( B @ addition ) @ ( zero @ star @ addition ) @ ( one @ leq ) ),
inference(rewrite,[status(thm)],[2477,22]) ).
thf(1364,plain,
one @ star @ ( one @ star @ leq ),
inference(rewrite,[status(thm)],[454,1278]) ).
thf(1520,plain,
( ( ( a @ star @ ( a @ ( a @ multiplication ) @ leq ) )
!= ( one @ star @ ( one @ star @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1364,19]) ).
thf(1521,plain,
( ( a @ star @ ( a @ ( a @ multiplication ) @ leq ) )
!= ( one @ star @ ( one @ star @ leq ) ) ),
inference(simp,[status(thm)],[1520]) ).
thf(1529,plain,
( ( ( one @ star )
!= ( a @ star ) )
| ( ( a @ ( a @ multiplication ) )
!= ( one @ star ) ) ),
inference(simp,[status(thm)],[1521]) ).
thf(10105,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= ( C @ ( zero @ star @ addition ) ) )
| ( ( B @ ( A @ addition ) @ ( a @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[31,10017]) ).
thf(10106,plain,
! [A: $i] :
( ( zero @ star @ ( A @ addition ) @ ( a @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[10105:[bind(A,$thf( A )),bind(B,$thf( zero @ star )),bind(C,$thf( A ))]]) ).
thf(10509,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ addition ) @ ( B @ addition ) )
!= ( zero @ star @ ( D @ addition ) @ ( a @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[225,10106]) ).
thf(10510,plain,
! [A: $i] :
( ( A @ ( a @ addition ) @ ( zero @ star @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[10509:[bind(A,$thf( zero @ star )),bind(B,$thf( a )),bind(C,$thf( C )),bind(D,$thf( C ))]]) ).
thf(10599,plain,
! [A: $i] :
( ( A @ ( a @ addition ) @ ( zero @ star @ addition ) )
!= zero ),
inference(simp,[status(thm)],[10510]) ).
thf(1456,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( one @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( B @ ( A @ leq ) )
| ( ( one @ star )
!= B ) ),
inference(paramod_ordered,[status(thm)],[1278,68]) ).
thf(1457,plain,
( ( one @ star @ ( one @ leq ) )
| ( ( one @ star )
!= ( one @ star ) ) ),
inference(pattern_uni,[status(thm)],[1456:[bind(A,$thf( one )),bind(B,$thf( one @ star ))]]) ).
thf(1470,plain,
one @ star @ ( one @ leq ),
inference(simp,[status(thm)],[1457]) ).
thf(9,axiom,
! [A: $i,B: $i,C: $i] :
( ( A @ ( C @ ( B @ ( A @ multiplication ) @ addition ) @ leq ) )
=> ( A @ ( B @ star @ ( C @ multiplication ) @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',star_induction_right) ).
thf(38,plain,
! [A: $i,B: $i,C: $i] :
( ( A @ ( C @ ( B @ ( A @ multiplication ) @ addition ) @ leq ) )
=> ( A @ ( B @ star @ ( C @ multiplication ) @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(39,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ star @ ( C @ multiplication ) @ leq ) )
| ~ ( A @ ( C @ ( B @ ( A @ multiplication ) @ addition ) @ leq ) ) ),
inference(cnf,[status(esa)],[38]) ).
thf(395,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ multiplication ) )
!= ( C @ ( B @ multiplication ) ) )
| ( B @ ( C @ star @ ( D @ multiplication ) @ leq ) )
| ~ ( B @ ( D @ ( zero @ addition ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[53,39]) ).
thf(396,plain,
! [B: $i,A: $i] :
( ( A @ ( zero @ star @ ( B @ multiplication ) @ leq ) )
| ~ ( A @ ( B @ ( zero @ addition ) @ leq ) ) ),
inference(pattern_uni,[status(thm)],[395:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( zero ))]]) ).
thf(417,plain,
! [B: $i,A: $i] :
( ( A @ ( zero @ star @ ( B @ multiplication ) @ leq ) )
| ~ ( A @ ( B @ ( zero @ addition ) @ leq ) ) ),
inference(simp,[status(thm)],[396]) ).
thf(11250,plain,
! [B: $i,A: $i] :
( ( A @ ( zero @ star @ ( B @ multiplication ) @ leq ) )
| ~ ( A @ ( B @ leq ) ) ),
inference(rewrite,[status(thm)],[417,202]) ).
thf(11269,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( one @ leq ) )
!= ( A @ ( B @ leq ) ) )
| ( A @ ( zero @ star @ ( B @ multiplication ) @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1470,11250]) ).
thf(11270,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( one @ leq ) )
!= ( A @ ( B @ leq ) ) )
| ( A @ ( zero @ star @ ( B @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[11269]) ).
thf(11271,plain,
one @ star @ ( zero @ star @ ( one @ multiplication ) @ leq ),
inference(pattern_uni,[status(thm)],[11270:[bind(A,$thf( one @ star )),bind(B,$thf( one ))]]) ).
thf(11366,plain,
one @ star @ ( zero @ star @ leq ),
inference(rewrite,[status(thm)],[11271,45]) ).
thf(11380,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( zero @ star @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[11366,66]) ).
thf(11381,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( zero @ star @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( ( B @ ( A @ addition ) )
= B ) ),
inference(simp,[status(thm)],[11380]) ).
thf(11382,plain,
( ( one @ star @ ( zero @ star @ addition ) )
= ( one @ star ) ),
inference(pattern_uni,[status(thm)],[11381:[bind(A,$thf( zero @ star )),bind(B,$thf( one @ star ))]]) ).
thf(404,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ multiplication ) )
!= ( C @ ( B @ multiplication ) ) )
| ( B @ ( C @ star @ ( D @ multiplication ) @ leq ) )
| ~ ( B @ ( D @ ( zero @ addition ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[34,39]) ).
thf(405,plain,
! [B: $i,A: $i] :
( ( zero @ ( A @ star @ ( B @ multiplication ) @ leq ) )
| ~ ( zero @ ( B @ ( zero @ addition ) @ leq ) ) ),
inference(pattern_uni,[status(thm)],[404:[bind(A,$thf( A )),bind(B,$thf( zero )),bind(C,$thf( A ))]]) ).
thf(421,plain,
! [B: $i,A: $i] :
( ( zero @ ( A @ star @ ( B @ multiplication ) @ leq ) )
| ~ ( zero @ ( B @ ( zero @ addition ) @ leq ) ) ),
inference(simp,[status(thm)],[405]) ).
thf(13732,plain,
! [B: $i,A: $i] :
( ( zero @ ( A @ star @ ( B @ multiplication ) @ leq ) )
| ~ ( zero @ ( B @ leq ) ) ),
inference(rewrite,[status(thm)],[421,202]) ).
thf(10250,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= ( C @ ( one @ star @ addition ) ) )
| ( ( B @ ( A @ addition ) @ ( a @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[31,10040]) ).
thf(10251,plain,
! [A: $i] :
( ( one @ star @ ( A @ addition ) @ ( a @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[10250:[bind(A,$thf( A )),bind(B,$thf( one @ star )),bind(C,$thf( A ))]]) ).
thf(6719,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( C @ ( a @ ( a @ multiplication ) @ addition ) ) )
| ( B != zero )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[66,6608]) ).
thf(6720,plain,
! [A: $i] :
( ( A != zero )
| ~ ( A @ ( a @ ( a @ multiplication ) @ leq ) ) ),
inference(pattern_uni,[status(thm)],[6719:[bind(A,$thf( a @ ( a @ multiplication ) )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(6749,plain,
~ ( zero @ ( a @ ( a @ multiplication ) @ leq ) ),
inference(simp,[status(thm)],[6720]) ).
thf(57,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( A @ star @ multiplication ) @ leq ) )
| ~ ( B @ ( C @ ( B @ ( A @ multiplication ) @ addition ) @ leq ) ) ),
inference(cnf,[status(esa)],[56]) ).
thf(6723,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= ( C @ ( a @ ( a @ multiplication ) @ addition ) ) )
| ( ( B @ ( A @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[31,6608]) ).
thf(6724,plain,
! [A: $i] :
( ( a @ ( a @ multiplication ) @ ( A @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[6723:[bind(A,$thf( A )),bind(B,$thf( a @ ( a @ multiplication ) )),bind(C,$thf( A ))]]) ).
thf(6847,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ multiplication ) @ ( C @ ( A @ multiplication ) @ addition ) )
!= ( a @ ( a @ multiplication ) @ ( D @ addition ) ) )
| ( ( C @ ( B @ ( A @ addition ) @ multiplication ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[42,6724]) ).
thf(6848,plain,
! [A: $i] :
( ( a @ ( a @ ( A @ addition ) @ multiplication ) )
!= zero ),
inference(pattern_uni,[status(thm)],[6847:[bind(A,$thf( E )),bind(B,$thf( a )),bind(C,$thf( a )),bind(D,$thf( a @ ( E @ multiplication ) ))]]) ).
thf(6905,plain,
! [A: $i] :
( ( a @ ( a @ ( A @ addition ) @ multiplication ) )
!= zero ),
inference(simp,[status(thm)],[6848]) ).
thf(10069,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ addition ) @ ( B @ addition ) )
!= ( D @ ( zero @ star @ addition ) @ ( a @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[225,10017]) ).
thf(10070,plain,
! [A: $i] :
( ( zero @ star @ ( a @ addition ) @ ( A @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[10069:[bind(A,$thf( A )),bind(B,$thf( a )),bind(C,$thf( zero @ star )),bind(D,$thf( A ))]]) ).
thf(7481,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ addition ) @ ( A @ addition ) )
!= ( D @ ( a @ addition ) ) )
| ( ( A @ ( C @ addition ) @ ( B @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[225,7440]) ).
thf(7482,plain,
! [B: $i,A: $i] :
( ( a @ ( B @ addition ) @ ( A @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[7481:[bind(A,$thf( a )),bind(B,$thf( E )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ addition ) ))]]) ).
thf(7546,plain,
! [B: $i,A: $i] :
( ( a @ ( B @ addition ) @ ( A @ addition ) )
!= zero ),
inference(simp,[status(thm)],[7482]) ).
thf(8900,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( one @ star @ addition ) @ ( one @ addition ) )
!= ( a @ ( C @ addition ) @ ( B @ addition ) ) )
| ( ( A @ ( one @ star @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[1376,7546]) ).
thf(8901,plain,
( ( a @ ( one @ star @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[8900:[bind(A,$thf( a )),bind(B,$thf( one )),bind(C,$thf( one @ star ))]]) ).
thf(9037,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( a @ ( one @ star @ addition ) ) )
| ( ( A @ ( B @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[31,8901]) ).
thf(9038,plain,
( ( one @ star @ ( a @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[9037:[bind(A,$thf( one @ star )),bind(B,$thf( a ))]]) ).
thf(9186,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( one @ star @ ( a @ addition ) ) )
| ( B != zero )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[66,9038]) ).
thf(9187,plain,
( ( ( one @ star )
!= zero )
| ~ ( one @ star @ ( a @ leq ) ) ),
inference(pattern_uni,[status(thm)],[9186:[bind(A,$thf( a )),bind(B,$thf( one @ star ))]]) ).
thf(2162,plain,
! [A: $i] :
( ( ( A @ ( zero @ star @ addition ) @ ( one @ leq ) )
!= ( a @ star @ ( a @ ( a @ multiplication ) @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2101,19]) ).
thf(2163,plain,
! [A: $i] :
( ( A @ ( zero @ star @ addition ) @ ( one @ leq ) )
!= ( a @ star @ ( a @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[2162]) ).
thf(2183,plain,
! [A: $i] :
( ( ( A @ ( zero @ star @ addition ) )
!= ( a @ star ) )
| ( ( a @ ( a @ multiplication ) )
!= one ) ),
inference(simp,[status(thm)],[2163]) ).
thf(4834,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( C @ ( zero @ star @ addition ) ) )
| ( B
!= ( a @ star ) )
| ( ( a @ ( a @ multiplication ) )
!= one )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[66,2183]) ).
thf(4835,plain,
! [A: $i] :
( ( A
!= ( a @ star ) )
| ( ( a @ ( a @ multiplication ) )
!= one )
| ~ ( A @ ( zero @ star @ leq ) ) ),
inference(pattern_uni,[status(thm)],[4834:[bind(A,$thf( zero @ star )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(4888,plain,
( ( ( a @ ( a @ multiplication ) )
!= one )
| ~ ( a @ star @ ( zero @ star @ leq ) ) ),
inference(simp,[status(thm)],[4835]) ).
thf(11369,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( zero @ star @ leq ) )
!= ( A @ ( B @ leq ) ) )
| ( A @ ( zero @ star @ ( B @ multiplication ) @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11366,11250]) ).
thf(11370,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( zero @ star @ leq ) )
!= ( A @ ( B @ leq ) ) )
| ( A @ ( zero @ star @ ( B @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[11369]) ).
thf(11371,plain,
one @ star @ ( zero @ star @ ( zero @ star @ multiplication ) @ leq ),
inference(pattern_uni,[status(thm)],[11370:[bind(A,$thf( one @ star )),bind(B,$thf( zero @ star ))]]) ).
thf(12331,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( zero @ star @ ( zero @ star @ multiplication ) @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[11371,66]) ).
thf(12332,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( zero @ star @ ( zero @ star @ multiplication ) @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( ( B @ ( A @ addition ) )
= B ) ),
inference(simp,[status(thm)],[12331]) ).
thf(12333,plain,
( ( one @ star @ ( zero @ star @ ( zero @ star @ multiplication ) @ addition ) )
= ( one @ star ) ),
inference(pattern_uni,[status(thm)],[12332:[bind(A,$thf( zero @ star @ ( zero @ star @ multiplication ) )),bind(B,$thf( one @ star ))]]) ).
thf(5786,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ multiplication ) @ ( C @ ( A @ multiplication ) @ addition ) )
!= ( a @ ( a @ multiplication ) @ ( D @ addition ) ) )
| ( ( C @ ( B @ ( A @ addition ) @ multiplication ) )
!= ( a @ star ) ) ),
inference(paramod_ordered,[status(thm)],[42,5699]) ).
thf(5787,plain,
! [A: $i] :
( ( a @ ( a @ ( A @ addition ) @ multiplication ) )
!= ( a @ star ) ),
inference(pattern_uni,[status(thm)],[5786:[bind(A,$thf( E )),bind(B,$thf( a )),bind(C,$thf( a )),bind(D,$thf( a @ ( E @ multiplication ) ))]]) ).
thf(5875,plain,
! [A: $i] :
( ( a @ ( a @ ( A @ addition ) @ multiplication ) )
!= ( a @ star ) ),
inference(simp,[status(thm)],[5787]) ).
thf(7479,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ addition ) @ ( B @ addition ) )
!= ( D @ ( a @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[225,7440]) ).
thf(7480,plain,
! [B: $i,A: $i] :
( ( A @ ( a @ addition ) @ ( B @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[7479:[bind(A,$thf( F )),bind(B,$thf( a )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ addition ) ))]]) ).
thf(7545,plain,
! [B: $i,A: $i] :
( ( A @ ( a @ addition ) @ ( B @ addition ) )
!= zero ),
inference(simp,[status(thm)],[7480]) ).
thf(5678,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ multiplication ) @ ( B @ ( A @ multiplication ) @ addition ) )
!= ( D @ ( a @ ( a @ multiplication ) @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ multiplication ) )
!= ( a @ star ) ) ),
inference(paramod_ordered,[status(thm)],[60,5642]) ).
thf(5679,plain,
! [A: $i] :
( ( A @ ( a @ addition ) @ ( a @ multiplication ) )
!= ( a @ star ) ),
inference(pattern_uni,[status(thm)],[5678:[bind(A,$thf( a )),bind(B,$thf( a )),bind(C,$thf( F )),bind(D,$thf( F @ ( a @ multiplication ) ))]]) ).
thf(5769,plain,
! [A: $i] :
( ( A @ ( a @ addition ) @ ( a @ multiplication ) )
!= ( a @ star ) ),
inference(simp,[status(thm)],[5679]) ).
thf(8907,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ star @ addition ) @ ( one @ addition ) )
!= ( a @ ( C @ addition ) @ ( B @ addition ) ) )
| ( ( A @ ( zero @ star @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[1134,7546]) ).
thf(8908,plain,
( ( a @ ( zero @ star @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[8907:[bind(A,$thf( a )),bind(B,$thf( one )),bind(C,$thf( zero @ star ))]]) ).
thf(9112,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( a @ ( zero @ star @ addition ) ) )
| ( ( A @ ( B @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[31,8908]) ).
thf(9113,plain,
( ( zero @ star @ ( a @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[9112:[bind(A,$thf( zero @ star )),bind(B,$thf( a ))]]) ).
thf(1396,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( one @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= ( one @ star ) ) ),
inference(paramod_ordered,[status(thm)],[1278,31]) ).
thf(1397,plain,
( ( one @ ( one @ star @ addition ) )
= ( one @ star ) ),
inference(pattern_uni,[status(thm)],[1396:[bind(A,$thf( one )),bind(B,$thf( one @ star ))]]) ).
thf(184,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ addition ) )
!= ( B @ ( C @ ( D @ addition ) @ addition ) ) )
| ( A
= ( B @ ( C @ addition ) @ ( D @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,22]) ).
thf(185,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) @ ( B @ addition ) @ ( A @ addition ) )
= ( B @ ( A @ addition ) ) ),
inference(pattern_uni,[status(thm)],[184:[bind(A,$thf( H @ ( G @ addition ) )),bind(B,$thf( H @ ( G @ addition ) )),bind(C,$thf( H )),bind(D,$thf( G ))]]) ).
thf(191,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) @ ( B @ addition ) @ ( A @ addition ) )
= ( B @ ( A @ addition ) ) ),
inference(simp,[status(thm)],[185]) ).
thf(3541,plain,
! [B: $i,A: $i] :
( ( ( one @ ( zero @ star @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( zero @ star @ ( B @ addition ) @ ( A @ addition ) )
= ( B @ ( A @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[1150,191]) ).
thf(3542,plain,
( ( zero @ star @ ( one @ addition ) @ ( zero @ star @ addition ) )
= ( one @ ( zero @ star @ addition ) ) ),
inference(pattern_uni,[status(thm)],[3541:[bind(A,$thf( zero @ star )),bind(B,$thf( one ))]]) ).
thf(3937,plain,
( ( zero @ star @ ( zero @ star @ addition ) )
= ( zero @ star ) ),
inference(rewrite,[status(thm)],[3542,1197,1150]) ).
thf(4805,plain,
! [B: $i,A: $i] :
( ( ( A @ ( zero @ addition ) )
!= ( B @ ( zero @ star @ addition ) ) )
| ( A
!= ( a @ star ) )
| ( ( a @ ( a @ multiplication ) )
!= one ) ),
inference(paramod_ordered,[status(thm)],[202,2183]) ).
thf(4856,plain,
! [A: $i] :
( ( A
!= ( a @ star ) )
| ( ( zero @ star )
!= zero )
| ( ( a @ ( a @ multiplication ) )
!= one ) ),
inference(simp,[status(thm)],[4805]) ).
thf(4902,plain,
( ( ( zero @ star )
!= zero )
| ( ( a @ ( a @ multiplication ) )
!= one ) ),
inference(simp,[status(thm)],[4856]) ).
thf(3209,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( one @ star @ addition ) @ ( one @ addition ) )
!= ( C @ ( B @ addition ) ) )
| ( C @ ( B @ leq ) )
| ( ( A @ ( one @ star @ addition ) )
!= C ) ),
inference(paramod_ordered,[status(thm)],[1376,68]) ).
thf(3210,plain,
! [A: $i] :
( ( A @ ( one @ star @ addition ) @ ( one @ leq ) )
| ( ( A @ ( one @ star @ addition ) )
!= ( A @ ( one @ star @ addition ) ) ) ),
inference(pattern_uni,[status(thm)],[3209:[bind(A,$thf( E )),bind(B,$thf( one )),bind(C,$thf( E @ ( one @ star @ addition ) ))]]) ).
thf(3262,plain,
! [A: $i] : ( A @ ( one @ star @ addition ) @ ( one @ leq ) ),
inference(simp,[status(thm)],[3210]) ).
thf(15,axiom,
! [A: $i] : ( A @ star @ ( A @ star @ ( A @ multiplication ) @ ( one @ addition ) @ leq ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',star_unfold_right) ).
thf(54,plain,
! [A: $i] : ( A @ star @ ( A @ star @ ( A @ multiplication ) @ ( one @ addition ) @ leq ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(7483,plain,
! [A: $i] :
( ( ( one @ ( zero @ star @ addition ) )
!= ( A @ ( a @ addition ) ) )
| ( ( zero @ star )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[1150,7440]) ).
thf(7512,plain,
! [A: $i] :
( ( one != A )
| ( ( zero @ star )
!= a )
| ( ( zero @ star )
!= zero ) ),
inference(simp,[status(thm)],[7483]) ).
thf(7534,plain,
( ( ( zero @ star )
!= a )
| ( ( zero @ star )
!= zero ) ),
inference(simp,[status(thm)],[7512]) ).
thf(69,plain,
! [A: $i] :
( ( ( A @ ( zero @ multiplication ) )
!= ( a @ ( a @ multiplication ) ) )
| ~ ( a @ star @ ( zero @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[34,19]) ).
thf(70,plain,
! [A: $i] :
( ( A != a )
| ( zero != a )
| ~ ( a @ star @ ( zero @ leq ) ) ),
inference(simp,[status(thm)],[69]) ).
thf(71,plain,
( ( zero != a )
| ~ ( a @ star @ ( zero @ leq ) ) ),
inference(simp,[status(thm)],[70]) ).
thf(1634,plain,
( ( zero != a )
| ~ $true ),
inference(rewrite,[status(thm)],[71,1471]) ).
thf(1635,plain,
zero != a,
inference(simp,[status(thm)],[1634]) ).
thf(150,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( E @ ( F @ addition ) ) )
| ( ( D @ ( A @ ( B @ addition ) @ ( C @ addition ) @ addition ) )
= ( D @ ( E @ addition ) @ ( F @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,22]) ).
thf(151,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ addition ) @ ( C @ addition ) @ addition ) )
= ( B @ ( A @ addition ) @ ( D @ ( C @ addition ) @ addition ) ) ),
inference(pattern_uni,[status(thm)],[150:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( G )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( H @ ( G @ addition ) ))]]) ).
thf(154,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ addition ) @ ( C @ addition ) @ addition ) )
= ( B @ ( A @ addition ) @ ( D @ ( C @ addition ) @ addition ) ) ),
inference(simp,[status(thm)],[151]) ).
thf(2642,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ addition ) @ addition ) @ ( C @ addition ) )
= ( B @ ( A @ addition ) @ ( D @ addition ) @ ( C @ addition ) ) ),
inference(rewrite,[status(thm)],[154,22]) ).
thf(400,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( E @ ( D @ multiplication ) ) )
| ( D @ ( E @ star @ ( F @ multiplication ) @ leq ) )
| ~ ( D @ ( F @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ addition ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[37,39]) ).
thf(401,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ multiplication ) @ ( A @ star @ ( B @ multiplication ) @ leq ) )
| ~ ( D @ ( C @ multiplication ) @ ( B @ ( A @ ( D @ multiplication ) @ ( C @ multiplication ) @ addition ) @ leq ) ) ),
inference(pattern_uni,[status(thm)],[400:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ multiplication ) )),bind(E,$thf( C ))]]) ).
thf(419,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ multiplication ) @ ( A @ star @ ( B @ multiplication ) @ leq ) )
| ~ ( D @ ( C @ multiplication ) @ ( B @ ( A @ ( D @ multiplication ) @ ( C @ multiplication ) @ addition ) @ leq ) ) ),
inference(simp,[status(thm)],[401]) ).
thf(1452,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ addition ) )
!= ( C @ ( B @ addition ) ) )
| ( C @ ( B @ leq ) )
| ( A != C ) ),
inference(paramod_ordered,[status(thm)],[25,68]) ).
thf(1453,plain,
! [A: $i] :
( ( A @ ( A @ leq ) )
| ( A != A ) ),
inference(pattern_uni,[status(thm)],[1452:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(1468,plain,
! [A: $i] : ( A @ ( A @ leq ) ),
inference(simp,[status(thm)],[1453]) ).
thf(1680,plain,
! [A: $i] :
( ( ( A @ ( A @ leq ) )
!= ( a @ star @ ( a @ ( a @ multiplication ) @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1468,19]) ).
thf(1681,plain,
! [A: $i] :
( ( A @ ( A @ leq ) )
!= ( a @ star @ ( a @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[1680]) ).
thf(1687,plain,
! [A: $i] :
( ( A
!= ( a @ star ) )
| ( A
!= ( a @ ( a @ multiplication ) ) ) ),
inference(simp,[status(thm)],[1681]) ).
thf(1690,plain,
( ( a @ ( a @ multiplication ) )
!= ( a @ star ) ),
inference(simp,[status(thm)],[1687]) ).
thf(4119,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ addition ) @ ( B @ addition ) )
!= ( one @ star @ ( one @ addition ) @ ( one @ star @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
= ( one @ star ) ) ),
inference(paramod_ordered,[status(thm)],[4102,1828]) ).
thf(4120,plain,
( ( one @ star @ ( one @ star @ addition ) @ ( one @ addition ) )
= ( one @ star ) ),
inference(pattern_uni,[status(thm)],[4119:[bind(A,$thf( one )),bind(B,$thf( one @ star )),bind(C,$thf( one @ star ))]]) ).
thf(4611,plain,
( ( one @ star @ ( one @ star @ addition ) )
= ( one @ star ) ),
inference(rewrite,[status(thm)],[4120,1376]) ).
thf(7468,plain,
! [A: $i] :
( ( ( one @ star @ ( one @ star @ addition ) )
!= ( A @ ( a @ addition ) ) )
| ( ( one @ star )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[4611,7440]) ).
thf(7507,plain,
! [A: $i] :
( ( ( one @ star )
!= A )
| ( ( one @ star )
!= a )
| ( ( one @ star )
!= zero ) ),
inference(simp,[status(thm)],[7468]) ).
thf(7529,plain,
( ( ( one @ star )
!= a )
| ( ( one @ star )
!= zero ) ),
inference(simp,[status(thm)],[7507]) ).
thf(11367,plain,
( ( ( one @ star @ ( zero @ star @ leq ) )
!= ( zero @ ( a @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11366,7524]) ).
thf(11368,plain,
( ( one @ star @ ( zero @ star @ leq ) )
!= ( zero @ ( a @ leq ) ) ),
inference(simp,[status(thm)],[11367]) ).
thf(11392,plain,
( ( ( one @ star )
!= zero )
| ( ( zero @ star )
!= a ) ),
inference(simp,[status(thm)],[11368]) ).
thf(320,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( D @ ( one @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[37,45]) ).
thf(324,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C != D )
| ( ( B @ ( A @ multiplication ) )
!= one )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= D ) ),
inference(simp,[status(thm)],[320]) ).
thf(330,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= one )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= C ) ),
inference(simp,[status(thm)],[324]) ).
thf(11550,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( zero @ star @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= ( one @ star ) ) ),
inference(paramod_ordered,[status(thm)],[11382,31]) ).
thf(11551,plain,
( ( zero @ star @ ( one @ star @ addition ) )
= ( one @ star ) ),
inference(pattern_uni,[status(thm)],[11550:[bind(A,$thf( zero @ star )),bind(B,$thf( one @ star ))]]) ).
thf(3821,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= ( C @ ( one @ star @ addition ) ) )
| ( B @ ( A @ addition ) @ ( one @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[31,3262]) ).
thf(3822,plain,
! [A: $i] : ( one @ star @ ( A @ addition ) @ ( one @ leq ) ),
inference(pattern_uni,[status(thm)],[3821:[bind(A,$thf( A )),bind(B,$thf( one @ star )),bind(C,$thf( A ))]]) ).
thf(3873,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( one @ star @ ( D @ addition ) ) )
| ( A @ ( B @ addition ) @ ( C @ addition ) @ ( one @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[22,3822]) ).
thf(3874,plain,
! [B: $i,A: $i] : ( one @ star @ ( B @ addition ) @ ( A @ addition ) @ ( one @ leq ) ),
inference(pattern_uni,[status(thm)],[3873:[bind(A,$thf( one @ star )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ addition ) ))]]) ).
thf(3908,plain,
! [B: $i,A: $i] : ( one @ star @ ( B @ addition ) @ ( A @ addition ) @ ( one @ leq ) ),
inference(simp,[status(thm)],[3874]) ).
thf(11275,plain,
! [B: $i,A: $i] :
( ( ( zero @ star @ ( one @ leq ) )
!= ( A @ ( B @ leq ) ) )
| ( A @ ( zero @ star @ ( B @ multiplication ) @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[499,11250]) ).
thf(11276,plain,
! [B: $i,A: $i] :
( ( ( zero @ star @ ( one @ leq ) )
!= ( A @ ( B @ leq ) ) )
| ( A @ ( zero @ star @ ( B @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[11275]) ).
thf(11277,plain,
zero @ star @ ( zero @ star @ ( one @ multiplication ) @ leq ),
inference(pattern_uni,[status(thm)],[11276:[bind(A,$thf( zero @ star )),bind(B,$thf( one ))]]) ).
thf(11397,plain,
zero @ star @ ( zero @ star @ leq ),
inference(rewrite,[status(thm)],[11277,45]) ).
thf(11400,plain,
! [B: $i,A: $i] :
( ( ( zero @ star @ ( zero @ star @ leq ) )
!= ( A @ ( B @ leq ) ) )
| ( A @ ( zero @ star @ ( B @ multiplication ) @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11397,11250]) ).
thf(11401,plain,
! [B: $i,A: $i] :
( ( ( zero @ star @ ( zero @ star @ leq ) )
!= ( A @ ( B @ leq ) ) )
| ( A @ ( zero @ star @ ( B @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[11400]) ).
thf(11402,plain,
zero @ star @ ( zero @ star @ ( zero @ star @ multiplication ) @ leq ),
inference(pattern_uni,[status(thm)],[11401:[bind(A,$thf( zero @ star )),bind(B,$thf( zero @ star ))]]) ).
thf(9258,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( zero @ star @ ( a @ addition ) ) )
| ( B != zero )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[66,9113]) ).
thf(9259,plain,
( ( ( zero @ star )
!= zero )
| ~ ( zero @ star @ ( a @ leq ) ) ),
inference(pattern_uni,[status(thm)],[9258:[bind(A,$thf( a )),bind(B,$thf( zero @ star ))]]) ).
thf(402,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ addition ) )
!= ( D @ ( C @ ( B @ multiplication ) @ addition ) ) )
| ( B @ ( C @ star @ ( D @ multiplication ) @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[25,39]) ).
thf(403,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ star @ ( B @ ( A @ multiplication ) @ multiplication ) @ leq ) )
| ~ ( A @ ( B @ ( A @ multiplication ) @ leq ) ) ),
inference(pattern_uni,[status(thm)],[402:[bind(A,$thf( H @ ( G @ multiplication ) )),bind(B,$thf( G )),bind(C,$thf( H )),bind(D,$thf( H @ ( G @ multiplication ) ))]]) ).
thf(420,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ star @ ( B @ ( A @ multiplication ) @ multiplication ) @ leq ) )
| ~ ( A @ ( B @ ( A @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[403]) ).
thf(12954,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ star @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) )
| ~ ( A @ ( B @ ( A @ multiplication ) @ leq ) ) ),
inference(rewrite,[status(thm)],[420,37]) ).
thf(6708,plain,
! [A: $i] :
( ( ( A @ ( a @ ( a @ multiplication ) @ addition ) )
!= ( one @ star @ ( one @ addition ) ) )
| ( ( one @ star )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[1278,6608]) ).
thf(6740,plain,
! [A: $i] :
( ( A
!= ( one @ star ) )
| ( ( a @ ( a @ multiplication ) )
!= one )
| ( ( one @ star )
!= zero ) ),
inference(simp,[status(thm)],[6708]) ).
thf(6762,plain,
( ( ( a @ ( a @ multiplication ) )
!= one )
| ( ( one @ star )
!= zero ) ),
inference(simp,[status(thm)],[6740]) ).
thf(316,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( D @ ( zero @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[37,34]) ).
thf(325,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C != D )
| ( ( B @ ( A @ multiplication ) )
!= zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[316]) ).
thf(331,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[325]) ).
thf(8576,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= ( D @ ( a @ addition ) ) )
| ( ( B @ ( A @ addition ) @ ( C @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[31,7526]) ).
thf(8577,plain,
! [B: $i,A: $i] :
( ( a @ ( A @ addition ) @ ( B @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[8576:[bind(A,$thf( A )),bind(B,$thf( a )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(8625,plain,
! [B: $i,A: $i] :
( ( a @ ( A @ addition ) @ ( B @ addition ) )
!= zero ),
inference(simp,[status(thm)],[8577]) ).
thf(6703,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ multiplication ) @ ( B @ ( A @ multiplication ) @ addition ) )
!= ( D @ ( a @ ( a @ multiplication ) @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ multiplication ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[60,6608]) ).
thf(6704,plain,
! [A: $i] :
( ( A @ ( a @ addition ) @ ( a @ multiplication ) )
!= zero ),
inference(pattern_uni,[status(thm)],[6703:[bind(A,$thf( a )),bind(B,$thf( a )),bind(C,$thf( F )),bind(D,$thf( F @ ( a @ multiplication ) ))]]) ).
thf(6775,plain,
! [A: $i] :
( ( A @ ( a @ addition ) @ ( a @ multiplication ) )
!= zero ),
inference(simp,[status(thm)],[6704]) ).
thf(518,plain,
( ( ( a @ star @ ( a @ ( a @ multiplication ) @ leq ) )
!= ( zero @ star @ ( one @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[499,19]) ).
thf(519,plain,
( ( a @ star @ ( a @ ( a @ multiplication ) @ leq ) )
!= ( zero @ star @ ( one @ leq ) ) ),
inference(simp,[status(thm)],[518]) ).
thf(524,plain,
( ( ( zero @ star )
!= ( a @ star ) )
| ( ( a @ ( a @ multiplication ) )
!= one ) ),
inference(simp,[status(thm)],[519]) ).
thf(55,plain,
! [A: $i] : ( A @ star @ ( A @ star @ ( A @ multiplication ) @ ( one @ addition ) @ leq ) ),
inference(cnf,[status(esa)],[54]) ).
thf(398,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( C @ ( B @ multiplication ) ) )
| ( B @ ( C @ star @ ( D @ multiplication ) @ leq ) )
| ~ ( B @ ( D @ ( A @ addition ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[48,39]) ).
thf(399,plain,
! [B: $i,A: $i] :
( ( A @ ( one @ star @ ( B @ multiplication ) @ leq ) )
| ~ ( A @ ( B @ ( A @ addition ) @ leq ) ) ),
inference(pattern_uni,[status(thm)],[398:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( one ))]]) ).
thf(418,plain,
! [B: $i,A: $i] :
( ( A @ ( one @ star @ ( B @ multiplication ) @ leq ) )
| ~ ( A @ ( B @ ( A @ addition ) @ leq ) ) ),
inference(simp,[status(thm)],[399]) ).
thf(1497,plain,
( ( ( a @ star @ ( a @ ( a @ multiplication ) @ leq ) )
!= ( one @ star @ ( one @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1470,19]) ).
thf(1498,plain,
( ( a @ star @ ( a @ ( a @ multiplication ) @ leq ) )
!= ( one @ star @ ( one @ leq ) ) ),
inference(simp,[status(thm)],[1497]) ).
thf(1508,plain,
( ( ( one @ star )
!= ( a @ star ) )
| ( ( a @ ( a @ multiplication ) )
!= one ) ),
inference(simp,[status(thm)],[1498]) ).
thf(10512,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ addition ) @ ( A @ addition ) )
!= ( zero @ star @ ( D @ addition ) @ ( a @ addition ) ) )
| ( ( A @ ( C @ addition ) @ ( B @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[225,10106]) ).
thf(10513,plain,
! [A: $i] :
( ( a @ ( zero @ star @ addition ) @ ( A @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[10512:[bind(A,$thf( a )),bind(B,$thf( B )),bind(C,$thf( zero @ star )),bind(D,$thf( B ))]]) ).
thf(10600,plain,
! [A: $i] :
( ( a @ ( zero @ star @ addition ) @ ( A @ addition ) )
!= zero ),
inference(simp,[status(thm)],[10513]) ).
thf(246,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ addition ) )
!= ( B @ ( C @ ( D @ addition ) @ addition ) ) )
| ( A
= ( B @ ( C @ addition ) @ ( D @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[202,22]) ).
thf(259,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A != B )
| ( ( C @ ( D @ addition ) )
!= zero )
| ( A
= ( B @ ( C @ addition ) @ ( D @ addition ) ) ) ),
inference(simp,[status(thm)],[246]) ).
thf(262,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ addition ) )
!= zero )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
= A ) ),
inference(simp,[status(thm)],[259]) ).
thf(6853,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ multiplication ) @ ( B @ ( A @ multiplication ) @ addition ) )
!= ( a @ ( a @ multiplication ) @ ( D @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ multiplication ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[60,6724]) ).
thf(6854,plain,
! [A: $i] :
( ( a @ ( A @ addition ) @ ( a @ multiplication ) )
!= zero ),
inference(pattern_uni,[status(thm)],[6853:[bind(A,$thf( a )),bind(B,$thf( F )),bind(C,$thf( a )),bind(D,$thf( F @ ( a @ multiplication ) ))]]) ).
thf(6906,plain,
! [A: $i] :
( ( a @ ( A @ addition ) @ ( a @ multiplication ) )
!= zero ),
inference(simp,[status(thm)],[6854]) ).
thf(10359,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ addition ) @ ( B @ addition ) )
!= ( zero @ star @ ( a @ addition ) @ ( D @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[225,10070]) ).
thf(10360,plain,
! [A: $i] :
( ( a @ ( A @ addition ) @ ( zero @ star @ addition ) )
!= zero ),
inference(pattern_uni,[status(thm)],[10359:[bind(A,$thf( zero @ star )),bind(B,$thf( B )),bind(C,$thf( a )),bind(D,$thf( B ))]]) ).
thf(10485,plain,
! [A: $i] :
( ( a @ ( A @ addition ) @ ( zero @ star @ addition ) )
!= zero ),
inference(simp,[status(thm)],[10360]) ).
thf(313,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( a @ ( a @ multiplication ) ) )
| ~ ( a @ star @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[37,19]) ).
thf(326,plain,
! [C: $i,B: $i,A: $i] :
( ( C != a )
| ( ( B @ ( A @ multiplication ) )
!= a )
| ~ ( a @ star @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[313]) ).
thf(332,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= a )
| ~ ( a @ star @ ( a @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[326]) ).
thf(85,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( a @ ( a @ multiplication ) ) )
| ~ ( a @ star @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[45,19]) ).
thf(88,plain,
! [A: $i] :
( ( A != a )
| ( one != a )
| ~ ( a @ star @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[85]) ).
thf(91,plain,
( ( one != a )
| ~ ( a @ star @ ( a @ leq ) ) ),
inference(simp,[status(thm)],[88]) ).
thf(1501,plain,
( ( ( one @ star @ ( one @ leq ) )
!= ( a @ star @ ( a @ leq ) ) )
| ( one != a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1470,91]) ).
thf(1502,plain,
( ( ( one @ star @ ( one @ leq ) )
!= ( a @ star @ ( a @ leq ) ) )
| ( one != a ) ),
inference(simp,[status(thm)],[1501]) ).
thf(1507,plain,
( ( ( one @ star )
!= ( a @ star ) )
| ( one != a )
| ( one != a ) ),
inference(simp,[status(thm)],[1502]) ).
thf(1512,plain,
( ( ( one @ star )
!= ( a @ star ) )
| ( one != a ) ),
inference(simp,[status(thm)],[1507]) ).
thf(1536,plain,
( ( one != a )
| ( one != a ) ),
inference(simp,[status(thm)],[1512]) ).
thf(1537,plain,
one != a,
inference(simp,[status(thm)],[1536]) ).
thf(5673,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ multiplication ) @ ( C @ ( A @ multiplication ) @ addition ) )
!= ( D @ ( a @ ( a @ multiplication ) @ addition ) ) )
| ( ( C @ ( B @ ( A @ addition ) @ multiplication ) )
!= ( a @ star ) ) ),
inference(paramod_ordered,[status(thm)],[42,5642]) ).
thf(5674,plain,
! [A: $i] :
( ( a @ ( A @ ( a @ addition ) @ multiplication ) )
!= ( a @ star ) ),
inference(pattern_uni,[status(thm)],[5673:[bind(A,$thf( a )),bind(B,$thf( E )),bind(C,$thf( a )),bind(D,$thf( a @ ( E @ multiplication ) ))]]) ).
thf(5768,plain,
! [A: $i] :
( ( a @ ( A @ ( a @ addition ) @ multiplication ) )
!= ( a @ star ) ),
inference(simp,[status(thm)],[5674]) ).
thf(590,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ multiplication ) )
!= ( D @ ( B @ multiplication ) ) )
| ( ( D @ ( C @ multiplication ) @ ( zero @ addition ) )
= ( D @ ( C @ ( B @ addition ) @ multiplication ) ) ) ),
inference(paramod_ordered,[status(thm)],[53,42]) ).
thf(591,plain,
! [B: $i,A: $i] :
( ( zero @ ( B @ multiplication ) @ ( zero @ addition ) )
= ( zero @ ( B @ ( A @ addition ) @ multiplication ) ) ),
inference(pattern_uni,[status(thm)],[590:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( C )),bind(D,$thf( zero ))]]) ).
thf(625,plain,
! [B: $i,A: $i] :
( ( zero @ ( B @ multiplication ) @ ( zero @ addition ) )
= ( zero @ ( B @ ( A @ addition ) @ multiplication ) ) ),
inference(simp,[status(thm)],[591]) ).
thf(592,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ multiplication ) )
!= ( D @ ( C @ multiplication ) ) )
| ( ( zero @ ( D @ ( B @ multiplication ) @ addition ) )
= ( D @ ( C @ ( B @ addition ) @ multiplication ) ) ) ),
inference(paramod_ordered,[status(thm)],[53,42]) ).
thf(593,plain,
! [B: $i,A: $i] :
( ( zero @ ( zero @ ( B @ multiplication ) @ addition ) )
= ( zero @ ( A @ ( B @ addition ) @ multiplication ) ) ),
inference(pattern_uni,[status(thm)],[592:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( zero ))]]) ).
thf(682,plain,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
= zero ),
inference(rewrite,[status(thm)],[593,53,28]) ).
thf(697,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ multiplication ) )
!= ( D @ ( C @ ( B @ multiplication ) @ multiplication ) ) )
| ( ( D @ ( C @ multiplication ) @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[682,37]) ).
thf(698,plain,
! [B: $i,A: $i] :
( ( zero @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[697:[bind(A,$thf( F @ ( E @ multiplication ) )),bind(B,$thf( E )),bind(C,$thf( F )),bind(D,$thf( zero ))]]) ).
thf(721,plain,
! [B: $i,A: $i] :
( ( zero @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ),
inference(simp,[status(thm)],[698]) ).
thf(728,plain,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
= zero ),
inference(rewrite,[status(thm)],[721,682]) ).
thf(917,plain,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
= zero ),
inference(rewrite,[status(thm)],[625,728,202]) ).
thf(934,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ multiplication ) )
!= ( D @ ( C @ ( B @ multiplication ) @ multiplication ) ) )
| ( ( D @ ( C @ multiplication ) @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[917,37]) ).
thf(935,plain,
! [B: $i,A: $i] :
( ( zero @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[934:[bind(A,$thf( F @ ( E @ multiplication ) )),bind(B,$thf( E )),bind(C,$thf( F )),bind(D,$thf( zero ))]]) ).
thf(961,plain,
! [B: $i,A: $i] :
( ( zero @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ),
inference(simp,[status(thm)],[935]) ).
thf(972,plain,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
= zero ),
inference(rewrite,[status(thm)],[961,917]) ).
thf(24044,plain,
$false,
inference(e,[status(thm)],[9516,1828,5878,10017,202,56,7524,10747,538,42,7499,1650,2516,1529,6608,37,10599,11382,25,11250,13732,10251,6749,46,57,261,29,20,6905,10070,61,9187,10106,4888,12333,1470,60,5875,6773,11371,28,38,7545,5769,9113,1397,2268,499,225,6724,1150,3937,4902,10217,1071,1278,32,34,45,3262,191,22,7440,54,7534,1635,49,187,2642,419,39,1690,1376,7546,7529,2182,1471,11392,66,330,11551,9899,2101,3908,11402,35,7526,9259,1134,48,12954,50,6762,331,8625,31,4611,6775,43,524,4102,40,55,418,23,26,1508,10040,58,11366,5699,2362,2183,10600,262,8908,51,8901,19,6906,3822,1197,5642,10485,332,9038,1537,5768,68,3474,11397,1468,972]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KLE170+1.002 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.11/0.39 % Computer : n019.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Fri Sep 25 19:30:33 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.31/1.18 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.71/1.49 % [INFO] Parsing done (307ms).
% 1.97/1.51 % [INFO] Running in sequential loop mode.
% 3.13/2.17 % [INFO] eprover registered as external prover.
% 3.13/2.18 % [INFO] Scanning for conjecture ...
% 3.38/2.31 % [INFO] Found a conjecture (or negated_conjecture) and 16 axioms. Running axiom selection ...
% 3.55/2.40 % [INFO] Axiom selection finished. Selected 16 axioms (removed 0 axioms).
% 3.55/2.48 % [INFO] Problem is first-order (TPTP FOF).
% 3.55/2.49 % [INFO] Type checking passed.
% 3.55/2.49 % [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 ...
% 98.80/21.79 % External prover 'e' found a proof!
% 98.80/21.79 % [INFO] Killing All external provers ...
% 99.04/21.80 % Time passed: 21256ms (effective reasoning time: 20275ms)
% 99.04/21.80 % 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)>
% 99.04/21.80 % Axioms used in derivation (16): additive_identity, star_induction_right, left_annihilation, star_induction_left, right_distributivity, star_unfold_left, right_annihilation, multiplicative_left_identity, additive_idempotence, additive_associativity, multiplicative_right_identity, star_unfold_right, order, additive_commutativity, multiplicative_associativity, left_distributivity
% 99.04/21.80 % No. of inferences in proof: 400
% 99.04/21.80 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 21256 ms resp. 20275 ms w/o parsing
% 100.07/22.06 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 100.07/22.06 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------