%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : GRP670-1 : TPTP v9.3.1. Released v4.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 : n006.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:21:43 AM UTC 2026
% Result : Unsatisfiable 103.34s 30.36s
% Output : Refutation 91.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 10
% Syntax : Number of formulae : 159 ( 68 unt; 0 typ; 0 def)
% Number of atoms : 297 ( 296 equ; 0 cnn)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 1389 ( 219 ~; 138 |; 0 &;1032 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 10 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 203 ( 0 ^; 203 !; 0 ?; 203 :)
% Comments :
%------------------------------------------------------------------------------
thf(mult_decl,type,
mult: $i > $i > $i ).
thf(a_decl,type,
a: $i ).
thf(b_decl,type,
b: $i ).
thf(c_decl,type,
c: $i ).
thf(ld_decl,type,
ld: $i > $i > $i ).
thf(rd_decl,type,
rd: $i > $i > $i ).
thf(unit_decl,type,
unit: $i ).
thf(i_decl,type,
i: $i > $i ).
thf(6,axiom,
! [A: $i] :
( ( unit @ ( A @ mult ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c05) ).
thf(22,plain,
! [A: $i] :
( ( unit @ ( A @ mult ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(23,plain,
! [A: $i] :
( ( unit @ ( A @ mult ) )
= A ),
inference(lifteq,[status(thm)],[22]) ).
thf(8,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ mult ) @ ( A @ i @ mult ) )
= B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c07) ).
thf(26,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ mult ) @ ( A @ i @ mult ) )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(27,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ mult ) @ ( A @ i @ mult ) )
= B ),
inference(lifteq,[status(thm)],[26]) ).
thf(497,plain,
! [C: $i,B: $i,A: $i] :
( ( ( unit @ ( A @ mult ) )
!= ( C @ ( B @ mult ) ) )
| ( ( A @ ( B @ i @ mult ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[23,27]) ).
thf(498,plain,
! [A: $i] :
( ( A @ ( A @ i @ mult ) )
= unit ),
inference(pattern_uni,[status(thm)],[497:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( unit ))]]) ).
thf(9,axiom,
! [B: $i,A: $i] :
( ( B @ i @ ( B @ ( A @ mult ) @ mult ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c08) ).
thf(28,plain,
! [B: $i,A: $i] :
( ( B @ i @ ( B @ ( A @ mult ) @ mult ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(29,plain,
! [B: $i,A: $i] :
( ( B @ i @ ( B @ ( A @ mult ) @ mult ) )
= A ),
inference(lifteq,[status(thm)],[28]) ).
thf(3,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ mult ) @ ( A @ ld ) )
= B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c02) ).
thf(16,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ mult ) @ ( A @ ld ) )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(17,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ mult ) @ ( A @ ld ) )
= B ),
inference(lifteq,[status(thm)],[16]) ).
thf(810,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ i @ ( B @ ( A @ mult ) @ mult ) )
!= ( D @ ( C @ mult ) ) )
| ( ( A @ ( C @ ld ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[29,17]) ).
thf(811,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ mult ) @ ld ) )
= ( B @ i ) ),
inference(pattern_uni,[status(thm)],[810:[bind(A,$thf( E )),bind(B,$thf( G )),bind(C,$thf( G @ ( E @ mult ) )),bind(D,$thf( G @ i ))]]) ).
thf(892,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ mult ) @ ld ) )
= ( B @ i ) ),
inference(simp,[status(thm)],[811]) ).
thf(2,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ ld ) @ ( A @ mult ) )
= B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c01) ).
thf(14,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ld ) @ ( A @ mult ) )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(15,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ld ) @ ( A @ mult ) )
= B ),
inference(lifteq,[status(thm)],[14]) ).
thf(501,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( D @ ( C @ mult ) ) )
| ( ( B @ ( C @ i @ mult ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[15,27]) ).
thf(502,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ld ) )
= ( B @ ( A @ i @ mult ) ) ),
inference(pattern_uni,[status(thm)],[501:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ ld ) ))]]) ).
thf(586,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ld ) )
= ( B @ ( A @ i @ mult ) ) ),
inference(simp,[status(thm)],[502]) ).
thf(4610,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ mult ) @ i @ mult ) )
= ( B @ i ) ),
inference(rewrite,[status(thm)],[892,586]) ).
thf(4672,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( C @ ( B @ mult ) ) )
| ( ( B @ ( unit @ i @ mult ) )
= ( C @ i ) ) ),
inference(paramod_ordered,[status(thm)],[498,4610]) ).
thf(4673,plain,
! [A: $i] :
( ( A @ i @ ( unit @ i @ mult ) )
= ( A @ i ) ),
inference(pattern_uni,[status(thm)],[4672:[bind(A,$thf( D )),bind(B,$thf( D @ i )),bind(C,$thf( D ))]]) ).
thf(4892,plain,
! [A: $i] :
( ( A @ i @ ( unit @ i @ mult ) )
= ( A @ i ) ),
inference(simp,[status(thm)],[4673]) ).
thf(615,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( unit @ ( B @ mult ) ) )
| ( unit = B ) ),
inference(paramod_ordered,[status(thm)],[498,23]) ).
thf(616,plain,
( ( unit @ i )
= unit ),
inference(pattern_uni,[status(thm)],[615:[bind(A,$thf( unit )),bind(B,$thf( unit @ i ))]]) ).
thf(5028,plain,
! [A: $i] :
( ( A @ i @ ( unit @ mult ) )
= ( A @ i ) ),
inference(rewrite,[status(thm)],[4892,616]) ).
thf(7,axiom,
! [A: $i] :
( ( A @ ( unit @ mult ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c06) ).
thf(24,plain,
! [A: $i] :
( ( A @ ( unit @ mult ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(25,plain,
! [A: $i] :
( ( A @ ( unit @ mult ) )
= A ),
inference(lifteq,[status(thm)],[24]) ).
thf(805,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( C @ ( B @ mult ) ) )
| ( ( C @ i @ ( A @ mult ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[25,29]) ).
thf(806,plain,
! [A: $i] :
( ( A @ i @ ( A @ mult ) )
= unit ),
inference(pattern_uni,[status(thm)],[805:[bind(A,$thf( A )),bind(B,$thf( unit )),bind(C,$thf( A ))]]) ).
thf(5,axiom,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ mult ) @ rd ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c04) ).
thf(20,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ mult ) @ rd ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(21,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ mult ) @ rd ) )
= A ),
inference(lifteq,[status(thm)],[20]) ).
thf(1225,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( C @ ( B @ mult ) ) )
| ( ( C @ ( unit @ rd ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[806,21]) ).
thf(1226,plain,
! [A: $i] :
( ( A @ i @ ( unit @ rd ) )
= A ),
inference(pattern_uni,[status(thm)],[1225:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ i ))]]) ).
thf(1364,plain,
! [A: $i] :
( ( A @ i @ ( unit @ rd ) )
= A ),
inference(simp,[status(thm)],[1226]) ).
thf(605,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( C @ ( B @ mult ) ) )
| ( ( C @ ( unit @ rd ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[498,21]) ).
thf(606,plain,
! [A: $i] :
( ( A @ ( unit @ rd ) )
= ( A @ i ) ),
inference(pattern_uni,[status(thm)],[605:[bind(A,$thf( D )),bind(B,$thf( D @ i )),bind(C,$thf( D ))]]) ).
thf(708,plain,
! [A: $i] :
( ( A @ ( unit @ rd ) )
= ( A @ i ) ),
inference(simp,[status(thm)],[606]) ).
thf(1380,plain,
! [A: $i] :
( ( A @ i @ i )
= A ),
inference(rewrite,[status(thm)],[1364,708]) ).
thf(1388,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i @ i )
!= ( C @ i ) )
| ( ( A @ ( C @ ( B @ mult ) @ mult ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[1380,29]) ).
thf(1389,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ i @ ( A @ mult ) @ mult ) )
= A ),
inference(pattern_uni,[status(thm)],[1388:[bind(A,$thf( D )),bind(B,$thf( B )),bind(C,$thf( D @ i ))]]) ).
thf(1406,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ i @ ( A @ mult ) @ mult ) )
= A ),
inference(simp,[status(thm)],[1389]) ).
thf(801,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( D @ ( C @ mult ) ) )
| ( ( D @ i @ ( B @ mult ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[15,29]) ).
thf(802,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ld ) @ i @ ( B @ mult ) )
= A ),
inference(pattern_uni,[status(thm)],[801:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ ld ) ))]]) ).
thf(890,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ld ) @ i @ ( B @ mult ) )
= A ),
inference(simp,[status(thm)],[802]) ).
thf(3807,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ i @ mult ) @ i @ ( B @ mult ) )
= A ),
inference(rewrite,[status(thm)],[890,586]) ).
thf(1,negated_conjecture,
( ( c @ ( b @ ( c @ mult ) @ mult ) @ ( b @ ( a @ mult ) @ mult ) )
!= ( c @ ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) @ mult ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
thf(11,plain,
( ( c @ ( b @ ( c @ mult ) @ mult ) @ ( b @ ( a @ mult ) @ mult ) )
!= ( c @ ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) @ mult ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(12,plain,
( ( c @ ( b @ ( c @ mult ) @ mult ) @ ( b @ ( a @ mult ) @ mult ) )
!= ( c @ ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) @ mult ) ) ),
inference(polarity_switch,[status(thm)],[11]) ).
thf(13,plain,
( ( c @ ( b @ ( c @ mult ) @ mult ) @ ( b @ ( a @ mult ) @ mult ) )
!= ( c @ ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) @ mult ) ) ),
inference(lifteq,[status(thm)],[12]) ).
thf(54,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( c @ ( b @ ( c @ mult ) @ mult ) ) )
| ( ( A @ ( b @ ( a @ mult ) @ mult ) )
!= ( c @ ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,13]) ).
thf(132,plain,
! [A: $i] :
( ( A != c )
| ( ( b @ ( c @ mult ) )
!= unit )
| ( A != c )
| ( ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[54]) ).
thf(144,plain,
( ( ( b @ ( c @ mult ) )
!= unit )
| ( ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[132]) ).
thf(189,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( b @ ( c @ ( b @ mult ) @ mult ) ) )
| ( ( b @ ( c @ mult ) )
!= unit )
| ( ( A @ ( a @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,144]) ).
thf(207,plain,
! [A: $i] :
( ( A != b )
| ( ( c @ ( b @ mult ) )
!= unit )
| ( ( b @ ( c @ mult ) )
!= unit )
| ( A != b )
| ( a != a ) ),
inference(simp,[status(thm)],[189]) ).
thf(241,plain,
( ( ( c @ ( b @ mult ) )
!= unit )
| ( ( b @ ( c @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[207]) ).
thf(272,plain,
( ( unit != unit )
| ( ( b @ ( c @ mult ) )
!= ( c @ ( b @ mult ) ) )
| ( ( c @ ( b @ mult ) )
!= unit ) ),
inference(eqfactor_ordered,[status(thm)],[241]) ).
thf(284,plain,
( ( c != b )
| ( c != b )
| ( ( c @ ( b @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[272]) ).
thf(289,plain,
( ( c != b )
| ( ( c @ ( b @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[284]) ).
thf(3835,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ i @ mult ) @ i @ ( B @ mult ) )
!= ( c @ ( b @ mult ) ) )
| ( c != b )
| ( A != unit ) ),
inference(paramod_ordered,[status(thm)],[3807,289]) ).
thf(3953,plain,
! [A: $i] :
( ( ( A @ ( unit @ i @ mult ) @ i )
!= c )
| ( A != b )
| ( c != b ) ),
inference(simp,[status(thm)],[3835]) ).
thf(4109,plain,
( ( ( b @ ( unit @ i @ mult ) @ i )
!= c )
| ( c != b ) ),
inference(simp,[status(thm)],[3953]) ).
thf(4216,plain,
( ( ( b @ ( unit @ mult ) @ i )
!= c )
| ( c != b ) ),
inference(rewrite,[status(thm)],[4109,616]) ).
thf(1390,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i @ i )
!= ( B @ i ) )
| ( ( C @ ( B @ mult ) @ ( A @ mult ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[1380,27]) ).
thf(1391,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ i @ mult ) @ ( B @ mult ) )
= A ),
inference(pattern_uni,[status(thm)],[1390:[bind(A,$thf( D )),bind(B,$thf( D @ i ))]]) ).
thf(1407,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ i @ mult ) @ ( B @ mult ) )
= A ),
inference(simp,[status(thm)],[1391]) ).
thf(4,axiom,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ rd ) @ mult ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c03) ).
thf(18,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ rd ) @ mult ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(19,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ rd ) @ mult ) )
= A ),
inference(lifteq,[status(thm)],[18]) ).
thf(513,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( D @ ( C @ mult ) ) )
| ( ( A @ ( C @ i @ mult ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[19,27]) ).
thf(514,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ rd ) @ i @ mult ) )
= B ),
inference(pattern_uni,[status(thm)],[513:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ rd ) )),bind(D,$thf( F ))]]) ).
thf(563,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ rd ) @ i @ mult ) )
= B ),
inference(simp,[status(thm)],[514]) ).
thf(2222,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ rd ) @ i @ mult ) )
!= ( b @ ( c @ mult ) ) )
| ( ( c @ ( b @ mult ) )
!= unit )
| ( B != unit ) ),
inference(paramod_ordered,[status(thm)],[563,241]) ).
thf(2269,plain,
! [A: $i] :
( ( A != b )
| ( ( unit @ ( A @ rd ) @ i )
!= c )
| ( ( c @ ( b @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[2222]) ).
thf(2388,plain,
( ( ( unit @ ( b @ rd ) @ i )
!= c )
| ( ( c @ ( b @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[2269]) ).
thf(831,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( D @ ( C @ mult ) ) )
| ( ( D @ i @ ( A @ mult ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[19,29]) ).
thf(832,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ rd ) )
= ( B @ i @ ( A @ mult ) ) ),
inference(pattern_uni,[status(thm)],[831:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ rd ) )),bind(D,$thf( F ))]]) ).
thf(896,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ rd ) )
= ( B @ i @ ( A @ mult ) ) ),
inference(simp,[status(thm)],[832]) ).
thf(8545,plain,
( ( ( unit @ i @ ( b @ mult ) @ i )
!= c )
| ( ( c @ ( b @ mult ) )
!= unit ) ),
inference(rewrite,[status(thm)],[2388,896]) ).
thf(69,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( b @ ( c @ mult ) ) )
| ( ( c @ ( B @ mult ) @ ( b @ ( a @ mult ) @ mult ) )
!= ( c @ ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[15,13]) ).
thf(75,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( b @ ( c @ mult ) ) )
| ( ( c @ ( B @ mult ) )
!= c )
| ( ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[69]) ).
thf(1842,plain,
! [A: $i] :
( ( A
!= ( b @ ( c @ mult ) ) )
| ( ( c @ ( A @ mult ) )
!= c )
| ( ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[75,15]) ).
thf(60,plain,
! [A: $i] :
( ( ( unit @ ( A @ mult ) )
!= ( c @ ( b @ ( c @ mult ) @ mult ) @ ( b @ ( a @ mult ) @ mult ) ) )
| ( A
!= ( c @ ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[23,13]) ).
thf(87,plain,
( ( ( c @ ( b @ ( c @ mult ) @ mult ) )
!= unit )
| ( ( c @ ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[60]) ).
thf(2178,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ rd ) @ i @ mult ) )
!= ( D @ ( C @ mult ) ) )
| ( ( D @ ( B @ rd ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[563,21]) ).
thf(2179,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ rd ) )
= ( B @ ( A @ rd ) @ i ) ),
inference(pattern_uni,[status(thm)],[2178:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( G @ ( F @ rd ) @ i )),bind(D,$thf( F ))]]) ).
thf(2360,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ rd ) )
= ( B @ ( A @ rd ) @ i ) ),
inference(simp,[status(thm)],[2179]) ).
thf(7908,plain,
! [B: $i,A: $i] :
( ( A @ i @ ( B @ mult ) )
= ( B @ i @ ( A @ mult ) @ i ) ),
inference(rewrite,[status(thm)],[2360,896]) ).
thf(7909,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i @ ( B @ mult ) )
!= ( C @ i @ ( unit @ mult ) ) )
| ( ( B @ i @ ( A @ mult ) @ i )
= ( C @ i ) ) ),
inference(paramod_ordered,[status(thm)],[7908,5028]) ).
thf(7910,plain,
! [A: $i] :
( ( unit @ i @ ( A @ mult ) @ i )
= ( A @ i ) ),
inference(pattern_uni,[status(thm)],[7909:[bind(A,$thf( A )),bind(B,$thf( unit )),bind(C,$thf( A ))]]) ).
thf(9134,plain,
! [A: $i] :
( ( unit @ ( A @ mult ) @ i )
= ( A @ i ) ),
inference(rewrite,[status(thm)],[7910,616]) ).
thf(636,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( c @ ( b @ mult ) ) )
| ( unit != unit )
| ( ( b @ ( c @ mult ) )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[498,241]) ).
thf(637,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( c @ ( b @ mult ) ) )
| ( ( b @ ( c @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[636]) ).
thf(651,plain,
! [A: $i] :
( ( A != c )
| ( ( A @ i )
!= b )
| ( ( b @ ( c @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[637]) ).
thf(690,plain,
( ( ( c @ i )
!= b )
| ( ( b @ ( c @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[651]) ).
thf(729,plain,
! [A: $i] :
( ( ( unit @ ( A @ mult ) )
!= ( b @ ( c @ mult ) ) )
| ( ( c @ i )
!= b )
| ( A != unit ) ),
inference(paramod_ordered,[status(thm)],[23,690]) ).
thf(740,plain,
( ( unit != b )
| ( unit != c )
| ( ( c @ i )
!= b ) ),
inference(simp,[status(thm)],[729]) ).
thf(984,plain,
( ( ( unit @ i )
!= ( c @ i ) )
| ( unit != b )
| ( unit != c )
| ( unit != b ) ),
inference(paramod_ordered,[status(thm)],[616,740]) ).
thf(985,plain,
( ( ( unit @ i )
!= ( c @ i ) )
| ( unit != c )
| ( unit != b ) ),
inference(simp,[status(thm)],[984]) ).
thf(986,plain,
( ( unit != c )
| ( unit != c )
| ( unit != b ) ),
inference(simp,[status(thm)],[985]) ).
thf(987,plain,
( ( unit != c )
| ( unit != b ) ),
inference(simp,[status(thm)],[986]) ).
thf(57,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( c @ ( b @ mult ) ) )
| ( ( c @ ( b @ ( A @ mult ) @ ( a @ mult ) @ mult ) )
!= ( c @ ( b @ ( c @ mult ) @ mult ) @ ( b @ ( a @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,13]) ).
thf(83,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( c @ ( b @ mult ) ) )
| ( ( c @ ( b @ ( c @ mult ) @ mult ) )
!= c )
| ( ( b @ ( A @ mult ) @ ( a @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[57]) ).
thf(3474,plain,
! [A: $i] :
( ( A
!= ( c @ ( b @ mult ) ) )
| ( ( c @ ( b @ ( c @ mult ) @ mult ) )
!= c )
| ( ( b @ ( A @ mult ) @ ( a @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[83,25]) ).
thf(63,plain,
! [A: $i] :
( ( ( unit @ ( A @ mult ) )
!= ( c @ ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) @ mult ) ) )
| ( A
!= ( c @ ( b @ ( c @ mult ) @ mult ) @ ( b @ ( a @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[23,13]) ).
thf(110,plain,
( ( unit != c )
| ( ( c @ ( b @ ( c @ mult ) @ mult ) @ ( b @ ( a @ mult ) @ mult ) )
!= ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[63]) ).
thf(53,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( b @ ( c @ mult ) ) )
| ( ( c @ ( A @ mult ) @ ( b @ ( a @ mult ) @ mult ) )
!= ( c @ ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,13]) ).
thf(94,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( b @ ( c @ mult ) ) )
| ( ( c @ ( A @ mult ) )
!= c )
| ( ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[53]) ).
thf(5433,plain,
! [A: $i] :
( ( A
!= ( b @ ( c @ mult ) ) )
| ( ( c @ ( A @ mult ) )
!= c )
| ( ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[94,25]) ).
thf(623,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( C @ ( B @ mult ) ) )
| ( ( unit @ ( B @ ld ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[498,17]) ).
thf(624,plain,
! [A: $i] :
( ( unit @ ( A @ i @ ld ) )
= A ),
inference(pattern_uni,[status(thm)],[623:[bind(A,$thf( D )),bind(B,$thf( D @ i )),bind(C,$thf( D ))]]) ).
thf(717,plain,
! [A: $i] :
( ( unit @ ( A @ i @ ld ) )
= A ),
inference(simp,[status(thm)],[624]) ).
thf(292,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( c @ ( b @ mult ) ) )
| ( c != b )
| ( B != unit ) ),
inference(paramod_ordered,[status(thm)],[15,289]) ).
thf(298,plain,
! [A: $i] :
( ( ( unit @ ( A @ ld ) )
!= c )
| ( A != b )
| ( c != b ) ),
inference(simp,[status(thm)],[292]) ).
thf(299,plain,
( ( ( unit @ ( b @ ld ) )
!= c )
| ( c != b ) ),
inference(simp,[status(thm)],[298]) ).
thf(965,plain,
! [A: $i] :
( ( ( unit @ ( A @ i @ ld ) )
!= ( unit @ ( b @ ld ) ) )
| ( A != c )
| ( c != b ) ),
inference(paramod_ordered,[status(thm)],[717,299]) ).
thf(968,plain,
( ( ( unit @ ( c @ i @ ld ) )
!= ( unit @ ( b @ ld ) ) )
| ( c != b ) ),
inference(simp,[status(thm)],[965]) ).
thf(5363,plain,
( ( ( unit @ ( c @ i @ i @ mult ) )
!= ( unit @ ( b @ i @ mult ) ) )
| ( c != b ) ),
inference(rewrite,[status(thm)],[968,586]) ).
thf(5367,plain,
( ( ( c @ i @ i )
!= ( unit @ i ) )
| ( ( unit @ ( b @ i @ mult ) )
!= ( unit @ ( unit @ mult ) ) )
| ( c != b ) ),
inference(paramod_ordered,[status(thm)],[616,5363]) ).
thf(5391,plain,
( ( ( c @ i )
!= unit )
| ( unit != unit )
| ( ( b @ i )
!= unit )
| ( c != b ) ),
inference(simp,[status(thm)],[5367]) ).
thf(5414,plain,
( ( ( c @ i )
!= unit )
| ( ( b @ i )
!= unit )
| ( c != b ) ),
inference(simp,[status(thm)],[5391]) ).
thf(5875,plain,
( ( unit != unit )
| ( ( c @ i )
!= ( b @ i ) )
| ( ( b @ i )
!= unit )
| ( c != b ) ),
inference(eqfactor_ordered,[status(thm)],[5414]) ).
thf(5879,plain,
( ( c != b )
| ( ( b @ i )
!= unit )
| ( c != b ) ),
inference(simp,[status(thm)],[5875]) ).
thf(5884,plain,
( ( ( b @ i )
!= unit )
| ( c != b ) ),
inference(simp,[status(thm)],[5879]) ).
thf(5885,plain,
( ( ( unit @ i )
!= ( b @ i ) )
| ( unit != unit )
| ( c != b ) ),
inference(paramod_ordered,[status(thm)],[616,5884]) ).
thf(5886,plain,
( ( ( unit @ i )
!= ( b @ i ) )
| ( c != b ) ),
inference(simp,[status(thm)],[5885]) ).
thf(5888,plain,
( ( unit != b )
| ( c != b ) ),
inference(simp,[status(thm)],[5886]) ).
thf(50,plain,
( ( ( c @ ( b @ ( c @ mult ) @ mult ) )
!= c )
| ( ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[13]) ).
thf(10,axiom,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ mult ) @ ( C @ mult ) @ ( B @ ( A @ mult ) @ mult ) )
= ( B @ ( A @ ( C @ ( B @ mult ) @ ( A @ mult ) @ mult ) @ mult ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c09) ).
thf(30,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ mult ) @ ( C @ mult ) @ ( B @ ( A @ mult ) @ mult ) )
= ( B @ ( A @ ( C @ ( B @ mult ) @ ( A @ mult ) @ mult ) @ mult ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(31,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( C @ ( B @ mult ) @ ( A @ mult ) @ mult ) @ mult ) )
= ( B @ ( A @ mult ) @ ( C @ mult ) @ ( B @ ( A @ mult ) @ mult ) ) ),
inference(lifteq,[status(thm)],[30]) ).
thf(2223,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ rd ) @ i @ mult ) )
!= ( c @ ( b @ mult ) ) )
| ( B != unit )
| ( ( b @ ( c @ mult ) )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[563,241]) ).
thf(2329,plain,
! [A: $i] :
( ( A != c )
| ( ( unit @ ( A @ rd ) @ i )
!= b )
| ( ( b @ ( c @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[2223]) ).
thf(2355,plain,
( ( ( unit @ ( c @ rd ) @ i )
!= b )
| ( ( b @ ( c @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[2329]) ).
thf(8449,plain,
( ( ( unit @ i @ ( c @ mult ) @ i )
!= b )
| ( ( b @ ( c @ mult ) )
!= unit ) ),
inference(rewrite,[status(thm)],[2355,896]) ).
thf(634,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( b @ ( c @ mult ) ) )
| ( ( c @ ( b @ mult ) )
!= unit )
| ( unit != unit ) ),
inference(paramod_ordered,[status(thm)],[498,241]) ).
thf(635,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( b @ ( c @ mult ) ) )
| ( ( c @ ( b @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[634]) ).
thf(659,plain,
! [A: $i] :
( ( A != b )
| ( ( A @ i )
!= c )
| ( ( c @ ( b @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[635]) ).
thf(698,plain,
( ( ( b @ i )
!= c )
| ( ( c @ ( b @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[659]) ).
thf(1219,plain,
! [A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( c @ ( b @ mult ) ) )
| ( ( b @ i )
!= c )
| ( unit != unit ) ),
inference(paramod_ordered,[status(thm)],[806,698]) ).
thf(1220,plain,
! [A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( c @ ( b @ mult ) ) )
| ( ( b @ i )
!= c ) ),
inference(simp,[status(thm)],[1219]) ).
thf(1279,plain,
! [A: $i] :
( ( ( A @ i )
!= c )
| ( A != b )
| ( ( b @ i )
!= c ) ),
inference(simp,[status(thm)],[1220]) ).
thf(1372,plain,
( ( b @ i )
!= c ),
inference(simp,[status(thm)],[1279]) ).
thf(1262,plain,
! [A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( b @ ( c @ mult ) ) )
| ( ( c @ i )
!= b )
| ( unit != unit ) ),
inference(paramod_ordered,[status(thm)],[806,690]) ).
thf(1263,plain,
! [A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( b @ ( c @ mult ) ) )
| ( ( c @ i )
!= b ) ),
inference(simp,[status(thm)],[1262]) ).
thf(1300,plain,
! [A: $i] :
( ( ( A @ i )
!= b )
| ( A != c )
| ( ( c @ i )
!= b ) ),
inference(simp,[status(thm)],[1263]) ).
thf(1341,plain,
( ( c @ i )
!= b ),
inference(simp,[status(thm)],[1300]) ).
thf(52,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( c @ ( b @ ( c @ mult ) @ mult ) @ ( b @ ( a @ mult ) @ mult ) ) )
| ( A
!= ( c @ ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,13]) ).
thf(82,plain,
( ( ( c @ ( b @ ( c @ ( b @ mult ) @ mult ) @ ( a @ mult ) @ mult ) )
!= ( c @ ( b @ ( c @ mult ) @ mult ) ) )
| ( ( b @ ( a @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[52]) ).
thf(56,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( b @ ( c @ ( b @ mult ) @ mult ) ) )
| ( ( c @ ( A @ ( a @ mult ) @ mult ) )
!= ( c @ ( b @ ( c @ mult ) @ mult ) @ ( b @ ( a @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,13]) ).
thf(78,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( b @ ( c @ ( b @ mult ) @ mult ) ) )
| ( ( c @ ( b @ ( c @ mult ) @ mult ) )
!= c )
| ( ( A @ ( a @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[56]) ).
thf(2421,plain,
! [A: $i] :
( ( A
!= ( b @ ( c @ ( b @ mult ) @ mult ) ) )
| ( ( c @ ( b @ ( c @ mult ) @ mult ) )
!= c )
| ( ( A @ ( a @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[78,25]) ).
thf(85474,plain,
$false,
inference(e,[status(thm)],[5028,1406,4216,28,1407,8545,1842,13,616,241,18,87,9134,987,3474,24,4610,25,14,110,20,289,29,5433,5888,806,586,3807,22,27,5363,144,498,50,16,31,11,8449,1372,7908,26,23,1341,896,82,2421,30,1380,5884]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP670-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % 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.14/0.39 % Computer : n006.cluster.edu
% 0.14/0.39 % Model : x86_64 x86_64
% 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39 % Memory : 8046.5625MB
% 0.14/0.39 % OS : Linux 6.8.0-71-generic
% 0.14/0.39 % CPULimit : 300
% 0.14/0.39 % WCLimit : 300
% 0.14/0.39 % DateTime : Fri Sep 25 15:34:41 UTC 2026
% 0.14/0.39 % CPUTime :
% 0.14/0.39 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.59/0.68 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 0.74/0.77 % [INFO] Parsing done (87ms).
% 0.74/0.78 % [INFO] Running in sequential loop mode.
% 1.15/0.96 % [INFO] eprover registered as external prover.
% 1.15/0.96 % [INFO] Scanning for conjecture ...
% 1.15/1.01 % [INFO] Found a conjecture (or negated_conjecture) and 9 axioms. Running axiom selection ...
% 1.15/1.02 % [INFO] Axiom selection finished. Selected 9 axioms (removed 0 axioms).
% 1.47/1.03 % [INFO] Problem is propositional (TPTP CNF).
% 1.47/1.03 % [INFO] Type checking passed.
% 1.47/1.04 % [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 ...
% 103.34/30.35 % External prover 'e' found a proof!
% 103.34/30.35 % [INFO] Killing All external provers ...
% 103.34/30.36 % Time passed: 29877ms (effective reasoning time: 29577ms)
% 103.34/30.36 % Axioms used in derivation (9): c05, c08, c01, c03, c06, c02, c07, c09, c04
% 103.34/30.36 % No. of inferences in proof: 159
% 103.34/30.36 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : 29877 ms resp. 29577 ms w/o parsing
% 91.91/30.44 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 91.91/30.44 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------