%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ALG007-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n016.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 06:45:53 AM UTC 2026
% Result : Unsatisfiable 73.13s 17.73s
% Output : Refutation 61.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 4
% Syntax : Number of formulae : 340 ( 172 unt; 0 typ; 0 def)
% Number of atoms : 554 ( 553 equ; 0 cnn)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 3311 ( 507 ~; 214 |; 0 &;2590 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 6 ( 4 usr; 4 con; 0-2 aty)
% Number of variables : 740 ( 0 ^; 740 !; 0 ?; 740 :)
% Comments :
%------------------------------------------------------------------------------
thf(difference_decl,type,
difference: $i > $i > $i ).
thf(a_decl,type,
a: $i ).
thf(b_decl,type,
b: $i ).
thf(c_decl,type,
c: $i ).
thf(2,axiom,
! [B: $i,A: $i] :
( ( A @ ( B @ difference ) @ ( A @ difference ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',set_difference_1) ).
thf(8,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ difference ) @ ( A @ difference ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(9,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ difference ) @ ( A @ difference ) )
= A ),
inference(lifteq,[status(thm)],[8]) ).
thf(18,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( C @ ( D @ difference ) ) )
| ( ( A @ ( C @ difference ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[9,9]) ).
thf(19,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ difference ) @ difference ) )
= ( B @ ( A @ difference ) ) ),
inference(pattern_uni,[status(thm)],[18:[bind(A,$thf( F )),bind(B,$thf( E )),bind(C,$thf( F @ ( E @ difference ) )),bind(D,$thf( F ))]]) ).
thf(28,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ difference ) @ difference ) )
= ( B @ ( A @ difference ) ) ),
inference(simp,[status(thm)],[19]) ).
thf(3,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ difference ) @ ( A @ difference ) )
= ( A @ ( B @ difference ) @ ( B @ difference ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',set_difference_2) ).
thf(10,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ difference ) @ ( A @ difference ) )
= ( A @ ( B @ difference ) @ ( B @ difference ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(11,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ difference ) @ ( A @ difference ) )
= ( A @ ( B @ difference ) @ ( B @ difference ) ) ),
inference(lifteq,[status(thm)],[10]) ).
thf(129,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ difference ) @ difference ) )
!= ( D @ ( C @ difference ) ) )
| ( ( B @ ( A @ difference ) @ ( C @ difference ) )
= ( C @ ( D @ difference ) @ ( D @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,11]) ).
thf(130,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
= ( B @ ( A @ difference ) @ ( B @ difference ) @ ( B @ difference ) ) ),
inference(pattern_uni,[status(thm)],[129:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ difference ) )),bind(D,$thf( F ))]]) ).
thf(206,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
= ( B @ ( A @ difference ) @ ( B @ difference ) @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[130]) ).
thf(12197,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
= ( B @ ( B @ difference ) ) ),
inference(rewrite,[status(thm)],[206,9]) ).
thf(4,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ difference ) @ difference ) )
= ( B @ ( C @ ( A @ difference ) @ difference ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',set_difference_3_simplified) ).
thf(12,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ difference ) @ difference ) )
= ( B @ ( C @ ( A @ difference ) @ difference ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(13,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ difference ) @ difference ) )
= ( B @ ( C @ ( A @ difference ) @ difference ) ) ),
inference(lifteq,[status(thm)],[12]) ).
thf(370,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( D @ ( E @ difference ) ) )
| ( ( B @ ( C @ ( A @ difference ) @ difference ) @ ( D @ difference ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[13,9]) ).
thf(371,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ difference ) @ difference ) @ ( A @ difference ) )
= A ),
inference(pattern_uni,[status(thm)],[370:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( C )),bind(D,$thf( C )),bind(E,$thf( G @ ( F @ difference ) ))]]) ).
thf(532,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ difference ) @ difference ) @ ( A @ difference ) )
= A ),
inference(simp,[status(thm)],[371]) ).
thf(674,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( A @ difference ) )
!= ( E @ ( C @ ( D @ difference ) @ difference ) ) )
| ( ( A @ ( B @ difference ) @ ( B @ difference ) @ ( C @ difference ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[11,532]) ).
thf(675,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ difference ) @ ( A @ difference ) @ ( A @ difference ) @ ( C @ difference ) )
= C ),
inference(pattern_uni,[status(thm)],[674:[bind(A,$thf( K @ ( J @ difference ) )),bind(B,$thf( I )),bind(C,$thf( K )),bind(D,$thf( J )),bind(E,$thf( I @ ( K @ ( J @ difference ) @ difference ) ))]]) ).
thf(740,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ difference ) @ ( A @ difference ) @ ( A @ difference ) @ ( C @ difference ) )
= C ),
inference(simp,[status(thm)],[675]) ).
thf(4396,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ ( B @ difference ) @ difference ) @ ( A @ difference ) )
!= ( F @ ( E @ difference ) @ ( D @ difference ) ) )
| ( ( A @ ( D @ difference ) @ ( F @ difference ) )
= F ) ),
inference(paramod_ordered,[status(thm)],[532,740]) ).
thf(4397,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ difference ) @ ( A @ difference ) )
= A ),
inference(pattern_uni,[status(thm)],[4396:[bind(A,$thf( H )),bind(B,$thf( G )),bind(C,$thf( C )),bind(D,$thf( H )),bind(E,$thf( H @ ( G @ difference ) )),bind(F,$thf( C ))]]) ).
thf(4642,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ difference ) @ ( A @ difference ) )
= A ),
inference(simp,[status(thm)],[4397]) ).
thf(1,negated_conjecture,
( ( c @ ( b @ ( a @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) @ ( c @ ( a @ difference ) @ difference ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_set_difference_3) ).
thf(5,plain,
( ( c @ ( b @ ( a @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) @ ( c @ ( a @ difference ) @ difference ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(6,plain,
( ( c @ ( b @ ( a @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) @ ( c @ ( a @ difference ) @ difference ) ) ),
inference(polarity_switch,[status(thm)],[5]) ).
thf(7,plain,
( ( c @ ( b @ difference ) @ ( c @ ( a @ difference ) @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ),
inference(lifteq,[status(thm)],[6]) ).
thf(16,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( c @ ( b @ difference ) ) )
| ( ( A @ ( c @ ( a @ difference ) @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,7]) ).
thf(24,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ difference ) )
!= c )
| ( A != b )
| ( ( A @ ( c @ ( a @ difference ) @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(simp,[status(thm)],[16]) ).
thf(33,plain,
! [A: $i] :
( ( ( b @ ( A @ difference ) )
!= c )
| ( ( b @ ( c @ ( a @ difference ) @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(simp,[status(thm)],[24]) ).
thf(1639,plain,
! [A: $i] :
( ( b @ ( A @ difference ) )
!= c ),
inference(simplifyReflect,[status(thm)],[33,13]) ).
thf(1642,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( b @ ( C @ difference ) ) )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[9,1639]) ).
thf(1659,plain,
! [B: $i,A: $i] :
( ( c @ ( A @ difference ) @ ( c @ difference ) )
!= ( b @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[1642]) ).
thf(1671,plain,
! [B: $i,A: $i] :
( ( c @ ( A @ difference ) @ ( c @ difference ) )
!= ( b @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[1659]) ).
thf(3033,plain,
! [A: $i] :
( ( b @ ( A @ difference ) )
!= c ),
inference(rewrite,[status(thm)],[1671,9]) ).
thf(6759,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ difference ) @ ( A @ difference ) )
!= ( b @ ( C @ difference ) ) )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[4642,3033]) ).
thf(6949,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ difference ) )
!= b )
| ( c != B ) ),
inference(simp,[status(thm)],[6759]) ).
thf(7160,plain,
! [A: $i] :
( ( A @ ( A @ difference ) )
!= b ),
inference(simp,[status(thm)],[6949]) ).
thf(7322,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ ( B @ difference ) @ difference ) @ ( A @ difference ) )
!= ( D @ ( D @ difference ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[532,7160]) ).
thf(7335,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( b @ ( A @ difference ) @ difference ) )
!= C )
| ( b != C ) ),
inference(simp,[status(thm)],[7322]) ).
thf(7347,plain,
! [B: $i,A: $i] :
( ( B @ ( b @ ( A @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[7335]) ).
thf(12361,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
!= ( D @ ( b @ ( C @ difference ) @ difference ) ) )
| ( ( B @ ( B @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[12197,7347]) ).
thf(12362,plain,
( ( b @ ( b @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[12361:[bind(A,$thf( E )),bind(B,$thf( b )),bind(C,$thf( E )),bind(D,$thf( b @ ( E @ difference ) ))]]) ).
thf(1643,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( b @ ( D @ difference ) ) )
| ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[13,1639]) ).
thf(1644,plain,
! [B: $i,A: $i] :
( ( B @ ( b @ ( A @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[1643:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( b )),bind(D,$thf( F @ ( E @ difference ) ))]]) ).
thf(1662,plain,
! [B: $i,A: $i] :
( ( B @ ( b @ ( A @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[1644]) ).
thf(1721,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( A @ difference ) )
!= ( D @ ( b @ ( C @ difference ) @ difference ) ) )
| ( ( A @ ( B @ difference ) @ ( B @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[11,1662]) ).
thf(1722,plain,
! [B: $i,A: $i] :
( ( b @ ( B @ difference ) @ ( A @ difference ) @ ( A @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[1721:[bind(A,$thf( b @ ( I @ difference ) )),bind(B,$thf( H )),bind(C,$thf( I )),bind(D,$thf( H @ ( b @ ( I @ difference ) @ difference ) ))]]) ).
thf(1756,plain,
! [B: $i,A: $i] :
( ( b @ ( B @ difference ) @ ( A @ difference ) @ ( A @ difference ) )
!= c ),
inference(simp,[status(thm)],[1722]) ).
thf(4152,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( A @ difference ) )
!= ( b @ ( D @ difference ) @ ( C @ difference ) ) )
| ( ( A @ ( B @ difference ) @ ( B @ difference ) @ ( C @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[11,1756]) ).
thf(4153,plain,
! [A: $i] :
( ( A @ ( b @ difference ) @ ( b @ difference ) @ ( A @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[4152:[bind(A,$thf( A )),bind(B,$thf( b )),bind(C,$thf( A )),bind(D,$thf( A ))]]) ).
thf(6773,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ difference ) @ ( A @ difference ) )
!= ( C @ ( b @ difference ) @ ( b @ difference ) @ ( C @ difference ) ) )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[4642,4153]) ).
thf(6990,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ difference ) )
!= ( B @ ( b @ difference ) @ ( b @ difference ) ) )
| ( c != B ) ),
inference(simp,[status(thm)],[6773]) ).
thf(7201,plain,
! [A: $i] :
( ( A @ ( A @ difference ) )
!= ( c @ ( b @ difference ) @ ( b @ difference ) ) ),
inference(simp,[status(thm)],[6990]) ).
thf(10298,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) @ ( b @ difference ) ) )
| ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= ( D @ ( D @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[13,7201]) ).
thf(10371,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C
!= ( c @ ( b @ difference ) ) )
| ( ( B @ ( A @ difference ) )
!= b )
| ( B != D )
| ( ( C @ ( A @ difference ) )
!= D ) ),
inference(simp,[status(thm)],[10298]) ).
thf(10407,plain,
! [A: $i] :
( ( c @ ( b @ difference ) @ ( A @ difference ) @ ( A @ difference ) )
!= b ),
inference(simp,[status(thm)],[10371]) ).
thf(1650,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ ( B @ difference ) @ difference ) @ ( A @ difference ) )
!= ( b @ ( D @ difference ) ) )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[532,1639]) ).
thf(1653,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( c @ ( A @ difference ) @ difference ) )
!= b )
| ( c != C ) ),
inference(simp,[status(thm)],[1650]) ).
thf(1665,plain,
! [B: $i,A: $i] :
( ( B @ ( c @ ( A @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[1653]) ).
thf(1766,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= ( E @ ( c @ ( D @ difference ) @ difference ) ) )
| ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[13,1665]) ).
thf(1767,plain,
! [B: $i,A: $i] :
( ( c @ ( B @ ( A @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[1766:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( c )),bind(D,$thf( A )),bind(E,$thf( B ))]]) ).
thf(14,plain,
( ( ( c @ ( b @ difference ) )
!= c )
| ( ( c @ ( a @ difference ) )
!= ( b @ ( a @ difference ) ) ) ),
inference(simp,[status(thm)],[7]) ).
thf(74,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) ) )
| ( ( B @ ( A @ difference ) )
!= c )
| ( ( c @ ( a @ difference ) )
!= ( b @ ( a @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,14]) ).
thf(75,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) ) )
| ( ( B @ ( A @ difference ) )
!= c )
| ( c != b )
| ( a != a ) ),
inference(simp,[status(thm)],[74]) ).
thf(88,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) ) )
| ( ( B @ ( A @ difference ) )
!= c )
| ( c != b ) ),
inference(simp,[status(thm)],[75]) ).
thf(377,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( D @ ( C @ difference ) ) )
| ( ( E @ ( A @ difference ) )
= ( D @ ( E @ ( C @ difference ) @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,13]) ).
thf(378,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ difference ) @ ( A @ ( C @ difference ) @ difference ) )
= ( A @ ( C @ difference ) ) ),
inference(pattern_uni,[status(thm)],[377:[bind(A,$thf( G )),bind(B,$thf( F )),bind(C,$thf( G )),bind(D,$thf( G @ ( F @ difference ) ))]]) ).
thf(535,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ difference ) @ ( A @ ( C @ difference ) @ difference ) )
= ( A @ ( C @ difference ) ) ),
inference(simp,[status(thm)],[378]) ).
thf(5042,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( C @ ( b @ difference ) @ ( b @ difference ) @ ( C @ difference ) ) )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[9,4153]) ).
thf(5085,plain,
! [B: $i,A: $i] :
( ( ( c @ ( A @ difference ) )
!= ( B @ ( b @ difference ) @ ( b @ difference ) ) )
| ( c != B ) ),
inference(simp,[status(thm)],[5042]) ).
thf(5111,plain,
! [A: $i] :
( ( c @ ( A @ difference ) )
!= ( c @ ( b @ difference ) @ ( b @ difference ) ) ),
inference(simp,[status(thm)],[5085]) ).
thf(5915,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( c @ ( C @ difference ) ) )
| ( A
!= ( c @ ( b @ difference ) @ ( b @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,5111]) ).
thf(5988,plain,
! [B: $i,A: $i] :
( ( ( c @ ( b @ difference ) @ ( b @ difference ) @ ( A @ difference ) )
!= c )
| ( ( c @ ( b @ difference ) @ ( b @ difference ) )
!= B ) ),
inference(simp,[status(thm)],[5915]) ).
thf(6057,plain,
! [A: $i] :
( ( c @ ( b @ difference ) @ ( b @ difference ) @ ( A @ difference ) )
!= c ),
inference(simp,[status(thm)],[5988]) ).
thf(6564,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ difference ) @ ( A @ ( C @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) @ ( b @ difference ) @ ( D @ difference ) ) )
| ( ( A @ ( C @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[535,6057]) ).
thf(6565,plain,
! [A: $i] :
( ( A @ ( c @ ( b @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[6564:[bind(A,$thf( F )),bind(B,$thf( b )),bind(C,$thf( c @ ( b @ difference ) )),bind(D,$thf( F @ ( c @ ( b @ difference ) @ difference ) ))]]) ).
thf(6613,plain,
! [A: $i] :
( ( A @ ( c @ ( b @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[6565]) ).
thf(6646,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( A @ difference ) )
!= ( C @ ( c @ ( b @ difference ) @ difference ) ) )
| ( ( A @ ( B @ difference ) @ ( B @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[11,6613]) ).
thf(6647,plain,
! [A: $i] :
( ( c @ ( b @ difference ) @ ( A @ difference ) @ ( A @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[6646:[bind(A,$thf( c @ ( b @ difference ) )),bind(B,$thf( G )),bind(C,$thf( G @ ( c @ ( b @ difference ) @ difference ) ))]]) ).
thf(6679,plain,
! [A: $i] :
( ( c @ ( b @ difference ) @ ( A @ difference ) @ ( A @ difference ) )
!= c ),
inference(simp,[status(thm)],[6647]) ).
thf(8043,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( A @ difference ) )
!= ( c @ ( b @ difference ) @ ( C @ difference ) @ ( C @ difference ) ) )
| ( ( A @ ( B @ difference ) @ ( B @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[11,6679]) ).
thf(8044,plain,
! [A: $i] :
( ( A @ ( c @ ( b @ difference ) @ difference ) @ ( c @ ( b @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[8043:[bind(A,$thf( A )),bind(B,$thf( c @ ( b @ difference ) )),bind(C,$thf( A ))]]) ).
thf(649,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( D @ ( E @ difference ) ) )
| ( ( F @ ( B @ ( C @ ( A @ difference ) @ difference ) @ difference ) @ ( D @ difference ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[13,532]) ).
thf(650,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ ( A @ ( C @ difference ) @ difference ) @ difference ) @ ( A @ difference ) )
= A ),
inference(pattern_uni,[status(thm)],[649:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( C )),bind(E,$thf( H @ ( G @ difference ) ))]]) ).
thf(735,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ ( A @ ( C @ difference ) @ difference ) @ difference ) @ ( A @ difference ) )
= A ),
inference(simp,[status(thm)],[650]) ).
thf(4161,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( D @ ( A @ ( C @ difference ) @ difference ) @ difference ) @ ( A @ difference ) )
!= ( b @ ( F @ difference ) @ ( E @ difference ) ) )
| ( ( A @ ( E @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[735,1756]) ).
thf(4162,plain,
! [A: $i] :
( ( A @ ( A @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[4161:[bind(A,$thf( J )),bind(B,$thf( b )),bind(C,$thf( I )),bind(D,$thf( H )),bind(E,$thf( J )),bind(F,$thf( H @ ( J @ ( I @ difference ) @ difference ) ))]]) ).
thf(4174,plain,
! [A: $i] :
( ( A @ ( A @ difference ) )
!= c ),
inference(simp,[status(thm)],[4162]) ).
thf(4234,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ ( B @ difference ) @ difference ) @ ( A @ difference ) )
!= ( D @ ( D @ difference ) ) )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[532,4174]) ).
thf(4244,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( c @ ( A @ difference ) @ difference ) )
!= C )
| ( c != C ) ),
inference(simp,[status(thm)],[4234]) ).
thf(4253,plain,
! [B: $i,A: $i] :
( ( B @ ( c @ ( A @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[4244]) ).
thf(4298,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( C @ difference ) ) )
| ( ( D @ ( B @ ( A @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[28,4253]) ).
thf(4299,plain,
! [B: $i,A: $i] :
( ( A @ ( c @ ( B @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[4298:[bind(A,$thf( E )),bind(B,$thf( c )),bind(C,$thf( c @ ( E @ difference ) )),bind(D,$thf( D ))]]) ).
thf(4339,plain,
! [B: $i,A: $i] :
( ( A @ ( c @ ( B @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[4299]) ).
thf(4310,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= ( E @ ( c @ ( D @ difference ) @ difference ) ) )
| ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[13,4253]) ).
thf(4311,plain,
! [B: $i,A: $i] :
( ( c @ ( B @ ( A @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[4310:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( c )),bind(D,$thf( A )),bind(E,$thf( B ))]]) ).
thf(154,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( B @ difference ) )
!= ( c @ ( b @ difference ) ) )
| ( ( B @ ( A @ difference ) @ ( A @ difference ) @ ( c @ ( a @ difference ) @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[11,7]) ).
thf(202,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( B @ difference ) )
!= ( c @ ( b @ difference ) ) )
| ( ( B @ ( A @ difference ) @ ( A @ difference ) )
!= c )
| ( ( c @ ( a @ difference ) )
!= ( b @ ( a @ difference ) ) ) ),
inference(simp,[status(thm)],[154]) ).
thf(6637,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( D @ ( c @ ( b @ difference ) @ difference ) ) )
| ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[13,6613]) ).
thf(6638,plain,
! [A: $i] :
( ( c @ ( A @ ( b @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[6637:[bind(A,$thf( b )),bind(B,$thf( c )),bind(C,$thf( C )),bind(D,$thf( C ))]]) ).
thf(6677,plain,
! [A: $i] :
( ( c @ ( A @ ( b @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[6638]) ).
thf(6698,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( A @ difference ) )
!= ( C @ ( b @ difference ) ) )
| ( ( c @ ( A @ ( B @ difference ) @ ( B @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[11,6677]) ).
thf(6699,plain,
! [A: $i] :
( ( c @ ( b @ ( A @ difference ) @ ( A @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[6698:[bind(A,$thf( b )),bind(B,$thf( E )),bind(C,$thf( E @ ( b @ difference ) ))]]) ).
thf(6732,plain,
! [A: $i] :
( ( c @ ( b @ ( A @ difference ) @ ( A @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[6699]) ).
thf(1708,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ difference ) @ difference ) )
!= ( b @ ( C @ difference ) ) )
| ( ( D @ ( B @ ( A @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[28,1662]) ).
thf(1709,plain,
! [B: $i,A: $i] :
( ( A @ ( b @ ( B @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[1708:[bind(A,$thf( E )),bind(B,$thf( b )),bind(C,$thf( b @ ( E @ difference ) )),bind(D,$thf( D ))]]) ).
thf(1750,plain,
! [B: $i,A: $i] :
( ( A @ ( b @ ( B @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[1709]) ).
thf(4147,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ difference ) @ ( A @ ( C @ difference ) @ difference ) )
!= ( b @ ( E @ difference ) @ ( D @ difference ) ) )
| ( ( A @ ( C @ difference ) @ ( D @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[535,1756]) ).
thf(4148,plain,
! [A: $i] :
( ( A @ ( b @ difference ) @ ( A @ ( b @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[4147:[bind(A,$thf( G )),bind(B,$thf( B )),bind(C,$thf( b )),bind(D,$thf( G @ ( b @ difference ) )),bind(E,$thf( B ))]]) ).
thf(4195,plain,
! [A: $i] :
( ( A @ ( b @ difference ) @ ( A @ ( b @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[4148]) ).
thf(7914,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ difference ) @ ( A @ difference ) )
!= ( C @ ( b @ difference ) ) )
| ( ( C @ ( b @ difference ) @ ( A @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[4642,4195]) ).
thf(7915,plain,
! [A: $i] :
( ( A @ ( A @ difference ) @ ( b @ difference ) @ ( b @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[7914:[bind(A,$thf( b )),bind(B,$thf( E )),bind(C,$thf( E @ ( E @ difference ) ))]]) ).
thf(7949,plain,
! [A: $i] :
( ( A @ ( A @ difference ) @ ( b @ difference ) @ ( b @ difference ) )
!= c ),
inference(simp,[status(thm)],[7915]) ).
thf(37,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( a @ difference ) ) )
| ( ( c @ ( b @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,7]) ).
thf(57,plain,
! [B: $i,A: $i] :
( ( B != c )
| ( ( B @ ( A @ difference ) )
!= a )
| ( ( c @ ( b @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(simp,[status(thm)],[37]) ).
thf(67,plain,
! [A: $i] :
( ( ( c @ ( A @ difference ) )
!= a )
| ( ( c @ ( b @ difference ) @ ( c @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(simp,[status(thm)],[57]) ).
thf(12413,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) @ ( c @ ( C @ difference ) @ difference ) ) )
| ( ( c @ ( C @ difference ) )
!= a )
| ( ( B @ ( B @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[12197,67]) ).
thf(12414,plain,
( ( ( c @ ( b @ difference ) )
!= a )
| ( ( c @ ( b @ ( a @ difference ) @ difference ) )
!= ( c @ ( c @ difference ) ) ) ),
inference(pattern_uni,[status(thm)],[12413:[bind(A,$thf( b )),bind(B,$thf( c )),bind(C,$thf( b ))]]) ).
thf(14732,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) )
| ( ( c @ ( b @ difference ) )
!= a )
| ( ( B @ ( A @ difference ) )
!= ( c @ ( c @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,12414]) ).
thf(14800,plain,
! [B: $i,A: $i] :
( ( B != c )
| ( ( B @ ( A @ difference ) )
!= ( b @ ( a @ difference ) ) )
| ( ( c @ ( b @ difference ) )
!= a )
| ( B != c )
| ( A != c ) ),
inference(simp,[status(thm)],[14732]) ).
thf(14952,plain,
( ( ( c @ ( c @ difference ) )
!= ( b @ ( a @ difference ) ) )
| ( ( c @ ( b @ difference ) )
!= a ) ),
inference(simp,[status(thm)],[14800]) ).
thf(15175,plain,
( ( c != b )
| ( c != a )
| ( ( c @ ( b @ difference ) )
!= a ) ),
inference(simp,[status(thm)],[14952]) ).
thf(6818,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ difference ) @ ( A @ difference ) )
!= ( C @ ( D @ difference ) ) )
| ( ( A @ ( C @ difference ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[4642,9]) ).
thf(6819,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( B @ difference ) @ difference ) )
= ( B @ ( B @ difference ) ) ),
inference(pattern_uni,[status(thm)],[6818:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( F @ ( F @ difference ) )),bind(D,$thf( A ))]]) ).
thf(7121,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( B @ difference ) @ difference ) )
= ( B @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[6819]) ).
thf(18525,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ difference ) @ difference ) )
!= ( c @ ( D @ difference ) ) )
| ( ( C @ ( B @ ( B @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[7121,4339]) ).
thf(18526,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( B @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[18525:[bind(A,$thf( c )),bind(B,$thf( F )),bind(C,$thf( C )),bind(D,$thf( F @ ( F @ difference ) ))]]) ).
thf(19191,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( B @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[18526]) ).
thf(2168,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ difference ) @ ( A @ ( C @ difference ) @ difference ) )
!= ( E @ ( D @ difference ) ) )
| ( ( c @ ( A @ ( C @ difference ) @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[535,1767]) ).
thf(2169,plain,
! [B: $i,A: $i] :
( ( c @ ( A @ ( B @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[2168:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( I )),bind(D,$thf( G @ ( I @ difference ) )),bind(E,$thf( I @ ( H @ difference ) ))]]) ).
thf(2216,plain,
! [B: $i,A: $i] :
( ( c @ ( A @ ( B @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[2169]) ).
thf(1660,plain,
! [B: $i,A: $i] :
( ( ( c @ ( A @ difference ) )
!= b )
| ( c != B ) ),
inference(simp,[status(thm)],[1642]) ).
thf(1672,plain,
! [A: $i] :
( ( c @ ( A @ difference ) )
!= b ),
inference(simp,[status(thm)],[1660]) ).
thf(1684,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( D @ ( A @ ( C @ difference ) @ difference ) @ difference ) @ ( A @ difference ) )
!= ( c @ ( E @ difference ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[735,1672]) ).
thf(1691,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( b @ ( B @ difference ) @ difference ) @ difference ) )
!= c )
| ( b != D ) ),
inference(simp,[status(thm)],[1684]) ).
thf(1703,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( b @ ( B @ difference ) @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[1691]) ).
thf(1714,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= ( E @ ( b @ ( D @ difference ) @ difference ) ) )
| ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[13,1662]) ).
thf(1715,plain,
! [B: $i,A: $i] :
( ( b @ ( B @ ( A @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[1714:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( b )),bind(D,$thf( A )),bind(E,$thf( B ))]]) ).
thf(12331,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
!= ( D @ ( C @ difference ) ) )
| ( ( b @ ( B @ ( B @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[12197,1715]) ).
thf(12332,plain,
! [A: $i] :
( ( b @ ( A @ ( A @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[12331:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( H @ ( G @ difference ) )),bind(D,$thf( H @ ( G @ difference ) ))]]) ).
thf(12843,plain,
! [A: $i] :
( ( b @ ( A @ ( A @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[12332]) ).
thf(13537,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( b @ ( D @ ( D @ difference ) @ difference ) ) )
| ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[13,12843]) ).
thf(13538,plain,
! [A: $i] :
( ( A @ ( b @ ( A @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[13537:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( b )),bind(D,$thf( B ))]]) ).
thf(13597,plain,
! [A: $i] :
( ( A @ ( b @ ( A @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[13538]) ).
thf(16569,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( C @ ( b @ ( C @ difference ) @ difference ) ) )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[9,13597]) ).
thf(16605,plain,
! [B: $i,A: $i] :
( ( ( c @ ( A @ difference ) )
!= B )
| ( ( b @ ( B @ difference ) )
!= c ) ),
inference(simp,[status(thm)],[16569]) ).
thf(16636,plain,
! [A: $i] :
( ( b @ ( c @ ( A @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[16605]) ).
thf(136,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( A @ difference ) )
!= ( C @ ( D @ difference ) ) )
| ( ( A @ ( B @ difference ) @ ( B @ difference ) @ ( C @ difference ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[11,9]) ).
thf(137,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ difference ) @ ( B @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
= ( B @ ( A @ difference ) ) ),
inference(pattern_uni,[status(thm)],[136:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ difference ) )),bind(D,$thf( E ))]]) ).
thf(209,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ difference ) @ ( B @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
= ( B @ ( A @ difference ) ) ),
inference(simp,[status(thm)],[137]) ).
thf(13663,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( B @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) @ ( b @ difference ) @ ( C @ difference ) ) )
| ( ( B @ ( A @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[209,6057]) ).
thf(13664,plain,
( ( b @ ( c @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[13663:[bind(A,$thf( c )),bind(B,$thf( b )),bind(C,$thf( b @ ( c @ difference ) ))]]) ).
thf(7417,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= ( E @ ( b @ ( D @ difference ) @ difference ) ) )
| ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[13,7347]) ).
thf(7418,plain,
! [B: $i,A: $i] :
( ( b @ ( B @ ( A @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[7417:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( b )),bind(D,$thf( A )),bind(E,$thf( B ))]]) ).
thf(16671,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( b @ ( c @ ( D @ difference ) @ difference ) ) )
| ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[13,16636]) ).
thf(16672,plain,
! [A: $i] :
( ( c @ ( b @ ( A @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[16671:[bind(A,$thf( A )),bind(B,$thf( c )),bind(C,$thf( b )),bind(D,$thf( A ))]]) ).
thf(12222,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
!= ( D @ ( C @ difference ) ) )
| ( ( c @ ( B @ ( B @ difference ) @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[12197,1767]) ).
thf(12223,plain,
! [A: $i] :
( ( c @ ( A @ ( A @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[12222:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( H @ ( G @ difference ) )),bind(D,$thf( H @ ( G @ difference ) ))]]) ).
thf(13111,plain,
! [A: $i] :
( ( c @ ( A @ ( A @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[12223]) ).
thf(15401,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( D @ ( D @ difference ) @ difference ) ) )
| ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[13,13111]) ).
thf(15402,plain,
! [A: $i] :
( ( A @ ( c @ ( A @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[15401:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( c )),bind(D,$thf( B ))]]) ).
thf(15477,plain,
! [A: $i] :
( ( A @ ( c @ ( A @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[15402]) ).
thf(156,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( A @ difference ) )
!= ( D @ ( C @ difference ) ) )
| ( ( A @ ( B @ difference ) @ ( B @ difference ) @ ( C @ difference ) )
= ( C @ ( D @ difference ) @ ( D @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[11,11]) ).
thf(157,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ difference ) @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
= ( A @ ( B @ difference ) @ ( B @ difference ) @ ( A @ difference ) ) ),
inference(pattern_uni,[status(thm)],[156:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ difference ) ))]]) ).
thf(215,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ difference ) @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
= ( A @ ( B @ difference ) @ ( B @ difference ) @ ( A @ difference ) ) ),
inference(simp,[status(thm)],[157]) ).
thf(16953,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ difference ) @ ( B @ difference ) @ ( A @ difference ) )
= ( B @ ( A @ difference ) ) ),
inference(rewrite,[status(thm)],[215,535]) ).
thf(17203,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( B @ difference ) @ ( A @ difference ) )
!= ( c @ ( b @ difference ) @ ( b @ difference ) ) )
| ( ( B @ ( A @ difference ) )
!= ( c @ ( C @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[16953,5111]) ).
thf(17482,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( B @ difference ) )
!= ( c @ ( b @ difference ) ) )
| ( A != b )
| ( B != c )
| ( A != C ) ),
inference(simp,[status(thm)],[17203]) ).
thf(17764,plain,
( ( b @ ( c @ difference ) @ ( c @ difference ) )
!= ( c @ ( b @ difference ) ) ),
inference(simp,[status(thm)],[17482]) ).
thf(18128,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( B @ difference ) @ ( A @ difference ) )
!= ( b @ ( c @ difference ) @ ( c @ difference ) ) )
| ( ( B @ ( A @ difference ) )
!= ( c @ ( b @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[16953,17764]) ).
thf(18228,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( B @ difference ) )
!= ( b @ ( c @ difference ) ) )
| ( A != c )
| ( B != c )
| ( A != b ) ),
inference(simp,[status(thm)],[18128]) ).
thf(18278,plain,
( ( ( b @ ( c @ difference ) @ ( c @ difference ) )
!= ( b @ ( c @ difference ) ) )
| ( c != b ) ),
inference(simp,[status(thm)],[18228]) ).
thf(18332,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( A @ difference ) )
!= ( b @ ( c @ difference ) @ ( c @ difference ) ) )
| ( ( A @ ( B @ difference ) @ ( B @ difference ) )
!= ( b @ ( c @ difference ) ) )
| ( c != b ) ),
inference(paramod_ordered,[status(thm)],[11,18278]) ).
thf(18333,plain,
( ( ( b @ ( c @ difference ) )
!= ( c @ ( b @ difference ) @ ( b @ difference ) ) )
| ( c != b ) ),
inference(pattern_uni,[status(thm)],[18332:[bind(A,$thf( c )),bind(B,$thf( b ))]]) ).
thf(6243,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ difference ) @ ( A @ ( C @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) @ ( c @ ( D @ difference ) @ difference ) ) )
| ( ( c @ ( D @ difference ) )
!= a )
| ( ( A @ ( C @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[535,67]) ).
thf(6244,plain,
( ( ( c @ ( c @ difference ) )
!= a )
| ( ( c @ ( b @ ( a @ difference ) @ difference ) )
!= ( c @ ( c @ difference ) ) ) ),
inference(pattern_uni,[status(thm)],[6243:[bind(A,$thf( c )),bind(B,$thf( b )),bind(C,$thf( c )),bind(D,$thf( c ))]]) ).
thf(8154,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) )
| ( ( c @ ( c @ difference ) )
!= a )
| ( ( B @ ( A @ difference ) )
!= ( c @ ( c @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,6244]) ).
thf(8186,plain,
! [B: $i,A: $i] :
( ( B != c )
| ( ( B @ ( A @ difference ) )
!= ( b @ ( a @ difference ) ) )
| ( ( c @ ( c @ difference ) )
!= a )
| ( B != c )
| ( A != c ) ),
inference(simp,[status(thm)],[8154]) ).
thf(8358,plain,
( ( ( c @ ( c @ difference ) )
!= ( b @ ( a @ difference ) ) )
| ( ( c @ ( c @ difference ) )
!= a ) ),
inference(simp,[status(thm)],[8186]) ).
thf(9418,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( c @ ( c @ difference ) ) )
| ( ( c @ ( c @ difference ) )
!= ( b @ ( a @ difference ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[9,8358]) ).
thf(9463,plain,
! [A: $i] :
( ( ( a @ ( A @ difference ) )
!= c )
| ( c != a )
| ( c != b )
| ( c != a ) ),
inference(simp,[status(thm)],[9418]) ).
thf(9556,plain,
! [A: $i] :
( ( ( a @ ( A @ difference ) )
!= c )
| ( c != b )
| ( c != a ) ),
inference(simp,[status(thm)],[9463]) ).
thf(10292,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) @ ( b @ difference ) ) )
| ( ( B @ ( A @ difference ) )
!= ( C @ ( C @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,7201]) ).
thf(10332,plain,
! [C: $i,B: $i,A: $i] :
( ( B
!= ( c @ ( b @ difference ) ) )
| ( ( B @ ( A @ difference ) )
!= b )
| ( B != C )
| ( A != C ) ),
inference(simp,[status(thm)],[10292]) ).
thf(10448,plain,
( ( c @ ( b @ difference ) @ ( c @ ( b @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[10332]) ).
thf(12200,plain,
( ( c @ ( c @ difference ) )
!= b ),
inference(rewrite,[status(thm)],[10448,12197]) ).
thf(9687,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( A @ difference ) )
!= ( b @ ( C @ difference ) @ ( C @ difference ) ) )
| ( ( c @ ( A @ ( B @ difference ) @ ( B @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[11,6732]) ).
thf(9688,plain,
! [A: $i] :
( ( c @ ( A @ ( b @ difference ) @ ( b @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[9687:[bind(A,$thf( A )),bind(B,$thf( b )),bind(C,$thf( A ))]]) ).
thf(7323,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( C @ ( C @ difference ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[9,7160]) ).
thf(7341,plain,
! [B: $i,A: $i] :
( ( ( b @ ( A @ difference ) )
!= B )
| ( b != B ) ),
inference(simp,[status(thm)],[7323]) ).
thf(7353,plain,
! [A: $i] :
( ( b @ ( A @ difference ) )
!= b ),
inference(simp,[status(thm)],[7341]) ).
thf(18509,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ difference ) @ difference ) )
!= ( c @ ( C @ difference ) ) )
| ( ( D @ ( B @ ( B @ difference ) @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[7121,1665]) ).
thf(18510,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( B @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[18509:[bind(A,$thf( c )),bind(B,$thf( F )),bind(C,$thf( F @ ( F @ difference ) )),bind(D,$thf( D ))]]) ).
thf(19186,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( B @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[18510]) ).
thf(19999,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= ( D @ ( E @ ( E @ difference ) @ difference ) ) )
| ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[13,19186]) ).
thf(20000,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[19999:[bind(A,$thf( C )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( B )),bind(E,$thf( C ))]]) ).
thf(20065,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[20000]) ).
thf(7639,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ difference ) @ ( A @ ( C @ difference ) @ difference ) )
!= ( E @ ( D @ difference ) ) )
| ( ( b @ ( A @ ( C @ difference ) @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[535,7418]) ).
thf(7640,plain,
! [B: $i,A: $i] :
( ( b @ ( A @ ( B @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[7639:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( I )),bind(D,$thf( G @ ( I @ difference ) )),bind(E,$thf( I @ ( H @ difference ) ))]]) ).
thf(7676,plain,
! [B: $i,A: $i] :
( ( b @ ( A @ ( B @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[7640]) ).
thf(12454,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
!= ( C @ ( D @ difference ) ) )
| ( ( b @ ( B @ ( B @ difference ) @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[12197,7676]) ).
thf(12455,plain,
! [A: $i] :
( ( b @ ( A @ ( A @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[12454:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( H @ ( G @ difference ) )),bind(D,$thf( H @ ( G @ difference ) ))]]) ).
thf(12866,plain,
! [A: $i] :
( ( b @ ( A @ ( A @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[12455]) ).
thf(9780,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( D @ ( b @ difference ) @ ( b @ difference ) @ difference ) ) )
| ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[13,9688]) ).
thf(9781,plain,
! [A: $i] :
( ( A @ ( b @ difference ) @ ( c @ ( b @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[9780:[bind(A,$thf( b )),bind(B,$thf( F @ ( b @ difference ) )),bind(C,$thf( c )),bind(D,$thf( F ))]]) ).
thf(9872,plain,
! [A: $i] :
( ( A @ ( b @ difference ) @ ( c @ ( b @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[9781]) ).
thf(152,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( A @ difference ) )
!= ( c @ ( b @ difference ) @ ( c @ ( a @ difference ) @ difference ) ) )
| ( ( A @ ( B @ difference ) @ ( B @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[11,7]) ).
thf(175,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ difference ) )
!= ( c @ ( b @ difference ) ) )
| ( A
!= ( c @ ( a @ difference ) ) )
| ( ( A @ ( B @ difference ) @ ( B @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(simp,[status(thm)],[152]) ).
thf(225,plain,
! [A: $i] :
( ( ( A @ ( c @ ( a @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) ) )
| ( ( c @ ( a @ difference ) @ ( A @ difference ) @ ( A @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(simp,[status(thm)],[175]) ).
thf(144,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( D @ ( C @ difference ) ) )
| ( ( A @ ( C @ difference ) )
= ( C @ ( D @ difference ) @ ( D @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,11]) ).
thf(145,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ difference ) @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
= ( B @ ( B @ difference ) ) ),
inference(pattern_uni,[status(thm)],[144:[bind(A,$thf( F )),bind(B,$thf( E )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ difference ) ))]]) ).
thf(212,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ difference ) @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
= ( B @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[145]) ).
thf(19996,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( D @ ( E @ ( E @ difference ) @ difference ) ) )
| ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[13,19186]) ).
thf(19997,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[19996:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( C )),bind(E,$thf( B ))]]) ).
thf(20064,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[19997]) ).
thf(5907,plain,
! [A: $i] :
( ( ( c @ ( b @ difference ) )
!= c )
| ( A != b ) ),
inference(simp,[status(thm)],[5111]) ).
thf(6008,plain,
( ( c @ ( b @ difference ) )
!= c ),
inference(simp,[status(thm)],[5907]) ).
thf(6868,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ difference ) @ ( A @ difference ) )
!= ( c @ ( b @ difference ) ) )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[4642,6008]) ).
thf(6939,plain,
! [A: $i] :
( ( ( A @ ( A @ difference ) )
!= c )
| ( c != b ) ),
inference(simp,[status(thm)],[6868]) ).
thf(7150,plain,
! [A: $i] :
( ( ( A @ ( A @ difference ) )
!= c )
| ( c != b ) ),
inference(simp,[status(thm)],[6939]) ).
thf(4235,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( C @ ( C @ difference ) ) )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[9,4174]) ).
thf(4247,plain,
! [B: $i,A: $i] :
( ( ( c @ ( A @ difference ) )
!= B )
| ( c != B ) ),
inference(simp,[status(thm)],[4235]) ).
thf(4256,plain,
! [A: $i] :
( ( c @ ( A @ difference ) )
!= c ),
inference(simp,[status(thm)],[4247]) ).
thf(4265,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( c @ ( C @ difference ) ) )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[9,4256]) ).
thf(4281,plain,
! [B: $i,A: $i] :
( ( c @ ( A @ difference ) @ ( c @ difference ) )
!= ( c @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[4265]) ).
thf(4293,plain,
! [B: $i,A: $i] :
( ( c @ ( A @ difference ) @ ( c @ difference ) )
!= ( c @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[4281]) ).
thf(7972,plain,
! [A: $i] :
( ( c @ ( A @ difference ) )
!= c ),
inference(rewrite,[status(thm)],[4293,9]) ).
thf(19672,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( C @ ( c @ ( C @ difference ) @ difference ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[9,15477]) ).
thf(19716,plain,
! [B: $i,A: $i] :
( ( ( b @ ( A @ difference ) )
!= B )
| ( ( c @ ( B @ difference ) )
!= b ) ),
inference(simp,[status(thm)],[19672]) ).
thf(19740,plain,
! [A: $i] :
( ( c @ ( b @ ( A @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[19716]) ).
thf(9050,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( D @ ( c @ ( b @ difference ) @ difference ) ) )
| ( ( B @ ( C @ ( A @ difference ) @ difference ) @ ( c @ ( b @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[13,8044]) ).
thf(9051,plain,
! [A: $i] :
( ( c @ ( A @ ( b @ difference ) @ difference ) @ ( c @ ( b @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[9050:[bind(A,$thf( b )),bind(B,$thf( c )),bind(C,$thf( C )),bind(D,$thf( C ))]]) ).
thf(9157,plain,
! [A: $i] :
( ( c @ ( A @ ( b @ difference ) @ difference ) @ ( c @ ( b @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[9051]) ).
thf(6926,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ difference ) @ ( A @ difference ) )
!= ( E @ ( D @ difference ) @ ( C @ difference ) ) )
| ( ( A @ ( C @ difference ) @ ( E @ difference ) )
= E ) ),
inference(paramod_ordered,[status(thm)],[4642,740]) ).
thf(6927,plain,
! [B: $i,A: $i] :
( ( A @ ( A @ difference ) @ ( B @ difference ) )
= B ),
inference(pattern_uni,[status(thm)],[6926:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B )),bind(E,$thf( B ))]]) ).
thf(1760,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( C @ difference ) ) )
| ( ( D @ ( B @ ( A @ difference ) @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[28,1665]) ).
thf(1761,plain,
! [B: $i,A: $i] :
( ( A @ ( c @ ( B @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[1760:[bind(A,$thf( E )),bind(B,$thf( c )),bind(C,$thf( c @ ( E @ difference ) )),bind(D,$thf( D ))]]) ).
thf(1795,plain,
! [B: $i,A: $i] :
( ( A @ ( c @ ( B @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[1761]) ).
thf(7408,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ difference ) @ difference ) )
!= ( b @ ( C @ difference ) ) )
| ( ( D @ ( B @ ( A @ difference ) @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[28,7347]) ).
thf(7409,plain,
! [B: $i,A: $i] :
( ( A @ ( b @ ( B @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[7408:[bind(A,$thf( E )),bind(B,$thf( b )),bind(C,$thf( b @ ( E @ difference ) )),bind(D,$thf( D ))]]) ).
thf(7455,plain,
! [B: $i,A: $i] :
( ( A @ ( b @ ( B @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[7409]) ).
thf(15004,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( b @ ( D @ ( D @ difference ) @ difference ) ) )
| ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[13,12866]) ).
thf(15005,plain,
! [A: $i] :
( ( A @ ( b @ ( A @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[15004:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( b )),bind(D,$thf( B ))]]) ).
thf(15068,plain,
! [A: $i] :
( ( A @ ( b @ ( A @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[15005]) ).
thf(21474,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ difference ) @ ( A @ ( C @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) @ ( D @ difference ) @ ( D @ difference ) ) )
| ( ( A @ ( C @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[535,10407]) ).
thf(21475,plain,
! [A: $i] :
( ( A @ ( c @ ( b @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[21474:[bind(A,$thf( H )),bind(B,$thf( H @ ( c @ ( b @ difference ) @ difference ) )),bind(C,$thf( c @ ( b @ difference ) )),bind(D,$thf( H @ ( c @ ( b @ difference ) @ difference ) ))]]) ).
thf(21575,plain,
! [A: $i] :
( ( A @ ( c @ ( b @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[21475]) ).
thf(1651,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( D @ ( A @ ( C @ difference ) @ difference ) @ difference ) @ ( A @ difference ) )
!= ( b @ ( E @ difference ) ) )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[735,1639]) ).
thf(1655,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( c @ ( B @ difference ) @ difference ) @ difference ) )
!= b )
| ( c != D ) ),
inference(simp,[status(thm)],[1651]) ).
thf(1667,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( c @ ( B @ difference ) @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[1655]) ).
thf(9611,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( a @ ( C @ difference ) ) )
| ( A != c )
| ( c != b )
| ( c != a ) ),
inference(paramod_ordered,[status(thm)],[9,9556]) ).
thf(9636,plain,
! [B: $i,A: $i] :
( ( ( c @ ( A @ difference ) )
!= a )
| ( c != B )
| ( c != b )
| ( c != a ) ),
inference(simp,[status(thm)],[9611]) ).
thf(9642,plain,
! [A: $i] :
( ( ( c @ ( A @ difference ) )
!= a )
| ( c != b )
| ( c != a ) ),
inference(simp,[status(thm)],[9636]) ).
thf(4791,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ difference ) @ ( A @ ( C @ difference ) @ difference ) )
!= ( E @ ( D @ difference ) ) )
| ( ( c @ ( A @ ( C @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[535,4311]) ).
thf(4792,plain,
! [B: $i,A: $i] :
( ( c @ ( A @ ( B @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[4791:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( I )),bind(D,$thf( G @ ( I @ difference ) )),bind(E,$thf( I @ ( H @ difference ) ))]]) ).
thf(4831,plain,
! [B: $i,A: $i] :
( ( c @ ( A @ ( B @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[4792]) ).
thf(12509,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
!= ( C @ ( D @ difference ) ) )
| ( ( c @ ( B @ ( B @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[12197,4831]) ).
thf(12510,plain,
! [A: $i] :
( ( c @ ( A @ ( A @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[12509:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( H @ ( G @ difference ) )),bind(D,$thf( H @ ( G @ difference ) ))]]) ).
thf(12880,plain,
! [A: $i] :
( ( c @ ( A @ ( A @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[12510]) ).
thf(15097,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( D @ ( D @ difference ) @ difference ) ) )
| ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[13,12880]) ).
thf(15098,plain,
! [A: $i] :
( ( A @ ( c @ ( A @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[15097:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( c )),bind(D,$thf( B ))]]) ).
thf(15173,plain,
! [A: $i] :
( ( A @ ( c @ ( A @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[15098]) ).
thf(38,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) ) )
| ( ( B @ ( A @ difference ) @ ( c @ ( a @ difference ) @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,7]) ).
thf(48,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) ) )
| ( ( B @ ( A @ difference ) )
!= c )
| ( ( c @ ( a @ difference ) )
!= ( b @ ( a @ difference ) ) ) ),
inference(simp,[status(thm)],[38]) ).
thf(39,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) @ ( c @ ( a @ difference ) @ difference ) ) )
| ( ( B @ ( A @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,7]) ).
thf(52,plain,
! [B: $i,A: $i] :
( ( B
!= ( c @ ( b @ difference ) ) )
| ( ( B @ ( A @ difference ) )
!= ( c @ ( a @ difference ) ) )
| ( ( B @ ( A @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(simp,[status(thm)],[39]) ).
thf(63,plain,
! [A: $i] :
( ( ( c @ ( b @ difference ) @ ( A @ difference ) )
!= ( c @ ( a @ difference ) ) )
| ( ( c @ ( b @ difference ) @ ( A @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(simp,[status(thm)],[52]) ).
thf(8023,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( c @ ( b @ difference ) @ ( C @ difference ) ) )
| ( ( A @ ( C @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[9,6679]) ).
thf(8024,plain,
( ( c @ ( c @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[8023:[bind(A,$thf( c )),bind(B,$thf( b )),bind(C,$thf( c ))]]) ).
thf(8118,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ difference ) @ ( A @ difference ) )
!= ( c @ ( c @ difference ) ) )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[4642,8024]) ).
thf(8120,plain,
! [A: $i] :
( ( A @ ( A @ difference ) @ ( c @ difference ) )
!= ( c @ ( c @ difference ) ) ),
inference(simp,[status(thm)],[8118]) ).
thf(8143,plain,
! [A: $i] :
( ( A @ ( A @ difference ) @ ( c @ difference ) )
!= ( c @ ( c @ difference ) ) ),
inference(simp,[status(thm)],[8120]) ).
thf(6938,plain,
! [A: $i] :
( ( A @ ( A @ difference ) @ ( c @ difference ) )
!= ( c @ ( b @ difference ) ) ),
inference(simp,[status(thm)],[6868]) ).
thf(7149,plain,
! [A: $i] :
( ( A @ ( A @ difference ) @ ( c @ difference ) )
!= ( c @ ( b @ difference ) ) ),
inference(simp,[status(thm)],[6938]) ).
thf(9413,plain,
( ( c != b )
| ( c != a )
| ( ( c @ ( c @ difference ) )
!= a ) ),
inference(simp,[status(thm)],[8358]) ).
thf(4132,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( b @ ( D @ difference ) @ ( C @ difference ) ) )
| ( ( A @ ( C @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[9,1756]) ).
thf(4133,plain,
( ( b @ ( b @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[4132:[bind(A,$thf( b )),bind(B,$thf( B )),bind(C,$thf( b )),bind(D,$thf( B ))]]) ).
thf(6886,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ difference ) @ ( A @ difference ) )
!= ( b @ ( b @ difference ) ) )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[4642,4133]) ).
thf(7108,plain,
! [A: $i] :
( ( A @ ( A @ difference ) @ ( c @ difference ) )
!= ( b @ ( b @ difference ) ) ),
inference(simp,[status(thm)],[6886]) ).
thf(7319,plain,
! [A: $i] :
( ( A @ ( A @ difference ) @ ( c @ difference ) )
!= ( b @ ( b @ difference ) ) ),
inference(simp,[status(thm)],[7108]) ).
thf(10287,plain,
! [A: $i] :
( ( A
!= ( c @ ( b @ difference ) ) )
| ( A != b ) ),
inference(simp,[status(thm)],[7201]) ).
thf(10439,plain,
( ( c @ ( b @ difference ) )
!= b ),
inference(simp,[status(thm)],[10287]) ).
thf(18791,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) @ ( b @ difference ) ) )
| ( ( B @ ( B @ difference ) )
!= ( c @ ( C @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[7121,5111]) ).
thf(19170,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) @ ( b @ difference ) ) )
| ( B != c )
| ( B != C ) ),
inference(simp,[status(thm)],[18791]) ).
thf(19531,plain,
! [A: $i] :
( ( A @ ( c @ ( c @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) @ ( b @ difference ) ) ),
inference(simp,[status(thm)],[19170]) ).
thf(20178,plain,
( ( c @ ( c @ difference ) )
!= ( c @ ( b @ difference ) @ ( b @ difference ) ) ),
inference(rewrite,[status(thm)],[19531,7121]) ).
thf(1683,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( c @ ( C @ difference ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[9,1672]) ).
thf(1687,plain,
! [B: $i,A: $i] :
( ( b @ ( A @ difference ) @ ( b @ difference ) )
!= ( c @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[1683]) ).
thf(1699,plain,
! [B: $i,A: $i] :
( ( b @ ( A @ difference ) @ ( b @ difference ) )
!= ( c @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[1687]) ).
thf(3398,plain,
! [A: $i] :
( ( c @ ( A @ difference ) )
!= b ),
inference(rewrite,[status(thm)],[1699,9]) ).
thf(10291,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ difference ) @ difference ) )
!= ( C @ ( C @ difference ) ) )
| ( ( B @ ( A @ difference ) )
!= ( c @ ( b @ difference ) @ ( b @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,7201]) ).
thf(10348,plain,
! [C: $i,B: $i,A: $i] :
( ( B != C )
| ( ( B @ ( A @ difference ) )
!= C )
| ( B
!= ( c @ ( b @ difference ) ) )
| ( A != b ) ),
inference(simp,[status(thm)],[10291]) ).
thf(10464,plain,
( ( c @ ( b @ difference ) @ ( b @ difference ) )
!= ( c @ ( b @ difference ) ) ),
inference(simp,[status(thm)],[10348]) ).
thf(12269,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
!= ( E @ ( b @ ( D @ difference ) @ difference ) ) )
| ( ( C @ ( B @ ( B @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[12197,1703]) ).
thf(12270,plain,
! [A: $i] :
( ( A @ ( b @ ( b @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[12269:[bind(A,$thf( F )),bind(B,$thf( b )),bind(C,$thf( C )),bind(D,$thf( F )),bind(E,$thf( b @ ( F @ difference ) ))]]) ).
thf(13120,plain,
! [A: $i] :
( ( A @ ( b @ ( b @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[12270]) ).
thf(13303,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( D @ ( b @ ( b @ difference ) @ difference ) ) )
| ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[13,13120]) ).
thf(13304,plain,
! [A: $i] :
( ( b @ ( A @ ( b @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[13303:[bind(A,$thf( b )),bind(B,$thf( b )),bind(C,$thf( C )),bind(D,$thf( C ))]]) ).
thf(13357,plain,
! [A: $i] :
( ( b @ ( A @ ( b @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[13304]) ).
thf(1817,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ difference ) @ ( A @ ( C @ difference ) @ difference ) )
!= ( E @ ( D @ difference ) ) )
| ( ( b @ ( A @ ( C @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[535,1715]) ).
thf(1818,plain,
! [B: $i,A: $i] :
( ( b @ ( A @ ( B @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[1817:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( I )),bind(D,$thf( G @ ( I @ difference ) )),bind(E,$thf( I @ ( H @ difference ) ))]]) ).
thf(1866,plain,
! [B: $i,A: $i] :
( ( b @ ( A @ ( B @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[1818]) ).
thf(7361,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( b @ ( C @ difference ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[9,7353]) ).
thf(7374,plain,
! [B: $i,A: $i] :
( ( b @ ( A @ difference ) @ ( b @ difference ) )
!= ( b @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[7361]) ).
thf(7390,plain,
! [B: $i,A: $i] :
( ( b @ ( A @ difference ) @ ( b @ difference ) )
!= ( b @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[7374]) ).
thf(11412,plain,
! [A: $i] :
( ( b @ ( A @ difference ) )
!= b ),
inference(rewrite,[status(thm)],[7390,9]) ).
thf(7916,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ difference ) @ ( A @ difference ) )
!= ( C @ ( b @ difference ) ) )
| ( ( A @ ( C @ ( b @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[4642,4195]) ).
thf(7917,plain,
! [A: $i] :
( ( b @ ( A @ ( A @ difference ) @ ( b @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[7916:[bind(A,$thf( b )),bind(B,$thf( E )),bind(C,$thf( E @ ( E @ difference ) ))]]) ).
thf(7950,plain,
! [A: $i] :
( ( b @ ( A @ ( A @ difference ) @ ( b @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[7917]) ).
thf(9667,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ ( D @ difference ) @ ( D @ difference ) @ difference ) ) )
| ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[13,6732]) ).
thf(9668,plain,
! [A: $i] :
( ( b @ ( A @ difference ) @ ( c @ ( A @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[9667:[bind(A,$thf( E )),bind(B,$thf( b @ ( E @ difference ) )),bind(C,$thf( c )),bind(D,$thf( E ))]]) ).
thf(9736,plain,
! [A: $i] :
( ( b @ ( A @ difference ) @ ( c @ ( A @ difference ) @ difference ) )
!= c ),
inference(simp,[status(thm)],[9668]) ).
thf(17,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( c @ ( b @ difference ) @ ( c @ ( a @ difference ) @ difference ) ) )
| ( A
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,7]) ).
thf(27,plain,
! [A: $i] :
( ( ( c @ ( b @ ( a @ difference ) @ difference ) @ ( A @ difference ) )
!= ( c @ ( b @ difference ) ) )
| ( ( c @ ( b @ ( a @ difference ) @ difference ) )
!= ( c @ ( a @ difference ) ) ) ),
inference(simp,[status(thm)],[17]) ).
thf(36,plain,
! [A: $i] :
( ( ( c @ ( b @ ( a @ difference ) @ difference ) @ ( A @ difference ) )
!= ( c @ ( b @ difference ) ) )
| ( ( c @ ( b @ ( a @ difference ) @ difference ) )
!= ( c @ ( a @ difference ) ) ) ),
inference(simp,[status(thm)],[27]) ).
thf(15,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( A @ difference ) )
!= ( c @ ( a @ difference ) ) )
| ( ( c @ ( b @ difference ) @ ( A @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,7]) ).
thf(21,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ difference ) )
!= c )
| ( A != a )
| ( ( c @ ( b @ difference ) @ ( A @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(simp,[status(thm)],[15]) ).
thf(30,plain,
! [A: $i] :
( ( ( a @ ( A @ difference ) )
!= c )
| ( ( c @ ( b @ ( a @ difference ) @ difference ) )
!= ( c @ ( b @ difference ) @ ( a @ difference ) ) ) ),
inference(simp,[status(thm)],[21]) ).
thf(151,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( A @ difference ) )
!= ( c @ ( b @ difference ) ) )
| ( ( A @ ( B @ difference ) @ ( B @ difference ) @ ( c @ ( a @ difference ) @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[11,7]) ).
thf(190,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( A @ difference ) )
!= ( c @ ( b @ difference ) ) )
| ( ( A @ ( B @ difference ) @ ( B @ difference ) )
!= c )
| ( ( c @ ( a @ difference ) )
!= ( b @ ( a @ difference ) ) ) ),
inference(simp,[status(thm)],[151]) ).
thf(21598,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( D @ ( c @ ( b @ difference ) @ difference ) ) )
| ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[13,21575]) ).
thf(21599,plain,
! [A: $i] :
( ( c @ ( A @ ( b @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[21598:[bind(A,$thf( b )),bind(B,$thf( c )),bind(C,$thf( C )),bind(D,$thf( C ))]]) ).
thf(21666,plain,
! [A: $i] :
( ( c @ ( A @ ( b @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[21599]) ).
thf(9953,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ ( B @ difference ) @ difference ) @ ( A @ difference ) )
!= ( D @ ( b @ difference ) ) )
| ( ( A @ ( c @ ( b @ difference ) @ difference ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[532,9872]) ).
thf(9954,plain,
( ( b @ ( c @ ( b @ difference ) @ difference ) )
!= c ),
inference(pattern_uni,[status(thm)],[9953:[bind(A,$thf( b )),bind(B,$thf( G )),bind(C,$thf( F )),bind(D,$thf( F @ ( b @ ( G @ difference ) @ difference ) ))]]) ).
thf(12375,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( B @ ( A @ difference ) @ difference ) )
!= ( E @ ( c @ ( D @ difference ) @ difference ) ) )
| ( ( C @ ( B @ ( B @ difference ) @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[12197,1667]) ).
thf(12376,plain,
! [A: $i] :
( ( A @ ( c @ ( c @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[12375:[bind(A,$thf( F )),bind(B,$thf( c )),bind(C,$thf( C )),bind(D,$thf( F )),bind(E,$thf( c @ ( F @ difference ) ))]]) ).
thf(12851,plain,
! [A: $i] :
( ( A @ ( c @ ( c @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[12376]) ).
thf(13235,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ difference ) @ difference ) )
!= ( D @ ( c @ ( c @ difference ) @ difference ) ) )
| ( ( B @ ( C @ ( A @ difference ) @ difference ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[13,12851]) ).
thf(13236,plain,
! [A: $i] :
( ( c @ ( A @ ( c @ difference ) @ difference ) )
!= b ),
inference(pattern_uni,[status(thm)],[13235:[bind(A,$thf( c )),bind(B,$thf( c )),bind(C,$thf( C )),bind(D,$thf( C ))]]) ).
thf(13289,plain,
! [A: $i] :
( ( c @ ( A @ ( c @ difference ) @ difference ) )
!= b ),
inference(simp,[status(thm)],[13236]) ).
thf(7109,plain,
! [A: $i] :
( ( ( A @ ( A @ difference ) )
!= b )
| ( c != b ) ),
inference(simp,[status(thm)],[6886]) ).
thf(7320,plain,
! [A: $i] :
( ( ( A @ ( A @ difference ) )
!= b )
| ( c != b ) ),
inference(simp,[status(thm)],[7109]) ).
thf(153,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ difference ) @ ( B @ difference ) )
!= ( c @ ( a @ difference ) ) )
| ( ( c @ ( b @ difference ) @ ( B @ ( A @ difference ) @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[11,7]) ).
thf(172,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ difference ) )
!= c )
| ( B != a )
| ( ( c @ ( b @ difference ) @ ( B @ ( A @ difference ) @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(simp,[status(thm)],[153]) ).
thf(222,plain,
! [A: $i] :
( ( ( A @ ( a @ difference ) )
!= c )
| ( ( c @ ( b @ difference ) @ ( a @ ( A @ difference ) @ ( A @ difference ) @ difference ) )
!= ( c @ ( b @ ( a @ difference ) @ difference ) ) ) ),
inference(simp,[status(thm)],[172]) ).
thf(41693,plain,
$false,
inference(e,[status(thm)],[12362,10407,8,1665,1767,88,8044,4339,4311,5,202,6732,6057,1750,10,1756,7949,15175,19191,2216,1703,16636,12843,13664,12197,7418,16672,15477,16953,18333,4253,9556,12200,9688,7353,28,20065,3033,8358,6677,9,1672,12866,12414,19186,9872,225,212,13597,20064,13,1715,7150,7972,7160,19740,4256,9157,6927,1795,12,7201,7347,7455,15068,6613,21575,7,1667,535,9642,15173,1662,209,6008,17764,48,63,8143,5111,67,7149,9413,8024,7319,6244,10439,6679,20178,4133,11,3398,7676,10464,13357,1866,11412,7950,1639,12880,9736,14952,36,30,18278,735,7121,190,13111,532,740,21666,4831,9954,4642,13289,7320,222,4174]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG007-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.14/0.40 % Computer : n016.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Sat Sep 26 21:03:02 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.14/0.40 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.85/0.99 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.22/1.16 % [INFO] Parsing done (165ms).
% 1.22/1.18 % [INFO] Running in sequential loop mode.
% 1.76/1.57 % [INFO] eprover registered as external prover.
% 1.76/1.58 % [INFO] Scanning for conjecture ...
% 1.95/1.65 % [INFO] Found a conjecture (or negated_conjecture) and 3 axioms. Running axiom selection ...
% 1.95/1.68 % [INFO] Axiom selection finished. Selected 3 axioms (removed 0 axioms).
% 1.95/1.69 % [INFO] Problem is propositional (TPTP CNF).
% 2.12/1.70 % [INFO] Type checking passed.
% 2.12/1.70 % [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 ...
% 73.13/17.72 % External prover 'e' found a proof!
% 73.13/17.72 % [INFO] Killing All external provers ...
% 73.13/17.73 % Time passed: 17181ms (effective reasoning time: 16543ms)
% 73.13/17.73 % Axioms used in derivation (3): set_difference_1, set_difference_2, set_difference_3_simplified
% 73.13/17.73 % No. of inferences in proof: 340
% 73.13/17.73 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p : 17181 ms resp. 16543 ms w/o parsing
% 61.12/17.90 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 61.12/17.91 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------