%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : KLE169+1 : TPTP v9.3.1. Released v5.2.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 : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:43:21 AM UTC 2026
% Result : Theorem 196.98s 50.38s
% Output : Refutation 199.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 18
% Syntax : Number of formulae : 824 ( 298 unt; 0 typ; 0 def)
% Number of atoms : 1859 (1522 equ; 0 cnn)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 7930 (1256 ~; 923 |; 3 &;5739 @)
% ( 1 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 12 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 800 ( 0 ^; 800 !; 0 ?; 800 :)
% Comments :
%------------------------------------------------------------------------------
thf(leq_decl,type,
leq: $i > $i > $o ).
thf(multiplication_decl,type,
multiplication: $i > $i > $i ).
thf(a_decl,type,
a: $i ).
thf(b_decl,type,
b: $i ).
thf(star_decl,type,
star: $i > $i ).
thf(sigma_decl,type,
sigma: $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/sandbox2/benchmark/theBenchmark.p',multiplicative_associativity) ).
thf(36,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(37,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= ( C @ ( B @ ( A @ multiplication ) @ multiplication ) ) ),
inference(cnf,[status(esa)],[36]) ).
thf(38,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
= ( C @ ( B @ multiplication ) @ ( A @ multiplication ) ) ),
inference(lifteq,[status(thm)],[37]) ).
thf(7,axiom,
! [A: $i] :
( ( A @ ( zero @ multiplication ) )
= zero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_annihilation) ).
thf(33,plain,
! [A: $i] :
( ( A @ ( zero @ multiplication ) )
= zero ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(34,plain,
! [A: $i] :
( ( A @ ( zero @ multiplication ) )
= zero ),
inference(cnf,[status(esa)],[33]) ).
thf(35,plain,
! [A: $i] :
( ( A @ ( zero @ multiplication ) )
= zero ),
inference(lifteq,[status(thm)],[34]) ).
thf(546,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)],[38,35]) ).
thf(577,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)],[546]) ).
thf(592,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[577]) ).
thf(6,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ addition ) )
= ( A @ ( B @ addition ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_commutativity) ).
thf(30,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ addition ) )
= ( A @ ( B @ addition ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(31,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) )
= ( A @ ( B @ addition ) ) ),
inference(cnf,[status(esa)],[30]) ).
thf(32,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) )
= ( A @ ( B @ addition ) ) ),
inference(lifteq,[status(thm)],[31]) ).
thf(5,axiom,
! [A: $i] :
( ( zero @ ( A @ addition ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_identity) ).
thf(27,plain,
! [A: $i] :
( ( zero @ ( A @ addition ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(28,plain,
! [A: $i] :
( ( zero @ ( A @ addition ) )
= A ),
inference(cnf,[status(esa)],[27]) ).
thf(29,plain,
! [A: $i] :
( ( zero @ ( A @ addition ) )
= A ),
inference(lifteq,[status(thm)],[28]) ).
thf(287,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( zero @ ( C @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[32,29]) ).
thf(288,plain,
! [A: $i] :
( ( A @ ( zero @ addition ) )
= A ),
inference(pattern_uni,[status(thm)],[287:[bind(A,$thf( A )),bind(B,$thf( zero )),bind(C,$thf( A ))]]) ).
thf(19,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
<=> ( ( B @ ( A @ addition ) )
= B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',order) ).
thf(64,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)],[19]) ).
thf(65,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)],[64]) ).
thf(66,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)],[65]) ).
thf(68,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ( ( B @ ( A @ addition ) )
!= B ) ),
inference(cnfConj,[status(thm)],[66]) ).
thf(70,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ( ( B @ ( A @ addition ) )
!= B ) ),
inference(lifteq,[status(thm)],[68]) ).
thf(71,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ( ( B @ ( A @ addition ) )
!= B ) ),
inference(simp,[status(thm)],[70]) ).
thf(3653,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ addition ) )
!= ( C @ ( B @ addition ) ) )
| ( C @ ( B @ leq ) )
| ( A != C ) ),
inference(paramod_ordered,[status(thm)],[288,71]) ).
thf(3654,plain,
! [A: $i] :
( ( A @ ( zero @ leq ) )
| ( A != A ) ),
inference(pattern_uni,[status(thm)],[3653:[bind(A,$thf( A )),bind(B,$thf( zero )),bind(C,$thf( A ))]]) ).
thf(3779,plain,
! [A: $i] : ( A @ ( zero @ leq ) ),
inference(simp,[status(thm)],[3654]) ).
thf(1,conjecture,
a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a) ).
thf(2,negated_conjecture,
~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(20,plain,
~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(3807,plain,
! [A: $i] :
( ( ( A @ ( zero @ leq ) )
!= ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3779,20]) ).
thf(3808,plain,
! [A: $i] :
( ( A @ ( zero @ leq ) )
!= ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[3807]) ).
thf(3826,plain,
! [A: $i] :
( ( A
!= ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) ) )
| ( ( a @ ( b @ multiplication ) @ ( a @ multiplication ) )
!= zero ) ),
inference(simp,[status(thm)],[3808]) ).
thf(3836,plain,
( ( a @ ( b @ multiplication ) @ ( a @ multiplication ) )
!= zero ),
inference(simp,[status(thm)],[3826]) ).
thf(79934,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) )
| ( zero != zero )
| ( ( B @ ( A @ multiplication ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[592,3836]) ).
thf(79935,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) )
| ( ( B @ ( A @ multiplication ) )
!= zero ) ),
inference(simp,[status(thm)],[79934]) ).
thf(79936,plain,
( ( b @ ( a @ multiplication ) )
!= zero ),
inference(pattern_uni,[status(thm)],[79935:[bind(A,$thf( a )),bind(B,$thf( b )),bind(C,$thf( a ))]]) ).
thf(15,axiom,
( sigma
= ( b @ ( a @ addition ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',an) ).
thf(55,plain,
( sigma
= ( b @ ( a @ addition ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(56,plain,
( ( b @ ( a @ addition ) )
= sigma ),
inference(lifteq,[status(thm)],[55]) ).
thf(3,axiom,
! [A: $i,B: $i,C: $i] :
( ( A @ ( B @ addition ) @ ( C @ addition ) )
= ( A @ ( B @ ( C @ addition ) @ addition ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_associativity) ).
thf(21,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(22,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ addition ) @ ( C @ addition ) )
= ( A @ ( B @ ( C @ addition ) @ addition ) ) ),
inference(cnf,[status(esa)],[21]) ).
thf(23,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( C @ addition ) @ addition ) )
= ( A @ ( B @ addition ) @ ( C @ addition ) ) ),
inference(lifteq,[status(thm)],[22]) ).
thf(160,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( a @ addition ) )
!= ( B @ ( C @ addition ) ) )
| ( ( A @ ( sigma @ addition ) )
= ( A @ ( B @ addition ) @ ( C @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[56,23]) ).
thf(161,plain,
! [A: $i] :
( ( A @ ( sigma @ addition ) )
= ( A @ ( b @ addition ) @ ( a @ addition ) ) ),
inference(pattern_uni,[status(thm)],[160:[bind(A,$thf( A )),bind(B,$thf( b )),bind(C,$thf( a ))]]) ).
thf(4,axiom,
! [A: $i] :
( ( A @ ( A @ addition ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_idempotence) ).
thf(24,plain,
! [A: $i] :
( ( A @ ( A @ addition ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(25,plain,
! [A: $i] :
( ( A @ ( A @ addition ) )
= A ),
inference(cnf,[status(esa)],[24]) ).
thf(26,plain,
! [A: $i] :
( ( A @ ( A @ addition ) )
= A ),
inference(lifteq,[status(thm)],[25]) ).
thf(236,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sigma @ addition ) )
!= ( B @ ( B @ addition ) ) )
| ( ( A @ ( b @ addition ) @ ( a @ addition ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[161,26]) ).
thf(237,plain,
( ( sigma @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[236:[bind(A,$thf( sigma )),bind(B,$thf( sigma ))]]) ).
thf(384,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( b @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[237,32]) ).
thf(385,plain,
( ( a @ ( sigma @ ( b @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[384:[bind(A,$thf( a )),bind(B,$thf( sigma @ ( b @ addition ) ))]]) ).
thf(445,plain,
( ( a @ ( sigma @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[385,23]) ).
thf(469,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( a @ ( sigma @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( b @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[32,445]) ).
thf(470,plain,
( ( sigma @ ( a @ addition ) @ ( b @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[469:[bind(A,$thf( sigma )),bind(B,$thf( a ))]]) ).
thf(717,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( a @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[470,32]) ).
thf(718,plain,
( ( b @ ( sigma @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[717:[bind(A,$thf( b )),bind(B,$thf( sigma @ ( a @ addition ) ))]]) ).
thf(839,plain,
( ( b @ ( sigma @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[718,23]) ).
thf(878,plain,
! [A: $i] :
( ( ( A @ ( sigma @ addition ) )
!= ( b @ ( sigma @ addition ) ) )
| ( ( A @ ( b @ addition ) @ ( a @ addition ) @ ( a @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[161,839]) ).
thf(879,plain,
( ( b @ ( b @ addition ) @ ( a @ addition ) @ ( a @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[878:[bind(A,$thf( b ))]]) ).
thf(1466,plain,
( ( b @ ( a @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[879,26]) ).
thf(1471,plain,
( ( ( b @ ( a @ addition ) )
!= ( b @ ( a @ addition ) ) )
| ( ( sigma @ ( a @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[56,1466]) ).
thf(1472,plain,
( ( sigma @ ( a @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[1471:[]]) ).
thf(486,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( a @ ( sigma @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) @ ( b @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[23,445]) ).
thf(493,plain,
! [C: $i,B: $i,A: $i] :
( ( A != a )
| ( ( B @ ( C @ addition ) )
!= sigma )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) @ ( b @ addition ) )
= sigma ) ),
inference(simp,[status(thm)],[486]) ).
thf(508,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= sigma )
| ( ( a @ ( A @ addition ) @ ( B @ addition ) @ ( b @ addition ) )
= sigma ) ),
inference(simp,[status(thm)],[493]) ).
thf(66810,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( a @ addition ) )
!= ( A @ ( B @ addition ) ) )
| ( sigma != sigma )
| ( ( a @ ( A @ addition ) @ ( B @ addition ) @ ( b @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[1472,508]) ).
thf(66811,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( a @ addition ) )
!= ( A @ ( B @ addition ) ) )
| ( ( a @ ( A @ addition ) @ ( B @ addition ) @ ( b @ addition ) )
= sigma ) ),
inference(simp,[status(thm)],[66810]) ).
thf(66812,plain,
( ( a @ ( sigma @ addition ) @ ( a @ addition ) @ ( b @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[66811:[bind(A,$thf( sigma )),bind(B,$thf( a ))]]) ).
thf(283,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[56,32]) ).
thf(284,plain,
( ( a @ ( b @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[283:[bind(A,$thf( a )),bind(B,$thf( b ))]]) ).
thf(349,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ ( b @ addition ) )
!= ( B @ ( C @ addition ) ) )
| ( ( A @ ( sigma @ addition ) )
= ( A @ ( B @ addition ) @ ( C @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[284,23]) ).
thf(350,plain,
! [A: $i] :
( ( A @ ( sigma @ addition ) )
= ( A @ ( a @ addition ) @ ( b @ addition ) ) ),
inference(pattern_uni,[status(thm)],[349:[bind(A,$thf( A )),bind(B,$thf( a )),bind(C,$thf( b ))]]) ).
thf(39895,plain,
! [A: $i] :
( ( A @ ( a @ addition ) @ ( b @ addition ) )
= ( A @ ( b @ addition ) @ ( a @ addition ) ) ),
inference(rewrite,[status(thm)],[350,161]) ).
thf(90821,plain,
( ( a @ ( sigma @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[66812,39895]) ).
thf(11,axiom,
! [A: $i] :
( ( A @ ( one @ multiplication ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_left_identity) ).
thf(44,plain,
! [A: $i] :
( ( A @ ( one @ multiplication ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(45,plain,
! [A: $i] :
( ( A @ ( one @ multiplication ) )
= A ),
inference(cnf,[status(esa)],[44]) ).
thf(46,plain,
! [A: $i] :
( ( A @ ( one @ multiplication ) )
= A ),
inference(lifteq,[status(thm)],[45]) ).
thf(3095,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( B @ ( A @ leq ) )
| ( sigma != B ) ),
inference(paramod_ordered,[status(thm)],[1472,71]) ).
thf(3096,plain,
( ( sigma @ ( a @ leq ) )
| ( sigma != sigma ) ),
inference(pattern_uni,[status(thm)],[3095:[bind(A,$thf( a )),bind(B,$thf( sigma ))]]) ).
thf(3115,plain,
sigma @ ( a @ leq ),
inference(simp,[status(thm)],[3096]) ).
thf(14,axiom,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
= zero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_annihilation) ).
thf(52,plain,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
= zero ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(53,plain,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
= zero ),
inference(cnf,[status(esa)],[52]) ).
thf(54,plain,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
= zero ),
inference(lifteq,[status(thm)],[53]) ).
thf(87,plain,
! [A: $i] :
( ( ( zero @ ( A @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) ) )
| ~ ( zero @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[54,20]) ).
thf(102,plain,
! [A: $i] :
( ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ( A != a )
| ~ ( zero @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[87]) ).
thf(110,plain,
( ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[102]) ).
thf(5081,plain,
( ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(rewrite,[status(thm)],[110,54]) ).
thf(5109,plain,
! [A: $i] :
( ( ( A @ ( zero @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) ) )
| ( zero != zero )
| ~ ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[35,5081]) ).
thf(5110,plain,
! [A: $i] :
( ( ( A @ ( zero @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) ) )
| ~ ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[5109]) ).
thf(5139,plain,
! [A: $i] :
( ( A != a )
| ( zero != sigma )
| ~ ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[5110]) ).
thf(5150,plain,
( ( zero != sigma )
| ~ ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[5139]) ).
thf(13243,plain,
( ( ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) )
!= ( sigma @ ( a @ leq ) ) )
| ( zero != sigma )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3115,5150]) ).
thf(13244,plain,
( ( ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) )
!= ( sigma @ ( a @ leq ) ) )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[13243]) ).
thf(13261,plain,
( ( zero != sigma )
| ( ( a @ ( b @ multiplication ) @ ( a @ multiplication ) )
!= a )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[13244]) ).
thf(13279,plain,
( ( ( a @ ( b @ multiplication ) @ ( a @ multiplication ) )
!= a )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[13261]) ).
thf(13299,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( ( A @ ( a @ multiplication ) )
!= a )
| ( zero != sigma ) ),
inference(paramod_ordered,[status(thm)],[46,13279]) ).
thf(13316,plain,
! [A: $i] :
( ( A != a )
| ( one != b )
| ( ( A @ ( a @ multiplication ) )
!= a )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[13299]) ).
thf(13321,plain,
( ( one != b )
| ( ( a @ ( a @ multiplication ) )
!= a )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[13316]) ).
thf(297,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= ( C @ ( sigma @ addition ) ) )
| ( ( B @ ( A @ addition ) )
= ( C @ ( b @ addition ) @ ( a @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[32,161]) ).
thf(298,plain,
! [A: $i] :
( ( sigma @ ( A @ addition ) )
= ( A @ ( b @ addition ) @ ( a @ addition ) ) ),
inference(pattern_uni,[status(thm)],[297:[bind(A,$thf( A )),bind(B,$thf( sigma )),bind(C,$thf( A ))]]) ).
thf(5380,plain,
! [A: $i] :
( ( ( a @ ( sigma @ addition ) @ ( b @ addition ) )
!= ( A @ ( b @ addition ) ) )
| ( ( sigma @ ( a @ addition ) )
= ( sigma @ ( A @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[445,298]) ).
thf(5381,plain,
( ( sigma @ ( a @ ( sigma @ addition ) @ addition ) )
= ( sigma @ ( a @ addition ) ) ),
inference(pattern_uni,[status(thm)],[5380:[bind(A,$thf( a @ ( sigma @ addition ) ))]]) ).
thf(6028,plain,
( ( sigma @ ( a @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[5381,1472,23]) ).
thf(6103,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( a @ addition ) @ ( sigma @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[6028,32]) ).
thf(6104,plain,
( ( sigma @ ( sigma @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[6103:[bind(A,$thf( sigma )),bind(B,$thf( sigma @ ( a @ addition ) ))]]) ).
thf(6832,plain,
( ( sigma @ ( sigma @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[6104,23]) ).
thf(6913,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( sigma @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[6832,32]) ).
thf(6914,plain,
( ( a @ ( sigma @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[6913:[bind(A,$thf( a )),bind(B,$thf( sigma @ ( sigma @ addition ) ))]]) ).
thf(7120,plain,
( ( a @ ( sigma @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[6914,23]) ).
thf(7218,plain,
! [A: $i] :
( ( ( A @ ( sigma @ addition ) )
!= ( a @ ( sigma @ addition ) ) )
| ( ( A @ ( b @ addition ) @ ( a @ addition ) @ ( sigma @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[161,7120]) ).
thf(7219,plain,
( ( a @ ( b @ addition ) @ ( a @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[7218:[bind(A,$thf( a ))]]) ).
thf(9056,plain,
( ( a @ ( b @ addition ) @ ( a @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[7219,161]) ).
thf(9187,plain,
! [A: $i] :
( ( ( a @ ( b @ addition ) @ ( a @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
!= ( A @ ( b @ addition ) @ ( a @ addition ) ) )
| ( ( sigma @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[9056,298]) ).
thf(9188,plain,
( ( sigma @ ( a @ ( b @ addition ) @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[9187:[bind(A,$thf( a @ ( b @ addition ) @ ( a @ addition ) ))]]) ).
thf(9681,plain,
( ( sigma @ ( a @ ( b @ addition ) @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[9188,23]) ).
thf(9807,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( a @ ( b @ addition ) @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[9681,32]) ).
thf(9808,plain,
( ( a @ ( sigma @ ( a @ ( b @ addition ) @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[9807:[bind(A,$thf( a )),bind(B,$thf( sigma @ ( a @ ( b @ addition ) @ addition ) ))]]) ).
thf(10131,plain,
( ( a @ ( sigma @ addition ) @ ( a @ ( b @ addition ) @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[9808,23]) ).
thf(10258,plain,
! [B: $i,A: $i] :
( ( ( a @ ( sigma @ addition ) @ ( a @ ( b @ addition ) @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[10131,32]) ).
thf(10259,plain,
( ( a @ ( b @ addition ) @ ( a @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[10258:[bind(A,$thf( a @ ( b @ addition ) )),bind(B,$thf( a @ ( sigma @ addition ) ))]]) ).
thf(11704,plain,
( ( a @ ( b @ addition ) @ ( a @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[10259,23]) ).
thf(11860,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( a @ ( b @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( a @ addition ) @ ( sigma @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[32,11704]) ).
thf(11861,plain,
( ( b @ ( a @ addition ) @ ( a @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[11860:[bind(A,$thf( b )),bind(B,$thf( a ))]]) ).
thf(15101,plain,
( ( b @ ( a @ addition ) @ ( a @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[11861,161]) ).
thf(15304,plain,
! [A: $i] :
( ( ( b @ ( a @ addition ) @ ( a @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
!= ( A @ ( b @ addition ) @ ( a @ addition ) ) )
| ( ( sigma @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[15101,298]) ).
thf(15305,plain,
( ( sigma @ ( b @ ( a @ addition ) @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[15304:[bind(A,$thf( b @ ( a @ addition ) @ ( a @ addition ) ))]]) ).
thf(17856,plain,
( ( sigma @ ( b @ ( a @ addition ) @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[15305,23]) ).
thf(18046,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( b @ ( a @ addition ) @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[17856,32]) ).
thf(18047,plain,
( ( a @ ( sigma @ ( b @ ( a @ addition ) @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[18046:[bind(A,$thf( a )),bind(B,$thf( sigma @ ( b @ ( a @ addition ) @ addition ) ))]]) ).
thf(22047,plain,
( ( a @ ( sigma @ addition ) @ ( b @ ( a @ addition ) @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[18047,23]) ).
thf(456,plain,
! [A: $i] :
( ( ( a @ ( sigma @ addition ) @ ( b @ addition ) )
!= ( zero @ ( A @ addition ) ) )
| ( sigma = A ) ),
inference(paramod_ordered,[status(thm)],[445,29]) ).
thf(499,plain,
! [A: $i] :
( ( ( a @ ( sigma @ addition ) )
!= zero )
| ( b != A )
| ( sigma = A ) ),
inference(simp,[status(thm)],[456]) ).
thf(513,plain,
( ( ( a @ ( sigma @ addition ) )
!= zero )
| ( sigma = b ) ),
inference(simp,[status(thm)],[499]) ).
thf(72731,plain,
( ( ( a @ ( b @ addition ) @ ( a @ addition ) )
!= zero )
| ( sigma = b ) ),
inference(rewrite,[status(thm)],[513,161]) ).
thf(1596,plain,
( ( sigma @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[470,1472]) ).
thf(218,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)],[26,23]) ).
thf(219,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) @ ( B @ addition ) @ ( A @ addition ) )
= ( B @ ( A @ addition ) ) ),
inference(pattern_uni,[status(thm)],[218:[bind(A,$thf( H @ ( G @ addition ) )),bind(B,$thf( H @ ( G @ addition ) )),bind(C,$thf( H )),bind(D,$thf( G ))]]) ).
thf(228,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) @ ( B @ addition ) @ ( A @ addition ) )
= ( B @ ( A @ addition ) ) ),
inference(simp,[status(thm)],[219]) ).
thf(22681,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( sigma @ ( B @ addition ) @ ( A @ addition ) )
= ( B @ ( A @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[1596,228]) ).
thf(22682,plain,
( ( sigma @ ( sigma @ addition ) @ ( b @ addition ) )
= ( sigma @ ( b @ addition ) ) ),
inference(pattern_uni,[status(thm)],[22681:[bind(A,$thf( b )),bind(B,$thf( sigma ))]]) ).
thf(32289,plain,
( ( sigma @ ( b @ addition ) @ ( a @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[22682,161,1596]) ).
thf(32524,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( b @ addition ) @ ( a @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[32289,32]) ).
thf(32525,plain,
( ( b @ ( sigma @ ( b @ addition ) @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[32524:[bind(A,$thf( b )),bind(B,$thf( sigma @ ( b @ addition ) @ ( a @ addition ) ))]]) ).
thf(38197,plain,
( ( b @ ( sigma @ ( b @ addition ) @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[32525,23]) ).
thf(38437,plain,
! [B: $i,A: $i] :
( ( ( b @ ( sigma @ ( b @ addition ) @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[38197,32]) ).
thf(38438,plain,
( ( a @ ( b @ ( sigma @ ( b @ addition ) @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[38437:[bind(A,$thf( a )),bind(B,$thf( b @ ( sigma @ ( b @ addition ) @ addition ) ))]]) ).
thf(48259,plain,
( ( a @ ( b @ addition ) @ ( sigma @ ( b @ addition ) @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[38438,23]) ).
thf(48334,plain,
( ( ( a @ ( b @ addition ) )
!= ( a @ ( b @ addition ) ) )
| ( ( sigma @ ( sigma @ ( b @ addition ) @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[284,48259]) ).
thf(48335,plain,
( ( sigma @ ( sigma @ ( b @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[48334:[]]) ).
thf(49117,plain,
( ( sigma @ ( sigma @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[48335,23]) ).
thf(49318,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( sigma @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[49117,32]) ).
thf(49319,plain,
( ( b @ ( sigma @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[49318:[bind(A,$thf( b )),bind(B,$thf( sigma @ ( sigma @ addition ) ))]]) ).
thf(49828,plain,
( ( b @ ( sigma @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[49319,23]) ).
thf(67,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
= B )
| ~ ( B @ ( A @ leq ) ) ),
inference(cnfConj,[status(thm)],[66]) ).
thf(69,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ leq ) )
| ( ( B @ ( A @ addition ) )
= B ) ),
inference(lifteq,[status(thm)],[67]) ).
thf(319,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( E @ ( D @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
= ( D @ ( E @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[23,32]) ).
thf(320,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ addition ) @ ( B @ addition ) )
= ( C @ ( B @ addition ) @ ( A @ addition ) ) ),
inference(pattern_uni,[status(thm)],[319:[bind(A,$thf( A )),bind(B,$thf( G )),bind(C,$thf( F )),bind(D,$thf( G @ ( F @ addition ) )),bind(E,$thf( A ))]]) ).
thf(323,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ addition ) @ ( B @ addition ) )
= ( C @ ( B @ addition ) @ ( A @ addition ) ) ),
inference(simp,[status(thm)],[320]) ).
thf(36004,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sigma @ ( b @ addition ) @ ( a @ addition ) @ ( b @ addition ) )
!= ( A @ ( C @ addition ) @ ( B @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[32289,323]) ).
thf(36005,plain,
( ( a @ ( b @ addition ) @ ( sigma @ ( b @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[36004:[bind(A,$thf( sigma @ ( b @ addition ) )),bind(B,$thf( b )),bind(C,$thf( a ))]]) ).
thf(43744,plain,
( ( a @ ( b @ addition ) @ ( sigma @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[36005,23]) ).
thf(44054,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ addition ) @ ( B @ addition ) )
!= ( a @ ( b @ addition ) @ ( sigma @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) @ ( b @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[323,43744]) ).
thf(44055,plain,
( ( b @ ( sigma @ addition ) @ ( a @ addition ) @ ( b @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[44054:[bind(A,$thf( a )),bind(B,$thf( sigma )),bind(C,$thf( b ))]]) ).
thf(58450,plain,
( ( b @ ( sigma @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[44055,39895]) ).
thf(313,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)],[32,23]) ).
thf(314,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ addition ) @ addition ) )
= ( C @ ( B @ addition ) @ ( A @ addition ) ) ),
inference(pattern_uni,[status(thm)],[313:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( B )),bind(E,$thf( A ))]]) ).
thf(33798,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ addition ) @ ( B @ addition ) )
= ( C @ ( B @ addition ) @ ( A @ addition ) ) ),
inference(rewrite,[status(thm)],[314,23]) ).
thf(48612,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ ( b @ addition ) @ ( sigma @ ( b @ addition ) @ addition ) )
!= ( C @ ( A @ addition ) @ ( B @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[48259,33798]) ).
thf(48613,plain,
( ( a @ ( sigma @ ( b @ addition ) @ addition ) @ ( b @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[48612:[bind(A,$thf( b )),bind(B,$thf( sigma @ ( b @ addition ) )),bind(C,$thf( a ))]]) ).
thf(162,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)],[23,23]) ).
thf(163,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)],[162:[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(172,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)],[163]) ).
thf(11061,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)],[172,23]) ).
thf(63882,plain,
( ( a @ ( sigma @ addition ) @ ( b @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[48613,11061]) ).
thf(3101,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ addition ) )
!= ( C @ ( B @ addition ) ) )
| ( C @ ( B @ leq ) )
| ( A != C ) ),
inference(paramod_ordered,[status(thm)],[26,71]) ).
thf(3102,plain,
! [A: $i] :
( ( A @ ( A @ leq ) )
| ( A != A ) ),
inference(pattern_uni,[status(thm)],[3101:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(3119,plain,
! [A: $i] : ( A @ ( A @ leq ) ),
inference(simp,[status(thm)],[3102]) ).
thf(12,axiom,
! [A: $i] :
( ( one @ ( A @ multiplication ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_right_identity) ).
thf(47,plain,
! [A: $i] :
( ( one @ ( A @ multiplication ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(48,plain,
! [A: $i] :
( ( one @ ( A @ multiplication ) )
= A ),
inference(cnf,[status(esa)],[47]) ).
thf(49,plain,
! [A: $i] :
( ( one @ ( A @ multiplication ) )
= A ),
inference(lifteq,[status(thm)],[48]) ).
thf(138,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[46,20]) ).
thf(139,plain,
! [A: $i] :
( ( A
!= ( a @ ( b @ multiplication ) ) )
| ( one != a )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[138]) ).
thf(152,plain,
( ( one != a )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[139]) ).
thf(8458,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) ) )
| ( one != a )
| ~ ( A @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[49,152]) ).
thf(8482,plain,
! [A: $i] :
( ( one != a )
| ( A != sigma )
| ( one != a )
| ~ ( A @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[8458]) ).
thf(8509,plain,
( ( one != a )
| ~ ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[8482]) ).
thf(79855,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( one != a )
| ~ ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[49,8509]) ).
thf(79883,plain,
! [A: $i] :
( ( one != a )
| ( A != b )
| ( one != a )
| ~ ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[79855]) ).
thf(79904,plain,
( ( one != a )
| ~ ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( b @ leq ) ) ),
inference(simp,[status(thm)],[79883]) ).
thf(81690,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( sigma @ ( a @ multiplication ) ) )
| ( one != a )
| ~ ( A @ ( sigma @ star @ multiplication ) @ ( b @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[46,79904]) ).
thf(81740,plain,
! [A: $i] :
( ( A != sigma )
| ( one != a )
| ( one != a )
| ~ ( A @ ( sigma @ star @ multiplication ) @ ( b @ leq ) ) ),
inference(simp,[status(thm)],[81690]) ).
thf(81752,plain,
( ( one != a )
| ~ ( sigma @ ( sigma @ star @ multiplication ) @ ( b @ leq ) ) ),
inference(simp,[status(thm)],[81740]) ).
thf(81922,plain,
! [A: $i] :
( ( ( A @ ( A @ leq ) )
!= ( sigma @ ( sigma @ star @ multiplication ) @ ( b @ leq ) ) )
| ( one != a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3119,81752]) ).
thf(81923,plain,
! [A: $i] :
( ( ( A @ ( A @ leq ) )
!= ( sigma @ ( sigma @ star @ multiplication ) @ ( b @ leq ) ) )
| ( one != a ) ),
inference(simp,[status(thm)],[81922]) ).
thf(81949,plain,
! [A: $i] :
( ( A
!= ( sigma @ ( sigma @ star @ multiplication ) ) )
| ( A != b )
| ( one != a ) ),
inference(simp,[status(thm)],[81923]) ).
thf(81970,plain,
( ( ( sigma @ ( sigma @ star @ multiplication ) )
!= b )
| ( one != a ) ),
inference(simp,[status(thm)],[81949]) ).
thf(483,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( a @ ( sigma @ addition ) @ ( b @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[445,23]) ).
thf(500,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( a @ ( sigma @ addition ) ) )
| ( ( B @ ( C @ addition ) )
!= b )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
= sigma ) ),
inference(simp,[status(thm)],[483]) ).
thf(514,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= b )
| ( ( a @ ( sigma @ addition ) @ ( A @ addition ) @ ( B @ addition ) )
= sigma ) ),
inference(simp,[status(thm)],[500]) ).
thf(73180,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= b )
| ( ( a @ ( b @ addition ) @ ( a @ addition ) @ ( A @ addition ) @ ( B @ addition ) )
= sigma ) ),
inference(rewrite,[status(thm)],[514,161]) ).
thf(43971,plain,
! [B: $i,A: $i] :
( ( ( a @ ( b @ addition ) @ ( sigma @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[43744,32]) ).
thf(43972,plain,
( ( b @ ( a @ ( b @ addition ) @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[43971:[bind(A,$thf( b )),bind(B,$thf( a @ ( b @ addition ) @ ( sigma @ addition ) ))]]) ).
thf(57470,plain,
( ( b @ ( a @ ( b @ addition ) @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[43972,23]) ).
thf(57868,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( a @ ( b @ addition ) @ addition ) @ ( sigma @ addition ) )
!= ( C @ ( A @ addition ) @ ( B @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[57470,33798]) ).
thf(57869,plain,
( ( b @ ( sigma @ addition ) @ ( a @ ( b @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[57868:[bind(A,$thf( a @ ( b @ addition ) )),bind(B,$thf( sigma )),bind(C,$thf( b ))]]) ).
thf(76143,plain,
( ( b @ ( sigma @ addition ) @ ( a @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[57869,23]) ).
thf(38528,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( sigma @ ( b @ addition ) @ addition ) @ ( a @ addition ) )
!= ( C @ ( A @ addition ) @ ( B @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[38197,33798]) ).
thf(38529,plain,
( ( b @ ( a @ addition ) @ ( sigma @ ( b @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[38528:[bind(A,$thf( sigma @ ( b @ addition ) )),bind(B,$thf( a )),bind(C,$thf( b ))]]) ).
thf(54637,plain,
( ( b @ ( a @ addition ) @ ( sigma @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[38529,23]) ).
thf(54905,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ addition ) @ ( sigma @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[54637,32]) ).
thf(54906,plain,
( ( b @ ( b @ ( a @ addition ) @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[54905:[bind(A,$thf( b )),bind(B,$thf( b @ ( a @ addition ) @ ( sigma @ addition ) ))]]) ).
thf(70143,plain,
( ( b @ ( b @ ( a @ addition ) @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[54906,23]) ).
thf(81705,plain,
! [A: $i] :
( ( ( zero @ ( A @ multiplication ) )
!= ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) ) )
| ( one != a )
| ~ ( zero @ ( b @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[54,79904]) ).
thf(81734,plain,
! [A: $i] :
( ( ( sigma @ ( a @ multiplication ) )
!= zero )
| ( A
!= ( sigma @ star ) )
| ( one != a )
| ~ ( zero @ ( b @ leq ) ) ),
inference(simp,[status(thm)],[81705]) ).
thf(81747,plain,
( ( ( sigma @ ( a @ multiplication ) )
!= zero )
| ( one != a )
| ~ ( zero @ ( b @ leq ) ) ),
inference(simp,[status(thm)],[81734]) ).
thf(557,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)],[38,46]) ).
thf(582,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)],[557]) ).
thf(597,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= one )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= C ) ),
inference(simp,[status(thm)],[582]) ).
thf(13,axiom,
! [A: $i] : ( A @ star @ ( A @ ( A @ star @ multiplication ) @ ( one @ addition ) @ leq ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',star_unfold_left) ).
thf(50,plain,
! [A: $i] : ( A @ star @ ( A @ ( A @ star @ multiplication ) @ ( one @ addition ) @ leq ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(51,plain,
! [A: $i] : ( A @ star @ ( A @ ( A @ star @ multiplication ) @ ( one @ addition ) @ leq ) ),
inference(cnf,[status(esa)],[50]) ).
thf(1200,plain,
! [B: $i,A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( B @ ( B @ star @ multiplication ) ) )
| ( B @ star @ ( A @ ( one @ addition ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[49,51]) ).
thf(1201,plain,
one @ star @ ( one @ star @ ( one @ addition ) @ leq ),
inference(pattern_uni,[status(thm)],[1200:[bind(A,$thf( one @ star )),bind(B,$thf( one ))]]) ).
thf(2724,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)],[1201,69]) ).
thf(2725,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( one @ star @ ( one @ addition ) @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( ( B @ ( A @ addition ) )
= B ) ),
inference(simp,[status(thm)],[2724]) ).
thf(2726,plain,
( ( one @ star @ ( one @ star @ ( one @ addition ) @ addition ) )
= ( one @ star ) ),
inference(pattern_uni,[status(thm)],[2725:[bind(A,$thf( one @ star @ ( one @ addition ) )),bind(B,$thf( one @ star ))]]) ).
thf(3985,plain,
( ( one @ star @ ( one @ star @ addition ) @ ( one @ addition ) )
= ( one @ star ) ),
inference(rewrite,[status(thm)],[2726,23]) ).
thf(4065,plain,
! [A: $i] :
( ( ( A @ ( A @ addition ) )
!= ( one @ star @ ( one @ star @ addition ) ) )
| ( ( A @ ( one @ addition ) )
= ( one @ star ) ) ),
inference(paramod_ordered,[status(thm)],[26,3985]) ).
thf(4066,plain,
( ( one @ star @ ( one @ addition ) )
= ( one @ star ) ),
inference(pattern_uni,[status(thm)],[4065:[bind(A,$thf( one @ star ))]]) ).
thf(4244,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( one @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( B @ ( A @ leq ) )
| ( ( one @ star )
!= B ) ),
inference(paramod_ordered,[status(thm)],[4066,71]) ).
thf(4245,plain,
( ( one @ star @ ( one @ leq ) )
| ( ( one @ star )
!= ( one @ star ) ) ),
inference(pattern_uni,[status(thm)],[4244:[bind(A,$thf( one )),bind(B,$thf( one @ star ))]]) ).
thf(4339,plain,
one @ star @ ( one @ leq ),
inference(simp,[status(thm)],[4245]) ).
thf(347,plain,
! [A: $i] :
( ( ( A @ ( A @ addition ) )
!= ( a @ ( b @ addition ) ) )
| ( A = sigma ) ),
inference(paramod_ordered,[status(thm)],[26,284]) ).
thf(352,plain,
! [A: $i] :
( ( A != a )
| ( A != b )
| ( A = sigma ) ),
inference(simp,[status(thm)],[347]) ).
thf(360,plain,
( ( b != a )
| ( sigma = b ) ),
inference(simp,[status(thm)],[352]) ).
thf(212,plain,
! [A: $i] :
( ( ( A @ ( A @ addition ) )
!= ( b @ ( a @ addition ) ) )
| ( A = sigma ) ),
inference(paramod_ordered,[status(thm)],[26,56]) ).
thf(224,plain,
! [A: $i] :
( ( A != b )
| ( A != a )
| ( A = sigma ) ),
inference(simp,[status(thm)],[212]) ).
thf(226,plain,
( ( b != a )
| ( sigma = a ) ),
inference(simp,[status(thm)],[224]) ).
thf(3069,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( B @ ( A @ leq ) )
| ( sigma != B ) ),
inference(paramod_ordered,[status(thm)],[1596,71]) ).
thf(3070,plain,
( ( sigma @ ( b @ leq ) )
| ( sigma != sigma ) ),
inference(pattern_uni,[status(thm)],[3069:[bind(A,$thf( b )),bind(B,$thf( sigma ))]]) ).
thf(3118,plain,
sigma @ ( b @ leq ),
inference(simp,[status(thm)],[3070]) ).
thf(81931,plain,
( ( ( sigma @ ( sigma @ star @ multiplication ) @ ( b @ leq ) )
!= ( sigma @ ( b @ leq ) ) )
| ( one != a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3118,81752]) ).
thf(81932,plain,
( ( ( sigma @ ( sigma @ star @ multiplication ) @ ( b @ leq ) )
!= ( sigma @ ( b @ leq ) ) )
| ( one != a ) ),
inference(simp,[status(thm)],[81931]) ).
thf(81956,plain,
( ( ( sigma @ ( sigma @ star @ multiplication ) )
!= sigma )
| ( b != b )
| ( one != a ) ),
inference(simp,[status(thm)],[81932]) ).
thf(81965,plain,
( ( ( sigma @ ( sigma @ star @ multiplication ) )
!= sigma )
| ( one != a ) ),
inference(simp,[status(thm)],[81956]) ).
thf(81983,plain,
( ( sigma != sigma )
| ( ( a @ ( sigma @ star @ multiplication ) )
!= sigma )
| ( one != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[226,81965]) ).
thf(81984,plain,
( ( ( a @ ( sigma @ star @ multiplication ) )
!= sigma )
| ( one != a )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[81983:[]]) ).
thf(100241,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( sigma @ star @ multiplication ) ) )
| ( A != sigma )
| ( one != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[49,81984]) ).
thf(100255,plain,
( ( one != a )
| ( ( sigma @ star )
!= sigma )
| ( one != a )
| ( b != a ) ),
inference(simp,[status(thm)],[100241]) ).
thf(100265,plain,
( ( ( sigma @ star )
!= sigma )
| ( one != a )
| ( b != a ) ),
inference(simp,[status(thm)],[100255]) ).
thf(100268,plain,
( ( sigma != sigma )
| ( ( b @ star )
!= sigma )
| ( one != a )
| ( b != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[360,100265]) ).
thf(100269,plain,
( ( sigma != sigma )
| ( ( b @ star )
!= sigma )
| ( one != a )
| ( b != a ) ),
inference(simp,[status(thm)],[100268]) ).
thf(100270,plain,
( ( ( b @ star )
!= sigma )
| ( one != a )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[100269:[]]) ).
thf(81703,plain,
( ( ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( b @ leq ) )
!= ( sigma @ ( b @ leq ) ) )
| ( one != a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3118,79904]) ).
thf(81704,plain,
( ( ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( b @ leq ) )
!= ( sigma @ ( b @ leq ) ) )
| ( one != a ) ),
inference(simp,[status(thm)],[81703]) ).
thf(81736,plain,
( ( ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) )
!= sigma )
| ( b != b )
| ( one != a ) ),
inference(simp,[status(thm)],[81704]) ).
thf(81749,plain,
( ( ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) )
!= sigma )
| ( one != a ) ),
inference(simp,[status(thm)],[81736]) ).
thf(96676,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) ) )
| ( A != sigma )
| ( one != a ) ),
inference(paramod_ordered,[status(thm)],[49,81749]) ).
thf(96702,plain,
( ( ( sigma @ ( a @ multiplication ) )
!= one )
| ( ( sigma @ star )
!= sigma )
| ( one != a ) ),
inference(simp,[status(thm)],[96676]) ).
thf(399,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sigma @ ( b @ addition ) @ ( a @ addition ) )
!= ( B @ ( C @ addition ) ) )
| ( ( A @ ( sigma @ addition ) )
= ( A @ ( B @ addition ) @ ( C @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[237,23]) ).
thf(400,plain,
! [A: $i] :
( ( A @ ( sigma @ addition ) )
= ( A @ ( sigma @ ( b @ addition ) @ addition ) @ ( a @ addition ) ) ),
inference(pattern_uni,[status(thm)],[399:[bind(A,$thf( A )),bind(B,$thf( sigma @ ( b @ addition ) )),bind(C,$thf( a ))]]) ).
thf(46299,plain,
! [A: $i] :
( ( A @ ( sigma @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
= ( A @ ( b @ addition ) @ ( a @ addition ) ) ),
inference(rewrite,[status(thm)],[400,161,11061]) ).
thf(1198,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( A @ multiplication ) )
!= ( B @ ( B @ star @ multiplication ) ) )
| ( B @ star @ ( zero @ ( one @ addition ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[54,51]) ).
thf(1199,plain,
zero @ star @ ( zero @ ( one @ addition ) @ leq ),
inference(pattern_uni,[status(thm)],[1198:[bind(A,$thf( zero @ star )),bind(B,$thf( zero ))]]) ).
thf(1248,plain,
zero @ star @ ( one @ leq ),
inference(rewrite,[status(thm)],[1199,29]) ).
thf(89,plain,
! [A: $i] :
( ( ( A @ ( zero @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) ) )
| ~ ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[35,20]) ).
thf(97,plain,
! [A: $i] :
( ( A
!= ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) ) )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[89]) ).
thf(105,plain,
( ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[97]) ).
thf(1263,plain,
( ( ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) )
!= ( zero @ star @ ( one @ leq ) ) )
| ( ( sigma @ star )
!= zero )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1248,105]) ).
thf(1264,plain,
( ( ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) )
!= ( zero @ star @ ( one @ leq ) ) )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[1263]) ).
thf(1275,plain,
( ( ( zero @ star )
!= zero )
| ( ( a @ ( b @ multiplication ) @ ( a @ multiplication ) )
!= one )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[1264]) ).
thf(127,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[46,105]) ).
thf(143,plain,
! [A: $i] :
( ( A
!= ( a @ ( b @ multiplication ) ) )
| ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[127]) ).
thf(156,plain,
( ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( a @ ( b @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[143]) ).
thf(436,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[49,156]) ).
thf(440,plain,
! [A: $i] :
( ( one != a )
| ( A != b )
| ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[436]) ).
thf(444,plain,
( ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( b @ leq ) ) ),
inference(simp,[status(thm)],[440]) ).
thf(1265,plain,
( ( ( zero @ star @ ( one @ leq ) )
!= ( zero @ ( b @ leq ) ) )
| ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1248,444]) ).
thf(1266,plain,
( ( ( zero @ star @ ( one @ leq ) )
!= ( zero @ ( b @ leq ) ) )
| ( one != a )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[1265]) ).
thf(1277,plain,
( ( ( zero @ star )
!= zero )
| ( one != b )
| ( one != a )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[1266]) ).
thf(1918,plain,
( ( zero != zero )
| ( ( zero @ star )
!= ( sigma @ star ) )
| ( one != b )
| ( one != a )
| ( ( sigma @ star )
!= zero ) ),
inference(eqfactor_ordered,[status(thm)],[1277]) ).
thf(1919,plain,
( ( ( zero @ star )
!= ( sigma @ star ) )
| ( one != b )
| ( one != a )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[1918]) ).
thf(137,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) ) )
| ~ ( A @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[46,20]) ).
thf(140,plain,
! [A: $i] :
( ( A
!= ( a @ ( sigma @ multiplication ) ) )
| ( one != a )
| ~ ( A @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[137]) ).
thf(153,plain,
( ( one != a )
| ~ ( a @ ( sigma @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[140]) ).
thf(81972,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( sigma @ ( sigma @ star @ multiplication ) ) )
| ( A != sigma )
| ( one != a ) ),
inference(paramod_ordered,[status(thm)],[46,81965]) ).
thf(81992,plain,
( ( sigma != sigma )
| ( ( sigma @ star )
!= one )
| ( one != a ) ),
inference(simp,[status(thm)],[81972]) ).
thf(81998,plain,
( ( ( sigma @ star )
!= one )
| ( one != a ) ),
inference(simp,[status(thm)],[81992]) ).
thf(4032,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)],[3985,32]) ).
thf(4033,plain,
( ( one @ ( one @ star @ ( one @ star @ addition ) @ addition ) )
= ( one @ star ) ),
inference(pattern_uni,[status(thm)],[4032:[bind(A,$thf( one )),bind(B,$thf( one @ star @ ( one @ star @ addition ) ))]]) ).
thf(4605,plain,
( ( one @ ( one @ star @ addition ) @ ( one @ star @ addition ) )
= ( one @ star ) ),
inference(rewrite,[status(thm)],[4033,23]) ).
thf(4652,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)],[4605,32]) ).
thf(4653,plain,
( ( one @ star @ ( one @ ( one @ star @ addition ) @ addition ) )
= ( one @ star ) ),
inference(pattern_uni,[status(thm)],[4652:[bind(A,$thf( one @ star )),bind(B,$thf( one @ ( one @ star @ addition ) ))]]) ).
thf(4839,plain,
( ( one @ star @ ( one @ addition ) @ ( one @ star @ addition ) )
= ( one @ star ) ),
inference(rewrite,[status(thm)],[4653,23]) ).
thf(13239,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( zero != sigma )
| ~ ( zero @ ( A @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[46,5150]) ).
thf(13272,plain,
! [A: $i] :
( ( A != a )
| ( one != b )
| ( zero != sigma )
| ~ ( zero @ ( A @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[13239]) ).
thf(13287,plain,
( ( one != b )
| ( zero != sigma )
| ~ ( zero @ ( a @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[13272]) ).
thf(10264,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( a @ ( b @ addition ) ) )
| ( ( a @ ( sigma @ addition ) @ ( A @ ( B @ addition ) @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[32,10131]) ).
thf(10265,plain,
( ( a @ ( sigma @ addition ) @ ( b @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[10264:[bind(A,$thf( b )),bind(B,$thf( a ))]]) ).
thf(12713,plain,
( ( a @ ( sigma @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[10265,23]) ).
thf(12879,plain,
! [B: $i,A: $i] :
( ( ( a @ ( sigma @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[12713,32]) ).
thf(12880,plain,
( ( a @ ( a @ ( sigma @ addition ) @ ( b @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[12879:[bind(A,$thf( a )),bind(B,$thf( a @ ( sigma @ addition ) @ ( b @ addition ) ))]]) ).
thf(16416,plain,
( ( a @ ( a @ ( sigma @ addition ) @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[12880,23]) ).
thf(16599,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ ( sigma @ addition ) @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[16416,32]) ).
thf(16600,plain,
( ( b @ ( a @ ( a @ ( sigma @ addition ) @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[16599:[bind(A,$thf( b )),bind(B,$thf( a @ ( a @ ( sigma @ addition ) @ addition ) ))]]) ).
thf(19318,plain,
( ( b @ ( a @ addition ) @ ( a @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[16600,23]) ).
thf(58726,plain,
! [B: $i,A: $i] :
( ( ( b @ ( sigma @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[58450,32]) ).
thf(58727,plain,
( ( a @ ( b @ ( sigma @ addition ) @ ( b @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[58726:[bind(A,$thf( a )),bind(B,$thf( b @ ( sigma @ addition ) @ ( b @ addition ) ))]]) ).
thf(77351,plain,
( ( a @ ( b @ ( sigma @ addition ) @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[58727,23]) ).
thf(77662,plain,
! [B: $i,A: $i] :
( ( ( a @ ( b @ ( sigma @ addition ) @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[77351,32]) ).
thf(77663,plain,
( ( b @ ( a @ ( b @ ( sigma @ addition ) @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[77662:[bind(A,$thf( b )),bind(B,$thf( a @ ( b @ ( sigma @ addition ) @ addition ) ))]]) ).
thf(103050,plain,
( ( b @ ( a @ addition ) @ ( b @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[77663,23]) ).
thf(49392,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sigma @ ( sigma @ addition ) @ ( b @ addition ) )
!= ( A @ ( C @ addition ) @ ( B @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[49117,323]) ).
thf(49393,plain,
( ( sigma @ ( b @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[49392:[bind(A,$thf( sigma )),bind(B,$thf( b )),bind(C,$thf( sigma ))]]) ).
thf(50584,plain,
( ( sigma @ ( b @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[49393,161]) ).
thf(50833,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( b @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[50584,32]) ).
thf(50834,plain,
( ( a @ ( sigma @ ( b @ addition ) @ ( b @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[50833:[bind(A,$thf( a )),bind(B,$thf( sigma @ ( b @ addition ) @ ( b @ addition ) ))]]) ).
thf(68923,plain,
( ( a @ ( sigma @ ( b @ addition ) @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[50834,23]) ).
thf(69215,plain,
! [B: $i,A: $i] :
( ( ( a @ ( sigma @ ( b @ addition ) @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[68923,32]) ).
thf(69216,plain,
( ( b @ ( a @ ( sigma @ ( b @ addition ) @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[69215:[bind(A,$thf( b )),bind(B,$thf( a @ ( sigma @ ( b @ addition ) @ addition ) ))]]) ).
thf(95147,plain,
( ( b @ ( a @ addition ) @ ( sigma @ ( b @ addition ) @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[69216,23]) ).
thf(55028,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( a @ addition ) @ ( sigma @ addition ) @ ( b @ addition ) )
!= ( C @ ( A @ addition ) @ ( B @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[54637,33798]) ).
thf(55029,plain,
( ( b @ ( a @ addition ) @ ( b @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[55028:[bind(A,$thf( sigma )),bind(B,$thf( b )),bind(C,$thf( b @ ( a @ addition ) ))]]) ).
thf(71269,plain,
( ( b @ ( a @ addition ) @ ( b @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[55029,161]) ).
thf(71624,plain,
! [A: $i] :
( ( ( b @ ( a @ addition ) @ ( b @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
!= ( A @ ( b @ addition ) @ ( a @ addition ) ) )
| ( ( sigma @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[71269,298]) ).
thf(71625,plain,
( ( sigma @ ( b @ ( a @ addition ) @ ( b @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[71624:[bind(A,$thf( b @ ( a @ addition ) @ ( b @ addition ) ))]]) ).
thf(98158,plain,
( ( sigma @ ( b @ ( a @ addition ) @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[71625,23]) ).
thf(13247,plain,
( ( ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) )
!= ( sigma @ ( b @ leq ) ) )
| ( zero != sigma )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3118,5150]) ).
thf(13248,plain,
( ( ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) )
!= ( sigma @ ( b @ leq ) ) )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[13247]) ).
thf(13264,plain,
( ( zero != sigma )
| ( ( a @ ( b @ multiplication ) @ ( a @ multiplication ) )
!= b )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[13248]) ).
thf(13280,plain,
( ( ( a @ ( b @ multiplication ) @ ( a @ multiplication ) )
!= b )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[13264]) ).
thf(82102,plain,
( ( sigma != sigma )
| ( ( a @ ( sigma @ star @ multiplication ) )
!= b )
| ( one != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[226,81970]) ).
thf(82103,plain,
( ( ( a @ ( sigma @ star @ multiplication ) )
!= b )
| ( one != a )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[82102:[]]) ).
thf(104556,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( sigma @ star @ multiplication ) ) )
| ( A != b )
| ( one != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[49,82103]) ).
thf(104570,plain,
( ( one != a )
| ( ( sigma @ star )
!= b )
| ( one != a )
| ( b != a ) ),
inference(simp,[status(thm)],[104556]) ).
thf(104580,plain,
( ( ( sigma @ star )
!= b )
| ( one != a )
| ( b != a ) ),
inference(simp,[status(thm)],[104570]) ).
thf(104593,plain,
( ( sigma != sigma )
| ( ( a @ star )
!= b )
| ( one != a )
| ( b != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[226,104580]) ).
thf(104594,plain,
( ( sigma != sigma )
| ( ( a @ star )
!= b )
| ( one != a )
| ( b != a ) ),
inference(simp,[status(thm)],[104593]) ).
thf(104595,plain,
( ( ( a @ star )
!= b )
| ( one != a )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[104594:[]]) ).
thf(81978,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( sigma @ ( sigma @ star @ multiplication ) ) )
| ( A != sigma )
| ( one != a ) ),
inference(paramod_ordered,[status(thm)],[49,81965]) ).
thf(81987,plain,
( ( one != sigma )
| ( ( sigma @ star )
!= sigma )
| ( one != a ) ),
inference(simp,[status(thm)],[81978]) ).
thf(4372,plain,
( ( ( one @ star @ ( one @ leq ) )
!= ( zero @ ( b @ leq ) ) )
| ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4339,444]) ).
thf(4373,plain,
( ( ( one @ star @ ( one @ leq ) )
!= ( zero @ ( b @ leq ) ) )
| ( one != a )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[4372]) ).
thf(4388,plain,
( ( ( one @ star )
!= zero )
| ( one != b )
| ( one != a )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[4373]) ).
thf(30811,plain,
( ( zero != zero )
| ( ( one @ star )
!= ( sigma @ star ) )
| ( one != b )
| ( one != a )
| ( ( sigma @ star )
!= zero ) ),
inference(eqfactor_ordered,[status(thm)],[4388]) ).
thf(30813,plain,
( ( one != sigma )
| ( one != b )
| ( one != a )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[30811]) ).
thf(40726,plain,
( ( sigma != sigma )
| ( one != sigma )
| ( one != b )
| ( one != a )
| ( ( b @ star )
!= zero )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[360,30813]) ).
thf(40727,plain,
( ( one != sigma )
| ( one != b )
| ( one != a )
| ( ( b @ star )
!= zero )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[40726:[]]) ).
thf(30812,plain,
( ( ( one @ star )
!= ( sigma @ star ) )
| ( one != b )
| ( one != a )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[30811]) ).
thf(177,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( A @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[49,105]) ).
thf(199,plain,
! [A: $i] :
( ( one != a )
| ( A != b )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( A @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[177]) ).
thf(208,plain,
( ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( b @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[199]) ).
thf(1257,plain,
( ( ( zero @ ( b @ ( a @ multiplication ) @ leq ) )
!= ( zero @ star @ ( one @ leq ) ) )
| ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1248,208]) ).
thf(1258,plain,
( ( ( zero @ ( b @ ( a @ multiplication ) @ leq ) )
!= ( zero @ star @ ( one @ leq ) ) )
| ( one != a )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[1257]) ).
thf(1279,plain,
( ( ( zero @ star )
!= zero )
| ( ( b @ ( a @ multiplication ) )
!= one )
| ( one != a )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[1258]) ).
thf(15073,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( ( A @ ( a @ multiplication ) )
!= b )
| ( zero != sigma ) ),
inference(paramod_ordered,[status(thm)],[46,13280]) ).
thf(15080,plain,
! [A: $i] :
( ( A != a )
| ( one != b )
| ( ( A @ ( a @ multiplication ) )
!= b )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[15073]) ).
thf(15092,plain,
( ( one != b )
| ( ( a @ ( a @ multiplication ) )
!= b )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[15080]) ).
thf(13259,plain,
( ( ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) )
!= ( zero @ star @ ( one @ leq ) ) )
| ( zero != sigma )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1248,5150]) ).
thf(13260,plain,
( ( ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) )
!= ( zero @ star @ ( one @ leq ) ) )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[13259]) ).
thf(13275,plain,
( ( ( zero @ star )
!= zero )
| ( ( a @ ( b @ multiplication ) @ ( a @ multiplication ) )
!= one )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[13260]) ).
thf(15072,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) )
| ( A != b )
| ( zero != sigma ) ),
inference(paramod_ordered,[status(thm)],[46,13280]) ).
thf(15086,plain,
( ( ( a @ ( b @ multiplication ) )
!= b )
| ( one != a )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[15072]) ).
thf(17841,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( A != b )
| ( one != a )
| ( zero != sigma ) ),
inference(paramod_ordered,[status(thm)],[49,15086]) ).
thf(17846,plain,
( ( one != a )
| ( b != b )
| ( one != a )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[17841]) ).
thf(17852,plain,
( ( one != a )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[17846]) ).
thf(542,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)],[38,38]) ).
thf(543,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)],[542:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ multiplication ) )),bind(E,$thf( C ))]]) ).
thf(606,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)],[543]) ).
thf(99575,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)],[606,38]) ).
thf(2808,plain,
! [B: $i,A: $i] :
( ( ( zero @ star @ ( one @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[1248,69]) ).
thf(2809,plain,
! [B: $i,A: $i] :
( ( ( zero @ star @ ( one @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( ( B @ ( A @ addition ) )
= B ) ),
inference(simp,[status(thm)],[2808]) ).
thf(2810,plain,
( ( zero @ star @ ( one @ addition ) )
= ( zero @ star ) ),
inference(pattern_uni,[status(thm)],[2809:[bind(A,$thf( one )),bind(B,$thf( zero @ star ))]]) ).
thf(3311,plain,
! [B: $i,A: $i] :
( ( ( zero @ star @ ( one @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= ( zero @ star ) ) ),
inference(paramod_ordered,[status(thm)],[2810,32]) ).
thf(3312,plain,
( ( one @ ( zero @ star @ addition ) )
= ( zero @ star ) ),
inference(pattern_uni,[status(thm)],[3311:[bind(A,$thf( one )),bind(B,$thf( zero @ star ))]]) ).
thf(81976,plain,
( ( sigma != sigma )
| ( ( b @ ( sigma @ star @ multiplication ) )
!= sigma )
| ( one != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[360,81965]) ).
thf(81977,plain,
( ( ( b @ ( sigma @ star @ multiplication ) )
!= sigma )
| ( one != a )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[81976:[]]) ).
thf(126,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( A @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[46,105]) ).
thf(146,plain,
! [A: $i] :
( ( A != a )
| ( one != b )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( A @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[126]) ).
thf(150,plain,
( ( one != b )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( a @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[146]) ).
thf(4378,plain,
( ( ( zero @ ( a @ ( a @ multiplication ) @ leq ) )
!= ( one @ star @ ( one @ leq ) ) )
| ( one != b )
| ( ( sigma @ star )
!= zero )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4339,150]) ).
thf(4379,plain,
( ( ( zero @ ( a @ ( a @ multiplication ) @ leq ) )
!= ( one @ star @ ( one @ leq ) ) )
| ( one != b )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[4378]) ).
thf(4383,plain,
( ( ( one @ star )
!= zero )
| ( ( a @ ( a @ multiplication ) )
!= one )
| ( one != b )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[4379]) ).
thf(16,axiom,
! [A: $i] : ( A @ star @ ( A @ star @ ( A @ multiplication ) @ ( one @ addition ) @ leq ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',star_unfold_right) ).
thf(57,plain,
! [A: $i] : ( A @ star @ ( A @ star @ ( A @ multiplication ) @ ( one @ addition ) @ leq ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(50051,plain,
! [A: $i] :
( ( ( A @ ( sigma @ addition ) )
!= ( b @ ( sigma @ addition ) ) )
| ( ( A @ ( b @ addition ) @ ( a @ addition ) @ ( sigma @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[161,49828]) ).
thf(50052,plain,
( ( b @ ( b @ addition ) @ ( a @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[50051:[bind(A,$thf( b ))]]) ).
thf(67626,plain,
( ( b @ ( b @ addition ) @ ( a @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[50052,161]) ).
thf(67948,plain,
! [A: $i] :
( ( ( b @ ( b @ addition ) @ ( a @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
!= ( A @ ( b @ addition ) @ ( a @ addition ) ) )
| ( ( sigma @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[67626,298]) ).
thf(67949,plain,
( ( sigma @ ( b @ ( b @ addition ) @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[67948:[bind(A,$thf( b @ ( b @ addition ) @ ( a @ addition ) ))]]) ).
thf(93820,plain,
( ( sigma @ ( b @ ( b @ addition ) @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[67949,23]) ).
thf(96665,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
!= ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) ) )
| ( C != sigma )
| ( one != a )
| ( ( B @ ( A @ multiplication ) )
!= one ) ),
inference(paramod_ordered,[status(thm)],[597,81749]) ).
thf(96666,plain,
( ( sigma != sigma )
| ( one != a )
| ( ( a @ ( sigma @ star @ multiplication ) )
!= one ) ),
inference(pattern_uni,[status(thm)],[96665:[bind(A,$thf( sigma @ star )),bind(B,$thf( a )),bind(C,$thf( sigma ))]]) ).
thf(96711,plain,
( ( one != a )
| ( ( a @ ( sigma @ star @ multiplication ) )
!= one ) ),
inference(simp,[status(thm)],[96666]) ).
thf(178,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[49,105]) ).
thf(202,plain,
! [A: $i] :
( ( ( a @ ( b @ multiplication ) )
!= one )
| ( A != a )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[178]) ).
thf(211,plain,
( ( ( a @ ( b @ multiplication ) )
!= one )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( a @ leq ) ) ),
inference(simp,[status(thm)],[202]) ).
thf(5096,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( A @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[49,5081]) ).
thf(5130,plain,
! [A: $i] :
( ( one != a )
| ( A != b )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( A @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[5096]) ).
thf(5145,plain,
( ( one != a )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( b @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[5130]) ).
thf(42651,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( b @ ( a @ multiplication ) ) )
| ( one != a )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[46,5145]) ).
thf(42696,plain,
! [A: $i] :
( ( A != b )
| ( one != a )
| ( one != a )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[42651]) ).
thf(42703,plain,
( ( one != a )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( b @ leq ) ) ),
inference(simp,[status(thm)],[42696]) ).
thf(545,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( b @ ( a @ multiplication ) ) )
| ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[38,208]) ).
thf(587,plain,
! [C: $i,B: $i,A: $i] :
( ( C != b )
| ( ( B @ ( A @ multiplication ) )
!= a )
| ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[545]) ).
thf(602,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= a )
| ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( b @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[587]) ).
thf(18,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ addition ) @ ( A @ multiplication ) )
= ( C @ ( A @ multiplication ) @ ( B @ ( A @ multiplication ) @ addition ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_distributivity) ).
thf(61,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)],[18]) ).
thf(220,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)],[26,23]) ).
thf(221,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) @ ( A @ addition ) )
= ( B @ ( A @ addition ) ) ),
inference(pattern_uni,[status(thm)],[220:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( A ))]]) ).
thf(40678,plain,
( ( sigma != sigma )
| ( one != a )
| ( ( b @ star )
!= zero )
| ~ ( zero @ ( b @ leq ) )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[360,444]) ).
thf(40679,plain,
( ( one != a )
| ( ( b @ star )
!= zero )
| ~ ( zero @ ( b @ leq ) )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[40678:[]]) ).
thf(3851,plain,
! [A: $i] :
( ( ( zero @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) )
| ( zero != zero ) ),
inference(paramod_ordered,[status(thm)],[54,3836]) ).
thf(3852,plain,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) ),
inference(simp,[status(thm)],[3851]) ).
thf(3858,plain,
! [A: $i] :
( ( ( a @ ( b @ multiplication ) )
!= zero )
| ( A != a ) ),
inference(simp,[status(thm)],[3852]) ).
thf(3870,plain,
( ( a @ ( b @ multiplication ) )
!= zero ),
inference(simp,[status(thm)],[3858]) ).
thf(243,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( D @ ( sigma @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
= ( D @ ( b @ addition ) @ ( a @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[23,161]) ).
thf(244,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A != D )
| ( ( B @ ( C @ addition ) )
!= sigma )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
= ( D @ ( b @ addition ) @ ( a @ addition ) ) ) ),
inference(simp,[status(thm)],[243]) ).
thf(248,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= sigma )
| ( ( C @ ( A @ addition ) @ ( B @ addition ) )
= ( C @ ( b @ addition ) @ ( a @ addition ) ) ) ),
inference(simp,[status(thm)],[244]) ).
thf(17,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ ( B @ ( A @ multiplication ) @ addition ) @ leq ) )
=> ( B @ ( C @ ( A @ star @ multiplication ) @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',star_induction_left) ).
thf(59,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)],[17]) ).
thf(60,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( A @ star @ multiplication ) @ leq ) )
| ~ ( B @ ( C @ ( B @ ( A @ multiplication ) @ addition ) @ leq ) ) ),
inference(cnf,[status(esa)],[59]) ).
thf(28763,plain,
( ( ( zero @ ( a @ ( a @ multiplication ) @ leq ) )
!= ( zero @ star @ ( one @ leq ) ) )
| ( one != b )
| ( zero != sigma )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1248,13287]) ).
thf(28764,plain,
( ( ( zero @ ( a @ ( a @ multiplication ) @ leq ) )
!= ( zero @ star @ ( one @ leq ) ) )
| ( one != b )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[28763]) ).
thf(28772,plain,
( ( ( zero @ star )
!= zero )
| ( ( a @ ( a @ multiplication ) )
!= one )
| ( one != b )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[28764]) ).
thf(115,plain,
! [A: $i] :
( ( ( zero @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( zero @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[54,105]) ).
thf(119,plain,
! [A: $i] :
( ( ( a @ ( b @ multiplication ) )
!= zero )
| ( A != a )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( zero @ leq ) ) ),
inference(simp,[status(thm)],[115]) ).
thf(123,plain,
( ( ( a @ ( b @ multiplication ) )
!= zero )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( zero @ leq ) ) ),
inference(simp,[status(thm)],[119]) ).
thf(550,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
!= zero )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( zero @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[38,123]) ).
thf(576,plain,
! [C: $i,B: $i,A: $i] :
( ( C != a )
| ( ( B @ ( A @ multiplication ) )
!= b )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
!= zero )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( zero @ leq ) ) ),
inference(simp,[status(thm)],[550]) ).
thf(591,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= b )
| ( ( a @ ( B @ multiplication ) @ ( A @ multiplication ) )
!= zero )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( zero @ leq ) ) ),
inference(simp,[status(thm)],[576]) ).
thf(78558,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= b )
| ( ( a @ ( B @ multiplication ) @ ( A @ multiplication ) )
!= zero )
| ( ( sigma @ star )
!= zero )
| ~ $true ),
inference(rewrite,[status(thm)],[591,3119]) ).
thf(78559,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= b )
| ( ( a @ ( B @ multiplication ) @ ( A @ multiplication ) )
!= zero )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[78558]) ).
thf(5097,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[49,5081]) ).
thf(5124,plain,
! [A: $i] :
( ( ( a @ ( b @ multiplication ) )
!= one )
| ( A != a )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[5097]) ).
thf(5142,plain,
( ( ( a @ ( b @ multiplication ) )
!= one )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( a @ leq ) ) ),
inference(simp,[status(thm)],[5124]) ).
thf(1631,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[1472,32]) ).
thf(1632,plain,
( ( a @ ( sigma @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[1631:[bind(A,$thf( a )),bind(B,$thf( sigma ))]]) ).
thf(1783,plain,
( ( a @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[1632,161]) ).
thf(866,plain,
! [B: $i,A: $i] :
( ( ( b @ ( sigma @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[839,32]) ).
thf(867,plain,
( ( a @ ( b @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[866:[bind(A,$thf( a )),bind(B,$thf( b @ ( sigma @ addition ) ))]]) ).
thf(1047,plain,
( ( a @ ( b @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[867,23]) ).
thf(66225,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ addition ) )
!= ( A @ ( B @ addition ) ) )
| ( sigma != sigma )
| ( ( a @ ( A @ addition ) @ ( B @ addition ) @ ( b @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[56,508]) ).
thf(66226,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ addition ) )
!= ( A @ ( B @ addition ) ) )
| ( ( a @ ( A @ addition ) @ ( B @ addition ) @ ( b @ addition ) )
= sigma ) ),
inference(simp,[status(thm)],[66225]) ).
thf(66227,plain,
( ( a @ ( b @ addition ) @ ( a @ addition ) @ ( b @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[66226:[bind(A,$thf( b )),bind(B,$thf( a ))]]) ).
thf(87088,plain,
( ( a @ ( b @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[66227,39895]) ).
thf(544,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[38,156]) ).
thf(583,plain,
! [C: $i,B: $i,A: $i] :
( ( C != a )
| ( ( B @ ( A @ multiplication ) )
!= b )
| ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[544]) ).
thf(598,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= b )
| ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( a @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[583]) ).
thf(402,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( sigma @ ( b @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) @ ( a @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[23,237]) ).
thf(407,plain,
! [C: $i,B: $i,A: $i] :
( ( A != sigma )
| ( ( B @ ( C @ addition ) )
!= b )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) @ ( a @ addition ) )
= sigma ) ),
inference(simp,[status(thm)],[402]) ).
thf(424,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= b )
| ( ( sigma @ ( A @ addition ) @ ( B @ addition ) @ ( a @ addition ) )
= sigma ) ),
inference(simp,[status(thm)],[407]) ).
thf(21978,plain,
( ( sigma != sigma )
| ( one != a )
| ( ( a @ star )
!= zero )
| ~ ( zero @ ( b @ leq ) )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[226,444]) ).
thf(21979,plain,
( ( one != a )
| ( ( a @ star )
!= zero )
| ~ ( zero @ ( b @ leq ) )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[21978:[]]) ).
thf(82097,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( sigma @ ( sigma @ star @ multiplication ) ) )
| ( A != b )
| ( one != a ) ),
inference(paramod_ordered,[status(thm)],[49,81970]) ).
thf(82109,plain,
( ( one != sigma )
| ( ( sigma @ star )
!= b )
| ( one != a ) ),
inference(simp,[status(thm)],[82097]) ).
thf(82095,plain,
( ( sigma != sigma )
| ( ( b @ ( sigma @ star @ multiplication ) )
!= b )
| ( one != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[360,81970]) ).
thf(82096,plain,
( ( ( b @ ( sigma @ star @ multiplication ) )
!= b )
| ( one != a )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[82095:[]]) ).
thf(4360,plain,
( ( ( one @ star @ ( one @ leq ) )
!= ( zero @ ( a @ leq ) ) )
| ( ( a @ ( b @ multiplication ) )
!= one )
| ( ( sigma @ star )
!= zero )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4339,211]) ).
thf(4361,plain,
( ( ( one @ star @ ( one @ leq ) )
!= ( zero @ ( a @ leq ) ) )
| ( ( a @ ( b @ multiplication ) )
!= one )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[4360]) ).
thf(4385,plain,
( ( ( one @ star )
!= zero )
| ( one != a )
| ( ( a @ ( b @ multiplication ) )
!= one )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[4361]) ).
thf(43702,plain,
( ( ( zero @ star @ ( one @ leq ) )
!= ( zero @ ( b @ leq ) ) )
| ( one != a )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1248,42703]) ).
thf(43703,plain,
( ( ( zero @ star @ ( one @ leq ) )
!= ( zero @ ( b @ leq ) ) )
| ( one != a )
| ( ( a @ ( sigma @ multiplication ) )
!= zero ) ),
inference(simp,[status(thm)],[43702]) ).
thf(43709,plain,
( ( ( zero @ star )
!= zero )
| ( one != b )
| ( one != a )
| ( ( a @ ( sigma @ multiplication ) )
!= zero ) ),
inference(simp,[status(thm)],[43703]) ).
thf(132,plain,
! [B: $i,A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( B @ ( zero @ multiplication ) ) )
| ( A = zero ) ),
inference(paramod_ordered,[status(thm)],[46,35]) ).
thf(144,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( one != zero )
| ( A = zero ) ),
inference(simp,[status(thm)],[132]) ).
thf(148,plain,
! [A: $i] :
( ( one != zero )
| ( A = zero ) ),
inference(simp,[status(thm)],[144]) ).
thf(6322,plain,
! [A: $i] :
( ( A
!= ( a @ ( b @ multiplication ) ) )
| ( zero != zero )
| ( one != zero ) ),
inference(paramod_ordered,[status(thm)],[148,3870]) ).
thf(6323,plain,
! [A: $i] :
( ( A
!= ( a @ ( b @ multiplication ) ) )
| ( one != zero ) ),
inference(simp,[status(thm)],[6322]) ).
thf(6324,plain,
one != zero,
inference(pattern_uni,[status(thm)],[6323:[bind(A,$thf( a @ ( b @ multiplication ) ))]]) ).
thf(9813,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( a @ ( b @ addition ) ) )
| ( ( sigma @ ( A @ ( B @ addition ) @ addition ) @ ( a @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[32,9681]) ).
thf(9814,plain,
( ( sigma @ ( b @ ( a @ addition ) @ addition ) @ ( a @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[9813:[bind(A,$thf( b )),bind(B,$thf( a ))]]) ).
thf(10585,plain,
( ( sigma @ ( b @ addition ) @ ( a @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[9814,23]) ).
thf(10721,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( b @ addition ) @ ( a @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[10585,32]) ).
thf(10722,plain,
( ( a @ ( sigma @ ( b @ addition ) @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[10721:[bind(A,$thf( a )),bind(B,$thf( sigma @ ( b @ addition ) @ ( a @ addition ) ))]]) ).
thf(13332,plain,
( ( a @ ( sigma @ ( b @ addition ) @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[10722,23]) ).
thf(13509,plain,
! [B: $i,A: $i] :
( ( ( a @ ( sigma @ ( b @ addition ) @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[13332,32]) ).
thf(13510,plain,
( ( a @ ( a @ ( sigma @ ( b @ addition ) @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[13509:[bind(A,$thf( a )),bind(B,$thf( a @ ( sigma @ ( b @ addition ) @ addition ) ))]]) ).
thf(17095,plain,
( ( a @ ( a @ addition ) @ ( sigma @ ( b @ addition ) @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[13510,23]) ).
thf(17278,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ addition ) @ ( sigma @ ( b @ addition ) @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[17095,32]) ).
thf(17279,plain,
( ( sigma @ ( b @ addition ) @ ( a @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[17278:[bind(A,$thf( sigma @ ( b @ addition ) )),bind(B,$thf( a @ ( a @ addition ) ))]]) ).
thf(21312,plain,
( ( sigma @ ( b @ addition ) @ ( a @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[17279,23]) ).
thf(21490,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( b @ addition ) @ ( a @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[21312,32]) ).
thf(21491,plain,
( ( a @ ( sigma @ ( b @ addition ) @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[21490:[bind(A,$thf( a )),bind(B,$thf( sigma @ ( b @ addition ) @ ( a @ addition ) ))]]) ).
thf(30832,plain,
( ( a @ ( sigma @ ( b @ addition ) @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[21491,23]) ).
thf(81981,plain,
( ( sigma != sigma )
| ( ( sigma @ ( a @ star @ multiplication ) )
!= sigma )
| ( one != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[226,81965]) ).
thf(81982,plain,
( ( ( sigma @ ( a @ star @ multiplication ) )
!= sigma )
| ( one != a )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[81981:[]]) ).
thf(555,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) ) )
| ~ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[38,20]) ).
thf(575,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( a @ ( sigma @ multiplication ) ) )
| ( ( B @ ( A @ multiplication ) )
!= a )
| ~ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[555]) ).
thf(615,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= a )
| ~ ( a @ ( sigma @ multiplication ) @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[575]) ).
thf(561,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[38,105]) ).
thf(578,plain,
! [C: $i,B: $i,A: $i] :
( ( C != a )
| ( ( B @ ( A @ multiplication ) )
!= b )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[561]) ).
thf(593,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= b )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( a @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[578]) ).
thf(398,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( sigma @ ( b @ addition ) @ ( a @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[237,23]) ).
thf(406,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sigma @ ( b @ addition ) ) )
| ( ( B @ ( C @ addition ) )
!= a )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
= sigma ) ),
inference(simp,[status(thm)],[398]) ).
thf(423,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= a )
| ( ( sigma @ ( b @ addition ) @ ( A @ addition ) @ ( B @ addition ) )
= sigma ) ),
inference(simp,[status(thm)],[406]) ).
thf(52293,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= a )
| ( ( sigma @ ( A @ addition ) @ ( B @ addition ) )
= sigma ) ),
inference(rewrite,[status(thm)],[423,1596]) ).
thf(484,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ ( sigma @ addition ) @ ( b @ addition ) )
!= ( B @ ( C @ addition ) ) )
| ( ( A @ ( sigma @ addition ) )
= ( A @ ( B @ addition ) @ ( C @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[445,23]) ).
thf(485,plain,
! [A: $i] :
( ( A @ ( sigma @ addition ) )
= ( A @ ( a @ ( sigma @ addition ) @ addition ) @ ( b @ addition ) ) ),
inference(pattern_uni,[status(thm)],[484:[bind(A,$thf( A )),bind(B,$thf( a @ ( sigma @ addition ) )),bind(C,$thf( b ))]]) ).
thf(60667,plain,
! [A: $i] :
( ( A @ ( a @ addition ) @ ( sigma @ addition ) @ ( b @ addition ) )
= ( A @ ( b @ addition ) @ ( a @ addition ) ) ),
inference(rewrite,[status(thm)],[485,161,11061]) ).
thf(1827,plain,
! [B: $i,A: $i] :
( ( ( a @ ( b @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[1783,32]) ).
thf(1828,plain,
( ( a @ ( a @ ( b @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[1827:[bind(A,$thf( a )),bind(B,$thf( a @ ( b @ addition ) ))]]) ).
thf(2302,plain,
( ( a @ ( a @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[1828,23]) ).
thf(5443,plain,
! [A: $i] :
( ( ( a @ ( a @ addition ) @ ( b @ addition ) )
!= ( A @ ( b @ addition ) ) )
| ( ( sigma @ ( a @ addition ) )
= ( sigma @ ( A @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[2302,298]) ).
thf(5444,plain,
( ( sigma @ ( a @ ( a @ addition ) @ addition ) )
= ( sigma @ ( a @ addition ) ) ),
inference(pattern_uni,[status(thm)],[5443:[bind(A,$thf( a @ ( a @ addition ) ))]]) ).
thf(7501,plain,
( ( sigma @ ( a @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[5444,1472,23]) ).
thf(7582,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( a @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[7501,32]) ).
thf(7583,plain,
( ( a @ ( sigma @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[7582:[bind(A,$thf( a )),bind(B,$thf( sigma @ ( a @ addition ) ))]]) ).
thf(7806,plain,
( ( a @ ( sigma @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[7583,23]) ).
thf(10262,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( a @ ( sigma @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( a @ ( b @ addition ) @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[32,10131]) ).
thf(10263,plain,
( ( sigma @ ( a @ addition ) @ ( a @ ( b @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[10262:[bind(A,$thf( sigma )),bind(B,$thf( a ))]]) ).
thf(12201,plain,
( ( sigma @ ( a @ addition ) @ ( a @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[10263,23]) ).
thf(12360,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( a @ addition ) @ ( a @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[12201,32]) ).
thf(12361,plain,
( ( b @ ( sigma @ ( a @ addition ) @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[12360:[bind(A,$thf( b )),bind(B,$thf( sigma @ ( a @ addition ) @ ( a @ addition ) ))]]) ).
thf(15807,plain,
( ( b @ ( sigma @ ( a @ addition ) @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[12361,23]) ).
thf(15997,plain,
! [B: $i,A: $i] :
( ( ( b @ ( sigma @ ( a @ addition ) @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[15807,32]) ).
thf(15998,plain,
( ( a @ ( b @ ( sigma @ ( a @ addition ) @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[15997:[bind(A,$thf( a )),bind(B,$thf( b @ ( sigma @ ( a @ addition ) @ addition ) ))]]) ).
thf(18488,plain,
( ( a @ ( b @ addition ) @ ( sigma @ ( a @ addition ) @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[15998,23]) ).
thf(18677,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( a @ ( b @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( sigma @ ( a @ addition ) @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[32,18488]) ).
thf(18678,plain,
( ( b @ ( a @ addition ) @ ( sigma @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[18677:[bind(A,$thf( b )),bind(B,$thf( a ))]]) ).
thf(24537,plain,
( ( b @ ( a @ addition ) @ ( sigma @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[18678,23]) ).
thf(4374,plain,
( ( ( zero @ ( b @ ( a @ multiplication ) @ leq ) )
!= ( one @ star @ ( one @ leq ) ) )
| ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4339,208]) ).
thf(4375,plain,
( ( ( zero @ ( b @ ( a @ multiplication ) @ leq ) )
!= ( one @ star @ ( one @ leq ) ) )
| ( one != a )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[4374]) ).
thf(4384,plain,
( ( ( one @ star )
!= zero )
| ( ( b @ ( a @ multiplication ) )
!= one )
| ( one != a )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[4375]) ).
thf(5092,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[46,5081]) ).
thf(5138,plain,
! [A: $i] :
( ( A
!= ( a @ ( b @ multiplication ) ) )
| ( one != a )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[5092]) ).
thf(5149,plain,
( ( one != a )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( a @ ( b @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[5138]) ).
thf(10,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ addition ) @ multiplication ) )
= ( C @ ( B @ multiplication ) @ ( C @ ( A @ multiplication ) @ addition ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_distributivity) ).
thf(41,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(34143,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ addition ) @ ( B @ addition ) )
!= ( a @ ( sigma @ addition ) @ ( a @ ( b @ addition ) @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[33798,10131]) ).
thf(34144,plain,
( ( a @ ( a @ ( b @ addition ) @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[34143:[bind(A,$thf( sigma )),bind(B,$thf( a @ ( b @ addition ) )),bind(C,$thf( a ))]]) ).
thf(40775,plain,
( ( a @ ( a @ ( b @ addition ) @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[34144,161]) ).
thf(241,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( sigma @ addition ) )
!= ( C @ ( D @ addition ) ) )
| ( ( B @ ( A @ ( b @ addition ) @ ( a @ addition ) @ addition ) )
= ( B @ ( C @ addition ) @ ( D @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[161,23]) ).
thf(242,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( b @ addition ) @ ( a @ addition ) @ addition ) )
= ( B @ ( A @ addition ) @ ( sigma @ addition ) ) ),
inference(pattern_uni,[status(thm)],[241:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( sigma ))]]) ).
thf(25175,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( b @ addition ) @ addition ) @ ( a @ addition ) )
= ( B @ ( A @ addition ) @ ( b @ addition ) @ ( a @ addition ) ) ),
inference(rewrite,[status(thm)],[242,161,23]) ).
thf(40998,plain,
! [A: $i] :
( ( ( a @ ( a @ ( b @ addition ) @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
!= ( A @ ( b @ addition ) @ ( a @ addition ) ) )
| ( ( sigma @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[40775,298]) ).
thf(40999,plain,
( ( sigma @ ( a @ ( a @ ( b @ addition ) @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[40998:[bind(A,$thf( a @ ( a @ ( b @ addition ) @ addition ) ))]]) ).
thf(55673,plain,
( ( sigma @ ( a @ addition ) @ ( a @ ( b @ addition ) @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[40999,23]) ).
thf(56099,plain,
( ( ( sigma @ ( a @ addition ) )
!= ( sigma @ ( a @ addition ) ) )
| ( ( sigma @ ( a @ ( b @ addition ) @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[1472,55673]) ).
thf(56100,plain,
( ( sigma @ ( a @ ( b @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[56099:[]]) ).
thf(56643,plain,
( ( sigma @ ( a @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[56100,23]) ).
thf(82100,plain,
( ( sigma != sigma )
| ( ( sigma @ ( a @ star @ multiplication ) )
!= b )
| ( one != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[226,81970]) ).
thf(82101,plain,
( ( ( sigma @ ( a @ star @ multiplication ) )
!= b )
| ( one != a )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[82100:[]]) ).
thf(82087,plain,
( ( sigma != sigma )
| ( ( b @ star )
!= one )
| ( one != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[360,81998]) ).
thf(82088,plain,
( ( ( b @ star )
!= one )
| ( one != a )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[82087:[]]) ).
thf(81930,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( sigma @ ( sigma @ star @ multiplication ) ) )
| ( one != a )
| ~ ( A @ ( b @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[49,81752]) ).
thf(81955,plain,
! [A: $i] :
( ( one != sigma )
| ( A
!= ( sigma @ star ) )
| ( one != a )
| ~ ( A @ ( b @ leq ) ) ),
inference(simp,[status(thm)],[81930]) ).
thf(81963,plain,
( ( one != sigma )
| ( one != a )
| ~ ( sigma @ star @ ( b @ leq ) ) ),
inference(simp,[status(thm)],[81955]) ).
thf(1259,plain,
( ( ( zero @ ( a @ ( a @ multiplication ) @ leq ) )
!= ( zero @ star @ ( one @ leq ) ) )
| ( one != b )
| ( ( sigma @ star )
!= zero )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1248,150]) ).
thf(1260,plain,
( ( ( zero @ ( a @ ( a @ multiplication ) @ leq ) )
!= ( zero @ star @ ( one @ leq ) ) )
| ( one != b )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[1259]) ).
thf(1273,plain,
( ( ( zero @ star )
!= zero )
| ( ( a @ ( a @ multiplication ) )
!= one )
| ( one != b )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[1260]) ).
thf(562,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[38,105]) ).
thf(586,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( a @ ( b @ multiplication ) ) )
| ( ( B @ ( A @ multiplication ) )
!= a )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[562]) ).
thf(601,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= a )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( a @ ( b @ multiplication ) @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[586]) ).
thf(1255,plain,
( ( ( zero @ ( a @ ( b @ multiplication ) @ leq ) )
!= ( zero @ star @ ( one @ leq ) ) )
| ( one != a )
| ( ( sigma @ star )
!= zero )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1248,156]) ).
thf(1256,plain,
( ( ( zero @ ( a @ ( b @ multiplication ) @ leq ) )
!= ( zero @ star @ ( one @ leq ) ) )
| ( one != a )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[1255]) ).
thf(1278,plain,
( ( ( zero @ star )
!= zero )
| ( ( a @ ( b @ multiplication ) )
!= one )
| ( one != a )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[1256]) ).
thf(16604,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( a @ ( sigma @ addition ) ) )
| ( ( a @ ( A @ ( B @ addition ) @ addition ) @ ( b @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[32,16416]) ).
thf(16605,plain,
( ( a @ ( sigma @ ( a @ addition ) @ addition ) @ ( b @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[16604:[bind(A,$thf( sigma )),bind(B,$thf( a ))]]) ).
thf(20053,plain,
( ( a @ ( sigma @ addition ) @ ( a @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[16605,11061]) ).
thf(20248,plain,
! [B: $i,A: $i] :
( ( ( a @ ( sigma @ addition ) @ ( a @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[20053,32]) ).
thf(20249,plain,
( ( b @ ( a @ ( sigma @ addition ) @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[20248:[bind(A,$thf( b )),bind(B,$thf( a @ ( sigma @ addition ) @ ( a @ addition ) ))]]) ).
thf(28066,plain,
( ( b @ ( a @ ( sigma @ addition ) @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[20249,23]) ).
thf(36257,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ addition ) @ ( A @ addition ) )
!= ( a @ ( b @ addition ) @ ( a @ addition ) @ ( sigma @ addition ) ) )
| ( ( A @ ( C @ addition ) @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[323,11704]) ).
thf(36258,plain,
( ( sigma @ ( a @ ( b @ addition ) @ addition ) @ ( a @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[36257:[bind(A,$thf( sigma )),bind(B,$thf( a )),bind(C,$thf( a @ ( b @ addition ) ))]]) ).
thf(45448,plain,
( ( sigma @ ( a @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[36258,11061]) ).
thf(45783,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sigma @ ( a @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
!= ( C @ ( A @ addition ) @ ( B @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[45448,33798]) ).
thf(45784,plain,
( ( sigma @ ( a @ addition ) @ ( a @ addition ) @ ( b @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[45783:[bind(A,$thf( b )),bind(B,$thf( a )),bind(C,$thf( sigma @ ( a @ addition ) ))]]) ).
thf(61782,plain,
( ( sigma @ ( a @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[45784,39895]) ).
thf(184,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) ) )
| ~ ( A @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[49,20]) ).
thf(195,plain,
! [A: $i] :
( ( one != a )
| ( A != sigma )
| ~ ( A @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[184]) ).
thf(204,plain,
( ( one != a )
| ~ ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[195]) ).
thf(76573,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( sigma @ addition ) @ ( a @ addition ) @ ( b @ addition ) )
!= ( A @ ( C @ addition ) @ ( B @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[76143,323]) ).
thf(76574,plain,
( ( a @ ( b @ addition ) @ ( b @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[76573:[bind(A,$thf( b @ ( sigma @ addition ) )),bind(B,$thf( b )),bind(C,$thf( a ))]]) ).
thf(101652,plain,
( ( a @ ( b @ addition ) @ ( b @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[76574,23]) ).
thf(76446,plain,
! [B: $i,A: $i] :
( ( ( b @ ( sigma @ addition ) @ ( a @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[76143,32]) ).
thf(76447,plain,
( ( b @ ( b @ ( sigma @ addition ) @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[76446:[bind(A,$thf( b )),bind(B,$thf( b @ ( sigma @ addition ) @ ( a @ addition ) ))]]) ).
thf(100278,plain,
( ( b @ ( b @ ( sigma @ addition ) @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[76447,23]) ).
thf(50033,plain,
! [B: $i,A: $i] :
( ( ( b @ ( sigma @ addition ) @ ( sigma @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[49828,32]) ).
thf(50034,plain,
( ( sigma @ ( b @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[50033:[bind(A,$thf( sigma )),bind(B,$thf( b @ ( sigma @ addition ) ))]]) ).
thf(51493,plain,
( ( sigma @ ( b @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[50034,23]) ).
thf(92,plain,
! [A: $i] :
( ( ( A @ ( zero @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) ) )
| ~ ( zero @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[35,20]) ).
thf(99,plain,
! [A: $i] :
( ( A
!= ( a @ ( sigma @ multiplication ) ) )
| ( zero != a )
| ~ ( zero @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[92]) ).
thf(107,plain,
( ( zero != a )
| ~ ( zero @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[99]) ).
thf(2642,plain,
( ( zero != a )
| ~ ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(rewrite,[status(thm)],[107,54]) ).
thf(2656,plain,
! [A: $i] :
( ( ( A @ ( zero @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) )
| ( zero != a )
| ~ ( zero @ ( zero @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[35,2642]) ).
thf(2668,plain,
! [A: $i] :
( ( A
!= ( a @ ( b @ multiplication ) ) )
| ( zero != a )
| ( zero != a )
| ~ ( zero @ ( zero @ leq ) ) ),
inference(simp,[status(thm)],[2656]) ).
thf(2681,plain,
( ( zero != a )
| ~ ( zero @ ( zero @ leq ) ) ),
inference(simp,[status(thm)],[2668]) ).
thf(3077,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ addition ) )
!= ( C @ ( B @ addition ) ) )
| ( C @ ( B @ leq ) )
| ( A != C ) ),
inference(paramod_ordered,[status(thm)],[29,71]) ).
thf(3078,plain,
! [A: $i] :
( ( zero @ ( A @ leq ) )
| ( A != zero ) ),
inference(pattern_uni,[status(thm)],[3077:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( zero ))]]) ).
thf(3114,plain,
zero @ ( zero @ leq ),
inference(simp,[status(thm)],[3078]) ).
thf(3122,plain,
( ( zero != a )
| ~ $true ),
inference(rewrite,[status(thm)],[2681,3114]) ).
thf(3123,plain,
zero != a,
inference(simp,[status(thm)],[3122]) ).
thf(465,plain,
! [B: $i,A: $i] :
( ( ( a @ ( sigma @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[445,32]) ).
thf(466,plain,
( ( b @ ( a @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[465:[bind(A,$thf( b )),bind(B,$thf( a @ ( sigma @ addition ) ))]]) ).
thf(617,plain,
( ( b @ ( a @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[466,23]) ).
thf(662,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( a @ addition ) @ ( sigma @ addition ) )
!= ( B @ ( C @ addition ) ) )
| ( ( A @ ( sigma @ addition ) )
= ( A @ ( B @ addition ) @ ( C @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[617,23]) ).
thf(663,plain,
! [A: $i] :
( ( A @ ( b @ ( a @ addition ) @ addition ) @ ( sigma @ addition ) )
= ( A @ ( sigma @ addition ) ) ),
inference(pattern_uni,[status(thm)],[662:[bind(A,$thf( A )),bind(B,$thf( b @ ( a @ addition ) )),bind(C,$thf( sigma ))]]) ).
thf(107625,plain,
! [A: $i] :
( ( A @ ( b @ addition ) @ ( a @ addition ) @ ( sigma @ addition ) )
= ( A @ ( b @ addition ) @ ( a @ addition ) ) ),
inference(rewrite,[status(thm)],[663,161,11061]) ).
thf(48495,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( a @ ( b @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( sigma @ ( b @ addition ) @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[32,48259]) ).
thf(48496,plain,
( ( b @ ( a @ addition ) @ ( sigma @ ( b @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[48495:[bind(A,$thf( b )),bind(B,$thf( a ))]]) ).
thf(62829,plain,
( ( b @ ( a @ addition ) @ ( sigma @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[48496,23]) ).
thf(13300,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) )
| ( A != a )
| ( zero != sigma ) ),
inference(paramod_ordered,[status(thm)],[49,13279]) ).
thf(13314,plain,
( ( ( a @ ( b @ multiplication ) )
!= one )
| ( a != a )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[13300]) ).
thf(13319,plain,
( ( ( a @ ( b @ multiplication ) )
!= one )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[13314]) ).
thf(24720,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ addition ) @ ( sigma @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[24537,32]) ).
thf(24721,plain,
( ( a @ ( b @ ( a @ addition ) @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[24720:[bind(A,$thf( a )),bind(B,$thf( b @ ( a @ addition ) @ ( sigma @ addition ) ))]]) ).
thf(33049,plain,
( ( a @ ( b @ ( a @ addition ) @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[24721,23]) ).
thf(28272,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ ( sigma @ addition ) @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[28066,32]) ).
thf(28273,plain,
( ( a @ ( b @ ( a @ ( sigma @ addition ) @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[28272:[bind(A,$thf( a )),bind(B,$thf( b @ ( a @ ( sigma @ addition ) @ addition ) ))]]) ).
thf(35148,plain,
( ( a @ ( b @ addition ) @ ( a @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[28273,23]) ).
thf(58819,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( sigma @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
!= ( A @ ( C @ addition ) @ ( B @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[58450,323]) ).
thf(58820,plain,
( ( b @ ( a @ addition ) @ ( b @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[58819:[bind(A,$thf( b @ ( sigma @ addition ) )),bind(B,$thf( a )),bind(C,$thf( b ))]]) ).
thf(78611,plain,
( ( b @ ( a @ addition ) @ ( b @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[58820,23]) ).
thf(348,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( a @ ( b @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[284,23]) ).
thf(354,plain,
! [C: $i,B: $i,A: $i] :
( ( A != a )
| ( ( B @ ( C @ addition ) )
!= b )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
= sigma ) ),
inference(simp,[status(thm)],[348]) ).
thf(362,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= b )
| ( ( a @ ( A @ addition ) @ ( B @ addition ) )
= sigma ) ),
inference(simp,[status(thm)],[354]) ).
thf(81693,plain,
! [A: $i] :
( ( ( A @ ( A @ leq ) )
!= ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( b @ leq ) ) )
| ( one != a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3119,79904]) ).
thf(81694,plain,
! [A: $i] :
( ( ( A @ ( A @ leq ) )
!= ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( b @ leq ) ) )
| ( one != a ) ),
inference(simp,[status(thm)],[81693]) ).
thf(81729,plain,
! [A: $i] :
( ( A
!= ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) ) )
| ( A != b )
| ( one != a ) ),
inference(simp,[status(thm)],[81694]) ).
thf(81743,plain,
( ( ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) )
!= b )
| ( one != a ) ),
inference(simp,[status(thm)],[81729]) ).
thf(90674,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( sigma @ ( a @ multiplication ) ) )
| ( ( A @ ( sigma @ star @ multiplication ) )
!= b )
| ( one != a ) ),
inference(paramod_ordered,[status(thm)],[49,81743]) ).
thf(90689,plain,
! [A: $i] :
( ( one != sigma )
| ( A != a )
| ( ( A @ ( sigma @ star @ multiplication ) )
!= b )
| ( one != a ) ),
inference(simp,[status(thm)],[90674]) ).
thf(90700,plain,
( ( one != sigma )
| ( ( a @ ( sigma @ star @ multiplication ) )
!= b )
| ( one != a ) ),
inference(simp,[status(thm)],[90689]) ).
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/sandbox2/benchmark/theBenchmark.p',star_induction_right) ).
thf(39,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(556,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[38,20]) ).
thf(584,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( a @ ( b @ multiplication ) ) )
| ( ( B @ ( A @ multiplication ) )
!= a )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[556]) ).
thf(599,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= a )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[584]) ).
thf(7893,plain,
! [B: $i,A: $i] :
( ( ( a @ ( sigma @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[7806,32]) ).
thf(7894,plain,
( ( a @ ( a @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[7893:[bind(A,$thf( a )),bind(B,$thf( a @ ( sigma @ addition ) ))]]) ).
thf(8120,plain,
( ( a @ ( a @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[7894,23]) ).
thf(70424,plain,
! [B: $i,A: $i] :
( ( ( b @ ( b @ ( a @ addition ) @ addition ) @ ( sigma @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[70143,32]) ).
thf(70425,plain,
( ( sigma @ ( b @ ( b @ ( a @ addition ) @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[70424:[bind(A,$thf( sigma )),bind(B,$thf( b @ ( b @ ( a @ addition ) @ addition ) ))]]) ).
thf(96714,plain,
( ( sigma @ ( b @ addition ) @ ( b @ ( a @ addition ) @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[70425,23]) ).
thf(22230,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( a @ ( sigma @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( b @ ( a @ addition ) @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[32,22047]) ).
thf(22231,plain,
( ( sigma @ ( a @ addition ) @ ( b @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[22230:[bind(A,$thf( sigma )),bind(B,$thf( a ))]]) ).
thf(31546,plain,
( ( sigma @ ( a @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[22231,23]) ).
thf(31771,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( a @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[31546,32]) ).
thf(31772,plain,
( ( a @ ( sigma @ ( a @ addition ) @ ( b @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[31771:[bind(A,$thf( a )),bind(B,$thf( sigma @ ( a @ addition ) @ ( b @ addition ) ))]]) ).
thf(37381,plain,
( ( a @ ( sigma @ ( a @ addition ) @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[31772,23]) ).
thf(37620,plain,
! [B: $i,A: $i] :
( ( ( a @ ( sigma @ ( a @ addition ) @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[37381,32]) ).
thf(37621,plain,
( ( b @ ( a @ ( sigma @ ( a @ addition ) @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[37620:[bind(A,$thf( b )),bind(B,$thf( a @ ( sigma @ ( a @ addition ) @ addition ) ))]]) ).
thf(47315,plain,
( ( b @ ( a @ addition ) @ ( sigma @ ( a @ addition ) @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[37621,23]) ).
thf(49303,plain,
! [A: $i] :
( ( ( sigma @ ( sigma @ addition ) @ ( b @ addition ) )
!= ( A @ ( b @ addition ) ) )
| ( ( sigma @ ( a @ addition ) )
= ( sigma @ ( A @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[49117,298]) ).
thf(49304,plain,
( ( sigma @ ( sigma @ ( sigma @ addition ) @ addition ) )
= ( sigma @ ( a @ addition ) ) ),
inference(pattern_uni,[status(thm)],[49303:[bind(A,$thf( sigma @ ( sigma @ addition ) ))]]) ).
thf(65276,plain,
( ( sigma @ ( sigma @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[49304,1472,23]) ).
thf(65517,plain,
! [A: $i] :
( ( ( sigma @ ( A @ addition ) )
!= ( sigma @ ( sigma @ addition ) ) )
| ( ( A @ ( b @ addition ) @ ( a @ addition ) @ ( sigma @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[298,65276]) ).
thf(65518,plain,
( ( sigma @ ( b @ addition ) @ ( a @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[65517:[bind(A,$thf( sigma ))]]) ).
thf(85401,plain,
( ( sigma @ ( b @ addition ) @ ( a @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[65518,161]) ).
thf(135,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) ) )
| ~ ( A @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[46,20]) ).
thf(142,plain,
! [A: $i] :
( ( A != a )
| ( one != sigma )
| ~ ( A @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[135]) ).
thf(155,plain,
( ( one != sigma )
| ~ ( a @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[142]) ).
thf(57741,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ ( b @ addition ) @ addition ) @ ( sigma @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[57470,32]) ).
thf(57742,plain,
( ( sigma @ ( b @ ( a @ ( b @ addition ) @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[57741:[bind(A,$thf( sigma )),bind(B,$thf( b @ ( a @ ( b @ addition ) @ addition ) ))]]) ).
thf(74966,plain,
( ( sigma @ ( b @ addition ) @ ( a @ ( b @ addition ) @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[57742,23]) ).
thf(554,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[38,20]) ).
thf(579,plain,
! [C: $i,B: $i,A: $i] :
( ( C != a )
| ( ( B @ ( A @ multiplication ) )
!= b )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[554]) ).
thf(594,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= b )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[579]) ).
thf(270,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( a @ ( a @ multiplication ) ) )
| ( one != b )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[46,150]) ).
thf(274,plain,
! [A: $i] :
( ( A != a )
| ( one != a )
| ( one != b )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[270]) ).
thf(278,plain,
( ( one != a )
| ( one != b )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( a @ leq ) ) ),
inference(simp,[status(thm)],[274]) ).
thf(4231,plain,
! [B: $i,A: $i] :
( ( ( one @ star @ ( one @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= ( one @ star ) ) ),
inference(paramod_ordered,[status(thm)],[4066,32]) ).
thf(4232,plain,
( ( one @ ( one @ star @ addition ) )
= ( one @ star ) ),
inference(pattern_uni,[status(thm)],[4231:[bind(A,$thf( one )),bind(B,$thf( one @ star ))]]) ).
thf(43822,plain,
( ( ( a @ ( b @ addition ) )
!= ( a @ ( b @ addition ) ) )
| ( ( sigma @ ( sigma @ addition ) @ ( b @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[284,43744]) ).
thf(43823,plain,
( ( sigma @ ( sigma @ addition ) @ ( b @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[43822:[]]) ).
thf(44551,plain,
( ( sigma @ ( b @ addition ) @ ( a @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[43823,161]) ).
thf(186,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) ) )
| ~ ( A @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[49,20]) ).
thf(200,plain,
! [A: $i] :
( ( ( a @ ( sigma @ multiplication ) )
!= one )
| ( A != a )
| ~ ( A @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[186]) ).
thf(209,plain,
( ( ( a @ ( sigma @ multiplication ) )
!= one )
| ~ ( a @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[200]) ).
thf(44068,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ ( b @ addition ) @ ( sigma @ addition ) @ ( b @ addition ) )
!= ( C @ ( A @ addition ) @ ( B @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[43744,33798]) ).
thf(44069,plain,
( ( a @ ( b @ addition ) @ ( b @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[44068:[bind(A,$thf( sigma )),bind(B,$thf( b )),bind(C,$thf( a @ ( b @ addition ) ))]]) ).
thf(59466,plain,
( ( a @ ( b @ addition ) @ ( b @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[44069,161]) ).
thf(43678,plain,
( ( ( one @ star @ ( one @ leq ) )
!= ( zero @ ( b @ leq ) ) )
| ( one != a )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4339,42703]) ).
thf(43679,plain,
( ( ( one @ star @ ( one @ leq ) )
!= ( zero @ ( b @ leq ) ) )
| ( one != a )
| ( ( a @ ( sigma @ multiplication ) )
!= zero ) ),
inference(simp,[status(thm)],[43678]) ).
thf(43714,plain,
( ( ( one @ star )
!= zero )
| ( one != b )
| ( one != a )
| ( ( a @ ( sigma @ multiplication ) )
!= zero ) ),
inference(simp,[status(thm)],[43679]) ).
thf(62,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ addition ) @ ( A @ multiplication ) )
= ( C @ ( A @ multiplication ) @ ( B @ ( A @ multiplication ) @ addition ) ) ),
inference(cnf,[status(esa)],[61]) ).
thf(63,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ multiplication ) @ ( B @ ( A @ multiplication ) @ addition ) )
= ( C @ ( B @ addition ) @ ( A @ multiplication ) ) ),
inference(lifteq,[status(thm)],[62]) ).
thf(82528,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) )
| ( C != a )
| ( zero != sigma )
| ( ( B @ ( A @ multiplication ) )
!= one ) ),
inference(paramod_ordered,[status(thm)],[597,13279]) ).
thf(82529,plain,
( ( a != a )
| ( zero != sigma )
| ( ( b @ ( a @ multiplication ) )
!= one ) ),
inference(pattern_uni,[status(thm)],[82528:[bind(A,$thf( a )),bind(B,$thf( b )),bind(C,$thf( a ))]]) ).
thf(82677,plain,
( ( zero != sigma )
| ( ( b @ ( a @ multiplication ) )
!= one ) ),
inference(simp,[status(thm)],[82529]) ).
thf(30822,plain,
( ( sigma != sigma )
| ( one != sigma )
| ( one != b )
| ( one != a )
| ( ( a @ star )
!= zero )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[226,30813]) ).
thf(30823,plain,
( ( one != sigma )
| ( one != b )
| ( one != a )
| ( ( a @ star )
!= zero )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[30822:[]]) ).
thf(33286,plain,
! [B: $i,A: $i] :
( ( ( a @ ( b @ ( a @ addition ) @ addition ) @ ( sigma @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[33049,32]) ).
thf(33287,plain,
( ( sigma @ ( a @ ( b @ ( a @ addition ) @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[33286:[bind(A,$thf( sigma )),bind(B,$thf( a @ ( b @ ( a @ addition ) @ addition ) ))]]) ).
thf(39036,plain,
( ( sigma @ ( a @ addition ) @ ( b @ ( a @ addition ) @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[33287,23]) ).
thf(64274,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ ( sigma @ addition ) @ ( b @ addition ) @ ( b @ addition ) )
!= ( A @ ( C @ addition ) @ ( B @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[63882,323]) ).
thf(64275,plain,
( ( b @ ( b @ addition ) @ ( a @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[64274:[bind(A,$thf( a @ ( sigma @ addition ) )),bind(B,$thf( b )),bind(C,$thf( b ))]]) ).
thf(84059,plain,
( ( b @ ( b @ addition ) @ ( a @ addition ) @ ( sigma @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[64275,23]) ).
thf(84551,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( b @ addition ) @ ( a @ addition ) @ ( sigma @ addition ) )
!= ( C @ ( A @ addition ) @ ( B @ addition ) ) )
| ( ( C @ ( B @ addition ) @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[84059,33798]) ).
thf(84552,plain,
( ( b @ ( b @ addition ) @ ( sigma @ addition ) @ ( a @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[84551:[bind(A,$thf( a )),bind(B,$thf( sigma )),bind(C,$thf( b @ ( b @ addition ) ))]]) ).
thf(109220,plain,
( ( b @ ( b @ addition ) @ ( b @ addition ) @ ( a @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[84552,161]) ).
thf(90673,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( sigma @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) ) )
| ( A != b )
| ( one != a ) ),
inference(paramod_ordered,[status(thm)],[49,81743]) ).
thf(90697,plain,
( ( ( sigma @ ( a @ multiplication ) )
!= one )
| ( ( sigma @ star )
!= b )
| ( one != a ) ),
inference(simp,[status(thm)],[90673]) ).
thf(100271,plain,
( ( sigma != sigma )
| ( ( a @ star )
!= sigma )
| ( one != a )
| ( b != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[226,100265]) ).
thf(100272,plain,
( ( sigma != sigma )
| ( ( a @ star )
!= sigma )
| ( one != a )
| ( b != a ) ),
inference(simp,[status(thm)],[100271]) ).
thf(100273,plain,
( ( ( a @ star )
!= sigma )
| ( one != a )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[100272:[]]) ).
thf(5091,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( A @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[46,5081]) ).
thf(5117,plain,
! [A: $i] :
( ( A != a )
| ( one != b )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( A @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[5091]) ).
thf(5152,plain,
( ( one != b )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( a @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[5117]) ).
thf(28745,plain,
( ( ( zero @ ( a @ ( a @ multiplication ) @ leq ) )
!= ( one @ star @ ( one @ leq ) ) )
| ( one != b )
| ( zero != sigma )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4339,13287]) ).
thf(28746,plain,
( ( ( zero @ ( a @ ( a @ multiplication ) @ leq ) )
!= ( one @ star @ ( one @ leq ) ) )
| ( one != b )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[28745]) ).
thf(28775,plain,
( ( ( one @ star )
!= zero )
| ( ( a @ ( a @ multiplication ) )
!= one )
| ( one != b )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[28746]) ).
thf(134,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) ) )
| ~ ( A @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[46,20]) ).
thf(141,plain,
! [A: $i] :
( ( A
!= ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) ) )
| ( ( sigma @ star )
!= one )
| ~ ( A @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[134]) ).
thf(154,plain,
( ( ( sigma @ star )
!= one )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[141]) ).
thf(551,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( a @ ( a @ multiplication ) ) )
| ( one != b )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[38,150]) ).
thf(585,plain,
! [C: $i,B: $i,A: $i] :
( ( C != a )
| ( ( B @ ( A @ multiplication ) )
!= a )
| ( one != b )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[551]) ).
thf(600,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= a )
| ( one != b )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( a @ ( B @ multiplication ) @ ( A @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[585]) ).
thf(159,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( b @ ( a @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[56,23]) ).
thf(170,plain,
! [C: $i,B: $i,A: $i] :
( ( A != b )
| ( ( B @ ( C @ addition ) )
!= a )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
= sigma ) ),
inference(simp,[status(thm)],[159]) ).
thf(175,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= a )
| ( ( b @ ( A @ addition ) @ ( B @ addition ) )
= sigma ) ),
inference(simp,[status(thm)],[170]) ).
thf(541,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
!= one )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( a @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[38,211]) ).
thf(580,plain,
! [C: $i,B: $i,A: $i] :
( ( C != a )
| ( ( B @ ( A @ multiplication ) )
!= b )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
!= one )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( a @ leq ) ) ),
inference(simp,[status(thm)],[541]) ).
thf(595,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= b )
| ( ( a @ ( B @ multiplication ) @ ( A @ multiplication ) )
!= one )
| ( ( sigma @ star )
!= zero )
| ~ ( zero @ ( a @ leq ) ) ),
inference(simp,[status(thm)],[580]) ).
thf(42,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ addition ) @ multiplication ) )
= ( C @ ( B @ multiplication ) @ ( C @ ( A @ multiplication ) @ addition ) ) ),
inference(cnf,[status(esa)],[41]) ).
thf(43,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ multiplication ) @ ( C @ ( A @ multiplication ) @ addition ) )
= ( C @ ( B @ ( A @ addition ) @ multiplication ) ) ),
inference(lifteq,[status(thm)],[42]) ).
thf(240,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( sigma @ addition ) )
!= ( B @ ( C @ ( D @ addition ) @ addition ) ) )
| ( ( A @ ( b @ addition ) @ ( a @ addition ) )
= ( B @ ( C @ addition ) @ ( D @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[161,23]) ).
thf(246,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A != B )
| ( ( C @ ( D @ addition ) )
!= sigma )
| ( ( A @ ( b @ addition ) @ ( a @ addition ) )
= ( B @ ( C @ addition ) @ ( D @ addition ) ) ) ),
inference(simp,[status(thm)],[240]) ).
thf(250,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ addition ) )
!= sigma )
| ( ( A @ ( b @ addition ) @ ( a @ addition ) )
= ( A @ ( B @ addition ) @ ( C @ addition ) ) ) ),
inference(simp,[status(thm)],[246]) ).
thf(185,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( A @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[49,20]) ).
thf(194,plain,
! [A: $i] :
( ( one != a )
| ( A != b )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( A @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[185]) ).
thf(203,plain,
( ( one != a )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( b @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[194]) ).
thf(43696,plain,
( ( sigma != sigma )
| ( one != a )
| ( ( a @ ( a @ multiplication ) )
!= zero )
| ~ ( zero @ ( b @ leq ) )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[226,42703]) ).
thf(43697,plain,
( ( one != a )
| ( ( a @ ( a @ multiplication ) )
!= zero )
| ~ ( zero @ ( b @ leq ) )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[43696:[]]) ).
thf(84,plain,
! [A: $i] :
( ( ( zero @ ( A @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) ) )
| ~ ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[54,20]) ).
thf(96,plain,
! [A: $i] :
( ( ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) )
!= zero )
| ( A
!= ( sigma @ star ) )
| ~ ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[84]) ).
thf(104,plain,
( ( ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) )
!= zero )
| ~ ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[96]) ).
thf(64155,plain,
! [B: $i,A: $i] :
( ( ( a @ ( sigma @ addition ) @ ( b @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[63882,32]) ).
thf(64156,plain,
( ( b @ ( a @ ( sigma @ addition ) @ ( b @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[64155:[bind(A,$thf( b )),bind(B,$thf( a @ ( sigma @ addition ) @ ( b @ addition ) ))]]) ).
thf(82791,plain,
( ( b @ ( a @ ( sigma @ addition ) @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[64156,23]) ).
thf(83108,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ ( sigma @ addition ) @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[82791,32]) ).
thf(83109,plain,
( ( b @ ( b @ ( a @ ( sigma @ addition ) @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[83108:[bind(A,$thf( b )),bind(B,$thf( b @ ( a @ ( sigma @ addition ) @ addition ) ))]]) ).
thf(106214,plain,
( ( b @ ( b @ addition ) @ ( a @ ( sigma @ addition ) @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[83109,23]) ).
thf(40,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ star @ ( C @ multiplication ) @ leq ) )
| ~ ( A @ ( C @ ( B @ ( A @ multiplication ) @ addition ) @ leq ) ) ),
inference(cnf,[status(esa)],[39]) ).
thf(1720,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[1596,32]) ).
thf(1721,plain,
( ( b @ ( sigma @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[1720:[bind(A,$thf( b )),bind(B,$thf( sigma ))]]) ).
thf(2004,plain,
( ( b @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[1721,161]) ).
thf(40566,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( A != one )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( a @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[49,5142]) ).
thf(40599,plain,
( ( one != a )
| ( one != b )
| ( ( a @ ( sigma @ multiplication ) )
!= zero )
| ~ ( zero @ ( a @ leq ) ) ),
inference(simp,[status(thm)],[40566]) ).
thf(66291,plain,
! [B: $i,A: $i] :
( ( ( a @ ( b @ addition ) )
!= ( A @ ( B @ addition ) ) )
| ( sigma != sigma )
| ( ( a @ ( A @ addition ) @ ( B @ addition ) @ ( b @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[284,508]) ).
thf(66292,plain,
! [B: $i,A: $i] :
( ( ( a @ ( b @ addition ) )
!= ( A @ ( B @ addition ) ) )
| ( ( a @ ( A @ addition ) @ ( B @ addition ) @ ( b @ addition ) )
= sigma ) ),
inference(simp,[status(thm)],[66291]) ).
thf(66293,plain,
( ( a @ ( a @ addition ) @ ( b @ addition ) @ ( b @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[66292:[bind(A,$thf( a )),bind(B,$thf( b ))]]) ).
thf(88407,plain,
( ( a @ ( a @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[66293,221]) ).
thf(88693,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[88407,32]) ).
thf(88694,plain,
( ( b @ ( a @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[88693:[bind(A,$thf( b )),bind(B,$thf( a @ ( a @ addition ) ))]]) ).
thf(89582,plain,
( ( b @ ( a @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[88694,23]) ).
thf(82093,plain,
( ( sigma != sigma )
| ( ( sigma @ ( b @ star @ multiplication ) )
!= b )
| ( one != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[360,81970]) ).
thf(82094,plain,
( ( ( sigma @ ( b @ star @ multiplication ) )
!= b )
| ( one != a )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[82093:[]]) ).
thf(187,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( b @ multiplication ) @ ( a @ multiplication ) ) )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[49,20]) ).
thf(198,plain,
! [A: $i] :
( ( ( a @ ( b @ multiplication ) )
!= one )
| ( A != a )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[187]) ).
thf(207,plain,
( ( ( a @ ( b @ multiplication ) )
!= one )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ leq ) ) ),
inference(simp,[status(thm)],[198]) ).
thf(90,plain,
! [A: $i] :
( ( ( A @ ( zero @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) ) )
| ~ ( zero @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[35,20]) ).
thf(103,plain,
! [A: $i] :
( ( A != a )
| ( zero != sigma )
| ~ ( zero @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[90]) ).
thf(111,plain,
( ( zero != sigma )
| ~ ( zero @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[103]) ).
thf(5164,plain,
( ( zero != sigma )
| ~ ( zero @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(rewrite,[status(thm)],[111,54]) ).
thf(58,plain,
! [A: $i] : ( A @ star @ ( A @ star @ ( A @ multiplication ) @ ( one @ addition ) @ leq ) ),
inference(cnf,[status(esa)],[57]) ).
thf(136,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( A @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[46,20]) ).
thf(147,plain,
! [A: $i] :
( ( A != a )
| ( one != b )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( A @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[136]) ).
thf(151,plain,
( ( one != b )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[147]) ).
thf(81974,plain,
( ( sigma != sigma )
| ( ( sigma @ ( b @ star @ multiplication ) )
!= sigma )
| ( one != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[360,81965]) ).
thf(81975,plain,
( ( ( sigma @ ( b @ star @ multiplication ) )
!= sigma )
| ( one != a )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[81974:[]]) ).
thf(66321,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ addition ) )
!= ( B @ ( C @ addition ) ) )
| ( A != sigma )
| ( ( a @ ( B @ addition ) @ ( C @ addition ) @ ( b @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[29,508]) ).
thf(66322,plain,
! [A: $i] :
( ( A != sigma )
| ( ( a @ ( zero @ addition ) @ ( A @ addition ) @ ( b @ addition ) )
= sigma ) ),
inference(pattern_uni,[status(thm)],[66321:[bind(A,$thf( A )),bind(B,$thf( zero )),bind(C,$thf( A ))]]) ).
thf(67598,plain,
( ( a @ ( zero @ addition ) @ ( sigma @ addition ) @ ( b @ addition ) )
= sigma ),
inference(simp,[status(thm)],[66322]) ).
thf(92267,plain,
( ( a @ ( zero @ addition ) @ ( b @ addition ) @ ( a @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[67598,161]) ).
thf(104590,plain,
( ( sigma != sigma )
| ( ( b @ star )
!= b )
| ( one != a )
| ( b != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[360,104580]) ).
thf(104591,plain,
( ( sigma != sigma )
| ( ( b @ star )
!= b )
| ( one != a )
| ( b != a ) ),
inference(simp,[status(thm)],[104590]) ).
thf(104592,plain,
( ( ( b @ star )
!= b )
| ( one != a )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[104591:[]]) ).
thf(553,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) ) )
| ~ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[38,20]) ).
thf(588,plain,
! [C: $i,B: $i,A: $i] :
( ( C != a )
| ( ( B @ ( A @ multiplication ) )
!= sigma )
| ~ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[553]) ).
thf(603,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= sigma )
| ~ ( a @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[588]) ).
thf(3882,plain,
! [A: $i] :
( ( ( A @ ( zero @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( zero != zero ) ),
inference(paramod_ordered,[status(thm)],[35,3870]) ).
thf(3883,plain,
! [A: $i] :
( ( A @ ( zero @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) ),
inference(simp,[status(thm)],[3882]) ).
thf(3884,plain,
! [A: $i] :
( ( A != a )
| ( zero != b ) ),
inference(simp,[status(thm)],[3883]) ).
thf(3892,plain,
zero != b,
inference(simp,[status(thm)],[3884]) ).
thf(183,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) ) )
| ~ ( A @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[49,20]) ).
thf(201,plain,
! [A: $i] :
( ( ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) )
!= one )
| ( A
!= ( sigma @ star ) )
| ~ ( A @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[183]) ).
thf(210,plain,
( ( ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) )
!= one )
| ~ ( sigma @ star @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[201]) ).
thf(482,plain,
! [A: $i] :
( ( ( A @ ( A @ addition ) )
!= ( a @ ( sigma @ addition ) @ ( b @ addition ) ) )
| ( A = sigma ) ),
inference(paramod_ordered,[status(thm)],[26,445]) ).
thf(491,plain,
! [A: $i] :
( ( A
!= ( a @ ( sigma @ addition ) ) )
| ( A != b )
| ( A = sigma ) ),
inference(simp,[status(thm)],[482]) ).
thf(506,plain,
( ( ( a @ ( sigma @ addition ) )
!= b )
| ( sigma = b ) ),
inference(simp,[status(thm)],[491]) ).
thf(64937,plain,
( ( ( a @ ( b @ addition ) @ ( a @ addition ) )
!= b )
| ( sigma = b ) ),
inference(rewrite,[status(thm)],[506,161]) ).
thf(82089,plain,
( ( sigma != sigma )
| ( ( a @ star )
!= one )
| ( one != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[226,81998]) ).
thf(82090,plain,
( ( ( a @ star )
!= one )
| ( one != a )
| ( b != a ) ),
inference(pattern_uni,[status(thm)],[82089:[]]) ).
thf(59769,plain,
! [A: $i] :
( ( ( a @ ( b @ addition ) @ ( b @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
!= ( A @ ( b @ addition ) @ ( a @ addition ) ) )
| ( ( sigma @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[59466,298]) ).
thf(59770,plain,
( ( sigma @ ( a @ ( b @ addition ) @ ( b @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[59769:[bind(A,$thf( a @ ( b @ addition ) @ ( b @ addition ) ))]]) ).
thf(80342,plain,
( ( sigma @ ( a @ ( b @ addition ) @ addition ) @ ( b @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[59770,23]) ).
thf(20846,plain,
! [B: $i,A: $i] :
( ( ( a @ ( b @ addition ) @ ( sigma @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( sigma @ ( A @ addition ) )
= ( B @ ( A @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[1047,221]) ).
thf(20847,plain,
( ( a @ ( b @ addition ) @ ( sigma @ addition ) )
= ( sigma @ ( sigma @ addition ) ) ),
inference(pattern_uni,[status(thm)],[20846:[bind(A,$thf( sigma )),bind(B,$thf( a @ ( b @ addition ) ))]]) ).
thf(28801,plain,
( ( sigma @ ( b @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[20847,161,1047]) ).
thf(80662,plain,
! [B: $i,A: $i] :
( ( ( sigma @ ( a @ ( b @ addition ) @ addition ) @ ( b @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[80342,32]) ).
thf(80663,plain,
( ( b @ ( sigma @ ( a @ ( b @ addition ) @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[80662:[bind(A,$thf( b )),bind(B,$thf( sigma @ ( a @ ( b @ addition ) @ addition ) ))]]) ).
thf(104607,plain,
( ( b @ ( sigma @ addition ) @ ( a @ ( b @ addition ) @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[80663,23]) ).
thf(4370,plain,
( ( ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) )
!= ( one @ star @ ( one @ leq ) ) )
| ( ( sigma @ star )
!= zero )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4339,105]) ).
thf(4371,plain,
( ( ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) )
!= ( one @ star @ ( one @ leq ) ) )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[4370]) ).
thf(4382,plain,
( ( ( one @ star )
!= zero )
| ( ( a @ ( b @ multiplication ) @ ( a @ multiplication ) )
!= one )
| ( ( sigma @ star )
!= zero ) ),
inference(simp,[status(thm)],[4371]) ).
thf(552,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( sigma @ star @ multiplication ) ) )
| ~ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[38,20]) ).
thf(581,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) ) )
| ( ( B @ ( A @ multiplication ) )
!= ( sigma @ star ) )
| ~ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[552]) ).
thf(596,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= ( sigma @ star ) )
| ~ ( a @ ( sigma @ multiplication ) @ ( a @ multiplication ) @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) ) ),
inference(simp,[status(thm)],[581]) ).
thf(3848,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( a @ ( b @ multiplication ) ) )
| ( ( A @ ( a @ multiplication ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[46,3836]) ).
thf(3857,plain,
! [A: $i] :
( ( A != a )
| ( one != b )
| ( ( A @ ( a @ multiplication ) )
!= zero ) ),
inference(simp,[status(thm)],[3848]) ).
thf(3869,plain,
( ( one != b )
| ( ( a @ ( a @ multiplication ) )
!= zero ) ),
inference(simp,[status(thm)],[3857]) ).
thf(13237,plain,
( ( ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) )
!= ( one @ star @ ( one @ leq ) ) )
| ( zero != sigma )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4339,5150]) ).
thf(13238,plain,
( ( ( zero @ ( a @ ( b @ multiplication ) @ ( a @ multiplication ) @ leq ) )
!= ( one @ star @ ( one @ leq ) ) )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[13237]) ).
thf(13262,plain,
( ( ( one @ star )
!= zero )
| ( ( a @ ( b @ multiplication ) @ ( a @ multiplication ) )
!= one )
| ( zero != sigma ) ),
inference(simp,[status(thm)],[13238]) ).
thf(85800,plain,
! [A: $i] :
( ( ( sigma @ ( b @ addition ) @ ( a @ addition ) @ ( b @ addition ) @ ( a @ addition ) )
!= ( A @ ( b @ addition ) @ ( a @ addition ) ) )
| ( ( sigma @ ( A @ addition ) )
= sigma ) ),
inference(paramod_ordered,[status(thm)],[85401,298]) ).
thf(85801,plain,
( ( sigma @ ( sigma @ ( b @ addition ) @ ( a @ addition ) @ addition ) )
= sigma ),
inference(pattern_uni,[status(thm)],[85800:[bind(A,$thf( sigma @ ( b @ addition ) @ ( a @ addition ) ))]]) ).
thf(110965,plain,
( ( sigma @ ( sigma @ ( b @ addition ) @ addition ) @ ( a @ addition ) )
= sigma ),
inference(rewrite,[status(thm)],[85801,23]) ).
thf(380,plain,
! [A: $i] :
( ( ( sigma @ ( b @ addition ) @ ( a @ addition ) )
!= ( zero @ ( A @ addition ) ) )
| ( sigma = A ) ),
inference(paramod_ordered,[status(thm)],[237,29]) ).
thf(416,plain,
! [A: $i] :
( ( ( sigma @ ( b @ addition ) )
!= zero )
| ( a != A )
| ( sigma = A ) ),
inference(simp,[status(thm)],[380]) ).
thf(418,plain,
( ( ( sigma @ ( b @ addition ) )
!= zero )
| ( sigma = a ) ),
inference(simp,[status(thm)],[416]) ).
thf(48191,plain,
( ( zero != sigma )
| ( sigma = a ) ),
inference(rewrite,[status(thm)],[418,1596]) ).
thf(123921,plain,
$false,
inference(e,[status(thm)],[79936,90821,13321,22047,72731,49828,69,58450,63882,81970,73180,1596,76143,70143,81747,597,4339,79904,56,100270,96702,46299,1275,1919,153,81998,4839,3836,17856,24,288,13287,19318,103050,95147,52,98158,13280,39895,104595,81987,40727,30812,5150,1279,15092,13275,77351,17852,46,284,29,99575,20,3312,152,228,81977,4383,57,93820,96711,211,42703,602,61,221,49117,40679,3870,248,60,28772,78559,5142,1783,1047,87088,38,598,424,21,33,21979,82109,82096,4385,43709,10131,6324,5145,6028,30832,3119,81982,156,615,5081,593,100265,52293,60667,7806,24537,4384,5149,3115,11061,41,40775,25175,56643,82101,105,360,82088,81963,508,81752,32,1273,3985,161,64,444,601,1278,298,28066,61782,44,59,204,27,101652,71,100278,51493,43744,3123,49,107625,62829,445,13319,33049,3118,54,35148,78611,3779,362,6832,90700,39,208,599,4388,8120,96714,47315,323,85401,155,74966,594,278,35,4232,44551,226,33798,1277,209,617,1472,59466,43714,63,81743,82677,30823,150,104580,39036,109220,50,90697,16416,18488,100273,8509,5152,28775,30813,81749,154,600,175,595,43,48259,250,203,43697,104,38197,106214,81984,68923,17095,40,26,2004,55,40599,23,89582,82094,207,81965,15807,67626,57470,5164,58,151,36,51,65276,81975,1248,92267,37381,104592,603,30,3892,210,82791,64937,82090,88407,50584,80342,28801,104607,2810,4382,596,3869,13279,13262,839,110965,4066,71269,47,82103,55673,592,48191]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : KLE169+1 : TPTP v9.3.1. Released v5.2.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.23/0.48 % Computer : n014.cluster.edu
% 0.23/0.48 % Model : x86_64 x86_64
% 0.23/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.23/0.48 % Memory : 8046.5625MB
% 0.23/0.48 % OS : Linux 6.8.0-71-generic
% 0.23/0.48 % CPULimit : 300
% 0.23/0.48 % WCLimit : 300
% 0.23/0.48 % DateTime : Fri Sep 25 19:30:17 UTC 2026
% 0.23/0.48 % CPUTime :
% 0.23/0.49 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.45/1.31 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.80/1.59 % [INFO] Parsing done (277ms).
% 2.05/1.60 % [INFO] Running in sequential loop mode.
% 2.67/1.94 % [INFO] eprover registered as external prover.
% 2.67/1.94 % [INFO] Scanning for conjecture ...
% 2.67/2.02 % [INFO] Found a conjecture (or negated_conjecture) and 17 axioms. Running axiom selection ...
% 3.01/2.07 % [INFO] Axiom selection finished. Selected 17 axioms (removed 0 axioms).
% 3.01/2.11 % [INFO] Problem is first-order (TPTP FOF).
% 3.01/2.11 % [INFO] Type checking passed.
% 3.01/2.12 % [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 ...
% 196.98/50.37 % External prover 'e' found a proof!
% 196.98/50.37 % [INFO] Killing All external provers ...
% 196.98/50.38 % Time passed: 49700ms (effective reasoning time: 48768ms)
% 196.98/50.38 % 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)>
% 196.98/50.38 % Axioms used in derivation (17): additive_identity, star_induction_right, left_annihilation, star_induction_left, right_distributivity, star_unfold_left, multiplicative_left_identity, additive_idempotence, additive_associativity, multiplicative_right_identity, star_unfold_right, order, additive_commutativity, right_annihilation, an, multiplicative_associativity, left_distributivity
% 196.98/50.38 % No. of inferences in proof: 824
% 196.98/50.38 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 49700 ms resp. 48768 ms w/o parsing
% 199.94/50.87 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 199.94/50.88 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------