%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : HEN006-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:31:37 AM UTC 2026
% Result : Unsatisfiable 99.90s 26.01s
% Output : Refutation 101.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 18
% Syntax : Number of formulae : 677 ( 72 unt; 0 typ; 0 def)
% Number of atoms : 2660 ( 896 equ; 0 cnn)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 7759 (1808 ~;1493 |; 0 &;4458 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 8 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 13 ( 10 usr; 9 con; 0-3 aty)
% Number of variables : 1488 ( 0 ^;1488 !; 0 ?;1488 :)
% Comments :
%------------------------------------------------------------------------------
thf(less_equal_decl,type,
less_equal: $i > $i > $o ).
thf(xQz_decl,type,
xQz: $i ).
thf(y_decl,type,
y: $i ).
thf(quotient_decl,type,
quotient: $i > $i > $i > $o ).
thf(zero_decl,type,
zero: $i ).
thf(divide_decl,type,
divide: $i > $i > $i ).
thf(identity_decl,type,
identity: $i ).
thf(x_decl,type,
x: $i ).
thf(z_decl,type,
z: $i ).
thf(xQy_decl,type,
xQy: $i ).
thf(12,axiom,
xQz @ ( z @ ( x @ quotient ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',xQz) ).
thf(36,plain,
xQz @ ( z @ ( x @ quotient ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(5,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C = D )
| ~ ( D @ ( B @ ( A @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_defined) ).
thf(24,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C = D )
| ~ ( D @ ( B @ ( A @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(25,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C = D )
| ~ ( D @ ( B @ ( A @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(cnf,[status(esa)],[24]) ).
thf(26,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( B @ ( A @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) )
| ( C = D ) ),
inference(lifteq,[status(thm)],[25]) ).
thf(16,axiom,
! [A: $i] : ( identity @ ( A @ less_equal ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_is_largest) ).
thf(42,plain,
! [A: $i] : ( identity @ ( A @ less_equal ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(1,negated_conjecture,
~ ( y @ ( xQz @ less_equal ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_xQzLEy) ).
thf(19,plain,
~ ( y @ ( xQz @ less_equal ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(20,plain,
~ ( y @ ( xQz @ less_equal ) ),
inference(polarity_switch,[status(thm)],[19]) ).
thf(126,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( y @ ( xQz @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,20]) ).
thf(127,plain,
! [A: $i] :
( ( identity @ ( A @ less_equal ) )
!= ( y @ ( xQz @ less_equal ) ) ),
inference(simp,[status(thm)],[126]) ).
thf(128,plain,
! [A: $i] :
( ( identity != y )
| ( A != xQz ) ),
inference(simp,[status(thm)],[127]) ).
thf(129,plain,
identity != y,
inference(simp,[status(thm)],[128]) ).
thf(553,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C != identity )
| ( D != y )
| ~ ( D @ ( B @ ( A @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[26,129]) ).
thf(554,plain,
! [C: $i,B: $i,A: $i] :
( ( C != y )
| ~ ( C @ ( B @ ( A @ quotient ) ) )
| ~ ( identity @ ( B @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[553:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( identity ))]]) ).
thf(656,plain,
! [B: $i,A: $i] :
( ~ ( y @ ( B @ ( A @ quotient ) ) )
| ~ ( identity @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[554]) ).
thf(782,plain,
! [B: $i,A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( identity @ ( B @ ( A @ quotient ) ) ) )
| ~ ( y @ ( B @ ( A @ quotient ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[36,656]) ).
thf(783,plain,
! [B: $i,A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( identity @ ( B @ ( A @ quotient ) ) ) )
| ~ ( y @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[782]) ).
thf(790,plain,
! [B: $i,A: $i] :
( ( identity != xQz )
| ( z != B )
| ( x != A )
| ~ ( y @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[783]) ).
thf(809,plain,
( ( identity != xQz )
| ~ ( y @ ( z @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[790]) ).
thf(15,axiom,
xQy @ ( y @ ( x @ quotient ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',xQy) ).
thf(41,plain,
xQy @ ( y @ ( x @ quotient ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(14,axiom,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ less_equal ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',divisor_existence) ).
thf(39,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ less_equal ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(40,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ less_equal ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(cnf,[status(esa)],[39]) ).
thf(1527,plain,
! [C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( C @ ( B @ ( A @ quotient ) ) ) )
| ( A @ ( C @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,40]) ).
thf(1528,plain,
! [C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( C @ ( B @ ( A @ quotient ) ) ) )
| ( A @ ( C @ less_equal ) ) ),
inference(simp,[status(thm)],[1527]) ).
thf(1529,plain,
x @ ( xQy @ less_equal ),
inference(pattern_uni,[status(thm)],[1528:[bind(A,$thf( x )),bind(B,$thf( y )),bind(C,$thf( xQy ))]]) ).
thf(18,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(44,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(45,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(cnf,[status(esa)],[44]) ).
thf(46,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[45]) ).
thf(1883,plain,
! [B: $i,A: $i] :
( ( ( x @ ( xQy @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ~ ( A @ ( B @ less_equal ) )
| ~ $true
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[1529,46]) ).
thf(1884,plain,
! [B: $i,A: $i] :
( ( ( x @ ( xQy @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ~ ( A @ ( B @ less_equal ) )
| ( A = B ) ),
inference(simp,[status(thm)],[1883]) ).
thf(1885,plain,
( ~ ( xQy @ ( x @ less_equal ) )
| ( xQy = x ) ),
inference(pattern_uni,[status(thm)],[1884:[bind(A,$thf( xQy )),bind(B,$thf( x ))]]) ).
thf(17,axiom,
z @ ( xQy @ less_equal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',xQyLEz) ).
thf(43,plain,
z @ ( xQy @ less_equal ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(4570,plain,
( ( xQy != xQy )
| ( z @ ( x @ less_equal ) )
| ~ ( xQy @ ( x @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[1885,43]) ).
thf(4571,plain,
( ( z @ ( x @ less_equal ) )
| ~ ( xQy @ ( x @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[4570:[]]) ).
thf(18243,plain,
( ( ( x @ ( xQy @ less_equal ) )
!= ( xQy @ ( x @ less_equal ) ) )
| ( z @ ( x @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1529,4571]) ).
thf(18244,plain,
( ( ( x @ ( xQy @ less_equal ) )
!= ( xQy @ ( x @ less_equal ) ) )
| ( z @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[18243]) ).
thf(18345,plain,
( ( xQy != x )
| ( xQy != x )
| ( z @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[18244]) ).
thf(18360,plain,
( ( xQy != x )
| ( z @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[18345]) ).
thf(3,axiom,
! [B: $i,A: $i] : ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closure) ).
thf(22,plain,
! [B: $i,A: $i] : ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(1530,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( E @ ( D @ ( C @ quotient ) ) ) )
| ( C @ ( E @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,40]) ).
thf(1531,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( E @ ( D @ ( C @ quotient ) ) ) )
| ( C @ ( E @ less_equal ) ) ),
inference(simp,[status(thm)],[1530]) ).
thf(1532,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ divide ) @ less_equal ) ),
inference(pattern_uni,[status(thm)],[1531:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( F )),bind(D,$thf( G )),bind(E,$thf( G @ ( F @ divide ) ))]]) ).
thf(1548,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ divide ) @ less_equal ) ),
inference(simp,[status(thm)],[1532]) ).
thf(2378,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( y @ ( xQz @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1548,20]) ).
thf(2379,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( y @ ( xQz @ less_equal ) ) ),
inference(simp,[status(thm)],[2378]) ).
thf(2407,plain,
! [B: $i,A: $i] :
( ( A != y )
| ( ( B @ ( A @ divide ) )
!= xQz ) ),
inference(simp,[status(thm)],[2379]) ).
thf(2412,plain,
! [A: $i] :
( ( A @ ( y @ divide ) )
!= xQz ),
inference(simp,[status(thm)],[2407]) ).
thf(9,axiom,
! [A: $i] : ( A @ ( zero @ less_equal ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',zero_is_smallest) ).
thf(31,plain,
! [A: $i] : ( A @ ( zero @ less_equal ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(2111,plain,
! [B: $i,A: $i] :
( ( ( z @ ( xQy @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ~ ( A @ ( B @ less_equal ) )
| ~ $true
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[43,46]) ).
thf(2112,plain,
! [B: $i,A: $i] :
( ( ( z @ ( xQy @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ~ ( A @ ( B @ less_equal ) )
| ( A = B ) ),
inference(simp,[status(thm)],[2111]) ).
thf(2113,plain,
( ~ ( xQy @ ( z @ less_equal ) )
| ( xQy = z ) ),
inference(pattern_uni,[status(thm)],[2112:[bind(A,$thf( xQy )),bind(B,$thf( z ))]]) ).
thf(5348,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( xQy @ ( z @ less_equal ) ) )
| ~ $true
| ( xQy = z ) ),
inference(paramod_ordered,[status(thm)],[31,2113]) ).
thf(5349,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( xQy @ ( z @ less_equal ) ) )
| ( xQy = z ) ),
inference(simp,[status(thm)],[5348]) ).
thf(5382,plain,
! [A: $i] :
( ( A != xQy )
| ( z != zero )
| ( xQy = z ) ),
inference(simp,[status(thm)],[5349]) ).
thf(5391,plain,
( ( z != zero )
| ( xQy = z ) ),
inference(simp,[status(thm)],[5382]) ).
thf(5653,plain,
( ( xQy != xQy )
| ( x @ ( z @ less_equal ) )
| ( z != zero ) ),
inference(paramod_ordered,[status(thm)],[5391,1529]) ).
thf(5654,plain,
( ( x @ ( z @ less_equal ) )
| ( z != zero ) ),
inference(pattern_uni,[status(thm)],[5653:[]]) ).
thf(5278,plain,
( ( xQy != xQy )
| ( x @ ( z @ less_equal ) )
| ~ ( xQy @ ( z @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[2113,1529]) ).
thf(5279,plain,
( ( x @ ( z @ less_equal ) )
| ~ ( xQy @ ( z @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[5278:[]]) ).
thf(20442,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( xQy @ ( z @ less_equal ) ) )
| ( x @ ( z @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,5279]) ).
thf(20443,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( xQy @ ( z @ less_equal ) ) )
| ( x @ ( z @ less_equal ) ) ),
inference(simp,[status(thm)],[20442]) ).
thf(20550,plain,
! [A: $i] :
( ( xQy != identity )
| ( A != z )
| ( x @ ( z @ less_equal ) ) ),
inference(simp,[status(thm)],[20443]) ).
thf(20563,plain,
( ( xQy != identity )
| ( x @ ( z @ less_equal ) ) ),
inference(simp,[status(thm)],[20550]) ).
thf(11,axiom,
! [B: $i,A: $i] :
( ( zero @ ( B @ ( A @ quotient ) ) )
| ~ ( B @ ( A @ less_equal ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_less_equal) ).
thf(34,plain,
! [B: $i,A: $i] :
( ( zero @ ( B @ ( A @ quotient ) ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(35,plain,
! [B: $i,A: $i] :
( ( zero @ ( B @ ( A @ quotient ) ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(cnf,[status(esa)],[34]) ).
thf(20638,plain,
! [B: $i,A: $i] :
( ( ( x @ ( z @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ~ $true
| ( xQy != identity ) ),
inference(paramod_ordered,[status(thm)],[20563,35]) ).
thf(20639,plain,
! [B: $i,A: $i] :
( ( ( x @ ( z @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ( xQy != identity ) ),
inference(simp,[status(thm)],[20638]) ).
thf(20640,plain,
( ( zero @ ( x @ ( z @ quotient ) ) )
| ( xQy != identity ) ),
inference(pattern_uni,[status(thm)],[20639:[bind(A,$thf( z )),bind(B,$thf( x ))]]) ).
thf(13,axiom,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_property) ).
thf(37,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(38,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(cnf,[status(esa)],[37]) ).
thf(55,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( E @ ( D @ ( B @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ $true
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[41,38]) ).
thf(56,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( E @ ( D @ ( B @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[55]) ).
thf(57,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( y @ ( B @ quotient ) ) )
| ~ ( D @ ( xQy @ ( C @ quotient ) ) )
| ~ ( C @ ( y @ ( A @ quotient ) ) )
| ~ ( B @ ( x @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[56:[bind(A,$thf( A )),bind(B,$thf( x )),bind(C,$thf( C )),bind(D,$thf( y )),bind(E,$thf( xQy ))]]) ).
thf(115,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( y @ ( B @ quotient ) ) )
| ~ ( D @ ( xQy @ ( C @ quotient ) ) )
| ~ ( C @ ( y @ ( A @ quotient ) ) )
| ~ ( B @ ( x @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[57]) ).
thf(4,axiom,
! [A: $i] : ( zero @ ( identity @ ( A @ quotient ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',everything_divide_identity_is_zero) ).
thf(23,plain,
! [A: $i] : ( zero @ ( identity @ ( A @ quotient ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(2,axiom,
! [A: $i] : ( A @ ( zero @ ( A @ quotient ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_divde_zero_is_x) ).
thf(21,plain,
! [A: $i] : ( A @ ( zero @ ( A @ quotient ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(751,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( y @ ( C @ ( B @ quotient ) ) ) )
| ~ $true
| ~ ( identity @ ( C @ ( B @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,656]) ).
thf(752,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( y @ ( C @ ( B @ quotient ) ) ) )
| ~ ( identity @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[751]) ).
thf(753,plain,
~ ( identity @ ( zero @ ( y @ quotient ) ) ),
inference(pattern_uni,[status(thm)],[752:[bind(A,$thf( y )),bind(B,$thf( y )),bind(C,$thf( zero ))]]) ).
thf(998,plain,
! [A: $i] :
( ( ( zero @ ( identity @ ( A @ quotient ) ) )
!= ( identity @ ( zero @ ( y @ quotient ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[23,753]) ).
thf(999,plain,
! [A: $i] :
( ( zero @ ( identity @ ( A @ quotient ) ) )
!= ( identity @ ( zero @ ( y @ quotient ) ) ) ),
inference(simp,[status(thm)],[998]) ).
thf(1007,plain,
! [A: $i] :
( ( identity != zero )
| ( identity != zero )
| ( A != y ) ),
inference(simp,[status(thm)],[999]) ).
thf(1012,plain,
identity != zero,
inference(simp,[status(thm)],[1007]) ).
thf(1991,plain,
! [B: $i,A: $i] :
( ( A != identity )
| ( B != zero )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[46,1012]) ).
thf(1992,plain,
! [A: $i] :
( ( A != zero )
| ~ ( identity @ ( A @ less_equal ) )
| ~ ( A @ ( identity @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[1991:[bind(A,$thf( identity ))]]) ).
thf(2232,plain,
( ~ ( identity @ ( zero @ less_equal ) )
| ~ ( zero @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[1992]) ).
thf(9780,plain,
( ~ $true
| ~ ( zero @ ( identity @ less_equal ) ) ),
inference(rewrite,[status(thm)],[2232,42]) ).
thf(9781,plain,
~ ( zero @ ( identity @ less_equal ) ),
inference(simp,[status(thm)],[9780]) ).
thf(9833,plain,
( ( ( z @ ( xQy @ less_equal ) )
!= ( zero @ ( identity @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43,9781]) ).
thf(9834,plain,
( ( z @ ( xQy @ less_equal ) )
!= ( zero @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[9833]) ).
thf(9853,plain,
( ( z != zero )
| ( xQy != identity ) ),
inference(simp,[status(thm)],[9834]) ).
thf(9916,plain,
( ( xQy != xQy )
| ( z != zero )
| ( z != identity )
| ( z != zero ) ),
inference(paramod_ordered,[status(thm)],[5391,9853]) ).
thf(9917,plain,
( ( xQy != xQy )
| ( z != identity )
| ( z != zero ) ),
inference(simp,[status(thm)],[9916]) ).
thf(9918,plain,
( ( z != identity )
| ( z != zero ) ),
inference(pattern_uni,[status(thm)],[9917:[]]) ).
thf(61,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( G @ ( E @ ( F @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ $true
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[41,38]) ).
thf(62,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( G @ ( E @ ( F @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[61]) ).
thf(63,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( xQy @ less_equal ) )
| ~ ( E @ ( D @ ( C @ quotient ) ) )
| ~ ( x @ ( D @ ( A @ quotient ) ) )
| ~ ( y @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[62:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( y )),bind(F,$thf( x )),bind(G,$thf( xQy ))]]) ).
thf(120,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( xQy @ less_equal ) )
| ~ ( E @ ( D @ ( C @ quotient ) ) )
| ~ ( x @ ( D @ ( A @ quotient ) ) )
| ~ ( y @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[63]) ).
thf(8,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ less_equal ) )
| ~ ( zero @ ( B @ ( A @ quotient ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_equal_quotient) ).
thf(29,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ less_equal ) )
| ~ ( zero @ ( B @ ( A @ quotient ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(30,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ less_equal ) )
| ~ ( zero @ ( B @ ( A @ quotient ) ) ) ),
inference(cnf,[status(esa)],[29]) ).
thf(449,plain,
! [B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( zero @ ( B @ ( A @ quotient ) ) ) )
| ( B @ ( A @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,30]) ).
thf(450,plain,
! [B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( zero @ ( B @ ( A @ quotient ) ) ) )
| ( B @ ( A @ less_equal ) ) ),
inference(simp,[status(thm)],[449]) ).
thf(460,plain,
! [B: $i,A: $i] :
( ( xQy != zero )
| ( y != B )
| ( x != A )
| ( B @ ( A @ less_equal ) ) ),
inference(simp,[status(thm)],[450]) ).
thf(463,plain,
( ( xQy != zero )
| ( y @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[460]) ).
thf(5692,plain,
( ( xQy != xQy )
| ( z != zero )
| ( y @ ( x @ less_equal ) )
| ( z != zero ) ),
inference(paramod_ordered,[status(thm)],[5391,463]) ).
thf(5693,plain,
( ( xQy != xQy )
| ( y @ ( x @ less_equal ) )
| ( z != zero ) ),
inference(simp,[status(thm)],[5692]) ).
thf(5694,plain,
( ( y @ ( x @ less_equal ) )
| ( z != zero ) ),
inference(pattern_uni,[status(thm)],[5693:[]]) ).
thf(1545,plain,
! [C: $i,B: $i,A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( C @ ( B @ ( A @ quotient ) ) ) )
| ( A @ ( C @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[36,40]) ).
thf(1546,plain,
! [C: $i,B: $i,A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( C @ ( B @ ( A @ quotient ) ) ) )
| ( A @ ( C @ less_equal ) ) ),
inference(simp,[status(thm)],[1545]) ).
thf(1547,plain,
x @ ( xQz @ less_equal ),
inference(pattern_uni,[status(thm)],[1546:[bind(A,$thf( x )),bind(B,$thf( z )),bind(C,$thf( xQz ))]]) ).
thf(1585,plain,
( ( ( x @ ( xQz @ less_equal ) )
!= ( y @ ( xQz @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1547,20]) ).
thf(1586,plain,
( ( x @ ( xQz @ less_equal ) )
!= ( y @ ( xQz @ less_equal ) ) ),
inference(simp,[status(thm)],[1585]) ).
thf(1606,plain,
( ( x != y )
| ( xQz != xQz ) ),
inference(simp,[status(thm)],[1586]) ).
thf(1608,plain,
x != y,
inference(simp,[status(thm)],[1606]) ).
thf(1771,plain,
! [B: $i,A: $i] :
( ( A != x )
| ( B != y )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[46,1608]) ).
thf(1772,plain,
! [A: $i] :
( ( A != y )
| ~ ( x @ ( A @ less_equal ) )
| ~ ( A @ ( x @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[1771:[bind(A,$thf( x ))]]) ).
thf(2247,plain,
( ~ ( x @ ( y @ less_equal ) )
| ~ ( y @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[1772]) ).
thf(13150,plain,
( ( ( y @ ( x @ less_equal ) )
!= ( y @ ( x @ less_equal ) ) )
| ~ ( x @ ( y @ less_equal ) )
| ~ $true
| ( z != zero ) ),
inference(paramod_ordered,[status(thm)],[5694,2247]) ).
thf(13151,plain,
( ( ( y @ ( x @ less_equal ) )
!= ( y @ ( x @ less_equal ) ) )
| ~ ( x @ ( y @ less_equal ) )
| ( z != zero ) ),
inference(simp,[status(thm)],[13150]) ).
thf(13152,plain,
( ~ ( x @ ( y @ less_equal ) )
| ( z != zero ) ),
inference(pattern_uni,[status(thm)],[13151:[]]) ).
thf(1995,plain,
! [B: $i,A: $i] :
( ( A != identity )
| ( B != y )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[46,129]) ).
thf(1996,plain,
! [A: $i] :
( ( A != y )
| ~ ( identity @ ( A @ less_equal ) )
| ~ ( A @ ( identity @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[1995:[bind(A,$thf( identity ))]]) ).
thf(2234,plain,
( ~ ( identity @ ( y @ less_equal ) )
| ~ ( y @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[1996]) ).
thf(10264,plain,
( ~ $true
| ~ ( y @ ( identity @ less_equal ) ) ),
inference(rewrite,[status(thm)],[2234,42]) ).
thf(10265,plain,
~ ( y @ ( identity @ less_equal ) ),
inference(simp,[status(thm)],[10264]) ).
thf(10307,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( y @ ( identity @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1548,10265]) ).
thf(10308,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( y @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[10307]) ).
thf(10341,plain,
! [B: $i,A: $i] :
( ( A != y )
| ( ( B @ ( A @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[10308]) ).
thf(10346,plain,
! [A: $i] :
( ( A @ ( y @ divide ) )
!= identity ),
inference(simp,[status(thm)],[10341]) ).
thf(122,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( y @ ( xQz @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[31,20]) ).
thf(123,plain,
! [A: $i] :
( ( A @ ( zero @ less_equal ) )
!= ( y @ ( xQz @ less_equal ) ) ),
inference(simp,[status(thm)],[122]) ).
thf(124,plain,
! [A: $i] :
( ( A != y )
| ( zero != xQz ) ),
inference(simp,[status(thm)],[123]) ).
thf(125,plain,
zero != xQz,
inference(simp,[status(thm)],[124]) ).
thf(1775,plain,
! [B: $i,A: $i] :
( ( A != zero )
| ( B != xQz )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[46,125]) ).
thf(1776,plain,
! [A: $i] :
( ( A != xQz )
| ~ ( zero @ ( A @ less_equal ) )
| ~ ( A @ ( zero @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[1775:[bind(A,$thf( zero ))]]) ).
thf(2251,plain,
( ~ ( zero @ ( xQz @ less_equal ) )
| ~ ( xQz @ ( zero @ less_equal ) ) ),
inference(simp,[status(thm)],[1776]) ).
thf(15849,plain,
( ~ ( zero @ ( xQz @ less_equal ) )
| ~ $true ),
inference(rewrite,[status(thm)],[2251,31]) ).
thf(15850,plain,
~ ( zero @ ( xQz @ less_equal ) ),
inference(simp,[status(thm)],[15849]) ).
thf(15902,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( zero @ ( xQz @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1548,15850]) ).
thf(15903,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( zero @ ( xQz @ less_equal ) ) ),
inference(simp,[status(thm)],[15902]) ).
thf(15939,plain,
! [B: $i,A: $i] :
( ( A != zero )
| ( ( B @ ( A @ divide ) )
!= xQz ) ),
inference(simp,[status(thm)],[15903]) ).
thf(15948,plain,
! [A: $i] :
( ( A @ ( zero @ divide ) )
!= xQz ),
inference(simp,[status(thm)],[15939]) ).
thf(6638,plain,
! [B: $i,A: $i] :
( ( ( y @ ( x @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ~ $true
| ( z != zero ) ),
inference(paramod_ordered,[status(thm)],[5694,35]) ).
thf(6639,plain,
! [B: $i,A: $i] :
( ( ( y @ ( x @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ( z != zero ) ),
inference(simp,[status(thm)],[6638]) ).
thf(6640,plain,
( ( zero @ ( y @ ( x @ quotient ) ) )
| ( z != zero ) ),
inference(pattern_uni,[status(thm)],[6639:[bind(A,$thf( x )),bind(B,$thf( y ))]]) ).
thf(6,axiom,
! [A: $i] : ( zero @ ( A @ ( zero @ quotient ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',zero_divide_anything_is_zero) ).
thf(27,plain,
! [A: $i] : ( zero @ ( A @ ( zero @ quotient ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(176,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( zero @ quotient ) ) )
!= ( G @ ( E @ ( B @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ $true
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[27,38]) ).
thf(177,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( zero @ quotient ) ) )
!= ( G @ ( E @ ( B @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[176]) ).
thf(178,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( A @ ( C @ quotient ) ) )
| ~ ( E @ ( D @ ( zero @ quotient ) ) )
| ~ ( D @ ( A @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( zero @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[177:[bind(A,$thf( A )),bind(B,$thf( zero )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( F )),bind(G,$thf( zero ))]]) ).
thf(185,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( A @ ( C @ quotient ) ) )
| ~ ( E @ ( D @ ( zero @ quotient ) ) )
| ~ ( D @ ( A @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( zero @ quotient ) ) ) ),
inference(simp,[status(thm)],[178]) ).
thf(5276,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( xQy @ ( z @ less_equal ) ) )
| ~ $true
| ( xQy = z ) ),
inference(paramod_ordered,[status(thm)],[42,2113]) ).
thf(5277,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( xQy @ ( z @ less_equal ) ) )
| ( xQy = z ) ),
inference(simp,[status(thm)],[5276]) ).
thf(5387,plain,
! [A: $i] :
( ( xQy != identity )
| ( A != z )
| ( xQy = z ) ),
inference(simp,[status(thm)],[5277]) ).
thf(5393,plain,
( ( xQy != identity )
| ( xQy = z ) ),
inference(simp,[status(thm)],[5387]) ).
thf(7,axiom,
! [A: $i] : ( zero @ ( A @ ( A @ quotient ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_divide_x_is_zero) ).
thf(28,plain,
! [A: $i] : ( zero @ ( A @ ( A @ quotient ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(446,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ quotient ) ) )
!= ( zero @ ( C @ ( B @ quotient ) ) ) )
| ( C @ ( B @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[28,30]) ).
thf(447,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ quotient ) ) )
!= ( zero @ ( C @ ( B @ quotient ) ) ) )
| ( C @ ( B @ less_equal ) ) ),
inference(simp,[status(thm)],[446]) ).
thf(448,plain,
! [A: $i] : ( A @ ( A @ less_equal ) ),
inference(pattern_uni,[status(thm)],[447:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(706,plain,
! [A: $i] :
( ( ( A @ ( A @ less_equal ) )
!= ( y @ ( xQz @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[448,20]) ).
thf(707,plain,
! [A: $i] :
( ( A @ ( A @ less_equal ) )
!= ( y @ ( xQz @ less_equal ) ) ),
inference(simp,[status(thm)],[706]) ).
thf(708,plain,
! [A: $i] :
( ( A != y )
| ( A != xQz ) ),
inference(simp,[status(thm)],[707]) ).
thf(709,plain,
y != xQz,
inference(simp,[status(thm)],[708]) ).
thf(1843,plain,
! [B: $i,A: $i] :
( ( ( x @ ( xQz @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ~ ( A @ ( B @ less_equal ) )
| ~ $true
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[1547,46]) ).
thf(1844,plain,
! [B: $i,A: $i] :
( ( ( x @ ( xQz @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ~ ( A @ ( B @ less_equal ) )
| ( A = B ) ),
inference(simp,[status(thm)],[1843]) ).
thf(1845,plain,
( ~ ( xQz @ ( x @ less_equal ) )
| ( x = xQz ) ),
inference(pattern_uni,[status(thm)],[1844:[bind(A,$thf( xQz )),bind(B,$thf( x ))]]) ).
thf(4169,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( xQz @ ( x @ less_equal ) ) )
| ~ $true
| ( x = xQz ) ),
inference(paramod_ordered,[status(thm)],[42,1845]) ).
thf(4170,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( xQz @ ( x @ less_equal ) ) )
| ( x = xQz ) ),
inference(simp,[status(thm)],[4169]) ).
thf(4274,plain,
! [A: $i] :
( ( identity != xQz )
| ( A != x )
| ( x = xQz ) ),
inference(simp,[status(thm)],[4170]) ).
thf(4287,plain,
( ( identity != xQz )
| ( x = xQz ) ),
inference(simp,[status(thm)],[4274]) ).
thf(3467,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( y @ ( z @ ( x @ quotient ) ) ) )
| ( identity != xQz )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,809]) ).
thf(3468,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( y @ ( z @ ( x @ quotient ) ) ) )
| ( identity != xQz ) ),
inference(simp,[status(thm)],[3467]) ).
thf(3500,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) )
!= y )
| ( B != z )
| ( A != x )
| ( identity != xQz ) ),
inference(simp,[status(thm)],[3468]) ).
thf(3516,plain,
( ( ( z @ ( x @ divide ) )
!= y )
| ( identity != xQz ) ),
inference(simp,[status(thm)],[3500]) ).
thf(17558,plain,
( ( x != x )
| ( ( z @ ( xQz @ divide ) )
!= y )
| ( identity != xQz )
| ( identity != xQz ) ),
inference(paramod_ordered,[status(thm)],[4287,3516]) ).
thf(17559,plain,
( ( x != x )
| ( ( z @ ( xQz @ divide ) )
!= y )
| ( identity != xQz ) ),
inference(simp,[status(thm)],[17558]) ).
thf(17560,plain,
( ( ( z @ ( xQz @ divide ) )
!= y )
| ( identity != xQz ) ),
inference(pattern_uni,[status(thm)],[17559:[]]) ).
thf(569,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( C @ ( B @ ( A @ quotient ) ) ) )
| ~ ( D @ ( B @ ( A @ quotient ) ) )
| ~ $true
| ( C = D ) ),
inference(paramod_ordered,[status(thm)],[41,26]) ).
thf(570,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( C @ ( B @ ( A @ quotient ) ) ) )
| ~ ( D @ ( B @ ( A @ quotient ) ) )
| ( C = D ) ),
inference(simp,[status(thm)],[569]) ).
thf(571,plain,
! [A: $i] :
( ~ ( A @ ( y @ ( x @ quotient ) ) )
| ( xQy = A ) ),
inference(pattern_uni,[status(thm)],[570:[bind(A,$thf( x )),bind(B,$thf( y )),bind(C,$thf( xQy ))]]) ).
thf(661,plain,
! [A: $i] :
( ~ ( A @ ( y @ ( x @ quotient ) ) )
| ( xQy = A ) ),
inference(simp,[status(thm)],[571]) ).
thf(904,plain,
! [A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( A @ ( y @ ( x @ quotient ) ) ) )
| ~ $true
| ( xQy = A ) ),
inference(paramod_ordered,[status(thm)],[36,661]) ).
thf(905,plain,
! [A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( A @ ( y @ ( x @ quotient ) ) ) )
| ( xQy = A ) ),
inference(simp,[status(thm)],[904]) ).
thf(907,plain,
! [A: $i] :
( ( xQz != A )
| ( z != y )
| ( x != x )
| ( xQy = A ) ),
inference(simp,[status(thm)],[905]) ).
thf(915,plain,
( ( z != y )
| ( xQy = xQz ) ),
inference(simp,[status(thm)],[907]) ).
thf(47,plain,
( ( ( z @ ( xQy @ less_equal ) )
!= ( y @ ( xQz @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43,20]) ).
thf(48,plain,
( ( z @ ( xQy @ less_equal ) )
!= ( y @ ( xQz @ less_equal ) ) ),
inference(simp,[status(thm)],[47]) ).
thf(49,plain,
( ( z != y )
| ( xQy != xQz ) ),
inference(simp,[status(thm)],[48]) ).
thf(1152,plain,
( ( xQy != xQy )
| ( z != y )
| ( xQz != xQz )
| ( z != y ) ),
inference(paramod_ordered,[status(thm)],[915,49]) ).
thf(1153,plain,
( ( xQy != xQy )
| ( z != y ) ),
inference(simp,[status(thm)],[1152]) ).
thf(1154,plain,
z != y,
inference(pattern_uni,[status(thm)],[1153:[]]) ).
thf(2011,plain,
! [B: $i,A: $i] :
( ( A != z )
| ( B != y )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[46,1154]) ).
thf(2012,plain,
! [A: $i] :
( ( A != y )
| ~ ( z @ ( A @ less_equal ) )
| ~ ( A @ ( z @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[2011:[bind(A,$thf( z ))]]) ).
thf(2239,plain,
( ~ ( z @ ( y @ less_equal ) )
| ~ ( y @ ( z @ less_equal ) ) ),
inference(simp,[status(thm)],[2012]) ).
thf(11224,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( z @ ( y @ less_equal ) ) )
| ~ $true
| ~ ( y @ ( z @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[31,2239]) ).
thf(11225,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( z @ ( y @ less_equal ) ) )
| ~ ( y @ ( z @ less_equal ) ) ),
inference(simp,[status(thm)],[11224]) ).
thf(11276,plain,
! [A: $i] :
( ( A != z )
| ( zero != y )
| ~ ( y @ ( z @ less_equal ) ) ),
inference(simp,[status(thm)],[11225]) ).
thf(11289,plain,
( ( zero != y )
| ~ ( y @ ( z @ less_equal ) ) ),
inference(simp,[status(thm)],[11276]) ).
thf(70,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( E @ ( D @ ( B @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ $true
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[36,38]) ).
thf(71,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( E @ ( D @ ( B @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[70]) ).
thf(72,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( z @ ( B @ quotient ) ) )
| ~ ( D @ ( xQz @ ( C @ quotient ) ) )
| ~ ( C @ ( z @ ( A @ quotient ) ) )
| ~ ( B @ ( x @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[71:[bind(A,$thf( A )),bind(B,$thf( x )),bind(C,$thf( C )),bind(D,$thf( z )),bind(E,$thf( xQz ))]]) ).
thf(110,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( z @ ( B @ quotient ) ) )
| ~ ( D @ ( xQz @ ( C @ quotient ) ) )
| ~ ( C @ ( z @ ( A @ quotient ) ) )
| ~ ( B @ ( x @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[72]) ).
thf(716,plain,
( ( ( y @ ( x @ less_equal ) )
!= ( y @ ( xQz @ less_equal ) ) )
| ~ $true
| ( xQy != zero ) ),
inference(paramod_ordered,[status(thm)],[463,20]) ).
thf(717,plain,
( ( ( y @ ( x @ less_equal ) )
!= ( y @ ( xQz @ less_equal ) ) )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[716]) ).
thf(730,plain,
( ( y != y )
| ( x != xQz )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[717]) ).
thf(734,plain,
( ( x != xQz )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[730]) ).
thf(4332,plain,
( ( x != x )
| ( xQz != xQz )
| ( xQy != zero )
| ( identity != xQz ) ),
inference(paramod_ordered,[status(thm)],[4287,734]) ).
thf(4333,plain,
( ( x != x )
| ( xQy != zero )
| ( identity != xQz ) ),
inference(simp,[status(thm)],[4332]) ).
thf(4334,plain,
( ( xQy != zero )
| ( identity != xQz ) ),
inference(pattern_uni,[status(thm)],[4333:[]]) ).
thf(173,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( zero @ quotient ) ) )
!= ( F @ ( E @ ( C @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[27,38]) ).
thf(174,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( zero @ quotient ) ) )
!= ( F @ ( E @ ( C @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[173]) ).
thf(175,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( A @ ( C @ quotient ) ) )
| ~ ( E @ ( zero @ ( D @ quotient ) ) )
| ~ ( D @ ( A @ ( B @ quotient ) ) )
| ~ ( C @ ( zero @ ( B @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[174:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( zero )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( zero ))]]) ).
thf(189,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( A @ ( C @ quotient ) ) )
| ~ ( E @ ( zero @ ( D @ quotient ) ) )
| ~ ( D @ ( A @ ( B @ quotient ) ) )
| ~ ( C @ ( zero @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[175]) ).
thf(869,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( A @ ( zero @ quotient ) ) )
!= ( B @ ( y @ ( x @ quotient ) ) ) )
| ~ $true
| ( xQy = B ) ),
inference(paramod_ordered,[status(thm)],[27,661]) ).
thf(870,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( A @ ( zero @ quotient ) ) )
!= ( B @ ( y @ ( x @ quotient ) ) ) )
| ( xQy = B ) ),
inference(simp,[status(thm)],[869]) ).
thf(908,plain,
! [B: $i,A: $i] :
( ( zero != B )
| ( A != y )
| ( x != zero )
| ( xQy = B ) ),
inference(simp,[status(thm)],[870]) ).
thf(916,plain,
( ( x != zero )
| ( xQy = zero ) ),
inference(simp,[status(thm)],[908]) ).
thf(4191,plain,
( ( x != x )
| ( xQz != xQz )
| ( xQy != zero )
| ~ ( xQz @ ( x @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[1845,734]) ).
thf(4192,plain,
( ( x != x )
| ( xQy != zero )
| ~ ( xQz @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[4191]) ).
thf(4193,plain,
( ( xQy != zero )
| ~ ( xQz @ ( x @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[4192:[]]) ).
thf(4785,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( xQz @ ( x @ less_equal ) ) )
| ( xQy != zero )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[31,4193]) ).
thf(4786,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( xQz @ ( x @ less_equal ) ) )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[4785]) ).
thf(4808,plain,
! [A: $i] :
( ( A != xQz )
| ( x != zero )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[4786]) ).
thf(4821,plain,
( ( x != zero )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[4808]) ).
thf(4848,plain,
( ( xQy != xQy )
| ( x != zero )
| ( zero != zero )
| ( x != zero ) ),
inference(paramod_ordered,[status(thm)],[916,4821]) ).
thf(4849,plain,
( ( xQy != xQy )
| ( x != zero ) ),
inference(simp,[status(thm)],[4848]) ).
thf(4850,plain,
x != zero,
inference(pattern_uni,[status(thm)],[4849:[]]) ).
thf(4881,plain,
! [B: $i,A: $i] :
( ( A != x )
| ( B != zero )
| ~ ( A @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[46,4850]) ).
thf(4882,plain,
! [A: $i] :
( ( A != zero )
| ~ ( x @ ( A @ less_equal ) )
| ~ ( A @ ( x @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[4881:[bind(A,$thf( x ))]]) ).
thf(4894,plain,
( ~ ( x @ ( zero @ less_equal ) )
| ~ ( zero @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[4882]) ).
thf(21221,plain,
( ~ $true
| ~ ( zero @ ( x @ less_equal ) ) ),
inference(rewrite,[status(thm)],[4894,31]) ).
thf(21222,plain,
~ ( zero @ ( x @ less_equal ) ),
inference(simp,[status(thm)],[21221]) ).
thf(21302,plain,
( ( ( z @ ( xQy @ less_equal ) )
!= ( zero @ ( x @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43,21222]) ).
thf(21303,plain,
( ( z @ ( xQy @ less_equal ) )
!= ( zero @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[21302]) ).
thf(21327,plain,
( ( z != zero )
| ( xQy != x ) ),
inference(simp,[status(thm)],[21303]) ).
thf(21429,plain,
( ( xQy != xQy )
| ( z != zero )
| ( x != x )
| ~ ( xQy @ ( x @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[1885,21327]) ).
thf(21430,plain,
( ( xQy != xQy )
| ( z != zero )
| ~ ( xQy @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[21429]) ).
thf(21431,plain,
( ( z != zero )
| ~ ( xQy @ ( x @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[21430:[]]) ).
thf(22574,plain,
( ( xQy != xQy )
| ( z != zero )
| ~ ( z @ ( x @ less_equal ) )
| ( z != zero ) ),
inference(paramod_ordered,[status(thm)],[5391,21431]) ).
thf(22575,plain,
( ( xQy != xQy )
| ~ ( z @ ( x @ less_equal ) )
| ( z != zero ) ),
inference(simp,[status(thm)],[22574]) ).
thf(22576,plain,
( ~ ( z @ ( x @ less_equal ) )
| ( z != zero ) ),
inference(pattern_uni,[status(thm)],[22575:[]]) ).
thf(9908,plain,
! [A: $i] :
( ( xQy != xQy )
| ( z != zero )
| ( A != identity )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[661,9853]) ).
thf(9909,plain,
! [A: $i] :
( ( z != zero )
| ( A != identity )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[9908:[]]) ).
thf(9941,plain,
( ( z != zero )
| ~ ( identity @ ( y @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[9909]) ).
thf(1183,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( B @ ( A @ quotient ) ) )
!= ( C @ ( y @ ( x @ quotient ) ) ) )
| ~ $true
| ( xQy = C )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[35,661]) ).
thf(1184,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( B @ ( A @ quotient ) ) )
!= ( C @ ( y @ ( x @ quotient ) ) ) )
| ( xQy = C )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(simp,[status(thm)],[1183]) ).
thf(1185,plain,
( ( xQy = zero )
| ~ ( y @ ( x @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[1184:[bind(A,$thf( x )),bind(B,$thf( y )),bind(C,$thf( zero ))]]) ).
thf(2803,plain,
( ( xQy != xQy )
| ( x != xQz )
| ( zero != zero )
| ~ ( y @ ( x @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[1185,734]) ).
thf(2804,plain,
( ( xQy != xQy )
| ( x != xQz )
| ~ ( y @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[2803]) ).
thf(2805,plain,
( ( x != xQz )
| ~ ( y @ ( x @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[2804:[]]) ).
thf(4203,plain,
( ( x != x )
| ( xQz != xQz )
| ~ ( y @ ( x @ less_equal ) )
| ~ ( xQz @ ( x @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[1845,2805]) ).
thf(4204,plain,
( ( x != x )
| ~ ( y @ ( x @ less_equal ) )
| ~ ( xQz @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[4203]) ).
thf(4205,plain,
( ~ ( y @ ( x @ less_equal ) )
| ~ ( xQz @ ( x @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[4204:[]]) ).
thf(1568,plain,
! [B: $i,A: $i] :
( ( ( x @ ( xQy @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1529,35]) ).
thf(1569,plain,
! [B: $i,A: $i] :
( ( ( x @ ( xQy @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[1568]) ).
thf(1570,plain,
zero @ ( x @ ( xQy @ quotient ) ),
inference(pattern_uni,[status(thm)],[1569:[bind(A,$thf( xQy )),bind(B,$thf( x ))]]) ).
thf(1667,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( x @ ( xQy @ quotient ) ) )
!= ( y @ ( B @ ( A @ quotient ) ) ) )
| ~ $true
| ~ ( identity @ ( B @ ( A @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[1570,656]) ).
thf(1668,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( x @ ( xQy @ quotient ) ) )
!= ( y @ ( B @ ( A @ quotient ) ) ) )
| ~ ( identity @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[1667]) ).
thf(1699,plain,
! [B: $i,A: $i] :
( ( zero != y )
| ( x != B )
| ( xQy != A )
| ~ ( identity @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[1668]) ).
thf(1714,plain,
( ( zero != y )
| ~ ( identity @ ( x @ ( xQy @ quotient ) ) ) ),
inference(simp,[status(thm)],[1699]) ).
thf(82,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( E @ ( D @ ( B @ quotient ) ) )
!= ( C @ ( B @ ( A @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[38]) ).
thf(99,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( A @ ( B @ quotient ) ) )
| ~ ( D @ ( B @ ( C @ quotient ) ) )
| ~ ( C @ ( A @ ( A @ quotient ) ) )
| ~ ( B @ ( A @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[82:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(106,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( A @ ( B @ quotient ) ) )
| ~ ( D @ ( B @ ( C @ quotient ) ) )
| ~ ( C @ ( A @ ( A @ quotient ) ) )
| ~ ( B @ ( A @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[99]) ).
thf(64,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( H @ ( D @ ( C @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ $true
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[41,38]) ).
thf(65,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( H @ ( D @ ( C @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[64]) ).
thf(66,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( xQy @ ( E @ less_equal ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( y @ ( A @ quotient ) ) )
| ~ ( C @ ( y @ ( B @ quotient ) ) )
| ~ ( x @ ( B @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[65:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( x )),bind(D,$thf( y )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( xQy ))]]) ).
thf(104,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( xQy @ ( E @ less_equal ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( y @ ( A @ quotient ) ) )
| ~ ( C @ ( y @ ( B @ quotient ) ) )
| ~ ( x @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[66]) ).
thf(236,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( E @ ( C @ ( D @ quotient ) ) ) )
| ( xQy @ ( E @ less_equal ) )
| ~ $true
| ~ ( D @ ( y @ ( A @ quotient ) ) )
| ~ ( C @ ( y @ ( B @ quotient ) ) )
| ~ ( x @ ( B @ ( A @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[36,104]) ).
thf(237,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( E @ ( C @ ( D @ quotient ) ) ) )
| ( xQy @ ( E @ less_equal ) )
| ~ ( D @ ( y @ ( A @ quotient ) ) )
| ~ ( C @ ( y @ ( B @ quotient ) ) )
| ~ ( x @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[236]) ).
thf(238,plain,
! [B: $i,A: $i] :
( ( xQy @ ( xQz @ less_equal ) )
| ~ ( x @ ( y @ ( A @ quotient ) ) )
| ~ ( z @ ( y @ ( B @ quotient ) ) )
| ~ ( x @ ( B @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[237:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( z )),bind(D,$thf( x )),bind(E,$thf( xQz ))]]) ).
thf(748,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( identity @ ( C @ ( B @ quotient ) ) ) )
| ~ ( y @ ( C @ ( B @ quotient ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[21,656]) ).
thf(749,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( identity @ ( C @ ( B @ quotient ) ) ) )
| ~ ( y @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[748]) ).
thf(750,plain,
~ ( y @ ( zero @ ( identity @ quotient ) ) ),
inference(pattern_uni,[status(thm)],[749:[bind(A,$thf( identity )),bind(B,$thf( identity )),bind(C,$thf( zero ))]]) ).
thf(938,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( y @ ( zero @ ( identity @ quotient ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,750]) ).
thf(939,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( y @ ( zero @ ( identity @ quotient ) ) ) ),
inference(simp,[status(thm)],[938]) ).
thf(962,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) )
!= y )
| ( B != zero )
| ( A != identity ) ),
inference(simp,[status(thm)],[939]) ).
thf(966,plain,
( ( zero @ ( identity @ divide ) )
!= y ),
inference(simp,[status(thm)],[962]) ).
thf(1595,plain,
! [B: $i,A: $i] :
( ( ( x @ ( xQz @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1547,35]) ).
thf(1596,plain,
! [B: $i,A: $i] :
( ( ( x @ ( xQz @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[1595]) ).
thf(1597,plain,
zero @ ( x @ ( xQz @ quotient ) ),
inference(pattern_uni,[status(thm)],[1596:[bind(A,$thf( xQz )),bind(B,$thf( x ))]]) ).
thf(2318,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( x @ ( xQz @ quotient ) ) )
!= ( y @ ( B @ ( A @ quotient ) ) ) )
| ~ $true
| ~ ( identity @ ( B @ ( A @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[1597,656]) ).
thf(2319,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( x @ ( xQz @ quotient ) ) )
!= ( y @ ( B @ ( A @ quotient ) ) ) )
| ~ ( identity @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[2318]) ).
thf(2349,plain,
! [B: $i,A: $i] :
( ( zero != y )
| ( x != B )
| ( xQz != A )
| ~ ( identity @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[2319]) ).
thf(2369,plain,
( ( zero != y )
| ~ ( identity @ ( x @ ( xQz @ quotient ) ) ) ),
inference(simp,[status(thm)],[2349]) ).
thf(16622,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( identity @ ( x @ ( xQz @ quotient ) ) ) )
| ( zero != y )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,2369]) ).
thf(16623,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( identity @ ( x @ ( xQz @ quotient ) ) ) )
| ( zero != y ) ),
inference(simp,[status(thm)],[16622]) ).
thf(16668,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) )
!= identity )
| ( B != x )
| ( A != xQz )
| ( zero != y ) ),
inference(simp,[status(thm)],[16623]) ).
thf(16693,plain,
( ( ( x @ ( xQz @ divide ) )
!= identity )
| ( zero != y ) ),
inference(simp,[status(thm)],[16668]) ).
thf(88,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( H @ ( D @ ( C @ quotient ) ) )
!= ( C @ ( B @ ( A @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[38]) ).
thf(95,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( D @ ( B @ ( C @ quotient ) ) )
| ~ ( C @ ( A @ ( E @ quotient ) ) )
| ~ ( B @ ( A @ ( A @ quotient ) ) )
| ~ ( E @ ( A @ ( E @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[88:[bind(A,$thf( H )),bind(B,$thf( D )),bind(C,$thf( H ))]]) ).
thf(121,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( D @ ( B @ ( C @ quotient ) ) )
| ~ ( C @ ( A @ ( E @ quotient ) ) )
| ~ ( B @ ( A @ ( A @ quotient ) ) )
| ~ ( E @ ( A @ ( E @ quotient ) ) ) ),
inference(simp,[status(thm)],[95]) ).
thf(133,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( F @ ( E @ ( C @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,38]) ).
thf(134,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( F @ ( E @ ( C @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[133]) ).
thf(135,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( zero @ ( C @ quotient ) ) )
| ~ ( E @ ( A @ ( D @ quotient ) ) )
| ~ ( D @ ( zero @ ( B @ quotient ) ) )
| ~ ( C @ ( A @ ( B @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[134:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( D )),bind(E,$thf( zero )),bind(F,$thf( A ))]]) ).
thf(147,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( zero @ ( C @ quotient ) ) )
| ~ ( E @ ( A @ ( D @ quotient ) ) )
| ~ ( D @ ( zero @ ( B @ quotient ) ) )
| ~ ( C @ ( A @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[135]) ).
thf(864,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( C @ ( y @ ( x @ quotient ) ) ) )
| ~ $true
| ( xQy = C ) ),
inference(paramod_ordered,[status(thm)],[22,661]) ).
thf(865,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( C @ ( y @ ( x @ quotient ) ) ) )
| ( xQy = C ) ),
inference(simp,[status(thm)],[864]) ).
thf(866,plain,
( ( y @ ( x @ divide ) )
= xQy ),
inference(pattern_uni,[status(thm)],[865:[bind(A,$thf( x )),bind(B,$thf( y )),bind(C,$thf( y @ ( x @ divide ) ))]]) ).
thf(4363,plain,
( ( x != x )
| ( xQy @ ( y @ ( xQz @ quotient ) ) )
| ( identity != xQz ) ),
inference(paramod_ordered,[status(thm)],[4287,41]) ).
thf(4364,plain,
( ( xQy @ ( y @ ( xQz @ quotient ) ) )
| ( identity != xQz ) ),
inference(pattern_uni,[status(thm)],[4363:[]]) ).
thf(15918,plain,
( ( ( z @ ( xQy @ less_equal ) )
!= ( zero @ ( xQz @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43,15850]) ).
thf(15919,plain,
( ( z @ ( xQy @ less_equal ) )
!= ( zero @ ( xQz @ less_equal ) ) ),
inference(simp,[status(thm)],[15918]) ).
thf(15937,plain,
( ( z != zero )
| ( xQy != xQz ) ),
inference(simp,[status(thm)],[15919]) ).
thf(16002,plain,
! [A: $i] :
( ( xQy != xQy )
| ( z != zero )
| ( A != xQz )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[661,15937]) ).
thf(16003,plain,
! [A: $i] :
( ( z != zero )
| ( A != xQz )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[16002:[]]) ).
thf(16028,plain,
( ( z != zero )
| ~ ( xQz @ ( y @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[16003]) ).
thf(847,plain,
! [B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( B @ ( y @ ( x @ quotient ) ) ) )
| ~ $true
| ( xQy = B ) ),
inference(paramod_ordered,[status(thm)],[21,661]) ).
thf(848,plain,
! [B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( B @ ( y @ ( x @ quotient ) ) ) )
| ( xQy = B ) ),
inference(simp,[status(thm)],[847]) ).
thf(910,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( zero != y )
| ( A != x )
| ( xQy = B ) ),
inference(simp,[status(thm)],[848]) ).
thf(919,plain,
( ( zero != y )
| ( xQy = x ) ),
inference(simp,[status(thm)],[910]) ).
thf(1432,plain,
( ( xQy != xQy )
| ( x @ ( y @ ( x @ quotient ) ) )
| ( zero != y ) ),
inference(paramod_ordered,[status(thm)],[919,41]) ).
thf(1433,plain,
( ( x @ ( y @ ( x @ quotient ) ) )
| ( zero != y ) ),
inference(pattern_uni,[status(thm)],[1432:[]]) ).
thf(58,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( F @ ( D @ ( A @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ $true
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[41,38]) ).
thf(59,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( F @ ( D @ ( A @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[58]) ).
thf(60,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( y @ ( B @ quotient ) ) )
| ~ ( D @ ( C @ ( xQy @ quotient ) ) )
| ~ ( C @ ( y @ ( A @ quotient ) ) )
| ~ ( B @ ( A @ ( x @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[59:[bind(A,$thf( x )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( y )),bind(E,$thf( E )),bind(F,$thf( xQy ))]]) ).
thf(116,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( y @ ( B @ quotient ) ) )
| ~ ( D @ ( C @ ( xQy @ quotient ) ) )
| ~ ( C @ ( y @ ( A @ quotient ) ) )
| ~ ( B @ ( A @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[60]) ).
thf(193,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ quotient ) ) )
!= ( F @ ( E @ ( C @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,38]) ).
thf(194,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ quotient ) ) )
!= ( F @ ( E @ ( C @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[193]) ).
thf(195,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( A @ ( C @ quotient ) ) )
| ~ ( E @ ( zero @ ( D @ quotient ) ) )
| ~ ( D @ ( A @ ( B @ quotient ) ) )
| ~ ( C @ ( A @ ( B @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[194:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( zero ))]]) ).
thf(206,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( A @ ( C @ quotient ) ) )
| ~ ( E @ ( zero @ ( D @ quotient ) ) )
| ~ ( D @ ( A @ ( B @ quotient ) ) )
| ~ ( C @ ( A @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[195]) ).
thf(246,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( F @ ( D @ ( E @ quotient ) ) ) )
| ( xQy @ ( F @ less_equal ) )
| ~ $true
| ~ ( E @ ( y @ ( B @ quotient ) ) )
| ~ ( D @ ( y @ ( C @ quotient ) ) )
| ~ ( x @ ( C @ ( B @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,104]) ).
thf(247,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( F @ ( D @ ( E @ quotient ) ) ) )
| ( xQy @ ( F @ less_equal ) )
| ~ ( E @ ( y @ ( B @ quotient ) ) )
| ~ ( D @ ( y @ ( C @ quotient ) ) )
| ~ ( x @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[246]) ).
thf(248,plain,
! [C: $i,B: $i,A: $i] :
( ( xQy @ ( A @ less_equal ) )
| ~ ( A @ ( y @ ( B @ quotient ) ) )
| ~ ( zero @ ( y @ ( C @ quotient ) ) )
| ~ ( x @ ( C @ ( B @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[247:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( zero )),bind(E,$thf( A )),bind(F,$thf( A ))]]) ).
thf(84,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( F @ ( D @ ( A @ quotient ) ) )
!= ( E @ ( D @ ( B @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[38]) ).
thf(92,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( C @ ( B @ quotient ) ) )
| ~ ( E @ ( D @ ( D @ quotient ) ) )
| ~ ( D @ ( C @ ( A @ quotient ) ) )
| ~ ( B @ ( A @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[84:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( F ))]]) ).
thf(117,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( C @ ( B @ quotient ) ) )
| ~ ( E @ ( D @ ( D @ quotient ) ) )
| ~ ( D @ ( C @ ( A @ quotient ) ) )
| ~ ( B @ ( A @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[92]) ).
thf(4322,plain,
( ( x != x )
| ( xQz @ ( xQy @ less_equal ) )
| ( identity != xQz ) ),
inference(paramod_ordered,[status(thm)],[4287,1529]) ).
thf(4323,plain,
( ( xQz @ ( xQy @ less_equal ) )
| ( identity != xQz ) ),
inference(pattern_uni,[status(thm)],[4322:[]]) ).
thf(18850,plain,
! [B: $i,A: $i] :
( ( ( z @ ( x @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ~ $true
| ( xQy != x ) ),
inference(paramod_ordered,[status(thm)],[18360,35]) ).
thf(18851,plain,
! [B: $i,A: $i] :
( ( ( z @ ( x @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ( xQy != x ) ),
inference(simp,[status(thm)],[18850]) ).
thf(18852,plain,
( ( zero @ ( z @ ( x @ quotient ) ) )
| ( xQy != x ) ),
inference(pattern_uni,[status(thm)],[18851:[bind(A,$thf( x )),bind(B,$thf( z ))]]) ).
thf(13190,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( x @ ( y @ less_equal ) ) )
| ~ $true
| ~ ( y @ ( x @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[31,2247]) ).
thf(13191,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( x @ ( y @ less_equal ) ) )
| ~ ( y @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[13190]) ).
thf(13234,plain,
! [A: $i] :
( ( A != x )
| ( zero != y )
| ~ ( y @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[13191]) ).
thf(13265,plain,
( ( zero != y )
| ~ ( y @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[13234]) ).
thf(4171,plain,
( ( x != x )
| ( xQz @ ( xQy @ less_equal ) )
| ~ ( xQz @ ( x @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[1845,1529]) ).
thf(4172,plain,
( ( xQz @ ( xQy @ less_equal ) )
| ~ ( xQz @ ( x @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[4171:[]]) ).
thf(11516,plain,
! [A: $i] :
( ( ( A @ ( A @ less_equal ) )
!= ( xQz @ ( x @ less_equal ) ) )
| ( xQz @ ( xQy @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[448,4172]) ).
thf(11517,plain,
! [A: $i] :
( ( ( A @ ( A @ less_equal ) )
!= ( xQz @ ( x @ less_equal ) ) )
| ( xQz @ ( xQy @ less_equal ) ) ),
inference(simp,[status(thm)],[11516]) ).
thf(11633,plain,
! [A: $i] :
( ( A != xQz )
| ( A != x )
| ( xQz @ ( xQy @ less_equal ) ) ),
inference(simp,[status(thm)],[11517]) ).
thf(11672,plain,
( ( x != xQz )
| ( xQz @ ( xQy @ less_equal ) ) ),
inference(simp,[status(thm)],[11633]) ).
thf(85,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( G @ ( E @ ( F @ quotient ) ) )
!= ( C @ ( B @ ( A @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[38]) ).
thf(96,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( A @ ( D @ quotient ) ) )
| ~ ( C @ ( A @ ( C @ quotient ) ) )
| ~ ( B @ ( A @ ( B @ quotient ) ) )
| ~ ( D @ ( B @ ( C @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[85:[bind(A,$thf( F )),bind(B,$thf( E )),bind(C,$thf( G ))]]) ).
thf(102,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( A @ ( D @ quotient ) ) )
| ~ ( C @ ( A @ ( C @ quotient ) ) )
| ~ ( B @ ( A @ ( B @ quotient ) ) )
| ~ ( D @ ( B @ ( C @ quotient ) ) ) ),
inference(simp,[status(thm)],[96]) ).
thf(10315,plain,
( ( ( y @ ( x @ less_equal ) )
!= ( y @ ( identity @ less_equal ) ) )
| ~ $true
| ( xQy != zero ) ),
inference(paramod_ordered,[status(thm)],[463,10265]) ).
thf(10316,plain,
( ( ( y @ ( x @ less_equal ) )
!= ( y @ ( identity @ less_equal ) ) )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[10315]) ).
thf(10338,plain,
( ( y != y )
| ( x != identity )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[10316]) ).
thf(10345,plain,
( ( x != identity )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[10338]) ).
thf(2400,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( D @ ( C @ less_equal ) ) )
| ( zero @ ( D @ ( C @ quotient ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1548,35]) ).
thf(2401,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( D @ ( C @ less_equal ) ) )
| ( zero @ ( D @ ( C @ quotient ) ) ) ),
inference(simp,[status(thm)],[2400]) ).
thf(2402,plain,
! [B: $i,A: $i] : ( zero @ ( A @ ( B @ ( A @ divide ) @ quotient ) ) ),
inference(pattern_uni,[status(thm)],[2401:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ divide ) )),bind(D,$thf( E ))]]) ).
thf(2409,plain,
! [B: $i,A: $i] : ( zero @ ( A @ ( B @ ( A @ divide ) @ quotient ) ) ),
inference(simp,[status(thm)],[2402]) ).
thf(20456,plain,
! [A: $i] :
( ( ( A @ ( A @ less_equal ) )
!= ( xQy @ ( z @ less_equal ) ) )
| ( x @ ( z @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[448,5279]) ).
thf(20457,plain,
! [A: $i] :
( ( ( A @ ( A @ less_equal ) )
!= ( xQy @ ( z @ less_equal ) ) )
| ( x @ ( z @ less_equal ) ) ),
inference(simp,[status(thm)],[20456]) ).
thf(20556,plain,
! [A: $i] :
( ( A != xQy )
| ( A != z )
| ( x @ ( z @ less_equal ) ) ),
inference(simp,[status(thm)],[20457]) ).
thf(20565,plain,
( ( xQy != z )
| ( x @ ( z @ less_equal ) ) ),
inference(simp,[status(thm)],[20556]) ).
thf(260,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( x @ ( B @ ( A @ quotient ) ) ) )
| ( xQy @ ( E @ less_equal ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( y @ ( A @ quotient ) ) )
| ~ ( C @ ( y @ ( B @ quotient ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,104]) ).
thf(261,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( x @ ( B @ ( A @ quotient ) ) ) )
| ( xQy @ ( E @ less_equal ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( y @ ( A @ quotient ) ) )
| ~ ( C @ ( y @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[260]) ).
thf(277,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( xQy != x )
| ( y != B )
| ( x != A )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( y @ ( A @ quotient ) ) )
| ~ ( C @ ( y @ ( B @ quotient ) ) )
| ( xQy @ ( E @ less_equal ) ) ),
inference(simp,[status(thm)],[261]) ).
thf(297,plain,
! [C: $i,B: $i,A: $i] :
( ( xQy != x )
| ~ ( C @ ( A @ ( B @ quotient ) ) )
| ~ ( B @ ( y @ ( x @ quotient ) ) )
| ~ ( A @ ( y @ ( y @ quotient ) ) )
| ( xQy @ ( C @ less_equal ) ) ),
inference(simp,[status(thm)],[277]) ).
thf(758,plain,
! [B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( identity @ ( B @ ( A @ quotient ) ) ) )
| ~ ( y @ ( B @ ( A @ quotient ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,656]) ).
thf(759,plain,
! [B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( identity @ ( B @ ( A @ quotient ) ) ) )
| ~ ( y @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[758]) ).
thf(796,plain,
! [B: $i,A: $i] :
( ( xQy != identity )
| ( y != B )
| ( x != A )
| ~ ( y @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[759]) ).
thf(815,plain,
( ( xQy != identity )
| ~ ( y @ ( y @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[796]) ).
thf(10,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(32,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)],[10]) ).
thf(33,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less_equal ) )
| ~ ( C @ ( B @ less_equal ) )
| ~ ( B @ ( A @ less_equal ) ) ),
inference(cnf,[status(esa)],[32]) ).
thf(6633,plain,
( ( ( y @ ( x @ less_equal ) )
!= ( y @ ( x @ less_equal ) ) )
| ( xQy = zero )
| ~ $true
| ( z != zero ) ),
inference(paramod_ordered,[status(thm)],[5694,1185]) ).
thf(6634,plain,
( ( ( y @ ( x @ less_equal ) )
!= ( y @ ( x @ less_equal ) ) )
| ( xQy = zero )
| ( z != zero ) ),
inference(simp,[status(thm)],[6633]) ).
thf(6635,plain,
( ( xQy = zero )
| ( z != zero ) ),
inference(pattern_uni,[status(thm)],[6634:[]]) ).
thf(18241,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( xQy @ ( x @ less_equal ) ) )
| ( z @ ( x @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,4571]) ).
thf(18242,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( xQy @ ( x @ less_equal ) ) )
| ( z @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[18241]) ).
thf(18346,plain,
! [A: $i] :
( ( xQy != identity )
| ( A != x )
| ( z @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[18242]) ).
thf(18362,plain,
( ( xQy != identity )
| ( z @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[18346]) ).
thf(19024,plain,
! [B: $i,A: $i] :
( ( ( z @ ( x @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ~ $true
| ( xQy != identity ) ),
inference(paramod_ordered,[status(thm)],[18362,35]) ).
thf(19025,plain,
! [B: $i,A: $i] :
( ( ( z @ ( x @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ( xQy != identity ) ),
inference(simp,[status(thm)],[19024]) ).
thf(19026,plain,
( ( zero @ ( z @ ( x @ quotient ) ) )
| ( xQy != identity ) ),
inference(pattern_uni,[status(thm)],[19025:[bind(A,$thf( x )),bind(B,$thf( z ))]]) ).
thf(4483,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( xQy @ ( x @ less_equal ) ) )
| ~ $true
| ( xQy = x ) ),
inference(paramod_ordered,[status(thm)],[42,1885]) ).
thf(4484,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( xQy @ ( x @ less_equal ) ) )
| ( xQy = x ) ),
inference(simp,[status(thm)],[4483]) ).
thf(4591,plain,
! [A: $i] :
( ( xQy != identity )
| ( A != x )
| ( xQy = x ) ),
inference(simp,[status(thm)],[4484]) ).
thf(4608,plain,
( ( xQy != identity )
| ( xQy = x ) ),
inference(simp,[status(thm)],[4591]) ).
thf(9288,plain,
( ( xQy != xQy )
| ( zero != y )
| ~ ( identity @ ( x @ ( x @ quotient ) ) )
| ( zero != y ) ),
inference(paramod_ordered,[status(thm)],[919,1714]) ).
thf(9289,plain,
( ( xQy != xQy )
| ~ ( identity @ ( x @ ( x @ quotient ) ) )
| ( zero != y ) ),
inference(simp,[status(thm)],[9288]) ).
thf(9290,plain,
( ~ ( identity @ ( x @ ( x @ quotient ) ) )
| ( zero != y ) ),
inference(pattern_uni,[status(thm)],[9289:[]]) ).
thf(27150,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( identity @ ( x @ ( x @ quotient ) ) ) )
| ~ $true
| ( zero != y ) ),
inference(paramod_ordered,[status(thm)],[22,9290]) ).
thf(27151,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( identity @ ( x @ ( x @ quotient ) ) ) )
| ( zero != y ) ),
inference(simp,[status(thm)],[27150]) ).
thf(27208,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) )
!= identity )
| ( B != x )
| ( A != x )
| ( zero != y ) ),
inference(simp,[status(thm)],[27151]) ).
thf(27228,plain,
( ( ( x @ ( x @ divide ) )
!= identity )
| ( zero != y ) ),
inference(simp,[status(thm)],[27208]) ).
thf(13183,plain,
( ( ( y @ ( x @ less_equal ) )
!= ( y @ ( x @ less_equal ) ) )
| ~ ( x @ ( y @ less_equal ) )
| ~ $true
| ( xQy != zero ) ),
inference(paramod_ordered,[status(thm)],[463,2247]) ).
thf(13184,plain,
( ( ( y @ ( x @ less_equal ) )
!= ( y @ ( x @ less_equal ) ) )
| ~ ( x @ ( y @ less_equal ) )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[13183]) ).
thf(13185,plain,
( ~ ( x @ ( y @ less_equal ) )
| ( xQy != zero ) ),
inference(pattern_uni,[status(thm)],[13184:[]]) ).
thf(13479,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( x @ ( y @ less_equal ) ) )
| ~ $true
| ( xQy != zero ) ),
inference(paramod_ordered,[status(thm)],[31,13185]) ).
thf(13480,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( x @ ( y @ less_equal ) ) )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[13479]) ).
thf(13512,plain,
! [A: $i] :
( ( A != x )
| ( zero != y )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[13480]) ).
thf(13523,plain,
( ( zero != y )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[13512]) ).
thf(13942,plain,
! [A: $i] :
( ( xQy != xQy )
| ( zero != y )
| ( A != zero )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[661,13523]) ).
thf(13943,plain,
! [A: $i] :
( ( zero != y )
| ( A != zero )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[13942:[]]) ).
thf(13976,plain,
( ( zero != y )
| ~ ( zero @ ( y @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[13943]) ).
thf(10671,plain,
! [A: $i] :
( ( xQy != xQy )
| ( x != identity )
| ( A != zero )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[661,10345]) ).
thf(10672,plain,
! [A: $i] :
( ( x != identity )
| ( A != zero )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[10671:[]]) ).
thf(10710,plain,
( ( x != identity )
| ~ ( zero @ ( y @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[10672]) ).
thf(170,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( zero @ quotient ) ) )
!= ( D @ ( C @ ( B @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[27,38]) ).
thf(171,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( zero @ quotient ) ) )
!= ( D @ ( C @ ( B @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) ) ),
inference(simp,[status(thm)],[170]) ).
thf(172,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( B @ ( zero @ quotient ) ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( B @ ( zero @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[171:[bind(A,$thf( A )),bind(B,$thf( zero )),bind(C,$thf( A )),bind(D,$thf( zero ))]]) ).
thf(188,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( B @ ( zero @ quotient ) ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( B @ ( zero @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[172]) ).
thf(760,plain,
! [B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( y @ ( B @ ( A @ quotient ) ) ) )
| ~ $true
| ~ ( identity @ ( B @ ( A @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[41,656]) ).
thf(761,plain,
! [B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( y @ ( B @ ( A @ quotient ) ) ) )
| ~ ( identity @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[760]) ).
thf(788,plain,
! [B: $i,A: $i] :
( ( xQy != y )
| ( y != B )
| ( x != A )
| ~ ( identity @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[761]) ).
thf(807,plain,
( ( xQy != y )
| ~ ( identity @ ( y @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[788]) ).
thf(3327,plain,
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( identity @ ( y @ ( x @ quotient ) ) ) )
| ( xQy != y )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,807]) ).
thf(3328,plain,
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( identity @ ( y @ ( x @ quotient ) ) ) )
| ( xQy != y ) ),
inference(simp,[status(thm)],[3327]) ).
thf(3368,plain,
( ( xQy != identity )
| ( y != y )
| ( x != x )
| ( xQy != y ) ),
inference(simp,[status(thm)],[3328]) ).
thf(3386,plain,
( ( xQy != identity )
| ( xQy != y ) ),
inference(simp,[status(thm)],[3368]) ).
thf(156,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( identity @ ( A @ quotient ) ) )
!= ( G @ ( E @ ( B @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ $true
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[23,38]) ).
thf(157,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( identity @ ( A @ quotient ) ) )
!= ( G @ ( E @ ( B @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[156]) ).
thf(158,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( identity @ ( C @ quotient ) ) )
| ~ ( E @ ( D @ ( zero @ quotient ) ) )
| ~ ( D @ ( identity @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[157:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( identity )),bind(F,$thf( F )),bind(G,$thf( zero ))]]) ).
thf(169,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( identity @ ( C @ quotient ) ) )
| ~ ( E @ ( D @ ( zero @ quotient ) ) )
| ~ ( D @ ( identity @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[158]) ).
thf(83,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( F @ ( D @ ( A @ quotient ) ) )
!= ( C @ ( B @ ( A @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[38]) ).
thf(101,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( B @ ( D @ quotient ) ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( C @ ( B @ ( B @ quotient ) ) )
| ~ ( D @ ( B @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[83:[bind(A,$thf( A )),bind(B,$thf( D )),bind(C,$thf( F ))]]) ).
thf(109,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( B @ ( D @ quotient ) ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( C @ ( B @ ( B @ quotient ) ) )
| ~ ( D @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[101]) ).
thf(1248,plain,
! [B: $i,A: $i] :
( ( ( z @ ( xQy @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43,35]) ).
thf(1249,plain,
! [B: $i,A: $i] :
( ( ( z @ ( xQy @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[1248]) ).
thf(1250,plain,
zero @ ( z @ ( xQy @ quotient ) ),
inference(pattern_uni,[status(thm)],[1249:[bind(A,$thf( xQy )),bind(B,$thf( z ))]]) ).
thf(1332,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( z @ ( xQy @ quotient ) ) )
!= ( y @ ( B @ ( A @ quotient ) ) ) )
| ~ $true
| ~ ( identity @ ( B @ ( A @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[1250,656]) ).
thf(1333,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( z @ ( xQy @ quotient ) ) )
!= ( y @ ( B @ ( A @ quotient ) ) ) )
| ~ ( identity @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[1332]) ).
thf(1358,plain,
! [B: $i,A: $i] :
( ( zero != y )
| ( z != B )
| ( xQy != A )
| ~ ( identity @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[1333]) ).
thf(1368,plain,
( ( zero != y )
| ~ ( identity @ ( z @ ( xQy @ quotient ) ) ) ),
inference(simp,[status(thm)],[1358]) ).
thf(7786,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( identity @ ( z @ ( xQy @ quotient ) ) ) )
| ( zero != y )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,1368]) ).
thf(7787,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( identity @ ( z @ ( xQy @ quotient ) ) ) )
| ( zero != y ) ),
inference(simp,[status(thm)],[7786]) ).
thf(7828,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) )
!= identity )
| ( B != z )
| ( A != xQy )
| ( zero != y ) ),
inference(simp,[status(thm)],[7787]) ).
thf(7846,plain,
( ( ( z @ ( xQy @ divide ) )
!= identity )
| ( zero != y ) ),
inference(simp,[status(thm)],[7828]) ).
thf(4787,plain,
( ( ( z @ ( xQy @ less_equal ) )
!= ( xQz @ ( x @ less_equal ) ) )
| ( xQy != zero )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43,4193]) ).
thf(4788,plain,
( ( ( z @ ( xQy @ less_equal ) )
!= ( xQz @ ( x @ less_equal ) ) )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[4787]) ).
thf(4804,plain,
( ( z != xQz )
| ( xQy != x )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[4788]) ).
thf(13407,plain,
( ( ( x @ ( xQy @ less_equal ) )
!= ( x @ ( y @ less_equal ) ) )
| ~ $true
| ( xQy != zero ) ),
inference(paramod_ordered,[status(thm)],[1529,13185]) ).
thf(13408,plain,
( ( ( x @ ( xQy @ less_equal ) )
!= ( x @ ( y @ less_equal ) ) )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[13407]) ).
thf(13511,plain,
( ( x != x )
| ( xQy != y )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[13408]) ).
thf(13522,plain,
( ( xQy != y )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[13511]) ).
thf(91,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( H @ ( D @ ( C @ quotient ) ) )
!= ( G @ ( E @ ( F @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[38]) ).
thf(98,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( E @ less_equal ) )
| ~ ( E @ ( D @ ( C @ quotient ) ) )
| ~ ( C @ ( D @ ( A @ quotient ) ) )
| ~ ( D @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[91:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( D )),bind(F,$thf( C )),bind(G,$thf( H ))]]) ).
thf(105,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( E @ less_equal ) )
| ~ ( E @ ( D @ ( C @ quotient ) ) )
| ~ ( C @ ( D @ ( A @ quotient ) ) )
| ~ ( D @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[98]) ).
thf(190,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ quotient ) ) )
!= ( D @ ( C @ ( B @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[28,38]) ).
thf(191,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ quotient ) ) )
!= ( D @ ( C @ ( B @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) ) ),
inference(simp,[status(thm)],[190]) ).
thf(192,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( B @ ( zero @ quotient ) ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( B @ ( A @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[191:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A )),bind(D,$thf( zero ))]]) ).
thf(205,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( B @ ( zero @ quotient ) ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( B @ ( A @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[192]) ).
thf(819,plain,
! [A: $i] :
( ( xQy != xQy )
| ( x != xQz )
| ( A != zero )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[661,734]) ).
thf(820,plain,
! [A: $i] :
( ( x != xQz )
| ( A != zero )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[819:[]]) ).
thf(921,plain,
( ( x != xQz )
| ~ ( zero @ ( y @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[820]) ).
thf(11222,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( y @ ( z @ less_equal ) ) )
| ~ ( z @ ( y @ less_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[31,2239]) ).
thf(11223,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( y @ ( z @ less_equal ) ) )
| ~ ( z @ ( y @ less_equal ) ) ),
inference(simp,[status(thm)],[11222]) ).
thf(11265,plain,
! [A: $i] :
( ( A != y )
| ( z != zero )
| ~ ( z @ ( y @ less_equal ) ) ),
inference(simp,[status(thm)],[11223]) ).
thf(11281,plain,
( ( z != zero )
| ~ ( z @ ( y @ less_equal ) ) ),
inference(simp,[status(thm)],[11265]) ).
thf(11361,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( z @ ( y @ less_equal ) ) )
| ( z != zero )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[31,11281]) ).
thf(11362,plain,
! [A: $i] :
( ( ( A @ ( zero @ less_equal ) )
!= ( z @ ( y @ less_equal ) ) )
| ( z != zero ) ),
inference(simp,[status(thm)],[11361]) ).
thf(11390,plain,
! [A: $i] :
( ( A != z )
| ( zero != y )
| ( z != zero ) ),
inference(simp,[status(thm)],[11362]) ).
thf(11407,plain,
( ( zero != y )
| ( z != zero ) ),
inference(simp,[status(thm)],[11390]) ).
thf(162,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( identity @ ( A @ quotient ) ) )
!= ( I @ ( E @ ( D @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ $true
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[23,38]) ).
thf(163,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( identity @ ( A @ quotient ) ) )
!= ( I @ ( E @ ( D @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[162]) ).
thf(164,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( zero @ ( F @ less_equal ) )
| ~ ( F @ ( D @ ( E @ quotient ) ) )
| ~ ( E @ ( identity @ ( B @ quotient ) ) )
| ~ ( D @ ( identity @ ( C @ quotient ) ) )
| ~ ( A @ ( C @ ( B @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[163:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( identity )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( H )),bind(I,$thf( zero ))]]) ).
thf(166,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( zero @ ( F @ less_equal ) )
| ~ ( F @ ( D @ ( E @ quotient ) ) )
| ~ ( E @ ( identity @ ( B @ quotient ) ) )
| ~ ( D @ ( identity @ ( C @ quotient ) ) )
| ~ ( A @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[164]) ).
thf(136,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( G @ ( E @ ( B @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ $true
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,38]) ).
thf(137,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( G @ ( E @ ( B @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[136]) ).
thf(138,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( zero @ ( C @ quotient ) ) )
| ~ ( E @ ( D @ ( A @ quotient ) ) )
| ~ ( D @ ( zero @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[137:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( zero )),bind(F,$thf( F )),bind(G,$thf( A ))]]) ).
thf(148,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( zero @ ( C @ quotient ) ) )
| ~ ( E @ ( D @ ( A @ quotient ) ) )
| ~ ( D @ ( zero @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[138]) ).
thf(9332,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( identity @ ( x @ ( xQy @ quotient ) ) ) )
| ( zero != y )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,1714]) ).
thf(9333,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( identity @ ( x @ ( xQy @ quotient ) ) ) )
| ( zero != y ) ),
inference(simp,[status(thm)],[9332]) ).
thf(9382,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) )
!= identity )
| ( B != x )
| ( A != xQy )
| ( zero != y ) ),
inference(simp,[status(thm)],[9333]) ).
thf(9404,plain,
( ( ( x @ ( xQy @ divide ) )
!= identity )
| ( zero != y ) ),
inference(simp,[status(thm)],[9382]) ).
thf(16010,plain,
( ( xQy != xQy )
| ( z != zero )
| ( z != xQz )
| ( z != zero ) ),
inference(paramod_ordered,[status(thm)],[5391,15937]) ).
thf(16011,plain,
( ( xQy != xQy )
| ( z != xQz )
| ( z != zero ) ),
inference(simp,[status(thm)],[16010]) ).
thf(16012,plain,
( ( z != xQz )
| ( z != zero ) ),
inference(pattern_uni,[status(thm)],[16011:[]]) ).
thf(139,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( H @ ( F @ ( G @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ $true
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,38]) ).
thf(140,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( H @ ( F @ ( G @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[139]) ).
thf(141,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( A @ less_equal ) )
| ~ ( F @ ( E @ ( D @ quotient ) ) )
| ~ ( A @ ( E @ ( B @ quotient ) ) )
| ~ ( zero @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[140:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( zero )),bind(G,$thf( A )),bind(H,$thf( A ))]]) ).
thf(149,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( A @ less_equal ) )
| ~ ( F @ ( E @ ( D @ quotient ) ) )
| ~ ( A @ ( E @ ( B @ quotient ) ) )
| ~ ( zero @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[141]) ).
thf(12658,plain,
! [B: $i,A: $i] :
( ( ( xQz @ ( xQy @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ~ $true
| ( x != xQz ) ),
inference(paramod_ordered,[status(thm)],[11672,35]) ).
thf(12659,plain,
! [B: $i,A: $i] :
( ( ( xQz @ ( xQy @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ( x != xQz ) ),
inference(simp,[status(thm)],[12658]) ).
thf(12660,plain,
( ( zero @ ( xQz @ ( xQy @ quotient ) ) )
| ( x != xQz ) ),
inference(pattern_uni,[status(thm)],[12659:[bind(A,$thf( xQy )),bind(B,$thf( xQz ))]]) ).
thf(21411,plain,
( ( xQy != xQy )
| ( z != zero )
| ( z != x )
| ( z != zero ) ),
inference(paramod_ordered,[status(thm)],[5391,21327]) ).
thf(21412,plain,
( ( xQy != xQy )
| ( z != x )
| ( z != zero ) ),
inference(simp,[status(thm)],[21411]) ).
thf(21413,plain,
( ( z != x )
| ( z != zero ) ),
inference(pattern_uni,[status(thm)],[21412:[]]) ).
thf(89,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( H @ ( D @ ( C @ quotient ) ) )
!= ( E @ ( D @ ( B @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[38]) ).
thf(93,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( E @ ( F @ ( D @ quotient ) ) )
| ~ ( D @ ( C @ ( A @ quotient ) ) )
| ~ ( F @ ( C @ ( B @ quotient ) ) )
| ~ ( B @ ( B @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[89:[bind(A,$thf( A )),bind(B,$thf( C )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( H ))]]) ).
thf(118,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( E @ ( F @ ( D @ quotient ) ) )
| ~ ( D @ ( C @ ( A @ quotient ) ) )
| ~ ( F @ ( C @ ( B @ quotient ) ) )
| ~ ( B @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[93]) ).
thf(7744,plain,
( ( xQy != xQy )
| ( zero != y )
| ~ ( identity @ ( z @ ( x @ quotient ) ) )
| ( zero != y ) ),
inference(paramod_ordered,[status(thm)],[919,1368]) ).
thf(7745,plain,
( ( xQy != xQy )
| ~ ( identity @ ( z @ ( x @ quotient ) ) )
| ( zero != y ) ),
inference(simp,[status(thm)],[7744]) ).
thf(7746,plain,
( ~ ( identity @ ( z @ ( x @ quotient ) ) )
| ( zero != y ) ),
inference(pattern_uni,[status(thm)],[7745:[]]) ).
thf(25770,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( identity @ ( z @ ( x @ quotient ) ) ) )
| ~ $true
| ( zero != y ) ),
inference(paramod_ordered,[status(thm)],[22,7746]) ).
thf(25771,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( identity @ ( z @ ( x @ quotient ) ) ) )
| ( zero != y ) ),
inference(simp,[status(thm)],[25770]) ).
thf(25828,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) )
!= identity )
| ( B != z )
| ( A != x )
| ( zero != y ) ),
inference(simp,[status(thm)],[25771]) ).
thf(25854,plain,
( ( ( z @ ( x @ divide ) )
!= identity )
| ( zero != y ) ),
inference(simp,[status(thm)],[25828]) ).
thf(11363,plain,
( ( ( z @ ( xQy @ less_equal ) )
!= ( z @ ( y @ less_equal ) ) )
| ( z != zero )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43,11281]) ).
thf(11364,plain,
( ( ( z @ ( xQy @ less_equal ) )
!= ( z @ ( y @ less_equal ) ) )
| ( z != zero ) ),
inference(simp,[status(thm)],[11363]) ).
thf(11382,plain,
( ( z != z )
| ( xQy != y )
| ( z != zero ) ),
inference(simp,[status(thm)],[11364]) ).
thf(11402,plain,
( ( xQy != y )
| ( z != zero ) ),
inference(simp,[status(thm)],[11382]) ).
thf(11418,plain,
! [A: $i] :
( ( xQy != xQy )
| ( A != y )
| ( z != zero )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[661,11402]) ).
thf(11419,plain,
! [A: $i] :
( ( A != y )
| ( z != zero )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[11418:[]]) ).
thf(11451,plain,
( ( z != zero )
| ~ ( y @ ( y @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[11419]) ).
thf(182,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( zero @ quotient ) ) )
!= ( I @ ( E @ ( D @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ $true
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[27,38]) ).
thf(183,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( zero @ quotient ) ) )
!= ( I @ ( E @ ( D @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[182]) ).
thf(184,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( zero @ ( F @ less_equal ) )
| ~ ( F @ ( D @ ( E @ quotient ) ) )
| ~ ( E @ ( A @ ( B @ quotient ) ) )
| ~ ( D @ ( A @ ( C @ quotient ) ) )
| ~ ( zero @ ( C @ ( B @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[183:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( zero )),bind(E,$thf( A )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( H )),bind(I,$thf( zero ))]]) ).
thf(187,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( zero @ ( F @ less_equal ) )
| ~ ( F @ ( D @ ( E @ quotient ) ) )
| ~ ( E @ ( A @ ( B @ quotient ) ) )
| ~ ( D @ ( A @ ( C @ quotient ) ) )
| ~ ( zero @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[184]) ).
thf(79,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( H @ ( D @ ( C @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ $true
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[36,38]) ).
thf(80,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( H @ ( D @ ( C @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[79]) ).
thf(81,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( xQz @ ( E @ less_equal ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( z @ ( A @ quotient ) ) )
| ~ ( C @ ( z @ ( B @ quotient ) ) )
| ~ ( x @ ( B @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[80:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( x )),bind(D,$thf( z )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( xQz ))]]) ).
thf(113,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( xQz @ ( E @ less_equal ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( z @ ( A @ quotient ) ) )
| ~ ( C @ ( z @ ( B @ quotient ) ) )
| ~ ( x @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[81]) ).
thf(4367,plain,
( ( x != x )
| ( xQz != xQz )
| ~ ( zero @ ( y @ ( x @ quotient ) ) )
| ( identity != xQz ) ),
inference(paramod_ordered,[status(thm)],[4287,921]) ).
thf(4368,plain,
( ( x != x )
| ~ ( zero @ ( y @ ( x @ quotient ) ) )
| ( identity != xQz ) ),
inference(simp,[status(thm)],[4367]) ).
thf(4369,plain,
( ~ ( zero @ ( y @ ( x @ quotient ) ) )
| ( identity != xQz ) ),
inference(pattern_uni,[status(thm)],[4368:[]]) ).
thf(11228,plain,
( ( ( z @ ( xQy @ less_equal ) )
!= ( z @ ( y @ less_equal ) ) )
| ~ $true
| ~ ( y @ ( z @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[43,2239]) ).
thf(11229,plain,
( ( ( z @ ( xQy @ less_equal ) )
!= ( z @ ( y @ less_equal ) ) )
| ~ ( y @ ( z @ less_equal ) ) ),
inference(simp,[status(thm)],[11228]) ).
thf(11269,plain,
( ( z != z )
| ( xQy != y )
| ~ ( y @ ( z @ less_equal ) ) ),
inference(simp,[status(thm)],[11229]) ).
thf(11283,plain,
( ( xQy != y )
| ~ ( y @ ( z @ less_equal ) ) ),
inference(simp,[status(thm)],[11269]) ).
thf(1434,plain,
( ( xQy != xQy )
| ( zero @ ( z @ ( x @ quotient ) ) )
| ( zero != y ) ),
inference(paramod_ordered,[status(thm)],[919,1250]) ).
thf(1435,plain,
( ( zero @ ( z @ ( x @ quotient ) ) )
| ( zero != y ) ),
inference(pattern_uni,[status(thm)],[1434:[]]) ).
thf(8537,plain,
( ( ( zero @ ( z @ ( x @ quotient ) ) )
!= ( y @ ( z @ ( x @ quotient ) ) ) )
| ( identity != xQz )
| ~ $true
| ( zero != y ) ),
inference(paramod_ordered,[status(thm)],[1435,809]) ).
thf(8538,plain,
( ( ( zero @ ( z @ ( x @ quotient ) ) )
!= ( y @ ( z @ ( x @ quotient ) ) ) )
| ( identity != xQz )
| ( zero != y ) ),
inference(simp,[status(thm)],[8537]) ).
thf(8756,plain,
( ( zero != y )
| ( z != z )
| ( x != x )
| ( identity != xQz )
| ( zero != y ) ),
inference(simp,[status(thm)],[8538]) ).
thf(8799,plain,
( ( identity != xQz )
| ( zero != y ) ),
inference(simp,[status(thm)],[8756]) ).
thf(982,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( identity @ ( zero @ ( y @ quotient ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,753]) ).
thf(983,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ divide ) @ ( B @ ( A @ quotient ) ) )
!= ( identity @ ( zero @ ( y @ quotient ) ) ) ),
inference(simp,[status(thm)],[982]) ).
thf(1006,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ divide ) )
!= identity )
| ( B != zero )
| ( A != y ) ),
inference(simp,[status(thm)],[983]) ).
thf(1011,plain,
( ( zero @ ( y @ divide ) )
!= identity ),
inference(simp,[status(thm)],[1006]) ).
thf(1438,plain,
( ( xQy != xQy )
| ( z @ ( x @ less_equal ) )
| ( zero != y ) ),
inference(paramod_ordered,[status(thm)],[919,43]) ).
thf(1439,plain,
( ( z @ ( x @ less_equal ) )
| ( zero != y ) ),
inference(pattern_uni,[status(thm)],[1438:[]]) ).
thf(5655,plain,
( ( xQy != xQy )
| ( z != zero )
| ( identity != xQz )
| ( z != zero ) ),
inference(paramod_ordered,[status(thm)],[5391,4334]) ).
thf(5656,plain,
( ( xQy != xQy )
| ( identity != xQz )
| ( z != zero ) ),
inference(simp,[status(thm)],[5655]) ).
thf(5657,plain,
( ( identity != xQz )
| ( z != zero ) ),
inference(pattern_uni,[status(thm)],[5656:[]]) ).
thf(13884,plain,
! [A: $i] :
( ( xQy != xQy )
| ( A != y )
| ( xQy != zero )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[661,13522]) ).
thf(13885,plain,
! [A: $i] :
( ( A != y )
| ( xQy != zero )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[13884:[]]) ).
thf(13930,plain,
( ( xQy != zero )
| ~ ( y @ ( y @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[13885]) ).
thf(86,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( G @ ( E @ ( F @ quotient ) ) )
!= ( E @ ( D @ ( B @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[38]) ).
thf(97,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( D @ ( A @ quotient ) ) )
| ~ ( D @ ( D @ ( C @ quotient ) ) )
| ~ ( B @ ( C @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[86:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( C )),bind(D,$thf( G )),bind(E,$thf( G ))]]) ).
thf(103,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( D @ ( A @ quotient ) ) )
| ~ ( D @ ( D @ ( C @ quotient ) ) )
| ~ ( B @ ( C @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[97]) ).
thf(67,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( C @ ( B @ ( A @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[36,38]) ).
thf(68,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( C @ ( B @ ( A @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[67]) ).
thf(69,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( A @ ( xQz @ quotient ) ) )
| ~ ( D @ ( B @ ( C @ quotient ) ) )
| ~ ( C @ ( A @ ( x @ quotient ) ) )
| ~ ( B @ ( A @ ( z @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[68:[bind(A,$thf( x )),bind(B,$thf( z )),bind(C,$thf( xQz ))]]) ).
thf(108,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( A @ ( xQz @ quotient ) ) )
| ~ ( D @ ( B @ ( C @ quotient ) ) )
| ~ ( C @ ( A @ ( x @ quotient ) ) )
| ~ ( B @ ( A @ ( z @ quotient ) ) ) ),
inference(simp,[status(thm)],[69]) ).
thf(936,plain,
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( y @ ( zero @ ( identity @ quotient ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,750]) ).
thf(937,plain,
( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( y @ ( zero @ ( identity @ quotient ) ) ) ),
inference(simp,[status(thm)],[936]) ).
thf(959,plain,
( ( xQy != y )
| ( zero != y )
| ( x != identity ) ),
inference(simp,[status(thm)],[937]) ).
thf(150,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( identity @ ( A @ quotient ) ) )
!= ( D @ ( C @ ( B @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[23,38]) ).
thf(151,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( identity @ ( A @ quotient ) ) )
!= ( D @ ( C @ ( B @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) ) ),
inference(simp,[status(thm)],[150]) ).
thf(152,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( B @ ( zero @ quotient ) ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( B @ ( A @ quotient ) ) )
| ~ ( C @ ( B @ ( identity @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[151:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( identity )),bind(D,$thf( zero ))]]) ).
thf(167,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( B @ ( zero @ quotient ) ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( B @ ( A @ quotient ) ) )
| ~ ( C @ ( B @ ( identity @ quotient ) ) ) ),
inference(simp,[status(thm)],[152]) ).
thf(202,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ quotient ) ) )
!= ( I @ ( E @ ( D @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ $true
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,38]) ).
thf(203,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ quotient ) ) )
!= ( I @ ( E @ ( D @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[202]) ).
thf(204,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( zero @ ( F @ less_equal ) )
| ~ ( F @ ( D @ ( E @ quotient ) ) )
| ~ ( E @ ( A @ ( B @ quotient ) ) )
| ~ ( D @ ( A @ ( C @ quotient ) ) )
| ~ ( A @ ( C @ ( B @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[203:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( A )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( H )),bind(I,$thf( zero ))]]) ).
thf(209,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( zero @ ( F @ less_equal ) )
| ~ ( F @ ( D @ ( E @ quotient ) ) )
| ~ ( E @ ( A @ ( B @ quotient ) ) )
| ~ ( D @ ( A @ ( C @ quotient ) ) )
| ~ ( A @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[204]) ).
thf(76,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( G @ ( E @ ( F @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ $true
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[36,38]) ).
thf(77,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( G @ ( E @ ( F @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[76]) ).
thf(78,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( xQz @ less_equal ) )
| ~ ( E @ ( D @ ( C @ quotient ) ) )
| ~ ( x @ ( D @ ( A @ quotient ) ) )
| ~ ( z @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[77:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( z )),bind(F,$thf( x )),bind(G,$thf( xQz ))]]) ).
thf(112,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( xQz @ less_equal ) )
| ~ ( E @ ( D @ ( C @ quotient ) ) )
| ~ ( x @ ( D @ ( A @ quotient ) ) )
| ~ ( z @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[78]) ).
thf(4335,plain,
( ( x != x )
| ( ( y @ ( xQz @ divide ) )
= xQy )
| ( identity != xQz ) ),
inference(paramod_ordered,[status(thm)],[4287,866]) ).
thf(4336,plain,
( ( ( y @ ( xQz @ divide ) )
= xQy )
| ( identity != xQz ) ),
inference(pattern_uni,[status(thm)],[4335:[]]) ).
thf(142,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( I @ ( E @ ( D @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ $true
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,38]) ).
thf(143,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( I @ ( E @ ( D @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[142]) ).
thf(144,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( F @ less_equal ) )
| ~ ( F @ ( D @ ( E @ quotient ) ) )
| ~ ( E @ ( zero @ ( B @ quotient ) ) )
| ~ ( D @ ( zero @ ( C @ quotient ) ) )
| ~ ( A @ ( C @ ( B @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[143:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( zero )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( H )),bind(I,$thf( A ))]]) ).
thf(145,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( F @ less_equal ) )
| ~ ( F @ ( D @ ( E @ quotient ) ) )
| ~ ( E @ ( zero @ ( B @ quotient ) ) )
| ~ ( D @ ( zero @ ( C @ quotient ) ) )
| ~ ( A @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[144]) ).
thf(262,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( C @ ( y @ ( B @ quotient ) ) ) )
| ( xQy @ ( E @ less_equal ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( y @ ( A @ quotient ) ) )
| ~ $true
| ~ ( x @ ( B @ ( A @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[41,104]) ).
thf(263,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( C @ ( y @ ( B @ quotient ) ) ) )
| ( xQy @ ( E @ less_equal ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( y @ ( A @ quotient ) ) )
| ~ ( x @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[262]) ).
thf(264,plain,
! [C: $i,B: $i,A: $i] :
( ( xQy @ ( C @ less_equal ) )
| ~ ( C @ ( xQy @ ( B @ quotient ) ) )
| ~ ( B @ ( y @ ( A @ quotient ) ) )
| ~ ( x @ ( x @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[263:[bind(A,$thf( A )),bind(B,$thf( x )),bind(C,$thf( xQy ))]]) ).
thf(295,plain,
! [C: $i,B: $i,A: $i] :
( ( xQy @ ( C @ less_equal ) )
| ~ ( C @ ( xQy @ ( B @ quotient ) ) )
| ~ ( B @ ( y @ ( A @ quotient ) ) )
| ~ ( x @ ( x @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[264]) ).
thf(19952,plain,
( ( x != x )
| ~ ( zero @ ( y @ ( xQz @ quotient ) ) )
| ( identity != xQz )
| ( identity != xQz ) ),
inference(paramod_ordered,[status(thm)],[4287,4369]) ).
thf(19953,plain,
( ( x != x )
| ~ ( zero @ ( y @ ( xQz @ quotient ) ) )
| ( identity != xQz ) ),
inference(simp,[status(thm)],[19952]) ).
thf(19954,plain,
( ~ ( zero @ ( y @ ( xQz @ quotient ) ) )
| ( identity != xQz ) ),
inference(pattern_uni,[status(thm)],[19953:[]]) ).
thf(10682,plain,
( ( xQy != xQy )
| ( x != identity )
| ( zero != zero )
| ~ ( y @ ( x @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[1185,10345]) ).
thf(10683,plain,
( ( xQy != xQy )
| ( x != identity )
| ~ ( y @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[10682]) ).
thf(10684,plain,
( ( x != identity )
| ~ ( y @ ( x @ less_equal ) ) ),
inference(pattern_uni,[status(thm)],[10683:[]]) ).
thf(4350,plain,
( ( x != x )
| ( zero @ ( xQz @ ( xQy @ quotient ) ) )
| ( identity != xQz ) ),
inference(paramod_ordered,[status(thm)],[4287,1570]) ).
thf(4351,plain,
( ( zero @ ( xQz @ ( xQy @ quotient ) ) )
| ( identity != xQz ) ),
inference(pattern_uni,[status(thm)],[4350:[]]) ).
thf(9821,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( zero @ ( identity @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1548,9781]) ).
thf(9822,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( zero @ ( identity @ less_equal ) ) ),
inference(simp,[status(thm)],[9821]) ).
thf(9848,plain,
! [B: $i,A: $i] :
( ( A != zero )
| ( ( B @ ( A @ divide ) )
!= identity ) ),
inference(simp,[status(thm)],[9822]) ).
thf(9863,plain,
! [A: $i] :
( ( A @ ( zero @ divide ) )
!= identity ),
inference(simp,[status(thm)],[9848]) ).
thf(5684,plain,
( ( xQy != xQy )
| ( z @ ( y @ ( x @ quotient ) ) )
| ( z != zero ) ),
inference(paramod_ordered,[status(thm)],[5391,41]) ).
thf(5685,plain,
( ( z @ ( y @ ( x @ quotient ) ) )
| ( z != zero ) ),
inference(pattern_uni,[status(thm)],[5684:[]]) ).
thf(5715,plain,
( ( xQy != xQy )
| ( z != zero )
| ~ ( xQz @ ( x @ less_equal ) )
| ( z != zero ) ),
inference(paramod_ordered,[status(thm)],[5391,4193]) ).
thf(5716,plain,
( ( xQy != xQy )
| ~ ( xQz @ ( x @ less_equal ) )
| ( z != zero ) ),
inference(simp,[status(thm)],[5715]) ).
thf(5717,plain,
( ~ ( xQz @ ( x @ less_equal ) )
| ( z != zero ) ),
inference(pattern_uni,[status(thm)],[5716:[]]) ).
thf(1238,plain,
! [B: $i,A: $i] :
( ( ( y @ ( x @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ~ $true
| ( xQy != zero ) ),
inference(paramod_ordered,[status(thm)],[463,35]) ).
thf(1239,plain,
! [B: $i,A: $i] :
( ( ( y @ ( x @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ( xQy != zero ) ),
inference(simp,[status(thm)],[1238]) ).
thf(1240,plain,
( ( zero @ ( y @ ( x @ quotient ) ) )
| ( xQy != zero ) ),
inference(pattern_uni,[status(thm)],[1239:[bind(A,$thf( x )),bind(B,$thf( y ))]]) ).
thf(4621,plain,
! [A: $i] :
( ( xQy != xQy )
| ( A != identity )
| ( xQy = x )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[661,4608]) ).
thf(4622,plain,
! [A: $i] :
( ( A != identity )
| ( xQy = x )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[4621:[]]) ).
thf(4639,plain,
( ( xQy = x )
| ~ ( identity @ ( y @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[4622]) ).
thf(20812,plain,
! [B: $i,A: $i] :
( ( ( x @ ( z @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ~ $true
| ( xQy != z ) ),
inference(paramod_ordered,[status(thm)],[20565,35]) ).
thf(20813,plain,
! [B: $i,A: $i] :
( ( ( x @ ( z @ less_equal ) )
!= ( B @ ( A @ less_equal ) ) )
| ( zero @ ( B @ ( A @ quotient ) ) )
| ( xQy != z ) ),
inference(simp,[status(thm)],[20812]) ).
thf(20814,plain,
( ( zero @ ( x @ ( z @ quotient ) ) )
| ( xQy != z ) ),
inference(pattern_uni,[status(thm)],[20813:[bind(A,$thf( z )),bind(B,$thf( x ))]]) ).
thf(5736,plain,
! [A: $i] :
( ( xQy != xQy )
| ( A != identity )
| ( xQy = z )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[661,5393]) ).
thf(5737,plain,
! [A: $i] :
( ( A != identity )
| ( xQy = z )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[5736:[]]) ).
thf(5756,plain,
( ( xQy = z )
| ~ ( identity @ ( y @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[5737]) ).
thf(24084,plain,
( ( xQy != xQy )
| ( z = x )
| ~ ( identity @ ( y @ ( x @ quotient ) ) )
| ~ ( identity @ ( y @ ( x @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[5756,4639]) ).
thf(24085,plain,
( ( xQy != xQy )
| ( z = x )
| ~ ( identity @ ( y @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[24084]) ).
thf(24086,plain,
( ( z = x )
| ~ ( identity @ ( y @ ( x @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[24085:[]]) ).
thf(52,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( C @ ( B @ ( A @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,38]) ).
thf(53,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( C @ ( B @ ( A @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[52]) ).
thf(54,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( A @ ( xQy @ quotient ) ) )
| ~ ( D @ ( B @ ( C @ quotient ) ) )
| ~ ( C @ ( A @ ( x @ quotient ) ) )
| ~ ( B @ ( A @ ( y @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[53:[bind(A,$thf( x )),bind(B,$thf( y )),bind(C,$thf( xQy ))]]) ).
thf(114,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( A @ ( xQy @ quotient ) ) )
| ~ ( D @ ( B @ ( C @ quotient ) ) )
| ~ ( C @ ( A @ ( x @ quotient ) ) )
| ~ ( B @ ( A @ ( y @ quotient ) ) ) ),
inference(simp,[status(thm)],[54]) ).
thf(13882,plain,
! [A: $i] :
( ( xQy != xQy )
| ( xQy != y )
| ( A != zero )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[661,13522]) ).
thf(13883,plain,
! [A: $i] :
( ( xQy != y )
| ( A != zero )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[13882:[]]) ).
thf(13929,plain,
( ( xQy != y )
| ~ ( zero @ ( y @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[13883]) ).
thf(87,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( G @ ( E @ ( F @ quotient ) ) )
!= ( F @ ( D @ ( A @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( F @ ( D @ ( A @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[38]) ).
thf(94,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( C @ ( B @ quotient ) ) )
| ~ ( D @ ( C @ ( D @ quotient ) ) )
| ~ ( C @ ( C @ ( A @ quotient ) ) )
| ~ ( B @ ( A @ ( D @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[87:[bind(A,$thf( G )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( E )),bind(E,$thf( E )),bind(F,$thf( G ))]]) ).
thf(119,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( C @ ( B @ quotient ) ) )
| ~ ( D @ ( C @ ( D @ quotient ) ) )
| ~ ( C @ ( C @ ( A @ quotient ) ) )
| ~ ( B @ ( A @ ( D @ quotient ) ) ) ),
inference(simp,[status(thm)],[94]) ).
thf(4319,plain,
( ( x != x )
| ( identity != xQz )
| ~ ( y @ ( z @ ( xQz @ quotient ) ) )
| ( identity != xQz ) ),
inference(paramod_ordered,[status(thm)],[4287,809]) ).
thf(4320,plain,
( ( x != x )
| ~ ( y @ ( z @ ( xQz @ quotient ) ) )
| ( identity != xQz ) ),
inference(simp,[status(thm)],[4319]) ).
thf(4321,plain,
( ~ ( y @ ( z @ ( xQz @ quotient ) ) )
| ( identity != xQz ) ),
inference(pattern_uni,[status(thm)],[4320:[]]) ).
thf(196,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ quotient ) ) )
!= ( G @ ( E @ ( B @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ $true
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,38]) ).
thf(197,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ quotient ) ) )
!= ( G @ ( E @ ( B @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[196]) ).
thf(198,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( A @ ( C @ quotient ) ) )
| ~ ( E @ ( D @ ( zero @ quotient ) ) )
| ~ ( D @ ( A @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[197:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( F )),bind(G,$thf( zero ))]]) ).
thf(207,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( A @ ( C @ quotient ) ) )
| ~ ( E @ ( D @ ( zero @ quotient ) ) )
| ~ ( D @ ( A @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[198]) ).
thf(32971,plain,
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( identity @ ( y @ ( x @ quotient ) ) ) )
| ( z = x )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,24086]) ).
thf(32972,plain,
( ( ( xQy @ ( y @ ( x @ quotient ) ) )
!= ( identity @ ( y @ ( x @ quotient ) ) ) )
| ( z = x ) ),
inference(simp,[status(thm)],[32971]) ).
thf(33118,plain,
( ( xQy != identity )
| ( y != y )
| ( x != x )
| ( z = x ) ),
inference(simp,[status(thm)],[32972]) ).
thf(33148,plain,
( ( xQy != identity )
| ( z = x ) ),
inference(simp,[status(thm)],[33118]) ).
thf(21403,plain,
! [A: $i] :
( ( xQy != xQy )
| ( z != zero )
| ( A != x )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[661,21327]) ).
thf(21404,plain,
! [A: $i] :
( ( z != zero )
| ( A != x )
| ~ ( A @ ( y @ ( x @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[21403:[]]) ).
thf(21440,plain,
( ( z != zero )
| ~ ( x @ ( y @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[21404]) ).
thf(153,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( identity @ ( A @ quotient ) ) )
!= ( F @ ( E @ ( C @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[23,38]) ).
thf(154,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( identity @ ( A @ quotient ) ) )
!= ( F @ ( E @ ( C @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( D @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[153]) ).
thf(155,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( identity @ ( C @ quotient ) ) )
| ~ ( E @ ( zero @ ( D @ quotient ) ) )
| ~ ( D @ ( identity @ ( B @ quotient ) ) )
| ~ ( C @ ( A @ ( B @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[154:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( D )),bind(E,$thf( identity )),bind(F,$thf( zero ))]]) ).
thf(168,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( identity @ ( C @ quotient ) ) )
| ~ ( E @ ( zero @ ( D @ quotient ) ) )
| ~ ( D @ ( identity @ ( B @ quotient ) ) )
| ~ ( C @ ( A @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[155]) ).
thf(130,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( D @ ( C @ ( B @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[21,38]) ).
thf(131,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ ( A @ quotient ) ) )
!= ( D @ ( C @ ( B @ quotient ) ) ) )
| ( I @ ( H @ less_equal ) )
| ~ ( I @ ( E @ ( D @ quotient ) ) )
| ~ ( H @ ( F @ ( G @ quotient ) ) )
| ~ ( G @ ( E @ ( B @ quotient ) ) )
| ~ ( F @ ( E @ ( C @ quotient ) ) ) ),
inference(simp,[status(thm)],[130]) ).
thf(132,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( B @ ( A @ quotient ) ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( B @ ( A @ quotient ) ) )
| ~ ( C @ ( B @ ( zero @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[131:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( zero )),bind(D,$thf( A ))]]) ).
thf(146,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ less_equal ) )
| ~ ( F @ ( B @ ( A @ quotient ) ) )
| ~ ( E @ ( C @ ( D @ quotient ) ) )
| ~ ( D @ ( B @ ( A @ quotient ) ) )
| ~ ( C @ ( B @ ( zero @ quotient ) ) ) ),
inference(simp,[status(thm)],[132]) ).
thf(254,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ quotient ) ) )
!= ( E @ ( y @ ( B @ quotient ) ) ) )
| ( xQy @ ( F @ less_equal ) )
| ~ ( F @ ( D @ ( E @ quotient ) ) )
| ~ $true
| ~ ( D @ ( y @ ( C @ quotient ) ) )
| ~ ( x @ ( C @ ( B @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,104]) ).
thf(255,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( zero @ ( A @ ( A @ quotient ) ) )
!= ( E @ ( y @ ( B @ quotient ) ) ) )
| ( xQy @ ( F @ less_equal ) )
| ~ ( F @ ( D @ ( E @ quotient ) ) )
| ~ ( D @ ( y @ ( C @ quotient ) ) )
| ~ ( x @ ( C @ ( B @ quotient ) ) ) ),
inference(simp,[status(thm)],[254]) ).
thf(256,plain,
! [C: $i,B: $i,A: $i] :
( ( xQy @ ( C @ less_equal ) )
| ~ ( C @ ( B @ ( zero @ quotient ) ) )
| ~ ( B @ ( y @ ( A @ quotient ) ) )
| ~ ( x @ ( A @ ( y @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[255:[bind(A,$thf( y )),bind(B,$thf( y )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( zero ))]]) ).
thf(294,plain,
! [C: $i,B: $i,A: $i] :
( ( xQy @ ( C @ less_equal ) )
| ~ ( C @ ( B @ ( zero @ quotient ) ) )
| ~ ( B @ ( y @ ( A @ quotient ) ) )
| ~ ( x @ ( A @ ( y @ quotient ) ) ) ),
inference(simp,[status(thm)],[256]) ).
thf(13078,plain,
( ( ( x @ ( xQy @ less_equal ) )
!= ( x @ ( y @ less_equal ) ) )
| ~ $true
| ~ ( y @ ( x @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[1529,2247]) ).
thf(13079,plain,
( ( ( x @ ( xQy @ less_equal ) )
!= ( x @ ( y @ less_equal ) ) )
| ~ ( y @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[13078]) ).
thf(13228,plain,
( ( x != x )
| ( xQy != y )
| ~ ( y @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[13079]) ).
thf(13262,plain,
( ( xQy != y )
| ~ ( y @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[13228]) ).
thf(21280,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( zero @ ( x @ less_equal ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1548,21222]) ).
thf(21281,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ divide ) @ less_equal ) )
!= ( zero @ ( x @ less_equal ) ) ),
inference(simp,[status(thm)],[21280]) ).
thf(21335,plain,
! [B: $i,A: $i] :
( ( A != zero )
| ( ( B @ ( A @ divide ) )
!= x ) ),
inference(simp,[status(thm)],[21281]) ).
thf(21351,plain,
! [A: $i] :
( ( A @ ( zero @ divide ) )
!= x ),
inference(simp,[status(thm)],[21335]) ).
thf(5666,plain,
( ( xQy != xQy )
| ( x != xQz )
| ( z != zero )
| ( z != zero ) ),
inference(paramod_ordered,[status(thm)],[5391,734]) ).
thf(5667,plain,
( ( xQy != xQy )
| ( x != xQz )
| ( z != zero ) ),
inference(simp,[status(thm)],[5666]) ).
thf(5668,plain,
( ( x != xQz )
| ( z != zero ) ),
inference(pattern_uni,[status(thm)],[5667:[]]) ).
thf(5680,plain,
( ( xQy != xQy )
| ( zero @ ( x @ ( z @ quotient ) ) )
| ( z != zero ) ),
inference(paramod_ordered,[status(thm)],[5391,1570]) ).
thf(5681,plain,
( ( zero @ ( x @ ( z @ quotient ) ) )
| ( z != zero ) ),
inference(pattern_uni,[status(thm)],[5680:[]]) ).
thf(4394,plain,
( ( x != x )
| ( xQz @ ( z @ ( xQz @ quotient ) ) )
| ( identity != xQz ) ),
inference(paramod_ordered,[status(thm)],[4287,36]) ).
thf(4395,plain,
( ( xQz @ ( z @ ( xQz @ quotient ) ) )
| ( identity != xQz ) ),
inference(pattern_uni,[status(thm)],[4394:[]]) ).
thf(4343,plain,
( ( x != x )
| ( xQz != xQz )
| ~ ( y @ ( x @ less_equal ) )
| ( identity != xQz ) ),
inference(paramod_ordered,[status(thm)],[4287,2805]) ).
thf(4344,plain,
( ( x != x )
| ~ ( y @ ( x @ less_equal ) )
| ( identity != xQz ) ),
inference(simp,[status(thm)],[4343]) ).
thf(4345,plain,
( ~ ( y @ ( x @ less_equal ) )
| ( identity != xQz ) ),
inference(pattern_uni,[status(thm)],[4344:[]]) ).
thf(73,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( F @ ( D @ ( A @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ $true
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(paramod_ordered,[status(thm)],[36,38]) ).
thf(74,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( xQz @ ( z @ ( x @ quotient ) ) )
!= ( F @ ( D @ ( A @ quotient ) ) ) )
| ( H @ ( G @ less_equal ) )
| ~ ( H @ ( D @ ( C @ quotient ) ) )
| ~ ( G @ ( E @ ( F @ quotient ) ) )
| ~ ( E @ ( D @ ( B @ quotient ) ) )
| ~ ( C @ ( B @ ( A @ quotient ) ) ) ),
inference(simp,[status(thm)],[73]) ).
thf(75,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( z @ ( B @ quotient ) ) )
| ~ ( D @ ( C @ ( xQz @ quotient ) ) )
| ~ ( C @ ( z @ ( A @ quotient ) ) )
| ~ ( B @ ( A @ ( x @ quotient ) ) ) ),
inference(pattern_uni,[status(thm)],[74:[bind(A,$thf( x )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( z )),bind(E,$thf( E )),bind(F,$thf( xQz ))]]) ).
thf(111,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ less_equal ) )
| ~ ( E @ ( z @ ( B @ quotient ) ) )
| ~ ( D @ ( C @ ( xQz @ quotient ) ) )
| ~ ( C @ ( z @ ( A @ quotient ) ) )
| ~ ( B @ ( A @ ( x @ quotient ) ) ) ),
inference(simp,[status(thm)],[75]) ).
thf(10305,plain,
( ( ( y @ ( x @ less_equal ) )
!= ( y @ ( identity @ less_equal ) ) )
| ~ $true
| ( z != zero ) ),
inference(paramod_ordered,[status(thm)],[5694,10265]) ).
thf(10306,plain,
( ( ( y @ ( x @ less_equal ) )
!= ( y @ ( identity @ less_equal ) ) )
| ( z != zero ) ),
inference(simp,[status(thm)],[10305]) ).
thf(10337,plain,
( ( y != y )
| ( x != identity )
| ( z != zero ) ),
inference(simp,[status(thm)],[10306]) ).
thf(10344,plain,
( ( x != identity )
| ( z != zero ) ),
inference(simp,[status(thm)],[10337]) ).
thf(11134,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( z @ ( y @ less_equal ) ) )
| ~ $true
| ~ ( y @ ( z @ less_equal ) ) ),
inference(paramod_ordered,[status(thm)],[42,2239]) ).
thf(11135,plain,
! [A: $i] :
( ( ( identity @ ( A @ less_equal ) )
!= ( z @ ( y @ less_equal ) ) )
| ~ ( y @ ( z @ less_equal ) ) ),
inference(simp,[status(thm)],[11134]) ).
thf(11280,plain,
! [A: $i] :
( ( z != identity )
| ( A != y )
| ~ ( y @ ( z @ less_equal ) ) ),
inference(simp,[status(thm)],[11135]) ).
thf(11294,plain,
( ( z != identity )
| ~ ( y @ ( z @ less_equal ) ) ),
inference(simp,[status(thm)],[11280]) ).
thf(73613,plain,
$false,
inference(e,[status(thm)],[809,18360,4571,2412,5654,20640,115,9918,120,13152,1608,10346,15948,6640,185,5393,42,709,24,1529,37,17560,11289,110,4334,125,5279,189,448,29,20,22576,9941,46,4205,1714,106,238,966,9781,16693,121,147,734,866,4364,16028,1433,116,206,248,117,4323,661,18852,13265,11672,102,4172,10345,2409,2805,20565,297,21,815,33,6635,19026,1570,28,38,4608,27228,13976,1012,10710,5391,188,3386,169,109,753,7846,5694,21431,4804,129,41,13522,105,205,921,11407,1185,750,166,148,1548,9853,9404,16012,149,12660,32,34,1154,22,44,21413,118,27,25854,919,9290,7746,21222,11451,187,113,4369,11283,8799,1011,39,1439,10265,5657,13930,103,4850,108,959,2369,1435,1250,167,11402,35,2239,209,112,4336,145,1845,1547,295,13523,19954,10684,1368,4287,15937,463,4351,13185,31,2247,2113,656,9863,5685,5717,43,1240,4639,104,20814,21327,40,26,24086,114,13929,5756,3516,23,119,4321,207,33148,21440,36,168,146,30,19,294,807,4193,15850,13262,21351,5668,20563,5681,4395,1597,1885,4345,111,11281,10344,11294,18362]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HEN006-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.13/0.40 % Computer : n019.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Fri Sep 25 15:56:49 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 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
% 0.83/0.99 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.19/1.18 % [INFO] Parsing done (181ms).
% 1.19/1.19 % [INFO] Running in sequential loop mode.
% 1.97/1.61 % [INFO] eprover registered as external prover.
% 1.97/1.61 % [INFO] Scanning for conjecture ...
% 2.14/1.70 % [INFO] Found a conjecture (or negated_conjecture) and 17 axioms. Running axiom selection ...
% 2.14/1.76 % [INFO] Axiom selection finished. Selected 17 axioms (removed 0 axioms).
% 2.14/1.79 % [INFO] Problem is propositional (TPTP CNF).
% 2.14/1.79 % [INFO] Type checking passed.
% 2.30/1.80 % [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 ...
% 99.90/26.00 % External prover 'e' found a proof!
% 99.90/26.01 % [INFO] Killing All external provers ...
% 99.90/26.01 % Time passed: 25456ms (effective reasoning time: 24808ms)
% 99.90/26.01 % Axioms used in derivation (17): quotient_property, xQz, closure, everything_divide_identity_is_zero, zero_divide_anything_is_zero, zero_is_smallest, xQyLEz, xQy, transitivity_of_less_equal, less_equal_quotient, identity_is_largest, x_divide_x_is_zero, quotient_less_equal, divisor_existence, well_defined, x_divde_zero_is_x, less_equal_and_equal
% 99.90/26.01 % No. of inferences in proof: 677
% 99.90/26.01 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : 25456 ms resp. 24808 ms w/o parsing
% 101.76/26.33 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 101.76/26.34 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------