%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : RNG006-3 : TPTP v9.3.1. Released v1.0.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 : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:25:11 AM UTC 2026
% Result : Unsatisfiable 206.82s 88.36s
% Output : Refutation 201.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 22
% Syntax : Number of formulae : 397 ( 43 unt; 0 typ; 0 def)
% Number of atoms : 2179 ( 561 equ; 0 cnn)
% Maximal formula atoms : 100 ( 5 avg)
% Number of connectives : 8266 (1605 ~;1486 |; 0 &;5175 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 237 ( 12 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 16 ( 13 usr; 10 con; 0-3 aty)
% Number of variables : 1759 ( 0 ^;1759 !; 0 ?;1759 :)
% Comments :
%------------------------------------------------------------------------------
thf(product_decl,type,
product: $i > $i > $i > $o ).
thf(a_decl,type,
a: $i ).
thf(bS_Ic_decl,type,
bS_Ic: $i ).
thf(aPb_S_IaPc_decl,type,
aPb_S_IaPc: $i ).
thf(sum_decl,type,
sum: $i > $i > $i > $o ).
thf(additive_identity_decl,type,
additive_identity: $i ).
thf(additive_inverse_decl,type,
additive_inverse: $i > $i ).
thf(add_decl,type,
add: $i > $i > $i ).
thf(aPb_decl,type,
aPb: $i ).
thf(aPc_decl,type,
aPc: $i ).
thf(b_decl,type,
b: $i ).
thf(c_decl,type,
c: $i ).
thf(multiply_decl,type,
multiply: $i > $i > $i ).
thf(2,axiom,
! [A: $i] : ( A @ ( additive_identity @ ( A @ sum ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_identity2) ).
thf(25,plain,
! [A: $i] : ( A @ ( additive_identity @ ( A @ sum ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(15,axiom,
aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aPb_plus_IaPc) ).
thf(48,plain,
aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(9,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C = D )
| ~ ( D @ ( B @ ( A @ sum ) ) )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addition_is_well_defined) ).
thf(35,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C = D )
| ~ ( D @ ( B @ ( A @ sum ) ) )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(36,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C = D )
| ~ ( D @ ( B @ ( A @ sum ) ) )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
inference(cnf,[status(esa)],[35]) ).
thf(37,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( B @ ( A @ sum ) ) )
| ~ ( C @ ( B @ ( A @ sum ) ) )
| ( C = D ) ),
inference(lifteq,[status(thm)],[36]) ).
thf(22579,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ~ ( D @ ( B @ ( A @ sum ) ) )
| ~ $true
| ( C = D ) ),
inference(paramod_ordered,[status(thm)],[48,37]) ).
thf(22580,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ~ ( D @ ( B @ ( A @ sum ) ) )
| ( C = D ) ),
inference(simp,[status(thm)],[22579]) ).
thf(22581,plain,
! [A: $i] :
( ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
| ( aPb_S_IaPc = A ) ),
inference(pattern_uni,[status(thm)],[22580:[bind(A,$thf( aPb )),bind(B,$thf( aPc @ additive_inverse )),bind(C,$thf( aPb_S_IaPc )),bind(D,$thf( D ))]]) ).
thf(23108,plain,
! [A: $i] :
( ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
| ( aPb_S_IaPc = A ) ),
inference(simp,[status(thm)],[22581]) ).
thf(22,axiom,
aPb @ ( b @ ( a @ product ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_times_b) ).
thf(58,plain,
aPb @ ( b @ ( a @ product ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(23760,plain,
! [A: $i] :
( ( A != aPb )
| ( aPb_S_IaPc @ ( b @ ( a @ product ) ) )
| ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(paramod_ordered,[status(thm)],[23108,58]) ).
thf(23761,plain,
( ( aPb_S_IaPc @ ( b @ ( a @ product ) ) )
| ~ ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(pattern_uni,[status(thm)],[23760:[bind(A,$thf( aPb ))]]) ).
thf(35680,plain,
! [A: $i] :
( ( ( A @ ( additive_identity @ ( A @ sum ) ) )
!= ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc @ ( b @ ( a @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[25,23761]) ).
thf(35681,plain,
! [A: $i] :
( ( ( A @ ( additive_identity @ ( A @ sum ) ) )
!= ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc @ ( b @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[35680]) ).
thf(35794,plain,
! [A: $i] :
( ( A != aPb )
| ( ( aPc @ additive_inverse )
!= additive_identity )
| ( A != aPb )
| ( aPb_S_IaPc @ ( b @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[35681]) ).
thf(35827,plain,
( ( ( aPc @ additive_inverse )
!= additive_identity )
| ( aPb_S_IaPc @ ( b @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[35794]) ).
thf(10,axiom,
! [A: $i] : ( A @ ( A @ ( additive_identity @ sum ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_identity1) ).
thf(38,plain,
! [A: $i] : ( A @ ( A @ ( additive_identity @ sum ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(23645,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( additive_identity @ sum ) ) )
!= ( B @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ~ $true
| ( aPb_S_IaPc = B ) ),
inference(paramod_ordered,[status(thm)],[38,23108]) ).
thf(23646,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( additive_identity @ sum ) ) )
!= ( B @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc = B ) ),
inference(simp,[status(thm)],[23645]) ).
thf(23824,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( A
!= ( aPc @ additive_inverse ) )
| ( aPb != additive_identity )
| ( aPb_S_IaPc = B ) ),
inference(simp,[status(thm)],[23646]) ).
thf(23850,plain,
( ( aPb != additive_identity )
| ( ( aPc @ additive_inverse )
= aPb_S_IaPc ) ),
inference(simp,[status(thm)],[23824]) ).
thf(19,axiom,
! [B: $i,A: $i] : ( B @ ( A @ multiply ) @ ( B @ ( A @ product ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',closure_of_multiplication) ).
thf(54,plain,
! [B: $i,A: $i] : ( B @ ( A @ multiply ) @ ( B @ ( A @ product ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(1,negated_conjecture,
~ ( aPb_S_IaPc @ ( bS_Ic @ ( a @ product ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_a_times_bS_Ic_is_aPb_S__IaPc) ).
thf(23,plain,
~ ( aPb_S_IaPc @ ( bS_Ic @ ( a @ product ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(24,plain,
~ ( aPb_S_IaPc @ ( bS_Ic @ ( a @ product ) ) ),
inference(polarity_switch,[status(thm)],[23]) ).
thf(67,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiply ) @ ( B @ ( A @ product ) ) )
!= ( aPb_S_IaPc @ ( bS_Ic @ ( a @ product ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[54,24]) ).
thf(68,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ multiply ) @ ( B @ ( A @ product ) ) )
!= ( aPb_S_IaPc @ ( bS_Ic @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[67]) ).
thf(69,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiply ) )
!= aPb_S_IaPc )
| ( B != bS_Ic )
| ( A != a ) ),
inference(simp,[status(thm)],[68]) ).
thf(70,plain,
( ( bS_Ic @ ( a @ multiply ) )
!= aPb_S_IaPc ),
inference(simp,[status(thm)],[69]) ).
thf(23633,plain,
! [A: $i] :
( ( A
!= ( bS_Ic @ ( a @ multiply ) ) )
| ( aPb_S_IaPc != aPb_S_IaPc )
| ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(paramod_ordered,[status(thm)],[23108,70]) ).
thf(23634,plain,
! [A: $i] :
( ( A
!= ( bS_Ic @ ( a @ multiply ) ) )
| ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(simp,[status(thm)],[23633]) ).
thf(23635,plain,
~ ( bS_Ic @ ( a @ multiply ) @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ),
inference(pattern_uni,[status(thm)],[23634:[bind(A,$thf( bS_Ic @ ( a @ multiply ) ))]]) ).
thf(23964,plain,
! [A: $i] :
( ( ( A @ ( additive_identity @ ( A @ sum ) ) )
!= ( bS_Ic @ ( a @ multiply ) @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[25,23635]) ).
thf(23965,plain,
! [A: $i] :
( ( A @ ( additive_identity @ ( A @ sum ) ) )
!= ( bS_Ic @ ( a @ multiply ) @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(simp,[status(thm)],[23964]) ).
thf(24033,plain,
! [A: $i] :
( ( A
!= ( bS_Ic @ ( a @ multiply ) ) )
| ( ( aPc @ additive_inverse )
!= additive_identity )
| ( A != aPb ) ),
inference(simp,[status(thm)],[23965]) ).
thf(24064,plain,
( ( ( bS_Ic @ ( a @ multiply ) )
!= aPb )
| ( ( aPc @ additive_inverse )
!= additive_identity ) ),
inference(simp,[status(thm)],[24033]) ).
thf(25414,plain,
( ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( ( bS_Ic @ ( a @ multiply ) )
!= aPb )
| ( additive_identity != aPb_S_IaPc )
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[23850,24064]) ).
thf(25415,plain,
( ( ( bS_Ic @ ( a @ multiply ) )
!= aPb )
| ( additive_identity != aPb_S_IaPc )
| ( aPb != additive_identity ) ),
inference(pattern_uni,[status(thm)],[25414:[]]) ).
thf(35755,plain,
( ( ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc @ ( b @ ( a @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,23761]) ).
thf(35756,plain,
( ( ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc @ ( b @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[35755]) ).
thf(35808,plain,
( ( aPb != aPb_S_IaPc )
| ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( aPb != aPb )
| ( aPb_S_IaPc @ ( b @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[35756]) ).
thf(35838,plain,
( ( aPb != aPb_S_IaPc )
| ( aPb_S_IaPc @ ( b @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[35808]) ).
thf(8,axiom,
! [A: $i] : ( additive_identity @ ( A @ ( A @ additive_inverse @ sum ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_inverse) ).
thf(34,plain,
! [A: $i] : ( additive_identity @ ( A @ ( A @ additive_inverse @ sum ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(63,plain,
( ( ( aPb @ ( b @ ( a @ product ) ) )
!= ( aPb_S_IaPc @ ( bS_Ic @ ( a @ product ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[58,24]) ).
thf(64,plain,
( ( aPb @ ( b @ ( a @ product ) ) )
!= ( aPb_S_IaPc @ ( bS_Ic @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[63]) ).
thf(65,plain,
( ( aPb != aPb_S_IaPc )
| ( b != bS_Ic )
| ( a != a ) ),
inference(simp,[status(thm)],[64]) ).
thf(66,plain,
( ( aPb != aPb_S_IaPc )
| ( b != bS_Ic ) ),
inference(simp,[status(thm)],[65]) ).
thf(23680,plain,
! [A: $i] :
( ( A != aPb )
| ( aPb_S_IaPc != aPb_S_IaPc )
| ( b != bS_Ic )
| ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(paramod_ordered,[status(thm)],[23108,66]) ).
thf(23681,plain,
! [A: $i] :
( ( A != aPb )
| ( b != bS_Ic )
| ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(simp,[status(thm)],[23680]) ).
thf(23682,plain,
( ( b != bS_Ic )
| ~ ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(pattern_uni,[status(thm)],[23681:[bind(A,$thf( aPb ))]]) ).
thf(24076,plain,
! [A: $i] :
( ( ( additive_identity @ ( A @ ( A @ additive_inverse @ sum ) ) )
!= ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( b != bS_Ic )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[34,23682]) ).
thf(24077,plain,
! [A: $i] :
( ( ( additive_identity @ ( A @ ( A @ additive_inverse @ sum ) ) )
!= ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( b != bS_Ic ) ),
inference(simp,[status(thm)],[24076]) ).
thf(24179,plain,
! [A: $i] :
( ( aPb != additive_identity )
| ( A
!= ( aPc @ additive_inverse ) )
| ( ( A @ additive_inverse )
!= aPb )
| ( b != bS_Ic ) ),
inference(simp,[status(thm)],[24077]) ).
thf(24212,plain,
( ( aPb != additive_identity )
| ( ( aPc @ additive_inverse @ additive_inverse )
!= aPb )
| ( b != bS_Ic ) ),
inference(simp,[status(thm)],[24179]) ).
thf(33777,plain,
( ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( aPb != additive_identity )
| ( ( aPb_S_IaPc @ additive_inverse )
!= aPb )
| ( b != bS_Ic )
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[23850,24212]) ).
thf(33778,plain,
( ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( ( aPb_S_IaPc @ additive_inverse )
!= aPb )
| ( b != bS_Ic )
| ( aPb != additive_identity ) ),
inference(simp,[status(thm)],[33777]) ).
thf(33779,plain,
( ( ( aPb_S_IaPc @ additive_inverse )
!= aPb )
| ( b != bS_Ic )
| ( aPb != additive_identity ) ),
inference(pattern_uni,[status(thm)],[33778:[]]) ).
thf(20,axiom,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( G @ ( B @ ( F @ product ) ) )
| ~ ( G @ ( E @ ( C @ sum ) ) )
| ~ ( F @ ( D @ ( A @ sum ) ) )
| ~ ( E @ ( B @ ( D @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distributivity4) ).
thf(55,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( G @ ( B @ ( F @ product ) ) )
| ~ ( G @ ( E @ ( C @ sum ) ) )
| ~ ( F @ ( D @ ( A @ sum ) ) )
| ~ ( E @ ( B @ ( D @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(56,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( G @ ( B @ ( F @ product ) ) )
| ~ ( G @ ( E @ ( C @ sum ) ) )
| ~ ( F @ ( D @ ( A @ sum ) ) )
| ~ ( E @ ( B @ ( D @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[55]) ).
thf(5,axiom,
! [B: $i,A: $i] : ( B @ ( A @ add ) @ ( B @ ( A @ sum ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',closure_of_addition) ).
thf(29,plain,
! [B: $i,A: $i] : ( B @ ( A @ add ) @ ( B @ ( A @ sum ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(23584,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ add ) @ ( B @ ( A @ sum ) ) )
!= ( C @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ~ $true
| ( aPb_S_IaPc = C ) ),
inference(paramod_ordered,[status(thm)],[29,23108]) ).
thf(23585,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ add ) @ ( B @ ( A @ sum ) ) )
!= ( C @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc = C ) ),
inference(simp,[status(thm)],[23584]) ).
thf(23586,plain,
( ( aPc @ additive_inverse @ ( aPb @ add ) )
= aPb_S_IaPc ),
inference(pattern_uni,[status(thm)],[23585:[bind(A,$thf( aPb )),bind(B,$thf( aPc @ additive_inverse )),bind(C,$thf( aPc @ additive_inverse @ ( aPb @ add ) ))]]) ).
thf(25278,plain,
( ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( ( aPb_S_IaPc @ ( aPb @ add ) )
= aPb_S_IaPc )
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[23850,23586]) ).
thf(25279,plain,
( ( ( aPb_S_IaPc @ ( aPb @ add ) )
= aPb_S_IaPc )
| ( aPb != additive_identity ) ),
inference(pattern_uni,[status(thm)],[25278:[]]) ).
thf(4,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ sum ) ) )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_addition) ).
thf(27,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ sum ) ) )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(28,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ sum ) ) )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
inference(cnf,[status(esa)],[27]) ).
thf(25309,plain,
( ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ~ ( bS_Ic @ ( a @ multiply ) @ ( aPb_S_IaPc @ ( aPb @ sum ) ) )
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[23850,23635]) ).
thf(25310,plain,
( ~ ( bS_Ic @ ( a @ multiply ) @ ( aPb_S_IaPc @ ( aPb @ sum ) ) )
| ( aPb != additive_identity ) ),
inference(pattern_uni,[status(thm)],[25309:[]]) ).
thf(30953,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ ( B @ sum ) ) )
!= ( bS_Ic @ ( a @ multiply ) @ ( aPb_S_IaPc @ ( aPb @ sum ) ) ) )
| ~ $true
| ( aPb != additive_identity )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,25310]) ).
thf(30954,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ ( B @ sum ) ) )
!= ( bS_Ic @ ( a @ multiply ) @ ( aPb_S_IaPc @ ( aPb @ sum ) ) ) )
| ( aPb != additive_identity )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
inference(simp,[status(thm)],[30953]) ).
thf(30955,plain,
( ( aPb != additive_identity )
| ~ ( bS_Ic @ ( a @ multiply ) @ ( aPb @ ( aPb_S_IaPc @ sum ) ) ) ),
inference(pattern_uni,[status(thm)],[30954:[bind(A,$thf( aPb_S_IaPc )),bind(B,$thf( aPb )),bind(C,$thf( bS_Ic @ ( a @ multiply ) ))]]) ).
thf(21,axiom,
aPc @ ( c @ ( a @ product ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_times_c) ).
thf(57,plain,
aPc @ ( c @ ( a @ product ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(23578,plain,
! [A: $i] :
( ( A != c )
| ( aPc @ ( aPb_S_IaPc @ ( a @ product ) ) )
| ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(paramod_ordered,[status(thm)],[23108,57]) ).
thf(23579,plain,
( ( aPc @ ( aPb_S_IaPc @ ( a @ product ) ) )
| ~ ( c @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(pattern_uni,[status(thm)],[23578:[bind(A,$thf( c ))]]) ).
thf(28986,plain,
( ( ( c @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPc @ ( aPb_S_IaPc @ ( a @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,23579]) ).
thf(28987,plain,
( ( ( c @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPc @ ( aPb_S_IaPc @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[28986]) ).
thf(29025,plain,
( ( c != aPb_S_IaPc )
| ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( aPb != aPb )
| ( aPc @ ( aPb_S_IaPc @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[28987]) ).
thf(29055,plain,
( ( c != aPb_S_IaPc )
| ( aPc @ ( aPb_S_IaPc @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[29025]) ).
thf(30038,plain,
( ( ( aPc @ ( aPb_S_IaPc @ ( a @ product ) ) )
!= ( aPb_S_IaPc @ ( bS_Ic @ ( a @ product ) ) ) )
| ~ $true
| ( c != aPb_S_IaPc ) ),
inference(paramod_ordered,[status(thm)],[29055,24]) ).
thf(30039,plain,
( ( ( aPc @ ( aPb_S_IaPc @ ( a @ product ) ) )
!= ( aPb_S_IaPc @ ( bS_Ic @ ( a @ product ) ) ) )
| ( c != aPb_S_IaPc ) ),
inference(simp,[status(thm)],[30038]) ).
thf(30679,plain,
( ( aPc != aPb_S_IaPc )
| ( aPb_S_IaPc != bS_Ic )
| ( a != a )
| ( c != aPb_S_IaPc ) ),
inference(simp,[status(thm)],[30039]) ).
thf(30878,plain,
( ( aPc != aPb_S_IaPc )
| ( aPb_S_IaPc != bS_Ic )
| ( c != aPb_S_IaPc ) ),
inference(simp,[status(thm)],[30679]) ).
thf(12,axiom,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( G @ ( E @ ( C @ sum ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distributivity1) ).
thf(41,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( G @ ( E @ ( C @ sum ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(42,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( G @ ( E @ ( C @ sum ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[41]) ).
thf(23534,plain,
! [A: $i] :
( ( A != aPb )
| ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb_S_IaPc @ sum ) ) )
| ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(paramod_ordered,[status(thm)],[23108,48]) ).
thf(23535,plain,
( ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb_S_IaPc @ sum ) ) )
| ~ ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(pattern_uni,[status(thm)],[23534:[bind(A,$thf( aPb ))]]) ).
thf(40915,plain,
! [A: $i] :
( ( ( A @ ( additive_identity @ ( A @ sum ) ) )
!= ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb_S_IaPc @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[25,23535]) ).
thf(40916,plain,
! [A: $i] :
( ( ( A @ ( additive_identity @ ( A @ sum ) ) )
!= ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb_S_IaPc @ sum ) ) ) ),
inference(simp,[status(thm)],[40915]) ).
thf(41045,plain,
! [A: $i] :
( ( A != aPb )
| ( ( aPc @ additive_inverse )
!= additive_identity )
| ( A != aPb )
| ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb_S_IaPc @ sum ) ) ) ),
inference(simp,[status(thm)],[40916]) ).
thf(41090,plain,
( ( ( aPc @ additive_inverse )
!= additive_identity )
| ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb_S_IaPc @ sum ) ) ) ),
inference(simp,[status(thm)],[41045]) ).
thf(42147,plain,
! [C: $i,B: $i,A: $i] :
( ( ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb_S_IaPc @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ~ $true
| ( ( aPc @ additive_inverse )
!= additive_identity ) ),
inference(paramod_ordered,[status(thm)],[41090,28]) ).
thf(42148,plain,
! [C: $i,B: $i,A: $i] :
( ( ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb_S_IaPc @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ( ( aPc @ additive_inverse )
!= additive_identity ) ),
inference(simp,[status(thm)],[42147]) ).
thf(42149,plain,
( ( aPb_S_IaPc @ ( aPb_S_IaPc @ ( aPc @ additive_inverse @ sum ) ) )
| ( ( aPc @ additive_inverse )
!= additive_identity ) ),
inference(pattern_uni,[status(thm)],[42148:[bind(A,$thf( aPb_S_IaPc )),bind(B,$thf( aPc @ additive_inverse )),bind(C,$thf( aPb_S_IaPc ))]]) ).
thf(17,axiom,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( C @ product ) ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_multiplication1) ).
thf(51,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( C @ product ) ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(52,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( C @ product ) ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[51]) ).
thf(18,axiom,
bS_Ic @ ( c @ additive_inverse @ ( b @ sum ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_plus_inverse_c) ).
thf(53,plain,
bS_Ic @ ( c @ additive_inverse @ ( b @ sum ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(305,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( b @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[53,28]) ).
thf(306,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( b @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) ) ),
inference(simp,[status(thm)],[305]) ).
thf(307,plain,
bS_Ic @ ( b @ ( c @ additive_inverse @ sum ) ),
inference(pattern_uni,[status(thm)],[306:[bind(A,$thf( b )),bind(B,$thf( c @ additive_inverse )),bind(C,$thf( bS_Ic ))]]) ).
thf(23587,plain,
! [A: $i] :
( ( A
!= ( c @ additive_inverse ) )
| ( bS_Ic @ ( b @ ( aPb_S_IaPc @ sum ) ) )
| ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(paramod_ordered,[status(thm)],[23108,307]) ).
thf(23588,plain,
( ( bS_Ic @ ( b @ ( aPb_S_IaPc @ sum ) ) )
| ~ ( c @ additive_inverse @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(pattern_uni,[status(thm)],[23587:[bind(A,$thf( c @ additive_inverse ))]]) ).
thf(43427,plain,
( ( ( c @ additive_inverse @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( bS_Ic @ ( b @ ( aPb_S_IaPc @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,23588]) ).
thf(43428,plain,
( ( ( c @ additive_inverse @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( bS_Ic @ ( b @ ( aPb_S_IaPc @ sum ) ) ) ),
inference(simp,[status(thm)],[43427]) ).
thf(43467,plain,
( ( ( c @ additive_inverse )
!= aPb_S_IaPc )
| ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( aPb != aPb )
| ( bS_Ic @ ( b @ ( aPb_S_IaPc @ sum ) ) ) ),
inference(simp,[status(thm)],[43428]) ).
thf(43517,plain,
( ( ( c @ additive_inverse )
!= aPb_S_IaPc )
| ( bS_Ic @ ( b @ ( aPb_S_IaPc @ sum ) ) ) ),
inference(simp,[status(thm)],[43467]) ).
thf(25274,plain,
( ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( aPb_S_IaPc @ ( aPb_S_IaPc @ ( aPb @ sum ) ) )
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[23850,48]) ).
thf(25275,plain,
( ( aPb_S_IaPc @ ( aPb_S_IaPc @ ( aPb @ sum ) ) )
| ( aPb != additive_identity ) ),
inference(pattern_uni,[status(thm)],[25274:[]]) ).
thf(14,axiom,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( G @ ( F @ ( A @ product ) ) )
| ~ ( G @ ( E @ ( C @ sum ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distributivity2) ).
thf(46,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( G @ ( F @ ( A @ product ) ) )
| ~ ( G @ ( E @ ( C @ sum ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(6,axiom,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( D @ ( C @ sum ) ) )
| ~ ( F @ ( E @ ( A @ sum ) ) )
| ~ ( E @ ( D @ ( B @ sum ) ) )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_addition2) ).
thf(30,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( D @ ( C @ sum ) ) )
| ~ ( F @ ( E @ ( A @ sum ) ) )
| ~ ( E @ ( D @ ( B @ sum ) ) )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(31,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( D @ ( C @ sum ) ) )
| ~ ( F @ ( E @ ( A @ sum ) ) )
| ~ ( E @ ( D @ ( B @ sum ) ) )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
inference(cnf,[status(esa)],[30]) ).
thf(383,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( b @ sum ) ) )
!= ( F @ ( E @ ( A @ sum ) ) ) )
| ( F @ ( D @ ( C @ sum ) ) )
| ~ $true
| ~ ( E @ ( D @ ( B @ sum ) ) )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
inference(paramod_ordered,[status(thm)],[53,31]) ).
thf(384,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( b @ sum ) ) )
!= ( F @ ( E @ ( A @ sum ) ) ) )
| ( F @ ( D @ ( C @ sum ) ) )
| ~ ( E @ ( D @ ( B @ sum ) ) )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
inference(simp,[status(thm)],[383]) ).
thf(385,plain,
! [C: $i,B: $i,A: $i] :
( ( bS_Ic @ ( C @ ( B @ sum ) ) )
| ~ ( c @ additive_inverse @ ( C @ ( A @ sum ) ) )
| ~ ( B @ ( A @ ( b @ sum ) ) ) ),
inference(pattern_uni,[status(thm)],[384:[bind(A,$thf( b )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( c @ additive_inverse )),bind(F,$thf( bS_Ic ))]]) ).
thf(501,plain,
! [C: $i,B: $i,A: $i] :
( ( bS_Ic @ ( C @ ( B @ sum ) ) )
| ~ ( c @ additive_inverse @ ( C @ ( A @ sum ) ) )
| ~ ( B @ ( A @ ( b @ sum ) ) ) ),
inference(simp,[status(thm)],[385]) ).
thf(640,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( additive_identity @ sum ) ) )
!= ( c @ additive_inverse @ ( D @ ( B @ sum ) ) ) )
| ( bS_Ic @ ( D @ ( C @ sum ) ) )
| ~ $true
| ~ ( C @ ( B @ ( b @ sum ) ) ) ),
inference(paramod_ordered,[status(thm)],[38,501]) ).
thf(641,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( additive_identity @ sum ) ) )
!= ( c @ additive_inverse @ ( D @ ( B @ sum ) ) ) )
| ( bS_Ic @ ( D @ ( C @ sum ) ) )
| ~ ( C @ ( B @ ( b @ sum ) ) ) ),
inference(simp,[status(thm)],[640]) ).
thf(642,plain,
! [A: $i] :
( ( bS_Ic @ ( c @ additive_inverse @ ( A @ sum ) ) )
| ~ ( A @ ( additive_identity @ ( b @ sum ) ) ) ),
inference(pattern_uni,[status(thm)],[641:[bind(A,$thf( c @ additive_inverse )),bind(B,$thf( additive_identity )),bind(C,$thf( C )),bind(D,$thf( c @ additive_inverse ))]]) ).
thf(678,plain,
! [A: $i] :
( ( bS_Ic @ ( c @ additive_inverse @ ( A @ sum ) ) )
| ~ ( A @ ( additive_identity @ ( b @ sum ) ) ) ),
inference(simp,[status(thm)],[642]) ).
thf(760,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( additive_identity @ sum ) ) )
!= ( B @ ( additive_identity @ ( b @ sum ) ) ) )
| ( bS_Ic @ ( c @ additive_inverse @ ( B @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[38,678]) ).
thf(761,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( additive_identity @ sum ) ) )
!= ( B @ ( additive_identity @ ( b @ sum ) ) ) )
| ( bS_Ic @ ( c @ additive_inverse @ ( B @ sum ) ) ) ),
inference(simp,[status(thm)],[760]) ).
thf(779,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( A != additive_identity )
| ( b != additive_identity )
| ( bS_Ic @ ( c @ additive_inverse @ ( B @ sum ) ) ) ),
inference(simp,[status(thm)],[761]) ).
thf(789,plain,
( ( b != additive_identity )
| ( bS_Ic @ ( c @ additive_inverse @ ( additive_identity @ sum ) ) ) ),
inference(simp,[status(thm)],[779]) ).
thf(59,plain,
( ( ( aPc @ ( c @ ( a @ product ) ) )
!= ( aPb_S_IaPc @ ( bS_Ic @ ( a @ product ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[57,24]) ).
thf(60,plain,
( ( aPc @ ( c @ ( a @ product ) ) )
!= ( aPb_S_IaPc @ ( bS_Ic @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[59]) ).
thf(61,plain,
( ( aPc != aPb_S_IaPc )
| ( c != bS_Ic )
| ( a != a ) ),
inference(simp,[status(thm)],[60]) ).
thf(62,plain,
( ( aPc != aPb_S_IaPc )
| ( c != bS_Ic ) ),
inference(simp,[status(thm)],[61]) ).
thf(23777,plain,
! [A: $i] :
( ( A != aPc )
| ( aPb_S_IaPc != aPb_S_IaPc )
| ( c != bS_Ic )
| ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(paramod_ordered,[status(thm)],[23108,62]) ).
thf(23778,plain,
! [A: $i] :
( ( A != aPc )
| ( c != bS_Ic )
| ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(simp,[status(thm)],[23777]) ).
thf(23779,plain,
( ( c != bS_Ic )
| ~ ( aPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(pattern_uni,[status(thm)],[23778:[bind(A,$thf( aPc ))]]) ).
thf(24292,plain,
! [A: $i] :
( ( ( additive_identity @ ( A @ ( A @ additive_inverse @ sum ) ) )
!= ( aPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( c != bS_Ic )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[34,23779]) ).
thf(24293,plain,
! [A: $i] :
( ( ( additive_identity @ ( A @ ( A @ additive_inverse @ sum ) ) )
!= ( aPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( c != bS_Ic ) ),
inference(simp,[status(thm)],[24292]) ).
thf(24406,plain,
! [A: $i] :
( ( aPc != additive_identity )
| ( A
!= ( aPc @ additive_inverse ) )
| ( ( A @ additive_inverse )
!= aPb )
| ( c != bS_Ic ) ),
inference(simp,[status(thm)],[24293]) ).
thf(24422,plain,
( ( aPc != additive_identity )
| ( ( aPc @ additive_inverse @ additive_inverse )
!= aPb )
| ( c != bS_Ic ) ),
inference(simp,[status(thm)],[24406]) ).
thf(104,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( additive_identity @ ( A @ sum ) ) )
!= ( G @ ( E @ ( C @ sum ) ) ) )
| ( H @ ( F @ ( D @ sum ) ) )
| ~ ( H @ ( G @ ( B @ product ) ) )
| ~ $true
| ~ ( F @ ( E @ ( B @ product ) ) )
| ~ ( D @ ( C @ ( B @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,42]) ).
thf(105,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( additive_identity @ ( A @ sum ) ) )
!= ( G @ ( E @ ( C @ sum ) ) ) )
| ( H @ ( F @ ( D @ sum ) ) )
| ~ ( H @ ( G @ ( B @ product ) ) )
| ~ ( F @ ( E @ ( B @ product ) ) )
| ~ ( D @ ( C @ ( B @ product ) ) ) ),
inference(simp,[status(thm)],[104]) ).
thf(106,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ ( C @ sum ) ) )
| ~ ( E @ ( A @ ( B @ product ) ) )
| ~ ( D @ ( additive_identity @ ( B @ product ) ) )
| ~ ( C @ ( A @ ( B @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[105:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( D )),bind(E,$thf( additive_identity )),bind(F,$thf( F )),bind(G,$thf( A ))]]) ).
thf(132,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ ( C @ sum ) ) )
| ~ ( E @ ( A @ ( B @ product ) ) )
| ~ ( D @ ( additive_identity @ ( B @ product ) ) )
| ~ ( C @ ( A @ ( B @ product ) ) ) ),
inference(simp,[status(thm)],[106]) ).
thf(74,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( additive_identity @ ( A @ ( A @ additive_inverse @ sum ) ) )
!= ( G @ ( E @ ( C @ sum ) ) ) )
| ( H @ ( F @ ( D @ sum ) ) )
| ~ ( H @ ( G @ ( B @ product ) ) )
| ~ $true
| ~ ( F @ ( E @ ( B @ product ) ) )
| ~ ( D @ ( C @ ( B @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[34,42]) ).
thf(75,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( additive_identity @ ( A @ ( A @ additive_inverse @ sum ) ) )
!= ( G @ ( E @ ( C @ sum ) ) ) )
| ( H @ ( F @ ( D @ sum ) ) )
| ~ ( H @ ( G @ ( B @ product ) ) )
| ~ ( F @ ( E @ ( B @ product ) ) )
| ~ ( D @ ( C @ ( B @ product ) ) ) ),
inference(simp,[status(thm)],[74]) ).
thf(76,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ sum ) ) )
| ~ ( D @ ( additive_identity @ ( A @ product ) ) )
| ~ ( C @ ( E @ ( A @ product ) ) )
| ~ ( B @ ( E @ additive_inverse @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[75:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( I @ additive_inverse )),bind(D,$thf( D )),bind(E,$thf( I )),bind(F,$thf( F )),bind(G,$thf( additive_identity ))]]) ).
thf(133,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ sum ) ) )
| ~ ( D @ ( additive_identity @ ( A @ product ) ) )
| ~ ( C @ ( E @ ( A @ product ) ) )
| ~ ( B @ ( E @ additive_inverse @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[76]) ).
thf(25316,plain,
( ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( c != bS_Ic )
| ~ ( aPc @ ( aPb_S_IaPc @ ( aPb @ sum ) ) )
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[23850,23779]) ).
thf(25317,plain,
( ( c != bS_Ic )
| ~ ( aPc @ ( aPb_S_IaPc @ ( aPb @ sum ) ) )
| ( aPb != additive_identity ) ),
inference(pattern_uni,[status(thm)],[25316:[]]) ).
thf(24138,plain,
! [A: $i] :
( ( ( A @ ( A @ ( additive_identity @ sum ) ) )
!= ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( b != bS_Ic )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[38,23682]) ).
thf(24139,plain,
! [A: $i] :
( ( ( A @ ( A @ ( additive_identity @ sum ) ) )
!= ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( b != bS_Ic ) ),
inference(simp,[status(thm)],[24138]) ).
thf(24196,plain,
! [A: $i] :
( ( A != aPb )
| ( A
!= ( aPc @ additive_inverse ) )
| ( aPb != additive_identity )
| ( b != bS_Ic ) ),
inference(simp,[status(thm)],[24139]) ).
thf(24201,plain,
( ( ( aPc @ additive_inverse )
!= aPb )
| ( aPb != additive_identity )
| ( b != bS_Ic ) ),
inference(simp,[status(thm)],[24196]) ).
thf(3,axiom,
! [A: $i] : ( additive_identity @ ( A @ additive_inverse @ ( A @ sum ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_inverse) ).
thf(26,plain,
! [A: $i] : ( additive_identity @ ( A @ additive_inverse @ ( A @ sum ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(767,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( A @ additive_inverse @ ( A @ sum ) ) )
!= ( B @ ( additive_identity @ ( b @ sum ) ) ) )
| ( bS_Ic @ ( c @ additive_inverse @ ( B @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[26,678]) ).
thf(768,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( A @ additive_inverse @ ( A @ sum ) ) )
!= ( B @ ( additive_identity @ ( b @ sum ) ) ) )
| ( bS_Ic @ ( c @ additive_inverse @ ( B @ sum ) ) ) ),
inference(simp,[status(thm)],[767]) ).
thf(783,plain,
! [B: $i,A: $i] :
( ( additive_identity != B )
| ( ( A @ additive_inverse )
!= additive_identity )
| ( A != b )
| ( bS_Ic @ ( c @ additive_inverse @ ( B @ sum ) ) ) ),
inference(simp,[status(thm)],[768]) ).
thf(793,plain,
( ( ( b @ additive_inverse )
!= additive_identity )
| ( bS_Ic @ ( c @ additive_inverse @ ( additive_identity @ sum ) ) ) ),
inference(simp,[status(thm)],[783]) ).
thf(24157,plain,
! [A: $i] :
( ( ( additive_identity @ ( A @ additive_inverse @ ( A @ sum ) ) )
!= ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( b != bS_Ic )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[26,23682]) ).
thf(24158,plain,
! [A: $i] :
( ( ( additive_identity @ ( A @ additive_inverse @ ( A @ sum ) ) )
!= ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( b != bS_Ic ) ),
inference(simp,[status(thm)],[24157]) ).
thf(24194,plain,
! [A: $i] :
( ( aPb != additive_identity )
| ( ( A @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( A != aPb )
| ( b != bS_Ic ) ),
inference(simp,[status(thm)],[24158]) ).
thf(24200,plain,
( ( aPb != additive_identity )
| ( ( aPc @ additive_inverse )
!= ( aPb @ additive_inverse ) )
| ( b != bS_Ic ) ),
inference(simp,[status(thm)],[24194]) ).
thf(31147,plain,
( ( aPb != additive_identity )
| ( aPc != aPb )
| ( b != bS_Ic ) ),
inference(simp,[status(thm)],[24200]) ).
thf(747,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ add ) @ ( B @ ( A @ sum ) ) )
!= ( C @ ( additive_identity @ ( b @ sum ) ) ) )
| ( bS_Ic @ ( c @ additive_inverse @ ( C @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[29,678]) ).
thf(748,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ add ) @ ( B @ ( A @ sum ) ) )
!= ( C @ ( additive_identity @ ( b @ sum ) ) ) )
| ( bS_Ic @ ( c @ additive_inverse @ ( C @ sum ) ) ) ),
inference(simp,[status(thm)],[747]) ).
thf(749,plain,
bS_Ic @ ( c @ additive_inverse @ ( additive_identity @ ( b @ add ) @ sum ) ),
inference(pattern_uni,[status(thm)],[748:[bind(A,$thf( b )),bind(B,$thf( additive_identity )),bind(C,$thf( additive_identity @ ( b @ add ) ))]]) ).
thf(2494,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( additive_identity @ ( b @ add ) @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[749,28]) ).
thf(2495,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( additive_identity @ ( b @ add ) @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) ) ),
inference(simp,[status(thm)],[2494]) ).
thf(2496,plain,
bS_Ic @ ( additive_identity @ ( b @ add ) @ ( c @ additive_inverse @ sum ) ),
inference(pattern_uni,[status(thm)],[2495:[bind(A,$thf( additive_identity @ ( b @ add ) )),bind(B,$thf( c @ additive_inverse )),bind(C,$thf( bS_Ic ))]]) ).
thf(332,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ add ) @ ( B @ ( A @ sum ) ) )
!= ( E @ ( D @ ( C @ sum ) ) ) )
| ( E @ ( C @ ( D @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[29,28]) ).
thf(333,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ add ) @ ( B @ ( A @ sum ) ) )
!= ( E @ ( D @ ( C @ sum ) ) ) )
| ( E @ ( C @ ( D @ sum ) ) ) ),
inference(simp,[status(thm)],[332]) ).
thf(334,plain,
! [B: $i,A: $i] : ( B @ ( A @ add ) @ ( A @ ( B @ sum ) ) ),
inference(pattern_uni,[status(thm)],[333:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( F )),bind(D,$thf( G )),bind(E,$thf( G @ ( F @ add ) ))]]) ).
thf(345,plain,
! [B: $i,A: $i] : ( B @ ( A @ add ) @ ( A @ ( B @ sum ) ) ),
inference(simp,[status(thm)],[334]) ).
thf(30995,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ add ) @ ( A @ ( B @ sum ) ) )
!= ( bS_Ic @ ( a @ multiply ) @ ( aPb_S_IaPc @ ( aPb @ sum ) ) ) )
| ~ $true
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[345,25310]) ).
thf(30996,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ add ) @ ( A @ ( B @ sum ) ) )
!= ( bS_Ic @ ( a @ multiply ) @ ( aPb_S_IaPc @ ( aPb @ sum ) ) ) )
| ( aPb != additive_identity ) ),
inference(simp,[status(thm)],[30995]) ).
thf(31057,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ add ) )
!= ( bS_Ic @ ( a @ multiply ) ) )
| ( A != aPb_S_IaPc )
| ( B != aPb )
| ( aPb != additive_identity ) ),
inference(simp,[status(thm)],[30996]) ).
thf(31090,plain,
( ( ( bS_Ic @ ( a @ multiply ) )
!= ( aPb @ ( aPb_S_IaPc @ add ) ) )
| ( aPb != additive_identity ) ),
inference(simp,[status(thm)],[31057]) ).
thf(23580,plain,
! [A: $i] :
( ( A != aPc )
| ( aPb_S_IaPc @ ( c @ ( a @ product ) ) )
| ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(paramod_ordered,[status(thm)],[23108,57]) ).
thf(23581,plain,
( ( aPb_S_IaPc @ ( c @ ( a @ product ) ) )
| ~ ( aPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(pattern_uni,[status(thm)],[23580:[bind(A,$thf( aPc ))]]) ).
thf(23530,plain,
! [A: $i] :
( ( A
!= ( aPc @ additive_inverse ) )
| ( aPb_S_IaPc @ ( aPb_S_IaPc @ ( aPb @ sum ) ) )
| ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(paramod_ordered,[status(thm)],[23108,48]) ).
thf(23531,plain,
( ( aPb_S_IaPc @ ( aPb_S_IaPc @ ( aPb @ sum ) ) )
| ~ ( aPc @ additive_inverse @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(pattern_uni,[status(thm)],[23530:[bind(A,$thf( aPc @ additive_inverse ))]]) ).
thf(31299,plain,
( ( ( aPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc @ ( c @ ( a @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,23581]) ).
thf(31300,plain,
( ( ( aPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc @ ( c @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[31299]) ).
thf(31349,plain,
( ( aPc != aPb_S_IaPc )
| ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( aPb != aPb )
| ( aPb_S_IaPc @ ( c @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[31300]) ).
thf(31378,plain,
( ( aPc != aPb_S_IaPc )
| ( aPb_S_IaPc @ ( c @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[31349]) ).
thf(7,axiom,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ ( A @ sum ) ) )
| ~ ( F @ ( D @ ( C @ sum ) ) )
| ~ ( E @ ( D @ ( B @ sum ) ) )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_addition1) ).
thf(32,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ ( A @ sum ) ) )
| ~ ( F @ ( D @ ( C @ sum ) ) )
| ~ ( E @ ( D @ ( B @ sum ) ) )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(33,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ ( A @ sum ) ) )
| ~ ( F @ ( D @ ( C @ sum ) ) )
| ~ ( E @ ( D @ ( B @ sum ) ) )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
inference(cnf,[status(esa)],[32]) ).
thf(23736,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( A @ additive_inverse @ ( A @ sum ) ) )
!= ( B @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ~ $true
| ( aPb_S_IaPc = B ) ),
inference(paramod_ordered,[status(thm)],[26,23108]) ).
thf(23737,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( A @ additive_inverse @ ( A @ sum ) ) )
!= ( B @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc = B ) ),
inference(simp,[status(thm)],[23736]) ).
thf(23818,plain,
! [B: $i,A: $i] :
( ( additive_identity != B )
| ( ( A @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( A != aPb )
| ( aPb_S_IaPc = B ) ),
inference(simp,[status(thm)],[23737]) ).
thf(23841,plain,
( ( ( aPc @ additive_inverse )
!= ( aPb @ additive_inverse ) )
| ( additive_identity = aPb_S_IaPc ) ),
inference(simp,[status(thm)],[23818]) ).
thf(41007,plain,
( ( ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb_S_IaPc @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,23535]) ).
thf(41008,plain,
( ( ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb_S_IaPc @ sum ) ) ) ),
inference(simp,[status(thm)],[41007]) ).
thf(41070,plain,
( ( aPb != aPb_S_IaPc )
| ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( aPb != aPb )
| ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb_S_IaPc @ sum ) ) ) ),
inference(simp,[status(thm)],[41008]) ).
thf(41105,plain,
( ( aPb != aPb_S_IaPc )
| ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb_S_IaPc @ sum ) ) ) ),
inference(simp,[status(thm)],[41070]) ).
thf(41684,plain,
! [C: $i,B: $i,A: $i] :
( ( ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb_S_IaPc @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ~ $true
| ( aPb != aPb_S_IaPc ) ),
inference(paramod_ordered,[status(thm)],[41105,28]) ).
thf(41685,plain,
! [C: $i,B: $i,A: $i] :
( ( ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb_S_IaPc @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ( aPb != aPb_S_IaPc ) ),
inference(simp,[status(thm)],[41684]) ).
thf(41686,plain,
( ( aPb_S_IaPc @ ( aPb_S_IaPc @ ( aPc @ additive_inverse @ sum ) ) )
| ( aPb != aPb_S_IaPc ) ),
inference(pattern_uni,[status(thm)],[41685:[bind(A,$thf( aPb_S_IaPc )),bind(B,$thf( aPc @ additive_inverse )),bind(C,$thf( aPb_S_IaPc ))]]) ).
thf(101,plain,
! [N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( G @ ( E @ ( C @ sum ) ) )
!= ( M @ ( K @ ( I @ sum ) ) ) )
| ( N @ ( L @ ( J @ sum ) ) )
| ~ ( N @ ( M @ ( H @ product ) ) )
| ~ $true
| ~ ( L @ ( K @ ( H @ product ) ) )
| ~ ( J @ ( I @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,42]) ).
thf(102,plain,
! [N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( G @ ( E @ ( C @ sum ) ) )
!= ( M @ ( K @ ( I @ sum ) ) ) )
| ( N @ ( L @ ( J @ sum ) ) )
| ~ ( N @ ( M @ ( H @ product ) ) )
| ~ ( L @ ( K @ ( H @ product ) ) )
| ~ ( J @ ( I @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[101]) ).
thf(103,plain,
! [K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( K @ ( J @ ( I @ sum ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[102:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( H )),bind(I,$thf( C )),bind(J,$thf( J )),bind(K,$thf( E )),bind(L,$thf( L )),bind(M,$thf( G ))]]) ).
thf(130,plain,
! [K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( K @ ( J @ ( I @ sum ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[103]) ).
thf(172,plain,
! [V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( K @ ( J @ ( I @ sum ) ) )
!= ( Q @ ( O @ ( M @ sum ) ) ) )
| ( V @ ( U @ ( T @ sum ) ) )
| ~ ( V @ ( R @ ( S @ product ) ) )
| ~ ( U @ ( P @ ( S @ product ) ) )
| ~ ( T @ ( N @ ( S @ product ) ) )
| ~ ( R @ ( Q @ ( L @ product ) ) )
| ~ $true
| ~ ( P @ ( O @ ( L @ product ) ) )
| ~ ( N @ ( M @ ( L @ product ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[130,130]) ).
thf(173,plain,
! [V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( K @ ( J @ ( I @ sum ) ) )
!= ( Q @ ( O @ ( M @ sum ) ) ) )
| ( V @ ( U @ ( T @ sum ) ) )
| ~ ( V @ ( R @ ( S @ product ) ) )
| ~ ( U @ ( P @ ( S @ product ) ) )
| ~ ( T @ ( N @ ( S @ product ) ) )
| ~ ( R @ ( Q @ ( L @ product ) ) )
| ~ ( P @ ( O @ ( L @ product ) ) )
| ~ ( N @ ( M @ ( L @ product ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[172]) ).
thf(174,plain,
! [S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( S @ ( R @ ( Q @ sum ) ) )
| ~ ( S @ ( O @ ( P @ product ) ) )
| ~ ( R @ ( N @ ( P @ product ) ) )
| ~ ( Q @ ( M @ ( P @ product ) ) )
| ~ ( O @ ( K @ ( L @ product ) ) )
| ~ ( N @ ( J @ ( L @ product ) ) )
| ~ ( M @ ( I @ ( L @ product ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[173:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( H )),bind(I,$thf( I )),bind(J,$thf( J )),bind(K,$thf( K )),bind(L,$thf( L )),bind(M,$thf( I )),bind(N,$thf( N )),bind(O,$thf( J )),bind(P,$thf( P )),bind(Q,$thf( K ))]]) ).
thf(290,plain,
! [S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( S @ ( R @ ( Q @ sum ) ) )
| ~ ( S @ ( O @ ( P @ product ) ) )
| ~ ( R @ ( N @ ( P @ product ) ) )
| ~ ( Q @ ( M @ ( P @ product ) ) )
| ~ ( O @ ( K @ ( L @ product ) ) )
| ~ ( N @ ( J @ ( L @ product ) ) )
| ~ ( M @ ( I @ ( L @ product ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[174]) ).
thf(943,plain,
! [ZL: $i,ZK: $i,ZJ: $i,ZI: $i,ZH: $i,ZG: $i,ZF: $i,ZE: $i,ZD: $i,ZC: $i,ZB: $i,ZA: $i,Z: $i,Y: $i,X: $i,W: $i,V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( S @ ( R @ ( Q @ sum ) ) )
!= ( Y @ ( W @ ( U @ sum ) ) ) )
| ( ZL @ ( ZK @ ( ZJ @ sum ) ) )
| ~ ( ZL @ ( ZH @ ( ZI @ product ) ) )
| ~ ( ZK @ ( ZG @ ( ZI @ product ) ) )
| ~ ( ZJ @ ( ZF @ ( ZI @ product ) ) )
| ~ ( ZH @ ( ZD @ ( ZE @ product ) ) )
| ~ ( ZG @ ( ZC @ ( ZE @ product ) ) )
| ~ ( ZF @ ( ZB @ ( ZE @ product ) ) )
| ~ ( ZD @ ( Z @ ( ZA @ product ) ) )
| ~ ( ZC @ ( X @ ( ZA @ product ) ) )
| ~ ( ZB @ ( V @ ( ZA @ product ) ) )
| ~ ( Z @ ( Y @ ( T @ product ) ) )
| ~ $true
| ~ ( X @ ( W @ ( T @ product ) ) )
| ~ ( V @ ( U @ ( T @ product ) ) )
| ~ ( S @ ( O @ ( P @ product ) ) )
| ~ ( R @ ( N @ ( P @ product ) ) )
| ~ ( Q @ ( M @ ( P @ product ) ) )
| ~ ( O @ ( K @ ( L @ product ) ) )
| ~ ( N @ ( J @ ( L @ product ) ) )
| ~ ( M @ ( I @ ( L @ product ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[290,290]) ).
thf(944,plain,
! [ZL: $i,ZK: $i,ZJ: $i,ZI: $i,ZH: $i,ZG: $i,ZF: $i,ZE: $i,ZD: $i,ZC: $i,ZB: $i,ZA: $i,Z: $i,Y: $i,X: $i,W: $i,V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( S @ ( R @ ( Q @ sum ) ) )
!= ( Y @ ( W @ ( U @ sum ) ) ) )
| ( ZL @ ( ZK @ ( ZJ @ sum ) ) )
| ~ ( ZL @ ( ZH @ ( ZI @ product ) ) )
| ~ ( ZK @ ( ZG @ ( ZI @ product ) ) )
| ~ ( ZJ @ ( ZF @ ( ZI @ product ) ) )
| ~ ( ZH @ ( ZD @ ( ZE @ product ) ) )
| ~ ( ZG @ ( ZC @ ( ZE @ product ) ) )
| ~ ( ZF @ ( ZB @ ( ZE @ product ) ) )
| ~ ( ZD @ ( Z @ ( ZA @ product ) ) )
| ~ ( ZC @ ( X @ ( ZA @ product ) ) )
| ~ ( ZB @ ( V @ ( ZA @ product ) ) )
| ~ ( Z @ ( Y @ ( T @ product ) ) )
| ~ ( X @ ( W @ ( T @ product ) ) )
| ~ ( V @ ( U @ ( T @ product ) ) )
| ~ ( S @ ( O @ ( P @ product ) ) )
| ~ ( R @ ( N @ ( P @ product ) ) )
| ~ ( Q @ ( M @ ( P @ product ) ) )
| ~ ( O @ ( K @ ( L @ product ) ) )
| ~ ( N @ ( J @ ( L @ product ) ) )
| ~ ( M @ ( I @ ( L @ product ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[943]) ).
thf(945,plain,
! [ZI: $i,ZH: $i,ZG: $i,ZF: $i,ZE: $i,ZD: $i,ZC: $i,ZB: $i,ZA: $i,Z: $i,Y: $i,X: $i,W: $i,V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ZI @ ( ZH @ ( ZG @ sum ) ) )
| ~ ( ZI @ ( ZE @ ( ZF @ product ) ) )
| ~ ( ZH @ ( ZD @ ( ZF @ product ) ) )
| ~ ( ZG @ ( ZC @ ( ZF @ product ) ) )
| ~ ( ZE @ ( ZA @ ( ZB @ product ) ) )
| ~ ( ZD @ ( Z @ ( ZB @ product ) ) )
| ~ ( ZC @ ( Y @ ( ZB @ product ) ) )
| ~ ( ZA @ ( W @ ( X @ product ) ) )
| ~ ( Z @ ( V @ ( X @ product ) ) )
| ~ ( Y @ ( U @ ( X @ product ) ) )
| ~ ( W @ ( S @ ( T @ product ) ) )
| ~ ( V @ ( R @ ( T @ product ) ) )
| ~ ( U @ ( Q @ ( T @ product ) ) )
| ~ ( S @ ( O @ ( P @ product ) ) )
| ~ ( R @ ( N @ ( P @ product ) ) )
| ~ ( Q @ ( M @ ( P @ product ) ) )
| ~ ( O @ ( K @ ( L @ product ) ) )
| ~ ( N @ ( J @ ( L @ product ) ) )
| ~ ( M @ ( I @ ( L @ product ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[944:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( H )),bind(I,$thf( I )),bind(J,$thf( J )),bind(K,$thf( K )),bind(L,$thf( L )),bind(M,$thf( M )),bind(N,$thf( N )),bind(O,$thf( O )),bind(P,$thf( P )),bind(Q,$thf( Q )),bind(R,$thf( R )),bind(S,$thf( S )),bind(T,$thf( T )),bind(U,$thf( Q )),bind(V,$thf( V )),bind(W,$thf( R )),bind(X,$thf( X )),bind(Y,$thf( S ))]]) ).
thf(1234,plain,
! [ZI: $i,ZH: $i,ZG: $i,ZF: $i,ZE: $i,ZD: $i,ZC: $i,ZB: $i,ZA: $i,Z: $i,Y: $i,X: $i,W: $i,V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ZI @ ( ZH @ ( ZG @ sum ) ) )
| ~ ( ZI @ ( ZE @ ( ZF @ product ) ) )
| ~ ( ZH @ ( ZD @ ( ZF @ product ) ) )
| ~ ( ZG @ ( ZC @ ( ZF @ product ) ) )
| ~ ( ZE @ ( ZA @ ( ZB @ product ) ) )
| ~ ( ZD @ ( Z @ ( ZB @ product ) ) )
| ~ ( ZC @ ( Y @ ( ZB @ product ) ) )
| ~ ( ZA @ ( W @ ( X @ product ) ) )
| ~ ( Z @ ( V @ ( X @ product ) ) )
| ~ ( Y @ ( U @ ( X @ product ) ) )
| ~ ( W @ ( S @ ( T @ product ) ) )
| ~ ( V @ ( R @ ( T @ product ) ) )
| ~ ( U @ ( Q @ ( T @ product ) ) )
| ~ ( S @ ( O @ ( P @ product ) ) )
| ~ ( R @ ( N @ ( P @ product ) ) )
| ~ ( Q @ ( M @ ( P @ product ) ) )
| ~ ( O @ ( K @ ( L @ product ) ) )
| ~ ( N @ ( J @ ( L @ product ) ) )
| ~ ( M @ ( I @ ( L @ product ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[945]) ).
thf(30940,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ add ) @ ( B @ ( A @ sum ) ) )
!= ( bS_Ic @ ( a @ multiply ) @ ( aPb_S_IaPc @ ( aPb @ sum ) ) ) )
| ~ $true
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[29,25310]) ).
thf(30941,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ add ) @ ( B @ ( A @ sum ) ) )
!= ( bS_Ic @ ( a @ multiply ) @ ( aPb_S_IaPc @ ( aPb @ sum ) ) ) )
| ( aPb != additive_identity ) ),
inference(simp,[status(thm)],[30940]) ).
thf(31063,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ add ) )
!= ( bS_Ic @ ( a @ multiply ) ) )
| ( B != aPb_S_IaPc )
| ( A != aPb )
| ( aPb != additive_identity ) ),
inference(simp,[status(thm)],[30941]) ).
thf(31093,plain,
( ( ( bS_Ic @ ( a @ multiply ) )
!= ( aPb_S_IaPc @ ( aPb @ add ) ) )
| ( aPb != additive_identity ) ),
inference(simp,[status(thm)],[31063]) ).
thf(43612,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( b @ ( aPb_S_IaPc @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ~ $true
| ( ( c @ additive_inverse )
!= aPb_S_IaPc ) ),
inference(paramod_ordered,[status(thm)],[43517,28]) ).
thf(43613,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( b @ ( aPb_S_IaPc @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ( ( c @ additive_inverse )
!= aPb_S_IaPc ) ),
inference(simp,[status(thm)],[43612]) ).
thf(43614,plain,
( ( bS_Ic @ ( aPb_S_IaPc @ ( b @ sum ) ) )
| ( ( c @ additive_inverse )
!= aPb_S_IaPc ) ),
inference(pattern_uni,[status(thm)],[43613:[bind(A,$thf( aPb_S_IaPc )),bind(B,$thf( b )),bind(C,$thf( bS_Ic ))]]) ).
thf(317,plain,
! [C: $i,B: $i,A: $i] :
( ( ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,28]) ).
thf(318,plain,
! [C: $i,B: $i,A: $i] :
( ( ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) ) ),
inference(simp,[status(thm)],[317]) ).
thf(319,plain,
aPb_S_IaPc @ ( aPb @ ( aPc @ additive_inverse @ sum ) ),
inference(pattern_uni,[status(thm)],[318:[bind(A,$thf( aPb )),bind(B,$thf( aPc @ additive_inverse )),bind(C,$thf( aPb_S_IaPc ))]]) ).
thf(25324,plain,
( ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( aPb_S_IaPc @ ( aPb @ ( aPb_S_IaPc @ sum ) ) )
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[23850,319]) ).
thf(25325,plain,
( ( aPb_S_IaPc @ ( aPb @ ( aPb_S_IaPc @ sum ) ) )
| ( aPb != additive_identity ) ),
inference(pattern_uni,[status(thm)],[25324:[]]) ).
thf(23508,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( A @ ( A @ additive_inverse @ sum ) ) )
!= ( B @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ~ $true
| ( aPb_S_IaPc = B ) ),
inference(paramod_ordered,[status(thm)],[34,23108]) ).
thf(23509,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( A @ ( A @ additive_inverse @ sum ) ) )
!= ( B @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc = B ) ),
inference(simp,[status(thm)],[23508]) ).
thf(23812,plain,
! [B: $i,A: $i] :
( ( additive_identity != B )
| ( A
!= ( aPc @ additive_inverse ) )
| ( ( A @ additive_inverse )
!= aPb )
| ( aPb_S_IaPc = B ) ),
inference(simp,[status(thm)],[23509]) ).
thf(23832,plain,
( ( ( aPc @ additive_inverse @ additive_inverse )
!= aPb )
| ( additive_identity = aPb_S_IaPc ) ),
inference(simp,[status(thm)],[23812]) ).
thf(25280,plain,
( ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( b != bS_Ic )
| ~ ( aPb @ ( aPb_S_IaPc @ ( aPb @ sum ) ) )
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[23850,23682]) ).
thf(25281,plain,
( ( b != bS_Ic )
| ~ ( aPb @ ( aPb_S_IaPc @ ( aPb @ sum ) ) )
| ( aPb != additive_identity ) ),
inference(pattern_uni,[status(thm)],[25280:[]]) ).
thf(35941,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ add ) @ ( A @ ( B @ sum ) ) )
!= ( aPb @ ( aPb_S_IaPc @ ( aPb @ sum ) ) ) )
| ( b != bS_Ic )
| ~ $true
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[345,25281]) ).
thf(35942,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ add ) @ ( A @ ( B @ sum ) ) )
!= ( aPb @ ( aPb_S_IaPc @ ( aPb @ sum ) ) ) )
| ( b != bS_Ic )
| ( aPb != additive_identity ) ),
inference(simp,[status(thm)],[35941]) ).
thf(35986,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ add ) )
!= aPb )
| ( A != aPb_S_IaPc )
| ( B != aPb )
| ( b != bS_Ic )
| ( aPb != additive_identity ) ),
inference(simp,[status(thm)],[35942]) ).
thf(36020,plain,
( ( ( aPb @ ( aPb_S_IaPc @ add ) )
!= aPb )
| ( b != bS_Ic )
| ( aPb != additive_identity ) ),
inference(simp,[status(thm)],[35986]) ).
thf(24373,plain,
! [A: $i] :
( ( ( additive_identity @ ( A @ additive_inverse @ ( A @ sum ) ) )
!= ( aPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( c != bS_Ic )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[26,23779]) ).
thf(24374,plain,
! [A: $i] :
( ( ( additive_identity @ ( A @ additive_inverse @ ( A @ sum ) ) )
!= ( aPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( c != bS_Ic ) ),
inference(simp,[status(thm)],[24373]) ).
thf(24408,plain,
! [A: $i] :
( ( aPc != additive_identity )
| ( ( A @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( A != aPb )
| ( c != bS_Ic ) ),
inference(simp,[status(thm)],[24374]) ).
thf(24423,plain,
( ( aPc != additive_identity )
| ( ( aPc @ additive_inverse )
!= ( aPb @ additive_inverse ) )
| ( c != bS_Ic ) ),
inference(simp,[status(thm)],[24408]) ).
thf(35901,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ ( B @ sum ) ) )
!= ( aPb @ ( aPb_S_IaPc @ ( aPb @ sum ) ) ) )
| ( b != bS_Ic )
| ~ $true
| ( aPb != additive_identity )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,25281]) ).
thf(35902,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ ( B @ sum ) ) )
!= ( aPb @ ( aPb_S_IaPc @ ( aPb @ sum ) ) ) )
| ( b != bS_Ic )
| ( aPb != additive_identity )
| ~ ( C @ ( B @ ( A @ sum ) ) ) ),
inference(simp,[status(thm)],[35901]) ).
thf(35903,plain,
( ( b != bS_Ic )
| ( aPb != additive_identity )
| ~ ( aPb @ ( aPb @ ( aPb_S_IaPc @ sum ) ) ) ),
inference(pattern_uni,[status(thm)],[35902:[bind(A,$thf( aPb_S_IaPc )),bind(B,$thf( aPb )),bind(C,$thf( aPb ))]]) ).
thf(98,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( aPb @ ( b @ ( a @ product ) ) )
!= ( G @ ( F @ ( A @ product ) ) ) )
| ( G @ ( E @ ( C @ sum ) ) )
| ~ $true
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[58,42]) ).
thf(99,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( aPb @ ( b @ ( a @ product ) ) )
!= ( G @ ( F @ ( A @ product ) ) ) )
| ( G @ ( E @ ( C @ sum ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[98]) ).
thf(100,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( aPb @ ( D @ ( B @ sum ) ) )
| ~ ( b @ ( C @ ( A @ sum ) ) )
| ~ ( D @ ( C @ ( a @ product ) ) )
| ~ ( B @ ( A @ ( a @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[99:[bind(A,$thf( a )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( b )),bind(G,$thf( aPb ))]]) ).
thf(129,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( aPb @ ( D @ ( B @ sum ) ) )
| ~ ( b @ ( C @ ( A @ sum ) ) )
| ~ ( D @ ( C @ ( a @ product ) ) )
| ~ ( B @ ( A @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[100]) ).
thf(714,plain,
! [A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( b @ sum ) ) )
!= ( A @ ( additive_identity @ ( b @ sum ) ) ) )
| ( bS_Ic @ ( c @ additive_inverse @ ( A @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[53,678]) ).
thf(715,plain,
! [A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( b @ sum ) ) )
!= ( A @ ( additive_identity @ ( b @ sum ) ) ) )
| ( bS_Ic @ ( c @ additive_inverse @ ( A @ sum ) ) ) ),
inference(simp,[status(thm)],[714]) ).
thf(777,plain,
! [A: $i] :
( ( bS_Ic != A )
| ( ( c @ additive_inverse )
!= additive_identity )
| ( b != b )
| ( bS_Ic @ ( c @ additive_inverse @ ( A @ sum ) ) ) ),
inference(simp,[status(thm)],[715]) ).
thf(787,plain,
( ( ( c @ additive_inverse )
!= additive_identity )
| ( bS_Ic @ ( c @ additive_inverse @ ( bS_Ic @ sum ) ) ) ),
inference(simp,[status(thm)],[777]) ).
thf(3113,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( bS_Ic @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ~ $true
| ( ( c @ additive_inverse )
!= additive_identity ) ),
inference(paramod_ordered,[status(thm)],[787,28]) ).
thf(3114,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( bS_Ic @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ( ( c @ additive_inverse )
!= additive_identity ) ),
inference(simp,[status(thm)],[3113]) ).
thf(3115,plain,
( ( bS_Ic @ ( bS_Ic @ ( c @ additive_inverse @ sum ) ) )
| ( ( c @ additive_inverse )
!= additive_identity ) ),
inference(pattern_uni,[status(thm)],[3114:[bind(A,$thf( bS_Ic )),bind(B,$thf( c @ additive_inverse )),bind(C,$thf( bS_Ic ))]]) ).
thf(107,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( aPc @ ( c @ ( a @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( G @ ( E @ ( C @ sum ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[57,42]) ).
thf(108,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( aPc @ ( c @ ( a @ product ) ) )
!= ( C @ ( B @ ( A @ product ) ) ) )
| ( G @ ( E @ ( C @ sum ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[107]) ).
thf(109,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ ( aPc @ sum ) ) )
| ~ ( D @ ( C @ ( a @ product ) ) )
| ~ ( C @ ( A @ ( c @ sum ) ) )
| ~ ( B @ ( A @ ( a @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[108:[bind(A,$thf( a )),bind(B,$thf( c )),bind(C,$thf( aPc ))]]) ).
thf(134,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ ( aPc @ sum ) ) )
| ~ ( D @ ( C @ ( a @ product ) ) )
| ~ ( C @ ( A @ ( c @ sum ) ) )
| ~ ( B @ ( A @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[109]) ).
thf(95,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( aPb @ ( b @ ( a @ product ) ) )
!= ( E @ ( D @ ( A @ product ) ) ) )
| ( G @ ( E @ ( C @ sum ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ $true
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[58,42]) ).
thf(96,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( aPb @ ( b @ ( a @ product ) ) )
!= ( E @ ( D @ ( A @ product ) ) ) )
| ( G @ ( E @ ( C @ sum ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[95]) ).
thf(97,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( aPb @ ( B @ sum ) ) )
| ~ ( D @ ( C @ ( a @ product ) ) )
| ~ ( C @ ( b @ ( A @ sum ) ) )
| ~ ( B @ ( A @ ( a @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[96:[bind(A,$thf( a )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( b )),bind(E,$thf( aPb ))]]) ).
thf(128,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( aPb @ ( B @ sum ) ) )
| ~ ( D @ ( C @ ( a @ product ) ) )
| ~ ( C @ ( b @ ( A @ sum ) ) )
| ~ ( B @ ( A @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[97]) ).
thf(13,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C = D )
| ~ ( D @ ( B @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplication_is_well_defined) ).
thf(43,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C = D )
| ~ ( D @ ( B @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(44,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C = D )
| ~ ( D @ ( B @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[43]) ).
thf(45,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( B @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) )
| ( C = D ) ),
inference(lifteq,[status(thm)],[44]) ).
thf(23758,plain,
! [A: $i] :
( ( A != b )
| ( aPb @ ( aPb_S_IaPc @ ( a @ product ) ) )
| ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(paramod_ordered,[status(thm)],[23108,58]) ).
thf(23759,plain,
( ( aPb @ ( aPb_S_IaPc @ ( a @ product ) ) )
| ~ ( b @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(pattern_uni,[status(thm)],[23758:[bind(A,$thf( b ))]]) ).
thf(33970,plain,
( ( ( b @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb @ ( aPb_S_IaPc @ ( a @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,23759]) ).
thf(33971,plain,
( ( ( b @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb @ ( aPb_S_IaPc @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[33970]) ).
thf(34009,plain,
( ( b != aPb_S_IaPc )
| ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( aPb != aPb )
| ( aPb @ ( aPb_S_IaPc @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[33971]) ).
thf(34041,plain,
( ( b != aPb_S_IaPc )
| ( aPb @ ( aPb_S_IaPc @ ( a @ product ) ) ) ),
inference(simp,[status(thm)],[34009]) ).
thf(34606,plain,
( ( ( aPb @ ( aPb_S_IaPc @ ( a @ product ) ) )
!= ( aPb_S_IaPc @ ( bS_Ic @ ( a @ product ) ) ) )
| ~ $true
| ( b != aPb_S_IaPc ) ),
inference(paramod_ordered,[status(thm)],[34041,24]) ).
thf(34607,plain,
( ( ( aPb @ ( aPb_S_IaPc @ ( a @ product ) ) )
!= ( aPb_S_IaPc @ ( bS_Ic @ ( a @ product ) ) ) )
| ( b != aPb_S_IaPc ) ),
inference(simp,[status(thm)],[34606]) ).
thf(35253,plain,
( ( aPb != aPb_S_IaPc )
| ( aPb_S_IaPc != bS_Ic )
| ( a != a )
| ( b != aPb_S_IaPc ) ),
inference(simp,[status(thm)],[34607]) ).
thf(35444,plain,
( ( aPb != aPb_S_IaPc )
| ( aPb_S_IaPc != bS_Ic )
| ( b != aPb_S_IaPc ) ),
inference(simp,[status(thm)],[35253]) ).
thf(23528,plain,
! [A: $i] :
( ( A != aPc )
| ( aPb_S_IaPc @ ( aPb_S_IaPc @ additive_inverse @ ( aPb @ sum ) ) )
| ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(paramod_ordered,[status(thm)],[23108,48]) ).
thf(23529,plain,
( ( aPb_S_IaPc @ ( aPb_S_IaPc @ additive_inverse @ ( aPb @ sum ) ) )
| ~ ( aPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(pattern_uni,[status(thm)],[23528:[bind(A,$thf( aPc ))]]) ).
thf(39370,plain,
( ( ( aPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc @ ( aPb_S_IaPc @ additive_inverse @ ( aPb @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,23529]) ).
thf(39371,plain,
( ( ( aPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc @ ( aPb_S_IaPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(simp,[status(thm)],[39370]) ).
thf(39411,plain,
( ( aPc != aPb_S_IaPc )
| ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( aPb != aPb )
| ( aPb_S_IaPc @ ( aPb_S_IaPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(simp,[status(thm)],[39371]) ).
thf(39454,plain,
( ( aPc != aPb_S_IaPc )
| ( aPb_S_IaPc @ ( aPb_S_IaPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(simp,[status(thm)],[39411]) ).
thf(16,axiom,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( G @ ( E @ ( C @ sum ) ) )
| ~ ( G @ ( B @ ( F @ product ) ) )
| ~ ( F @ ( D @ ( A @ sum ) ) )
| ~ ( E @ ( B @ ( D @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distributivity3) ).
thf(49,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( G @ ( E @ ( C @ sum ) ) )
| ~ ( G @ ( B @ ( F @ product ) ) )
| ~ ( F @ ( D @ ( A @ sum ) ) )
| ~ ( E @ ( B @ ( D @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(24111,plain,
! [A: $i] :
( ( ( A @ ( additive_identity @ ( A @ sum ) ) )
!= ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( b != bS_Ic )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[25,23682]) ).
thf(24112,plain,
! [A: $i] :
( ( ( A @ ( additive_identity @ ( A @ sum ) ) )
!= ( aPb @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( b != bS_Ic ) ),
inference(simp,[status(thm)],[24111]) ).
thf(24189,plain,
! [A: $i] :
( ( A != aPb )
| ( ( aPc @ additive_inverse )
!= additive_identity )
| ( A != aPb )
| ( b != bS_Ic ) ),
inference(simp,[status(thm)],[24112]) ).
thf(24218,plain,
( ( ( aPc @ additive_inverse )
!= additive_identity )
| ( b != bS_Ic ) ),
inference(simp,[status(thm)],[24189]) ).
thf(762,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ add ) @ ( A @ ( B @ sum ) ) )
!= ( C @ ( additive_identity @ ( b @ sum ) ) ) )
| ( bS_Ic @ ( c @ additive_inverse @ ( C @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[345,678]) ).
thf(763,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ add ) @ ( A @ ( B @ sum ) ) )
!= ( C @ ( additive_identity @ ( b @ sum ) ) ) )
| ( bS_Ic @ ( c @ additive_inverse @ ( C @ sum ) ) ) ),
inference(simp,[status(thm)],[762]) ).
thf(764,plain,
bS_Ic @ ( c @ additive_inverse @ ( b @ ( additive_identity @ add ) @ sum ) ),
inference(pattern_uni,[status(thm)],[763:[bind(A,$thf( additive_identity )),bind(B,$thf( b )),bind(C,$thf( b @ ( additive_identity @ add ) ))]]) ).
thf(40354,plain,
( ( ( aPc @ additive_inverse @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc @ ( aPb_S_IaPc @ ( aPb @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,23531]) ).
thf(40355,plain,
( ( ( aPc @ additive_inverse @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc @ ( aPb_S_IaPc @ ( aPb @ sum ) ) ) ),
inference(simp,[status(thm)],[40354]) ).
thf(40416,plain,
( ( ( aPc @ additive_inverse )
!= aPb_S_IaPc )
| ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( aPb != aPb )
| ( aPb_S_IaPc @ ( aPb_S_IaPc @ ( aPb @ sum ) ) ) ),
inference(simp,[status(thm)],[40355]) ).
thf(40445,plain,
( ( ( aPc @ additive_inverse )
!= aPb_S_IaPc )
| ( aPb_S_IaPc @ ( aPb_S_IaPc @ ( aPb @ sum ) ) ) ),
inference(simp,[status(thm)],[40416]) ).
thf(40525,plain,
! [C: $i,B: $i,A: $i] :
( ( ( aPb_S_IaPc @ ( aPb_S_IaPc @ ( aPb @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ~ $true
| ( ( aPc @ additive_inverse )
!= aPb_S_IaPc ) ),
inference(paramod_ordered,[status(thm)],[40445,28]) ).
thf(40526,plain,
! [C: $i,B: $i,A: $i] :
( ( ( aPb_S_IaPc @ ( aPb_S_IaPc @ ( aPb @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ( ( aPc @ additive_inverse )
!= aPb_S_IaPc ) ),
inference(simp,[status(thm)],[40525]) ).
thf(40527,plain,
( ( aPb_S_IaPc @ ( aPb @ ( aPb_S_IaPc @ sum ) ) )
| ( ( aPc @ additive_inverse )
!= aPb_S_IaPc ) ),
inference(pattern_uni,[status(thm)],[40526:[bind(A,$thf( aPb )),bind(B,$thf( aPb_S_IaPc )),bind(C,$thf( aPb_S_IaPc ))]]) ).
thf(11,axiom,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( D @ ( C @ product ) ) )
| ~ ( F @ ( E @ ( A @ product ) ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_multiplication2) ).
thf(39,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( D @ ( C @ product ) ) )
| ~ ( F @ ( E @ ( A @ product ) ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(24010,plain,
! [A: $i] :
( ( ( additive_identity @ ( A @ additive_inverse @ ( A @ sum ) ) )
!= ( bS_Ic @ ( a @ multiply ) @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[26,23635]) ).
thf(24011,plain,
! [A: $i] :
( ( additive_identity @ ( A @ additive_inverse @ ( A @ sum ) ) )
!= ( bS_Ic @ ( a @ multiply ) @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(simp,[status(thm)],[24010]) ).
thf(24030,plain,
! [A: $i] :
( ( ( bS_Ic @ ( a @ multiply ) )
!= additive_identity )
| ( ( A @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( A != aPb ) ),
inference(simp,[status(thm)],[24011]) ).
thf(24062,plain,
( ( ( bS_Ic @ ( a @ multiply ) )
!= additive_identity )
| ( ( aPc @ additive_inverse )
!= ( aPb @ additive_inverse ) ) ),
inference(simp,[status(thm)],[24030]) ).
thf(28720,plain,
( ( ( bS_Ic @ ( a @ multiply ) )
!= additive_identity )
| ( aPc != aPb ) ),
inference(simp,[status(thm)],[24062]) ).
thf(77,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ multiply ) @ ( B @ ( A @ product ) ) )
!= ( E @ ( D @ ( C @ product ) ) ) )
| ( I @ ( G @ ( E @ sum ) ) )
| ~ ( I @ ( H @ ( C @ product ) ) )
| ~ ( H @ ( F @ ( D @ sum ) ) )
| ~ ( G @ ( F @ ( C @ product ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[54,42]) ).
thf(78,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ multiply ) @ ( B @ ( A @ product ) ) )
!= ( E @ ( D @ ( C @ product ) ) ) )
| ( I @ ( G @ ( E @ sum ) ) )
| ~ ( I @ ( H @ ( C @ product ) ) )
| ~ ( H @ ( F @ ( D @ sum ) ) )
| ~ ( G @ ( F @ ( C @ product ) ) ) ),
inference(simp,[status(thm)],[77]) ).
thf(79,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ ( F @ ( E @ multiply ) @ sum ) ) )
| ~ ( D @ ( C @ ( E @ product ) ) )
| ~ ( C @ ( A @ ( F @ sum ) ) )
| ~ ( B @ ( A @ ( E @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[78:[bind(A,$thf( J )),bind(B,$thf( K )),bind(C,$thf( J )),bind(D,$thf( K )),bind(E,$thf( K @ ( J @ multiply ) ))]]) ).
thf(135,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ ( F @ ( E @ multiply ) @ sum ) ) )
| ~ ( D @ ( C @ ( E @ product ) ) )
| ~ ( C @ ( A @ ( F @ sum ) ) )
| ~ ( B @ ( A @ ( E @ product ) ) ) ),
inference(simp,[status(thm)],[79]) ).
thf(23675,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ add ) @ ( A @ ( B @ sum ) ) )
!= ( C @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ~ $true
| ( aPb_S_IaPc = C ) ),
inference(paramod_ordered,[status(thm)],[345,23108]) ).
thf(23676,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ add ) @ ( A @ ( B @ sum ) ) )
!= ( C @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc = C ) ),
inference(simp,[status(thm)],[23675]) ).
thf(23677,plain,
( ( aPb @ ( aPc @ additive_inverse @ add ) )
= aPb_S_IaPc ),
inference(pattern_uni,[status(thm)],[23676:[bind(A,$thf( aPc @ additive_inverse )),bind(B,$thf( aPb )),bind(C,$thf( aPb @ ( aPc @ additive_inverse @ add ) ))]]) ).
thf(716,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( A @ ( A @ additive_inverse @ sum ) ) )
!= ( B @ ( additive_identity @ ( b @ sum ) ) ) )
| ( bS_Ic @ ( c @ additive_inverse @ ( B @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[34,678]) ).
thf(717,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( A @ ( A @ additive_inverse @ sum ) ) )
!= ( B @ ( additive_identity @ ( b @ sum ) ) ) )
| ( bS_Ic @ ( c @ additive_inverse @ ( B @ sum ) ) ) ),
inference(simp,[status(thm)],[716]) ).
thf(784,plain,
! [B: $i,A: $i] :
( ( additive_identity != B )
| ( A != additive_identity )
| ( ( A @ additive_inverse )
!= b )
| ( bS_Ic @ ( c @ additive_inverse @ ( B @ sum ) ) ) ),
inference(simp,[status(thm)],[717]) ).
thf(795,plain,
( ( ( additive_identity @ additive_inverse )
!= b )
| ( bS_Ic @ ( c @ additive_inverse @ ( additive_identity @ sum ) ) ) ),
inference(simp,[status(thm)],[784]) ).
thf(39532,plain,
! [C: $i,B: $i,A: $i] :
( ( ( aPb_S_IaPc @ ( aPb_S_IaPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ~ $true
| ( aPc != aPb_S_IaPc ) ),
inference(paramod_ordered,[status(thm)],[39454,28]) ).
thf(39533,plain,
! [C: $i,B: $i,A: $i] :
( ( ( aPb_S_IaPc @ ( aPb_S_IaPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ( aPc != aPb_S_IaPc ) ),
inference(simp,[status(thm)],[39532]) ).
thf(39534,plain,
( ( aPb_S_IaPc @ ( aPb @ ( aPb_S_IaPc @ additive_inverse @ sum ) ) )
| ( aPc != aPb_S_IaPc ) ),
inference(pattern_uni,[status(thm)],[39533:[bind(A,$thf( aPb )),bind(B,$thf( aPb_S_IaPc @ additive_inverse )),bind(C,$thf( aPb_S_IaPc ))]]) ).
thf(2580,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( additive_identity @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ~ $true
| ( b != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[789,28]) ).
thf(2581,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( additive_identity @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ( b != additive_identity ) ),
inference(simp,[status(thm)],[2580]) ).
thf(2582,plain,
( ( bS_Ic @ ( additive_identity @ ( c @ additive_inverse @ sum ) ) )
| ( b != additive_identity ) ),
inference(pattern_uni,[status(thm)],[2581:[bind(A,$thf( additive_identity )),bind(B,$thf( c @ additive_inverse )),bind(C,$thf( bS_Ic ))]]) ).
thf(23991,plain,
! [A: $i] :
( ( ( A @ ( A @ ( additive_identity @ sum ) ) )
!= ( bS_Ic @ ( a @ multiply ) @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[38,23635]) ).
thf(23992,plain,
! [A: $i] :
( ( A @ ( A @ ( additive_identity @ sum ) ) )
!= ( bS_Ic @ ( a @ multiply ) @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(simp,[status(thm)],[23991]) ).
thf(24036,plain,
! [A: $i] :
( ( A
!= ( bS_Ic @ ( a @ multiply ) ) )
| ( A
!= ( aPc @ additive_inverse ) )
| ( aPb != additive_identity ) ),
inference(simp,[status(thm)],[23992]) ).
thf(24066,plain,
( ( ( bS_Ic @ ( a @ multiply ) )
!= ( aPc @ additive_inverse ) )
| ( aPb != additive_identity ) ),
inference(simp,[status(thm)],[24036]) ).
thf(25318,plain,
( ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( ( aPb @ ( aPb_S_IaPc @ add ) )
= aPb_S_IaPc )
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[23850,23677]) ).
thf(25319,plain,
( ( ( aPb @ ( aPb_S_IaPc @ add ) )
= aPb_S_IaPc )
| ( aPb != additive_identity ) ),
inference(pattern_uni,[status(thm)],[25318:[]]) ).
thf(50,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( G @ ( E @ ( C @ sum ) ) )
| ~ ( G @ ( B @ ( F @ product ) ) )
| ~ ( F @ ( D @ ( A @ sum ) ) )
| ~ ( E @ ( B @ ( D @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[49]) ).
thf(24322,plain,
! [A: $i] :
( ( ( A @ ( additive_identity @ ( A @ sum ) ) )
!= ( aPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( c != bS_Ic )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[25,23779]) ).
thf(24323,plain,
! [A: $i] :
( ( ( A @ ( additive_identity @ ( A @ sum ) ) )
!= ( aPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( c != bS_Ic ) ),
inference(simp,[status(thm)],[24322]) ).
thf(24392,plain,
! [A: $i] :
( ( A != aPc )
| ( ( aPc @ additive_inverse )
!= additive_identity )
| ( A != aPb )
| ( c != bS_Ic ) ),
inference(simp,[status(thm)],[24323]) ).
thf(24417,plain,
( ( aPc != aPb )
| ( ( aPc @ additive_inverse )
!= additive_identity )
| ( c != bS_Ic ) ),
inference(simp,[status(thm)],[24392]) ).
thf(28370,plain,
( ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( aPc != aPb )
| ( additive_identity != aPb_S_IaPc )
| ( c != bS_Ic )
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[23850,24417]) ).
thf(28371,plain,
( ( aPc != aPb )
| ( additive_identity != aPb_S_IaPc )
| ( c != bS_Ic )
| ( aPb != additive_identity ) ),
inference(pattern_uni,[status(thm)],[28370:[]]) ).
thf(25272,plain,
! [A: $i] :
( ( ( aPc @ additive_inverse )
!= ( A @ additive_inverse ) )
| ( additive_identity @ ( A @ ( aPb_S_IaPc @ sum ) ) )
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[23850,34]) ).
thf(25273,plain,
( ( additive_identity @ ( aPc @ ( aPb_S_IaPc @ sum ) ) )
| ( aPb != additive_identity ) ),
inference(pattern_uni,[status(thm)],[25272:[bind(A,$thf( aPc ))]]) ).
thf(23569,plain,
! [B: $i,A: $i] :
( ( ( A @ ( additive_identity @ ( A @ sum ) ) )
!= ( B @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ~ $true
| ( aPb_S_IaPc = B ) ),
inference(paramod_ordered,[status(thm)],[25,23108]) ).
thf(23570,plain,
! [B: $i,A: $i] :
( ( ( A @ ( additive_identity @ ( A @ sum ) ) )
!= ( B @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( aPb_S_IaPc = B ) ),
inference(simp,[status(thm)],[23569]) ).
thf(23808,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( aPc @ additive_inverse )
!= additive_identity )
| ( A != aPb )
| ( aPb_S_IaPc = B ) ),
inference(simp,[status(thm)],[23570]) ).
thf(23826,plain,
( ( ( aPc @ additive_inverse )
!= additive_identity )
| ( aPb = aPb_S_IaPc ) ),
inference(simp,[status(thm)],[23808]) ).
thf(23925,plain,
! [A: $i] :
( ( ( additive_identity @ ( A @ ( A @ additive_inverse @ sum ) ) )
!= ( bS_Ic @ ( a @ multiply ) @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[34,23635]) ).
thf(23926,plain,
! [A: $i] :
( ( additive_identity @ ( A @ ( A @ additive_inverse @ sum ) ) )
!= ( bS_Ic @ ( a @ multiply ) @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(simp,[status(thm)],[23925]) ).
thf(24048,plain,
! [A: $i] :
( ( ( bS_Ic @ ( a @ multiply ) )
!= additive_identity )
| ( A
!= ( aPc @ additive_inverse ) )
| ( ( A @ additive_inverse )
!= aPb ) ),
inference(simp,[status(thm)],[23926]) ).
thf(24071,plain,
( ( ( bS_Ic @ ( a @ multiply ) )
!= additive_identity )
| ( ( aPc @ additive_inverse @ additive_inverse )
!= aPb ) ),
inference(simp,[status(thm)],[24048]) ).
thf(26416,plain,
( ( aPc != aPb )
| ( additive_identity = aPb_S_IaPc ) ),
inference(simp,[status(thm)],[23841]) ).
thf(24349,plain,
! [A: $i] :
( ( ( A @ ( A @ ( additive_identity @ sum ) ) )
!= ( aPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( c != bS_Ic )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[38,23779]) ).
thf(24350,plain,
! [A: $i] :
( ( ( A @ ( A @ ( additive_identity @ sum ) ) )
!= ( aPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( c != bS_Ic ) ),
inference(simp,[status(thm)],[24349]) ).
thf(24403,plain,
! [A: $i] :
( ( A != aPc )
| ( A
!= ( aPc @ additive_inverse ) )
| ( aPb != additive_identity )
| ( c != bS_Ic ) ),
inference(simp,[status(thm)],[24350]) ).
thf(24421,plain,
( ( ( aPc @ additive_inverse )
!= aPc )
| ( aPb != additive_identity )
| ( c != bS_Ic ) ),
inference(simp,[status(thm)],[24403]) ).
thf(25326,plain,
! [A: $i] :
( ( ( aPc @ additive_inverse )
!= ( A @ additive_inverse ) )
| ( additive_identity @ ( aPb_S_IaPc @ ( A @ sum ) ) )
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[23850,26]) ).
thf(25327,plain,
( ( additive_identity @ ( aPb_S_IaPc @ ( aPc @ sum ) ) )
| ( aPb != additive_identity ) ),
inference(pattern_uni,[status(thm)],[25326:[bind(A,$thf( aPc ))]]) ).
thf(40,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( D @ ( C @ product ) ) )
| ~ ( F @ ( E @ ( A @ product ) ) )
| ~ ( E @ ( D @ ( B @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[39]) ).
thf(31172,plain,
( ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( aPb != additive_identity )
| ( ( aPb @ additive_inverse )
!= aPb_S_IaPc )
| ( b != bS_Ic )
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[23850,24200]) ).
thf(31173,plain,
( ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( ( aPb @ additive_inverse )
!= aPb_S_IaPc )
| ( b != bS_Ic )
| ( aPb != additive_identity ) ),
inference(simp,[status(thm)],[31172]) ).
thf(31174,plain,
( ( ( aPb @ additive_inverse )
!= aPb_S_IaPc )
| ( b != bS_Ic )
| ( aPb != additive_identity ) ),
inference(pattern_uni,[status(thm)],[31173:[]]) ).
thf(23589,plain,
! [A: $i] :
( ( A != b )
| ( bS_Ic @ ( aPb_S_IaPc @ ( c @ additive_inverse @ sum ) ) )
| ~ ( A @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(paramod_ordered,[status(thm)],[23108,307]) ).
thf(23590,plain,
( ( bS_Ic @ ( aPb_S_IaPc @ ( c @ additive_inverse @ sum ) ) )
| ~ ( b @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) ),
inference(pattern_uni,[status(thm)],[23589:[bind(A,$thf( b ))]]) ).
thf(22297,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( additive_identity @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ~ $true
| ( ( b @ additive_inverse )
!= additive_identity ) ),
inference(paramod_ordered,[status(thm)],[793,28]) ).
thf(22298,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( additive_identity @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ( ( b @ additive_inverse )
!= additive_identity ) ),
inference(simp,[status(thm)],[22297]) ).
thf(22299,plain,
( ( bS_Ic @ ( additive_identity @ ( c @ additive_inverse @ sum ) ) )
| ( ( b @ additive_inverse )
!= additive_identity ) ),
inference(pattern_uni,[status(thm)],[22298:[bind(A,$thf( additive_identity )),bind(B,$thf( c @ additive_inverse )),bind(C,$thf( bS_Ic ))]]) ).
thf(25313,plain,
( ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( additive_identity != aPb_S_IaPc )
| ( b != bS_Ic )
| ( aPb != additive_identity ) ),
inference(paramod_ordered,[status(thm)],[23850,24218]) ).
thf(25314,plain,
( ( additive_identity != aPb_S_IaPc )
| ( b != bS_Ic )
| ( aPb != additive_identity ) ),
inference(pattern_uni,[status(thm)],[25313:[]]) ).
thf(1448,plain,
! [ZZR: $i,ZZQ: $i,ZZP: $i,ZZO: $i,ZZN: $i,ZZM: $i,ZZL: $i,ZZK: $i,ZZJ: $i,ZZI: $i,ZZH: $i,ZZG: $i,ZZF: $i,ZZE: $i,ZZD: $i,ZZC: $i,ZZB: $i,ZZA: $i,ZZ: $i,ZY: $i,ZX: $i,ZW: $i,ZV: $i,ZU: $i,ZT: $i,ZS: $i,ZR: $i,ZQ: $i,ZP: $i,ZO: $i,ZN: $i,ZM: $i,ZL: $i,ZK: $i,ZJ: $i,ZI: $i,ZH: $i,ZG: $i,ZF: $i,ZE: $i,ZD: $i,ZC: $i,ZB: $i,ZA: $i,Z: $i,Y: $i,X: $i,W: $i,V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( ZI @ ( ZH @ ( ZG @ sum ) ) )
!= ( ZO @ ( ZM @ ( ZK @ sum ) ) ) )
| ( ZZR @ ( ZZQ @ ( ZZP @ sum ) ) )
| ~ ( ZZR @ ( ZZN @ ( ZZO @ product ) ) )
| ~ ( ZZQ @ ( ZZM @ ( ZZO @ product ) ) )
| ~ ( ZZP @ ( ZZL @ ( ZZO @ product ) ) )
| ~ ( ZZN @ ( ZZJ @ ( ZZK @ product ) ) )
| ~ ( ZZM @ ( ZZI @ ( ZZK @ product ) ) )
| ~ ( ZZL @ ( ZZH @ ( ZZK @ product ) ) )
| ~ ( ZZJ @ ( ZZF @ ( ZZG @ product ) ) )
| ~ ( ZZI @ ( ZZE @ ( ZZG @ product ) ) )
| ~ ( ZZH @ ( ZZD @ ( ZZG @ product ) ) )
| ~ ( ZZF @ ( ZZB @ ( ZZC @ product ) ) )
| ~ ( ZZE @ ( ZZA @ ( ZZC @ product ) ) )
| ~ ( ZZD @ ( ZZ @ ( ZZC @ product ) ) )
| ~ ( ZZB @ ( ZX @ ( ZY @ product ) ) )
| ~ ( ZZA @ ( ZW @ ( ZY @ product ) ) )
| ~ ( ZZ @ ( ZV @ ( ZY @ product ) ) )
| ~ ( ZX @ ( ZT @ ( ZU @ product ) ) )
| ~ ( ZW @ ( ZS @ ( ZU @ product ) ) )
| ~ ( ZV @ ( ZR @ ( ZU @ product ) ) )
| ~ ( ZT @ ( ZP @ ( ZQ @ product ) ) )
| ~ ( ZS @ ( ZN @ ( ZQ @ product ) ) )
| ~ ( ZR @ ( ZL @ ( ZQ @ product ) ) )
| ~ ( ZP @ ( ZO @ ( ZJ @ product ) ) )
| ~ $true
| ~ ( ZN @ ( ZM @ ( ZJ @ product ) ) )
| ~ ( ZL @ ( ZK @ ( ZJ @ product ) ) )
| ~ ( ZI @ ( ZE @ ( ZF @ product ) ) )
| ~ ( ZH @ ( ZD @ ( ZF @ product ) ) )
| ~ ( ZG @ ( ZC @ ( ZF @ product ) ) )
| ~ ( ZE @ ( ZA @ ( ZB @ product ) ) )
| ~ ( ZD @ ( Z @ ( ZB @ product ) ) )
| ~ ( ZC @ ( Y @ ( ZB @ product ) ) )
| ~ ( ZA @ ( W @ ( X @ product ) ) )
| ~ ( Z @ ( V @ ( X @ product ) ) )
| ~ ( Y @ ( U @ ( X @ product ) ) )
| ~ ( W @ ( S @ ( T @ product ) ) )
| ~ ( V @ ( R @ ( T @ product ) ) )
| ~ ( U @ ( Q @ ( T @ product ) ) )
| ~ ( S @ ( O @ ( P @ product ) ) )
| ~ ( R @ ( N @ ( P @ product ) ) )
| ~ ( Q @ ( M @ ( P @ product ) ) )
| ~ ( O @ ( K @ ( L @ product ) ) )
| ~ ( N @ ( J @ ( L @ product ) ) )
| ~ ( M @ ( I @ ( L @ product ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[1234,1234]) ).
thf(1449,plain,
! [ZZR: $i,ZZQ: $i,ZZP: $i,ZZO: $i,ZZN: $i,ZZM: $i,ZZL: $i,ZZK: $i,ZZJ: $i,ZZI: $i,ZZH: $i,ZZG: $i,ZZF: $i,ZZE: $i,ZZD: $i,ZZC: $i,ZZB: $i,ZZA: $i,ZZ: $i,ZY: $i,ZX: $i,ZW: $i,ZV: $i,ZU: $i,ZT: $i,ZS: $i,ZR: $i,ZQ: $i,ZP: $i,ZO: $i,ZN: $i,ZM: $i,ZL: $i,ZK: $i,ZJ: $i,ZI: $i,ZH: $i,ZG: $i,ZF: $i,ZE: $i,ZD: $i,ZC: $i,ZB: $i,ZA: $i,Z: $i,Y: $i,X: $i,W: $i,V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( ZI @ ( ZH @ ( ZG @ sum ) ) )
!= ( ZO @ ( ZM @ ( ZK @ sum ) ) ) )
| ( ZZR @ ( ZZQ @ ( ZZP @ sum ) ) )
| ~ ( ZZR @ ( ZZN @ ( ZZO @ product ) ) )
| ~ ( ZZQ @ ( ZZM @ ( ZZO @ product ) ) )
| ~ ( ZZP @ ( ZZL @ ( ZZO @ product ) ) )
| ~ ( ZZN @ ( ZZJ @ ( ZZK @ product ) ) )
| ~ ( ZZM @ ( ZZI @ ( ZZK @ product ) ) )
| ~ ( ZZL @ ( ZZH @ ( ZZK @ product ) ) )
| ~ ( ZZJ @ ( ZZF @ ( ZZG @ product ) ) )
| ~ ( ZZI @ ( ZZE @ ( ZZG @ product ) ) )
| ~ ( ZZH @ ( ZZD @ ( ZZG @ product ) ) )
| ~ ( ZZF @ ( ZZB @ ( ZZC @ product ) ) )
| ~ ( ZZE @ ( ZZA @ ( ZZC @ product ) ) )
| ~ ( ZZD @ ( ZZ @ ( ZZC @ product ) ) )
| ~ ( ZZB @ ( ZX @ ( ZY @ product ) ) )
| ~ ( ZZA @ ( ZW @ ( ZY @ product ) ) )
| ~ ( ZZ @ ( ZV @ ( ZY @ product ) ) )
| ~ ( ZX @ ( ZT @ ( ZU @ product ) ) )
| ~ ( ZW @ ( ZS @ ( ZU @ product ) ) )
| ~ ( ZV @ ( ZR @ ( ZU @ product ) ) )
| ~ ( ZT @ ( ZP @ ( ZQ @ product ) ) )
| ~ ( ZS @ ( ZN @ ( ZQ @ product ) ) )
| ~ ( ZR @ ( ZL @ ( ZQ @ product ) ) )
| ~ ( ZP @ ( ZO @ ( ZJ @ product ) ) )
| ~ ( ZN @ ( ZM @ ( ZJ @ product ) ) )
| ~ ( ZL @ ( ZK @ ( ZJ @ product ) ) )
| ~ ( ZI @ ( ZE @ ( ZF @ product ) ) )
| ~ ( ZH @ ( ZD @ ( ZF @ product ) ) )
| ~ ( ZG @ ( ZC @ ( ZF @ product ) ) )
| ~ ( ZE @ ( ZA @ ( ZB @ product ) ) )
| ~ ( ZD @ ( Z @ ( ZB @ product ) ) )
| ~ ( ZC @ ( Y @ ( ZB @ product ) ) )
| ~ ( ZA @ ( W @ ( X @ product ) ) )
| ~ ( Z @ ( V @ ( X @ product ) ) )
| ~ ( Y @ ( U @ ( X @ product ) ) )
| ~ ( W @ ( S @ ( T @ product ) ) )
| ~ ( V @ ( R @ ( T @ product ) ) )
| ~ ( U @ ( Q @ ( T @ product ) ) )
| ~ ( S @ ( O @ ( P @ product ) ) )
| ~ ( R @ ( N @ ( P @ product ) ) )
| ~ ( Q @ ( M @ ( P @ product ) ) )
| ~ ( O @ ( K @ ( L @ product ) ) )
| ~ ( N @ ( J @ ( L @ product ) ) )
| ~ ( M @ ( I @ ( L @ product ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[1448]) ).
thf(1450,plain,
! [ZZO: $i,ZZN: $i,ZZM: $i,ZZL: $i,ZZK: $i,ZZJ: $i,ZZI: $i,ZZH: $i,ZZG: $i,ZZF: $i,ZZE: $i,ZZD: $i,ZZC: $i,ZZB: $i,ZZA: $i,ZZ: $i,ZY: $i,ZX: $i,ZW: $i,ZV: $i,ZU: $i,ZT: $i,ZS: $i,ZR: $i,ZQ: $i,ZP: $i,ZO: $i,ZN: $i,ZM: $i,ZL: $i,ZK: $i,ZJ: $i,ZI: $i,ZH: $i,ZG: $i,ZF: $i,ZE: $i,ZD: $i,ZC: $i,ZB: $i,ZA: $i,Z: $i,Y: $i,X: $i,W: $i,V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ZZO @ ( ZZN @ ( ZZM @ sum ) ) )
| ~ ( ZZO @ ( ZZK @ ( ZZL @ product ) ) )
| ~ ( ZZN @ ( ZZJ @ ( ZZL @ product ) ) )
| ~ ( ZZM @ ( ZZI @ ( ZZL @ product ) ) )
| ~ ( ZZK @ ( ZZG @ ( ZZH @ product ) ) )
| ~ ( ZZJ @ ( ZZF @ ( ZZH @ product ) ) )
| ~ ( ZZI @ ( ZZE @ ( ZZH @ product ) ) )
| ~ ( ZZG @ ( ZZC @ ( ZZD @ product ) ) )
| ~ ( ZZF @ ( ZZB @ ( ZZD @ product ) ) )
| ~ ( ZZE @ ( ZZA @ ( ZZD @ product ) ) )
| ~ ( ZZC @ ( ZY @ ( ZZ @ product ) ) )
| ~ ( ZZB @ ( ZX @ ( ZZ @ product ) ) )
| ~ ( ZZA @ ( ZW @ ( ZZ @ product ) ) )
| ~ ( ZY @ ( ZU @ ( ZV @ product ) ) )
| ~ ( ZX @ ( ZT @ ( ZV @ product ) ) )
| ~ ( ZW @ ( ZS @ ( ZV @ product ) ) )
| ~ ( ZU @ ( ZQ @ ( ZR @ product ) ) )
| ~ ( ZT @ ( ZP @ ( ZR @ product ) ) )
| ~ ( ZS @ ( ZO @ ( ZR @ product ) ) )
| ~ ( ZQ @ ( ZM @ ( ZN @ product ) ) )
| ~ ( ZP @ ( ZL @ ( ZN @ product ) ) )
| ~ ( ZO @ ( ZK @ ( ZN @ product ) ) )
| ~ ( ZM @ ( ZI @ ( ZJ @ product ) ) )
| ~ ( ZL @ ( ZH @ ( ZJ @ product ) ) )
| ~ ( ZK @ ( ZG @ ( ZJ @ product ) ) )
| ~ ( ZI @ ( ZE @ ( ZF @ product ) ) )
| ~ ( ZH @ ( ZD @ ( ZF @ product ) ) )
| ~ ( ZG @ ( ZC @ ( ZF @ product ) ) )
| ~ ( ZE @ ( ZA @ ( ZB @ product ) ) )
| ~ ( ZD @ ( Z @ ( ZB @ product ) ) )
| ~ ( ZC @ ( Y @ ( ZB @ product ) ) )
| ~ ( ZA @ ( W @ ( X @ product ) ) )
| ~ ( Z @ ( V @ ( X @ product ) ) )
| ~ ( Y @ ( U @ ( X @ product ) ) )
| ~ ( W @ ( S @ ( T @ product ) ) )
| ~ ( V @ ( R @ ( T @ product ) ) )
| ~ ( U @ ( Q @ ( T @ product ) ) )
| ~ ( S @ ( O @ ( P @ product ) ) )
| ~ ( R @ ( N @ ( P @ product ) ) )
| ~ ( Q @ ( M @ ( P @ product ) ) )
| ~ ( O @ ( K @ ( L @ product ) ) )
| ~ ( N @ ( J @ ( L @ product ) ) )
| ~ ( M @ ( I @ ( L @ product ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[1449:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( H )),bind(I,$thf( I )),bind(J,$thf( J )),bind(K,$thf( K )),bind(L,$thf( L )),bind(M,$thf( M )),bind(N,$thf( N )),bind(O,$thf( O )),bind(P,$thf( P )),bind(Q,$thf( Q )),bind(R,$thf( R )),bind(S,$thf( S )),bind(T,$thf( T )),bind(U,$thf( U )),bind(V,$thf( V )),bind(W,$thf( W )),bind(X,$thf( X )),bind(Y,$thf( Y )),bind(Z,$thf( Z )),bind(ZA,$thf( ZA )),bind(ZB,$thf( ZB )),bind(ZC,$thf( ZC )),bind(ZD,$thf( ZD )),bind(ZE,$thf( ZE )),bind(ZF,$thf( ZF )),bind(ZG,$thf( ZG )),bind(ZH,$thf( ZH )),bind(ZI,$thf( ZI )),bind(ZJ,$thf( ZJ )),bind(ZK,$thf( ZG )),bind(ZL,$thf( ZL )),bind(ZM,$thf( ZH )),bind(ZN,$thf( ZN )),bind(ZO,$thf( ZI ))]]) ).
thf(2362,plain,
! [ZZO: $i,ZZN: $i,ZZM: $i,ZZL: $i,ZZK: $i,ZZJ: $i,ZZI: $i,ZZH: $i,ZZG: $i,ZZF: $i,ZZE: $i,ZZD: $i,ZZC: $i,ZZB: $i,ZZA: $i,ZZ: $i,ZY: $i,ZX: $i,ZW: $i,ZV: $i,ZU: $i,ZT: $i,ZS: $i,ZR: $i,ZQ: $i,ZP: $i,ZO: $i,ZN: $i,ZM: $i,ZL: $i,ZK: $i,ZJ: $i,ZI: $i,ZH: $i,ZG: $i,ZF: $i,ZE: $i,ZD: $i,ZC: $i,ZB: $i,ZA: $i,Z: $i,Y: $i,X: $i,W: $i,V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ZZO @ ( ZZN @ ( ZZM @ sum ) ) )
| ~ ( ZZO @ ( ZZK @ ( ZZL @ product ) ) )
| ~ ( ZZN @ ( ZZJ @ ( ZZL @ product ) ) )
| ~ ( ZZM @ ( ZZI @ ( ZZL @ product ) ) )
| ~ ( ZZK @ ( ZZG @ ( ZZH @ product ) ) )
| ~ ( ZZJ @ ( ZZF @ ( ZZH @ product ) ) )
| ~ ( ZZI @ ( ZZE @ ( ZZH @ product ) ) )
| ~ ( ZZG @ ( ZZC @ ( ZZD @ product ) ) )
| ~ ( ZZF @ ( ZZB @ ( ZZD @ product ) ) )
| ~ ( ZZE @ ( ZZA @ ( ZZD @ product ) ) )
| ~ ( ZZC @ ( ZY @ ( ZZ @ product ) ) )
| ~ ( ZZB @ ( ZX @ ( ZZ @ product ) ) )
| ~ ( ZZA @ ( ZW @ ( ZZ @ product ) ) )
| ~ ( ZY @ ( ZU @ ( ZV @ product ) ) )
| ~ ( ZX @ ( ZT @ ( ZV @ product ) ) )
| ~ ( ZW @ ( ZS @ ( ZV @ product ) ) )
| ~ ( ZU @ ( ZQ @ ( ZR @ product ) ) )
| ~ ( ZT @ ( ZP @ ( ZR @ product ) ) )
| ~ ( ZS @ ( ZO @ ( ZR @ product ) ) )
| ~ ( ZQ @ ( ZM @ ( ZN @ product ) ) )
| ~ ( ZP @ ( ZL @ ( ZN @ product ) ) )
| ~ ( ZO @ ( ZK @ ( ZN @ product ) ) )
| ~ ( ZM @ ( ZI @ ( ZJ @ product ) ) )
| ~ ( ZL @ ( ZH @ ( ZJ @ product ) ) )
| ~ ( ZK @ ( ZG @ ( ZJ @ product ) ) )
| ~ ( ZI @ ( ZE @ ( ZF @ product ) ) )
| ~ ( ZH @ ( ZD @ ( ZF @ product ) ) )
| ~ ( ZG @ ( ZC @ ( ZF @ product ) ) )
| ~ ( ZE @ ( ZA @ ( ZB @ product ) ) )
| ~ ( ZD @ ( Z @ ( ZB @ product ) ) )
| ~ ( ZC @ ( Y @ ( ZB @ product ) ) )
| ~ ( ZA @ ( W @ ( X @ product ) ) )
| ~ ( Z @ ( V @ ( X @ product ) ) )
| ~ ( Y @ ( U @ ( X @ product ) ) )
| ~ ( W @ ( S @ ( T @ product ) ) )
| ~ ( V @ ( R @ ( T @ product ) ) )
| ~ ( U @ ( Q @ ( T @ product ) ) )
| ~ ( S @ ( O @ ( P @ product ) ) )
| ~ ( R @ ( N @ ( P @ product ) ) )
| ~ ( Q @ ( M @ ( P @ product ) ) )
| ~ ( O @ ( K @ ( L @ product ) ) )
| ~ ( N @ ( J @ ( L @ product ) ) )
| ~ ( M @ ( I @ ( L @ product ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[1450]) ).
thf(34124,plain,
( ( aPc != additive_identity )
| ( aPc != aPb )
| ( c != bS_Ic ) ),
inference(simp,[status(thm)],[24423]) ).
thf(2537,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( b @ ( additive_identity @ add ) @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[764,28]) ).
thf(2538,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( b @ ( additive_identity @ add ) @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) ) ),
inference(simp,[status(thm)],[2537]) ).
thf(2539,plain,
bS_Ic @ ( b @ ( additive_identity @ add ) @ ( c @ additive_inverse @ sum ) ),
inference(pattern_uni,[status(thm)],[2538:[bind(A,$thf( b @ ( additive_identity @ add ) )),bind(B,$thf( c @ additive_inverse )),bind(C,$thf( bS_Ic ))]]) ).
thf(71,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( b @ sum ) ) )
!= ( F @ ( D @ ( B @ sum ) ) ) )
| ( G @ ( E @ ( C @ sum ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ $true
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[53,42]) ).
thf(72,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( b @ sum ) ) )
!= ( F @ ( D @ ( B @ sum ) ) ) )
| ( G @ ( E @ ( C @ sum ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[71]) ).
thf(73,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ sum ) ) )
| ~ ( D @ ( bS_Ic @ ( A @ product ) ) )
| ~ ( C @ ( c @ additive_inverse @ ( A @ product ) ) )
| ~ ( B @ ( b @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[72:[bind(A,$thf( A )),bind(B,$thf( b )),bind(C,$thf( C )),bind(D,$thf( c @ additive_inverse )),bind(E,$thf( E )),bind(F,$thf( bS_Ic )),bind(G,$thf( G ))]]) ).
thf(131,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ sum ) ) )
| ~ ( D @ ( bS_Ic @ ( A @ product ) ) )
| ~ ( C @ ( c @ additive_inverse @ ( A @ product ) ) )
| ~ ( B @ ( b @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[73]) ).
thf(47,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( G @ ( F @ ( A @ product ) ) )
| ~ ( G @ ( E @ ( C @ sum ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(cnf,[status(esa)],[46]) ).
thf(22360,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( additive_identity @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ~ $true
| ( ( additive_identity @ additive_inverse )
!= b ) ),
inference(paramod_ordered,[status(thm)],[795,28]) ).
thf(22361,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bS_Ic @ ( c @ additive_inverse @ ( additive_identity @ sum ) ) )
!= ( C @ ( B @ ( A @ sum ) ) ) )
| ( C @ ( A @ ( B @ sum ) ) )
| ( ( additive_identity @ additive_inverse )
!= b ) ),
inference(simp,[status(thm)],[22360]) ).
thf(22362,plain,
( ( bS_Ic @ ( additive_identity @ ( c @ additive_inverse @ sum ) ) )
| ( ( additive_identity @ additive_inverse )
!= b ) ),
inference(pattern_uni,[status(thm)],[22361:[bind(A,$thf( additive_identity )),bind(B,$thf( c @ additive_inverse )),bind(C,$thf( bS_Ic ))]]) ).
thf(3532,plain,
! [ZZZZZD: $i,ZZZZZC: $i,ZZZZZB: $i,ZZZZZA: $i,ZZZZZ: $i,ZZZZY: $i,ZZZZX: $i,ZZZZW: $i,ZZZZV: $i,ZZZZU: $i,ZZZZT: $i,ZZZZS: $i,ZZZZR: $i,ZZZZQ: $i,ZZZZP: $i,ZZZZO: $i,ZZZZN: $i,ZZZZM: $i,ZZZZL: $i,ZZZZK: $i,ZZZZJ: $i,ZZZZI: $i,ZZZZH: $i,ZZZZG: $i,ZZZZF: $i,ZZZZE: $i,ZZZZD: $i,ZZZZC: $i,ZZZZB: $i,ZZZZA: $i,ZZZZ: $i,ZZZY: $i,ZZZX: $i,ZZZW: $i,ZZZV: $i,ZZZU: $i,ZZZT: $i,ZZZS: $i,ZZZR: $i,ZZZQ: $i,ZZZP: $i,ZZZO: $i,ZZZN: $i,ZZZM: $i,ZZZL: $i,ZZZK: $i,ZZZJ: $i,ZZZI: $i,ZZZH: $i,ZZZG: $i,ZZZF: $i,ZZZE: $i,ZZZD: $i,ZZZC: $i,ZZZB: $i,ZZZA: $i,ZZZ: $i,ZZY: $i,ZZX: $i,ZZW: $i,ZZV: $i,ZZU: $i,ZZT: $i,ZZS: $i,ZZR: $i,ZZQ: $i,ZZP: $i,ZZO: $i,ZZN: $i,ZZM: $i,ZZL: $i,ZZK: $i,ZZJ: $i,ZZI: $i,ZZH: $i,ZZG: $i,ZZF: $i,ZZE: $i,ZZD: $i,ZZC: $i,ZZB: $i,ZZA: $i,ZZ: $i,ZY: $i,ZX: $i,ZW: $i,ZV: $i,ZU: $i,ZT: $i,ZS: $i,ZR: $i,ZQ: $i,ZP: $i,ZO: $i,ZN: $i,ZM: $i,ZL: $i,ZK: $i,ZJ: $i,ZI: $i,ZH: $i,ZG: $i,ZF: $i,ZE: $i,ZD: $i,ZC: $i,ZB: $i,ZA: $i,Z: $i,Y: $i,X: $i,W: $i,V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( ZZO @ ( ZZN @ ( ZZM @ sum ) ) )
!= ( ZZU @ ( ZZS @ ( ZZQ @ sum ) ) ) )
| ( ZZZZZD @ ( ZZZZZC @ ( ZZZZZB @ sum ) ) )
| ~ ( ZZZZZD @ ( ZZZZZ @ ( ZZZZZA @ product ) ) )
| ~ ( ZZZZZC @ ( ZZZZY @ ( ZZZZZA @ product ) ) )
| ~ ( ZZZZZB @ ( ZZZZX @ ( ZZZZZA @ product ) ) )
| ~ ( ZZZZZ @ ( ZZZZV @ ( ZZZZW @ product ) ) )
| ~ ( ZZZZY @ ( ZZZZU @ ( ZZZZW @ product ) ) )
| ~ ( ZZZZX @ ( ZZZZT @ ( ZZZZW @ product ) ) )
| ~ ( ZZZZV @ ( ZZZZR @ ( ZZZZS @ product ) ) )
| ~ ( ZZZZU @ ( ZZZZQ @ ( ZZZZS @ product ) ) )
| ~ ( ZZZZT @ ( ZZZZP @ ( ZZZZS @ product ) ) )
| ~ ( ZZZZR @ ( ZZZZN @ ( ZZZZO @ product ) ) )
| ~ ( ZZZZQ @ ( ZZZZM @ ( ZZZZO @ product ) ) )
| ~ ( ZZZZP @ ( ZZZZL @ ( ZZZZO @ product ) ) )
| ~ ( ZZZZN @ ( ZZZZJ @ ( ZZZZK @ product ) ) )
| ~ ( ZZZZM @ ( ZZZZI @ ( ZZZZK @ product ) ) )
| ~ ( ZZZZL @ ( ZZZZH @ ( ZZZZK @ product ) ) )
| ~ ( ZZZZJ @ ( ZZZZF @ ( ZZZZG @ product ) ) )
| ~ ( ZZZZI @ ( ZZZZE @ ( ZZZZG @ product ) ) )
| ~ ( ZZZZH @ ( ZZZZD @ ( ZZZZG @ product ) ) )
| ~ ( ZZZZF @ ( ZZZZB @ ( ZZZZC @ product ) ) )
| ~ ( ZZZZE @ ( ZZZZA @ ( ZZZZC @ product ) ) )
| ~ ( ZZZZD @ ( ZZZZ @ ( ZZZZC @ product ) ) )
| ~ ( ZZZZB @ ( ZZZX @ ( ZZZY @ product ) ) )
| ~ ( ZZZZA @ ( ZZZW @ ( ZZZY @ product ) ) )
| ~ ( ZZZZ @ ( ZZZV @ ( ZZZY @ product ) ) )
| ~ ( ZZZX @ ( ZZZT @ ( ZZZU @ product ) ) )
| ~ ( ZZZW @ ( ZZZS @ ( ZZZU @ product ) ) )
| ~ ( ZZZV @ ( ZZZR @ ( ZZZU @ product ) ) )
| ~ ( ZZZT @ ( ZZZP @ ( ZZZQ @ product ) ) )
| ~ ( ZZZS @ ( ZZZO @ ( ZZZQ @ product ) ) )
| ~ ( ZZZR @ ( ZZZN @ ( ZZZQ @ product ) ) )
| ~ ( ZZZP @ ( ZZZL @ ( ZZZM @ product ) ) )
| ~ ( ZZZO @ ( ZZZK @ ( ZZZM @ product ) ) )
| ~ ( ZZZN @ ( ZZZJ @ ( ZZZM @ product ) ) )
| ~ ( ZZZL @ ( ZZZH @ ( ZZZI @ product ) ) )
| ~ ( ZZZK @ ( ZZZG @ ( ZZZI @ product ) ) )
| ~ ( ZZZJ @ ( ZZZF @ ( ZZZI @ product ) ) )
| ~ ( ZZZH @ ( ZZZD @ ( ZZZE @ product ) ) )
| ~ ( ZZZG @ ( ZZZC @ ( ZZZE @ product ) ) )
| ~ ( ZZZF @ ( ZZZB @ ( ZZZE @ product ) ) )
| ~ ( ZZZD @ ( ZZZ @ ( ZZZA @ product ) ) )
| ~ ( ZZZC @ ( ZZY @ ( ZZZA @ product ) ) )
| ~ ( ZZZB @ ( ZZX @ ( ZZZA @ product ) ) )
| ~ ( ZZZ @ ( ZZV @ ( ZZW @ product ) ) )
| ~ ( ZZY @ ( ZZT @ ( ZZW @ product ) ) )
| ~ ( ZZX @ ( ZZR @ ( ZZW @ product ) ) )
| ~ ( ZZV @ ( ZZU @ ( ZZP @ product ) ) )
| ~ $true
| ~ ( ZZT @ ( ZZS @ ( ZZP @ product ) ) )
| ~ ( ZZR @ ( ZZQ @ ( ZZP @ product ) ) )
| ~ ( ZZO @ ( ZZK @ ( ZZL @ product ) ) )
| ~ ( ZZN @ ( ZZJ @ ( ZZL @ product ) ) )
| ~ ( ZZM @ ( ZZI @ ( ZZL @ product ) ) )
| ~ ( ZZK @ ( ZZG @ ( ZZH @ product ) ) )
| ~ ( ZZJ @ ( ZZF @ ( ZZH @ product ) ) )
| ~ ( ZZI @ ( ZZE @ ( ZZH @ product ) ) )
| ~ ( ZZG @ ( ZZC @ ( ZZD @ product ) ) )
| ~ ( ZZF @ ( ZZB @ ( ZZD @ product ) ) )
| ~ ( ZZE @ ( ZZA @ ( ZZD @ product ) ) )
| ~ ( ZZC @ ( ZY @ ( ZZ @ product ) ) )
| ~ ( ZZB @ ( ZX @ ( ZZ @ product ) ) )
| ~ ( ZZA @ ( ZW @ ( ZZ @ product ) ) )
| ~ ( ZY @ ( ZU @ ( ZV @ product ) ) )
| ~ ( ZX @ ( ZT @ ( ZV @ product ) ) )
| ~ ( ZW @ ( ZS @ ( ZV @ product ) ) )
| ~ ( ZU @ ( ZQ @ ( ZR @ product ) ) )
| ~ ( ZT @ ( ZP @ ( ZR @ product ) ) )
| ~ ( ZS @ ( ZO @ ( ZR @ product ) ) )
| ~ ( ZQ @ ( ZM @ ( ZN @ product ) ) )
| ~ ( ZP @ ( ZL @ ( ZN @ product ) ) )
| ~ ( ZO @ ( ZK @ ( ZN @ product ) ) )
| ~ ( ZM @ ( ZI @ ( ZJ @ product ) ) )
| ~ ( ZL @ ( ZH @ ( ZJ @ product ) ) )
| ~ ( ZK @ ( ZG @ ( ZJ @ product ) ) )
| ~ ( ZI @ ( ZE @ ( ZF @ product ) ) )
| ~ ( ZH @ ( ZD @ ( ZF @ product ) ) )
| ~ ( ZG @ ( ZC @ ( ZF @ product ) ) )
| ~ ( ZE @ ( ZA @ ( ZB @ product ) ) )
| ~ ( ZD @ ( Z @ ( ZB @ product ) ) )
| ~ ( ZC @ ( Y @ ( ZB @ product ) ) )
| ~ ( ZA @ ( W @ ( X @ product ) ) )
| ~ ( Z @ ( V @ ( X @ product ) ) )
| ~ ( Y @ ( U @ ( X @ product ) ) )
| ~ ( W @ ( S @ ( T @ product ) ) )
| ~ ( V @ ( R @ ( T @ product ) ) )
| ~ ( U @ ( Q @ ( T @ product ) ) )
| ~ ( S @ ( O @ ( P @ product ) ) )
| ~ ( R @ ( N @ ( P @ product ) ) )
| ~ ( Q @ ( M @ ( P @ product ) ) )
| ~ ( O @ ( K @ ( L @ product ) ) )
| ~ ( N @ ( J @ ( L @ product ) ) )
| ~ ( M @ ( I @ ( L @ product ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(paramod_ordered,[status(thm)],[2362,2362]) ).
thf(3533,plain,
! [ZZZZZD: $i,ZZZZZC: $i,ZZZZZB: $i,ZZZZZA: $i,ZZZZZ: $i,ZZZZY: $i,ZZZZX: $i,ZZZZW: $i,ZZZZV: $i,ZZZZU: $i,ZZZZT: $i,ZZZZS: $i,ZZZZR: $i,ZZZZQ: $i,ZZZZP: $i,ZZZZO: $i,ZZZZN: $i,ZZZZM: $i,ZZZZL: $i,ZZZZK: $i,ZZZZJ: $i,ZZZZI: $i,ZZZZH: $i,ZZZZG: $i,ZZZZF: $i,ZZZZE: $i,ZZZZD: $i,ZZZZC: $i,ZZZZB: $i,ZZZZA: $i,ZZZZ: $i,ZZZY: $i,ZZZX: $i,ZZZW: $i,ZZZV: $i,ZZZU: $i,ZZZT: $i,ZZZS: $i,ZZZR: $i,ZZZQ: $i,ZZZP: $i,ZZZO: $i,ZZZN: $i,ZZZM: $i,ZZZL: $i,ZZZK: $i,ZZZJ: $i,ZZZI: $i,ZZZH: $i,ZZZG: $i,ZZZF: $i,ZZZE: $i,ZZZD: $i,ZZZC: $i,ZZZB: $i,ZZZA: $i,ZZZ: $i,ZZY: $i,ZZX: $i,ZZW: $i,ZZV: $i,ZZU: $i,ZZT: $i,ZZS: $i,ZZR: $i,ZZQ: $i,ZZP: $i,ZZO: $i,ZZN: $i,ZZM: $i,ZZL: $i,ZZK: $i,ZZJ: $i,ZZI: $i,ZZH: $i,ZZG: $i,ZZF: $i,ZZE: $i,ZZD: $i,ZZC: $i,ZZB: $i,ZZA: $i,ZZ: $i,ZY: $i,ZX: $i,ZW: $i,ZV: $i,ZU: $i,ZT: $i,ZS: $i,ZR: $i,ZQ: $i,ZP: $i,ZO: $i,ZN: $i,ZM: $i,ZL: $i,ZK: $i,ZJ: $i,ZI: $i,ZH: $i,ZG: $i,ZF: $i,ZE: $i,ZD: $i,ZC: $i,ZB: $i,ZA: $i,Z: $i,Y: $i,X: $i,W: $i,V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( ZZO @ ( ZZN @ ( ZZM @ sum ) ) )
!= ( ZZU @ ( ZZS @ ( ZZQ @ sum ) ) ) )
| ( ZZZZZD @ ( ZZZZZC @ ( ZZZZZB @ sum ) ) )
| ~ ( ZZZZZD @ ( ZZZZZ @ ( ZZZZZA @ product ) ) )
| ~ ( ZZZZZC @ ( ZZZZY @ ( ZZZZZA @ product ) ) )
| ~ ( ZZZZZB @ ( ZZZZX @ ( ZZZZZA @ product ) ) )
| ~ ( ZZZZZ @ ( ZZZZV @ ( ZZZZW @ product ) ) )
| ~ ( ZZZZY @ ( ZZZZU @ ( ZZZZW @ product ) ) )
| ~ ( ZZZZX @ ( ZZZZT @ ( ZZZZW @ product ) ) )
| ~ ( ZZZZV @ ( ZZZZR @ ( ZZZZS @ product ) ) )
| ~ ( ZZZZU @ ( ZZZZQ @ ( ZZZZS @ product ) ) )
| ~ ( ZZZZT @ ( ZZZZP @ ( ZZZZS @ product ) ) )
| ~ ( ZZZZR @ ( ZZZZN @ ( ZZZZO @ product ) ) )
| ~ ( ZZZZQ @ ( ZZZZM @ ( ZZZZO @ product ) ) )
| ~ ( ZZZZP @ ( ZZZZL @ ( ZZZZO @ product ) ) )
| ~ ( ZZZZN @ ( ZZZZJ @ ( ZZZZK @ product ) ) )
| ~ ( ZZZZM @ ( ZZZZI @ ( ZZZZK @ product ) ) )
| ~ ( ZZZZL @ ( ZZZZH @ ( ZZZZK @ product ) ) )
| ~ ( ZZZZJ @ ( ZZZZF @ ( ZZZZG @ product ) ) )
| ~ ( ZZZZI @ ( ZZZZE @ ( ZZZZG @ product ) ) )
| ~ ( ZZZZH @ ( ZZZZD @ ( ZZZZG @ product ) ) )
| ~ ( ZZZZF @ ( ZZZZB @ ( ZZZZC @ product ) ) )
| ~ ( ZZZZE @ ( ZZZZA @ ( ZZZZC @ product ) ) )
| ~ ( ZZZZD @ ( ZZZZ @ ( ZZZZC @ product ) ) )
| ~ ( ZZZZB @ ( ZZZX @ ( ZZZY @ product ) ) )
| ~ ( ZZZZA @ ( ZZZW @ ( ZZZY @ product ) ) )
| ~ ( ZZZZ @ ( ZZZV @ ( ZZZY @ product ) ) )
| ~ ( ZZZX @ ( ZZZT @ ( ZZZU @ product ) ) )
| ~ ( ZZZW @ ( ZZZS @ ( ZZZU @ product ) ) )
| ~ ( ZZZV @ ( ZZZR @ ( ZZZU @ product ) ) )
| ~ ( ZZZT @ ( ZZZP @ ( ZZZQ @ product ) ) )
| ~ ( ZZZS @ ( ZZZO @ ( ZZZQ @ product ) ) )
| ~ ( ZZZR @ ( ZZZN @ ( ZZZQ @ product ) ) )
| ~ ( ZZZP @ ( ZZZL @ ( ZZZM @ product ) ) )
| ~ ( ZZZO @ ( ZZZK @ ( ZZZM @ product ) ) )
| ~ ( ZZZN @ ( ZZZJ @ ( ZZZM @ product ) ) )
| ~ ( ZZZL @ ( ZZZH @ ( ZZZI @ product ) ) )
| ~ ( ZZZK @ ( ZZZG @ ( ZZZI @ product ) ) )
| ~ ( ZZZJ @ ( ZZZF @ ( ZZZI @ product ) ) )
| ~ ( ZZZH @ ( ZZZD @ ( ZZZE @ product ) ) )
| ~ ( ZZZG @ ( ZZZC @ ( ZZZE @ product ) ) )
| ~ ( ZZZF @ ( ZZZB @ ( ZZZE @ product ) ) )
| ~ ( ZZZD @ ( ZZZ @ ( ZZZA @ product ) ) )
| ~ ( ZZZC @ ( ZZY @ ( ZZZA @ product ) ) )
| ~ ( ZZZB @ ( ZZX @ ( ZZZA @ product ) ) )
| ~ ( ZZZ @ ( ZZV @ ( ZZW @ product ) ) )
| ~ ( ZZY @ ( ZZT @ ( ZZW @ product ) ) )
| ~ ( ZZX @ ( ZZR @ ( ZZW @ product ) ) )
| ~ ( ZZV @ ( ZZU @ ( ZZP @ product ) ) )
| ~ ( ZZT @ ( ZZS @ ( ZZP @ product ) ) )
| ~ ( ZZR @ ( ZZQ @ ( ZZP @ product ) ) )
| ~ ( ZZO @ ( ZZK @ ( ZZL @ product ) ) )
| ~ ( ZZN @ ( ZZJ @ ( ZZL @ product ) ) )
| ~ ( ZZM @ ( ZZI @ ( ZZL @ product ) ) )
| ~ ( ZZK @ ( ZZG @ ( ZZH @ product ) ) )
| ~ ( ZZJ @ ( ZZF @ ( ZZH @ product ) ) )
| ~ ( ZZI @ ( ZZE @ ( ZZH @ product ) ) )
| ~ ( ZZG @ ( ZZC @ ( ZZD @ product ) ) )
| ~ ( ZZF @ ( ZZB @ ( ZZD @ product ) ) )
| ~ ( ZZE @ ( ZZA @ ( ZZD @ product ) ) )
| ~ ( ZZC @ ( ZY @ ( ZZ @ product ) ) )
| ~ ( ZZB @ ( ZX @ ( ZZ @ product ) ) )
| ~ ( ZZA @ ( ZW @ ( ZZ @ product ) ) )
| ~ ( ZY @ ( ZU @ ( ZV @ product ) ) )
| ~ ( ZX @ ( ZT @ ( ZV @ product ) ) )
| ~ ( ZW @ ( ZS @ ( ZV @ product ) ) )
| ~ ( ZU @ ( ZQ @ ( ZR @ product ) ) )
| ~ ( ZT @ ( ZP @ ( ZR @ product ) ) )
| ~ ( ZS @ ( ZO @ ( ZR @ product ) ) )
| ~ ( ZQ @ ( ZM @ ( ZN @ product ) ) )
| ~ ( ZP @ ( ZL @ ( ZN @ product ) ) )
| ~ ( ZO @ ( ZK @ ( ZN @ product ) ) )
| ~ ( ZM @ ( ZI @ ( ZJ @ product ) ) )
| ~ ( ZL @ ( ZH @ ( ZJ @ product ) ) )
| ~ ( ZK @ ( ZG @ ( ZJ @ product ) ) )
| ~ ( ZI @ ( ZE @ ( ZF @ product ) ) )
| ~ ( ZH @ ( ZD @ ( ZF @ product ) ) )
| ~ ( ZG @ ( ZC @ ( ZF @ product ) ) )
| ~ ( ZE @ ( ZA @ ( ZB @ product ) ) )
| ~ ( ZD @ ( Z @ ( ZB @ product ) ) )
| ~ ( ZC @ ( Y @ ( ZB @ product ) ) )
| ~ ( ZA @ ( W @ ( X @ product ) ) )
| ~ ( Z @ ( V @ ( X @ product ) ) )
| ~ ( Y @ ( U @ ( X @ product ) ) )
| ~ ( W @ ( S @ ( T @ product ) ) )
| ~ ( V @ ( R @ ( T @ product ) ) )
| ~ ( U @ ( Q @ ( T @ product ) ) )
| ~ ( S @ ( O @ ( P @ product ) ) )
| ~ ( R @ ( N @ ( P @ product ) ) )
| ~ ( Q @ ( M @ ( P @ product ) ) )
| ~ ( O @ ( K @ ( L @ product ) ) )
| ~ ( N @ ( J @ ( L @ product ) ) )
| ~ ( M @ ( I @ ( L @ product ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[3532]) ).
thf(3534,plain,
! [ZZZZZA: $i,ZZZZZ: $i,ZZZZY: $i,ZZZZX: $i,ZZZZW: $i,ZZZZV: $i,ZZZZU: $i,ZZZZT: $i,ZZZZS: $i,ZZZZR: $i,ZZZZQ: $i,ZZZZP: $i,ZZZZO: $i,ZZZZN: $i,ZZZZM: $i,ZZZZL: $i,ZZZZK: $i,ZZZZJ: $i,ZZZZI: $i,ZZZZH: $i,ZZZZG: $i,ZZZZF: $i,ZZZZE: $i,ZZZZD: $i,ZZZZC: $i,ZZZZB: $i,ZZZZA: $i,ZZZZ: $i,ZZZY: $i,ZZZX: $i,ZZZW: $i,ZZZV: $i,ZZZU: $i,ZZZT: $i,ZZZS: $i,ZZZR: $i,ZZZQ: $i,ZZZP: $i,ZZZO: $i,ZZZN: $i,ZZZM: $i,ZZZL: $i,ZZZK: $i,ZZZJ: $i,ZZZI: $i,ZZZH: $i,ZZZG: $i,ZZZF: $i,ZZZE: $i,ZZZD: $i,ZZZC: $i,ZZZB: $i,ZZZA: $i,ZZZ: $i,ZZY: $i,ZZX: $i,ZZW: $i,ZZV: $i,ZZU: $i,ZZT: $i,ZZS: $i,ZZR: $i,ZZQ: $i,ZZP: $i,ZZO: $i,ZZN: $i,ZZM: $i,ZZL: $i,ZZK: $i,ZZJ: $i,ZZI: $i,ZZH: $i,ZZG: $i,ZZF: $i,ZZE: $i,ZZD: $i,ZZC: $i,ZZB: $i,ZZA: $i,ZZ: $i,ZY: $i,ZX: $i,ZW: $i,ZV: $i,ZU: $i,ZT: $i,ZS: $i,ZR: $i,ZQ: $i,ZP: $i,ZO: $i,ZN: $i,ZM: $i,ZL: $i,ZK: $i,ZJ: $i,ZI: $i,ZH: $i,ZG: $i,ZF: $i,ZE: $i,ZD: $i,ZC: $i,ZB: $i,ZA: $i,Z: $i,Y: $i,X: $i,W: $i,V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ZZZZZA @ ( ZZZZZ @ ( ZZZZY @ sum ) ) )
| ~ ( ZZZZZA @ ( ZZZZW @ ( ZZZZX @ product ) ) )
| ~ ( ZZZZZ @ ( ZZZZV @ ( ZZZZX @ product ) ) )
| ~ ( ZZZZY @ ( ZZZZU @ ( ZZZZX @ product ) ) )
| ~ ( ZZZZW @ ( ZZZZS @ ( ZZZZT @ product ) ) )
| ~ ( ZZZZV @ ( ZZZZR @ ( ZZZZT @ product ) ) )
| ~ ( ZZZZU @ ( ZZZZQ @ ( ZZZZT @ product ) ) )
| ~ ( ZZZZS @ ( ZZZZO @ ( ZZZZP @ product ) ) )
| ~ ( ZZZZR @ ( ZZZZN @ ( ZZZZP @ product ) ) )
| ~ ( ZZZZQ @ ( ZZZZM @ ( ZZZZP @ product ) ) )
| ~ ( ZZZZO @ ( ZZZZK @ ( ZZZZL @ product ) ) )
| ~ ( ZZZZN @ ( ZZZZJ @ ( ZZZZL @ product ) ) )
| ~ ( ZZZZM @ ( ZZZZI @ ( ZZZZL @ product ) ) )
| ~ ( ZZZZK @ ( ZZZZG @ ( ZZZZH @ product ) ) )
| ~ ( ZZZZJ @ ( ZZZZF @ ( ZZZZH @ product ) ) )
| ~ ( ZZZZI @ ( ZZZZE @ ( ZZZZH @ product ) ) )
| ~ ( ZZZZG @ ( ZZZZC @ ( ZZZZD @ product ) ) )
| ~ ( ZZZZF @ ( ZZZZB @ ( ZZZZD @ product ) ) )
| ~ ( ZZZZE @ ( ZZZZA @ ( ZZZZD @ product ) ) )
| ~ ( ZZZZC @ ( ZZZY @ ( ZZZZ @ product ) ) )
| ~ ( ZZZZB @ ( ZZZX @ ( ZZZZ @ product ) ) )
| ~ ( ZZZZA @ ( ZZZW @ ( ZZZZ @ product ) ) )
| ~ ( ZZZY @ ( ZZZU @ ( ZZZV @ product ) ) )
| ~ ( ZZZX @ ( ZZZT @ ( ZZZV @ product ) ) )
| ~ ( ZZZW @ ( ZZZS @ ( ZZZV @ product ) ) )
| ~ ( ZZZU @ ( ZZZQ @ ( ZZZR @ product ) ) )
| ~ ( ZZZT @ ( ZZZP @ ( ZZZR @ product ) ) )
| ~ ( ZZZS @ ( ZZZO @ ( ZZZR @ product ) ) )
| ~ ( ZZZQ @ ( ZZZM @ ( ZZZN @ product ) ) )
| ~ ( ZZZP @ ( ZZZL @ ( ZZZN @ product ) ) )
| ~ ( ZZZO @ ( ZZZK @ ( ZZZN @ product ) ) )
| ~ ( ZZZM @ ( ZZZI @ ( ZZZJ @ product ) ) )
| ~ ( ZZZL @ ( ZZZH @ ( ZZZJ @ product ) ) )
| ~ ( ZZZK @ ( ZZZG @ ( ZZZJ @ product ) ) )
| ~ ( ZZZI @ ( ZZZE @ ( ZZZF @ product ) ) )
| ~ ( ZZZH @ ( ZZZD @ ( ZZZF @ product ) ) )
| ~ ( ZZZG @ ( ZZZC @ ( ZZZF @ product ) ) )
| ~ ( ZZZE @ ( ZZZA @ ( ZZZB @ product ) ) )
| ~ ( ZZZD @ ( ZZZ @ ( ZZZB @ product ) ) )
| ~ ( ZZZC @ ( ZZY @ ( ZZZB @ product ) ) )
| ~ ( ZZZA @ ( ZZW @ ( ZZX @ product ) ) )
| ~ ( ZZZ @ ( ZZV @ ( ZZX @ product ) ) )
| ~ ( ZZY @ ( ZZU @ ( ZZX @ product ) ) )
| ~ ( ZZW @ ( ZZS @ ( ZZT @ product ) ) )
| ~ ( ZZV @ ( ZZR @ ( ZZT @ product ) ) )
| ~ ( ZZU @ ( ZZQ @ ( ZZT @ product ) ) )
| ~ ( ZZS @ ( ZZO @ ( ZZP @ product ) ) )
| ~ ( ZZR @ ( ZZN @ ( ZZP @ product ) ) )
| ~ ( ZZQ @ ( ZZM @ ( ZZP @ product ) ) )
| ~ ( ZZO @ ( ZZK @ ( ZZL @ product ) ) )
| ~ ( ZZN @ ( ZZJ @ ( ZZL @ product ) ) )
| ~ ( ZZM @ ( ZZI @ ( ZZL @ product ) ) )
| ~ ( ZZK @ ( ZZG @ ( ZZH @ product ) ) )
| ~ ( ZZJ @ ( ZZF @ ( ZZH @ product ) ) )
| ~ ( ZZI @ ( ZZE @ ( ZZH @ product ) ) )
| ~ ( ZZG @ ( ZZC @ ( ZZD @ product ) ) )
| ~ ( ZZF @ ( ZZB @ ( ZZD @ product ) ) )
| ~ ( ZZE @ ( ZZA @ ( ZZD @ product ) ) )
| ~ ( ZZC @ ( ZY @ ( ZZ @ product ) ) )
| ~ ( ZZB @ ( ZX @ ( ZZ @ product ) ) )
| ~ ( ZZA @ ( ZW @ ( ZZ @ product ) ) )
| ~ ( ZY @ ( ZU @ ( ZV @ product ) ) )
| ~ ( ZX @ ( ZT @ ( ZV @ product ) ) )
| ~ ( ZW @ ( ZS @ ( ZV @ product ) ) )
| ~ ( ZU @ ( ZQ @ ( ZR @ product ) ) )
| ~ ( ZT @ ( ZP @ ( ZR @ product ) ) )
| ~ ( ZS @ ( ZO @ ( ZR @ product ) ) )
| ~ ( ZQ @ ( ZM @ ( ZN @ product ) ) )
| ~ ( ZP @ ( ZL @ ( ZN @ product ) ) )
| ~ ( ZO @ ( ZK @ ( ZN @ product ) ) )
| ~ ( ZM @ ( ZI @ ( ZJ @ product ) ) )
| ~ ( ZL @ ( ZH @ ( ZJ @ product ) ) )
| ~ ( ZK @ ( ZG @ ( ZJ @ product ) ) )
| ~ ( ZI @ ( ZE @ ( ZF @ product ) ) )
| ~ ( ZH @ ( ZD @ ( ZF @ product ) ) )
| ~ ( ZG @ ( ZC @ ( ZF @ product ) ) )
| ~ ( ZE @ ( ZA @ ( ZB @ product ) ) )
| ~ ( ZD @ ( Z @ ( ZB @ product ) ) )
| ~ ( ZC @ ( Y @ ( ZB @ product ) ) )
| ~ ( ZA @ ( W @ ( X @ product ) ) )
| ~ ( Z @ ( V @ ( X @ product ) ) )
| ~ ( Y @ ( U @ ( X @ product ) ) )
| ~ ( W @ ( S @ ( T @ product ) ) )
| ~ ( V @ ( R @ ( T @ product ) ) )
| ~ ( U @ ( Q @ ( T @ product ) ) )
| ~ ( S @ ( O @ ( P @ product ) ) )
| ~ ( R @ ( N @ ( P @ product ) ) )
| ~ ( Q @ ( M @ ( P @ product ) ) )
| ~ ( O @ ( K @ ( L @ product ) ) )
| ~ ( N @ ( J @ ( L @ product ) ) )
| ~ ( M @ ( I @ ( L @ product ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(pattern_uni,[status(thm)],[3533:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( H )),bind(I,$thf( I )),bind(J,$thf( J )),bind(K,$thf( K )),bind(L,$thf( L )),bind(M,$thf( M )),bind(N,$thf( N )),bind(O,$thf( O )),bind(P,$thf( P )),bind(Q,$thf( Q )),bind(R,$thf( R )),bind(S,$thf( S )),bind(T,$thf( T )),bind(U,$thf( U )),bind(V,$thf( V )),bind(W,$thf( W )),bind(X,$thf( X )),bind(Y,$thf( Y )),bind(Z,$thf( Z )),bind(ZA,$thf( ZA )),bind(ZB,$thf( ZB )),bind(ZC,$thf( ZC )),bind(ZD,$thf( ZD )),bind(ZE,$thf( ZE )),bind(ZF,$thf( ZF )),bind(ZG,$thf( ZG )),bind(ZH,$thf( ZH )),bind(ZI,$thf( ZI )),bind(ZJ,$thf( ZJ )),bind(ZK,$thf( ZK )),bind(ZL,$thf( ZL )),bind(ZM,$thf( ZM )),bind(ZN,$thf( ZN )),bind(ZO,$thf( ZO )),bind(ZP,$thf( ZP )),bind(ZQ,$thf( ZQ )),bind(ZR,$thf( ZR )),bind(ZS,$thf( ZS )),bind(ZT,$thf( ZT )),bind(ZU,$thf( ZU )),bind(ZV,$thf( ZV )),bind(ZW,$thf( ZW )),bind(ZX,$thf( ZX )),bind(ZY,$thf( ZY )),bind(ZZ,$thf( ZZ )),bind(ZZA,$thf( ZZA )),bind(ZZB,$thf( ZZB )),bind(ZZC,$thf( ZZC )),bind(ZZD,$thf( ZZD )),bind(ZZE,$thf( ZZE )),bind(ZZF,$thf( ZZF )),bind(ZZG,$thf( ZZG )),bind(ZZH,$thf( ZZH )),bind(ZZI,$thf( ZZI )),bind(ZZJ,$thf( ZZJ )),bind(ZZK,$thf( ZZK )),bind(ZZL,$thf( ZZL )),bind(ZZM,$thf( ZZM )),bind(ZZN,$thf( ZZN )),bind(ZZO,$thf( ZZO )),bind(ZZP,$thf( ZZP )),bind(ZZQ,$thf( ZZM )),bind(ZZR,$thf( ZZR )),bind(ZZS,$thf( ZZN )),bind(ZZT,$thf( ZZT )),bind(ZZU,$thf( ZZO ))]]) ).
thf(6839,plain,
! [ZZZZZA: $i,ZZZZZ: $i,ZZZZY: $i,ZZZZX: $i,ZZZZW: $i,ZZZZV: $i,ZZZZU: $i,ZZZZT: $i,ZZZZS: $i,ZZZZR: $i,ZZZZQ: $i,ZZZZP: $i,ZZZZO: $i,ZZZZN: $i,ZZZZM: $i,ZZZZL: $i,ZZZZK: $i,ZZZZJ: $i,ZZZZI: $i,ZZZZH: $i,ZZZZG: $i,ZZZZF: $i,ZZZZE: $i,ZZZZD: $i,ZZZZC: $i,ZZZZB: $i,ZZZZA: $i,ZZZZ: $i,ZZZY: $i,ZZZX: $i,ZZZW: $i,ZZZV: $i,ZZZU: $i,ZZZT: $i,ZZZS: $i,ZZZR: $i,ZZZQ: $i,ZZZP: $i,ZZZO: $i,ZZZN: $i,ZZZM: $i,ZZZL: $i,ZZZK: $i,ZZZJ: $i,ZZZI: $i,ZZZH: $i,ZZZG: $i,ZZZF: $i,ZZZE: $i,ZZZD: $i,ZZZC: $i,ZZZB: $i,ZZZA: $i,ZZZ: $i,ZZY: $i,ZZX: $i,ZZW: $i,ZZV: $i,ZZU: $i,ZZT: $i,ZZS: $i,ZZR: $i,ZZQ: $i,ZZP: $i,ZZO: $i,ZZN: $i,ZZM: $i,ZZL: $i,ZZK: $i,ZZJ: $i,ZZI: $i,ZZH: $i,ZZG: $i,ZZF: $i,ZZE: $i,ZZD: $i,ZZC: $i,ZZB: $i,ZZA: $i,ZZ: $i,ZY: $i,ZX: $i,ZW: $i,ZV: $i,ZU: $i,ZT: $i,ZS: $i,ZR: $i,ZQ: $i,ZP: $i,ZO: $i,ZN: $i,ZM: $i,ZL: $i,ZK: $i,ZJ: $i,ZI: $i,ZH: $i,ZG: $i,ZF: $i,ZE: $i,ZD: $i,ZC: $i,ZB: $i,ZA: $i,Z: $i,Y: $i,X: $i,W: $i,V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ZZZZZA @ ( ZZZZZ @ ( ZZZZY @ sum ) ) )
| ~ ( ZZZZZA @ ( ZZZZW @ ( ZZZZX @ product ) ) )
| ~ ( ZZZZZ @ ( ZZZZV @ ( ZZZZX @ product ) ) )
| ~ ( ZZZZY @ ( ZZZZU @ ( ZZZZX @ product ) ) )
| ~ ( ZZZZW @ ( ZZZZS @ ( ZZZZT @ product ) ) )
| ~ ( ZZZZV @ ( ZZZZR @ ( ZZZZT @ product ) ) )
| ~ ( ZZZZU @ ( ZZZZQ @ ( ZZZZT @ product ) ) )
| ~ ( ZZZZS @ ( ZZZZO @ ( ZZZZP @ product ) ) )
| ~ ( ZZZZR @ ( ZZZZN @ ( ZZZZP @ product ) ) )
| ~ ( ZZZZQ @ ( ZZZZM @ ( ZZZZP @ product ) ) )
| ~ ( ZZZZO @ ( ZZZZK @ ( ZZZZL @ product ) ) )
| ~ ( ZZZZN @ ( ZZZZJ @ ( ZZZZL @ product ) ) )
| ~ ( ZZZZM @ ( ZZZZI @ ( ZZZZL @ product ) ) )
| ~ ( ZZZZK @ ( ZZZZG @ ( ZZZZH @ product ) ) )
| ~ ( ZZZZJ @ ( ZZZZF @ ( ZZZZH @ product ) ) )
| ~ ( ZZZZI @ ( ZZZZE @ ( ZZZZH @ product ) ) )
| ~ ( ZZZZG @ ( ZZZZC @ ( ZZZZD @ product ) ) )
| ~ ( ZZZZF @ ( ZZZZB @ ( ZZZZD @ product ) ) )
| ~ ( ZZZZE @ ( ZZZZA @ ( ZZZZD @ product ) ) )
| ~ ( ZZZZC @ ( ZZZY @ ( ZZZZ @ product ) ) )
| ~ ( ZZZZB @ ( ZZZX @ ( ZZZZ @ product ) ) )
| ~ ( ZZZZA @ ( ZZZW @ ( ZZZZ @ product ) ) )
| ~ ( ZZZY @ ( ZZZU @ ( ZZZV @ product ) ) )
| ~ ( ZZZX @ ( ZZZT @ ( ZZZV @ product ) ) )
| ~ ( ZZZW @ ( ZZZS @ ( ZZZV @ product ) ) )
| ~ ( ZZZU @ ( ZZZQ @ ( ZZZR @ product ) ) )
| ~ ( ZZZT @ ( ZZZP @ ( ZZZR @ product ) ) )
| ~ ( ZZZS @ ( ZZZO @ ( ZZZR @ product ) ) )
| ~ ( ZZZQ @ ( ZZZM @ ( ZZZN @ product ) ) )
| ~ ( ZZZP @ ( ZZZL @ ( ZZZN @ product ) ) )
| ~ ( ZZZO @ ( ZZZK @ ( ZZZN @ product ) ) )
| ~ ( ZZZM @ ( ZZZI @ ( ZZZJ @ product ) ) )
| ~ ( ZZZL @ ( ZZZH @ ( ZZZJ @ product ) ) )
| ~ ( ZZZK @ ( ZZZG @ ( ZZZJ @ product ) ) )
| ~ ( ZZZI @ ( ZZZE @ ( ZZZF @ product ) ) )
| ~ ( ZZZH @ ( ZZZD @ ( ZZZF @ product ) ) )
| ~ ( ZZZG @ ( ZZZC @ ( ZZZF @ product ) ) )
| ~ ( ZZZE @ ( ZZZA @ ( ZZZB @ product ) ) )
| ~ ( ZZZD @ ( ZZZ @ ( ZZZB @ product ) ) )
| ~ ( ZZZC @ ( ZZY @ ( ZZZB @ product ) ) )
| ~ ( ZZZA @ ( ZZW @ ( ZZX @ product ) ) )
| ~ ( ZZZ @ ( ZZV @ ( ZZX @ product ) ) )
| ~ ( ZZY @ ( ZZU @ ( ZZX @ product ) ) )
| ~ ( ZZW @ ( ZZS @ ( ZZT @ product ) ) )
| ~ ( ZZV @ ( ZZR @ ( ZZT @ product ) ) )
| ~ ( ZZU @ ( ZZQ @ ( ZZT @ product ) ) )
| ~ ( ZZS @ ( ZZO @ ( ZZP @ product ) ) )
| ~ ( ZZR @ ( ZZN @ ( ZZP @ product ) ) )
| ~ ( ZZQ @ ( ZZM @ ( ZZP @ product ) ) )
| ~ ( ZZO @ ( ZZK @ ( ZZL @ product ) ) )
| ~ ( ZZN @ ( ZZJ @ ( ZZL @ product ) ) )
| ~ ( ZZM @ ( ZZI @ ( ZZL @ product ) ) )
| ~ ( ZZK @ ( ZZG @ ( ZZH @ product ) ) )
| ~ ( ZZJ @ ( ZZF @ ( ZZH @ product ) ) )
| ~ ( ZZI @ ( ZZE @ ( ZZH @ product ) ) )
| ~ ( ZZG @ ( ZZC @ ( ZZD @ product ) ) )
| ~ ( ZZF @ ( ZZB @ ( ZZD @ product ) ) )
| ~ ( ZZE @ ( ZZA @ ( ZZD @ product ) ) )
| ~ ( ZZC @ ( ZY @ ( ZZ @ product ) ) )
| ~ ( ZZB @ ( ZX @ ( ZZ @ product ) ) )
| ~ ( ZZA @ ( ZW @ ( ZZ @ product ) ) )
| ~ ( ZY @ ( ZU @ ( ZV @ product ) ) )
| ~ ( ZX @ ( ZT @ ( ZV @ product ) ) )
| ~ ( ZW @ ( ZS @ ( ZV @ product ) ) )
| ~ ( ZU @ ( ZQ @ ( ZR @ product ) ) )
| ~ ( ZT @ ( ZP @ ( ZR @ product ) ) )
| ~ ( ZS @ ( ZO @ ( ZR @ product ) ) )
| ~ ( ZQ @ ( ZM @ ( ZN @ product ) ) )
| ~ ( ZP @ ( ZL @ ( ZN @ product ) ) )
| ~ ( ZO @ ( ZK @ ( ZN @ product ) ) )
| ~ ( ZM @ ( ZI @ ( ZJ @ product ) ) )
| ~ ( ZL @ ( ZH @ ( ZJ @ product ) ) )
| ~ ( ZK @ ( ZG @ ( ZJ @ product ) ) )
| ~ ( ZI @ ( ZE @ ( ZF @ product ) ) )
| ~ ( ZH @ ( ZD @ ( ZF @ product ) ) )
| ~ ( ZG @ ( ZC @ ( ZF @ product ) ) )
| ~ ( ZE @ ( ZA @ ( ZB @ product ) ) )
| ~ ( ZD @ ( Z @ ( ZB @ product ) ) )
| ~ ( ZC @ ( Y @ ( ZB @ product ) ) )
| ~ ( ZA @ ( W @ ( X @ product ) ) )
| ~ ( Z @ ( V @ ( X @ product ) ) )
| ~ ( Y @ ( U @ ( X @ product ) ) )
| ~ ( W @ ( S @ ( T @ product ) ) )
| ~ ( V @ ( R @ ( T @ product ) ) )
| ~ ( U @ ( Q @ ( T @ product ) ) )
| ~ ( S @ ( O @ ( P @ product ) ) )
| ~ ( R @ ( N @ ( P @ product ) ) )
| ~ ( Q @ ( M @ ( P @ product ) ) )
| ~ ( O @ ( K @ ( L @ product ) ) )
| ~ ( N @ ( J @ ( L @ product ) ) )
| ~ ( M @ ( I @ ( L @ product ) ) )
| ~ ( K @ ( G @ ( H @ product ) ) )
| ~ ( J @ ( E @ ( H @ product ) ) )
| ~ ( I @ ( C @ ( H @ product ) ) )
| ~ ( G @ ( F @ ( A @ product ) ) )
| ~ ( F @ ( D @ ( B @ sum ) ) )
| ~ ( E @ ( D @ ( A @ product ) ) )
| ~ ( C @ ( B @ ( A @ product ) ) ) ),
inference(simp,[status(thm)],[3534]) ).
thf(44233,plain,
( ( ( b @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( bS_Ic @ ( aPb_S_IaPc @ ( c @ additive_inverse @ sum ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,23590]) ).
thf(44234,plain,
( ( ( b @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) )
!= ( aPb_S_IaPc @ ( aPc @ additive_inverse @ ( aPb @ sum ) ) ) )
| ( bS_Ic @ ( aPb_S_IaPc @ ( c @ additive_inverse @ sum ) ) ) ),
inference(simp,[status(thm)],[44233]) ).
thf(44326,plain,
( ( b != aPb_S_IaPc )
| ( ( aPc @ additive_inverse )
!= ( aPc @ additive_inverse ) )
| ( aPb != aPb )
| ( bS_Ic @ ( aPb_S_IaPc @ ( c @ additive_inverse @ sum ) ) ) ),
inference(simp,[status(thm)],[44234]) ).
thf(44393,plain,
( ( b != aPb_S_IaPc )
| ( bS_Ic @ ( aPb_S_IaPc @ ( c @ additive_inverse @ sum ) ) ) ),
inference(simp,[status(thm)],[44326]) ).
thf(48395,plain,
$false,
inference(e,[status(thm)],[35827,25415,35838,33779,56,25279,30955,30878,23682,42,24,37,25,42149,52,29055,43517,25275,23108,46,57,24064,29,789,24422,132,133,25317,24201,307,678,793,31147,2496,31090,23581,23531,70,31378,33,28,38,23841,41686,1234,31093,43614,25325,23832,36020,53,24423,25281,23850,23635,35903,129,3115,41,23588,134,128,24212,41105,45,32,34,35444,27,54,787,39454,49,24200,24218,764,23779,40527,39,28720,345,66,130,135,23677,23759,35,795,39534,749,2582,48,24066,25319,24062,50,40445,28371,25273,31,23826,43,24071,25310,26416,23579,24421,25327,319,40,31174,26,23529,23,23590,22299,55,25314,23761,2362,290,58,23535,30,51,41090,23586,34124,34041,2539,62,501,131,47,24417,22362,6839,44393]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG006-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.07 % 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.11/0.39 % Computer : n007.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sat Sep 26 05:42:23 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 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
% 0.84/0.97 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.22/1.17 % [INFO] Parsing done (191ms).
% 1.22/1.18 % [INFO] Running in sequential loop mode.
% 1.86/1.57 % [INFO] eprover registered as external prover.
% 1.86/1.58 % [INFO] Scanning for conjecture ...
% 2.07/1.67 % [INFO] Found a conjecture (or negated_conjecture) and 21 axioms. Running axiom selection ...
% 2.21/1.73 % [INFO] Axiom selection finished. Selected 21 axioms (removed 0 axioms).
% 2.21/1.77 % [INFO] Problem is propositional (TPTP CNF).
% 2.21/1.78 % [INFO] Type checking passed.
% 2.21/1.79 % [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 ...
% 206.82/88.36 % External prover 'e' found a proof!
% 206.82/88.36 % [INFO] Killing All external provers ...
% 206.82/88.36 % Time passed: 87820ms (effective reasoning time: 87173ms)
% 206.82/88.36 % Axioms used in derivation (21): addition_is_well_defined, additive_identity2, additive_identity1, associativity_of_multiplication2, aPb_plus_IaPc, distributivity1, closure_of_multiplication, associativity_of_addition2, a_times_b, associativity_of_multiplication1, distributivity4, closure_of_addition, distributivity3, b_plus_inverse_c, commutativity_of_addition, distributivity2, associativity_of_addition1, left_inverse, multiplication_is_well_defined, right_inverse, a_times_c
% 206.82/88.36 % No. of inferences in proof: 397
% 206.82/88.36 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p : 87820 ms resp. 87173 ms w/o parsing
% 201.22/88.54 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 201.22/88.54 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------