%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYN157-1 : TPTP v9.3.1. Released v1.1.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 : n001.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 09:16:54 AM UTC 2026
% Result : Unsatisfiable 176.18s 92.28s
% Output : Refutation 176.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 29
% Syntax : Number of formulae : 171 ( 42 unt; 0 typ; 0 def)
% Number of atoms : 484 ( 46 equ; 0 cnn)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 1351 ( 232 ~; 221 |; 0 &; 898 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 7 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 29 ( 26 usr; 7 con; 0-3 aty)
% Number of variables : 269 ( 0 ^; 269 !; 0 ?; 269 :)
% Comments :
%------------------------------------------------------------------------------
thf(n5_decl,type,
n5: $i > $i > $o ).
thf(d_decl,type,
d: $i ).
thf(k4_decl,type,
k4: $i > $o ).
thf(m0_decl,type,
m0: $i > $i > $i > $o ).
thf(r0_decl,type,
r0: $i > $o ).
thf(p0_decl,type,
p0: $i > $i > $o ).
thf(n0_decl,type,
n0: $i > $i > $o ).
thf(e_decl,type,
e: $i ).
thf(q1_decl,type,
q1: $i > $i > $i > $o ).
thf(c_decl,type,
c: $i ).
thf(q3_decl,type,
q3: $i > $i > $o ).
thf(m1_decl,type,
m1: $i > $i > $i > $o ).
thf(q0_decl,type,
q0: $i > $i > $o ).
thf(m3_decl,type,
m3: $i > $i > $i > $o ).
thf(p2_decl,type,
p2: $i > $i > $i > $o ).
thf(k1_decl,type,
k1: $i > $o ).
thf(p1_decl,type,
p1: $i > $i > $i > $o ).
thf(a_decl,type,
a: $i ).
thf(b_decl,type,
b: $i ).
thf(q2_decl,type,
q2: $i > $i > $i > $o ).
thf(k0_decl,type,
k0: $i > $o ).
thf(l0_decl,type,
l0: $i > $o ).
thf(s0_decl,type,
s0: $i > $o ).
thf(n4_decl,type,
n4: $i > $i > $o ).
thf(r3_decl,type,
r3: $i > $i > $i > $o ).
thf(n2_decl,type,
n2: $i > $o ).
thf(38,axiom,
b @ r0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_9) ).
thf(440,plain,
b @ r0,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(244,axiom,
b @ ( a @ q0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_36) ).
thf(837,plain,
b @ ( a @ q0 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[244]) ).
thf(269,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( c @ ( B @ m1 ) ) )
| ~ ( B @ ( A @ q0 ) )
| ~ ( a @ ( C @ ( a @ m0 ) ) )
| ( B @ ( a @ ( A @ m1 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_024) ).
thf(884,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( c @ ( B @ m1 ) ) )
| ~ ( B @ ( A @ q0 ) )
| ~ ( a @ ( C @ ( a @ m0 ) ) )
| ( B @ ( a @ ( A @ m1 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[269]) ).
thf(885,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( c @ ( B @ m1 ) ) )
| ~ ( B @ ( A @ q0 ) )
| ~ ( a @ ( C @ ( a @ m0 ) ) )
| ( B @ ( a @ ( A @ m1 ) ) ) ),
inference(cnf,[status(esa)],[884]) ).
thf(251,axiom,
! [A: $i] : ( a @ ( A @ ( a @ m0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_12) ).
thf(850,plain,
! [A: $i] : ( a @ ( A @ ( a @ m0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[251]) ).
thf(40404,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( c @ ( B @ m1 ) ) )
| ~ ( B @ ( A @ q0 ) )
| ~ $true
| ( B @ ( a @ ( A @ m1 ) ) ) ),
inference(rewrite,[status(thm)],[885,850]) ).
thf(40405,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( c @ ( B @ m1 ) ) )
| ~ ( B @ ( A @ q0 ) )
| ( B @ ( a @ ( A @ m1 ) ) ) ),
inference(simp,[status(thm)],[40404]) ).
thf(40513,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ q0 ) )
!= ( B @ ( A @ q0 ) ) )
| ~ ( B @ ( c @ ( B @ m1 ) ) )
| ~ $true
| ( B @ ( a @ ( A @ m1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[837,40405]) ).
thf(40514,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ q0 ) )
!= ( B @ ( A @ q0 ) ) )
| ~ ( B @ ( c @ ( B @ m1 ) ) )
| ( B @ ( a @ ( A @ m1 ) ) ) ),
inference(simp,[status(thm)],[40513]) ).
thf(40515,plain,
( ~ ( b @ ( c @ ( b @ m1 ) ) )
| ( b @ ( a @ ( a @ m1 ) ) ) ),
inference(pattern_uni,[status(thm)],[40514:[bind(A,$thf( a )),bind(B,$thf( b ))]]) ).
thf(75,axiom,
! [A: $i] : ( A @ ( b @ p0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_14) ).
thf(511,plain,
! [A: $i] : ( A @ ( b @ p0 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(46,axiom,
! [B: $i,A: $i] :
( ~ ( A @ s0 )
| ~ ( B @ ( A @ p0 ) )
| ( A @ ( B @ ( A @ m1 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_029) ).
thf(455,plain,
! [B: $i,A: $i] :
( ~ ( A @ s0 )
| ~ ( B @ ( A @ p0 ) )
| ( A @ ( B @ ( A @ m1 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(456,plain,
! [B: $i,A: $i] :
( ~ ( A @ s0 )
| ~ ( B @ ( A @ p0 ) )
| ( A @ ( B @ ( A @ m1 ) ) ) ),
inference(cnf,[status(esa)],[455]) ).
thf(6970,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( b @ p0 ) )
!= ( C @ ( B @ p0 ) ) )
| ~ ( B @ s0 )
| ~ $true
| ( B @ ( C @ ( B @ m1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[511,456]) ).
thf(6971,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( b @ p0 ) )
!= ( C @ ( B @ p0 ) ) )
| ~ ( B @ s0 )
| ( B @ ( C @ ( B @ m1 ) ) ) ),
inference(simp,[status(thm)],[6970]) ).
thf(6972,plain,
! [A: $i] :
( ~ ( b @ s0 )
| ( b @ ( A @ ( b @ m1 ) ) ) ),
inference(pattern_uni,[status(thm)],[6971:[bind(A,$thf( A )),bind(B,$thf( b )),bind(C,$thf( A ))]]) ).
thf(58,axiom,
b @ s0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_5) ).
thf(479,plain,
b @ s0,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(7659,plain,
! [A: $i] :
( ~ $true
| ( b @ ( A @ ( b @ m1 ) ) ) ),
inference(rewrite,[status(thm)],[6972,479]) ).
thf(7660,plain,
! [A: $i] : ( b @ ( A @ ( b @ m1 ) ) ),
inference(simp,[status(thm)],[7659]) ).
thf(46601,plain,
( ~ $true
| ( b @ ( a @ ( a @ m1 ) ) ) ),
inference(rewrite,[status(thm)],[40515,7660]) ).
thf(46602,plain,
b @ ( a @ ( a @ m1 ) ),
inference(simp,[status(thm)],[46601]) ).
thf(29,axiom,
b @ k0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_32) ).
thf(425,plain,
b @ k0,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(172,axiom,
a @ l0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_20) ).
thf(699,plain,
a @ l0,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[172]) ).
thf(36,axiom,
! [B: $i,A: $i] :
( ~ ( B @ k0 )
| ~ ( A @ l0 )
| ( A @ ( B @ ( A @ m1 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_021) ).
thf(436,plain,
! [B: $i,A: $i] :
( ~ ( B @ k0 )
| ~ ( A @ l0 )
| ( A @ ( B @ ( A @ m1 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(437,plain,
! [B: $i,A: $i] :
( ~ ( B @ k0 )
| ~ ( A @ l0 )
| ( A @ ( B @ ( A @ m1 ) ) ) ),
inference(cnf,[status(esa)],[436]) ).
thf(4237,plain,
! [B: $i,A: $i] :
( ( ( a @ l0 )
!= ( A @ l0 ) )
| ~ ( B @ k0 )
| ~ $true
| ( A @ ( B @ ( A @ m1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[699,437]) ).
thf(4238,plain,
! [B: $i,A: $i] :
( ( ( a @ l0 )
!= ( A @ l0 ) )
| ~ ( B @ k0 )
| ( A @ ( B @ ( A @ m1 ) ) ) ),
inference(simp,[status(thm)],[4237]) ).
thf(4239,plain,
! [A: $i] :
( ~ ( A @ k0 )
| ( a @ ( A @ ( a @ m1 ) ) ) ),
inference(pattern_uni,[status(thm)],[4238:[bind(A,$thf( a ))]]) ).
thf(4244,plain,
! [A: $i] :
( ~ ( A @ k0 )
| ( a @ ( A @ ( a @ m1 ) ) ) ),
inference(simp,[status(thm)],[4239]) ).
thf(4354,plain,
! [A: $i] :
( ( ( b @ k0 )
!= ( A @ k0 ) )
| ~ $true
| ( a @ ( A @ ( a @ m1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[425,4244]) ).
thf(4355,plain,
! [A: $i] :
( ( ( b @ k0 )
!= ( A @ k0 ) )
| ( a @ ( A @ ( a @ m1 ) ) ) ),
inference(simp,[status(thm)],[4354]) ).
thf(4356,plain,
a @ ( b @ ( a @ m1 ) ),
inference(pattern_uni,[status(thm)],[4355:[bind(A,$thf( b ))]]) ).
thf(166,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( D @ ( C @ m1 ) ) )
| ~ ( A @ ( B @ ( C @ m1 ) ) )
| ( B @ ( B @ ( A @ m1 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_016) ).
thf(687,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( D @ ( C @ m1 ) ) )
| ~ ( A @ ( B @ ( C @ m1 ) ) )
| ( B @ ( B @ ( A @ m1 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[166]) ).
thf(688,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( D @ ( C @ m1 ) ) )
| ~ ( A @ ( B @ ( C @ m1 ) ) )
| ( B @ ( B @ ( A @ m1 ) ) ) ),
inference(cnf,[status(esa)],[687]) ).
thf(26651,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( a @ ( b @ ( a @ m1 ) ) )
!= ( A @ ( B @ ( C @ m1 ) ) ) )
| ~ ( B @ ( D @ ( C @ m1 ) ) )
| ~ $true
| ( B @ ( B @ ( A @ m1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[4356,688]) ).
thf(26652,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( a @ ( b @ ( a @ m1 ) ) )
!= ( A @ ( B @ ( C @ m1 ) ) ) )
| ~ ( B @ ( D @ ( C @ m1 ) ) )
| ( B @ ( B @ ( A @ m1 ) ) ) ),
inference(simp,[status(thm)],[26651]) ).
thf(26653,plain,
! [A: $i] :
( ~ ( b @ ( A @ ( a @ m1 ) ) )
| ( b @ ( b @ ( a @ m1 ) ) ) ),
inference(pattern_uni,[status(thm)],[26652:[bind(A,$thf( a )),bind(B,$thf( b )),bind(C,$thf( a ))]]) ).
thf(26699,plain,
! [A: $i] :
( ~ ( b @ ( A @ ( a @ m1 ) ) )
| ( b @ ( b @ ( a @ m1 ) ) ) ),
inference(simp,[status(thm)],[26653]) ).
thf(61756,plain,
! [A: $i] :
( ( ( b @ ( a @ ( a @ m1 ) ) )
!= ( b @ ( A @ ( a @ m1 ) ) ) )
| ~ $true
| ( b @ ( b @ ( a @ m1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[46602,26699]) ).
thf(61757,plain,
! [A: $i] :
( ( ( b @ ( a @ ( a @ m1 ) ) )
!= ( b @ ( A @ ( a @ m1 ) ) ) )
| ( b @ ( b @ ( a @ m1 ) ) ) ),
inference(simp,[status(thm)],[61756]) ).
thf(61758,plain,
b @ ( b @ ( a @ m1 ) ),
inference(pattern_uni,[status(thm)],[61757:[bind(A,$thf( a ))]]) ).
thf(271,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( B @ ( A @ m1 ) ) )
| ~ ( C @ r0 )
| ( B @ ( A @ ( A @ q1 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_113) ).
thf(888,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( B @ ( A @ m1 ) ) )
| ~ ( C @ r0 )
| ( B @ ( A @ ( A @ q1 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[271]) ).
thf(889,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( B @ ( A @ m1 ) ) )
| ~ ( C @ r0 )
| ( B @ ( A @ ( A @ q1 ) ) ) ),
inference(cnf,[status(esa)],[888]) ).
thf(61974,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( b @ ( a @ m1 ) ) )
!= ( B @ ( B @ ( A @ m1 ) ) ) )
| ~ $true
| ~ ( C @ r0 )
| ( B @ ( A @ ( A @ q1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[61758,889]) ).
thf(61975,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( b @ ( a @ m1 ) ) )
!= ( B @ ( B @ ( A @ m1 ) ) ) )
| ~ ( C @ r0 )
| ( B @ ( A @ ( A @ q1 ) ) ) ),
inference(simp,[status(thm)],[61974]) ).
thf(61976,plain,
! [A: $i] :
( ~ ( A @ r0 )
| ( b @ ( a @ ( a @ q1 ) ) ) ),
inference(pattern_uni,[status(thm)],[61975:[bind(A,$thf( a )),bind(B,$thf( b ))]]) ).
thf(62042,plain,
! [A: $i] :
( ~ ( A @ r0 )
| ( b @ ( a @ ( a @ q1 ) ) ) ),
inference(simp,[status(thm)],[61976]) ).
thf(202,axiom,
b @ ( e @ n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_11) ).
thf(757,plain,
b @ ( e @ n0 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[202]) ).
thf(145,axiom,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ n0 ) )
| ( A @ k1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_001) ).
thf(647,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ n0 ) )
| ( A @ k1 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[145]) ).
thf(648,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ n0 ) )
| ( A @ k1 ) ),
inference(cnf,[status(esa)],[647]) ).
thf(3261,plain,
! [B: $i,A: $i] :
( ( ( b @ ( e @ n0 ) )
!= ( A @ ( B @ n0 ) ) )
| ~ $true
| ( A @ k1 ) ),
inference(paramod_ordered,[status(thm)],[757,648]) ).
thf(3262,plain,
! [B: $i,A: $i] :
( ( ( b @ ( e @ n0 ) )
!= ( A @ ( B @ n0 ) ) )
| ( A @ k1 ) ),
inference(simp,[status(thm)],[3261]) ).
thf(3263,plain,
b @ k1,
inference(pattern_uni,[status(thm)],[3262:[bind(A,$thf( b )),bind(B,$thf( e ))]]) ).
thf(179,axiom,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ m1 ) ) )
| ( A @ ( B @ ( A @ p2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_176) ).
thf(712,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ m1 ) ) )
| ( A @ ( B @ ( A @ p2 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[179]) ).
thf(713,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ m1 ) ) )
| ( A @ ( B @ ( A @ p2 ) ) ) ),
inference(cnf,[status(esa)],[712]) ).
thf(28025,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( A @ ( b @ m1 ) ) )
!= ( C @ ( B @ ( C @ m1 ) ) ) )
| ~ $true
| ( B @ ( C @ ( B @ p2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[7660,713]) ).
thf(28026,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( A @ ( b @ m1 ) ) )
!= ( C @ ( B @ ( C @ m1 ) ) ) )
| ( B @ ( C @ ( B @ p2 ) ) ) ),
inference(simp,[status(thm)],[28025]) ).
thf(28027,plain,
! [A: $i] : ( A @ ( b @ ( A @ p2 ) ) ),
inference(pattern_uni,[status(thm)],[28026:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( b ))]]) ).
thf(153,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ ( e @ p2 ) ) )
| ~ ( C @ k1 )
| ( B @ ( B @ ( A @ p2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_155) ).
thf(663,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ ( e @ p2 ) ) )
| ~ ( C @ k1 )
| ( B @ ( B @ ( A @ p2 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[153]) ).
thf(664,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ ( e @ p2 ) ) )
| ~ ( C @ k1 )
| ( B @ ( B @ ( A @ p2 ) ) ) ),
inference(cnf,[status(esa)],[663]) ).
thf(28863,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( b @ ( A @ p2 ) ) )
!= ( C @ ( B @ ( e @ p2 ) ) ) )
| ~ $true
| ~ ( D @ k1 )
| ( C @ ( C @ ( B @ p2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[28027,664]) ).
thf(28864,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( b @ ( A @ p2 ) ) )
!= ( C @ ( B @ ( e @ p2 ) ) ) )
| ~ ( D @ k1 )
| ( C @ ( C @ ( B @ p2 ) ) ) ),
inference(simp,[status(thm)],[28863]) ).
thf(28865,plain,
! [A: $i] :
( ~ ( A @ k1 )
| ( e @ ( e @ ( b @ p2 ) ) ) ),
inference(pattern_uni,[status(thm)],[28864:[bind(A,$thf( e )),bind(B,$thf( b )),bind(C,$thf( e ))]]) ).
thf(28869,plain,
! [A: $i] :
( ~ ( A @ k1 )
| ( e @ ( e @ ( b @ p2 ) ) ) ),
inference(simp,[status(thm)],[28865]) ).
thf(38824,plain,
! [A: $i] :
( ( ( b @ k1 )
!= ( A @ k1 ) )
| ~ $true
| ( e @ ( e @ ( b @ p2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[3263,28869]) ).
thf(38825,plain,
! [A: $i] :
( ( ( b @ k1 )
!= ( A @ k1 ) )
| ( e @ ( e @ ( b @ p2 ) ) ) ),
inference(simp,[status(thm)],[38824]) ).
thf(38826,plain,
e @ ( e @ ( b @ p2 ) ),
inference(pattern_uni,[status(thm)],[38825:[bind(A,$thf( b ))]]) ).
thf(33,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ ( A @ p2 ) ) )
| ( A @ ( B @ ( A @ r3 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_267) ).
thf(431,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ ( A @ p2 ) ) )
| ( A @ ( B @ ( A @ r3 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(432,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ ( A @ p2 ) ) )
| ( A @ ( B @ ( A @ r3 ) ) ) ),
inference(cnf,[status(esa)],[431]) ).
thf(38941,plain,
! [C: $i,B: $i,A: $i] :
( ( ( e @ ( e @ ( b @ p2 ) ) )
!= ( B @ ( C @ ( A @ p2 ) ) ) )
| ~ $true
| ( A @ ( B @ ( A @ r3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[38826,432]) ).
thf(38942,plain,
! [C: $i,B: $i,A: $i] :
( ( ( e @ ( e @ ( b @ p2 ) ) )
!= ( B @ ( C @ ( A @ p2 ) ) ) )
| ( A @ ( B @ ( A @ r3 ) ) ) ),
inference(simp,[status(thm)],[38941]) ).
thf(38943,plain,
b @ ( e @ ( b @ r3 ) ),
inference(pattern_uni,[status(thm)],[38942:[bind(A,$thf( b )),bind(B,$thf( e )),bind(C,$thf( e ))]]) ).
thf(76,axiom,
! [B: $i,A: $i] :
( ~ ( B @ ( e @ ( A @ r3 ) ) )
| ~ ( B @ ( a @ ( a @ q1 ) ) )
| ~ ( A @ ( A @ q3 ) )
| ( e @ k4 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_276) ).
thf(512,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( e @ ( A @ r3 ) ) )
| ~ ( B @ ( a @ ( a @ q1 ) ) )
| ~ ( A @ ( A @ q3 ) )
| ( e @ k4 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(513,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( e @ ( A @ r3 ) ) )
| ~ ( B @ ( a @ ( a @ q1 ) ) )
| ~ ( A @ ( A @ q3 ) )
| ( e @ k4 ) ),
inference(cnf,[status(esa)],[512]) ).
thf(338,axiom,
d @ s0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
thf(1009,plain,
d @ s0,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[338]) ).
thf(21,axiom,
! [B: $i,A: $i] :
( ~ ( A @ s0 )
| ~ ( B @ s0 )
| ( A @ ( A @ ( A @ p1 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_072) ).
thf(409,plain,
! [B: $i,A: $i] :
( ~ ( A @ s0 )
| ~ ( B @ s0 )
| ( A @ ( A @ ( A @ p1 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(410,plain,
! [B: $i,A: $i] :
( ~ ( A @ s0 )
| ~ ( B @ s0 )
| ( A @ ( A @ ( A @ p1 ) ) ) ),
inference(cnf,[status(esa)],[409]) ).
thf(2602,plain,
! [B: $i,A: $i] :
( ( ( d @ s0 )
!= ( A @ s0 ) )
| ~ $true
| ~ ( B @ s0 )
| ( A @ ( A @ ( A @ p1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[1009,410]) ).
thf(2603,plain,
! [B: $i,A: $i] :
( ( ( d @ s0 )
!= ( A @ s0 ) )
| ~ ( B @ s0 )
| ( A @ ( A @ ( A @ p1 ) ) ) ),
inference(simp,[status(thm)],[2602]) ).
thf(2604,plain,
! [A: $i] :
( ~ ( A @ s0 )
| ( d @ ( d @ ( d @ p1 ) ) ) ),
inference(pattern_uni,[status(thm)],[2603:[bind(A,$thf( d ))]]) ).
thf(2610,plain,
! [A: $i] :
( ~ ( A @ s0 )
| ( d @ ( d @ ( d @ p1 ) ) ) ),
inference(simp,[status(thm)],[2604]) ).
thf(2614,plain,
! [A: $i] :
( ( ( b @ s0 )
!= ( A @ s0 ) )
| ~ $true
| ( d @ ( d @ ( d @ p1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[479,2610]) ).
thf(2615,plain,
! [A: $i] :
( ( ( b @ s0 )
!= ( A @ s0 ) )
| ( d @ ( d @ ( d @ p1 ) ) ) ),
inference(simp,[status(thm)],[2614]) ).
thf(2616,plain,
d @ ( d @ ( d @ p1 ) ),
inference(pattern_uni,[status(thm)],[2615:[bind(A,$thf( b ))]]) ).
thf(112,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ p1 ) ) )
| ( A @ n2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_137) ).
thf(583,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ p1 ) ) )
| ( A @ n2 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[112]) ).
thf(584,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ p1 ) ) )
| ( A @ n2 ) ),
inference(cnf,[status(esa)],[583]) ).
thf(17266,plain,
! [C: $i,B: $i,A: $i] :
( ( ( d @ ( d @ ( d @ p1 ) ) )
!= ( A @ ( C @ ( B @ p1 ) ) ) )
| ~ $true
| ( A @ n2 ) ),
inference(paramod_ordered,[status(thm)],[2616,584]) ).
thf(17267,plain,
! [C: $i,B: $i,A: $i] :
( ( ( d @ ( d @ ( d @ p1 ) ) )
!= ( A @ ( C @ ( B @ p1 ) ) ) )
| ( A @ n2 ) ),
inference(simp,[status(thm)],[17266]) ).
thf(17268,plain,
d @ n2,
inference(pattern_uni,[status(thm)],[17267:[bind(A,$thf( d )),bind(B,$thf( d )),bind(C,$thf( d ))]]) ).
thf(114,axiom,
! [A: $i] :
( ~ ( A @ n2 )
| ( A @ ( A @ ( A @ m3 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_236) ).
thf(586,plain,
! [A: $i] :
( ~ ( A @ n2 )
| ( A @ ( A @ ( A @ m3 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[114]) ).
thf(587,plain,
! [A: $i] :
( ~ ( A @ n2 )
| ( A @ ( A @ ( A @ m3 ) ) ) ),
inference(cnf,[status(esa)],[586]) ).
thf(18381,plain,
! [A: $i] :
( ( ( d @ n2 )
!= ( A @ n2 ) )
| ~ $true
| ( A @ ( A @ ( A @ m3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[17268,587]) ).
thf(18382,plain,
! [A: $i] :
( ( ( d @ n2 )
!= ( A @ n2 ) )
| ( A @ ( A @ ( A @ m3 ) ) ) ),
inference(simp,[status(thm)],[18381]) ).
thf(18383,plain,
d @ ( d @ ( d @ m3 ) ),
inference(pattern_uni,[status(thm)],[18382:[bind(A,$thf( d ))]]) ).
thf(27,axiom,
! [B: $i,A: $i] :
( ~ ( A @ ( A @ ( A @ m3 ) ) )
| ~ ( B @ k4 )
| ( A @ ( A @ n4 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_284) ).
thf(421,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( A @ ( A @ m3 ) ) )
| ~ ( B @ k4 )
| ( A @ ( A @ n4 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(422,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( A @ ( A @ m3 ) ) )
| ~ ( B @ k4 )
| ( A @ ( A @ n4 ) ) ),
inference(cnf,[status(esa)],[421]) ).
thf(18428,plain,
! [B: $i,A: $i] :
( ( ( d @ ( d @ ( d @ m3 ) ) )
!= ( A @ ( A @ ( A @ m3 ) ) ) )
| ~ $true
| ~ ( B @ k4 )
| ( A @ ( A @ n4 ) ) ),
inference(paramod_ordered,[status(thm)],[18383,422]) ).
thf(18429,plain,
! [B: $i,A: $i] :
( ( ( d @ ( d @ ( d @ m3 ) ) )
!= ( A @ ( A @ ( A @ m3 ) ) ) )
| ~ ( B @ k4 )
| ( A @ ( A @ n4 ) ) ),
inference(simp,[status(thm)],[18428]) ).
thf(18430,plain,
! [A: $i] :
( ~ ( A @ k4 )
| ( d @ ( d @ n4 ) ) ),
inference(pattern_uni,[status(thm)],[18429:[bind(A,$thf( d ))]]) ).
thf(18432,plain,
! [A: $i] :
( ~ ( A @ k4 )
| ( d @ ( d @ n4 ) ) ),
inference(simp,[status(thm)],[18430]) ).
thf(314,axiom,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ n4 ) )
| ( A @ ( A @ n5 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_309) ).
thf(967,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ n4 ) )
| ( A @ ( A @ n5 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[314]) ).
thf(968,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ n4 ) )
| ( A @ ( A @ n5 ) ) ),
inference(cnf,[status(esa)],[967]) ).
thf(47333,plain,
! [C: $i,B: $i,A: $i] :
( ( ( d @ ( d @ n4 ) )
!= ( B @ ( C @ n4 ) ) )
| ~ $true
| ( B @ ( B @ n5 ) )
| ~ ( A @ k4 ) ),
inference(paramod_ordered,[status(thm)],[18432,968]) ).
thf(47334,plain,
! [C: $i,B: $i,A: $i] :
( ( ( d @ ( d @ n4 ) )
!= ( B @ ( C @ n4 ) ) )
| ( B @ ( B @ n5 ) )
| ~ ( A @ k4 ) ),
inference(simp,[status(thm)],[47333]) ).
thf(47335,plain,
! [A: $i] :
( ( d @ ( d @ n5 ) )
| ~ ( A @ k4 ) ),
inference(pattern_uni,[status(thm)],[47334:[bind(A,$thf( A )),bind(B,$thf( d )),bind(C,$thf( d ))]]) ).
thf(1,negated_conjecture,
! [A: $i] :
~ ( d @ ( A @ n5 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
thf(370,plain,
! [A: $i] :
~ ( d @ ( A @ n5 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(371,plain,
! [A: $i] :
~ ( d @ ( A @ n5 ) ),
inference(polarity_switch,[status(thm)],[370]) ).
thf(49050,plain,
! [A: $i] :
( $false
| ~ ( A @ k4 ) ),
inference(rewrite,[status(thm)],[47335,371]) ).
thf(49051,plain,
! [A: $i] :
~ ( A @ k4 ),
inference(simp,[status(thm)],[49050]) ).
thf(49054,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( e @ ( A @ r3 ) ) )
| ~ ( B @ ( a @ ( a @ q1 ) ) )
| ~ ( A @ ( A @ q3 ) )
| $false ),
inference(rewrite,[status(thm)],[513,49051]) ).
thf(49055,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( e @ ( A @ r3 ) ) )
| ~ ( B @ ( a @ ( a @ q1 ) ) )
| ~ ( A @ ( A @ q3 ) ) ),
inference(simp,[status(thm)],[49054]) ).
thf(49174,plain,
! [B: $i,A: $i] :
( ( ( b @ ( e @ ( b @ r3 ) ) )
!= ( B @ ( e @ ( A @ r3 ) ) ) )
| ~ $true
| ~ ( B @ ( a @ ( a @ q1 ) ) )
| ~ ( A @ ( A @ q3 ) ) ),
inference(paramod_ordered,[status(thm)],[38943,49055]) ).
thf(49175,plain,
! [B: $i,A: $i] :
( ( ( b @ ( e @ ( b @ r3 ) ) )
!= ( B @ ( e @ ( A @ r3 ) ) ) )
| ~ ( B @ ( a @ ( a @ q1 ) ) )
| ~ ( A @ ( A @ q3 ) ) ),
inference(simp,[status(thm)],[49174]) ).
thf(49176,plain,
( ~ ( b @ ( a @ ( a @ q1 ) ) )
| ~ ( b @ ( b @ q3 ) ) ),
inference(pattern_uni,[status(thm)],[49175:[bind(A,$thf( b )),bind(B,$thf( b ))]]) ).
thf(31,axiom,
e @ ( b @ q0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_21) ).
thf(428,plain,
e @ ( b @ q0 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(47,axiom,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ q0 ) )
| ( A @ ( A @ ( A @ p1 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_067) ).
thf(457,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ q0 ) )
| ( A @ ( A @ ( A @ p1 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(458,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ q0 ) )
| ( A @ ( A @ ( A @ p1 ) ) ) ),
inference(cnf,[status(esa)],[457]) ).
thf(7592,plain,
! [B: $i,A: $i] :
( ( ( e @ ( b @ q0 ) )
!= ( A @ ( B @ q0 ) ) )
| ~ $true
| ( A @ ( A @ ( A @ p1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[428,458]) ).
thf(7593,plain,
! [B: $i,A: $i] :
( ( ( e @ ( b @ q0 ) )
!= ( A @ ( B @ q0 ) ) )
| ( A @ ( A @ ( A @ p1 ) ) ) ),
inference(simp,[status(thm)],[7592]) ).
thf(7594,plain,
e @ ( e @ ( e @ p1 ) ),
inference(pattern_uni,[status(thm)],[7593:[bind(A,$thf( e )),bind(B,$thf( b ))]]) ).
thf(57,axiom,
! [B: $i,A: $i] :
( ~ ( A @ ( A @ ( A @ p1 ) ) )
| ~ ( B @ k0 )
| ( B @ ( B @ ( A @ q2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_177) ).
thf(477,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( A @ ( A @ p1 ) ) )
| ~ ( B @ k0 )
| ( B @ ( B @ ( A @ q2 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(478,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( A @ ( A @ p1 ) ) )
| ~ ( B @ k0 )
| ( B @ ( B @ ( A @ q2 ) ) ) ),
inference(cnf,[status(esa)],[477]) ).
thf(13650,plain,
! [B: $i,A: $i] :
( ( ( e @ ( e @ ( e @ p1 ) ) )
!= ( A @ ( A @ ( A @ p1 ) ) ) )
| ~ $true
| ~ ( B @ k0 )
| ( B @ ( B @ ( A @ q2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[7594,478]) ).
thf(13651,plain,
! [B: $i,A: $i] :
( ( ( e @ ( e @ ( e @ p1 ) ) )
!= ( A @ ( A @ ( A @ p1 ) ) ) )
| ~ ( B @ k0 )
| ( B @ ( B @ ( A @ q2 ) ) ) ),
inference(simp,[status(thm)],[13650]) ).
thf(13652,plain,
! [A: $i] :
( ~ ( A @ k0 )
| ( A @ ( A @ ( e @ q2 ) ) ) ),
inference(pattern_uni,[status(thm)],[13651:[bind(A,$thf( e ))]]) ).
thf(13679,plain,
! [A: $i] :
( ~ ( A @ k0 )
| ( A @ ( A @ ( e @ q2 ) ) ) ),
inference(simp,[status(thm)],[13652]) ).
thf(14724,plain,
! [A: $i] :
( ( ( b @ k0 )
!= ( A @ k0 ) )
| ~ $true
| ( A @ ( A @ ( e @ q2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[425,13679]) ).
thf(14725,plain,
! [A: $i] :
( ( ( b @ k0 )
!= ( A @ k0 ) )
| ( A @ ( A @ ( e @ q2 ) ) ) ),
inference(simp,[status(thm)],[14724]) ).
thf(14726,plain,
b @ ( b @ ( e @ q2 ) ),
inference(pattern_uni,[status(thm)],[14725:[bind(A,$thf( b ))]]) ).
thf(207,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ n0 ) )
| ~ ( B @ ( A @ ( C @ q2 ) ) )
| ( B @ ( A @ q3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_255) ).
thf(766,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ n0 ) )
| ~ ( B @ ( A @ ( C @ q2 ) ) )
| ( B @ ( A @ q3 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[207]) ).
thf(767,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ n0 ) )
| ~ ( B @ ( A @ ( C @ q2 ) ) )
| ( B @ ( A @ q3 ) ) ),
inference(cnf,[status(esa)],[766]) ).
thf(32014,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( b @ ( e @ q2 ) ) )
!= ( B @ ( A @ ( C @ q2 ) ) ) )
| ~ ( A @ ( C @ n0 ) )
| ~ $true
| ( B @ ( A @ q3 ) ) ),
inference(paramod_ordered,[status(thm)],[14726,767]) ).
thf(32015,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( b @ ( e @ q2 ) ) )
!= ( B @ ( A @ ( C @ q2 ) ) ) )
| ~ ( A @ ( C @ n0 ) )
| ( B @ ( A @ q3 ) ) ),
inference(simp,[status(thm)],[32014]) ).
thf(32016,plain,
( ~ ( b @ ( e @ n0 ) )
| ( b @ ( b @ q3 ) ) ),
inference(pattern_uni,[status(thm)],[32015:[bind(A,$thf( b )),bind(B,$thf( b )),bind(C,$thf( e ))]]) ).
thf(33322,plain,
( ~ $true
| ( b @ ( b @ q3 ) ) ),
inference(rewrite,[status(thm)],[32016,757]) ).
thf(33323,plain,
b @ ( b @ q3 ),
inference(simp,[status(thm)],[33322]) ).
thf(49354,plain,
( ~ ( b @ ( a @ ( a @ q1 ) ) )
| ~ $true ),
inference(rewrite,[status(thm)],[49176,33323]) ).
thf(49355,plain,
~ ( b @ ( a @ ( a @ q1 ) ) ),
inference(simp,[status(thm)],[49354]) ).
thf(62231,plain,
! [A: $i] :
( ~ ( A @ r0 )
| $false ),
inference(rewrite,[status(thm)],[62042,49355]) ).
thf(62232,plain,
! [A: $i] :
~ ( A @ r0 ),
inference(simp,[status(thm)],[62231]) ).
thf(62233,plain,
$false,
inference(rewrite,[status(thm)],[440,62232]) ).
thf(62234,plain,
$false,
inference(simp,[status(thm)],[62233]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN157-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.16/0.40 % Computer : n001.cluster.edu
% 0.16/0.40 % Model : x86_64 x86_64
% 0.16/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.40 % Memory : 8046.5625MB
% 0.16/0.40 % OS : Linux 6.8.0-71-generic
% 0.16/0.40 % CPULimit : 300
% 0.16/0.40 % WCLimit : 300
% 0.16/0.40 % DateTime : Sat Sep 26 17:22:28 UTC 2026
% 0.16/0.40 % CPUTime :
% 0.16/0.40 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.84/0.98 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.38/1.28 % [INFO] Parsing done (292ms).
% 1.38/1.29 % [INFO] Running in sequential loop mode.
% 2.68/1.69 % [INFO] eprover registered as external prover.
% 2.68/1.69 % [INFO] Scanning for conjecture ...
% 3.12/1.83 % [INFO] Found a conjecture (or negated_conjecture) and 368 axioms. Running axiom selection ...
% 3.33/1.98 % [INFO] Axiom selection finished. Selected 368 axioms (removed 0 axioms).
% 4.16/2.15 % [INFO] Problem is propositional (TPTP CNF).
% 4.16/2.16 % [INFO] Type checking passed.
% 4.16/2.17 % [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 ...
% 176.18/92.27 % [INFO] Killing All external provers ...
% 176.18/92.27 % Time passed: 91730ms (effective reasoning time: 90974ms)
% 176.18/92.28 % Axioms used in derivation (28): rule_067, rule_276, rule_113, axiom_21, rule_309, rule_016, rule_284, axiom_1, rule_177, axiom_5, axiom_11, axiom_12, axiom_9, rule_001, axiom_32, rule_176, axiom_20, rule_137, rule_155, axiom_36, rule_267, rule_021, rule_024, rule_029, rule_236, axiom_14, rule_255, rule_072
% 176.18/92.28 % No. of inferences in proof: 171
% 176.18/92.28 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : 91730 ms resp. 90974 ms w/o parsing
% 176.44/92.33 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 176.44/92.34 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------