%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : HEN011-4 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n005.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:31:42 AM UTC 2026
% Result : Unsatisfiable 154.09s 40.98s
% Output : Refutation 155.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 18
% Syntax : Number of formulae : 553 ( 185 unt; 0 typ; 0 def)
% Number of atoms : 1452 ( 676 equ; 0 cnn)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 5824 ( 859 ~; 591 |; 0 &;4374 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 9 ( 6 usr; 6 con; 0-2 aty)
% Number of variables : 907 ( 0 ^; 907 !; 0 ?; 907 :)
% Comments :
%------------------------------------------------------------------------------
thf(divide_decl,type,
divide: $i > $i > $i ).
thf(identity_decl,type,
identity: $i ).
thf(a_decl,type,
a: $i ).
thf(b_decl,type,
b: $i ).
thf(less_equal_decl,type,
less_equal: $i > $i > $o ).
thf(zero_decl,type,
zero: $i ).
thf(10,axiom,
! [A: $i] :
( ( A @ ( A @ divide ) )
= zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_divide_x_is_zero) ).
thf(38,plain,
! [A: $i] :
( ( A @ ( A @ divide ) )
= zero ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(39,plain,
! [A: $i] :
( ( A @ ( A @ divide ) )
= zero ),
inference(lifteq,[status(thm)],[38]) ).
thf(6,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ less_equal ) )
| ( ( B @ ( A @ divide ) )
!= zero ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_less_equal2) ).
thf(30,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ less_equal ) )
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(31,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ less_equal ) )
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(cnf,[status(esa)],[30]) ).
thf(32,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ less_equal ) )
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(lifteq,[status(thm)],[31]) ).
thf(1184,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ divide ) )
!= ( C @ ( B @ divide ) ) )
| ( C @ ( B @ less_equal ) )
| ( zero != zero ) ),
inference(paramod_ordered,[status(thm)],[39,32]) ).
thf(1185,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ divide ) )
!= ( C @ ( B @ divide ) ) )
| ( C @ ( B @ less_equal ) ) ),
inference(simp,[status(thm)],[1184]) ).
thf(1186,plain,
! [A: $i] : ( A @ ( A @ less_equal ) ),
inference(pattern_uni,[status(thm)],[1185:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(5,axiom,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( A @ divide ) @ less_equal ) )
| ~ ( C @ ( B @ ( A @ divide ) @ less_equal ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',property_of_divide1) ).
thf(28,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( A @ divide ) @ less_equal ) )
| ~ ( C @ ( B @ ( A @ divide ) @ less_equal ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(29,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( A @ divide ) @ less_equal ) )
| ~ ( C @ ( B @ ( A @ divide ) @ less_equal ) ) ),
inference(cnf,[status(esa)],[28]) ).
thf(1279,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1186,29]) ).
thf(1280,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[1279]) ).
thf(1281,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( A @ divide ) @ ( A @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[1280:[bind(A,$thf( H @ ( G @ divide ) )),bind(B,$thf( G )),bind(C,$thf( H )),bind(D,$thf( H @ ( G @ divide ) ))]]) ).
thf(1300,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( A @ divide ) @ ( A @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[1281]) ).
thf(1388,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ divide ) )
!= ( C @ ( B @ divide ) ) )
| ( C @ ( zero @ ( B @ divide ) @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[39,1300]) ).
thf(1389,plain,
! [A: $i] : ( A @ ( zero @ ( A @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[1388:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(13,axiom,
! [A: $i] : ( identity @ ( A @ less_equal ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_is_largest) ).
thf(43,plain,
! [A: $i] : ( identity @ ( A @ less_equal ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(986,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43,29]) ).
thf(987,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[986]) ).
thf(988,plain,
! [B: $i,A: $i] : ( B @ ( identity @ ( A @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[987:[bind(A,$thf( F @ ( E @ divide ) )),bind(B,$thf( E )),bind(C,$thf( F )),bind(D,$thf( identity ))]]) ).
thf(1002,plain,
! [B: $i,A: $i] : ( B @ ( identity @ ( A @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[988]) ).
thf(14,axiom,
! [A: $i] :
( ( identity @ ( A @ divide ) )
= zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',everything_divide_id_is_zero) ).
thf(44,plain,
! [A: $i] :
( ( identity @ ( A @ divide ) )
= zero ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(45,plain,
! [A: $i] :
( ( identity @ ( A @ divide ) )
= zero ),
inference(lifteq,[status(thm)],[44]) ).
thf(1015,plain,
! [A: $i] : ( A @ ( zero @ less_equal ) ),
inference(rewrite,[status(thm)],[1002,45]) ).
thf(4,axiom,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_equal_and_equal) ).
thf(25,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(26,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(cnf,[status(esa)],[25]) ).
thf(27,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[26]) ).
thf(1,negated_conjecture,
( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
thf(19,plain,
( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(20,plain,
( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) ) ),
inference(polarity_switch,[status(thm)],[19]) ).
thf(21,plain,
( ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ),
inference(lifteq,[status(thm)],[20]) ).
thf(61,plain,
( ( ( b @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( b @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) ) ) ),
inference(simp,[status(thm)],[21]) ).
thf(98,plain,
( ( ( b @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) ) )
| ( identity != identity )
| ( ( b @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) ) ) ),
inference(simp,[status(thm)],[61]) ).
thf(168,plain,
( ( b @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) ) ),
inference(simp,[status(thm)],[98]) ).
thf(250,plain,
( ( b != a )
| ( identity != identity ) ),
inference(simp,[status(thm)],[168]) ).
thf(258,plain,
b != a,
inference(simp,[status(thm)],[250]) ).
thf(556,plain,
! [B: $i,A: $i] :
( ( A != b )
| ( B != a )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[27,258]) ).
thf(557,plain,
! [A: $i] :
( ( A != a )
| ~ ( b @ ( A @ less_equal ) )
| ~ ( A @ ( b @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[556:[bind(A,$thf( b ))]]) ).
thf(658,plain,
( ~ ( b @ ( a @ less_equal ) )
| ~ ( a @ ( b @ less_equal ) ) ),
inference(simp,[status(thm)],[557]) ).
thf(1123,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( a @ ( b @ less_equal ) ) )
| ~ ( b @ ( a @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1015,658]) ).
thf(1124,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( a @ ( b @ less_equal ) ) )
| ~ ( b @ ( a @ less_equal ) ) ),
inference(simp,[status(thm)],[1123]) ).
thf(1141,plain,
! [A: $i] :
( ( A != a )
| ( zero != b )
| ~ ( b @ ( a @ less_equal ) ) ),
inference(simp,[status(thm)],[1124]) ).
thf(1160,plain,
( ( zero != b )
| ~ ( b @ ( a @ less_equal ) ) ),
inference(simp,[status(thm)],[1141]) ).
thf(2244,plain,
! [A: $i] :
( ( ( A @ ( zero @ ( A @ divide ) @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ( zero != b )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1389,1160]) ).
thf(2245,plain,
! [A: $i] :
( ( ( A @ ( zero @ ( A @ divide ) @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ( zero != b ) ),
inference(simp,[status(thm)],[2244]) ).
thf(2273,plain,
! [A: $i] :
( ( A != b )
| ( ( zero @ ( A @ divide ) )
!= a )
| ( zero != b ) ),
inference(simp,[status(thm)],[2245]) ).
thf(2282,plain,
( ( ( zero @ ( b @ divide ) )
!= a )
| ( zero != b ) ),
inference(simp,[status(thm)],[2273]) ).
thf(1125,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ~ $true
| ~ ( a @ ( b @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[1015,658]) ).
thf(1126,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ~ ( a @ ( b @ less_equal ) ) ),
inference(simp,[status(thm)],[1125]) ).
thf(1149,plain,
! [A: $i] :
( ( A != b )
| ( zero != a )
| ~ ( a @ ( b @ less_equal ) ) ),
inference(simp,[status(thm)],[1126]) ).
thf(1168,plain,
( ( zero != a )
| ~ ( a @ ( b @ less_equal ) ) ),
inference(simp,[status(thm)],[1149]) ).
thf(15,axiom,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) )
= zero )
| ~ ( B @ ( A @ less_equal ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_less_equal1) ).
thf(46,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) )
= zero )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(47,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) )
= zero )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(cnf,[status(esa)],[46]) ).
thf(48,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ less_equal ) )
| ( ( B @ ( A @ divide ) )
= zero ) ),
inference(lifteq,[status(thm)],[47]) ).
thf(2474,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ divide ) @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ~ $true
| ( ( C @ ( B @ divide ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[1389,48]) ).
thf(2475,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ divide ) @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ( ( C @ ( B @ divide ) )
= zero ) ),
inference(simp,[status(thm)],[2474]) ).
thf(2476,plain,
! [A: $i] :
( ( A @ ( zero @ ( A @ divide ) @ divide ) )
= zero ),
inference(pattern_uni,[status(thm)],[2475:[bind(A,$thf( D )),bind(B,$thf( zero @ ( D @ divide ) )),bind(C,$thf( D ))]]) ).
thf(2522,plain,
! [A: $i] :
( ( A @ ( zero @ ( A @ divide ) @ divide ) )
= zero ),
inference(simp,[status(thm)],[2476]) ).
thf(3254,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ divide ) @ divide ) )
!= ( C @ ( B @ divide ) ) )
| ( C @ ( zero @ ( B @ divide ) @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[2522,1300]) ).
thf(3255,plain,
! [A: $i] : ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[3254:[bind(A,$thf( D )),bind(B,$thf( zero @ ( D @ divide ) )),bind(C,$thf( D ))]]) ).
thf(3323,plain,
! [A: $i] : ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[3255]) ).
thf(5536,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3323,29]) ).
thf(5537,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[5536]) ).
thf(5538,plain,
! [A: $i] : ( zero @ ( A @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[5537:[bind(A,$thf( E )),bind(B,$thf( zero @ ( E @ divide ) )),bind(C,$thf( zero )),bind(D,$thf( E ))]]) ).
thf(5628,plain,
! [A: $i] : ( zero @ ( A @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[5538]) ).
thf(6178,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ~ $true
| ( ( C @ ( B @ divide ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[5628,48]) ).
thf(6179,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ( ( C @ ( B @ divide ) )
= zero ) ),
inference(simp,[status(thm)],[6178]) ).
thf(6180,plain,
! [A: $i] :
( ( zero @ ( A @ ( zero @ ( A @ divide ) @ divide ) @ divide ) )
= zero ),
inference(pattern_uni,[status(thm)],[6179:[bind(A,$thf( E )),bind(B,$thf( E @ ( zero @ ( E @ divide ) @ divide ) )),bind(C,$thf( zero ))]]) ).
thf(6231,plain,
! [A: $i] :
( ( zero @ ( A @ ( zero @ ( A @ divide ) @ divide ) @ divide ) )
= zero ),
inference(simp,[status(thm)],[6180]) ).
thf(9,axiom,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ divide ) @ ( B @ ( C @ divide ) @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',property_of_divide2) ).
thf(36,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ divide ) @ ( B @ ( C @ divide ) @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(37,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ divide ) @ ( B @ ( C @ divide ) @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(cnf,[status(esa)],[36]) ).
thf(1523,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ( B @ ( D @ divide ) @ ( C @ ( D @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43,37]) ).
thf(1524,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ( B @ ( D @ divide ) @ ( C @ ( D @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[1523]) ).
thf(1525,plain,
! [B: $i,A: $i] : ( A @ ( B @ divide ) @ ( identity @ ( B @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[1524:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( identity ))]]) ).
thf(1551,plain,
! [B: $i,A: $i] : ( A @ ( B @ divide ) @ ( identity @ ( B @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[1525]) ).
thf(41068,plain,
! [B: $i,A: $i] : ( A @ ( B @ divide ) @ ( zero @ less_equal ) ),
inference(rewrite,[status(thm)],[1551,45]) ).
thf(3,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less_equal ) )
| ~ ( C @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_of_less_equal) ).
thf(23,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less_equal ) )
| ~ ( C @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(24,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less_equal ) )
| ~ ( C @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(cnf,[status(esa)],[23]) ).
thf(272,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ( D @ ( B @ less_equal ) )
| ~ ( D @ ( C @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43,24]) ).
thf(273,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ( D @ ( B @ less_equal ) )
| ~ ( D @ ( C @ less_equal ) ) ),
inference(simp,[status(thm)],[272]) ).
thf(274,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ less_equal ) )
| ~ ( B @ ( identity @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[273:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( identity ))]]) ).
thf(280,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ less_equal ) )
| ~ ( B @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[274]) ).
thf(26087,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ( zero != b )
| ~ $true
| ~ ( B @ ( identity @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[280,1160]) ).
thf(26088,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ( zero != b )
| ~ ( B @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[26087]) ).
thf(26089,plain,
( ( zero != b )
| ~ ( b @ ( identity @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[26088:[bind(A,$thf( a )),bind(B,$thf( b ))]]) ).
thf(27984,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( b @ ( identity @ less_equal ) ) )
| ( zero != b )
| ~ $true
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[32,26089]) ).
thf(27985,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( b @ ( identity @ less_equal ) ) )
| ( zero != b )
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[27984]) ).
thf(27986,plain,
( ( zero != b )
| ( ( b @ ( identity @ divide ) )
!= zero ) ),
inference(pattern_uni,[status(thm)],[27985:[bind(A,$thf( identity )),bind(B,$thf( b ))]]) ).
thf(8,axiom,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ divide ) @ less_equal ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_smaller_than_numerator) ).
thf(35,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ divide ) @ less_equal ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(326,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( D @ ( C @ less_equal ) ) )
| ( E @ ( C @ less_equal ) )
| ~ ( E @ ( D @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,24]) ).
thf(327,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( D @ ( C @ less_equal ) ) )
| ( E @ ( C @ less_equal ) )
| ~ ( E @ ( D @ less_equal ) ) ),
inference(simp,[status(thm)],[326]) ).
thf(328,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ divide ) @ less_equal ) )
| ~ ( A @ ( B @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[327:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( G @ ( F @ divide ) )),bind(D,$thf( F ))]]) ).
thf(340,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ divide ) @ less_equal ) )
| ~ ( A @ ( B @ less_equal ) ) ),
inference(simp,[status(thm)],[328]) ).
thf(940,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( E @ ( D @ ( C @ divide ) @ less_equal ) ) )
| ( D @ ( E @ ( C @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,29]) ).
thf(941,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( E @ ( D @ ( C @ divide ) @ less_equal ) ) )
| ( D @ ( E @ ( C @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[940]) ).
thf(942,plain,
! [B: $i,A: $i] : ( B @ ( A @ ( A @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[941:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B )),bind(E,$thf( A ))]]) ).
thf(2377,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( A @ divide ) @ less_equal ) )
!= ( D @ ( C @ less_equal ) ) )
| ~ $true
| ( ( D @ ( C @ divide ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[942,48]) ).
thf(2378,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( A @ divide ) @ less_equal ) )
!= ( D @ ( C @ less_equal ) ) )
| ( ( D @ ( C @ divide ) )
= zero ) ),
inference(simp,[status(thm)],[2377]) ).
thf(2379,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( B @ divide ) @ divide ) )
= zero ),
inference(pattern_uni,[status(thm)],[2378:[bind(A,$thf( F )),bind(B,$thf( B )),bind(C,$thf( F @ ( F @ divide ) )),bind(D,$thf( B ))]]) ).
thf(2534,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( B @ divide ) @ divide ) )
= zero ),
inference(simp,[status(thm)],[2379]) ).
thf(16669,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ divide ) @ divide ) )
!= ( D @ ( C @ divide ) ) )
| ( D @ ( zero @ ( C @ divide ) @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[2534,1300]) ).
thf(16670,plain,
! [B: $i,A: $i] : ( A @ ( zero @ ( B @ ( B @ divide ) @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[16669:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( F @ ( F @ divide ) )),bind(D,$thf( A ))]]) ).
thf(16915,plain,
! [B: $i,A: $i] : ( A @ ( zero @ ( B @ ( B @ divide ) @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[16670]) ).
thf(27987,plain,
! [A: $i] :
( ( ( A @ ( zero @ ( A @ divide ) @ less_equal ) )
!= ( b @ ( identity @ less_equal ) ) )
| ( zero != b )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1389,26089]) ).
thf(27988,plain,
! [A: $i] :
( ( ( A @ ( zero @ ( A @ divide ) @ less_equal ) )
!= ( b @ ( identity @ less_equal ) ) )
| ( zero != b ) ),
inference(simp,[status(thm)],[27987]) ).
thf(28045,plain,
! [A: $i] :
( ( A != b )
| ( ( zero @ ( A @ divide ) )
!= identity )
| ( zero != b ) ),
inference(simp,[status(thm)],[27988]) ).
thf(28074,plain,
( ( ( zero @ ( b @ divide ) )
!= identity )
| ( zero != b ) ),
inference(simp,[status(thm)],[28045]) ).
thf(17,axiom,
! [A: $i] :
( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) )
= ( A @ ( identity @ divide ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',one_inversion_equals_three) ).
thf(51,plain,
! [A: $i] :
( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) )
= ( A @ ( identity @ divide ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(52,plain,
! [A: $i] :
( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) )
= ( A @ ( identity @ divide ) ) ),
inference(lifteq,[status(thm)],[51]) ).
thf(368,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) ) )
| ( ( A @ ( identity @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(paramod_ordered,[status(thm)],[52,21]) ).
thf(406,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( b @ ( identity @ divide ) )
!= identity )
| ( A
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( a @ ( identity @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[368]) ).
thf(432,plain,
( ( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( b @ ( identity @ divide ) )
!= identity )
| ( ( a @ ( identity @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[406]) ).
thf(45265,plain,
( ( ( b @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( b @ ( identity @ divide ) )
!= identity )
| ( ( a @ ( identity @ divide ) )
!= identity ) ),
inference(rewrite,[status(thm)],[432,52]) ).
thf(2241,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ divide ) @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1389,29]) ).
thf(2242,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ divide ) @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[2241]) ).
thf(2243,plain,
! [A: $i] : ( zero @ ( A @ ( A @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[2242:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( zero )),bind(D,$thf( A ))]]) ).
thf(2585,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ divide ) @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ~ $true
| ( ( C @ ( B @ divide ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[2243,48]) ).
thf(2586,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ divide ) @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ( ( C @ ( B @ divide ) )
= zero ) ),
inference(simp,[status(thm)],[2585]) ).
thf(2587,plain,
! [A: $i] :
( ( zero @ ( A @ ( A @ divide ) @ divide ) )
= zero ),
inference(pattern_uni,[status(thm)],[2586:[bind(A,$thf( E )),bind(B,$thf( E @ ( E @ divide ) )),bind(C,$thf( zero ))]]) ).
thf(2613,plain,
! [A: $i] :
( ( zero @ ( A @ ( A @ divide ) @ divide ) )
= zero ),
inference(simp,[status(thm)],[2587]) ).
thf(3534,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ divide ) @ divide ) )
!= ( C @ ( B @ divide ) ) )
| ( C @ ( zero @ ( B @ divide ) @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[2613,1300]) ).
thf(3535,plain,
! [A: $i] : ( zero @ ( zero @ ( A @ ( A @ divide ) @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[3534:[bind(A,$thf( E )),bind(B,$thf( E @ ( E @ divide ) )),bind(C,$thf( zero ))]]) ).
thf(3634,plain,
! [A: $i] : ( zero @ ( zero @ ( A @ ( A @ divide ) @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[3535]) ).
thf(12,axiom,
! [C: $i,B: $i,A: $i] : ( B @ ( C @ ( A @ divide ) @ divide ) @ ( B @ ( C @ divide ) @ ( B @ ( A @ divide ) @ divide ) @ less_equal ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_property) ).
thf(42,plain,
! [C: $i,B: $i,A: $i] : ( B @ ( C @ ( A @ divide ) @ divide ) @ ( B @ ( C @ divide ) @ ( B @ ( A @ divide ) @ divide ) @ less_equal ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(11,axiom,
! [A: $i] :
( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( A @ ( identity @ divide ) @ divide ) )
= ( A @ ( identity @ divide ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',property_of_inversion) ).
thf(40,plain,
! [A: $i] :
( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( A @ ( identity @ divide ) @ divide ) )
= ( A @ ( identity @ divide ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(41,plain,
! [A: $i] :
( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( A @ ( identity @ divide ) @ divide ) )
= ( A @ ( identity @ divide ) ) ),
inference(lifteq,[status(thm)],[40]) ).
thf(1503,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ( B @ ( D @ divide ) @ ( C @ ( D @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1015,37]) ).
thf(1504,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ( B @ ( D @ divide ) @ ( C @ ( D @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[1503]) ).
thf(1505,plain,
! [B: $i,A: $i] : ( zero @ ( B @ divide ) @ ( A @ ( B @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[1504:[bind(A,$thf( A )),bind(B,$thf( zero )),bind(C,$thf( A ))]]) ).
thf(1539,plain,
! [B: $i,A: $i] : ( zero @ ( B @ divide ) @ ( A @ ( B @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[1505]) ).
thf(32309,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( A @ ( identity @ divide ) @ divide ) )
!= ( B @ ( C @ divide ) ) )
| ( zero @ ( C @ divide ) @ ( A @ ( identity @ divide ) @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[41,1539]) ).
thf(32310,plain,
! [A: $i] : ( zero @ ( A @ ( identity @ divide ) @ divide ) @ ( A @ ( identity @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[32309:[bind(A,$thf( I )),bind(B,$thf( I @ ( identity @ divide ) @ ( identity @ divide ) )),bind(C,$thf( I @ ( identity @ divide ) ))]]) ).
thf(32484,plain,
! [A: $i] : ( zero @ ( A @ ( identity @ divide ) @ divide ) @ ( A @ ( identity @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[32310]) ).
thf(35237,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( identity @ divide ) @ divide ) @ ( A @ ( identity @ divide ) @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32484,29]) ).
thf(35238,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( identity @ divide ) @ divide ) @ ( A @ ( identity @ divide ) @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[35237]) ).
thf(35239,plain,
! [A: $i] : ( A @ ( zero @ ( A @ ( identity @ divide ) @ divide ) @ ( identity @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[35238:[bind(A,$thf( H )),bind(B,$thf( identity )),bind(C,$thf( H )),bind(D,$thf( zero @ ( H @ ( identity @ divide ) @ divide ) ))]]) ).
thf(35538,plain,
! [A: $i] : ( A @ ( zero @ ( A @ ( identity @ divide ) @ divide ) @ ( identity @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[35239]) ).
thf(16,axiom,
! [A: $i] :
( ( A @ ( zero @ divide ) )
= zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',zero_divide_anything_is_zero) ).
thf(49,plain,
! [A: $i] :
( ( A @ ( zero @ divide ) )
= zero ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(50,plain,
! [A: $i] :
( ( A @ ( zero @ divide ) )
= zero ),
inference(lifteq,[status(thm)],[49]) ).
thf(285,plain,
! [A: $i] :
( ( ( A @ ( A @ divide ) )
!= ( a @ ( identity @ divide ) ) )
| ( ( zero @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(paramod_ordered,[status(thm)],[39,21]) ).
thf(305,plain,
! [A: $i] :
( ( A != a )
| ( A != identity )
| ( ( zero @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(simp,[status(thm)],[285]) ).
thf(317,plain,
( ( a != identity )
| ( ( zero @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(simp,[status(thm)],[305]) ).
thf(373,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ divide ) )
!= ( B @ ( identity @ divide ) ) )
| ( ( zero @ ( identity @ divide ) @ ( identity @ divide ) )
= ( B @ ( identity @ divide ) ) ) ),
inference(paramod_ordered,[status(thm)],[39,52]) ).
thf(374,plain,
( ( zero @ ( identity @ divide ) @ ( identity @ divide ) )
= ( identity @ ( identity @ divide ) ) ),
inference(pattern_uni,[status(thm)],[373:[bind(A,$thf( identity )),bind(B,$thf( identity ))]]) ).
thf(759,plain,
( ( zero @ ( identity @ divide ) @ ( identity @ divide ) )
= zero ),
inference(rewrite,[status(thm)],[374,39]) ).
thf(1190,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( B @ ( A @ divide ) ) )
| ( B @ ( A @ less_equal ) )
| ( zero != zero ) ),
inference(paramod_ordered,[status(thm)],[759,32]) ).
thf(1191,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( B @ ( A @ divide ) ) )
| ( B @ ( A @ less_equal ) ) ),
inference(simp,[status(thm)],[1190]) ).
thf(1192,plain,
zero @ ( identity @ divide ) @ ( identity @ less_equal ),
inference(pattern_uni,[status(thm)],[1191:[bind(A,$thf( identity )),bind(B,$thf( zero @ ( identity @ divide ) ))]]) ).
thf(26092,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( identity @ divide ) @ ( identity @ less_equal ) )
!= ( B @ ( identity @ less_equal ) ) )
| ( B @ ( A @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1192,280]) ).
thf(26093,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( identity @ divide ) @ ( identity @ less_equal ) )
!= ( B @ ( identity @ less_equal ) ) )
| ( B @ ( A @ less_equal ) ) ),
inference(simp,[status(thm)],[26092]) ).
thf(26094,plain,
! [A: $i] : ( zero @ ( identity @ divide ) @ ( A @ less_equal ) ),
inference(pattern_uni,[status(thm)],[26093:[bind(A,$thf( A )),bind(B,$thf( zero @ ( identity @ divide ) ))]]) ).
thf(26386,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( identity @ divide ) @ ( A @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ~ $true
| ( ( C @ ( B @ divide ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[26094,48]) ).
thf(26387,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( identity @ divide ) @ ( A @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ( ( C @ ( B @ divide ) )
= zero ) ),
inference(simp,[status(thm)],[26386]) ).
thf(26388,plain,
! [A: $i] :
( ( zero @ ( identity @ divide ) @ ( A @ divide ) )
= zero ),
inference(pattern_uni,[status(thm)],[26387:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( zero @ ( identity @ divide ) ))]]) ).
thf(31403,plain,
( ( a != identity )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= zero ) ),
inference(rewrite,[status(thm)],[317,26388]) ).
thf(31515,plain,
! [A: $i] :
( ( ( A @ ( zero @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ( a != identity )
| ( zero != zero ) ),
inference(paramod_ordered,[status(thm)],[50,31403]) ).
thf(31516,plain,
! [A: $i] :
( ( ( A @ ( zero @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ( a != identity ) ),
inference(simp,[status(thm)],[31515]) ).
thf(31600,plain,
! [A: $i] :
( ( A
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( a @ ( identity @ divide ) )
!= zero )
| ( a != identity ) ),
inference(simp,[status(thm)],[31516]) ).
thf(31650,plain,
( ( ( a @ ( identity @ divide ) )
!= zero )
| ( a != identity ) ),
inference(simp,[status(thm)],[31600]) ).
thf(40880,plain,
! [A: $i] :
( ( ( A @ ( A @ divide ) )
!= ( a @ ( identity @ divide ) ) )
| ( zero != zero )
| ( a != identity ) ),
inference(paramod_ordered,[status(thm)],[39,31650]) ).
thf(40881,plain,
! [A: $i] :
( ( ( A @ ( A @ divide ) )
!= ( a @ ( identity @ divide ) ) )
| ( a != identity ) ),
inference(simp,[status(thm)],[40880]) ).
thf(40902,plain,
! [A: $i] :
( ( A != a )
| ( A != identity )
| ( a != identity ) ),
inference(simp,[status(thm)],[40881]) ).
thf(40918,plain,
a != identity,
inference(simp,[status(thm)],[40902]) ).
thf(40933,plain,
! [B: $i,A: $i] :
( ( A != a )
| ( B != identity )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[27,40918]) ).
thf(40934,plain,
! [A: $i] :
( ( A != identity )
| ~ ( a @ ( A @ less_equal ) )
| ~ ( A @ ( a @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[40933:[bind(A,$thf( a ))]]) ).
thf(40937,plain,
( ~ ( a @ ( identity @ less_equal ) )
| ~ ( identity @ ( a @ less_equal ) ) ),
inference(simp,[status(thm)],[40934]) ).
thf(45099,plain,
( ~ ( a @ ( identity @ less_equal ) )
| ~ $true ),
inference(rewrite,[status(thm)],[40937,43]) ).
thf(45100,plain,
~ ( a @ ( identity @ less_equal ) ),
inference(simp,[status(thm)],[45099]) ).
thf(45127,plain,
! [A: $i] :
( ( ( A @ ( zero @ ( A @ ( identity @ divide ) @ divide ) @ ( identity @ divide ) @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35538,45100]) ).
thf(45128,plain,
! [A: $i] :
( ( A @ ( zero @ ( A @ ( identity @ divide ) @ divide ) @ ( identity @ divide ) @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[45127]) ).
thf(45227,plain,
! [A: $i] :
( ( A != a )
| ( ( zero @ ( A @ ( identity @ divide ) @ divide ) @ ( identity @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[45128]) ).
thf(45255,plain,
( ( zero @ ( a @ ( identity @ divide ) @ divide ) @ ( identity @ divide ) )
!= identity ),
inference(simp,[status(thm)],[45227]) ).
thf(1133,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ~ $true
| ~ ( a @ ( b @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[43,658]) ).
thf(1134,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ~ ( a @ ( b @ less_equal ) ) ),
inference(simp,[status(thm)],[1133]) ).
thf(1142,plain,
! [A: $i] :
( ( b != identity )
| ( A != a )
| ~ ( a @ ( b @ less_equal ) ) ),
inference(simp,[status(thm)],[1134]) ).
thf(1161,plain,
( ( b != identity )
| ~ ( a @ ( b @ less_equal ) ) ),
inference(simp,[status(thm)],[1142]) ).
thf(2015,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( a @ ( b @ less_equal ) ) )
| ( b != identity )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,1161]) ).
thf(2016,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( a @ ( b @ less_equal ) ) )
| ( b != identity ) ),
inference(simp,[status(thm)],[2015]) ).
thf(2027,plain,
! [B: $i,A: $i] :
( ( A != a )
| ( ( B @ ( A @ divide ) )
!= b )
| ( b != identity ) ),
inference(simp,[status(thm)],[2016]) ).
thf(2039,plain,
! [A: $i] :
( ( ( A @ ( a @ divide ) )
!= b )
| ( b != identity ) ),
inference(simp,[status(thm)],[2027]) ).
thf(251,plain,
! [A: $i] :
( ( ( A @ ( zero @ divide ) )
!= ( b @ ( identity @ divide ) ) )
| ( ( a @ ( identity @ divide ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[50,168]) ).
thf(254,plain,
! [A: $i] :
( ( A != b )
| ( zero != identity )
| ( ( a @ ( identity @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[251]) ).
thf(259,plain,
( ( zero != identity )
| ( ( a @ ( identity @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[254]) ).
thf(880,plain,
! [A: $i] :
( ( ( A @ ( zero @ divide ) )
!= ( a @ ( identity @ divide ) ) )
| ( zero != identity )
| ( zero != zero ) ),
inference(paramod_ordered,[status(thm)],[50,259]) ).
thf(881,plain,
! [A: $i] :
( ( ( A @ ( zero @ divide ) )
!= ( a @ ( identity @ divide ) ) )
| ( zero != identity ) ),
inference(simp,[status(thm)],[880]) ).
thf(908,plain,
! [A: $i] :
( ( A != a )
| ( zero != identity )
| ( zero != identity ) ),
inference(simp,[status(thm)],[881]) ).
thf(916,plain,
zero != identity,
inference(simp,[status(thm)],[908]) ).
thf(923,plain,
! [B: $i,A: $i] :
( ( A != zero )
| ( B != identity )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[27,916]) ).
thf(924,plain,
! [A: $i] :
( ( A != identity )
| ~ ( zero @ ( A @ less_equal ) )
| ~ ( A @ ( zero @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[923:[bind(A,$thf( zero ))]]) ).
thf(927,plain,
( ~ ( zero @ ( identity @ less_equal ) )
| ~ ( identity @ ( zero @ less_equal ) ) ),
inference(simp,[status(thm)],[924]) ).
thf(3652,plain,
( ~ ( zero @ ( identity @ less_equal ) )
| ~ $true ),
inference(rewrite,[status(thm)],[927,1015]) ).
thf(3653,plain,
~ ( zero @ ( identity @ less_equal ) ),
inference(simp,[status(thm)],[3652]) ).
thf(550,plain,
! [C: $i,B: $i,A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ~ ( B @ ( C @ less_equal ) )
| ~ $true
| ( B = C ) ),
inference(paramod_ordered,[status(thm)],[43,27]) ).
thf(551,plain,
! [C: $i,B: $i,A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ~ ( B @ ( C @ less_equal ) )
| ( B = C ) ),
inference(simp,[status(thm)],[550]) ).
thf(552,plain,
! [A: $i] :
( ~ ( A @ ( identity @ less_equal ) )
| ( A = identity ) ),
inference(pattern_uni,[status(thm)],[551:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( identity ))]]) ).
thf(65108,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( identity @ divide ) @ ( A @ less_equal ) )
!= ( B @ ( identity @ less_equal ) ) )
| ~ $true
| ( B = identity ) ),
inference(paramod_ordered,[status(thm)],[26094,552]) ).
thf(65109,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( identity @ divide ) @ ( A @ less_equal ) )
!= ( B @ ( identity @ less_equal ) ) )
| ( B = identity ) ),
inference(simp,[status(thm)],[65108]) ).
thf(65110,plain,
( ( zero @ ( identity @ divide ) )
= identity ),
inference(pattern_uni,[status(thm)],[65109:[bind(A,$thf( identity )),bind(B,$thf( zero @ ( identity @ divide ) ))]]) ).
thf(65894,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( identity @ divide ) )
!= ( A @ ( B @ divide ) ) )
| ( zero @ ( B @ divide ) @ ( identity @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[65110,1539]) ).
thf(65895,plain,
zero @ ( identity @ divide ) @ ( identity @ less_equal ),
inference(pattern_uni,[status(thm)],[65894:[bind(A,$thf( zero )),bind(B,$thf( identity ))]]) ).
thf(66987,plain,
identity @ ( identity @ less_equal ),
inference(rewrite,[status(thm)],[65895,65110]) ).
thf(5581,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ~ $true
| ( ( C @ ( B @ divide ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[3323,48]) ).
thf(5582,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ( ( C @ ( B @ divide ) )
= zero ) ),
inference(simp,[status(thm)],[5581]) ).
thf(5583,plain,
! [A: $i] :
( ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) )
= zero ),
inference(pattern_uni,[status(thm)],[5582:[bind(A,$thf( F )),bind(B,$thf( zero @ ( zero @ ( F @ divide ) @ divide ) )),bind(C,$thf( F ))]]) ).
thf(5640,plain,
! [A: $i] :
( ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) )
= zero ),
inference(simp,[status(thm)],[5583]) ).
thf(6520,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) )
!= ( C @ ( B @ divide ) ) )
| ( C @ ( zero @ ( B @ divide ) @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[5640,1300]) ).
thf(6521,plain,
! [A: $i] : ( A @ ( zero @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[6520:[bind(A,$thf( F )),bind(B,$thf( zero @ ( zero @ ( F @ divide ) @ divide ) )),bind(C,$thf( F ))]]) ).
thf(6708,plain,
! [A: $i] : ( A @ ( zero @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[6521]) ).
thf(45135,plain,
! [A: $i] :
( ( ( A @ ( zero @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6708,45100]) ).
thf(45136,plain,
! [A: $i] :
( ( A @ ( zero @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[45135]) ).
thf(45233,plain,
! [A: $i] :
( ( A != a )
| ( ( zero @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[45136]) ).
thf(45260,plain,
( ( zero @ ( zero @ ( zero @ ( a @ divide ) @ divide ) @ divide ) )
!= identity ),
inference(simp,[status(thm)],[45233]) ).
thf(7,axiom,
( ( zero @ ( a @ divide ) )
= a ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_divide_zero_is_x) ).
thf(33,plain,
( ( zero @ ( a @ divide ) )
= a ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(34,plain,
( ( zero @ ( a @ divide ) )
= a ),
inference(lifteq,[status(thm)],[33]) ).
thf(47471,plain,
( ( zero @ ( zero @ ( a @ divide ) @ divide ) )
!= identity ),
inference(rewrite,[status(thm)],[45260,34]) ).
thf(6127,plain,
! [A: $i] :
( ( ( zero @ ( A @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( zero @ ( identity @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5628,3653]) ).
thf(6128,plain,
! [A: $i] :
( ( zero @ ( A @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( zero @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[6127]) ).
thf(6209,plain,
! [A: $i] :
( ( zero != zero )
| ( ( A @ ( zero @ ( A @ divide ) @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[6128]) ).
thf(6240,plain,
! [A: $i] :
( ( A @ ( zero @ ( A @ divide ) @ divide ) )
!= identity ),
inference(simp,[status(thm)],[6209]) ).
thf(3688,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ divide ) @ ( A @ divide ) @ less_equal ) )
!= ( zero @ ( identity @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1300,3653]) ).
thf(3689,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ divide ) @ ( A @ divide ) @ less_equal ) )
!= ( zero @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[3688]) ).
thf(3696,plain,
! [B: $i,A: $i] :
( ( B != zero )
| ( ( B @ ( A @ divide ) @ ( A @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[3689]) ).
thf(3710,plain,
! [A: $i] :
( ( zero @ ( A @ divide ) @ ( A @ divide ) )
!= identity ),
inference(simp,[status(thm)],[3696]) ).
thf(4979,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ divide ) @ divide ) )
!= ( zero @ ( B @ divide ) ) )
| ( ( zero @ ( B @ divide ) )
!= identity ) ),
inference(paramod_ordered,[status(thm)],[2613,3710]) ).
thf(4980,plain,
! [A: $i] :
( ( zero @ ( A @ ( A @ divide ) @ divide ) )
!= identity ),
inference(pattern_uni,[status(thm)],[4979:[bind(A,$thf( D )),bind(B,$thf( D @ ( D @ divide ) ))]]) ).
thf(5052,plain,
! [A: $i] :
( ( zero @ ( A @ ( A @ divide ) @ divide ) )
!= identity ),
inference(simp,[status(thm)],[4980]) ).
thf(284,plain,
! [A: $i] :
( ( ( A @ ( A @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) ) )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[39,21]) ).
thf(303,plain,
! [A: $i] :
( ( A
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( A
!= ( b @ ( identity @ divide ) ) )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[284]) ).
thf(316,plain,
( ( ( a @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( b @ ( identity @ divide ) ) )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[303]) ).
thf(1588,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ( zero != b )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,1160]) ).
thf(1589,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ( zero != b ) ),
inference(simp,[status(thm)],[1588]) ).
thf(1604,plain,
! [B: $i,A: $i] :
( ( A != b )
| ( ( B @ ( A @ divide ) )
!= a )
| ( zero != b ) ),
inference(simp,[status(thm)],[1589]) ).
thf(1609,plain,
! [A: $i] :
( ( ( A @ ( b @ divide ) )
!= a )
| ( zero != b ) ),
inference(simp,[status(thm)],[1604]) ).
thf(45143,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) )
| ~ $true
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[32,45100]) ).
thf(45144,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) )
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[45143]) ).
thf(45145,plain,
( ( a @ ( identity @ divide ) )
!= zero ),
inference(pattern_uni,[status(thm)],[45144:[bind(A,$thf( identity )),bind(B,$thf( a ))]]) ).
thf(1453,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( identity @ divide ) @ ( identity @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( A @ ( C @ divide ) @ ( B @ ( C @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1192,37]) ).
thf(1454,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( identity @ divide ) @ ( identity @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( A @ ( C @ divide ) @ ( B @ ( C @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[1453]) ).
thf(1455,plain,
! [A: $i] : ( identity @ ( A @ divide ) @ ( zero @ ( identity @ divide ) @ ( A @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[1454:[bind(A,$thf( identity )),bind(B,$thf( zero @ ( identity @ divide ) )),bind(C,$thf( C ))]]) ).
thf(1546,plain,
! [A: $i] : ( identity @ ( A @ divide ) @ ( zero @ ( identity @ divide ) @ ( A @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[1455]) ).
thf(11130,plain,
! [A: $i] : ( zero @ ( zero @ ( identity @ divide ) @ ( A @ divide ) @ less_equal ) ),
inference(rewrite,[status(thm)],[1546,45]) ).
thf(11157,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( zero @ ( identity @ divide ) @ ( A @ divide ) @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11130,29]) ).
thf(11158,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( zero @ ( identity @ divide ) @ ( A @ divide ) @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[11157]) ).
thf(11159,plain,
! [A: $i] : ( zero @ ( identity @ divide ) @ ( zero @ ( A @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[11158:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( zero @ ( identity @ divide ) )),bind(D,$thf( zero ))]]) ).
thf(11761,plain,
! [A: $i] :
( ( ( zero @ ( a @ divide ) )
!= ( zero @ ( A @ divide ) ) )
| ( zero @ ( identity @ divide ) @ ( a @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[34,11159]) ).
thf(11762,plain,
zero @ ( identity @ divide ) @ ( a @ less_equal ),
inference(pattern_uni,[status(thm)],[11761:[bind(A,$thf( a ))]]) ).
thf(18,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ divide ) @ ( C @ ( A @ divide ) @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',property_of_divide3) ).
thf(53,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ divide ) @ ( C @ ( A @ divide ) @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(54,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ divide ) @ ( C @ ( A @ divide ) @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(cnf,[status(esa)],[53]) ).
thf(11968,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( identity @ divide ) @ ( a @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( C @ ( B @ divide ) @ ( C @ ( A @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11762,54]) ).
thf(11969,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( identity @ divide ) @ ( a @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( C @ ( B @ divide ) @ ( C @ ( A @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[11968]) ).
thf(11970,plain,
! [A: $i] : ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( A @ ( a @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[11969:[bind(A,$thf( a )),bind(B,$thf( zero @ ( identity @ divide ) )),bind(C,$thf( C ))]]) ).
thf(12026,plain,
! [A: $i] : ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( A @ ( a @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[11970]) ).
thf(20122,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( A @ ( a @ divide ) @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[12026,29]) ).
thf(20123,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( A @ ( a @ divide ) @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[20122]) ).
thf(20124,plain,
! [A: $i] : ( A @ ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( a @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[20123:[bind(A,$thf( F )),bind(B,$thf( a )),bind(C,$thf( F )),bind(D,$thf( F @ ( zero @ ( identity @ divide ) @ divide ) ))]]) ).
thf(20389,plain,
! [A: $i] : ( A @ ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( a @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[20124]) ).
thf(45199,plain,
! [A: $i] :
( ( ( A @ ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( a @ divide ) @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[20389,45100]) ).
thf(45200,plain,
! [A: $i] :
( ( A @ ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( a @ divide ) @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[45199]) ).
thf(45215,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( a @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[45200]) ).
thf(45244,plain,
( ( a @ ( zero @ ( identity @ divide ) @ divide ) @ ( a @ divide ) )
!= identity ),
inference(simp,[status(thm)],[45215]) ).
thf(65748,plain,
( ( a @ ( identity @ divide ) @ ( a @ divide ) )
!= identity ),
inference(rewrite,[status(thm)],[45244,65110]) ).
thf(62,plain,
( ( ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( zero @ ( a @ divide ) ) )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[34,21]) ).
thf(89,plain,
( ( ( a @ ( identity @ divide ) @ ( identity @ divide ) )
!= zero )
| ( ( b @ ( identity @ divide ) )
!= a )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= a ) ),
inference(simp,[status(thm)],[62]) ).
thf(370,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( A @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(paramod_ordered,[status(thm)],[52,21]) ).
thf(401,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) ) )
| ( identity != identity )
| ( ( A @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(simp,[status(thm)],[370]) ).
thf(428,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) ) )
| ( ( A @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(simp,[status(thm)],[401]) ).
thf(1204,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( a @ ( b @ less_equal ) ) )
| ~ ( b @ ( a @ less_equal ) )
| ~ $true
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[32,658]) ).
thf(1205,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( a @ ( b @ less_equal ) ) )
| ~ ( b @ ( a @ less_equal ) )
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[1204]) ).
thf(1206,plain,
( ~ ( b @ ( a @ less_equal ) )
| ( ( a @ ( b @ divide ) )
!= zero ) ),
inference(pattern_uni,[status(thm)],[1205:[bind(A,$thf( b )),bind(B,$thf( a ))]]) ).
thf(26078,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ~ $true
| ( ( a @ ( b @ divide ) )
!= zero )
| ~ ( B @ ( identity @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[280,1206]) ).
thf(26079,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ( ( a @ ( b @ divide ) )
!= zero )
| ~ ( B @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[26078]) ).
thf(26080,plain,
( ( ( a @ ( b @ divide ) )
!= zero )
| ~ ( b @ ( identity @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[26079:[bind(A,$thf( a )),bind(B,$thf( b ))]]) ).
thf(263,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ less_equal ) )
!= ( F @ ( E @ less_equal ) ) )
| ( F @ ( D @ less_equal ) )
| ~ $true
| ~ ( E @ ( D @ less_equal ) )
| ~ ( C @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[24,24]) ).
thf(264,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ less_equal ) )
!= ( F @ ( E @ less_equal ) ) )
| ( F @ ( D @ less_equal ) )
| ~ ( E @ ( D @ less_equal ) )
| ~ ( C @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(simp,[status(thm)],[263]) ).
thf(265,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( D @ less_equal ) )
| ~ ( A @ ( D @ less_equal ) )
| ~ ( C @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[264:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( C ))]]) ).
thf(506,plain,
! [B: $i,A: $i] :
( ( B
!= ( b @ ( identity @ divide ) ) )
| ( ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( A @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[27,21]) ).
thf(507,plain,
! [A: $i] :
( ( ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( A @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( b @ ( identity @ divide ) @ less_equal ) )
| ~ ( b @ ( identity @ divide ) @ ( A @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[506:[bind(A,$thf( A )),bind(B,$thf( b @ ( identity @ divide ) ))]]) ).
thf(6023,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( zero @ ( A @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ~ $true
| ( ( C @ ( B @ divide ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[3634,48]) ).
thf(6024,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( zero @ ( A @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ( ( C @ ( B @ divide ) )
= zero ) ),
inference(simp,[status(thm)],[6023]) ).
thf(6025,plain,
! [A: $i] :
( ( zero @ ( zero @ ( A @ ( A @ divide ) @ divide ) @ divide ) )
= zero ),
inference(pattern_uni,[status(thm)],[6024:[bind(A,$thf( G )),bind(B,$thf( zero @ ( G @ ( G @ divide ) @ divide ) )),bind(C,$thf( zero ))]]) ).
thf(6069,plain,
! [A: $i] :
( ( zero @ ( zero @ ( A @ ( A @ divide ) @ divide ) @ divide ) )
= zero ),
inference(simp,[status(thm)],[6025]) ).
thf(8693,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( zero @ ( A @ ( A @ divide ) @ divide ) @ divide ) )
!= ( zero @ ( B @ divide ) ) )
| ( ( zero @ ( B @ divide ) )
!= identity ) ),
inference(paramod_ordered,[status(thm)],[6069,3710]) ).
thf(8694,plain,
! [A: $i] :
( ( zero @ ( zero @ ( A @ ( A @ divide ) @ divide ) @ divide ) )
!= identity ),
inference(pattern_uni,[status(thm)],[8693:[bind(A,$thf( F )),bind(B,$thf( zero @ ( F @ ( F @ divide ) @ divide ) ))]]) ).
thf(9031,plain,
! [A: $i] :
( ( zero @ ( zero @ ( A @ ( A @ divide ) @ divide ) @ divide ) )
!= identity ),
inference(simp,[status(thm)],[8694]) ).
thf(32417,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ divide ) @ divide ) )
!= ( zero @ ( C @ divide ) ) )
| ( zero @ ( B @ ( C @ divide ) @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[2522,1539]) ).
thf(32418,plain,
! [A: $i] : ( zero @ ( A @ ( zero @ ( zero @ divide ) @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[32417:[bind(A,$thf( zero )),bind(B,$thf( B )),bind(C,$thf( zero @ ( zero @ divide ) ))]]) ).
thf(32478,plain,
! [A: $i] : ( zero @ ( A @ ( zero @ ( zero @ divide ) @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[32418]) ).
thf(32899,plain,
zero @ ( zero @ less_equal ),
inference(rewrite,[status(thm)],[32478,2534]) ).
thf(498,plain,
! [B: $i,A: $i] :
( ( B != identity )
| ( ( a @ ( identity @ divide ) @ ( A @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[27,21]) ).
thf(499,plain,
! [A: $i] :
( ( ( a @ ( identity @ divide ) @ ( A @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( identity @ less_equal ) )
| ~ ( identity @ ( A @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[498:[bind(A,$thf( A )),bind(B,$thf( identity ))]]) ).
thf(56339,plain,
! [A: $i] :
( ( ( a @ ( identity @ divide ) @ ( A @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( identity @ less_equal ) )
| ~ $true ),
inference(rewrite,[status(thm)],[499,43]) ).
thf(56340,plain,
! [A: $i] :
( ( ( a @ ( identity @ divide ) @ ( A @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[56339]) ).
thf(253,plain,
! [A: $i] :
( ( ( identity @ ( A @ divide ) )
!= ( b @ ( identity @ divide ) ) )
| ( ( a @ ( identity @ divide ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[45,168]) ).
thf(256,plain,
! [A: $i] :
( ( b != identity )
| ( A != identity )
| ( ( a @ ( identity @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[253]) ).
thf(257,plain,
( ( b != identity )
| ( ( a @ ( identity @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[256]) ).
thf(384,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) ) )
| ( b != identity )
| ( ( A @ ( identity @ divide ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[52,257]) ).
thf(411,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) )
!= a )
| ( identity != identity )
| ( b != identity )
| ( ( A @ ( identity @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[384]) ).
thf(435,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) )
!= a )
| ( b != identity )
| ( ( A @ ( identity @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[411]) ).
thf(568,plain,
! [B: $i,A: $i] :
( ( B != identity )
| ( ( b @ ( A @ divide ) )
!= ( a @ ( identity @ divide ) ) )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[27,168]) ).
thf(569,plain,
! [A: $i] :
( ( ( b @ ( A @ divide ) )
!= ( a @ ( identity @ divide ) ) )
| ~ ( A @ ( identity @ less_equal ) )
| ~ ( identity @ ( A @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[568:[bind(A,$thf( A )),bind(B,$thf( identity ))]]) ).
thf(67210,plain,
! [A: $i] :
( ( ( b @ ( A @ divide ) )
!= ( a @ ( identity @ divide ) ) )
| ~ ( A @ ( identity @ less_equal ) )
| ~ $true ),
inference(rewrite,[status(thm)],[569,43]) ).
thf(67211,plain,
! [A: $i] :
( ( ( b @ ( A @ divide ) )
!= ( a @ ( identity @ divide ) ) )
| ~ ( A @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[67210]) ).
thf(3667,plain,
! [A: $i] :
( ( ( zero @ ( A @ ( A @ divide ) @ less_equal ) )
!= ( zero @ ( identity @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2243,3653]) ).
thf(3668,plain,
! [A: $i] :
( ( zero @ ( A @ ( A @ divide ) @ less_equal ) )
!= ( zero @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[3667]) ).
thf(3702,plain,
! [A: $i] :
( ( zero != zero )
| ( ( A @ ( A @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[3668]) ).
thf(3714,plain,
! [A: $i] :
( ( A @ ( A @ divide ) )
!= identity ),
inference(simp,[status(thm)],[3702]) ).
thf(1586,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ( zero != b )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1015,1160]) ).
thf(1587,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ( zero != b ) ),
inference(simp,[status(thm)],[1586]) ).
thf(1596,plain,
! [A: $i] :
( ( A != b )
| ( zero != a )
| ( zero != b ) ),
inference(simp,[status(thm)],[1587]) ).
thf(1612,plain,
( ( zero != a )
| ( zero != b ) ),
inference(simp,[status(thm)],[1596]) ).
thf(2315,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( a @ ( b @ less_equal ) ) )
| ( zero != a )
| ~ $true
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[32,1168]) ).
thf(2316,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( a @ ( b @ less_equal ) ) )
| ( zero != a )
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[2315]) ).
thf(2317,plain,
( ( zero != a )
| ( ( a @ ( b @ divide ) )
!= zero ) ),
inference(pattern_uni,[status(thm)],[2316:[bind(A,$thf( b )),bind(B,$thf( a ))]]) ).
thf(2334,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( a @ ( b @ less_equal ) ) )
| ( zero != a )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,1168]) ).
thf(2335,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( a @ ( b @ less_equal ) ) )
| ( zero != a ) ),
inference(simp,[status(thm)],[2334]) ).
thf(2343,plain,
! [B: $i,A: $i] :
( ( A != a )
| ( ( B @ ( A @ divide ) )
!= b )
| ( zero != a ) ),
inference(simp,[status(thm)],[2335]) ).
thf(2355,plain,
! [A: $i] :
( ( ( A @ ( a @ divide ) )
!= b )
| ( zero != a ) ),
inference(simp,[status(thm)],[2343]) ).
thf(2486,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( D @ ( C @ less_equal ) ) )
| ~ $true
| ( ( D @ ( C @ divide ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[35,48]) ).
thf(2487,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( D @ ( C @ less_equal ) ) )
| ( ( D @ ( C @ divide ) )
= zero ) ),
inference(simp,[status(thm)],[2486]) ).
thf(2488,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ divide ) @ divide ) )
= zero ),
inference(pattern_uni,[status(thm)],[2487:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ divide ) )),bind(D,$thf( E ))]]) ).
thf(2526,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ divide ) @ divide ) )
= zero ),
inference(simp,[status(thm)],[2488]) ).
thf(15399,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ divide ) )
!= ( D @ ( C @ divide ) ) )
| ( D @ ( zero @ ( C @ divide ) @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[2526,1300]) ).
thf(15400,plain,
! [B: $i,A: $i] : ( A @ ( zero @ ( B @ ( A @ divide ) @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[15399:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ divide ) )),bind(D,$thf( E ))]]) ).
thf(15598,plain,
! [B: $i,A: $i] : ( A @ ( zero @ ( B @ ( A @ divide ) @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[15400]) ).
thf(45181,plain,
! [B: $i,A: $i] :
( ( ( A @ ( zero @ ( B @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15598,45100]) ).
thf(45182,plain,
! [B: $i,A: $i] :
( ( A @ ( zero @ ( B @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[45181]) ).
thf(45232,plain,
! [B: $i,A: $i] :
( ( A != a )
| ( ( zero @ ( B @ ( A @ divide ) @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[45182]) ).
thf(45259,plain,
! [A: $i] :
( ( zero @ ( A @ ( a @ divide ) @ divide ) )
!= identity ),
inference(simp,[status(thm)],[45232]) ).
thf(404,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) ) )
| ( A
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( a @ ( identity @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[368]) ).
thf(431,plain,
( ( ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( a @ ( identity @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[404]) ).
thf(44562,plain,
( ( ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( a @ ( identity @ divide ) )
!= identity ) ),
inference(rewrite,[status(thm)],[431,52]) ).
thf(502,plain,
! [B: $i,A: $i] :
( ( B
!= ( a @ ( identity @ divide ) ) )
| ( ( A @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[27,21]) ).
thf(503,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( a @ ( identity @ divide ) @ less_equal ) )
| ~ ( a @ ( identity @ divide ) @ ( A @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[502:[bind(A,$thf( A )),bind(B,$thf( a @ ( identity @ divide ) ))]]) ).
thf(496,plain,
! [B: $i,A: $i] :
( ( B != identity )
| ( ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( A @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[27,21]) ).
thf(497,plain,
! [A: $i] :
( ( ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( A @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( identity @ less_equal ) )
| ~ ( identity @ ( A @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[496:[bind(A,$thf( A )),bind(B,$thf( identity ))]]) ).
thf(54946,plain,
! [A: $i] :
( ( ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( A @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( identity @ less_equal ) )
| ~ $true ),
inference(rewrite,[status(thm)],[497,43]) ).
thf(54947,plain,
! [A: $i] :
( ( ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( A @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[54946]) ).
thf(9532,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( A @ ( zero @ ( A @ divide ) @ divide ) @ divide ) )
!= ( zero @ ( B @ divide ) ) )
| ( ( zero @ ( B @ divide ) )
!= identity ) ),
inference(paramod_ordered,[status(thm)],[6231,3710]) ).
thf(9533,plain,
! [A: $i] :
( ( zero @ ( A @ ( zero @ ( A @ divide ) @ divide ) @ divide ) )
!= identity ),
inference(pattern_uni,[status(thm)],[9532:[bind(A,$thf( D )),bind(B,$thf( D @ ( zero @ ( D @ divide ) @ divide ) ))]]) ).
thf(9835,plain,
! [A: $i] :
( ( zero @ ( A @ ( zero @ ( A @ divide ) @ divide ) @ divide ) )
!= identity ),
inference(simp,[status(thm)],[9533]) ).
thf(11050,plain,
! [B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ divide ) @ divide ) )
!= ( zero @ ( B @ divide ) ) )
| ( ( zero @ ( B @ ( zero @ divide ) @ divide ) )
!= identity ) ),
inference(paramod_ordered,[status(thm)],[2522,9835]) ).
thf(11051,plain,
( ( zero @ ( zero @ ( zero @ divide ) @ ( zero @ divide ) @ divide ) )
!= identity ),
inference(pattern_uni,[status(thm)],[11050:[bind(A,$thf( zero )),bind(B,$thf( zero @ ( zero @ divide ) ))]]) ).
thf(6425,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ divide ) @ divide ) )
!= ( zero @ ( B @ divide ) ) )
| ( ( B @ ( zero @ ( zero @ divide ) @ divide ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[2613,5640]) ).
thf(6426,plain,
! [A: $i] :
( ( A @ ( A @ divide ) @ ( zero @ ( zero @ divide ) @ divide ) )
= zero ),
inference(pattern_uni,[status(thm)],[6425:[bind(A,$thf( D )),bind(B,$thf( D @ ( D @ divide ) ))]]) ).
thf(6694,plain,
! [A: $i] :
( ( A @ ( A @ divide ) @ ( zero @ ( zero @ divide ) @ divide ) )
= zero ),
inference(simp,[status(thm)],[6426]) ).
thf(6385,plain,
! [B: $i,A: $i] :
( ( ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) )
!= ( zero @ ( B @ divide ) ) )
| ( ( B @ ( zero @ ( zero @ divide ) @ divide ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[5640,5640]) ).
thf(6386,plain,
( ( zero @ ( zero @ ( zero @ divide ) @ divide ) @ ( zero @ ( zero @ divide ) @ divide ) )
= zero ),
inference(pattern_uni,[status(thm)],[6385:[bind(A,$thf( zero )),bind(B,$thf( zero @ ( zero @ ( zero @ divide ) @ divide ) ))]]) ).
thf(7618,plain,
( ( zero @ ( zero @ divide ) )
= zero ),
inference(rewrite,[status(thm)],[6386,39,2522]) ).
thf(10240,plain,
! [A: $i] :
( ( A @ ( A @ divide ) @ ( zero @ divide ) )
= zero ),
inference(rewrite,[status(thm)],[6694,7618]) ).
thf(11539,plain,
( ( zero @ ( zero @ divide ) )
!= identity ),
inference(rewrite,[status(thm)],[11051,10240]) ).
thf(45177,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ divide ) @ ( A @ divide ) @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1300,45100]) ).
thf(45178,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ divide ) @ ( A @ divide ) @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[45177]) ).
thf(45237,plain,
! [B: $i,A: $i] :
( ( B != a )
| ( ( B @ ( A @ divide ) @ ( A @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[45178]) ).
thf(45263,plain,
! [A: $i] :
( ( a @ ( A @ divide ) @ ( A @ divide ) )
!= identity ),
inference(simp,[status(thm)],[45237]) ).
thf(65,plain,
( ( ( zero @ ( a @ divide ) )
!= ( b @ ( identity @ divide ) ) )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ divide ) ) ) ),
inference(paramod_ordered,[status(thm)],[34,21]) ).
thf(73,plain,
( ( ( zero @ ( a @ divide ) )
!= ( b @ ( identity @ divide ) ) )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( a @ ( identity @ divide ) )
!= a ) ),
inference(simp,[status(thm)],[65]) ).
thf(4195,plain,
( ( ( b @ ( identity @ divide ) )
!= a )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( a @ ( identity @ divide ) )
!= a ) ),
inference(rewrite,[status(thm)],[73,34]) ).
thf(69,plain,
! [A: $i] :
( ( ( identity @ ( A @ divide ) )
!= ( b @ ( identity @ divide ) ) )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( zero @ divide ) ) ) ),
inference(paramod_ordered,[status(thm)],[45,21]) ).
thf(71,plain,
! [A: $i] :
( ( b != identity )
| ( A != identity )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( zero @ divide ) ) ) ),
inference(simp,[status(thm)],[69]) ).
thf(90,plain,
( ( b != identity )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( zero @ divide ) ) ) ),
inference(simp,[status(thm)],[71]) ).
thf(7155,plain,
( ( b != identity )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= zero ) ),
inference(rewrite,[status(thm)],[90,50]) ).
thf(371,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( b @ ( identity @ divide ) ) )
| ( ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( A @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(paramod_ordered,[status(thm)],[52,21]) ).
thf(417,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( b @ ( identity @ divide ) ) )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( A @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) ) ) ),
inference(simp,[status(thm)],[371]) ).
thf(38560,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) )
!= ( b @ ( identity @ divide ) ) )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( A @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) ) ) ),
inference(rewrite,[status(thm)],[417,52]) ).
thf(2,axiom,
! [A: $i] : ( A @ ( zero @ less_equal ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',zero_is_smallest) ).
thf(22,plain,
! [A: $i] : ( A @ ( zero @ less_equal ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(269,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( D @ ( C @ less_equal ) ) )
| ( D @ ( B @ less_equal ) )
| ~ $true
| ~ ( C @ ( B @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[22,24]) ).
thf(270,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( D @ ( C @ less_equal ) ) )
| ( D @ ( B @ less_equal ) )
| ~ ( C @ ( B @ less_equal ) ) ),
inference(simp,[status(thm)],[269]) ).
thf(271,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ less_equal ) )
| ~ ( zero @ ( B @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[270:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( zero )),bind(D,$thf( A ))]]) ).
thf(25753,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ divide ) @ ( A @ divide ) @ less_equal ) )
!= ( zero @ ( D @ less_equal ) ) )
| ( C @ ( D @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1300,271]) ).
thf(25754,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ divide ) @ ( A @ divide ) @ less_equal ) )
!= ( zero @ ( D @ less_equal ) ) )
| ( C @ ( D @ less_equal ) ) ),
inference(simp,[status(thm)],[25753]) ).
thf(25755,plain,
! [B: $i,A: $i] : ( A @ ( zero @ ( B @ divide ) @ ( B @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[25754:[bind(A,$thf( G )),bind(B,$thf( zero )),bind(C,$thf( C )),bind(D,$thf( zero @ ( G @ divide ) @ ( G @ divide ) ))]]) ).
thf(25818,plain,
! [B: $i,A: $i] : ( A @ ( zero @ ( B @ divide ) @ ( B @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[25755]) ).
thf(260,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ less_equal ) )
!= ( E @ ( D @ less_equal ) ) )
| ( F @ ( D @ less_equal ) )
| ~ ( F @ ( E @ less_equal ) )
| ~ $true
| ~ ( C @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[24,24]) ).
thf(261,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ less_equal ) )
!= ( E @ ( D @ less_equal ) ) )
| ( F @ ( D @ less_equal ) )
| ~ ( F @ ( E @ less_equal ) )
| ~ ( C @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(simp,[status(thm)],[260]) ).
thf(262,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( A @ less_equal ) )
| ~ ( D @ ( C @ less_equal ) )
| ~ ( C @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[261:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( C ))]]) ).
thf(281,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( A @ less_equal ) )
| ~ ( D @ ( C @ less_equal ) )
| ~ ( C @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(simp,[status(thm)],[262]) ).
thf(383,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( b @ ( identity @ divide ) ) )
| ( ( A @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) ) ) ),
inference(paramod_ordered,[status(thm)],[52,168]) ).
thf(422,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) )
!= b )
| ( identity != identity )
| ( ( A @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) ) ) ),
inference(simp,[status(thm)],[383]) ).
thf(445,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) )
!= b )
| ( ( A @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) ) ) ),
inference(simp,[status(thm)],[422]) ).
thf(16558,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ divide ) @ divide ) )
!= ( D @ ( C @ divide ) ) )
| ( D @ ( C @ less_equal ) )
| ( zero != zero ) ),
inference(paramod_ordered,[status(thm)],[2534,32]) ).
thf(16559,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ divide ) @ divide ) )
!= ( D @ ( C @ divide ) ) )
| ( D @ ( C @ less_equal ) ) ),
inference(simp,[status(thm)],[16558]) ).
thf(16560,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[16559:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( F @ ( F @ divide ) )),bind(D,$thf( A ))]]) ).
thf(16900,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[16560]) ).
thf(1207,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ~ $true
| ~ ( a @ ( b @ less_equal ) )
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[32,658]) ).
thf(1208,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ~ ( a @ ( b @ less_equal ) )
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[1207]) ).
thf(1209,plain,
( ~ ( a @ ( b @ less_equal ) )
| ( ( b @ ( a @ divide ) )
!= zero ) ),
inference(pattern_uni,[status(thm)],[1208:[bind(A,$thf( a )),bind(B,$thf( b ))]]) ).
thf(18248,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6708,29]) ).
thf(18249,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[18248]) ).
thf(18250,plain,
! [A: $i] : ( zero @ ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[18249:[bind(A,$thf( G )),bind(B,$thf( zero @ ( zero @ ( G @ divide ) @ divide ) )),bind(C,$thf( zero )),bind(D,$thf( G ))]]) ).
thf(18457,plain,
! [A: $i] : ( zero @ ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[18250]) ).
thf(45173,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,45100]) ).
thf(45174,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[45173]) ).
thf(45224,plain,
! [B: $i,A: $i] :
( ( A != a )
| ( ( B @ ( A @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[45174]) ).
thf(45253,plain,
! [A: $i] :
( ( A @ ( a @ divide ) )
!= identity ),
inference(simp,[status(thm)],[45224]) ).
thf(25759,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( zero @ ( C @ less_equal ) ) )
| ( B @ ( C @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5628,271]) ).
thf(25760,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( zero @ ( C @ less_equal ) ) )
| ( B @ ( C @ less_equal ) ) ),
inference(simp,[status(thm)],[25759]) ).
thf(25761,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( zero @ ( B @ divide ) @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[25760:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ ( zero @ ( E @ divide ) @ divide ) ))]]) ).
thf(25822,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( zero @ ( B @ divide ) @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[25761]) ).
thf(8733,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( zero @ ( A @ ( A @ divide ) @ divide ) @ divide ) )
!= ( C @ ( B @ divide ) ) )
| ( C @ ( zero @ ( B @ divide ) @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[6069,1300]) ).
thf(8734,plain,
! [A: $i] : ( zero @ ( zero @ ( zero @ ( A @ ( A @ divide ) @ divide ) @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[8733:[bind(A,$thf( G )),bind(B,$thf( zero @ ( G @ ( G @ divide ) @ divide ) )),bind(C,$thf( zero ))]]) ).
thf(8926,plain,
! [A: $i] : ( zero @ ( zero @ ( zero @ ( A @ ( A @ divide ) @ divide ) @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[8734]) ).
thf(1129,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ~ $true
| ~ ( a @ ( b @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[35,658]) ).
thf(1130,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ~ ( a @ ( b @ less_equal ) ) ),
inference(simp,[status(thm)],[1129]) ).
thf(1143,plain,
! [B: $i,A: $i] :
( ( A != b )
| ( ( B @ ( A @ divide ) )
!= a )
| ~ ( a @ ( b @ less_equal ) ) ),
inference(simp,[status(thm)],[1130]) ).
thf(1162,plain,
! [A: $i] :
( ( ( A @ ( b @ divide ) )
!= a )
| ~ ( a @ ( b @ less_equal ) ) ),
inference(simp,[status(thm)],[1143]) ).
thf(2266,plain,
! [A: $i] :
( ( ( A @ ( zero @ ( A @ divide ) @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ~ $true
| ~ ( a @ ( b @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[1389,658]) ).
thf(2267,plain,
! [A: $i] :
( ( ( A @ ( zero @ ( A @ divide ) @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ~ ( a @ ( b @ less_equal ) ) ),
inference(simp,[status(thm)],[2266]) ).
thf(2280,plain,
! [A: $i] :
( ( A != b )
| ( ( zero @ ( A @ divide ) )
!= a )
| ~ ( a @ ( b @ less_equal ) ) ),
inference(simp,[status(thm)],[2267]) ).
thf(2289,plain,
( ( ( zero @ ( b @ divide ) )
!= a )
| ~ ( a @ ( b @ less_equal ) ) ),
inference(simp,[status(thm)],[2280]) ).
thf(11218,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( zero @ ( identity @ divide ) @ ( A @ divide ) @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ~ $true
| ( ( C @ ( B @ divide ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[11130,48]) ).
thf(11219,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( zero @ ( identity @ divide ) @ ( A @ divide ) @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ( ( C @ ( B @ divide ) )
= zero ) ),
inference(simp,[status(thm)],[11218]) ).
thf(11220,plain,
! [A: $i] :
( ( zero @ ( zero @ ( identity @ divide ) @ ( A @ divide ) @ divide ) )
= zero ),
inference(pattern_uni,[status(thm)],[11219:[bind(A,$thf( D )),bind(B,$thf( zero @ ( identity @ divide ) @ ( D @ divide ) )),bind(C,$thf( zero ))]]) ).
thf(11307,plain,
! [A: $i] :
( ( zero @ ( zero @ ( identity @ divide ) @ ( A @ divide ) @ divide ) )
= zero ),
inference(simp,[status(thm)],[11220]) ).
thf(12711,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( zero @ ( identity @ divide ) @ ( A @ divide ) @ divide ) )
!= ( C @ ( D @ ( B @ divide ) @ divide ) ) )
| ( zero @ ( C @ ( D @ divide ) @ ( C @ ( B @ divide ) @ divide ) @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[11307,42]) ).
thf(12712,plain,
! [A: $i] : ( zero @ ( zero @ ( zero @ ( identity @ divide ) @ divide ) @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[12711:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( zero )),bind(D,$thf( zero @ ( identity @ divide ) ))]]) ).
thf(1703,plain,
! [A: $i] :
( ( ( zero @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( A @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( zero @ ( A @ ( identity @ divide ) @ divide ) )
= ( A @ ( identity @ divide ) ) ) ),
inference(paramod_ordered,[status(thm)],[759,41]) ).
thf(1704,plain,
( ( zero @ ( zero @ ( identity @ divide ) @ divide ) )
= ( zero @ ( identity @ divide ) ) ),
inference(pattern_uni,[status(thm)],[1703:[bind(A,$thf( zero ))]]) ).
thf(15982,plain,
! [A: $i] : ( zero @ ( zero @ ( identity @ divide ) @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) ),
inference(rewrite,[status(thm)],[12712,1704]) ).
thf(25762,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( zero @ ( identity @ divide ) @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( zero @ ( C @ less_equal ) ) )
| ( B @ ( C @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15982,271]) ).
thf(25763,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( zero @ ( identity @ divide ) @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( zero @ ( C @ less_equal ) ) )
| ( B @ ( C @ less_equal ) ) ),
inference(simp,[status(thm)],[25762]) ).
thf(25764,plain,
! [B: $i,A: $i] : ( A @ ( zero @ ( identity @ divide ) @ ( zero @ ( B @ divide ) @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[25763:[bind(A,$thf( F )),bind(B,$thf( B )),bind(C,$thf( zero @ ( identity @ divide ) @ ( zero @ ( F @ divide ) @ divide ) ))]]) ).
thf(25823,plain,
! [B: $i,A: $i] : ( A @ ( zero @ ( identity @ divide ) @ ( zero @ ( B @ divide ) @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[25764]) ).
thf(32063,plain,
! [A: $i] : ( A @ ( zero @ less_equal ) ),
inference(rewrite,[status(thm)],[25823,26388]) ).
thf(45197,plain,
! [A: $i] :
( ( ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3323,45100]) ).
thf(45198,plain,
! [A: $i] :
( ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[45197]) ).
thf(45208,plain,
! [A: $i] :
( ( A != a )
| ( ( zero @ ( zero @ ( A @ divide ) @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[45198]) ).
thf(45240,plain,
( ( zero @ ( zero @ ( a @ divide ) @ divide ) )
!= identity ),
inference(simp,[status(thm)],[45208]) ).
thf(46519,plain,
( ( zero @ ( a @ divide ) )
!= identity ),
inference(rewrite,[status(thm)],[45240,34]) ).
thf(504,plain,
! [B: $i,A: $i] :
( ( B
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( A @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[27,21]) ).
thf(505,plain,
! [A: $i] :
( ( ( A @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( a @ ( identity @ divide ) @ ( identity @ divide ) @ less_equal ) )
| ~ ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( A @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[504:[bind(A,$thf( A )),bind(B,$thf( a @ ( identity @ divide ) @ ( identity @ divide ) ))]]) ).
thf(423,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) )
!= b )
| ( identity != identity )
| ( A != a )
| ( identity != identity ) ),
inference(simp,[status(thm)],[383]) ).
thf(446,plain,
( ( a @ ( identity @ divide ) @ ( identity @ divide ) )
!= b ),
inference(simp,[status(thm)],[423]) ).
thf(2505,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( zero != b )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[48,446]) ).
thf(2506,plain,
( ( zero != b )
| ~ ( a @ ( identity @ divide ) @ ( identity @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[2505:[bind(A,$thf( identity )),bind(B,$thf( a @ ( identity @ divide ) ))]]) ).
thf(392,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( A @ divide ) )
!= ( B @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( B @ ( identity @ divide ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[45,52]) ).
thf(396,plain,
! [B: $i,A: $i] :
( ( ( B @ ( identity @ divide ) @ ( identity @ divide ) )
!= identity )
| ( A != identity )
| ( ( B @ ( identity @ divide ) )
= zero ) ),
inference(simp,[status(thm)],[392]) ).
thf(426,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) )
!= identity )
| ( ( A @ ( identity @ divide ) )
= zero ) ),
inference(simp,[status(thm)],[396]) ).
thf(17110,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ divide ) @ less_equal ) )
!= ( E @ ( D @ ( C @ divide ) @ less_equal ) ) )
| ( D @ ( E @ ( C @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[16900,29]) ).
thf(17111,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ divide ) @ less_equal ) )
!= ( E @ ( D @ ( C @ divide ) @ less_equal ) ) )
| ( D @ ( E @ ( C @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[17110]) ).
thf(17112,plain,
! [B: $i,A: $i] : ( B @ ( A @ ( B @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[17111:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( B )),bind(E,$thf( A ))]]) ).
thf(68,plain,
! [A: $i] :
( ( ( identity @ ( A @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( zero @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(paramod_ordered,[status(thm)],[45,21]) ).
thf(87,plain,
! [A: $i] :
( ( ( a @ ( identity @ divide ) )
!= identity )
| ( A != identity )
| ( ( zero @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(simp,[status(thm)],[68]) ).
thf(95,plain,
( ( ( a @ ( identity @ divide ) )
!= identity )
| ( ( zero @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(simp,[status(thm)],[87]) ).
thf(2010,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( a @ ( b @ less_equal ) ) )
| ( b != identity )
| ~ $true
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[32,1161]) ).
thf(2011,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( a @ ( b @ less_equal ) ) )
| ( b != identity )
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[2010]) ).
thf(2012,plain,
( ( b != identity )
| ( ( a @ ( b @ divide ) )
!= zero ) ),
inference(pattern_uni,[status(thm)],[2011:[bind(A,$thf( b )),bind(B,$thf( a ))]]) ).
thf(418,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) )
!= b )
| ( identity != identity )
| ( ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( A @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(simp,[status(thm)],[371]) ).
thf(441,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) )
!= b )
| ( ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( A @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(simp,[status(thm)],[418]) ).
thf(25787,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( a @ divide ) @ less_equal ) )
!= ( zero @ ( C @ less_equal ) ) )
| ( B @ ( C @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[20389,271]) ).
thf(25788,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( a @ divide ) @ less_equal ) )
!= ( zero @ ( C @ less_equal ) ) )
| ( B @ ( C @ less_equal ) ) ),
inference(simp,[status(thm)],[25787]) ).
thf(25789,plain,
! [A: $i] : ( A @ ( zero @ ( zero @ ( identity @ divide ) @ divide ) @ ( a @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[25788:[bind(A,$thf( zero )),bind(B,$thf( B )),bind(C,$thf( zero @ ( zero @ ( identity @ divide ) @ divide ) @ ( a @ divide ) ))]]) ).
thf(25832,plain,
! [A: $i] : ( A @ ( zero @ ( zero @ ( identity @ divide ) @ divide ) @ ( a @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[25789]) ).
thf(28525,plain,
! [A: $i] : ( A @ ( zero @ ( identity @ divide ) @ ( a @ divide ) @ less_equal ) ),
inference(rewrite,[status(thm)],[25832,1704]) ).
thf(32606,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( identity @ divide ) @ ( a @ divide ) @ less_equal ) )
!= ( B @ ( C @ less_equal ) ) )
| ( B @ ( D @ ( C @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[28525,340]) ).
thf(32607,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( identity @ divide ) @ ( a @ divide ) @ less_equal ) )
!= ( B @ ( C @ less_equal ) ) )
| ( B @ ( D @ ( C @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[32606]) ).
thf(32608,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( zero @ ( identity @ divide ) @ ( a @ divide ) @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[32607:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( zero @ ( identity @ divide ) @ ( a @ divide ) )),bind(D,$thf( D ))]]) ).
thf(32859,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( zero @ ( identity @ divide ) @ ( a @ divide ) @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[32608]) ).
thf(37920,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( zero @ divide ) @ less_equal ) ),
inference(rewrite,[status(thm)],[32859,26388]) ).
thf(706,plain,
! [A: $i] :
( ( ( A @ ( A @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( zero != b ) ),
inference(paramod_ordered,[status(thm)],[39,446]) ).
thf(736,plain,
! [A: $i] :
( ( A
!= ( a @ ( identity @ divide ) ) )
| ( A != identity )
| ( zero != b ) ),
inference(simp,[status(thm)],[706]) ).
thf(744,plain,
( ( ( a @ ( identity @ divide ) )
!= identity )
| ( zero != b ) ),
inference(simp,[status(thm)],[736]) ).
thf(1583,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ( zero != b )
| ~ $true
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[32,1160]) ).
thf(1584,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ( zero != b )
| ( ( B @ ( A @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[1583]) ).
thf(1585,plain,
( ( zero != b )
| ( ( b @ ( a @ divide ) )
!= zero ) ),
inference(pattern_uni,[status(thm)],[1584:[bind(A,$thf( a )),bind(B,$thf( b ))]]) ).
thf(570,plain,
! [B: $i,A: $i] :
( ( B != b )
| ( ( A @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) ) )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[27,168]) ).
thf(571,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) ) )
| ~ ( A @ ( b @ less_equal ) )
| ~ ( b @ ( A @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[570:[bind(A,$thf( A )),bind(B,$thf( b ))]]) ).
thf(3042,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ( D @ ( C @ divide ) @ ( D @ ( B @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43,54]) ).
thf(3043,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( C @ ( B @ less_equal ) ) )
| ( D @ ( C @ divide ) @ ( D @ ( B @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[3042]) ).
thf(3044,plain,
! [B: $i,A: $i] : ( B @ ( identity @ divide ) @ ( B @ ( A @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[3043:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( identity ))]]) ).
thf(3092,plain,
! [B: $i,A: $i] : ( B @ ( identity @ divide ) @ ( B @ ( A @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[3044]) ).
thf(28016,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( b @ ( identity @ less_equal ) ) )
| ( zero != b )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,26089]) ).
thf(28017,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( b @ ( identity @ less_equal ) ) )
| ( zero != b ) ),
inference(simp,[status(thm)],[28016]) ).
thf(28050,plain,
! [B: $i,A: $i] :
( ( A != b )
| ( ( B @ ( A @ divide ) )
!= identity )
| ( zero != b ) ),
inference(simp,[status(thm)],[28017]) ).
thf(28078,plain,
! [A: $i] :
( ( ( A @ ( b @ divide ) )
!= identity )
| ( zero != b ) ),
inference(simp,[status(thm)],[28050]) ).
thf(494,plain,
! [B: $i,A: $i] :
( ( B != b )
| ( ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( A @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[27,21]) ).
thf(495,plain,
! [A: $i] :
( ( ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( A @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( b @ less_equal ) )
| ~ ( b @ ( A @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[494:[bind(A,$thf( A )),bind(B,$thf( b ))]]) ).
thf(586,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ less_equal ) )
!= ( E @ ( D @ less_equal ) ) )
| ~ ( D @ ( E @ less_equal ) )
| ~ $true
| ( D = E )
| ~ ( C @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[24,27]) ).
thf(587,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ less_equal ) )
!= ( E @ ( D @ less_equal ) ) )
| ~ ( D @ ( E @ less_equal ) )
| ( D = E )
| ~ ( C @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(simp,[status(thm)],[586]) ).
thf(588,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ less_equal ) )
| ( A = C )
| ~ ( C @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[587:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( C ))]]) ).
thf(2139,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( identity @ ( A @ divide ) )
!= ( C @ ( D @ ( B @ divide ) @ divide ) ) )
| ( zero @ ( C @ ( D @ divide ) @ ( C @ ( B @ divide ) @ divide ) @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[45,42]) ).
thf(2140,plain,
! [B: $i,A: $i] : ( zero @ ( identity @ ( B @ divide ) @ ( identity @ ( A @ divide ) @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[2139:[bind(A,$thf( F @ ( E @ divide ) )),bind(B,$thf( E )),bind(C,$thf( identity )),bind(D,$thf( F ))]]) ).
thf(2214,plain,
! [B: $i,A: $i] : ( zero @ ( identity @ ( B @ divide ) @ ( identity @ ( A @ divide ) @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[2140]) ).
thf(17709,plain,
zero @ ( zero @ ( zero @ divide ) @ less_equal ),
inference(rewrite,[status(thm)],[2214,45]) ).
thf(17725,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( zero @ ( zero @ divide ) @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( A @ ( C @ divide ) @ ( B @ ( C @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[17709,37]) ).
thf(17726,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( zero @ ( zero @ divide ) @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( A @ ( C @ divide ) @ ( B @ ( C @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[17725]) ).
thf(17727,plain,
! [A: $i] : ( zero @ ( zero @ divide ) @ ( A @ divide ) @ ( zero @ ( A @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[17726:[bind(A,$thf( zero @ ( zero @ divide ) )),bind(B,$thf( zero )),bind(C,$thf( C ))]]) ).
thf(17868,plain,
! [A: $i] : ( zero @ ( zero @ divide ) @ ( A @ divide ) @ ( zero @ ( A @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[17727]) ).
thf(21093,plain,
! [A: $i] : ( zero @ ( A @ divide ) @ ( zero @ ( A @ divide ) @ less_equal ) ),
inference(rewrite,[status(thm)],[17868,7618]) ).
thf(21152,plain,
! [A: $i] :
( ( ( zero @ ( a @ divide ) )
!= ( zero @ ( A @ divide ) ) )
| ( zero @ ( A @ divide ) @ ( a @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[34,21093]) ).
thf(21153,plain,
zero @ ( a @ divide ) @ ( a @ less_equal ),
inference(pattern_uni,[status(thm)],[21152:[bind(A,$thf( a ))]]) ).
thf(21327,plain,
a @ ( a @ less_equal ),
inference(rewrite,[status(thm)],[21153,34]) ).
thf(369,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) ) )
| ( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(paramod_ordered,[status(thm)],[52,21]) ).
thf(408,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) )
!= a )
| ( identity != identity )
| ( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(simp,[status(thm)],[369]) ).
thf(433,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) )
!= a )
| ( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(simp,[status(thm)],[408]) ).
thf(26149,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ~ $true
| ~ ( a @ ( b @ less_equal ) )
| ~ ( B @ ( identity @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[280,658]) ).
thf(26150,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ~ ( a @ ( b @ less_equal ) )
| ~ ( B @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[26149]) ).
thf(26151,plain,
( ~ ( a @ ( b @ less_equal ) )
| ~ ( b @ ( identity @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[26150:[bind(A,$thf( a )),bind(B,$thf( b ))]]) ).
thf(9584,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( zero @ ( A @ divide ) @ divide ) @ divide ) )
!= ( C @ ( B @ divide ) ) )
| ( C @ ( zero @ ( B @ divide ) @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[6231,1300]) ).
thf(9585,plain,
! [A: $i] : ( zero @ ( zero @ ( A @ ( zero @ ( A @ divide ) @ divide ) @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[9584:[bind(A,$thf( E )),bind(B,$thf( E @ ( zero @ ( E @ divide ) @ divide ) )),bind(C,$thf( zero ))]]) ).
thf(9839,plain,
! [A: $i] : ( zero @ ( zero @ ( A @ ( zero @ ( A @ divide ) @ divide ) @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[9585]) ).
thf(1594,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ( zero != b )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43,1160]) ).
thf(1595,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( b @ ( a @ less_equal ) ) )
| ( zero != b ) ),
inference(simp,[status(thm)],[1594]) ).
thf(1598,plain,
! [A: $i] :
( ( b != identity )
| ( A != a )
| ( zero != b ) ),
inference(simp,[status(thm)],[1595]) ).
thf(1614,plain,
( ( b != identity )
| ( zero != b ) ),
inference(simp,[status(thm)],[1598]) ).
thf(23128,plain,
! [A: $i] :
( ( ( zero @ ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) @ less_equal ) )
!= ( zero @ ( identity @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[18457,3653]) ).
thf(23129,plain,
! [A: $i] :
( ( zero @ ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) @ less_equal ) )
!= ( zero @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[23128]) ).
thf(23353,plain,
! [A: $i] :
( ( zero != zero )
| ( ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[23129]) ).
thf(23388,plain,
! [A: $i] :
( ( A @ ( zero @ ( zero @ ( A @ divide ) @ divide ) @ divide ) )
!= identity ),
inference(simp,[status(thm)],[23353]) ).
thf(405,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( b @ ( identity @ divide ) )
!= identity )
| ( ( A @ ( identity @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) ) ),
inference(simp,[status(thm)],[368]) ).
thf(2978,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( identity @ divide ) @ ( identity @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( C @ ( B @ divide ) @ ( C @ ( A @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1192,54]) ).
thf(2979,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( identity @ divide ) @ ( identity @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( C @ ( B @ divide ) @ ( C @ ( A @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[2978]) ).
thf(2980,plain,
! [A: $i] : ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( A @ ( identity @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[2979:[bind(A,$thf( identity )),bind(B,$thf( zero @ ( identity @ divide ) )),bind(C,$thf( C ))]]) ).
thf(3072,plain,
! [A: $i] : ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( A @ ( identity @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[2980]) ).
thf(17913,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( A @ ( identity @ divide ) @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3072,29]) ).
thf(17914,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( A @ ( identity @ divide ) @ less_equal ) )
!= ( D @ ( C @ ( B @ divide ) @ less_equal ) ) )
| ( C @ ( D @ ( B @ divide ) @ less_equal ) ) ),
inference(simp,[status(thm)],[17913]) ).
thf(17915,plain,
! [A: $i] : ( A @ ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( identity @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[17914:[bind(A,$thf( F )),bind(B,$thf( identity )),bind(C,$thf( F )),bind(D,$thf( F @ ( zero @ ( identity @ divide ) @ divide ) ))]]) ).
thf(18189,plain,
! [A: $i] : ( A @ ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( identity @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[17915]) ).
thf(45169,plain,
! [A: $i] :
( ( ( A @ ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( identity @ divide ) @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[18189,45100]) ).
thf(45170,plain,
! [A: $i] :
( ( A @ ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( identity @ divide ) @ less_equal ) )
!= ( a @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[45169]) ).
thf(45218,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ ( zero @ ( identity @ divide ) @ divide ) @ ( identity @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[45170]) ).
thf(45248,plain,
( ( a @ ( zero @ ( identity @ divide ) @ divide ) @ ( identity @ divide ) )
!= identity ),
inference(simp,[status(thm)],[45218]) ).
thf(65750,plain,
( ( a @ ( identity @ divide ) @ ( identity @ divide ) )
!= identity ),
inference(rewrite,[status(thm)],[45248,65110]) ).
thf(191,plain,
! [A: $i] :
( ( ( A @ ( zero @ divide ) )
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) ) )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[50,21]) ).
thf(216,plain,
! [A: $i] :
( ( A
!= ( a @ ( identity @ divide ) @ ( identity @ divide ) ) )
| ( ( b @ ( identity @ divide ) )
!= zero )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[191]) ).
thf(239,plain,
( ( ( b @ ( identity @ divide ) )
!= zero )
| ( ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) )
!= zero ) ),
inference(simp,[status(thm)],[216]) ).
thf(329,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( E @ ( D @ less_equal ) ) )
| ( E @ ( C @ less_equal ) )
| ~ $true
| ~ ( D @ ( C @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[35,24]) ).
thf(330,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( E @ ( D @ less_equal ) ) )
| ( E @ ( C @ less_equal ) )
| ~ ( D @ ( C @ less_equal ) ) ),
inference(simp,[status(thm)],[329]) ).
thf(331,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ less_equal ) )
| ~ ( C @ ( B @ divide ) @ ( A @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[330:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( C )),bind(D,$thf( G @ ( F @ divide ) )),bind(E,$thf( F ))]]) ).
thf(341,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ less_equal ) )
| ~ ( C @ ( B @ divide ) @ ( A @ less_equal ) ) ),
inference(simp,[status(thm)],[331]) ).
thf(500,plain,
! [B: $i,A: $i] :
( ( B != identity )
| ( ( a @ ( A @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[27,21]) ).
thf(501,plain,
! [A: $i] :
( ( ( a @ ( A @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( identity @ less_equal ) )
| ~ ( identity @ ( A @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[500:[bind(A,$thf( A )),bind(B,$thf( identity ))]]) ).
thf(58329,plain,
! [A: $i] :
( ( ( a @ ( A @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( identity @ less_equal ) )
| ~ $true ),
inference(rewrite,[status(thm)],[501,43]) ).
thf(58330,plain,
! [A: $i] :
( ( ( a @ ( A @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[58329]) ).
thf(490,plain,
! [B: $i,A: $i] :
( ( B != a )
| ( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[27,21]) ).
thf(491,plain,
! [A: $i] :
( ( ( A @ ( identity @ divide ) @ ( identity @ divide ) @ ( b @ ( identity @ divide ) @ divide ) )
!= ( b @ ( identity @ divide ) @ ( identity @ divide ) @ ( a @ ( identity @ divide ) @ divide ) ) )
| ~ ( A @ ( a @ less_equal ) )
| ~ ( a @ ( A @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[490:[bind(A,$thf( A )),bind(B,$thf( a ))]]) ).
thf(124838,plain,
$false,
inference(e,[status(thm)],[2282,1168,6231,41068,27986,26089,340,16915,28074,45265,3634,42,24,45255,37,25,52,2039,3653,66987,47471,5640,6240,5052,316,29,46,1609,45145,65748,32484,280,89,428,26080,265,507,35538,1206,942,9031,21,33,32899,56340,28,38,916,435,6708,53,67211,1160,3714,2613,1612,2317,1539,2243,2355,45259,44562,41,503,54947,11539,45263,4195,45,32,7155,34,38560,44,25818,281,27,22,1389,445,54,49,9835,16900,1209,18457,45253,25822,3710,39,271,8926,552,1162,40918,2289,32063,46519,10240,505,35,658,2506,426,17112,95,2012,7618,48,6069,50,1300,1186,441,15598,65110,37920,744,5628,1585,43,446,571,3092,28078,45100,495,588,21327,40,258,2526,23,433,26151,9839,1161,1614,2534,36,168,30,51,23388,2522,405,19,65750,239,341,3323,58330,491]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HEN011-4 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.13/0.38 % Computer : n005.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Fri Sep 25 15:57:47 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.08/1.05 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.36/1.25 % [INFO] Parsing done (202ms).
% 1.36/1.27 % [INFO] Running in sequential loop mode.
% 2.03/1.67 % [INFO] eprover registered as external prover.
% 2.03/1.68 % [INFO] Scanning for conjecture ...
% 2.26/1.77 % [INFO] Found a conjecture (or negated_conjecture) and 17 axioms. Running axiom selection ...
% 2.44/1.83 % [INFO] Axiom selection finished. Selected 17 axioms (removed 0 axioms).
% 2.44/1.86 % [INFO] Problem is propositional (TPTP CNF).
% 2.44/1.86 % [INFO] Type checking passed.
% 2.44/1.87 % [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 ...
% 154.09/40.97 % External prover 'e' found a proof!
% 154.09/40.97 % [INFO] Killing All external provers ...
% 154.09/40.98 % Time passed: 40391ms (effective reasoning time: 39704ms)
% 154.09/40.98 % Axioms used in derivation (17): property_of_inversion, identity_is_largest, x_divide_x_is_zero, property_of_divide2, zero_divide_anything_is_zero, property_of_divide1, everything_divide_id_is_zero, quotient_less_equal2, less_equal_and_equal, zero_is_smallest, x_divide_zero_is_x, quotient_less_equal1, transitivity_of_less_equal, quotient_smaller_than_numerator, quotient_property, one_inversion_equals_three, property_of_divide3
% 154.09/40.98 % No. of inferences in proof: 553
% 154.09/40.98 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : 40391 ms resp. 39704 ms w/o parsing
% 155.19/41.16 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 155.19/41.17 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------