%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : FLD007-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:10:16 AM UTC 2026
% Result : Unsatisfiable 101.74s 24.06s
% Output : Refutation 99.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 29
% Syntax : Number of formulae : 688 ( 171 unt; 0 typ; 0 def)
% Number of atoms : 2310 ( 597 equ; 0 cnn)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 6833 (1036 ~; 862 |; 0 &;4935 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 13 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 572 ( 0 ^; 572 !; 0 ?; 572 :)
% Comments :
%------------------------------------------------------------------------------
thf(equalish_decl,type,
equalish: $i > $i > $o ).
thf(additive_inverse_decl,type,
additive_inverse: $i > $i ).
thf(a_decl,type,
a: $i ).
thf(defined_decl,type,
defined: $i > $o ).
thf(multiply_decl,type,
multiply: $i > $i > $i ).
thf(less_or_equal_decl,type,
less_or_equal: $i > $i > $o ).
thf(add_decl,type,
add: $i > $i > $i ).
thf(additive_identity_decl,type,
additive_identity: $i ).
thf(multiplicative_identity_decl,type,
multiplicative_identity: $i ).
thf(multiplicative_inverse_decl,type,
multiplicative_inverse: $i > $i ).
thf(22,axiom,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( A @ ( B @ multiply ) @ ( B @ ( A @ multiply ) @ equalish ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_multiplication) ).
thf(69,plain,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( A @ ( B @ multiply ) @ ( B @ ( A @ multiply ) @ equalish ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(4,axiom,
additive_identity @ defined,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_definedness_of_additive_identity) ).
thf(36,plain,
additive_identity @ defined,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(20,axiom,
! [A: $i] :
( ~ ( A @ defined )
| ( A @ ( A @ equalish ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_of_equality) ).
thf(65,plain,
! [A: $i] :
( ~ ( A @ defined )
| ( A @ ( A @ equalish ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(66,plain,
! [A: $i] :
( ~ ( A @ defined )
| ( A @ ( A @ equalish ) ) ),
inference(cnf,[status(esa)],[65]) ).
thf(7658,plain,
! [A: $i] :
( ( ( additive_identity @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[36,66]) ).
thf(7659,plain,
! [A: $i] :
( ( ( additive_identity @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7658]) ).
thf(7660,plain,
additive_identity @ ( additive_identity @ equalish ),
inference(pattern_uni,[status(thm)],[7659:[bind(A,$thf( additive_identity ))]]) ).
thf(19,axiom,
a @ defined,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_is_defined) ).
thf(64,plain,
a @ defined,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(17,axiom,
! [A: $i] :
( ~ ( A @ defined )
| ( A @ additive_inverse @ defined ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_definedness_of_additive_inverse) ).
thf(60,plain,
! [A: $i] :
( ~ ( A @ defined )
| ( A @ additive_inverse @ defined ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(61,plain,
! [A: $i] :
( ~ ( A @ defined )
| ( A @ additive_inverse @ defined ) ),
inference(cnf,[status(esa)],[60]) ).
thf(652,plain,
! [A: $i] :
( ( ( a @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[64,61]) ).
thf(653,plain,
! [A: $i] :
( ( ( a @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[652]) ).
thf(654,plain,
a @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[653:[bind(A,$thf( a ))]]) ).
thf(820,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[654,61]) ).
thf(821,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[820]) ).
thf(822,plain,
a @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[821:[bind(A,$thf( a @ additive_inverse ))]]) ).
thf(14,axiom,
! [A: $i] :
( ~ ( A @ defined )
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_of_identity_multiplication) ).
thf(54,plain,
! [A: $i] :
( ~ ( A @ defined )
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(55,plain,
! [A: $i] :
( ~ ( A @ defined )
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(cnf,[status(esa)],[54]) ).
thf(4981,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[822,55]) ).
thf(4982,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(simp,[status(thm)],[4981]) ).
thf(4983,plain,
a @ additive_inverse @ additive_inverse @ ( a @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ),
inference(pattern_uni,[status(thm)],[4982:[bind(A,$thf( a @ additive_inverse @ additive_inverse ))]]) ).
thf(21,axiom,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ equalish ) )
| ( B @ ( A @ equalish ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_equality) ).
thf(67,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ equalish ) )
| ( B @ ( A @ equalish ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(68,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ equalish ) )
| ( B @ ( A @ equalish ) ) ),
inference(cnf,[status(esa)],[67]) ).
thf(1,negated_conjecture,
~ ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_inverse_not_equal_to_a_2) ).
thf(30,plain,
~ ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(31,plain,
~ ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ),
inference(polarity_switch,[status(thm)],[30]) ).
thf(7995,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ $true
| ~ ( A @ ( B @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[68,31]) ).
thf(7996,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ ( A @ ( B @ equalish ) ) ),
inference(simp,[status(thm)],[7995]) ).
thf(7997,plain,
~ ( a @ additive_inverse @ additive_inverse @ ( a @ equalish ) ),
inference(pattern_uni,[status(thm)],[7996:[bind(A,$thf( a @ additive_inverse @ additive_inverse )),bind(B,$thf( a ))]]) ).
thf(8290,plain,
( ( ( a @ additive_inverse @ additive_inverse @ ( a @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( a @ additive_inverse @ additive_inverse @ ( a @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4983,7997]) ).
thf(8291,plain,
( ( a @ additive_inverse @ additive_inverse @ ( a @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( a @ additive_inverse @ additive_inverse @ ( a @ equalish ) ) ),
inference(simp,[status(thm)],[8290]) ).
thf(8402,plain,
( ( ( a @ additive_inverse @ additive_inverse )
!= ( a @ additive_inverse @ additive_inverse ) )
| ( ( a @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ multiply ) )
!= a ) ),
inference(simp,[status(thm)],[8291]) ).
thf(8415,plain,
( ( a @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ multiply ) )
!= a ),
inference(simp,[status(thm)],[8402]) ).
thf(631,plain,
! [A: $i] :
( ( ( additive_identity @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[36,61]) ).
thf(632,plain,
! [A: $i] :
( ( ( additive_identity @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[631]) ).
thf(633,plain,
additive_identity @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[632:[bind(A,$thf( additive_identity ))]]) ).
thf(730,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[633,61]) ).
thf(731,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[730]) ).
thf(732,plain,
additive_identity @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[731:[bind(A,$thf( additive_identity @ additive_inverse ))]]) ).
thf(1048,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[732,61]) ).
thf(1049,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[1048]) ).
thf(1050,plain,
additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[1049:[bind(A,$thf( additive_identity @ additive_inverse @ additive_inverse ))]]) ).
thf(1209,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[1050,61]) ).
thf(1210,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[1209]) ).
thf(1211,plain,
additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[1210:[bind(A,$thf( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(27,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ defined )
| ~ ( B @ defined )
| ~ ( A @ defined )
| ( C @ ( B @ ( A @ add ) @ add ) @ ( C @ ( B @ add ) @ ( A @ add ) @ equalish ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_addition) ).
thf(79,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ defined )
| ~ ( B @ defined )
| ~ ( A @ defined )
| ( C @ ( B @ ( A @ add ) @ add ) @ ( C @ ( B @ add ) @ ( A @ add ) @ equalish ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(80,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ defined )
| ~ ( B @ defined )
| ~ ( A @ defined )
| ( C @ ( B @ ( A @ add ) @ add ) @ ( C @ ( B @ add ) @ ( A @ add ) @ equalish ) ) ),
inference(cnf,[status(esa)],[79]) ).
thf(113,plain,
! [C: $i,B: $i,A: $i] :
( ( ( additive_identity @ defined )
!= ( C @ defined ) )
| ~ $true
| ~ ( B @ defined )
| ~ ( A @ defined )
| ( C @ ( B @ ( A @ add ) @ add ) @ ( C @ ( B @ add ) @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[36,80]) ).
thf(114,plain,
! [C: $i,B: $i,A: $i] :
( ( ( additive_identity @ defined )
!= ( C @ defined ) )
| ~ ( B @ defined )
| ~ ( A @ defined )
| ( C @ ( B @ ( A @ add ) @ add ) @ ( C @ ( B @ add ) @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[113]) ).
thf(115,plain,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( additive_identity @ ( B @ ( A @ add ) @ add ) @ ( additive_identity @ ( B @ add ) @ ( A @ add ) @ equalish ) ) ),
inference(pattern_uni,[status(thm)],[114:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( additive_identity ))]]) ).
thf(5,axiom,
multiplicative_identity @ defined,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_definedness_of_multiplicative_identity) ).
thf(37,plain,
multiplicative_identity @ defined,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(595,plain,
! [A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[37,61]) ).
thf(596,plain,
! [A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[595]) ).
thf(597,plain,
multiplicative_identity @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[596:[bind(A,$thf( multiplicative_identity ))]]) ).
thf(681,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[597,61]) ).
thf(682,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[681]) ).
thf(683,plain,
multiplicative_identity @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[682:[bind(A,$thf( multiplicative_identity @ additive_inverse ))]]) ).
thf(23,axiom,
! [A: $i] :
( ( additive_identity @ ( A @ equalish ) )
| ~ ( A @ defined )
| ( A @ multiplicative_inverse @ defined ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_definedness_of_multiplicative_inverse) ).
thf(71,plain,
! [A: $i] :
( ( additive_identity @ ( A @ equalish ) )
| ~ ( A @ defined )
| ( A @ multiplicative_inverse @ defined ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(72,plain,
! [A: $i] :
( ( additive_identity @ ( A @ equalish ) )
| ~ ( A @ defined )
| ( A @ multiplicative_inverse @ defined ) ),
inference(cnf,[status(esa)],[71]) ).
thf(124,plain,
! [A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ~ $true
| ( A @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[37,72]) ).
thf(125,plain,
! [A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ( A @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[124]) ).
thf(126,plain,
( ( additive_identity @ ( multiplicative_identity @ equalish ) )
| ( multiplicative_identity @ multiplicative_inverse @ defined ) ),
inference(pattern_uni,[status(thm)],[125:[bind(A,$thf( multiplicative_identity ))]]) ).
thf(8028,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( multiplicative_identity @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) )
| ( multiplicative_identity @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[126,68]) ).
thf(8029,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( multiplicative_identity @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) )
| ( multiplicative_identity @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[8028]) ).
thf(8030,plain,
( ( multiplicative_identity @ ( additive_identity @ equalish ) )
| ( multiplicative_identity @ multiplicative_inverse @ defined ) ),
inference(pattern_uni,[status(thm)],[8029:[bind(A,$thf( additive_identity )),bind(B,$thf( multiplicative_identity ))]]) ).
thf(29,axiom,
~ ( multiplicative_identity @ ( additive_identity @ equalish ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',different_identities) ).
thf(83,plain,
~ ( multiplicative_identity @ ( additive_identity @ equalish ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(84,plain,
~ ( multiplicative_identity @ ( additive_identity @ equalish ) ),
inference(polarity_switch,[status(thm)],[83]) ).
thf(9360,plain,
( $false
| ( multiplicative_identity @ multiplicative_inverse @ defined ) ),
inference(rewrite,[status(thm)],[8030,84]) ).
thf(9361,plain,
multiplicative_identity @ multiplicative_inverse @ defined,
inference(simp,[status(thm)],[9360]) ).
thf(9371,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[9361,61]) ).
thf(9372,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[9371]) ).
thf(9373,plain,
multiplicative_identity @ multiplicative_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[9372:[bind(A,$thf( multiplicative_identity @ multiplicative_inverse ))]]) ).
thf(739,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ~ $true
| ( A @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[633,72]) ).
thf(740,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ( A @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[739]) ).
thf(741,plain,
( ( additive_identity @ ( additive_identity @ additive_inverse @ equalish ) )
| ( additive_identity @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(pattern_uni,[status(thm)],[740:[bind(A,$thf( additive_identity @ additive_inverse ))]]) ).
thf(7581,plain,
! [A: $i] :
( ( ( a @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[64,66]) ).
thf(7582,plain,
! [A: $i] :
( ( ( a @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7581]) ).
thf(7583,plain,
a @ ( a @ equalish ),
inference(pattern_uni,[status(thm)],[7582:[bind(A,$thf( a ))]]) ).
thf(7754,plain,
( ( ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( a @ ( a @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7583,31]) ).
thf(7755,plain,
( ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( a @ ( a @ equalish ) ) ),
inference(simp,[status(thm)],[7754]) ).
thf(7775,plain,
( ( a != a )
| ( ( a @ additive_inverse @ additive_inverse )
!= a ) ),
inference(simp,[status(thm)],[7755]) ).
thf(7781,plain,
( ( a @ additive_inverse @ additive_inverse )
!= a ),
inference(simp,[status(thm)],[7775]) ).
thf(15,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( C @ defined )
| ~ ( A @ defined )
| ( B @ ( C @ ( A @ add ) @ multiply ) @ ( B @ ( C @ multiply ) @ ( B @ ( A @ multiply ) @ add ) @ equalish ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distributivity) ).
thf(56,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( C @ defined )
| ~ ( A @ defined )
| ( B @ ( C @ ( A @ add ) @ multiply ) @ ( B @ ( C @ multiply ) @ ( B @ ( A @ multiply ) @ add ) @ equalish ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(4904,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[633,55]) ).
thf(4905,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(simp,[status(thm)],[4904]) ).
thf(4906,plain,
additive_identity @ additive_inverse @ ( additive_identity @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ),
inference(pattern_uni,[status(thm)],[4905:[bind(A,$thf( additive_identity @ additive_inverse ))]]) ).
thf(7947,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ additive_inverse @ ( additive_identity @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[4906,68]) ).
thf(7948,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ additive_inverse @ ( additive_identity @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7947]) ).
thf(7949,plain,
additive_identity @ additive_inverse @ ( multiplicative_identity @ multiply ) @ ( additive_identity @ additive_inverse @ equalish ),
inference(pattern_uni,[status(thm)],[7948:[bind(A,$thf( additive_identity @ additive_inverse )),bind(B,$thf( additive_identity @ additive_inverse @ ( multiplicative_identity @ multiply ) ))]]) ).
thf(94,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ add ) @ add ) @ ( C @ ( B @ add ) @ ( A @ add ) @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true
| ~ ( C @ defined )
| ~ ( B @ defined )
| ~ ( A @ defined ) ),
inference(paramod_ordered,[status(thm)],[80,84]) ).
thf(95,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ add ) @ add ) @ ( C @ ( B @ add ) @ ( A @ add ) @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ ( C @ defined )
| ~ ( B @ defined )
| ~ ( A @ defined ) ),
inference(simp,[status(thm)],[94]) ).
thf(117,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( C @ ( B @ add ) @ ( A @ add ) )
!= additive_identity )
| ~ ( C @ defined )
| ~ ( B @ defined )
| ~ ( A @ defined ) ),
inference(simp,[status(thm)],[95]) ).
thf(296,plain,
! [C: $i,B: $i,A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( C @ defined ) )
| ( ( C @ ( B @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( C @ ( B @ add ) @ ( A @ add ) )
!= additive_identity )
| ~ $true
| ~ ( B @ defined )
| ~ ( A @ defined ) ),
inference(paramod_ordered,[status(thm)],[37,117]) ).
thf(297,plain,
! [C: $i,B: $i,A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( C @ defined ) )
| ( ( C @ ( B @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( C @ ( B @ add ) @ ( A @ add ) )
!= additive_identity )
| ~ ( B @ defined )
| ~ ( A @ defined ) ),
inference(simp,[status(thm)],[296]) ).
thf(298,plain,
! [B: $i,A: $i] :
( ( ( multiplicative_identity @ ( B @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( B @ add ) @ ( A @ add ) )
!= additive_identity )
| ~ ( B @ defined )
| ~ ( A @ defined ) ),
inference(pattern_uni,[status(thm)],[297:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( multiplicative_identity ))]]) ).
thf(371,plain,
! [B: $i,A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( B @ defined ) )
| ( ( multiplicative_identity @ ( B @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( B @ add ) @ ( A @ add ) )
!= additive_identity )
| ~ $true
| ~ ( A @ defined ) ),
inference(paramod_ordered,[status(thm)],[37,298]) ).
thf(372,plain,
! [B: $i,A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( B @ defined ) )
| ( ( multiplicative_identity @ ( B @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( B @ add ) @ ( A @ add ) )
!= additive_identity )
| ~ ( A @ defined ) ),
inference(simp,[status(thm)],[371]) ).
thf(373,plain,
! [A: $i] :
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity )
| ~ ( A @ defined ) ),
inference(pattern_uni,[status(thm)],[372:[bind(A,$thf( A )),bind(B,$thf( multiplicative_identity ))]]) ).
thf(812,plain,
! [A: $i] :
( ( ( a @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[64,373]) ).
thf(813,plain,
! [A: $i] :
( ( ( a @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity ) ),
inference(simp,[status(thm)],[812]) ).
thf(814,plain,
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( a @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( a @ add ) )
!= additive_identity ) ),
inference(pattern_uni,[status(thm)],[813:[bind(A,$thf( a ))]]) ).
thf(132,plain,
! [A: $i] :
( ( ( additive_identity @ ( A @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ $true
| ~ ( A @ defined )
| ( A @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[72,31]) ).
thf(133,plain,
! [A: $i] :
( ( ( additive_identity @ ( A @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ ( A @ defined )
| ( A @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[132]) ).
thf(137,plain,
! [A: $i] :
( ( additive_identity != a )
| ( A
!= ( a @ additive_inverse @ additive_inverse ) )
| ~ ( A @ defined )
| ( A @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[133]) ).
thf(139,plain,
( ( additive_identity != a )
| ~ ( a @ additive_inverse @ additive_inverse @ defined )
| ( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[137]) ).
thf(1100,plain,
( ( additive_identity != a )
| ~ $true
| ( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(rewrite,[status(thm)],[139,822]) ).
thf(1101,plain,
( ( additive_identity != a )
| ( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[1100]) ).
thf(1258,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined )
| ( additive_identity != a ) ),
inference(paramod_ordered,[status(thm)],[1101,61]) ).
thf(1259,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined )
| ( additive_identity != a ) ),
inference(simp,[status(thm)],[1258]) ).
thf(1260,plain,
( ( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ additive_inverse @ defined )
| ( additive_identity != a ) ),
inference(pattern_uni,[status(thm)],[1259:[bind(A,$thf( a @ additive_inverse @ additive_inverse @ multiplicative_inverse ))]]) ).
thf(11,axiom,
! [A: $i] :
( ~ ( A @ defined )
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_of_inverse_addition) ).
thf(48,plain,
! [A: $i] :
( ~ ( A @ defined )
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(49,plain,
! [A: $i] :
( ~ ( A @ defined )
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(cnf,[status(esa)],[48]) ).
thf(3452,plain,
! [A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( A @ defined ) )
| ~ $true
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[37,49]) ).
thf(3453,plain,
! [A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[3452]) ).
thf(3454,plain,
additive_identity @ ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[3453:[bind(A,$thf( multiplicative_identity ))]]) ).
thf(3571,plain,
( ( ( additive_identity @ ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ add ) @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3454,31]) ).
thf(3572,plain,
( ( additive_identity @ ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ add ) @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[3571]) ).
thf(3577,plain,
( ( additive_identity != a )
| ( ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ add ) )
!= ( a @ additive_inverse @ additive_inverse ) ) ),
inference(simp,[status(thm)],[3572]) ).
thf(10068,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[9373,61]) ).
thf(10069,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[10068]) ).
thf(10070,plain,
multiplicative_identity @ multiplicative_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[10069:[bind(A,$thf( multiplicative_identity @ multiplicative_inverse @ additive_inverse ))]]) ).
thf(10454,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[10070,61]) ).
thf(10455,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[10454]) ).
thf(10456,plain,
multiplicative_identity @ multiplicative_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[10455:[bind(A,$thf( multiplicative_identity @ multiplicative_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(11537,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[10456,61]) ).
thf(11538,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[11537]) ).
thf(11539,plain,
multiplicative_identity @ multiplicative_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[11538:[bind(A,$thf( multiplicative_identity @ multiplicative_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(13973,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[11539,61]) ).
thf(13974,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[13973]) ).
thf(13975,plain,
multiplicative_identity @ multiplicative_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[13974:[bind(A,$thf( multiplicative_identity @ multiplicative_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(8,axiom,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( B @ ( A @ add ) @ defined ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_definedness_of_addition) ).
thf(42,plain,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( B @ ( A @ add ) @ defined ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(7501,plain,
! [A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[37,66]) ).
thf(7502,plain,
! [A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7501]) ).
thf(7503,plain,
multiplicative_identity @ ( multiplicative_identity @ equalish ),
inference(pattern_uni,[status(thm)],[7502:[bind(A,$thf( multiplicative_identity ))]]) ).
thf(4913,plain,
! [A: $i] :
( ( ( a @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[64,55]) ).
thf(4914,plain,
! [A: $i] :
( ( ( a @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(simp,[status(thm)],[4913]) ).
thf(4915,plain,
a @ ( a @ ( multiplicative_identity @ multiply ) @ equalish ),
inference(pattern_uni,[status(thm)],[4914:[bind(A,$thf( a ))]]) ).
thf(13,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ equalish ) )
| ~ ( C @ ( A @ equalish ) )
| ( B @ ( A @ equalish ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity_of_equality) ).
thf(52,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ equalish ) )
| ~ ( C @ ( A @ equalish ) )
| ( B @ ( A @ equalish ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(53,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ equalish ) )
| ~ ( C @ ( A @ equalish ) )
| ( B @ ( A @ equalish ) ) ),
inference(cnf,[status(esa)],[52]) ).
thf(4101,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ $true
| ~ ( B @ ( C @ equalish ) )
| ~ ( C @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[53,31]) ).
thf(4102,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ ( B @ ( C @ equalish ) )
| ~ ( C @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[4101]) ).
thf(4103,plain,
! [A: $i] :
( ~ ( a @ ( A @ equalish ) )
| ~ ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(pattern_uni,[status(thm)],[4102:[bind(A,$thf( a @ additive_inverse @ additive_inverse )),bind(B,$thf( a )),bind(C,$thf( C ))]]) ).
thf(4246,plain,
! [A: $i] :
( ~ ( a @ ( A @ equalish ) )
| ~ ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[4103]) ).
thf(5042,plain,
! [A: $i] :
( ( ( a @ ( a @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( a @ ( A @ equalish ) ) )
| ~ $true
| ~ ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[4915,4246]) ).
thf(5043,plain,
! [A: $i] :
( ( ( a @ ( a @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( a @ ( A @ equalish ) ) )
| ~ ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[5042]) ).
thf(5044,plain,
~ ( a @ ( multiplicative_identity @ multiply ) @ ( a @ additive_inverse @ additive_inverse @ equalish ) ),
inference(pattern_uni,[status(thm)],[5043:[bind(A,$thf( a @ ( multiplicative_identity @ multiply ) ))]]) ).
thf(7696,plain,
( ( ( a @ ( multiplicative_identity @ multiply ) @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( multiplicative_identity @ ( multiplicative_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7503,5044]) ).
thf(7697,plain,
( ( a @ ( multiplicative_identity @ multiply ) @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( multiplicative_identity @ ( multiplicative_identity @ equalish ) ) ),
inference(simp,[status(thm)],[7696]) ).
thf(7729,plain,
( ( ( a @ ( multiplicative_identity @ multiply ) )
!= multiplicative_identity )
| ( ( a @ additive_inverse @ additive_inverse )
!= multiplicative_identity ) ),
inference(simp,[status(thm)],[7697]) ).
thf(1102,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[822,61]) ).
thf(1103,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[1102]) ).
thf(1104,plain,
a @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[1103:[bind(A,$thf( a @ additive_inverse @ additive_inverse ))]]) ).
thf(3464,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[1104,49]) ).
thf(3465,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[3464]) ).
thf(3466,plain,
additive_identity @ ( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ ( a @ additive_inverse @ additive_inverse @ additive_inverse @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[3465:[bind(A,$thf( a @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(3554,plain,
! [A: $i] :
( ( ( additive_identity @ defined )
!= ( A @ defined ) )
| ~ $true
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[36,49]) ).
thf(3555,plain,
! [A: $i] :
( ( ( additive_identity @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[3554]) ).
thf(3556,plain,
additive_identity @ ( additive_identity @ additive_inverse @ ( additive_identity @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[3555:[bind(A,$thf( additive_identity ))]]) ).
thf(3591,plain,
( ( ( additive_identity @ ( additive_identity @ additive_inverse @ ( additive_identity @ add ) @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3556,31]) ).
thf(3592,plain,
( ( additive_identity @ ( additive_identity @ additive_inverse @ ( additive_identity @ add ) @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[3591]) ).
thf(3597,plain,
( ( additive_identity != a )
| ( ( additive_identity @ additive_inverse @ ( additive_identity @ add ) )
!= ( a @ additive_inverse @ additive_inverse ) ) ),
inference(simp,[status(thm)],[3592]) ).
thf(1532,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[1104,61]) ).
thf(1533,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[1532]) ).
thf(1534,plain,
a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[1533:[bind(A,$thf( a @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(1700,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[1534,61]) ).
thf(1701,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[1700]) ).
thf(1702,plain,
a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[1701:[bind(A,$thf( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(2254,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[1702,61]) ).
thf(2255,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[2254]) ).
thf(2256,plain,
a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[2255:[bind(A,$thf( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(2566,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[2256,61]) ).
thf(2567,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[2566]) ).
thf(2568,plain,
a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[2567:[bind(A,$thf( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(2755,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[2568,61]) ).
thf(2756,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[2755]) ).
thf(2757,plain,
a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[2756:[bind(A,$thf( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(3219,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[2757,61]) ).
thf(3220,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[3219]) ).
thf(3221,plain,
a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[3220:[bind(A,$thf( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(10119,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[9373,66]) ).
thf(10120,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[10119]) ).
thf(10121,plain,
multiplicative_identity @ multiplicative_inverse @ additive_inverse @ ( multiplicative_identity @ multiplicative_inverse @ additive_inverse @ equalish ),
inference(pattern_uni,[status(thm)],[10120:[bind(A,$thf( multiplicative_identity @ multiplicative_inverse @ additive_inverse ))]]) ).
thf(7803,plain,
! [A: $i] :
( ( ( additive_identity @ ( additive_identity @ equalish ) )
!= ( a @ ( A @ equalish ) ) )
| ~ $true
| ~ ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[7660,4246]) ).
thf(7804,plain,
! [A: $i] :
( ( ( additive_identity @ ( additive_identity @ equalish ) )
!= ( a @ ( A @ equalish ) ) )
| ~ ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[7803]) ).
thf(7817,plain,
! [A: $i] :
( ( additive_identity != a )
| ( additive_identity != A )
| ~ ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[7804]) ).
thf(7825,plain,
( ( additive_identity != a )
| ~ ( additive_identity @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[7817]) ).
thf(7801,plain,
! [A: $i] :
( ( ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( additive_identity @ ( additive_identity @ equalish ) ) )
| ~ ( a @ ( A @ equalish ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7660,4246]) ).
thf(7802,plain,
! [A: $i] :
( ( ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( additive_identity @ ( additive_identity @ equalish ) ) )
| ~ ( a @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7801]) ).
thf(7814,plain,
! [A: $i] :
( ( A != additive_identity )
| ( ( a @ additive_inverse @ additive_inverse )
!= additive_identity )
| ~ ( a @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7802]) ).
thf(7823,plain,
( ( ( a @ additive_inverse @ additive_inverse )
!= additive_identity )
| ~ ( a @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[7814]) ).
thf(10861,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ equalish ) )
!= ( a @ ( additive_identity @ equalish ) ) )
| ( ( a @ additive_inverse @ additive_inverse )
!= additive_identity )
| ~ $true
| ~ ( A @ ( B @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[68,7823]) ).
thf(10862,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ equalish ) )
!= ( a @ ( additive_identity @ equalish ) ) )
| ( ( a @ additive_inverse @ additive_inverse )
!= additive_identity )
| ~ ( A @ ( B @ equalish ) ) ),
inference(simp,[status(thm)],[10861]) ).
thf(10863,plain,
( ( ( a @ additive_inverse @ additive_inverse )
!= additive_identity )
| ~ ( additive_identity @ ( a @ equalish ) ) ),
inference(pattern_uni,[status(thm)],[10862:[bind(A,$thf( additive_identity )),bind(B,$thf( a ))]]) ).
thf(7875,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( additive_identity @ additive_inverse @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) )
| ( additive_identity @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[741,68]) ).
thf(7876,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( additive_identity @ additive_inverse @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) )
| ( additive_identity @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[7875]) ).
thf(7877,plain,
( ( additive_identity @ additive_inverse @ ( additive_identity @ equalish ) )
| ( additive_identity @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(pattern_uni,[status(thm)],[7876:[bind(A,$thf( additive_identity )),bind(B,$thf( additive_identity @ additive_inverse ))]]) ).
thf(1057,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ~ $true
| ( A @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[732,72]) ).
thf(1058,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ( A @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[1057]) ).
thf(1059,plain,
( ( additive_identity @ ( additive_identity @ additive_inverse @ additive_inverse @ equalish ) )
| ( additive_identity @ additive_inverse @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(pattern_uni,[status(thm)],[1058:[bind(A,$thf( additive_identity @ additive_inverse @ additive_inverse ))]]) ).
thf(3440,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[683,49]) ).
thf(3441,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[3440]) ).
thf(3442,plain,
additive_identity @ ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ additive_inverse @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[3441:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse ))]]) ).
thf(996,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[683,61]) ).
thf(997,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[996]) ).
thf(998,plain,
multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[997:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse ))]]) ).
thf(3461,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[998,49]) ).
thf(3462,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[3461]) ).
thf(3463,plain,
additive_identity @ ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[3462:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(10,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ equalish ) )
| ~ ( B @ defined )
| ( B @ ( C @ multiply ) @ ( B @ ( A @ multiply ) @ equalish ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',compatibility_of_equality_and_multiplication) ).
thf(46,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ equalish ) )
| ~ ( B @ defined )
| ( B @ ( C @ multiply ) @ ( B @ ( A @ multiply ) @ equalish ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(91,plain,
! [C: $i,B: $i,A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( C @ defined ) )
| ~ $true
| ~ ( B @ defined )
| ~ ( A @ defined )
| ( C @ ( B @ ( A @ add ) @ add ) @ ( C @ ( B @ add ) @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[37,80]) ).
thf(92,plain,
! [C: $i,B: $i,A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( C @ defined ) )
| ~ ( B @ defined )
| ~ ( A @ defined )
| ( C @ ( B @ ( A @ add ) @ add ) @ ( C @ ( B @ add ) @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[91]) ).
thf(93,plain,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( multiplicative_identity @ ( B @ ( A @ add ) @ add ) @ ( multiplicative_identity @ ( B @ add ) @ ( A @ add ) @ equalish ) ) ),
inference(pattern_uni,[status(thm)],[92:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( multiplicative_identity ))]]) ).
thf(57,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( C @ defined )
| ~ ( A @ defined )
| ( B @ ( C @ ( A @ add ) @ multiply ) @ ( B @ ( C @ multiply ) @ ( B @ ( A @ multiply ) @ add ) @ equalish ) ) ),
inference(cnf,[status(esa)],[56]) ).
thf(26,axiom,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ less_or_equal ) )
| ~ ( B @ ( A @ less_or_equal ) )
| ( B @ ( A @ equalish ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_of_order_relation) ).
thf(77,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ less_or_equal ) )
| ~ ( B @ ( A @ less_or_equal ) )
| ( B @ ( A @ equalish ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(78,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ less_or_equal ) )
| ~ ( B @ ( A @ less_or_equal ) )
| ( B @ ( A @ equalish ) ) ),
inference(cnf,[status(esa)],[77]) ).
thf(815,plain,
! [A: $i] :
( ( ( additive_identity @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[36,373]) ).
thf(816,plain,
! [A: $i] :
( ( ( additive_identity @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity ) ),
inference(simp,[status(thm)],[815]) ).
thf(817,plain,
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( additive_identity @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( additive_identity @ add ) )
!= additive_identity ) ),
inference(pattern_uni,[status(thm)],[816:[bind(A,$thf( additive_identity ))]]) ).
thf(25,axiom,
! [A: $i] :
( ~ ( A @ defined )
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_of_identity_addition) ).
thf(75,plain,
! [A: $i] :
( ~ ( A @ defined )
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(76,plain,
! [A: $i] :
( ~ ( A @ defined )
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
inference(cnf,[status(esa)],[75]) ).
thf(9918,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[654,76]) ).
thf(9919,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[9918]) ).
thf(9920,plain,
a @ additive_inverse @ ( a @ additive_inverse @ ( additive_identity @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[9919:[bind(A,$thf( a @ additive_inverse ))]]) ).
thf(12704,plain,
! [B: $i,A: $i] :
( ( ( a @ additive_inverse @ ( a @ additive_inverse @ ( additive_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[9920,68]) ).
thf(12705,plain,
! [B: $i,A: $i] :
( ( ( a @ additive_inverse @ ( a @ additive_inverse @ ( additive_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[12704]) ).
thf(12706,plain,
a @ additive_inverse @ ( additive_identity @ add ) @ ( a @ additive_inverse @ equalish ),
inference(pattern_uni,[status(thm)],[12705:[bind(A,$thf( a @ additive_inverse )),bind(B,$thf( a @ additive_inverse @ ( additive_identity @ add ) ))]]) ).
thf(4844,plain,
! [A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[37,55]) ).
thf(4845,plain,
! [A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(simp,[status(thm)],[4844]) ).
thf(4846,plain,
multiplicative_identity @ ( multiplicative_identity @ ( multiplicative_identity @ multiply ) @ equalish ),
inference(pattern_uni,[status(thm)],[4845:[bind(A,$thf( multiplicative_identity ))]]) ).
thf(5010,plain,
! [A: $i] :
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ ( a @ ( A @ equalish ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4846,4246]) ).
thf(5011,plain,
! [A: $i] :
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ ( a @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[5010]) ).
thf(5021,plain,
! [A: $i] :
( ( multiplicative_identity != A )
| ( ( multiplicative_identity @ ( multiplicative_identity @ multiply ) )
!= ( a @ additive_inverse @ additive_inverse ) )
| ~ ( a @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[5011]) ).
thf(5027,plain,
( ( ( multiplicative_identity @ ( multiplicative_identity @ multiply ) )
!= ( a @ additive_inverse @ additive_inverse ) )
| ~ ( a @ ( multiplicative_identity @ equalish ) ) ),
inference(simp,[status(thm)],[5021]) ).
thf(7786,plain,
( ( ( a @ ( multiplicative_identity @ multiply ) @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( additive_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7660,5044]) ).
thf(7787,plain,
( ( a @ ( multiplicative_identity @ multiply ) @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( additive_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[7786]) ).
thf(7818,plain,
( ( ( a @ ( multiplicative_identity @ multiply ) )
!= additive_identity )
| ( ( a @ additive_inverse @ additive_inverse )
!= additive_identity ) ),
inference(simp,[status(thm)],[7787]) ).
thf(11969,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ equalish ) )
!= ( additive_identity @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ( additive_identity != a )
| ~ $true
| ~ ( A @ ( B @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[68,7825]) ).
thf(11970,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ equalish ) )
!= ( additive_identity @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ( additive_identity != a )
| ~ ( A @ ( B @ equalish ) ) ),
inference(simp,[status(thm)],[11969]) ).
thf(11971,plain,
( ( additive_identity != a )
| ~ ( a @ additive_inverse @ additive_inverse @ ( additive_identity @ equalish ) ) ),
inference(pattern_uni,[status(thm)],[11970:[bind(A,$thf( a @ additive_inverse @ additive_inverse )),bind(B,$thf( additive_identity ))]]) ).
thf(129,plain,
! [A: $i] :
( ( ( a @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ~ $true
| ( A @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[64,72]) ).
thf(130,plain,
! [A: $i] :
( ( ( a @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ( A @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[129]) ).
thf(131,plain,
( ( additive_identity @ ( a @ equalish ) )
| ( a @ multiplicative_inverse @ defined ) ),
inference(pattern_uni,[status(thm)],[130:[bind(A,$thf( a ))]]) ).
thf(8352,plain,
( ( ( a @ additive_inverse @ additive_inverse @ ( a @ equalish ) )
!= ( additive_identity @ ( a @ equalish ) ) )
| ~ $true
| ( a @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[131,7997]) ).
thf(8353,plain,
( ( ( a @ additive_inverse @ additive_inverse @ ( a @ equalish ) )
!= ( additive_identity @ ( a @ equalish ) ) )
| ( a @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[8352]) ).
thf(8376,plain,
( ( ( a @ additive_inverse @ additive_inverse )
!= additive_identity )
| ( a != a )
| ( a @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[8353]) ).
thf(8411,plain,
( ( ( a @ additive_inverse @ additive_inverse )
!= additive_identity )
| ( a @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[8376]) ).
thf(690,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ~ $true
| ( A @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[597,72]) ).
thf(691,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ( A @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[690]) ).
thf(692,plain,
( ( additive_identity @ ( multiplicative_identity @ additive_inverse @ equalish ) )
| ( multiplicative_identity @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(pattern_uni,[status(thm)],[691:[bind(A,$thf( multiplicative_identity @ additive_inverse ))]]) ).
thf(9863,plain,
! [A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[37,76]) ).
thf(9864,plain,
! [A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[9863]) ).
thf(9865,plain,
multiplicative_identity @ ( multiplicative_identity @ ( additive_identity @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[9864:[bind(A,$thf( multiplicative_identity ))]]) ).
thf(105,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ add ) @ add ) @ ( C @ ( B @ add ) @ ( A @ add ) @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ $true
| ~ ( C @ defined )
| ~ ( B @ defined )
| ~ ( A @ defined ) ),
inference(paramod_ordered,[status(thm)],[80,31]) ).
thf(106,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ add ) @ add ) @ ( C @ ( B @ add ) @ ( A @ add ) @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ ( C @ defined )
| ~ ( B @ defined )
| ~ ( A @ defined ) ),
inference(simp,[status(thm)],[105]) ).
thf(116,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ add ) @ add ) )
!= a )
| ( ( C @ ( B @ add ) @ ( A @ add ) )
!= ( a @ additive_inverse @ additive_inverse ) )
| ~ ( C @ defined )
| ~ ( B @ defined )
| ~ ( A @ defined ) ),
inference(simp,[status(thm)],[106]) ).
thf(24,axiom,
! [A: $i] :
( ( additive_identity @ ( A @ equalish ) )
| ~ ( A @ defined )
| ( multiplicative_identity @ ( A @ multiplicative_inverse @ ( A @ multiply ) @ equalish ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_of_inverse_multiplication) ).
thf(73,plain,
! [A: $i] :
( ( additive_identity @ ( A @ equalish ) )
| ~ ( A @ defined )
| ( multiplicative_identity @ ( A @ multiplicative_inverse @ ( A @ multiply ) @ equalish ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(74,plain,
! [A: $i] :
( ( additive_identity @ ( A @ equalish ) )
| ~ ( A @ defined )
| ( multiplicative_identity @ ( A @ multiplicative_inverse @ ( A @ multiply ) @ equalish ) ) ),
inference(cnf,[status(esa)],[73]) ).
thf(3506,plain,
! [A: $i] :
( ( ( a @ defined )
!= ( A @ defined ) )
| ~ $true
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[64,49]) ).
thf(3507,plain,
! [A: $i] :
( ( ( a @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[3506]) ).
thf(3508,plain,
additive_identity @ ( a @ additive_inverse @ ( a @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[3507:[bind(A,$thf( a ))]]) ).
thf(7950,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( a @ additive_inverse @ ( a @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[3508,68]) ).
thf(7951,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( a @ additive_inverse @ ( a @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7950]) ).
thf(7952,plain,
a @ additive_inverse @ ( a @ add ) @ ( additive_identity @ equalish ),
inference(pattern_uni,[status(thm)],[7951:[bind(A,$thf( additive_identity )),bind(B,$thf( a @ additive_inverse @ ( a @ add ) ))]]) ).
thf(8959,plain,
( ( ( a @ additive_inverse @ ( a @ add ) @ ( additive_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7952,84]) ).
thf(8960,plain,
( ( a @ additive_inverse @ ( a @ add ) @ ( additive_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[8959]) ).
thf(8991,plain,
( ( ( a @ additive_inverse @ ( a @ add ) )
!= multiplicative_identity )
| ( additive_identity != additive_identity ) ),
inference(simp,[status(thm)],[8960]) ).
thf(9007,plain,
( ( a @ additive_inverse @ ( a @ add ) )
!= multiplicative_identity ),
inference(simp,[status(thm)],[8991]) ).
thf(3557,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[822,49]) ).
thf(3558,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[3557]) ).
thf(3559,plain,
additive_identity @ ( a @ additive_inverse @ additive_inverse @ additive_inverse @ ( a @ additive_inverse @ additive_inverse @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[3558:[bind(A,$thf( a @ additive_inverse @ additive_inverse ))]]) ).
thf(3443,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[597,49]) ).
thf(3444,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[3443]) ).
thf(3445,plain,
additive_identity @ ( multiplicative_identity @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[3444:[bind(A,$thf( multiplicative_identity @ additive_inverse ))]]) ).
thf(7915,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( multiplicative_identity @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[3445,68]) ).
thf(7916,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( multiplicative_identity @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7915]) ).
thf(7917,plain,
multiplicative_identity @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ add ) @ ( additive_identity @ equalish ),
inference(pattern_uni,[status(thm)],[7916:[bind(A,$thf( additive_identity )),bind(B,$thf( multiplicative_identity @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ add ) ))]]) ).
thf(16336,plain,
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ add ) @ ( additive_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7917,84]) ).
thf(16337,plain,
( ( multiplicative_identity @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ add ) @ ( additive_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[16336]) ).
thf(16392,plain,
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ add ) )
!= multiplicative_identity )
| ( additive_identity != additive_identity ) ),
inference(simp,[status(thm)],[16337]) ).
thf(16401,plain,
( ( multiplicative_identity @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ add ) )
!= multiplicative_identity ),
inference(simp,[status(thm)],[16392]) ).
thf(1644,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[1211,61]) ).
thf(1645,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[1644]) ).
thf(1646,plain,
additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[1645:[bind(A,$thf( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(2191,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[1646,61]) ).
thf(2192,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[2191]) ).
thf(2193,plain,
additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[2192:[bind(A,$thf( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(2380,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[2193,61]) ).
thf(2381,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[2380]) ).
thf(2382,plain,
additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[2381:[bind(A,$thf( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(7713,plain,
! [A: $i] :
( ( ( multiplicative_identity @ ( multiplicative_identity @ equalish ) )
!= ( a @ ( A @ equalish ) ) )
| ~ $true
| ~ ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[7503,4246]) ).
thf(7714,plain,
! [A: $i] :
( ( ( multiplicative_identity @ ( multiplicative_identity @ equalish ) )
!= ( a @ ( A @ equalish ) ) )
| ~ ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[7713]) ).
thf(7724,plain,
! [A: $i] :
( ( multiplicative_identity != a )
| ( multiplicative_identity != A )
| ~ ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[7714]) ).
thf(7735,plain,
( ( multiplicative_identity != a )
| ~ ( multiplicative_identity @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[7724]) ).
thf(9938,plain,
! [A: $i] :
( ( ( a @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[64,76]) ).
thf(9939,plain,
! [A: $i] :
( ( ( a @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[9938]) ).
thf(9940,plain,
a @ ( a @ ( additive_identity @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[9939:[bind(A,$thf( a ))]]) ).
thf(10311,plain,
! [A: $i] :
( ( ( a @ ( a @ ( additive_identity @ add ) @ equalish ) )
!= ( a @ ( A @ equalish ) ) )
| ~ $true
| ~ ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[9940,4246]) ).
thf(10312,plain,
! [A: $i] :
( ( ( a @ ( a @ ( additive_identity @ add ) @ equalish ) )
!= ( a @ ( A @ equalish ) ) )
| ~ ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[10311]) ).
thf(10313,plain,
~ ( a @ ( additive_identity @ add ) @ ( a @ additive_inverse @ additive_inverse @ equalish ) ),
inference(pattern_uni,[status(thm)],[10312:[bind(A,$thf( a @ ( additive_identity @ add ) ))]]) ).
thf(1089,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[732,373]) ).
thf(1090,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity ) ),
inference(simp,[status(thm)],[1089]) ).
thf(1091,plain,
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( additive_identity @ additive_inverse @ additive_inverse @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( additive_identity @ additive_inverse @ additive_inverse @ add ) )
!= additive_identity ) ),
inference(pattern_uni,[status(thm)],[1090:[bind(A,$thf( additive_identity @ additive_inverse @ additive_inverse ))]]) ).
thf(7561,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[654,66]) ).
thf(7562,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7561]) ).
thf(7563,plain,
a @ additive_inverse @ ( a @ additive_inverse @ equalish ),
inference(pattern_uni,[status(thm)],[7562:[bind(A,$thf( a @ additive_inverse ))]]) ).
thf(8081,plain,
( ( ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( a @ additive_inverse @ ( a @ additive_inverse @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7563,31]) ).
thf(8082,plain,
( ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( a @ additive_inverse @ ( a @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[8081]) ).
thf(8098,plain,
( ( ( a @ additive_inverse )
!= a )
| ( ( a @ additive_inverse @ additive_inverse )
!= ( a @ additive_inverse ) ) ),
inference(simp,[status(thm)],[8082]) ).
thf(17324,plain,
( ( ( a @ additive_inverse )
!= a )
| ( ( a @ additive_inverse )
!= a ) ),
inference(simp,[status(thm)],[8098]) ).
thf(17325,plain,
( ( a @ additive_inverse )
!= a ),
inference(simp,[status(thm)],[17324]) ).
thf(3497,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[633,49]) ).
thf(3498,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[3497]) ).
thf(3499,plain,
additive_identity @ ( additive_identity @ additive_inverse @ additive_inverse @ ( additive_identity @ additive_inverse @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[3498:[bind(A,$thf( additive_identity @ additive_inverse ))]]) ).
thf(7918,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( additive_identity @ additive_inverse @ additive_inverse @ ( additive_identity @ additive_inverse @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[3499,68]) ).
thf(7919,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( additive_identity @ additive_inverse @ additive_inverse @ ( additive_identity @ additive_inverse @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7918]) ).
thf(7920,plain,
additive_identity @ additive_inverse @ additive_inverse @ ( additive_identity @ additive_inverse @ add ) @ ( additive_identity @ equalish ),
inference(pattern_uni,[status(thm)],[7919:[bind(A,$thf( additive_identity )),bind(B,$thf( additive_identity @ additive_inverse @ additive_inverse @ ( additive_identity @ additive_inverse @ add ) ))]]) ).
thf(16418,plain,
( ( ( additive_identity @ additive_inverse @ additive_inverse @ ( additive_identity @ additive_inverse @ add ) @ ( additive_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7920,84]) ).
thf(16419,plain,
( ( additive_identity @ additive_inverse @ additive_inverse @ ( additive_identity @ additive_inverse @ add ) @ ( additive_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[16418]) ).
thf(16467,plain,
( ( ( additive_identity @ additive_inverse @ additive_inverse @ ( additive_identity @ additive_inverse @ add ) )
!= multiplicative_identity )
| ( additive_identity != additive_identity ) ),
inference(simp,[status(thm)],[16419]) ).
thf(16484,plain,
( ( additive_identity @ additive_inverse @ additive_inverse @ ( additive_identity @ additive_inverse @ add ) )
!= multiplicative_identity ),
inference(simp,[status(thm)],[16467]) ).
thf(70,plain,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( A @ ( B @ multiply ) @ ( B @ ( A @ multiply ) @ equalish ) ) ),
inference(cnf,[status(esa)],[69]) ).
thf(2692,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[2382,61]) ).
thf(2693,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[2692]) ).
thf(2694,plain,
additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[2693:[bind(A,$thf( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(3152,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[2694,61]) ).
thf(3153,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[3152]) ).
thf(3154,plain,
additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[3153:[bind(A,$thf( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(7921,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( additive_identity @ additive_inverse @ ( additive_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[3556,68]) ).
thf(7922,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( additive_identity @ additive_inverse @ ( additive_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7921]) ).
thf(7923,plain,
additive_identity @ additive_inverse @ ( additive_identity @ add ) @ ( additive_identity @ equalish ),
inference(pattern_uni,[status(thm)],[7922:[bind(A,$thf( additive_identity )),bind(B,$thf( additive_identity @ additive_inverse @ ( additive_identity @ add ) ))]]) ).
thf(8853,plain,
( ( ( additive_identity @ additive_inverse @ ( additive_identity @ add ) @ ( additive_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7923,84]) ).
thf(8854,plain,
( ( additive_identity @ additive_inverse @ ( additive_identity @ add ) @ ( additive_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[8853]) ).
thf(8890,plain,
( ( ( additive_identity @ additive_inverse @ ( additive_identity @ add ) )
!= multiplicative_identity )
| ( additive_identity != additive_identity ) ),
inference(simp,[status(thm)],[8854]) ).
thf(8899,plain,
( ( additive_identity @ additive_inverse @ ( additive_identity @ add ) )
!= multiplicative_identity ),
inference(simp,[status(thm)],[8890]) ).
thf(7904,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[4915,68]) ).
thf(7905,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7904]) ).
thf(7906,plain,
a @ ( multiplicative_identity @ multiply ) @ ( a @ equalish ),
inference(pattern_uni,[status(thm)],[7905:[bind(A,$thf( a )),bind(B,$thf( a @ ( multiplicative_identity @ multiply ) ))]]) ).
thf(2,axiom,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( B @ ( A @ multiply ) @ defined ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_definedness_of_multiplication) ).
thf(32,plain,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( B @ ( A @ multiply ) @ defined ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(33,plain,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( B @ ( A @ multiply ) @ defined ) ),
inference(cnf,[status(esa)],[32]) ).
thf(6,axiom,
! [B: $i,A: $i] :
( ~ ( B @ ( additive_identity @ less_or_equal ) )
| ~ ( A @ ( additive_identity @ less_or_equal ) )
| ( B @ ( A @ multiply ) @ ( additive_identity @ less_or_equal ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',compatibility_of_order_relation_and_multiplication) ).
thf(38,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( additive_identity @ less_or_equal ) )
| ~ ( A @ ( additive_identity @ less_or_equal ) )
| ( B @ ( A @ multiply ) @ ( additive_identity @ less_or_equal ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(7572,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[633,66]) ).
thf(7573,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7572]) ).
thf(7574,plain,
additive_identity @ additive_inverse @ ( additive_identity @ additive_inverse @ equalish ),
inference(pattern_uni,[status(thm)],[7573:[bind(A,$thf( additive_identity @ additive_inverse ))]]) ).
thf(8112,plain,
( ( ( additive_identity @ additive_inverse @ ( additive_identity @ additive_inverse @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7574,84]) ).
thf(8113,plain,
( ( additive_identity @ additive_inverse @ ( additive_identity @ additive_inverse @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[8112]) ).
thf(8145,plain,
( ( ( additive_identity @ additive_inverse )
!= multiplicative_identity )
| ( ( additive_identity @ additive_inverse )
!= additive_identity ) ),
inference(simp,[status(thm)],[8113]) ).
thf(1157,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ~ $true
| ( A @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[998,72]) ).
thf(1158,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ( A @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[1157]) ).
thf(1159,plain,
( ( additive_identity @ ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ equalish ) )
| ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(pattern_uni,[status(thm)],[1158:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(4975,plain,
! [A: $i] :
( ( ( additive_identity @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[36,55]) ).
thf(4976,plain,
! [A: $i] :
( ( ( additive_identity @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(simp,[status(thm)],[4975]) ).
thf(4977,plain,
additive_identity @ ( additive_identity @ ( multiplicative_identity @ multiply ) @ equalish ),
inference(pattern_uni,[status(thm)],[4976:[bind(A,$thf( additive_identity ))]]) ).
thf(8046,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( additive_identity @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[4977,68]) ).
thf(8047,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( additive_identity @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[8046]) ).
thf(8048,plain,
additive_identity @ ( multiplicative_identity @ multiply ) @ ( additive_identity @ equalish ),
inference(pattern_uni,[status(thm)],[8047:[bind(A,$thf( additive_identity )),bind(B,$thf( additive_identity @ ( multiplicative_identity @ multiply ) ))]]) ).
thf(5830,plain,
( ( ( additive_identity @ additive_inverse @ ( additive_identity @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4906,84]) ).
thf(5831,plain,
( ( additive_identity @ additive_inverse @ ( additive_identity @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[5830]) ).
thf(5854,plain,
( ( ( additive_identity @ additive_inverse )
!= multiplicative_identity )
| ( ( additive_identity @ additive_inverse @ ( multiplicative_identity @ multiply ) )
!= additive_identity ) ),
inference(simp,[status(thm)],[5831]) ).
thf(9929,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[633,76]) ).
thf(9930,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[9929]) ).
thf(9931,plain,
additive_identity @ additive_inverse @ ( additive_identity @ additive_inverse @ ( additive_identity @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[9930:[bind(A,$thf( additive_identity @ additive_inverse ))]]) ).
thf(12767,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ additive_inverse @ ( additive_identity @ additive_inverse @ ( additive_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[9931,68]) ).
thf(12768,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ additive_inverse @ ( additive_identity @ additive_inverse @ ( additive_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[12767]) ).
thf(12769,plain,
additive_identity @ additive_inverse @ ( additive_identity @ add ) @ ( additive_identity @ additive_inverse @ equalish ),
inference(pattern_uni,[status(thm)],[12768:[bind(A,$thf( additive_identity @ additive_inverse )),bind(B,$thf( additive_identity @ additive_inverse @ ( additive_identity @ add ) ))]]) ).
thf(1141,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[822,373]) ).
thf(1142,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity ) ),
inference(simp,[status(thm)],[1141]) ).
thf(1143,plain,
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( a @ additive_inverse @ additive_inverse @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( a @ additive_inverse @ additive_inverse @ add ) )
!= additive_identity ) ),
inference(pattern_uni,[status(thm)],[1142:[bind(A,$thf( a @ additive_inverse @ additive_inverse ))]]) ).
thf(1160,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[998,61]) ).
thf(1161,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[1160]) ).
thf(1162,plain,
multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[1161:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(1588,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[1162,61]) ).
thf(1589,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[1588]) ).
thf(1590,plain,
multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[1589:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(1756,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[1590,61]) ).
thf(1757,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[1756]) ).
thf(1758,plain,
multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[1757:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(2317,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[1758,61]) ).
thf(2318,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[2317]) ).
thf(2319,plain,
multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[2318:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(2629,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[2319,61]) ).
thf(2630,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[2629]) ).
thf(2631,plain,
multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[2630:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(3085,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[2631,61]) ).
thf(3086,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[3085]) ).
thf(3087,plain,
multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[3086:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(7739,plain,
( ( ( multiplicative_identity @ ( additive_identity @ equalish ) )
!= ( a @ ( a @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7583,84]) ).
thf(7740,plain,
( ( multiplicative_identity @ ( additive_identity @ equalish ) )
!= ( a @ ( a @ equalish ) ) ),
inference(simp,[status(thm)],[7739]) ).
thf(7774,plain,
( ( multiplicative_identity != a )
| ( additive_identity != a ) ),
inference(simp,[status(thm)],[7740]) ).
thf(3286,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[3087,61]) ).
thf(3287,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[3286]) ).
thf(3288,plain,
multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[3287:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(4423,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[3288,61]) ).
thf(4424,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[4423]) ).
thf(4425,plain,
multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[4424:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(4859,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[1104,55]) ).
thf(4860,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(simp,[status(thm)],[4859]) ).
thf(4861,plain,
a @ additive_inverse @ additive_inverse @ additive_inverse @ ( a @ additive_inverse @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ),
inference(pattern_uni,[status(thm)],[4860:[bind(A,$thf( a @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(4895,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[654,55]) ).
thf(4896,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(simp,[status(thm)],[4895]) ).
thf(4897,plain,
a @ additive_inverse @ ( a @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ),
inference(pattern_uni,[status(thm)],[4896:[bind(A,$thf( a @ additive_inverse ))]]) ).
thf(7974,plain,
! [B: $i,A: $i] :
( ( ( a @ additive_inverse @ ( a @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[4897,68]) ).
thf(7975,plain,
! [B: $i,A: $i] :
( ( ( a @ additive_inverse @ ( a @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7974]) ).
thf(7976,plain,
a @ additive_inverse @ ( multiplicative_identity @ multiply ) @ ( a @ additive_inverse @ equalish ),
inference(pattern_uni,[status(thm)],[7975:[bind(A,$thf( a @ additive_inverse )),bind(B,$thf( a @ additive_inverse @ ( multiplicative_identity @ multiply ) ))]]) ).
thf(1037,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[683,373]) ).
thf(1038,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity ) ),
inference(simp,[status(thm)],[1037]) ).
thf(1039,plain,
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( multiplicative_identity @ additive_inverse @ additive_inverse @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( multiplicative_identity @ additive_inverse @ additive_inverse @ add ) )
!= additive_identity ) ),
inference(pattern_uni,[status(thm)],[1038:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse ))]]) ).
thf(8422,plain,
( ( ( additive_identity @ ( multiplicative_identity @ multiply ) @ ( additive_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8048,84]) ).
thf(8423,plain,
( ( additive_identity @ ( multiplicative_identity @ multiply ) @ ( additive_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[8422]) ).
thf(8460,plain,
( ( ( additive_identity @ ( multiplicative_identity @ multiply ) )
!= multiplicative_identity )
| ( additive_identity != additive_identity ) ),
inference(simp,[status(thm)],[8423]) ).
thf(8467,plain,
( ( additive_identity @ ( multiplicative_identity @ multiply ) )
!= multiplicative_identity ),
inference(simp,[status(thm)],[8460]) ).
thf(5061,plain,
( ( ( additive_identity @ ( additive_identity @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4977,31]) ).
thf(5062,plain,
( ( additive_identity @ ( additive_identity @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[5061]) ).
thf(5080,plain,
( ( additive_identity != a )
| ( ( additive_identity @ ( multiplicative_identity @ multiply ) )
!= ( a @ additive_inverse @ additive_inverse ) ) ),
inference(simp,[status(thm)],[5062]) ).
thf(7666,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[822,66]) ).
thf(7667,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7666]) ).
thf(7668,plain,
a @ additive_inverse @ additive_inverse @ ( a @ additive_inverse @ additive_inverse @ equalish ),
inference(pattern_uni,[status(thm)],[7667:[bind(A,$thf( a @ additive_inverse @ additive_inverse ))]]) ).
thf(7711,plain,
! [A: $i] :
( ( ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( multiplicative_identity @ ( multiplicative_identity @ equalish ) ) )
| ~ ( a @ ( A @ equalish ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7503,4246]) ).
thf(7712,plain,
! [A: $i] :
( ( ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( multiplicative_identity @ ( multiplicative_identity @ equalish ) ) )
| ~ ( a @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7711]) ).
thf(7728,plain,
! [A: $i] :
( ( A != multiplicative_identity )
| ( ( a @ additive_inverse @ additive_inverse )
!= multiplicative_identity )
| ~ ( a @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7712]) ).
thf(7731,plain,
( ( ( a @ additive_inverse @ additive_inverse )
!= multiplicative_identity )
| ~ ( a @ ( multiplicative_identity @ equalish ) ) ),
inference(simp,[status(thm)],[7728]) ).
thf(9579,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ equalish ) )
!= ( a @ ( multiplicative_identity @ equalish ) ) )
| ( ( a @ additive_inverse @ additive_inverse )
!= multiplicative_identity )
| ~ $true
| ~ ( A @ ( B @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[68,7731]) ).
thf(9580,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ equalish ) )
!= ( a @ ( multiplicative_identity @ equalish ) ) )
| ( ( a @ additive_inverse @ additive_inverse )
!= multiplicative_identity )
| ~ ( A @ ( B @ equalish ) ) ),
inference(simp,[status(thm)],[9579]) ).
thf(9581,plain,
( ( ( a @ additive_inverse @ additive_inverse )
!= multiplicative_identity )
| ~ ( multiplicative_identity @ ( a @ equalish ) ) ),
inference(pattern_uni,[status(thm)],[9580:[bind(A,$thf( multiplicative_identity )),bind(B,$thf( a ))]]) ).
thf(5032,plain,
( ( ( a @ ( a @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4915,31]) ).
thf(5033,plain,
( ( a @ ( a @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[5032]) ).
thf(5053,plain,
( ( a != a )
| ( ( a @ ( multiplicative_identity @ multiply ) )
!= ( a @ additive_inverse @ additive_inverse ) ) ),
inference(simp,[status(thm)],[5033]) ).
thf(5058,plain,
( ( a @ ( multiplicative_identity @ multiply ) )
!= ( a @ additive_inverse @ additive_inverse ) ),
inference(simp,[status(thm)],[5053]) ).
thf(7,axiom,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( A @ ( B @ less_or_equal ) )
| ( B @ ( A @ less_or_equal ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',totality_of_order_relation) ).
thf(40,plain,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( A @ ( B @ less_or_equal ) )
| ( B @ ( A @ less_or_equal ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(41,plain,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( A @ ( B @ less_or_equal ) )
| ( B @ ( A @ less_or_equal ) ) ),
inference(cnf,[status(esa)],[40]) ).
thf(5012,plain,
! [A: $i] :
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( a @ ( A @ equalish ) ) )
| ~ $true
| ~ ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[4846,4246]) ).
thf(5013,plain,
! [A: $i] :
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( a @ ( A @ equalish ) ) )
| ~ ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[5012]) ).
thf(5020,plain,
! [A: $i] :
( ( multiplicative_identity != a )
| ( ( multiplicative_identity @ ( multiplicative_identity @ multiply ) )
!= A )
| ~ ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[5013]) ).
thf(5026,plain,
( ( multiplicative_identity != a )
| ~ ( multiplicative_identity @ ( multiplicative_identity @ multiply ) @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[5020]) ).
thf(1307,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined )
| ( additive_identity != a ) ),
inference(paramod_ordered,[status(thm)],[1260,61]) ).
thf(1308,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined )
| ( additive_identity != a ) ),
inference(simp,[status(thm)],[1307]) ).
thf(1309,plain,
( ( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ additive_inverse @ additive_inverse @ defined )
| ( additive_identity != a ) ),
inference(pattern_uni,[status(thm)],[1308:[bind(A,$thf( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ additive_inverse ))]]) ).
thf(1812,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined )
| ( additive_identity != a ) ),
inference(paramod_ordered,[status(thm)],[1309,61]) ).
thf(1813,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined )
| ( additive_identity != a ) ),
inference(simp,[status(thm)],[1812]) ).
thf(1814,plain,
( ( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
| ( additive_identity != a ) ),
inference(pattern_uni,[status(thm)],[1813:[bind(A,$thf( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(3581,plain,
( ( ( additive_identity @ ( a @ additive_inverse @ ( a @ add ) @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3508,31]) ).
thf(3582,plain,
( ( additive_identity @ ( a @ additive_inverse @ ( a @ add ) @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[3581]) ).
thf(3587,plain,
( ( additive_identity != a )
| ( ( a @ additive_inverse @ ( a @ add ) )
!= ( a @ additive_inverse @ additive_inverse ) ) ),
inference(simp,[status(thm)],[3582]) ).
thf(7939,plain,
! [B: $i,A: $i] :
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[4846,68]) ).
thf(7940,plain,
! [B: $i,A: $i] :
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7939]) ).
thf(7941,plain,
multiplicative_identity @ ( multiplicative_identity @ multiply ) @ ( multiplicative_identity @ equalish ),
inference(pattern_uni,[status(thm)],[7940:[bind(A,$thf( multiplicative_identity )),bind(B,$thf( multiplicative_identity @ ( multiplicative_identity @ multiply ) ))]]) ).
thf(3488,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[654,49]) ).
thf(3489,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[3488]) ).
thf(3490,plain,
additive_identity @ ( a @ additive_inverse @ additive_inverse @ ( a @ additive_inverse @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[3489:[bind(A,$thf( a @ additive_inverse ))]]) ).
thf(7983,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( a @ additive_inverse @ additive_inverse @ ( a @ additive_inverse @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[3490,68]) ).
thf(7984,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( a @ additive_inverse @ additive_inverse @ ( a @ additive_inverse @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7983]) ).
thf(7985,plain,
a @ additive_inverse @ additive_inverse @ ( a @ additive_inverse @ add ) @ ( additive_identity @ equalish ),
inference(pattern_uni,[status(thm)],[7984:[bind(A,$thf( additive_identity )),bind(B,$thf( a @ additive_inverse @ additive_inverse @ ( a @ additive_inverse @ add ) ))]]) ).
thf(9,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ less_or_equal ) )
| ~ ( C @ ( A @ less_or_equal ) )
| ( B @ ( A @ less_or_equal ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity_of_order_relation) ).
thf(44,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ less_or_equal ) )
| ~ ( C @ ( A @ less_or_equal ) )
| ( B @ ( A @ less_or_equal ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(45,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ less_or_equal ) )
| ~ ( C @ ( A @ less_or_equal ) )
| ( B @ ( A @ less_or_equal ) ) ),
inference(cnf,[status(esa)],[44]) ).
thf(7489,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[683,66]) ).
thf(7490,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7489]) ).
thf(7491,plain,
multiplicative_identity @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ additive_inverse @ equalish ),
inference(pattern_uni,[status(thm)],[7490:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse ))]]) ).
thf(2439,plain,
( ( ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( additive_identity @ ( multiplicative_identity @ additive_inverse @ equalish ) ) )
| ~ $true
| ( multiplicative_identity @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[692,31]) ).
thf(2440,plain,
( ( ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( additive_identity @ ( multiplicative_identity @ additive_inverse @ equalish ) ) )
| ( multiplicative_identity @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[2439]) ).
thf(2442,plain,
( ( additive_identity != a )
| ( ( a @ additive_inverse @ additive_inverse )
!= ( multiplicative_identity @ additive_inverse ) )
| ( multiplicative_identity @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[2440]) ).
thf(4017,plain,
( ( additive_identity != a )
| ( ( a @ additive_inverse )
!= multiplicative_identity )
| ( multiplicative_identity @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[2442]) ).
thf(10016,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[9361,76]) ).
thf(10017,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[10016]) ).
thf(10018,plain,
multiplicative_identity @ multiplicative_inverse @ ( multiplicative_identity @ multiplicative_inverse @ ( additive_identity @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[10017:[bind(A,$thf( multiplicative_identity @ multiplicative_inverse ))]]) ).
thf(13616,plain,
! [B: $i,A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ ( multiplicative_identity @ multiplicative_inverse @ ( additive_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[10018,68]) ).
thf(13617,plain,
! [B: $i,A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ ( multiplicative_identity @ multiplicative_inverse @ ( additive_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[13616]) ).
thf(13618,plain,
multiplicative_identity @ multiplicative_inverse @ ( additive_identity @ add ) @ ( multiplicative_identity @ multiplicative_inverse @ equalish ),
inference(pattern_uni,[status(thm)],[13617:[bind(A,$thf( multiplicative_identity @ multiplicative_inverse )),bind(B,$thf( multiplicative_identity @ multiplicative_inverse @ ( additive_identity @ add ) ))]]) ).
thf(4919,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[732,55]) ).
thf(4920,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(simp,[status(thm)],[4919]) ).
thf(4921,plain,
additive_identity @ additive_inverse @ additive_inverse @ ( additive_identity @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ),
inference(pattern_uni,[status(thm)],[4920:[bind(A,$thf( additive_identity @ additive_inverse @ additive_inverse ))]]) ).
thf(3,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ less_or_equal ) )
| ~ ( B @ defined )
| ( B @ ( C @ add ) @ ( B @ ( A @ add ) @ less_or_equal ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',compatibility_of_order_relation_and_addition) ).
thf(34,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ less_or_equal ) )
| ~ ( B @ defined )
| ( B @ ( C @ add ) @ ( B @ ( A @ add ) @ less_or_equal ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(10319,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ ( additive_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[9940,68]) ).
thf(10320,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ ( additive_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[10319]) ).
thf(10321,plain,
a @ ( additive_identity @ add ) @ ( a @ equalish ),
inference(pattern_uni,[status(thm)],[10320:[bind(A,$thf( a )),bind(B,$thf( a @ ( additive_identity @ add ) ))]]) ).
thf(9416,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[9361,49]) ).
thf(9417,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[9416]) ).
thf(9418,plain,
additive_identity @ ( multiplicative_identity @ multiplicative_inverse @ additive_inverse @ ( multiplicative_identity @ multiplicative_inverse @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[9417:[bind(A,$thf( multiplicative_identity @ multiplicative_inverse ))]]) ).
thf(1005,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ~ $true
| ( A @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[683,72]) ).
thf(1006,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ( A @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[1005]) ).
thf(1007,plain,
( ( additive_identity @ ( multiplicative_identity @ additive_inverse @ additive_inverse @ equalish ) )
| ( multiplicative_identity @ additive_inverse @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(pattern_uni,[status(thm)],[1006:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse ))]]) ).
thf(5002,plain,
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4846,31]) ).
thf(5003,plain,
( ( multiplicative_identity @ ( multiplicative_identity @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[5002]) ).
thf(5022,plain,
( ( multiplicative_identity != a )
| ( ( multiplicative_identity @ ( multiplicative_identity @ multiply ) )
!= ( a @ additive_inverse @ additive_inverse ) ) ),
inference(simp,[status(thm)],[5003]) ).
thf(16,axiom,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( A @ ( B @ add ) @ ( B @ ( A @ add ) @ equalish ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_addition) ).
thf(58,plain,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( A @ ( B @ add ) @ ( B @ ( A @ add ) @ equalish ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(59,plain,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( A @ ( B @ add ) @ ( B @ ( A @ add ) @ equalish ) ) ),
inference(cnf,[status(esa)],[58]) ).
thf(110,plain,
! [C: $i,B: $i,A: $i] :
( ( ( additive_identity @ defined )
!= ( B @ defined ) )
| ~ ( C @ defined )
| ~ $true
| ~ ( A @ defined )
| ( C @ ( B @ ( A @ add ) @ add ) @ ( C @ ( B @ add ) @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[36,80]) ).
thf(111,plain,
! [C: $i,B: $i,A: $i] :
( ( ( additive_identity @ defined )
!= ( B @ defined ) )
| ~ ( C @ defined )
| ~ ( A @ defined )
| ( C @ ( B @ ( A @ add ) @ add ) @ ( C @ ( B @ add ) @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[110]) ).
thf(112,plain,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( B @ ( additive_identity @ ( A @ add ) @ add ) @ ( B @ ( additive_identity @ add ) @ ( A @ add ) @ equalish ) ) ),
inference(pattern_uni,[status(thm)],[111:[bind(A,$thf( A )),bind(B,$thf( additive_identity ))]]) ).
thf(118,plain,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( B @ ( additive_identity @ ( A @ add ) @ add ) @ ( B @ ( additive_identity @ add ) @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[112]) ).
thf(4835,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[597,55]) ).
thf(4836,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(simp,[status(thm)],[4835]) ).
thf(4837,plain,
multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ),
inference(pattern_uni,[status(thm)],[4836:[bind(A,$thf( multiplicative_identity @ additive_inverse ))]]) ).
thf(7492,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[597,66]) ).
thf(7493,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7492]) ).
thf(7494,plain,
multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ equalish ),
inference(pattern_uni,[status(thm)],[7493:[bind(A,$thf( multiplicative_identity @ additive_inverse ))]]) ).
thf(7846,plain,
( ( ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7494,31]) ).
thf(7847,plain,
( ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[7846]) ).
thf(7865,plain,
( ( ( multiplicative_identity @ additive_inverse )
!= a )
| ( ( a @ additive_inverse @ additive_inverse )
!= ( multiplicative_identity @ additive_inverse ) ) ),
inference(simp,[status(thm)],[7847]) ).
thf(829,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ~ $true
| ( A @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[654,72]) ).
thf(830,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ( A @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[829]) ).
thf(831,plain,
( ( additive_identity @ ( a @ additive_inverse @ equalish ) )
| ( a @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(pattern_uni,[status(thm)],[830:[bind(A,$thf( a @ additive_inverse ))]]) ).
thf(782,plain,
! [A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37,373]) ).
thf(783,plain,
! [A: $i] :
( ( ( multiplicative_identity @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity ) ),
inference(simp,[status(thm)],[782]) ).
thf(784,plain,
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( multiplicative_identity @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( multiplicative_identity @ add ) )
!= additive_identity ) ),
inference(pattern_uni,[status(thm)],[783:[bind(A,$thf( multiplicative_identity ))]]) ).
thf(28,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ defined )
| ~ ( B @ defined )
| ~ ( A @ defined )
| ( C @ ( B @ ( A @ multiply ) @ multiply ) @ ( C @ ( B @ multiply ) @ ( A @ multiply ) @ equalish ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_multiplication) ).
thf(81,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ defined )
| ~ ( B @ defined )
| ~ ( A @ defined )
| ( C @ ( B @ ( A @ multiply ) @ multiply ) @ ( C @ ( B @ multiply ) @ ( A @ multiply ) @ equalish ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(9769,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ equalish ) )
!= ( multiplicative_identity @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ( multiplicative_identity != a )
| ~ $true
| ~ ( A @ ( B @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[68,7735]) ).
thf(9770,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ equalish ) )
!= ( multiplicative_identity @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ( multiplicative_identity != a )
| ~ ( A @ ( B @ equalish ) ) ),
inference(simp,[status(thm)],[9769]) ).
thf(9771,plain,
( ( multiplicative_identity != a )
| ~ ( a @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ equalish ) ) ),
inference(pattern_uni,[status(thm)],[9770:[bind(A,$thf( a @ additive_inverse @ additive_inverse )),bind(B,$thf( multiplicative_identity ))]]) ).
thf(39,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( additive_identity @ less_or_equal ) )
| ~ ( A @ ( additive_identity @ less_or_equal ) )
| ( B @ ( A @ multiply ) @ ( additive_identity @ less_or_equal ) ) ),
inference(cnf,[status(esa)],[38]) ).
thf(861,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[654,373]) ).
thf(862,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity ) ),
inference(simp,[status(thm)],[861]) ).
thf(863,plain,
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( a @ additive_inverse @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( a @ additive_inverse @ add ) )
!= additive_identity ) ),
inference(pattern_uni,[status(thm)],[862:[bind(A,$thf( a @ additive_inverse ))]]) ).
thf(8066,plain,
( ( ( a @ additive_inverse @ ( a @ additive_inverse @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7563,84]) ).
thf(8067,plain,
( ( a @ additive_inverse @ ( a @ additive_inverse @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[8066]) ).
thf(8103,plain,
( ( ( a @ additive_inverse )
!= multiplicative_identity )
| ( ( a @ additive_inverse )
!= additive_identity ) ),
inference(simp,[status(thm)],[8067]) ).
thf(7799,plain,
( ( ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( additive_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7660,31]) ).
thf(7800,plain,
( ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( additive_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[7799]) ).
thf(7820,plain,
( ( additive_identity != a )
| ( ( a @ additive_inverse @ additive_inverse )
!= additive_identity ) ),
inference(simp,[status(thm)],[7800]) ).
thf(797,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[633,373]) ).
thf(798,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity ) ),
inference(simp,[status(thm)],[797]) ).
thf(799,plain,
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( additive_identity @ additive_inverse @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( additive_identity @ additive_inverse @ add ) )
!= additive_identity ) ),
inference(pattern_uni,[status(thm)],[798:[bind(A,$thf( additive_identity @ additive_inverse ))]]) ).
thf(4275,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[3154,61]) ).
thf(4276,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[4275]) ).
thf(4277,plain,
additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[4276:[bind(A,$thf( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(1111,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ~ $true
| ( A @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[822,72]) ).
thf(1112,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ equalish ) )
| ( A @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[1111]) ).
thf(1113,plain,
( ( additive_identity @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
| ( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(pattern_uni,[status(thm)],[1112:[bind(A,$thf( a @ additive_inverse @ additive_inverse ))]]) ).
thf(10010,plain,
! [A: $i] :
( ( ( additive_identity @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[36,76]) ).
thf(10011,plain,
! [A: $i] :
( ( ( additive_identity @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[10010]) ).
thf(10012,plain,
additive_identity @ ( additive_identity @ ( additive_identity @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[10011:[bind(A,$thf( additive_identity ))]]) ).
thf(10422,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( additive_identity @ ( additive_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[10012,68]) ).
thf(10423,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( additive_identity @ ( additive_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[10422]) ).
thf(10424,plain,
additive_identity @ ( additive_identity @ add ) @ ( additive_identity @ equalish ),
inference(pattern_uni,[status(thm)],[10423:[bind(A,$thf( additive_identity )),bind(B,$thf( additive_identity @ ( additive_identity @ add ) ))]]) ).
thf(35,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ less_or_equal ) )
| ~ ( B @ defined )
| ( B @ ( C @ add ) @ ( B @ ( A @ add ) @ less_or_equal ) ) ),
inference(cnf,[status(esa)],[34]) ).
thf(16574,plain,
( ( ( multiplicative_identity @ additive_inverse )
!= a )
| ( ( a @ additive_inverse )
!= multiplicative_identity ) ),
inference(simp,[status(thm)],[7865]) ).
thf(7944,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[3454,68]) ).
thf(7945,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7944]) ).
thf(7946,plain,
multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ add ) @ ( additive_identity @ equalish ),
inference(pattern_uni,[status(thm)],[7945:[bind(A,$thf( additive_identity )),bind(B,$thf( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ add ) ))]]) ).
thf(8906,plain,
( ( ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ add ) @ ( additive_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7946,84]) ).
thf(8907,plain,
( ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ add ) @ ( additive_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[8906]) ).
thf(8938,plain,
( ( ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ add ) )
!= multiplicative_identity )
| ( additive_identity != additive_identity ) ),
inference(simp,[status(thm)],[8907]) ).
thf(8949,plain,
( ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ add ) )
!= multiplicative_identity ),
inference(simp,[status(thm)],[8938]) ).
thf(7831,plain,
( ( ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7494,84]) ).
thf(7832,plain,
( ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[7831]) ).
thf(7864,plain,
( ( ( multiplicative_identity @ additive_inverse )
!= multiplicative_identity )
| ( ( multiplicative_identity @ additive_inverse )
!= additive_identity ) ),
inference(simp,[status(thm)],[7832]) ).
thf(5798,plain,
( ( ( a @ additive_inverse @ ( a @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4897,84]) ).
thf(5799,plain,
( ( a @ additive_inverse @ ( a @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[5798]) ).
thf(5822,plain,
( ( ( a @ additive_inverse )
!= multiplicative_identity )
| ( ( a @ additive_inverse @ ( multiplicative_identity @ multiply ) )
!= additive_identity ) ),
inference(simp,[status(thm)],[5799]) ).
thf(18,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ equalish ) )
| ~ ( B @ ( C @ less_or_equal ) )
| ( B @ ( A @ less_or_equal ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',compatibility_of_equality_and_order_relation) ).
thf(62,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ equalish ) )
| ~ ( B @ ( C @ less_or_equal ) )
| ( B @ ( A @ less_or_equal ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(63,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ equalish ) )
| ~ ( B @ ( C @ less_or_equal ) )
| ( B @ ( A @ less_or_equal ) ) ),
inference(cnf,[status(esa)],[62]) ).
thf(8037,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( a @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) )
| ( a @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[131,68]) ).
thf(8038,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( a @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) )
| ( a @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[8037]) ).
thf(8039,plain,
( ( a @ ( additive_identity @ equalish ) )
| ( a @ multiplicative_inverse @ defined ) ),
inference(pattern_uni,[status(thm)],[8038:[bind(A,$thf( additive_identity )),bind(B,$thf( a ))]]) ).
thf(12,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ equalish ) )
| ~ ( B @ defined )
| ( B @ ( C @ add ) @ ( B @ ( A @ add ) @ equalish ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',compatibility_of_equality_and_addition) ).
thf(50,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ equalish ) )
| ~ ( B @ defined )
| ( B @ ( C @ add ) @ ( B @ ( A @ add ) @ equalish ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(4349,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ additive_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[3221,61]) ).
thf(4350,plain,
! [A: $i] :
( ( ( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ additive_inverse @ defined ) ),
inference(simp,[status(thm)],[4349]) ).
thf(4351,plain,
a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ defined,
inference(pattern_uni,[status(thm)],[4350:[bind(A,$thf( a @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(10307,plain,
( ( ( a @ ( a @ ( additive_identity @ add ) @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9940,31]) ).
thf(10308,plain,
( ( a @ ( a @ ( additive_identity @ add ) @ equalish ) )
!= ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) ),
inference(simp,[status(thm)],[10307]) ).
thf(10333,plain,
( ( a != a )
| ( ( a @ ( additive_identity @ add ) )
!= ( a @ additive_inverse @ additive_inverse ) ) ),
inference(simp,[status(thm)],[10308]) ).
thf(10343,plain,
( ( a @ ( additive_identity @ add ) )
!= ( a @ additive_inverse @ additive_inverse ) ),
inference(simp,[status(thm)],[10333]) ).
thf(9443,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[9361,55]) ).
thf(9444,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(simp,[status(thm)],[9443]) ).
thf(9445,plain,
multiplicative_identity @ multiplicative_inverse @ ( multiplicative_identity @ multiplicative_inverse @ ( multiplicative_identity @ multiply ) @ equalish ),
inference(pattern_uni,[status(thm)],[9444:[bind(A,$thf( multiplicative_identity @ multiplicative_inverse ))]]) ).
thf(12578,plain,
! [B: $i,A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ ( multiplicative_identity @ multiplicative_inverse @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[9445,68]) ).
thf(12579,plain,
! [B: $i,A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ ( multiplicative_identity @ multiplicative_inverse @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[12578]) ).
thf(12580,plain,
multiplicative_identity @ multiplicative_inverse @ ( multiplicative_identity @ multiply ) @ ( multiplicative_identity @ multiplicative_inverse @ equalish ),
inference(pattern_uni,[status(thm)],[12579:[bind(A,$thf( multiplicative_identity @ multiplicative_inverse )),bind(B,$thf( multiplicative_identity @ multiplicative_inverse @ ( multiplicative_identity @ multiply ) ))]]) ).
thf(3491,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[1050,49]) ).
thf(3492,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[3491]) ).
thf(3493,plain,
additive_identity @ ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ additive_inverse @ ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[3492:[bind(A,$thf( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(43,plain,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( B @ ( A @ add ) @ defined ) ),
inference(cnf,[status(esa)],[42]) ).
thf(10259,plain,
! [B: $i,A: $i] :
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( additive_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[9865,68]) ).
thf(10260,plain,
! [B: $i,A: $i] :
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( additive_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[10259]) ).
thf(10261,plain,
multiplicative_identity @ ( additive_identity @ add ) @ ( multiplicative_identity @ equalish ),
inference(pattern_uni,[status(thm)],[10260:[bind(A,$thf( multiplicative_identity )),bind(B,$thf( multiplicative_identity @ ( additive_identity @ add ) ))]]) ).
thf(7587,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[732,66]) ).
thf(7588,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7587]) ).
thf(7589,plain,
additive_identity @ additive_inverse @ additive_inverse @ ( additive_identity @ additive_inverse @ additive_inverse @ equalish ),
inference(pattern_uni,[status(thm)],[7588:[bind(A,$thf( additive_identity @ additive_inverse @ additive_inverse ))]]) ).
thf(102,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ defined )
!= ( C @ defined ) )
| ~ $true
| ~ ( B @ defined )
| ~ ( A @ defined )
| ( C @ ( B @ ( A @ add ) @ add ) @ ( C @ ( B @ add ) @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[64,80]) ).
thf(103,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ defined )
!= ( C @ defined ) )
| ~ ( B @ defined )
| ~ ( A @ defined )
| ( C @ ( B @ ( A @ add ) @ add ) @ ( C @ ( B @ add ) @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[102]) ).
thf(104,plain,
! [B: $i,A: $i] :
( ~ ( B @ defined )
| ~ ( A @ defined )
| ( a @ ( B @ ( A @ add ) @ add ) @ ( a @ ( B @ add ) @ ( A @ add ) @ equalish ) ) ),
inference(pattern_uni,[status(thm)],[103:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( a ))]]) ).
thf(9419,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[9361,66]) ).
thf(9420,plain,
! [A: $i] :
( ( ( multiplicative_identity @ multiplicative_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[9419]) ).
thf(9421,plain,
multiplicative_identity @ multiplicative_inverse @ ( multiplicative_identity @ multiplicative_inverse @ equalish ),
inference(pattern_uni,[status(thm)],[9420:[bind(A,$thf( multiplicative_identity @ multiplicative_inverse ))]]) ).
thf(10174,plain,
( ( ( multiplicative_identity @ multiplicative_inverse @ ( multiplicative_identity @ multiplicative_inverse @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9421,84]) ).
thf(10175,plain,
( ( multiplicative_identity @ multiplicative_inverse @ ( multiplicative_identity @ multiplicative_inverse @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[10174]) ).
thf(10214,plain,
( ( ( multiplicative_identity @ multiplicative_inverse )
!= multiplicative_identity )
| ( ( multiplicative_identity @ multiplicative_inverse )
!= additive_identity ) ),
inference(simp,[status(thm)],[10175]) ).
thf(10288,plain,
( ( ( a @ ( a @ ( additive_identity @ add ) @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9940,84]) ).
thf(10289,plain,
( ( a @ ( a @ ( additive_identity @ add ) @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[10288]) ).
thf(10332,plain,
( ( multiplicative_identity != a )
| ( ( a @ ( additive_identity @ add ) )
!= additive_identity ) ),
inference(simp,[status(thm)],[10289]) ).
thf(10679,plain,
( ( ( additive_identity @ ( additive_identity @ add ) @ ( additive_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[10424,84]) ).
thf(10680,plain,
( ( additive_identity @ ( additive_identity @ add ) @ ( additive_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[10679]) ).
thf(10725,plain,
( ( ( additive_identity @ ( additive_identity @ add ) )
!= multiplicative_identity )
| ( additive_identity != additive_identity ) ),
inference(simp,[status(thm)],[10680]) ).
thf(10727,plain,
( ( additive_identity @ ( additive_identity @ add ) )
!= multiplicative_identity ),
inference(simp,[status(thm)],[10725]) ).
thf(10619,plain,
( ( ( a @ ( additive_identity @ add ) @ ( a @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[10321,84]) ).
thf(10620,plain,
( ( a @ ( additive_identity @ add ) @ ( a @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[10619]) ).
thf(10659,plain,
( ( ( a @ ( additive_identity @ add ) )
!= multiplicative_identity )
| ( additive_identity != a ) ),
inference(simp,[status(thm)],[10620]) ).
thf(4832,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[683,55]) ).
thf(4833,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(simp,[status(thm)],[4832]) ).
thf(4834,plain,
multiplicative_identity @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ),
inference(pattern_uni,[status(thm)],[4833:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse ))]]) ).
thf(779,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[597,373]) ).
thf(780,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( ( multiplicative_identity @ ( multiplicative_identity @ ( A @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( A @ add ) )
!= additive_identity ) ),
inference(simp,[status(thm)],[779]) ).
thf(781,plain,
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( multiplicative_identity @ additive_inverse @ add ) @ add ) )
!= multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ add ) @ ( multiplicative_identity @ additive_inverse @ add ) )
!= additive_identity ) ),
inference(pattern_uni,[status(thm)],[780:[bind(A,$thf( multiplicative_identity @ additive_inverse ))]]) ).
thf(7694,plain,
( ( ( multiplicative_identity @ ( multiplicative_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7503,84]) ).
thf(7695,plain,
( ( multiplicative_identity @ ( multiplicative_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[7694]) ).
thf(7730,plain,
( ( multiplicative_identity != multiplicative_identity )
| ( multiplicative_identity != additive_identity ) ),
inference(simp,[status(thm)],[7695]) ).
thf(7732,plain,
multiplicative_identity != additive_identity,
inference(simp,[status(thm)],[7730]) ).
thf(7962,plain,
! [B: $i,A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[4837,68]) ).
thf(7963,plain,
! [B: $i,A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[7962]) ).
thf(7964,plain,
multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ multiply ) @ ( multiplicative_identity @ additive_inverse @ equalish ),
inference(pattern_uni,[status(thm)],[7963:[bind(A,$thf( multiplicative_identity @ additive_inverse )),bind(B,$thf( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ multiply ) ))]]) ).
thf(8158,plain,
( ( ( a @ ( multiplicative_identity @ multiply ) @ ( a @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7906,84]) ).
thf(8159,plain,
( ( a @ ( multiplicative_identity @ multiply ) @ ( a @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[8158]) ).
thf(8197,plain,
( ( ( a @ ( multiplicative_identity @ multiply ) )
!= multiplicative_identity )
| ( additive_identity != a ) ),
inference(simp,[status(thm)],[8159]) ).
thf(4898,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[1050,55]) ).
thf(4899,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(simp,[status(thm)],[4898]) ).
thf(4900,plain,
additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ),
inference(pattern_uni,[status(thm)],[4899:[bind(A,$thf( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(82,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ defined )
| ~ ( B @ defined )
| ~ ( A @ defined )
| ( C @ ( B @ ( A @ multiply ) @ multiply ) @ ( C @ ( B @ multiply ) @ ( A @ multiply ) @ equalish ) ) ),
inference(cnf,[status(esa)],[81]) ).
thf(3509,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[732,49]) ).
thf(3510,plain,
! [A: $i] :
( ( ( additive_identity @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( additive_identity @ ( A @ additive_inverse @ ( A @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[3509]) ).
thf(3511,plain,
additive_identity @ ( additive_identity @ additive_inverse @ additive_inverse @ additive_inverse @ ( additive_identity @ additive_inverse @ additive_inverse @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[3510:[bind(A,$thf( additive_identity @ additive_inverse @ additive_inverse ))]]) ).
thf(51,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ equalish ) )
| ~ ( B @ defined )
| ( B @ ( C @ add ) @ ( B @ ( A @ add ) @ equalish ) ) ),
inference(cnf,[status(esa)],[50]) ).
thf(10229,plain,
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( additive_identity @ add ) @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9865,84]) ).
thf(10230,plain,
( ( multiplicative_identity @ ( multiplicative_identity @ ( additive_identity @ add ) @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[10229]) ).
thf(10265,plain,
( ( multiplicative_identity != multiplicative_identity )
| ( ( multiplicative_identity @ ( additive_identity @ add ) )
!= additive_identity ) ),
inference(simp,[status(thm)],[10230]) ).
thf(10280,plain,
( ( multiplicative_identity @ ( additive_identity @ add ) )
!= additive_identity ),
inference(simp,[status(thm)],[10265]) ).
thf(5030,plain,
( ( ( a @ ( a @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4915,84]) ).
thf(5031,plain,
( ( a @ ( a @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[5030]) ).
thf(5051,plain,
( ( multiplicative_identity != a )
| ( ( a @ ( multiplicative_identity @ multiply ) )
!= additive_identity ) ),
inference(simp,[status(thm)],[5031]) ).
thf(5090,plain,
( ( ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4837,84]) ).
thf(5091,plain,
( ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[5090]) ).
thf(5110,plain,
( ( ( multiplicative_identity @ additive_inverse )
!= multiplicative_identity )
| ( ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ multiply ) )
!= additive_identity ) ),
inference(simp,[status(thm)],[5091]) ).
thf(6486,plain,
! [A: $i] :
( ( ( additive_identity @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ ( a @ ( A @ equalish ) )
| ~ $true
| ( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[1113,4246]) ).
thf(6487,plain,
! [A: $i] :
( ( ( additive_identity @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( A @ ( a @ additive_inverse @ additive_inverse @ equalish ) ) )
| ~ ( a @ ( A @ equalish ) )
| ( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[6486]) ).
thf(6488,plain,
( ~ ( a @ ( additive_identity @ equalish ) )
| ( a @ additive_inverse @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(pattern_uni,[status(thm)],[6487:[bind(A,$thf( additive_identity ))]]) ).
thf(9857,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[597,76]) ).
thf(9858,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( additive_identity @ add ) @ equalish ) ) ),
inference(simp,[status(thm)],[9857]) ).
thf(9859,plain,
multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ ( additive_identity @ add ) @ equalish ),
inference(pattern_uni,[status(thm)],[9858:[bind(A,$thf( multiplicative_identity @ additive_inverse ))]]) ).
thf(12641,plain,
! [B: $i,A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ ( additive_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[9859,68]) ).
thf(12642,plain,
! [B: $i,A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ ( additive_identity @ add ) @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) ) ),
inference(simp,[status(thm)],[12641]) ).
thf(12643,plain,
multiplicative_identity @ additive_inverse @ ( additive_identity @ add ) @ ( multiplicative_identity @ additive_inverse @ equalish ),
inference(pattern_uni,[status(thm)],[12642:[bind(A,$thf( multiplicative_identity @ additive_inverse )),bind(B,$thf( multiplicative_identity @ additive_inverse @ ( additive_identity @ add ) ))]]) ).
thf(47,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ equalish ) )
| ~ ( B @ defined )
| ( B @ ( C @ multiply ) @ ( B @ ( A @ multiply ) @ equalish ) ) ),
inference(cnf,[status(esa)],[46]) ).
thf(7898,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( multiplicative_identity @ additive_inverse @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) )
| ( multiplicative_identity @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[692,68]) ).
thf(7899,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( multiplicative_identity @ additive_inverse @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) )
| ( multiplicative_identity @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[7898]) ).
thf(7900,plain,
( ( multiplicative_identity @ additive_inverse @ ( additive_identity @ equalish ) )
| ( multiplicative_identity @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(pattern_uni,[status(thm)],[7899:[bind(A,$thf( additive_identity )),bind(B,$thf( multiplicative_identity @ additive_inverse ))]]) ).
thf(5000,plain,
( ( ( multiplicative_identity @ ( multiplicative_identity @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4846,84]) ).
thf(5001,plain,
( ( multiplicative_identity @ ( multiplicative_identity @ ( multiplicative_identity @ multiply ) @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[5000]) ).
thf(5023,plain,
( ( multiplicative_identity != multiplicative_identity )
| ( ( multiplicative_identity @ ( multiplicative_identity @ multiply ) )
!= additive_identity ) ),
inference(simp,[status(thm)],[5001]) ).
thf(5029,plain,
( ( multiplicative_identity @ ( multiplicative_identity @ multiply ) )
!= additive_identity ),
inference(simp,[status(thm)],[5023]) ).
thf(7709,plain,
( ( ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( multiplicative_identity @ ( multiplicative_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7503,31]) ).
thf(7710,plain,
( ( a @ ( a @ additive_inverse @ additive_inverse @ equalish ) )
!= ( multiplicative_identity @ ( multiplicative_identity @ equalish ) ) ),
inference(simp,[status(thm)],[7709]) ).
thf(7723,plain,
( ( multiplicative_identity != a )
| ( ( a @ additive_inverse @ additive_inverse )
!= multiplicative_identity ) ),
inference(simp,[status(thm)],[7710]) ).
thf(17009,plain,
( ( ( a @ additive_inverse @ additive_inverse @ ( a @ additive_inverse @ add ) @ ( additive_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7985,84]) ).
thf(17010,plain,
( ( a @ additive_inverse @ additive_inverse @ ( a @ additive_inverse @ add ) @ ( additive_identity @ equalish ) )
!= ( multiplicative_identity @ ( additive_identity @ equalish ) ) ),
inference(simp,[status(thm)],[17009]) ).
thf(17057,plain,
( ( ( a @ additive_inverse @ additive_inverse @ ( a @ additive_inverse @ add ) )
!= multiplicative_identity )
| ( additive_identity != additive_identity ) ),
inference(simp,[status(thm)],[17010]) ).
thf(17076,plain,
( ( a @ additive_inverse @ additive_inverse @ ( a @ additive_inverse @ add ) )
!= multiplicative_identity ),
inference(simp,[status(thm)],[17057]) ).
thf(4856,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ~ $true
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(paramod_ordered,[status(thm)],[998,55]) ).
thf(4857,plain,
! [A: $i] :
( ( ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ defined )
!= ( A @ defined ) )
| ( A @ ( A @ ( multiplicative_identity @ multiply ) @ equalish ) ) ),
inference(simp,[status(thm)],[4856]) ).
thf(4858,plain,
multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse @ ( multiplicative_identity @ multiply ) @ equalish ),
inference(pattern_uni,[status(thm)],[4857:[bind(A,$thf( multiplicative_identity @ additive_inverse @ additive_inverse @ additive_inverse ))]]) ).
thf(7968,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( a @ additive_inverse @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ~ $true
| ( B @ ( A @ equalish ) )
| ( a @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(paramod_ordered,[status(thm)],[831,68]) ).
thf(7969,plain,
! [B: $i,A: $i] :
( ( ( additive_identity @ ( a @ additive_inverse @ equalish ) )
!= ( A @ ( B @ equalish ) ) )
| ( B @ ( A @ equalish ) )
| ( a @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(simp,[status(thm)],[7968]) ).
thf(7970,plain,
( ( a @ additive_inverse @ ( additive_identity @ equalish ) )
| ( a @ additive_inverse @ multiplicative_inverse @ defined ) ),
inference(pattern_uni,[status(thm)],[7969:[bind(A,$thf( additive_identity )),bind(B,$thf( a @ additive_inverse ))]]) ).
thf(25381,plain,
$false,
inference(e,[status(thm)],[69,7660,8415,1211,115,683,9373,741,7781,597,56,7949,814,1260,3577,13975,42,7729,3466,37,3597,3221,10121,7825,10863,7877,1059,52,3442,3463,46,93,57,78,7997,817,12706,5027,7818,84,11971,8411,10070,61,692,9865,998,116,74,1104,9007,3559,7952,16401,2382,7735,60,10313,117,4915,1091,17325,16484,70,3154,8899,7906,33,5044,38,8145,7503,1159,3445,8048,65,3499,3556,7923,5854,12769,1143,1534,7917,2694,3087,2631,53,7774,4983,4425,4861,7976,1039,8467,5080,77,7668,4846,654,9581,1050,5058,41,5026,3454,73,1814,633,3587,4906,7941,3508,11539,7985,45,7491,7920,4017,13618,4921,298,32,34,64,10321,9418,1007,732,44,2568,5022,59,118,71,2193,54,4837,7865,2319,49,2442,831,784,81,9771,9920,76,39,7731,863,9931,8103,7820,66,799,4897,1162,4277,2757,1113,10424,80,35,3490,10456,1758,16574,8949,2256,7864,48,5822,63,8039,50,67,7494,4351,7583,10343,10012,12580,9445,31,3493,1702,4246,72,43,3288,10261,7589,104,10214,10332,10018,10727,1590,10659,55,4834,781,1646,7732,40,7964,1101,8197,4900,9940,75,58,9421,82,1309,7574,7946,3511,36,30,51,10280,373,9361,5051,5110,79,6488,9859,822,68,62,12643,7563,131,47,7900,5029,83,7723,17076,4977,4858,7823,7970]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : FLD007-1 : TPTP v9.3.1. Bugfixed v2.1.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.12/0.39 % Computer : n026.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 02:23:25 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/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
% 1.08/1.15 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.71/1.45 % [INFO] Parsing done (297ms).
% 1.71/1.47 % [INFO] Running in sequential loop mode.
% 2.99/2.05 % [INFO] eprover registered as external prover.
% 2.99/2.06 % [INFO] Scanning for conjecture ...
% 3.18/2.19 % [INFO] Found a conjecture (or negated_conjecture) and 28 axioms. Running axiom selection ...
% 3.25/2.28 % [INFO] Axiom selection finished. Selected 28 axioms (removed 0 axioms).
% 3.46/2.35 % [INFO] Problem is propositional (TPTP CNF).
% 3.46/2.35 % [INFO] Type checking passed.
% 3.46/2.36 % [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 ...
% 101.17/24.05 % External prover 'e' found a proof!
% 101.17/24.05 % [INFO] Killing All external provers ...
% 101.74/24.05 % Time passed: 23444ms (effective reasoning time: 22568ms)
% 101.74/24.05 % Axioms used in derivation (28): existence_of_identity_multiplication, transitivity_of_order_relation, associativity_multiplication, well_definedness_of_additive_identity, compatibility_of_order_relation_and_multiplication, well_definedness_of_multiplication, existence_of_identity_addition, transitivity_of_equality, reflexivity_of_equality, totality_of_order_relation, commutativity_addition, commutativity_multiplication, existence_of_inverse_addition, well_definedness_of_addition, distributivity, compatibility_of_equality_and_multiplication, a_is_defined, antisymmetry_of_order_relation, associativity_addition, compatibility_of_equality_and_addition, existence_of_inverse_multiplication, well_definedness_of_multiplicative_identity, well_definedness_of_additive_inverse, symmetry_of_equality, different_identities, well_definedness_of_multiplicative_inverse, compatibility_of_equality_and_order_relation, compatibility_of_order_relation_and_addition
% 101.74/24.05 % No. of inferences in proof: 688
% 101.74/24.06 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p : 23444 ms resp. 22568 ms w/o parsing
% 99.32/24.38 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 99.32/24.39 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------