%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : GRA117^1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 07:50:21 AM UTC 2026
% Result : Unsatisfiable 95.74s 22.84s
% Output : Refutation 90.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 18
% Syntax : Number of formulae : 308 ( 61 unt; 0 typ; 0 def)
% Number of atoms : 1385 ( 444 equ; 0 cnn)
% Maximal formula atoms : 8 ( 4 avg)
% Number of connectives : 3040 ( 395 ~; 867 |; 0 &;1778 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 10 ( 7 usr; 8 con; 0-2 aty)
% Number of variables : 254 ( 0 ^; 254 !; 0 ?; 254 :)
% Comments :
%------------------------------------------------------------------------------
thf(r_decl,type,
r: $i > $i > $o ).
thf(v0_decl,type,
v0: $i ).
thf(v1_decl,type,
v1: $i ).
thf(v2_decl,type,
v2: $i ).
thf(v3_decl,type,
v3: $i ).
thf(v4_decl,type,
v4: $i ).
thf(v5_decl,type,
v5: $i ).
thf(3,axiom,
! [A: $i,B: $i,C: $i] :
( ( A = B )
| ( A = C )
| ( B = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rno3acl) ).
thf(25,plain,
! [A: $i,B: $i,C: $i] :
( ( A = B )
| ( A = C )
| ( B = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(26,plain,
! [A: $i,B: $i] :
( ( A = B )
| ! [C: $i] :
( ( A = C )
| ( B = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C ) ) ),
inference(miniscope,[status(thm)],[25]) ).
thf(27,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( A = C )
| ( B = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C ) ),
inference(cnf,[status(esa)],[26]) ).
thf(28,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( A = C )
| ( B = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C ) ),
inference(lifteq,[status(thm)],[27]) ).
thf(7,axiom,
v0 != v3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v0nv3) ).
thf(38,plain,
v0 != v3,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(39,plain,
v0 != v3,
inference(polarity_switch,[status(thm)],[38]) ).
thf(40,plain,
v3 != v0,
inference(lifteq,[status(thm)],[39]) ).
thf(138,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( B = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( C != v0 )
| ( A != v3 ) ),
inference(paramod_ordered,[status(thm)],[28,40]) ).
thf(139,plain,
! [B: $i,A: $i] :
( ( v3 = A )
| ( A = B )
| ( r @ v3 @ A )
| ( r @ v3 @ B )
| ( r @ A @ B )
| ( B != v0 ) ),
inference(pattern_uni,[status(thm)],[138:[bind(A,$thf( v3 ))]]) ).
thf(164,plain,
! [A: $i] :
( ( v3 = A )
| ( A = v0 )
| ( r @ v3 @ A )
| ( r @ v3 @ v0 )
| ( r @ A @ v0 ) ),
inference(simp,[status(thm)],[139]) ).
thf(18,axiom,
v4 != v5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v4nv5) ).
thf(71,plain,
v4 != v5,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(72,plain,
v4 != v5,
inference(polarity_switch,[status(thm)],[71]) ).
thf(73,plain,
v5 != v4,
inference(lifteq,[status(thm)],[72]) ).
thf(8,axiom,
v1 != v3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v1nv3) ).
thf(41,plain,
v1 != v3,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(42,plain,
v1 != v3,
inference(polarity_switch,[status(thm)],[41]) ).
thf(43,plain,
v3 != v1,
inference(lifteq,[status(thm)],[42]) ).
thf(128,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( B = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( A != v1 )
| ( C != v3 ) ),
inference(paramod_ordered,[status(thm)],[28,43]) ).
thf(129,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( B = v3 )
| ( r @ A @ B )
| ( r @ A @ v3 )
| ( r @ B @ v3 )
| ( A != v1 ) ),
inference(pattern_uni,[status(thm)],[128:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( v3 ))]]) ).
thf(158,plain,
! [A: $i] :
( ( v1 = A )
| ( A = v3 )
| ( r @ v1 @ A )
| ( r @ v1 @ v3 )
| ( r @ A @ v3 ) ),
inference(simp,[status(thm)],[129]) ).
thf(13,axiom,
v3 != v4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v3nv4) ).
thf(56,plain,
v3 != v4,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(57,plain,
v3 != v4,
inference(polarity_switch,[status(thm)],[56]) ).
thf(58,plain,
v4 != v3,
inference(lifteq,[status(thm)],[57]) ).
thf(364,plain,
! [A: $i] :
( ( v1 = A )
| ( r @ v1 @ A )
| ( r @ v1 @ v3 )
| ( r @ A @ v3 )
| ( v3 != v3 )
| ( A != v4 ) ),
inference(paramod_ordered,[status(thm)],[158,58]) ).
thf(365,plain,
! [A: $i] :
( ( v1 = A )
| ( r @ v1 @ A )
| ( r @ v1 @ v3 )
| ( r @ A @ v3 )
| ( A != v4 ) ),
inference(simp,[status(thm)],[364]) ).
thf(366,plain,
( ( v4 = v1 )
| ( r @ v1 @ v4 )
| ( r @ v1 @ v3 )
| ( r @ v4 @ v3 ) ),
inference(pattern_uni,[status(thm)],[365:[bind(A,$thf( v4 ))]]) ).
thf(11,axiom,
v1 != v4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v1nv4) ).
thf(50,plain,
v1 != v4,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(51,plain,
v1 != v4,
inference(polarity_switch,[status(thm)],[50]) ).
thf(52,plain,
v4 != v1,
inference(lifteq,[status(thm)],[51]) ).
thf(996,plain,
( ( r @ v1 @ v4 )
| ( r @ v1 @ v3 )
| ( r @ v4 @ v3 ) ),
inference(simplifyReflect,[status(thm)],[366,52]) ).
thf(1066,plain,
( ( r @ v1 @ v4 )
| ( r @ v1 @ v3 )
| ( ( r @ v4 @ v3 )
!= ( r @ v1 @ v4 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[996]) ).
thf(1070,plain,
( ( r @ v1 @ v4 )
| ( r @ v1 @ v3 )
| ( ( r @ v4 @ v3 )
!= ( r @ v1 @ v4 ) ) ),
inference(simp,[status(thm)],[1066]) ).
thf(130,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( A = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( C != v1 )
| ( B != v3 ) ),
inference(paramod_ordered,[status(thm)],[28,43]) ).
thf(131,plain,
! [B: $i,A: $i] :
( ( A = v3 )
| ( A = B )
| ( r @ A @ v3 )
| ( r @ A @ B )
| ( r @ v3 @ B )
| ( B != v1 ) ),
inference(pattern_uni,[status(thm)],[130:[bind(A,$thf( A )),bind(B,$thf( v3 ))]]) ).
thf(159,plain,
! [A: $i] :
( ( A = v3 )
| ( A = v1 )
| ( r @ A @ v3 )
| ( r @ A @ v1 )
| ( r @ v3 @ v1 ) ),
inference(simp,[status(thm)],[131]) ).
thf(17,axiom,
v3 != v5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v3nv5) ).
thf(68,plain,
v3 != v5,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(69,plain,
v3 != v5,
inference(polarity_switch,[status(thm)],[68]) ).
thf(70,plain,
v5 != v3,
inference(lifteq,[status(thm)],[69]) ).
thf(1846,plain,
! [A: $i] :
( ( A = v1 )
| ( r @ A @ v3 )
| ( r @ A @ v1 )
| ( r @ v3 @ v1 )
| ( v3 != v3 )
| ( A != v5 ) ),
inference(paramod_ordered,[status(thm)],[159,70]) ).
thf(1847,plain,
! [A: $i] :
( ( A = v1 )
| ( r @ A @ v3 )
| ( r @ A @ v1 )
| ( r @ v3 @ v1 )
| ( A != v5 ) ),
inference(simp,[status(thm)],[1846]) ).
thf(1848,plain,
( ( v5 = v1 )
| ( r @ v5 @ v3 )
| ( r @ v5 @ v1 )
| ( r @ v3 @ v1 ) ),
inference(pattern_uni,[status(thm)],[1847:[bind(A,$thf( v5 ))]]) ).
thf(15,axiom,
v1 != v5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v1nv5) ).
thf(62,plain,
v1 != v5,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(63,plain,
v1 != v5,
inference(polarity_switch,[status(thm)],[62]) ).
thf(64,plain,
v5 != v1,
inference(lifteq,[status(thm)],[63]) ).
thf(7824,plain,
( ( r @ v5 @ v3 )
| ( r @ v5 @ v1 )
| ( r @ v3 @ v1 ) ),
inference(simplifyReflect,[status(thm)],[1848,64]) ).
thf(7959,plain,
( ( r @ v5 @ v1 )
| ( r @ v3 @ v1 )
| ( ( r @ v5 @ v3 )
!= ( r @ v5 @ v1 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[7824]) ).
thf(7974,plain,
( ( r @ v5 @ v1 )
| ( r @ v3 @ v1 )
| ( ( r @ v5 @ v3 )
!= ( r @ v5 @ v1 ) ) ),
inference(simp,[status(thm)],[7959]) ).
thf(2,axiom,
! [A: $i,B: $i,C: $i] :
( ( A = B )
| ( A = C )
| ( B = C )
| ~ ( r @ A @ B )
| ~ ( r @ A @ C )
| ~ ( r @ B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rno3cl) ).
thf(21,plain,
! [A: $i,B: $i,C: $i] :
( ( A = B )
| ( A = C )
| ( B = C )
| ~ ( r @ A @ B )
| ~ ( r @ A @ C )
| ~ ( r @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(22,plain,
! [A: $i,B: $i] :
( ( A = B )
| ! [C: $i] :
( ( A = C )
| ( B = C )
| ~ ( r @ A @ B )
| ~ ( r @ A @ C )
| ~ ( r @ B @ C ) ) ),
inference(miniscope,[status(thm)],[21]) ).
thf(23,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( A = C )
| ( B = C )
| ~ ( r @ A @ B )
| ~ ( r @ A @ C )
| ~ ( r @ B @ C ) ),
inference(cnf,[status(esa)],[22]) ).
thf(24,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( A = C )
| ( B = C )
| ~ ( r @ A @ B )
| ~ ( r @ A @ C )
| ~ ( r @ B @ C ) ),
inference(lifteq,[status(thm)],[23]) ).
thf(538,plain,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ( B = C )
| ~ ( r @ A @ B )
| ~ ( r @ A @ C )
| ~ ( r @ B @ C )
| ( B != v1 )
| ( A != v4 ) ),
inference(paramod_ordered,[status(thm)],[24,52]) ).
thf(539,plain,
! [B: $i,A: $i] :
( ( v4 = B )
| ( A = B )
| ~ ( r @ v4 @ A )
| ~ ( r @ v4 @ B )
| ~ ( r @ A @ B )
| ( A != v1 ) ),
inference(pattern_uni,[status(thm)],[538:[bind(A,$thf( v4 ))]]) ).
thf(866,plain,
! [A: $i] :
( ( v4 = A )
| ( v1 = A )
| ~ ( r @ v4 @ v1 )
| ~ ( r @ v4 @ A )
| ~ ( r @ v1 @ A ) ),
inference(simp,[status(thm)],[539]) ).
thf(1204,plain,
! [A: $i] :
( ( v1 = A )
| ~ ( r @ v4 @ v1 )
| ~ ( r @ v4 @ A )
| ~ ( r @ v1 @ A )
| ( v4 != v4 )
| ( A != v5 ) ),
inference(paramod_ordered,[status(thm)],[866,73]) ).
thf(1205,plain,
! [A: $i] :
( ( v1 = A )
| ~ ( r @ v4 @ v1 )
| ~ ( r @ v4 @ A )
| ~ ( r @ v1 @ A )
| ( A != v5 ) ),
inference(simp,[status(thm)],[1204]) ).
thf(1206,plain,
( ( v5 = v1 )
| ~ ( r @ v4 @ v1 )
| ~ ( r @ v4 @ v5 )
| ~ ( r @ v1 @ v5 ) ),
inference(pattern_uni,[status(thm)],[1205:[bind(A,$thf( v5 ))]]) ).
thf(4911,plain,
( ~ ( r @ v4 @ v1 )
| ~ ( r @ v4 @ v5 )
| ~ ( r @ v1 @ v5 ) ),
inference(simplifyReflect,[status(thm)],[1206,64]) ).
thf(5286,plain,
( ~ ( r @ v4 @ v1 )
| ~ ( r @ v1 @ v5 )
| ( ( r @ v4 @ v5 )
!= ( r @ v1 @ v5 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[4911]) ).
thf(5320,plain,
( ~ ( r @ v4 @ v1 )
| ~ ( r @ v1 @ v5 )
| ( ( r @ v4 @ v5 )
!= ( r @ v1 @ v5 ) ) ),
inference(simp,[status(thm)],[5286]) ).
thf(132,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( A = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( B != v1 )
| ( C != v3 ) ),
inference(paramod_ordered,[status(thm)],[28,43]) ).
thf(133,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( A = v3 )
| ( r @ A @ B )
| ( r @ A @ v3 )
| ( r @ B @ v3 )
| ( B != v1 ) ),
inference(pattern_uni,[status(thm)],[132:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( v3 ))]]) ).
thf(160,plain,
! [A: $i] :
( ( A = v1 )
| ( A = v3 )
| ( r @ A @ v1 )
| ( r @ A @ v3 )
| ( r @ v1 @ v3 ) ),
inference(simp,[status(thm)],[133]) ).
thf(2571,plain,
! [A: $i] :
( ( A = v1 )
| ( r @ A @ v1 )
| ( r @ A @ v3 )
| ( r @ v1 @ v3 )
| ( v3 != v3 )
| ( A != v5 ) ),
inference(paramod_ordered,[status(thm)],[160,70]) ).
thf(2572,plain,
! [A: $i] :
( ( A = v1 )
| ( r @ A @ v1 )
| ( r @ A @ v3 )
| ( r @ v1 @ v3 )
| ( A != v5 ) ),
inference(simp,[status(thm)],[2571]) ).
thf(2573,plain,
( ( v5 = v1 )
| ( r @ v5 @ v1 )
| ( r @ v5 @ v3 )
| ( r @ v1 @ v3 ) ),
inference(pattern_uni,[status(thm)],[2572:[bind(A,$thf( v5 ))]]) ).
thf(20162,plain,
( ( r @ v5 @ v1 )
| ( r @ v5 @ v3 )
| ( r @ v1 @ v3 ) ),
inference(simplifyReflect,[status(thm)],[2573,64]) ).
thf(144,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( A = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( B != v0 )
| ( C != v3 ) ),
inference(paramod_ordered,[status(thm)],[28,40]) ).
thf(145,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( A = v3 )
| ( r @ A @ B )
| ( r @ A @ v3 )
| ( r @ B @ v3 )
| ( B != v0 ) ),
inference(pattern_uni,[status(thm)],[144:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( v3 ))]]) ).
thf(170,plain,
! [A: $i] :
( ( A = v0 )
| ( A = v3 )
| ( r @ A @ v0 )
| ( r @ A @ v3 )
| ( r @ v0 @ v3 ) ),
inference(simp,[status(thm)],[145]) ).
thf(440,plain,
! [A: $i] :
( ( v1 = A )
| ( r @ v1 @ A )
| ( r @ v1 @ v3 )
| ( r @ A @ v3 )
| ( v3 != v3 )
| ( A != v5 ) ),
inference(paramod_ordered,[status(thm)],[158,70]) ).
thf(441,plain,
! [A: $i] :
( ( v1 = A )
| ( r @ v1 @ A )
| ( r @ v1 @ v3 )
| ( r @ A @ v3 )
| ( A != v5 ) ),
inference(simp,[status(thm)],[440]) ).
thf(442,plain,
( ( v5 = v1 )
| ( r @ v1 @ v5 )
| ( r @ v1 @ v3 )
| ( r @ v5 @ v3 ) ),
inference(pattern_uni,[status(thm)],[441:[bind(A,$thf( v5 ))]]) ).
thf(1560,plain,
( ( r @ v1 @ v5 )
| ( r @ v1 @ v3 )
| ( r @ v5 @ v3 ) ),
inference(simplifyReflect,[status(thm)],[442,64]) ).
thf(1,axiom,
! [A: $i,B: $i] :
( ~ ( r @ A @ B )
| ( r @ B @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rsym) ).
thf(19,plain,
! [A: $i,B: $i] :
( ~ ( r @ A @ B )
| ( r @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(20,plain,
! [B: $i,A: $i] :
( ~ ( r @ A @ B )
| ( r @ B @ A ) ),
inference(cnf,[status(esa)],[19]) ).
thf(1594,plain,
! [B: $i,A: $i] :
( ( r @ v1 @ v5 )
| ( r @ v1 @ v3 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v5 @ v3 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[1560,20]) ).
thf(1595,plain,
! [B: $i,A: $i] :
( ( r @ v1 @ v5 )
| ( r @ v1 @ v3 )
| ( r @ B @ A )
| ( ( r @ v5 @ v3 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[1594]) ).
thf(1596,plain,
( ( r @ v1 @ v5 )
| ( r @ v1 @ v3 )
| ( r @ v3 @ v5 ) ),
inference(pattern_uni,[status(thm)],[1595:[bind(A,$thf( v5 )),bind(B,$thf( v3 ))]]) ).
thf(1691,plain,
! [A: $i] :
( ( A = v1 )
| ( r @ A @ v3 )
| ( r @ A @ v1 )
| ( r @ v3 @ v1 )
| ( v3 != v3 )
| ( A != v4 ) ),
inference(paramod_ordered,[status(thm)],[159,58]) ).
thf(1692,plain,
! [A: $i] :
( ( A = v1 )
| ( r @ A @ v3 )
| ( r @ A @ v1 )
| ( r @ v3 @ v1 )
| ( A != v4 ) ),
inference(simp,[status(thm)],[1691]) ).
thf(1693,plain,
( ( v4 = v1 )
| ( r @ v4 @ v3 )
| ( r @ v4 @ v1 )
| ( r @ v3 @ v1 ) ),
inference(pattern_uni,[status(thm)],[1692:[bind(A,$thf( v4 ))]]) ).
thf(4114,plain,
( ( r @ v4 @ v3 )
| ( r @ v4 @ v1 )
| ( r @ v3 @ v1 ) ),
inference(simplifyReflect,[status(thm)],[1693,52]) ).
thf(4222,plain,
( ( r @ v4 @ v1 )
| ( r @ v3 @ v1 )
| ( ( r @ v4 @ v3 )
!= ( r @ v3 @ v1 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[4114]) ).
thf(4226,plain,
( ( r @ v4 @ v1 )
| ( r @ v3 @ v1 )
| ( ( r @ v4 @ v3 )
!= ( r @ v3 @ v1 ) ) ),
inference(simp,[status(thm)],[4222]) ).
thf(1067,plain,
( ( r @ v1 @ v4 )
| ( r @ v1 @ v3 )
| ( ( r @ v4 @ v3 )
!= ( r @ v1 @ v3 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[996]) ).
thf(1068,plain,
( ( r @ v1 @ v4 )
| ( r @ v1 @ v3 )
| ( ( r @ v4 @ v3 )
!= ( r @ v1 @ v3 ) ) ),
inference(simp,[status(thm)],[1067]) ).
thf(7873,plain,
! [B: $i,A: $i] :
( ( r @ v5 @ v1 )
| ( r @ v3 @ v1 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v5 @ v3 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[7824,20]) ).
thf(7874,plain,
! [B: $i,A: $i] :
( ( r @ v5 @ v1 )
| ( r @ v3 @ v1 )
| ( r @ B @ A )
| ( ( r @ v5 @ v3 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[7873]) ).
thf(7875,plain,
( ( r @ v5 @ v1 )
| ( r @ v3 @ v1 )
| ( r @ v3 @ v5 ) ),
inference(pattern_uni,[status(thm)],[7874:[bind(A,$thf( v5 )),bind(B,$thf( v3 ))]]) ).
thf(8981,plain,
( ( r @ v3 @ v1 )
| ( r @ v3 @ v5 )
| ( ( r @ v5 @ v1 )
!= ( r @ v3 @ v1 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[7875]) ).
thf(8988,plain,
( ( r @ v3 @ v1 )
| ( r @ v3 @ v5 )
| ( ( r @ v5 @ v1 )
!= ( r @ v3 @ v1 ) ) ),
inference(simp,[status(thm)],[8981]) ).
thf(1030,plain,
! [B: $i,A: $i] :
( ( r @ v1 @ v4 )
| ( r @ v1 @ v3 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v4 @ v3 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[996,20]) ).
thf(1031,plain,
! [B: $i,A: $i] :
( ( r @ v1 @ v4 )
| ( r @ v1 @ v3 )
| ( r @ B @ A )
| ( ( r @ v4 @ v3 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[1030]) ).
thf(1032,plain,
( ( r @ v1 @ v4 )
| ( r @ v1 @ v3 )
| ( r @ v3 @ v4 ) ),
inference(pattern_uni,[status(thm)],[1031:[bind(A,$thf( v4 )),bind(B,$thf( v3 ))]]) ).
thf(1163,plain,
( ( r @ v1 @ v4 )
| ( r @ v1 @ v3 )
| ( ( r @ v3 @ v4 )
!= ( r @ v1 @ v3 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[1032]) ).
thf(1164,plain,
( ( r @ v1 @ v4 )
| ( r @ v1 @ v3 )
| ( ( r @ v3 @ v4 )
!= ( r @ v1 @ v3 ) ) ),
inference(simp,[status(thm)],[1163]) ).
thf(9,axiom,
v2 != v3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v2nv3) ).
thf(44,plain,
v2 != v3,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(45,plain,
v2 != v3,
inference(polarity_switch,[status(thm)],[44]) ).
thf(46,plain,
v3 != v2,
inference(lifteq,[status(thm)],[45]) ).
thf(1769,plain,
! [A: $i] :
( ( A = v1 )
| ( r @ A @ v3 )
| ( r @ A @ v1 )
| ( r @ v3 @ v1 )
| ( A != v2 )
| ( v3 != v3 ) ),
inference(paramod_ordered,[status(thm)],[159,46]) ).
thf(1770,plain,
! [A: $i] :
( ( A = v1 )
| ( r @ A @ v3 )
| ( r @ A @ v1 )
| ( r @ v3 @ v1 )
| ( A != v2 ) ),
inference(pattern_uni,[status(thm)],[1769:[]]) ).
thf(1996,plain,
( ( v2 = v1 )
| ( r @ v2 @ v3 )
| ( r @ v2 @ v1 )
| ( r @ v3 @ v1 ) ),
inference(simp,[status(thm)],[1770]) ).
thf(6,axiom,
v1 != v2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v1nv2) ).
thf(35,plain,
v1 != v2,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(36,plain,
v1 != v2,
inference(polarity_switch,[status(thm)],[35]) ).
thf(37,plain,
v2 != v1,
inference(lifteq,[status(thm)],[36]) ).
thf(14964,plain,
( ( r @ v2 @ v3 )
| ( r @ v2 @ v1 )
| ( r @ v3 @ v1 ) ),
inference(simplifyReflect,[status(thm)],[1996,37]) ).
thf(88,plain,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ( B = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( A != v2 )
| ( B != v3 ) ),
inference(paramod_ordered,[status(thm)],[28,46]) ).
thf(89,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( v3 = B )
| ( r @ A @ v3 )
| ( r @ A @ B )
| ( r @ v3 @ B )
| ( A != v2 ) ),
inference(pattern_uni,[status(thm)],[88:[bind(A,$thf( A )),bind(B,$thf( v3 ))]]) ).
thf(174,plain,
! [A: $i] :
( ( v2 = A )
| ( v3 = A )
| ( r @ v2 @ v3 )
| ( r @ v2 @ A )
| ( r @ v3 @ A ) ),
inference(simp,[status(thm)],[89]) ).
thf(134,plain,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ( B = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( B != v0 )
| ( A != v3 ) ),
inference(paramod_ordered,[status(thm)],[28,40]) ).
thf(135,plain,
! [B: $i,A: $i] :
( ( v3 = B )
| ( A = B )
| ( r @ v3 @ A )
| ( r @ v3 @ B )
| ( r @ A @ B )
| ( A != v0 ) ),
inference(pattern_uni,[status(thm)],[134:[bind(A,$thf( v3 ))]]) ).
thf(161,plain,
! [A: $i] :
( ( v3 = A )
| ( v0 = A )
| ( r @ v3 @ v0 )
| ( r @ v3 @ A )
| ( r @ v0 @ A ) ),
inference(simp,[status(thm)],[135]) ).
thf(3426,plain,
! [A: $i] :
( ( v0 = A )
| ( r @ v3 @ v0 )
| ( r @ v3 @ A )
| ( r @ v0 @ A )
| ( v3 != v3 )
| ( A != v4 ) ),
inference(paramod_ordered,[status(thm)],[161,58]) ).
thf(3427,plain,
! [A: $i] :
( ( v0 = A )
| ( r @ v3 @ v0 )
| ( r @ v3 @ A )
| ( r @ v0 @ A )
| ( A != v4 ) ),
inference(simp,[status(thm)],[3426]) ).
thf(3428,plain,
( ( v4 = v0 )
| ( r @ v3 @ v0 )
| ( r @ v3 @ v4 )
| ( r @ v0 @ v4 ) ),
inference(pattern_uni,[status(thm)],[3427:[bind(A,$thf( v4 ))]]) ).
thf(10,axiom,
v0 != v4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v0nv4) ).
thf(47,plain,
v0 != v4,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(48,plain,
v0 != v4,
inference(polarity_switch,[status(thm)],[47]) ).
thf(49,plain,
v4 != v0,
inference(lifteq,[status(thm)],[48]) ).
thf(28308,plain,
( ( r @ v3 @ v0 )
| ( r @ v3 @ v4 )
| ( r @ v0 @ v4 ) ),
inference(simplifyReflect,[status(thm)],[3428,49]) ).
thf(28375,plain,
! [B: $i,A: $i] :
( ( r @ v3 @ v0 )
| ( r @ v0 @ v4 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v3 @ v4 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[28308,20]) ).
thf(28376,plain,
! [B: $i,A: $i] :
( ( r @ v3 @ v0 )
| ( r @ v0 @ v4 )
| ( r @ B @ A )
| ( ( r @ v3 @ v4 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[28375]) ).
thf(28377,plain,
( ( r @ v3 @ v0 )
| ( r @ v0 @ v4 )
| ( r @ v4 @ v3 ) ),
inference(pattern_uni,[status(thm)],[28376:[bind(A,$thf( v3 )),bind(B,$thf( v4 ))]]) ).
thf(8909,plain,
! [B: $i,A: $i] :
( ( r @ v3 @ v1 )
| ( r @ v3 @ v5 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v5 @ v1 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[7875,20]) ).
thf(8910,plain,
! [B: $i,A: $i] :
( ( r @ v3 @ v1 )
| ( r @ v3 @ v5 )
| ( r @ B @ A )
| ( ( r @ v5 @ v1 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[8909]) ).
thf(8911,plain,
( ( r @ v3 @ v1 )
| ( r @ v3 @ v5 )
| ( r @ v1 @ v5 ) ),
inference(pattern_uni,[status(thm)],[8910:[bind(A,$thf( v5 )),bind(B,$thf( v1 ))]]) ).
thf(3625,plain,
! [A: $i] :
( ( v0 = A )
| ( r @ v3 @ v0 )
| ( r @ v3 @ A )
| ( r @ v0 @ A )
| ( v3 != v3 )
| ( A != v5 ) ),
inference(paramod_ordered,[status(thm)],[161,70]) ).
thf(3626,plain,
! [A: $i] :
( ( v0 = A )
| ( r @ v3 @ v0 )
| ( r @ v3 @ A )
| ( r @ v0 @ A )
| ( A != v5 ) ),
inference(simp,[status(thm)],[3625]) ).
thf(3627,plain,
( ( v5 = v0 )
| ( r @ v3 @ v0 )
| ( r @ v3 @ v5 )
| ( r @ v0 @ v5 ) ),
inference(pattern_uni,[status(thm)],[3626:[bind(A,$thf( v5 ))]]) ).
thf(14,axiom,
v0 != v5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v0nv5) ).
thf(59,plain,
v0 != v5,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(60,plain,
v0 != v5,
inference(polarity_switch,[status(thm)],[59]) ).
thf(61,plain,
v5 != v0,
inference(lifteq,[status(thm)],[60]) ).
thf(31043,plain,
( ( r @ v3 @ v0 )
| ( r @ v3 @ v5 )
| ( r @ v0 @ v5 ) ),
inference(simplifyReflect,[status(thm)],[3627,61]) ).
thf(4153,plain,
! [B: $i,A: $i] :
( ( r @ v4 @ v1 )
| ( r @ v3 @ v1 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v4 @ v3 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[4114,20]) ).
thf(4154,plain,
! [B: $i,A: $i] :
( ( r @ v4 @ v1 )
| ( r @ v3 @ v1 )
| ( r @ B @ A )
| ( ( r @ v4 @ v3 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[4153]) ).
thf(4155,plain,
( ( r @ v4 @ v1 )
| ( r @ v3 @ v1 )
| ( r @ v3 @ v4 ) ),
inference(pattern_uni,[status(thm)],[4154:[bind(A,$thf( v4 )),bind(B,$thf( v3 ))]]) ).
thf(4349,plain,
( ( r @ v3 @ v1 )
| ( r @ v3 @ v4 )
| ( ( r @ v4 @ v1 )
!= ( r @ v3 @ v4 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[4155]) ).
thf(4353,plain,
( ( r @ v3 @ v1 )
| ( r @ v3 @ v4 )
| ( ( r @ v4 @ v1 )
!= ( r @ v3 @ v4 ) ) ),
inference(simp,[status(thm)],[4349]) ).
thf(15026,plain,
! [B: $i,A: $i] :
( ( r @ v2 @ v3 )
| ( r @ v2 @ v1 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v3 @ v1 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[14964,20]) ).
thf(15027,plain,
! [B: $i,A: $i] :
( ( r @ v2 @ v3 )
| ( r @ v2 @ v1 )
| ( r @ B @ A )
| ( ( r @ v3 @ v1 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[15026]) ).
thf(15028,plain,
( ( r @ v2 @ v3 )
| ( r @ v2 @ v1 )
| ( r @ v1 @ v3 ) ),
inference(pattern_uni,[status(thm)],[15027:[bind(A,$thf( v3 )),bind(B,$thf( v1 ))]]) ).
thf(1640,plain,
( ( r @ v1 @ v5 )
| ( r @ v1 @ v3 )
| ( ( r @ v5 @ v3 )
!= ( r @ v1 @ v3 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[1560]) ).
thf(1641,plain,
( ( r @ v1 @ v5 )
| ( r @ v1 @ v3 )
| ( ( r @ v5 @ v3 )
!= ( r @ v1 @ v3 ) ) ),
inference(simp,[status(thm)],[1640]) ).
thf(2380,plain,
! [A: $i] :
( ( A = v1 )
| ( r @ A @ v1 )
| ( r @ A @ v3 )
| ( r @ v1 @ v3 )
| ( v3 != v3 )
| ( A != v4 ) ),
inference(paramod_ordered,[status(thm)],[160,58]) ).
thf(2381,plain,
! [A: $i] :
( ( A = v1 )
| ( r @ A @ v1 )
| ( r @ A @ v3 )
| ( r @ v1 @ v3 )
| ( A != v4 ) ),
inference(simp,[status(thm)],[2380]) ).
thf(2382,plain,
( ( v4 = v1 )
| ( r @ v4 @ v1 )
| ( r @ v4 @ v3 )
| ( r @ v1 @ v3 ) ),
inference(pattern_uni,[status(thm)],[2381:[bind(A,$thf( v4 ))]]) ).
thf(18047,plain,
( ( r @ v4 @ v1 )
| ( r @ v4 @ v3 )
| ( r @ v1 @ v3 ) ),
inference(simplifyReflect,[status(thm)],[2382,52]) ).
thf(18114,plain,
! [B: $i,A: $i] :
( ( r @ v4 @ v1 )
| ( r @ v1 @ v3 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v4 @ v3 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[18047,20]) ).
thf(18115,plain,
! [B: $i,A: $i] :
( ( r @ v4 @ v1 )
| ( r @ v1 @ v3 )
| ( r @ B @ A )
| ( ( r @ v4 @ v3 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[18114]) ).
thf(18116,plain,
( ( r @ v4 @ v1 )
| ( r @ v1 @ v3 )
| ( r @ v3 @ v4 ) ),
inference(pattern_uni,[status(thm)],[18115:[bind(A,$thf( v4 )),bind(B,$thf( v3 ))]]) ).
thf(4,axiom,
v0 != v1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v0nv1) ).
thf(29,plain,
v0 != v1,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(31109,plain,
! [B: $i,A: $i] :
( ( r @ v3 @ v0 )
| ( r @ v0 @ v5 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v3 @ v5 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[31043,20]) ).
thf(31110,plain,
! [B: $i,A: $i] :
( ( r @ v3 @ v0 )
| ( r @ v0 @ v5 )
| ( r @ B @ A )
| ( ( r @ v3 @ v5 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[31109]) ).
thf(31111,plain,
( ( r @ v3 @ v0 )
| ( r @ v0 @ v5 )
| ( r @ v5 @ v3 ) ),
inference(pattern_uni,[status(thm)],[31110:[bind(A,$thf( v3 )),bind(B,$thf( v5 ))]]) ).
thf(5285,plain,
( ~ ( r @ v4 @ v1 )
| ~ ( r @ v1 @ v5 )
| ( ( r @ v4 @ v5 )
!= ( r @ v4 @ v1 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[4911]) ).
thf(5307,plain,
( ~ ( r @ v4 @ v1 )
| ~ ( r @ v1 @ v5 )
| ( ( r @ v4 @ v5 )
!= ( r @ v4 @ v1 ) ) ),
inference(simp,[status(thm)],[5285]) ).
thf(7195,plain,
! [B: $i,A: $i] :
( ~ ( r @ A @ B )
| ~ $true
| ~ ( r @ v1 @ v5 )
| ( ( r @ v4 @ v5 )
!= ( r @ v4 @ v1 ) )
| ( ( r @ B @ A )
!= ( r @ v4 @ v1 ) ) ),
inference(paramod_ordered,[status(thm)],[20,5307]) ).
thf(7196,plain,
! [B: $i,A: $i] :
( ~ ( r @ A @ B )
| ~ ( r @ v1 @ v5 )
| ( ( r @ v4 @ v5 )
!= ( r @ v4 @ v1 ) )
| ( ( r @ B @ A )
!= ( r @ v4 @ v1 ) ) ),
inference(simp,[status(thm)],[7195]) ).
thf(7197,plain,
( ~ ( r @ v1 @ v4 )
| ~ ( r @ v1 @ v5 )
| ( ( r @ v4 @ v5 )
!= ( r @ v4 @ v1 ) ) ),
inference(pattern_uni,[status(thm)],[7196:[bind(A,$thf( v1 )),bind(B,$thf( v4 ))]]) ).
thf(378,plain,
! [A: $i] :
( ( v1 = A )
| ( r @ v1 @ A )
| ( r @ v1 @ v3 )
| ( r @ A @ v3 )
| ( A != v2 )
| ( v3 != v3 ) ),
inference(paramod_ordered,[status(thm)],[158,46]) ).
thf(379,plain,
! [A: $i] :
( ( v1 = A )
| ( r @ v1 @ A )
| ( r @ v1 @ v3 )
| ( r @ A @ v3 )
| ( A != v2 ) ),
inference(pattern_uni,[status(thm)],[378:[]]) ).
thf(514,plain,
( ( v2 = v1 )
| ( r @ v1 @ v2 )
| ( r @ v1 @ v3 )
| ( r @ v2 @ v3 ) ),
inference(simp,[status(thm)],[379]) ).
thf(3259,plain,
( ( r @ v1 @ v2 )
| ( r @ v1 @ v3 )
| ( r @ v2 @ v3 ) ),
inference(simplifyReflect,[status(thm)],[514,37]) ).
thf(3299,plain,
! [B: $i,A: $i] :
( ( r @ v1 @ v2 )
| ( r @ v1 @ v3 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v2 @ v3 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[3259,20]) ).
thf(3300,plain,
! [B: $i,A: $i] :
( ( r @ v1 @ v2 )
| ( r @ v1 @ v3 )
| ( r @ B @ A )
| ( ( r @ v2 @ v3 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[3299]) ).
thf(3301,plain,
( ( r @ v1 @ v2 )
| ( r @ v1 @ v3 )
| ( r @ v3 @ v2 ) ),
inference(pattern_uni,[status(thm)],[3300:[bind(A,$thf( v2 )),bind(B,$thf( v3 ))]]) ).
thf(2082,plain,
( ( r @ v1 @ v5 )
| ( r @ v1 @ v3 )
| ( ( r @ v3 @ v5 )
!= ( r @ v1 @ v3 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[1596]) ).
thf(2083,plain,
( ( r @ v1 @ v5 )
| ( r @ v1 @ v3 )
| ( ( r @ v3 @ v5 )
!= ( r @ v1 @ v3 ) ) ),
inference(simp,[status(thm)],[2082]) ).
thf(1878,plain,
! [A: $i] :
( ( A = v1 )
| ( r @ A @ v3 )
| ( r @ A @ v1 )
| ( r @ v3 @ v1 )
| ( A != v0 )
| ( v3 != v3 ) ),
inference(paramod_ordered,[status(thm)],[159,40]) ).
thf(1879,plain,
! [A: $i] :
( ( A = v1 )
| ( r @ A @ v3 )
| ( r @ A @ v1 )
| ( r @ v3 @ v1 )
| ( A != v0 ) ),
inference(pattern_uni,[status(thm)],[1878:[]]) ).
thf(1950,plain,
( ( v1 = v0 )
| ( r @ v0 @ v3 )
| ( r @ v0 @ v1 )
| ( r @ v3 @ v1 ) ),
inference(simp,[status(thm)],[1879]) ).
thf(30,plain,
v0 != v1,
inference(polarity_switch,[status(thm)],[29]) ).
thf(31,plain,
v1 != v0,
inference(lifteq,[status(thm)],[30]) ).
thf(11890,plain,
( ( r @ v0 @ v3 )
| ( r @ v0 @ v1 )
| ( r @ v3 @ v1 ) ),
inference(simplifyReflect,[status(thm)],[1950,31]) ).
thf(11950,plain,
! [B: $i,A: $i] :
( ( r @ v0 @ v3 )
| ( r @ v0 @ v1 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v3 @ v1 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[11890,20]) ).
thf(11951,plain,
! [B: $i,A: $i] :
( ( r @ v0 @ v3 )
| ( r @ v0 @ v1 )
| ( r @ B @ A )
| ( ( r @ v3 @ v1 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[11950]) ).
thf(11952,plain,
( ( r @ v0 @ v3 )
| ( r @ v0 @ v1 )
| ( r @ v1 @ v3 ) ),
inference(pattern_uni,[status(thm)],[11951:[bind(A,$thf( v3 )),bind(B,$thf( v1 ))]]) ).
thf(3422,plain,
! [A: $i] :
( ( v0 = A )
| ( r @ v3 @ v0 )
| ( r @ v3 @ A )
| ( r @ v0 @ A )
| ( A != v1 )
| ( v3 != v3 ) ),
inference(paramod_ordered,[status(thm)],[161,43]) ).
thf(3423,plain,
! [A: $i] :
( ( v0 = A )
| ( r @ v3 @ v0 )
| ( r @ v3 @ A )
| ( r @ v0 @ A )
| ( A != v1 ) ),
inference(pattern_uni,[status(thm)],[3422:[]]) ).
thf(3769,plain,
( ( v1 = v0 )
| ( r @ v3 @ v0 )
| ( r @ v3 @ v1 )
| ( r @ v0 @ v1 ) ),
inference(simp,[status(thm)],[3423]) ).
thf(33667,plain,
( ( r @ v3 @ v0 )
| ( r @ v3 @ v1 )
| ( r @ v0 @ v1 ) ),
inference(simplifyReflect,[status(thm)],[3769,31]) ).
thf(33733,plain,
! [B: $i,A: $i] :
( ( r @ v3 @ v0 )
| ( r @ v0 @ v1 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v3 @ v1 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[33667,20]) ).
thf(33734,plain,
! [B: $i,A: $i] :
( ( r @ v3 @ v0 )
| ( r @ v0 @ v1 )
| ( r @ B @ A )
| ( ( r @ v3 @ v1 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[33733]) ).
thf(33735,plain,
( ( r @ v3 @ v0 )
| ( r @ v0 @ v1 )
| ( r @ v1 @ v3 ) ),
inference(pattern_uni,[status(thm)],[33734:[bind(A,$thf( v3 )),bind(B,$thf( v1 ))]]) ).
thf(76,plain,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ( B = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( A != v1 )
| ( B != v2 ) ),
inference(paramod_ordered,[status(thm)],[28,37]) ).
thf(77,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( v2 = B )
| ( r @ A @ v2 )
| ( r @ A @ B )
| ( r @ v2 @ B )
| ( A != v1 ) ),
inference(pattern_uni,[status(thm)],[76:[bind(A,$thf( A )),bind(B,$thf( v2 ))]]) ).
thf(165,plain,
! [A: $i] :
( ( v1 = A )
| ( v2 = A )
| ( r @ v1 @ v2 )
| ( r @ v1 @ A )
| ( r @ v2 @ A ) ),
inference(simp,[status(thm)],[77]) ).
thf(16,axiom,
v2 != v5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v2nv5) ).
thf(65,plain,
v2 != v5,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(5020,plain,
! [B: $i,A: $i] :
( ~ ( r @ A @ B )
| ~ $true
| ~ ( r @ v4 @ v5 )
| ~ ( r @ v1 @ v5 )
| ( ( r @ B @ A )
!= ( r @ v4 @ v1 ) ) ),
inference(paramod_ordered,[status(thm)],[20,4911]) ).
thf(5021,plain,
! [B: $i,A: $i] :
( ~ ( r @ A @ B )
| ~ ( r @ v4 @ v5 )
| ~ ( r @ v1 @ v5 )
| ( ( r @ B @ A )
!= ( r @ v4 @ v1 ) ) ),
inference(simp,[status(thm)],[5020]) ).
thf(5022,plain,
( ~ ( r @ v1 @ v4 )
| ~ ( r @ v4 @ v5 )
| ~ ( r @ v1 @ v5 ) ),
inference(pattern_uni,[status(thm)],[5021:[bind(A,$thf( v1 )),bind(B,$thf( v4 ))]]) ).
thf(5962,plain,
( ~ ( r @ v1 @ v4 )
| ~ ( r @ v1 @ v5 )
| ( ( r @ v4 @ v5 )
!= ( r @ v1 @ v4 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[5022]) ).
thf(5988,plain,
( ~ ( r @ v1 @ v4 )
| ~ ( r @ v1 @ v5 )
| ( ( r @ v4 @ v5 )
!= ( r @ v1 @ v4 ) ) ),
inference(simp,[status(thm)],[5962]) ).
thf(451,plain,
! [A: $i] :
( ( v1 = A )
| ( r @ v1 @ A )
| ( r @ v1 @ v3 )
| ( r @ A @ v3 )
| ( A != v0 )
| ( v3 != v3 ) ),
inference(paramod_ordered,[status(thm)],[158,40]) ).
thf(452,plain,
! [A: $i] :
( ( v1 = A )
| ( r @ v1 @ A )
| ( r @ v1 @ v3 )
| ( r @ A @ v3 )
| ( A != v0 ) ),
inference(pattern_uni,[status(thm)],[451:[]]) ).
thf(507,plain,
( ( v1 = v0 )
| ( r @ v1 @ v0 )
| ( r @ v1 @ v3 )
| ( r @ v0 @ v3 ) ),
inference(simp,[status(thm)],[452]) ).
thf(2234,plain,
( ( r @ v1 @ v0 )
| ( r @ v1 @ v3 )
| ( r @ v0 @ v3 ) ),
inference(simplifyReflect,[status(thm)],[507,31]) ).
thf(2269,plain,
! [B: $i,A: $i] :
( ( r @ v1 @ v0 )
| ( r @ v0 @ v3 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v1 @ v3 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[2234,20]) ).
thf(2270,plain,
! [B: $i,A: $i] :
( ( r @ v1 @ v0 )
| ( r @ v0 @ v3 )
| ( r @ B @ A )
| ( ( r @ v1 @ v3 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[2269]) ).
thf(2271,plain,
( ( r @ v1 @ v0 )
| ( r @ v0 @ v3 )
| ( r @ v3 @ v1 ) ),
inference(pattern_uni,[status(thm)],[2270:[bind(A,$thf( v1 )),bind(B,$thf( v3 ))]]) ).
thf(2837,plain,
( ( r @ v1 @ v0 )
| ( r @ v0 @ v3 )
| ( ( r @ v3 @ v1 )
!= ( r @ v1 @ v0 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[2271]) ).
thf(2841,plain,
( ( r @ v1 @ v0 )
| ( r @ v0 @ v3 )
| ( ( r @ v3 @ v1 )
!= ( r @ v1 @ v0 ) ) ),
inference(simp,[status(thm)],[2837]) ).
thf(12,axiom,
v2 != v4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v2nv4) ).
thf(53,plain,
v2 != v4,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(80,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( B = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( A != v1 )
| ( C != v2 ) ),
inference(paramod_ordered,[status(thm)],[28,37]) ).
thf(81,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( B = v2 )
| ( r @ A @ B )
| ( r @ A @ v2 )
| ( r @ B @ v2 )
| ( A != v1 ) ),
inference(pattern_uni,[status(thm)],[80:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( v2 ))]]) ).
thf(169,plain,
! [A: $i] :
( ( v1 = A )
| ( A = v2 )
| ( r @ v1 @ A )
| ( r @ v1 @ v2 )
| ( r @ A @ v2 ) ),
inference(simp,[status(thm)],[81]) ).
thf(3938,plain,
( ( r @ v1 @ v2 )
| ( r @ v1 @ v3 )
| ( ( r @ v3 @ v2 )
!= ( r @ v1 @ v3 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[3301]) ).
thf(3941,plain,
( ( r @ v1 @ v2 )
| ( r @ v1 @ v3 )
| ( ( r @ v3 @ v2 )
!= ( r @ v1 @ v3 ) ) ),
inference(simp,[status(thm)],[3938]) ).
thf(4289,plain,
! [B: $i,A: $i] :
( ( r @ v3 @ v1 )
| ( r @ v3 @ v4 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v4 @ v1 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[4155,20]) ).
thf(4290,plain,
! [B: $i,A: $i] :
( ( r @ v3 @ v1 )
| ( r @ v3 @ v4 )
| ( r @ B @ A )
| ( ( r @ v4 @ v1 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[4289]) ).
thf(4291,plain,
( ( r @ v3 @ v1 )
| ( r @ v3 @ v4 )
| ( r @ v1 @ v4 ) ),
inference(pattern_uni,[status(thm)],[4290:[bind(A,$thf( v4 )),bind(B,$thf( v1 ))]]) ).
thf(86,plain,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ( B = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( B != v2 )
| ( A != v3 ) ),
inference(paramod_ordered,[status(thm)],[28,46]) ).
thf(87,plain,
! [B: $i,A: $i] :
( ( v3 = B )
| ( A = B )
| ( r @ v3 @ A )
| ( r @ v3 @ B )
| ( r @ A @ B )
| ( A != v2 ) ),
inference(pattern_uni,[status(thm)],[86:[bind(A,$thf( v3 ))]]) ).
thf(173,plain,
! [A: $i] :
( ( v3 = A )
| ( v2 = A )
| ( r @ v3 @ v2 )
| ( r @ v3 @ A )
| ( r @ v2 @ A ) ),
inference(simp,[status(thm)],[87]) ).
thf(15283,plain,
! [B: $i,A: $i] :
( ( r @ v2 @ v1 )
| ( r @ v1 @ v3 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v2 @ v3 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[15028,20]) ).
thf(15284,plain,
! [B: $i,A: $i] :
( ( r @ v2 @ v1 )
| ( r @ v1 @ v3 )
| ( r @ B @ A )
| ( ( r @ v2 @ v3 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[15283]) ).
thf(15285,plain,
( ( r @ v2 @ v1 )
| ( r @ v1 @ v3 )
| ( r @ v3 @ v2 ) ),
inference(pattern_uni,[status(thm)],[15284:[bind(A,$thf( v2 )),bind(B,$thf( v3 ))]]) ).
thf(4221,plain,
( ( r @ v4 @ v1 )
| ( r @ v3 @ v1 )
| ( ( r @ v4 @ v3 )
!= ( r @ v4 @ v1 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[4114]) ).
thf(4223,plain,
( ( r @ v4 @ v1 )
| ( r @ v3 @ v1 )
| ( ( r @ v4 @ v3 )
!= ( r @ v4 @ v1 ) ) ),
inference(simp,[status(thm)],[4221]) ).
thf(140,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( B = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( A != v0 )
| ( C != v3 ) ),
inference(paramod_ordered,[status(thm)],[28,40]) ).
thf(141,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( B = v3 )
| ( r @ A @ B )
| ( r @ A @ v3 )
| ( r @ B @ v3 )
| ( A != v0 ) ),
inference(pattern_uni,[status(thm)],[140:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( v3 ))]]) ).
thf(166,plain,
! [A: $i] :
( ( v0 = A )
| ( A = v3 )
| ( r @ v0 @ A )
| ( r @ v0 @ v3 )
| ( r @ A @ v3 ) ),
inference(simp,[status(thm)],[141]) ).
thf(5,axiom,
v0 != v2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v0nv2) ).
thf(32,plain,
v0 != v2,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(33,plain,
v0 != v2,
inference(polarity_switch,[status(thm)],[32]) ).
thf(34,plain,
v2 != v0,
inference(lifteq,[status(thm)],[33]) ).
thf(2317,plain,
( ( r @ v1 @ v0 )
| ( r @ v0 @ v3 )
| ( ( r @ v1 @ v3 )
!= ( r @ v1 @ v0 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[2234]) ).
thf(2319,plain,
( ( r @ v1 @ v0 )
| ( r @ v0 @ v3 )
| ( ( r @ v1 @ v3 )
!= ( r @ v1 @ v0 ) ) ),
inference(simp,[status(thm)],[2317]) ).
thf(20226,plain,
! [B: $i,A: $i] :
( ( r @ v5 @ v1 )
| ( r @ v1 @ v3 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v5 @ v3 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[20162,20]) ).
thf(20227,plain,
! [B: $i,A: $i] :
( ( r @ v5 @ v1 )
| ( r @ v1 @ v3 )
| ( r @ B @ A )
| ( ( r @ v5 @ v3 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[20226]) ).
thf(20228,plain,
( ( r @ v5 @ v1 )
| ( r @ v1 @ v3 )
| ( r @ v3 @ v5 ) ),
inference(pattern_uni,[status(thm)],[20227:[bind(A,$thf( v5 )),bind(B,$thf( v3 ))]]) ).
thf(84,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( A = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( B != v1 )
| ( C != v2 ) ),
inference(paramod_ordered,[status(thm)],[28,37]) ).
thf(85,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( A = v2 )
| ( r @ A @ B )
| ( r @ A @ v2 )
| ( r @ B @ v2 )
| ( B != v1 ) ),
inference(pattern_uni,[status(thm)],[84:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( v2 ))]]) ).
thf(172,plain,
! [A: $i] :
( ( A = v1 )
| ( A = v2 )
| ( r @ A @ v1 )
| ( r @ A @ v2 )
| ( r @ v1 @ v2 ) ),
inference(simp,[status(thm)],[85]) ).
thf(2838,plain,
( ( r @ v1 @ v0 )
| ( r @ v0 @ v3 )
| ( ( r @ v3 @ v1 )
!= ( r @ v0 @ v3 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[2271]) ).
thf(2839,plain,
( ( r @ v1 @ v0 )
| ( r @ v0 @ v3 )
| ( ( r @ v3 @ v1 )
!= ( r @ v0 @ v3 ) ) ),
inference(simp,[status(thm)],[2838]) ).
thf(4876,plain,
( ( r @ v3 @ v1 )
| ( r @ v1 @ v4 )
| ( ( r @ v3 @ v4 )
!= ( r @ v1 @ v4 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[4291]) ).
thf(4882,plain,
( ( r @ v3 @ v1 )
| ( r @ v1 @ v4 )
| ( ( r @ v3 @ v4 )
!= ( r @ v1 @ v4 ) ) ),
inference(simp,[status(thm)],[4876]) ).
thf(3358,plain,
( ( r @ v1 @ v2 )
| ( r @ v1 @ v3 )
| ( ( r @ v2 @ v3 )
!= ( r @ v1 @ v3 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[3259]) ).
thf(3363,plain,
( ( r @ v1 @ v2 )
| ( r @ v1 @ v3 )
| ( ( r @ v2 @ v3 )
!= ( r @ v1 @ v3 ) ) ),
inference(simp,[status(thm)],[3358]) ).
thf(78,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( B = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( C != v1 )
| ( A != v2 ) ),
inference(paramod_ordered,[status(thm)],[28,37]) ).
thf(79,plain,
! [B: $i,A: $i] :
( ( v2 = A )
| ( A = B )
| ( r @ v2 @ A )
| ( r @ v2 @ B )
| ( r @ A @ B )
| ( B != v1 ) ),
inference(pattern_uni,[status(thm)],[78:[bind(A,$thf( v2 ))]]) ).
thf(167,plain,
! [A: $i] :
( ( v2 = A )
| ( A = v1 )
| ( r @ v2 @ A )
| ( r @ v2 @ v1 )
| ( r @ A @ v1 ) ),
inference(simp,[status(thm)],[79]) ).
thf(1162,plain,
( ( r @ v1 @ v4 )
| ( r @ v1 @ v3 )
| ( ( r @ v3 @ v4 )
!= ( r @ v1 @ v4 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[1032]) ).
thf(1166,plain,
( ( r @ v1 @ v4 )
| ( r @ v1 @ v3 )
| ( ( r @ v3 @ v4 )
!= ( r @ v1 @ v4 ) ) ),
inference(simp,[status(thm)],[1162]) ).
thf(136,plain,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ( B = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( A != v0 )
| ( B != v3 ) ),
inference(paramod_ordered,[status(thm)],[28,40]) ).
thf(137,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( v3 = B )
| ( r @ A @ v3 )
| ( r @ A @ B )
| ( r @ v3 @ B )
| ( A != v0 ) ),
inference(pattern_uni,[status(thm)],[136:[bind(A,$thf( A )),bind(B,$thf( v3 ))]]) ).
thf(162,plain,
! [A: $i] :
( ( v0 = A )
| ( v3 = A )
| ( r @ v0 @ v3 )
| ( r @ v0 @ A )
| ( r @ v3 @ A ) ),
inference(simp,[status(thm)],[137]) ).
thf(4875,plain,
( ( r @ v3 @ v1 )
| ( r @ v1 @ v4 )
| ( ( r @ v3 @ v4 )
!= ( r @ v3 @ v1 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[4291]) ).
thf(4879,plain,
( ( r @ v3 @ v1 )
| ( r @ v1 @ v4 )
| ( ( r @ v3 @ v4 )
!= ( r @ v3 @ v1 ) ) ),
inference(simp,[status(thm)],[4875]) ).
thf(66,plain,
v2 != v5,
inference(polarity_switch,[status(thm)],[65]) ).
thf(67,plain,
v5 != v2,
inference(lifteq,[status(thm)],[66]) ).
thf(4800,plain,
! [B: $i,A: $i] :
( ( r @ v3 @ v1 )
| ( r @ v1 @ v4 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v3 @ v4 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[4291,20]) ).
thf(4801,plain,
! [B: $i,A: $i] :
( ( r @ v3 @ v1 )
| ( r @ v1 @ v4 )
| ( r @ B @ A )
| ( ( r @ v3 @ v4 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[4800]) ).
thf(4802,plain,
( ( r @ v3 @ v1 )
| ( r @ v1 @ v4 )
| ( r @ v4 @ v3 ) ),
inference(pattern_uni,[status(thm)],[4801:[bind(A,$thf( v3 )),bind(B,$thf( v4 ))]]) ).
thf(5551,plain,
( ( r @ v3 @ v1 )
| ( r @ v1 @ v4 )
| ( ( r @ v4 @ v3 )
!= ( r @ v3 @ v1 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[4802]) ).
thf(5555,plain,
( ( r @ v3 @ v1 )
| ( r @ v1 @ v4 )
| ( ( r @ v4 @ v3 )
!= ( r @ v3 @ v1 ) ) ),
inference(simp,[status(thm)],[5551]) ).
thf(4348,plain,
( ( r @ v3 @ v1 )
| ( r @ v3 @ v4 )
| ( ( r @ v4 @ v1 )
!= ( r @ v3 @ v1 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[4155]) ).
thf(4351,plain,
( ( r @ v3 @ v1 )
| ( r @ v3 @ v4 )
| ( ( r @ v4 @ v1 )
!= ( r @ v3 @ v1 ) ) ),
inference(simp,[status(thm)],[4348]) ).
thf(2318,plain,
( ( r @ v1 @ v0 )
| ( r @ v0 @ v3 )
| ( ( r @ v1 @ v3 )
!= ( r @ v0 @ v3 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[2234]) ).
thf(2322,plain,
( ( r @ v1 @ v0 )
| ( r @ v0 @ v3 )
| ( ( r @ v1 @ v3 )
!= ( r @ v0 @ v3 ) ) ),
inference(simp,[status(thm)],[2318]) ).
thf(9091,plain,
! [B: $i,A: $i] :
( ( r @ v3 @ v1 )
| ( r @ v1 @ v5 )
| ~ $true
| ( r @ B @ A )
| ( ( r @ v3 @ v5 )
!= ( r @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[8911,20]) ).
thf(9092,plain,
! [B: $i,A: $i] :
( ( r @ v3 @ v1 )
| ( r @ v1 @ v5 )
| ( r @ B @ A )
| ( ( r @ v3 @ v5 )
!= ( r @ A @ B ) ) ),
inference(simp,[status(thm)],[9091]) ).
thf(9093,plain,
( ( r @ v3 @ v1 )
| ( r @ v1 @ v5 )
| ( r @ v5 @ v3 ) ),
inference(pattern_uni,[status(thm)],[9092:[bind(A,$thf( v3 )),bind(B,$thf( v5 ))]]) ).
thf(3357,plain,
( ( r @ v1 @ v2 )
| ( r @ v1 @ v3 )
| ( ( r @ v2 @ v3 )
!= ( r @ v1 @ v2 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[3259]) ).
thf(3359,plain,
( ( r @ v1 @ v2 )
| ( r @ v1 @ v3 )
| ( ( r @ v2 @ v3 )
!= ( r @ v1 @ v2 ) ) ),
inference(simp,[status(thm)],[3357]) ).
thf(3937,plain,
( ( r @ v1 @ v2 )
| ( r @ v1 @ v3 )
| ( ( r @ v3 @ v2 )
!= ( r @ v1 @ v2 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[3301]) ).
thf(3943,plain,
( ( r @ v1 @ v2 )
| ( r @ v1 @ v3 )
| ( ( r @ v3 @ v2 )
!= ( r @ v1 @ v2 ) ) ),
inference(simp,[status(thm)],[3937]) ).
thf(1639,plain,
( ( r @ v1 @ v5 )
| ( r @ v1 @ v3 )
| ( ( r @ v5 @ v3 )
!= ( r @ v1 @ v5 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[1560]) ).
thf(1646,plain,
( ( r @ v1 @ v5 )
| ( r @ v1 @ v3 )
| ( ( r @ v5 @ v3 )
!= ( r @ v1 @ v5 ) ) ),
inference(simp,[status(thm)],[1639]) ).
thf(54,plain,
v2 != v4,
inference(polarity_switch,[status(thm)],[53]) ).
thf(55,plain,
v4 != v2,
inference(lifteq,[status(thm)],[54]) ).
thf(82,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( A = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( C != v1 )
| ( B != v2 ) ),
inference(paramod_ordered,[status(thm)],[28,37]) ).
thf(83,plain,
! [B: $i,A: $i] :
( ( A = v2 )
| ( A = B )
| ( r @ A @ v2 )
| ( r @ A @ B )
| ( r @ v2 @ B )
| ( B != v1 ) ),
inference(pattern_uni,[status(thm)],[82:[bind(A,$thf( A )),bind(B,$thf( v2 ))]]) ).
thf(171,plain,
! [A: $i] :
( ( A = v2 )
| ( A = v1 )
| ( r @ A @ v2 )
| ( r @ A @ v1 )
| ( r @ v2 @ v1 ) ),
inference(simp,[status(thm)],[83]) ).
thf(5963,plain,
( ~ ( r @ v1 @ v4 )
| ~ ( r @ v1 @ v5 )
| ( ( r @ v4 @ v5 )
!= ( r @ v1 @ v5 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[5022]) ).
thf(6007,plain,
( ~ ( r @ v1 @ v4 )
| ~ ( r @ v1 @ v5 )
| ( ( r @ v4 @ v5 )
!= ( r @ v1 @ v5 ) ) ),
inference(simp,[status(thm)],[5963]) ).
thf(142,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ( A = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( C != v0 )
| ( B != v3 ) ),
inference(paramod_ordered,[status(thm)],[28,40]) ).
thf(143,plain,
! [B: $i,A: $i] :
( ( A = v3 )
| ( A = B )
| ( r @ A @ v3 )
| ( r @ A @ B )
| ( r @ v3 @ B )
| ( B != v0 ) ),
inference(pattern_uni,[status(thm)],[142:[bind(A,$thf( A )),bind(B,$thf( v3 ))]]) ).
thf(168,plain,
! [A: $i] :
( ( A = v3 )
| ( A = v0 )
| ( r @ A @ v3 )
| ( r @ A @ v0 )
| ( r @ v3 @ v0 ) ),
inference(simp,[status(thm)],[143]) ).
thf(5552,plain,
( ( r @ v3 @ v1 )
| ( r @ v1 @ v4 )
| ( ( r @ v4 @ v3 )
!= ( r @ v1 @ v4 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[4802]) ).
thf(5559,plain,
( ( r @ v3 @ v1 )
| ( r @ v1 @ v4 )
| ( ( r @ v4 @ v3 )
!= ( r @ v1 @ v4 ) ) ),
inference(simp,[status(thm)],[5552]) ).
thf(74,plain,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ( B = C )
| ( r @ A @ B )
| ( r @ A @ C )
| ( r @ B @ C )
| ( B != v1 )
| ( A != v2 ) ),
inference(paramod_ordered,[status(thm)],[28,37]) ).
thf(75,plain,
! [B: $i,A: $i] :
( ( v2 = B )
| ( A = B )
| ( r @ v2 @ A )
| ( r @ v2 @ B )
| ( r @ A @ B )
| ( A != v1 ) ),
inference(pattern_uni,[status(thm)],[74:[bind(A,$thf( v2 ))]]) ).
thf(163,plain,
! [A: $i] :
( ( v2 = A )
| ( v1 = A )
| ( r @ v2 @ v1 )
| ( r @ v2 @ A )
| ( r @ v1 @ A ) ),
inference(simp,[status(thm)],[75]) ).
thf(5706,plain,
! [A: $i] :
( ( v1 = A )
| ~ ( r @ v4 @ v1 )
| ~ ( r @ v4 @ A )
| ~ ( r @ v1 @ A )
| ~ ( r @ v1 @ v4 )
| ~ ( r @ A @ v5 )
| ~ ( r @ v1 @ v5 )
| ( v4 != v4 ) ),
inference(paramod_ordered,[status(thm)],[866,5022]) ).
thf(5707,plain,
! [A: $i] :
( ( v1 = A )
| ~ ( r @ v4 @ v1 )
| ~ ( r @ v4 @ A )
| ~ ( r @ v1 @ A )
| ~ ( r @ v1 @ v4 )
| ~ ( r @ A @ v5 )
| ~ ( r @ v1 @ v5 ) ),
inference(pattern_uni,[status(thm)],[5706:[]]) ).
thf(2081,plain,
( ( r @ v1 @ v5 )
| ( r @ v1 @ v3 )
| ( ( r @ v3 @ v5 )
!= ( r @ v1 @ v5 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[1596]) ).
thf(2087,plain,
( ( r @ v1 @ v5 )
| ( r @ v1 @ v3 )
| ( ( r @ v3 @ v5 )
!= ( r @ v1 @ v5 ) ) ),
inference(simp,[status(thm)],[2081]) ).
thf(7960,plain,
( ( r @ v5 @ v1 )
| ( r @ v3 @ v1 )
| ( ( r @ v5 @ v3 )
!= ( r @ v3 @ v1 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[7824]) ).
thf(7970,plain,
( ( r @ v5 @ v1 )
| ( r @ v3 @ v1 )
| ( ( r @ v5 @ v3 )
!= ( r @ v3 @ v1 ) ) ),
inference(simp,[status(thm)],[7960]) ).
thf(45676,plain,
$false,
inference(e,[status(thm)],[164,73,1070,7974,58,5320,20162,170,1596,4226,1068,8988,56,7824,1164,14964,174,24,37,25,28377,8911,52,31043,4353,15028,20,46,1641,18116,29,866,18047,61,31111,7197,28308,3301,2083,11952,160,70,33735,21,165,1560,28,38,1032,65,4155,5988,2841,53,169,3941,4291,33667,173,15285,41,4223,166,161,64,32,34,44,59,5022,71,7875,49,2319,159,20228,172,996,2839,4882,4911,3363,167,35,1166,162,2271,2234,4879,50,67,5555,4351,2322,9093,3359,31,4802,3943,43,1646,40,158,55,171,4114,6007,168,19,5559,11890,3259,47,163,68,62,5307,5707,2087,7970]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRA117^1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.12 % 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.26/0.31 % Computer : n019.cluster.edu
% 0.26/0.31 % Model : x86_64 x86_64
% 0.26/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.26/0.31 % Memory : 8046.5625MB
% 0.26/0.31 % OS : Linux 6.8.0-71-generic
% 0.26/0.31 % CPULimit : 300
% 0.26/0.31 % WCLimit : 300
% 0.26/0.31 % DateTime : Tue Sep 29 19:00:32 UTC 2026
% 0.26/0.31 % CPUTime :
% 0.26/0.31 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.97/0.77 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.40/0.93 % [INFO] Parsing done (157ms).
% 1.40/0.95 % [INFO] Running in sequential loop mode.
% 1.96/1.25 % [INFO] eprover registered as external prover.
% 1.96/1.26 % [INFO] Scanning for conjecture ...
% 2.21/1.30 % [INFO] 18 axioms and no conjecture found.
% 2.21/1.35 % [INFO] Problem is higher-order (TPTP THF).
% 2.21/1.35 % [INFO] Type checking passed.
% 2.21/1.35 % [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 ...
% 95.74/22.83 % External prover 'e' found a proof!
% 95.74/22.83 % [INFO] Killing All external provers ...
% 95.74/22.84 % Time passed: 22388ms (effective reasoning time: 21885ms)
% 95.74/22.84 % Axioms used in derivation (18): v4nv5, v3nv4, v1nv4, v1nv2, v1nv5, rno3acl, v0nv1, v2nv4, v0nv5, rsym, v2nv3, v0nv4, v1nv3, v0nv3, v2nv5, v0nv2, rno3cl, v3nv5
% 95.74/22.84 % No. of inferences in proof: 308
% 95.74/22.84 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : 22388 ms resp. 21885 ms w/o parsing
% 90.37/23.05 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 90.37/23.05 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------