%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYN212-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 : n007.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:17:00 AM UTC 2026
% Result : Unsatisfiable 206.19s 119.01s
% Output : Refutation 206.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 15
% Syntax : Number of formulae : 89 ( 24 unt; 0 typ; 0 def)
% Number of atoms : 244 ( 28 equ; 0 cnn)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 667 ( 102 ~; 99 |; 0 &; 466 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 18 ( 15 usr; 5 con; 0-3 aty)
% Number of variables : 148 ( 0 ^; 148 !; 0 ?; 148 :)
% Comments :
%------------------------------------------------------------------------------
thf(s4_decl,type,
s4: $i > $o ).
thf(e_decl,type,
e: $i ).
thf(n0_decl,type,
n0: $i > $i > $o ).
thf(p3_decl,type,
p3: $i > $i > $i > $o ).
thf(m3_decl,type,
m3: $i > $i > $i > $o ).
thf(m0_decl,type,
m0: $i > $i > $i > $o ).
thf(d_decl,type,
d: $i ).
thf(a_decl,type,
a: $i ).
thf(q1_decl,type,
q1: $i > $i > $i > $o ).
thf(m1_decl,type,
m1: $i > $i > $i > $o ).
thf(p2_decl,type,
p2: $i > $i > $i > $o ).
thf(k1_decl,type,
k1: $i > $o ).
thf(k0_decl,type,
k0: $i > $o ).
thf(l0_decl,type,
l0: $i > $o ).
thf(l1_decl,type,
l1: $i > $i > $o ).
thf(299,axiom,
e @ ( e @ n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_30) ).
thf(939,plain,
e @ ( e @ n0 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[299]) ).
thf(57,axiom,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ n0 ) )
| ( A @ ( A @ l1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_002) ).
thf(476,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ n0 ) )
| ( A @ ( A @ l1 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(477,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ n0 ) )
| ( A @ ( A @ l1 ) ) ),
inference(cnf,[status(esa)],[476]) ).
thf(7411,plain,
! [B: $i,A: $i] :
( ( ( e @ ( e @ n0 ) )
!= ( A @ ( B @ n0 ) ) )
| ~ $true
| ( A @ ( A @ l1 ) ) ),
inference(paramod_ordered,[status(thm)],[939,477]) ).
thf(7412,plain,
! [B: $i,A: $i] :
( ( ( e @ ( e @ n0 ) )
!= ( A @ ( B @ n0 ) ) )
| ( A @ ( A @ l1 ) ) ),
inference(simp,[status(thm)],[7411]) ).
thf(7413,plain,
e @ ( e @ l1 ),
inference(pattern_uni,[status(thm)],[7412:[bind(A,$thf( e )),bind(B,$thf( e ))]]) ).
thf(204,axiom,
! [B: $i,A: $i] : ( B @ ( d @ ( A @ m0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_19) ).
thf(759,plain,
! [B: $i,A: $i] : ( B @ ( d @ ( A @ m0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[204]) ).
thf(105,axiom,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ ( A @ m0 ) ) )
| ( A @ ( A @ ( A @ q1 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_122) ).
thf(566,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ ( A @ m0 ) ) )
| ( A @ ( A @ ( A @ q1 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[105]) ).
thf(567,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ ( A @ m0 ) ) )
| ( A @ ( A @ ( A @ q1 ) ) ) ),
inference(cnf,[status(esa)],[566]) ).
thf(13963,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( d @ ( A @ m0 ) ) )
!= ( C @ ( D @ ( C @ m0 ) ) ) )
| ~ $true
| ( C @ ( C @ ( C @ q1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[759,567]) ).
thf(13964,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( d @ ( A @ m0 ) ) )
!= ( C @ ( D @ ( C @ m0 ) ) ) )
| ( C @ ( C @ ( C @ q1 ) ) ) ),
inference(simp,[status(thm)],[13963]) ).
thf(13965,plain,
! [A: $i] : ( A @ ( A @ ( A @ q1 ) ) ),
inference(pattern_uni,[status(thm)],[13964:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( d ))]]) ).
thf(13985,plain,
! [A: $i] : ( A @ ( A @ ( A @ q1 ) ) ),
inference(simp,[status(thm)],[13965]) ).
thf(147,axiom,
! [A: $i] :
( ~ ( A @ ( A @ ( A @ q1 ) ) )
| ( A @ ( A @ ( A @ p2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_154) ).
thf(649,plain,
! [A: $i] :
( ~ ( A @ ( A @ ( A @ q1 ) ) )
| ( A @ ( A @ ( A @ p2 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[147]) ).
thf(650,plain,
! [A: $i] :
( ~ ( A @ ( A @ ( A @ q1 ) ) )
| ( A @ ( A @ ( A @ p2 ) ) ) ),
inference(cnf,[status(esa)],[649]) ).
thf(19367,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ q1 ) ) )
!= ( B @ ( B @ ( B @ q1 ) ) ) )
| ~ $true
| ( B @ ( B @ ( B @ p2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[13985,650]) ).
thf(19368,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ q1 ) ) )
!= ( B @ ( B @ ( B @ q1 ) ) ) )
| ( B @ ( B @ ( B @ p2 ) ) ) ),
inference(simp,[status(thm)],[19367]) ).
thf(19369,plain,
! [A: $i] : ( A @ ( A @ ( A @ p2 ) ) ),
inference(pattern_uni,[status(thm)],[19368:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(187,axiom,
! [A: $i] :
( ~ ( A @ ( A @ ( A @ p2 ) ) )
| ( A @ ( A @ ( A @ m3 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_238) ).
thf(726,plain,
! [A: $i] :
( ~ ( A @ ( A @ ( A @ p2 ) ) )
| ( A @ ( A @ ( A @ m3 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[187]) ).
thf(727,plain,
! [A: $i] :
( ~ ( A @ ( A @ ( A @ p2 ) ) )
| ( A @ ( A @ ( A @ m3 ) ) ) ),
inference(cnf,[status(esa)],[726]) ).
thf(26469,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ p2 ) ) )
!= ( B @ ( B @ ( B @ p2 ) ) ) )
| ~ $true
| ( B @ ( B @ ( B @ m3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[19369,727]) ).
thf(26470,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ p2 ) ) )
!= ( B @ ( B @ ( B @ p2 ) ) ) )
| ( B @ ( B @ ( B @ m3 ) ) ) ),
inference(simp,[status(thm)],[26469]) ).
thf(26471,plain,
! [A: $i] : ( A @ ( A @ ( A @ m3 ) ) ),
inference(pattern_uni,[status(thm)],[26470:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(149,axiom,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ n0 ) )
| ( A @ k1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_001) ).
thf(653,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ n0 ) )
| ( A @ k1 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[149]) ).
thf(654,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ n0 ) )
| ( A @ k1 ) ),
inference(cnf,[status(esa)],[653]) ).
thf(2955,plain,
! [B: $i,A: $i] :
( ( ( e @ ( e @ n0 ) )
!= ( A @ ( B @ n0 ) ) )
| ~ $true
| ( A @ k1 ) ),
inference(paramod_ordered,[status(thm)],[939,654]) ).
thf(2956,plain,
! [B: $i,A: $i] :
( ( ( e @ ( e @ n0 ) )
!= ( A @ ( B @ n0 ) ) )
| ( A @ k1 ) ),
inference(simp,[status(thm)],[2955]) ).
thf(2957,plain,
e @ k1,
inference(pattern_uni,[status(thm)],[2956:[bind(A,$thf( e )),bind(B,$thf( e ))]]) ).
thf(319,axiom,
e @ k0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_28) ).
thf(976,plain,
e @ k0,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[319]) ).
thf(175,axiom,
a @ l0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_20) ).
thf(703,plain,
a @ l0,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[175]) ).
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(438,plain,
! [B: $i,A: $i] :
( ~ ( B @ k0 )
| ~ ( A @ l0 )
| ( A @ ( B @ ( A @ m1 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(439,plain,
! [B: $i,A: $i] :
( ~ ( B @ k0 )
| ~ ( A @ l0 )
| ( A @ ( B @ ( A @ m1 ) ) ) ),
inference(cnf,[status(esa)],[438]) ).
thf(4165,plain,
! [B: $i,A: $i] :
( ( ( a @ l0 )
!= ( A @ l0 ) )
| ~ ( B @ k0 )
| ~ $true
| ( A @ ( B @ ( A @ m1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[703,439]) ).
thf(4166,plain,
! [B: $i,A: $i] :
( ( ( a @ l0 )
!= ( A @ l0 ) )
| ~ ( B @ k0 )
| ( A @ ( B @ ( A @ m1 ) ) ) ),
inference(simp,[status(thm)],[4165]) ).
thf(4167,plain,
! [A: $i] :
( ~ ( A @ k0 )
| ( a @ ( A @ ( a @ m1 ) ) ) ),
inference(pattern_uni,[status(thm)],[4166:[bind(A,$thf( a ))]]) ).
thf(4178,plain,
! [A: $i] :
( ~ ( A @ k0 )
| ( a @ ( A @ ( a @ m1 ) ) ) ),
inference(simp,[status(thm)],[4167]) ).
thf(4880,plain,
! [A: $i] :
( ( ( e @ k0 )
!= ( A @ k0 ) )
| ~ $true
| ( a @ ( A @ ( a @ m1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[976,4178]) ).
thf(4881,plain,
! [A: $i] :
( ( ( e @ k0 )
!= ( A @ k0 ) )
| ( a @ ( A @ ( a @ m1 ) ) ) ),
inference(simp,[status(thm)],[4880]) ).
thf(4882,plain,
a @ ( e @ ( a @ m1 ) ),
inference(pattern_uni,[status(thm)],[4881:[bind(A,$thf( e ))]]) ).
thf(182,axiom,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ m1 ) ) )
| ( A @ ( B @ ( A @ p2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_176) ).
thf(716,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ m1 ) ) )
| ( A @ ( B @ ( A @ p2 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[182]) ).
thf(717,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ m1 ) ) )
| ( A @ ( B @ ( A @ p2 ) ) ) ),
inference(cnf,[status(esa)],[716]) ).
thf(24976,plain,
! [B: $i,A: $i] :
( ( ( a @ ( e @ ( a @ m1 ) ) )
!= ( B @ ( A @ ( B @ m1 ) ) ) )
| ~ $true
| ( A @ ( B @ ( A @ p2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[4882,717]) ).
thf(24977,plain,
! [B: $i,A: $i] :
( ( ( a @ ( e @ ( a @ m1 ) ) )
!= ( B @ ( A @ ( B @ m1 ) ) ) )
| ( A @ ( B @ ( A @ p2 ) ) ) ),
inference(simp,[status(thm)],[24976]) ).
thf(24978,plain,
e @ ( a @ ( e @ p2 ) ),
inference(pattern_uni,[status(thm)],[24977:[bind(A,$thf( e )),bind(B,$thf( a ))]]) ).
thf(326,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(988,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)],[326]) ).
thf(989,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ ( e @ p2 ) ) )
| ~ ( C @ k1 )
| ( B @ ( B @ ( A @ p2 ) ) ) ),
inference(cnf,[status(esa)],[988]) ).
thf(48457,plain,
! [C: $i,B: $i,A: $i] :
( ( ( e @ ( a @ ( e @ p2 ) ) )
!= ( B @ ( A @ ( e @ p2 ) ) ) )
| ~ $true
| ~ ( C @ k1 )
| ( B @ ( B @ ( A @ p2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[24978,989]) ).
thf(48458,plain,
! [C: $i,B: $i,A: $i] :
( ( ( e @ ( a @ ( e @ p2 ) ) )
!= ( B @ ( A @ ( e @ p2 ) ) ) )
| ~ ( C @ k1 )
| ( B @ ( B @ ( A @ p2 ) ) ) ),
inference(simp,[status(thm)],[48457]) ).
thf(48459,plain,
! [A: $i] :
( ~ ( A @ k1 )
| ( e @ ( e @ ( a @ p2 ) ) ) ),
inference(pattern_uni,[status(thm)],[48458:[bind(A,$thf( a )),bind(B,$thf( e ))]]) ).
thf(48776,plain,
! [A: $i] :
( ~ ( A @ k1 )
| ( e @ ( e @ ( a @ p2 ) ) ) ),
inference(simp,[status(thm)],[48459]) ).
thf(49243,plain,
! [A: $i] :
( ( ( e @ k1 )
!= ( A @ k1 ) )
| ~ $true
| ( e @ ( e @ ( a @ p2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[2957,48776]) ).
thf(49244,plain,
! [A: $i] :
( ( ( e @ k1 )
!= ( A @ k1 ) )
| ( e @ ( e @ ( a @ p2 ) ) ) ),
inference(simp,[status(thm)],[49243]) ).
thf(49245,plain,
e @ ( e @ ( a @ p2 ) ),
inference(pattern_uni,[status(thm)],[49244:[bind(A,$thf( e ))]]) ).
thf(188,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( B @ ( A @ p2 ) ) )
| ~ ( D @ ( C @ ( B @ m3 ) ) )
| ( B @ ( B @ ( A @ p3 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_251) ).
thf(728,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( B @ ( A @ p2 ) ) )
| ~ ( D @ ( C @ ( B @ m3 ) ) )
| ( B @ ( B @ ( A @ p3 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[188]) ).
thf(729,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( B @ ( A @ p2 ) ) )
| ~ ( D @ ( C @ ( B @ m3 ) ) )
| ( B @ ( B @ ( A @ p3 ) ) ) ),
inference(cnf,[status(esa)],[728]) ).
thf(49335,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( e @ ( e @ ( a @ p2 ) ) )
!= ( D @ ( B @ ( A @ p2 ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ m3 ) ) )
| ( B @ ( B @ ( A @ p3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[49245,729]) ).
thf(49336,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( e @ ( e @ ( a @ p2 ) ) )
!= ( D @ ( B @ ( A @ p2 ) ) ) )
| ~ ( D @ ( C @ ( B @ m3 ) ) )
| ( B @ ( B @ ( A @ p3 ) ) ) ),
inference(simp,[status(thm)],[49335]) ).
thf(49337,plain,
! [A: $i] :
( ~ ( e @ ( A @ ( e @ m3 ) ) )
| ( e @ ( e @ ( a @ p3 ) ) ) ),
inference(pattern_uni,[status(thm)],[49336:[bind(A,$thf( a )),bind(B,$thf( e )),bind(C,$thf( C )),bind(D,$thf( e ))]]) ).
thf(49392,plain,
! [A: $i] :
( ~ ( e @ ( A @ ( e @ m3 ) ) )
| ( e @ ( e @ ( a @ p3 ) ) ) ),
inference(simp,[status(thm)],[49337]) ).
thf(71770,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ m3 ) ) )
!= ( e @ ( B @ ( e @ m3 ) ) ) )
| ~ $true
| ( e @ ( e @ ( a @ p3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[26471,49392]) ).
thf(71771,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ m3 ) ) )
!= ( e @ ( B @ ( e @ m3 ) ) ) )
| ( e @ ( e @ ( a @ p3 ) ) ) ),
inference(simp,[status(thm)],[71770]) ).
thf(71772,plain,
e @ ( e @ ( a @ p3 ) ),
inference(pattern_uni,[status(thm)],[71771:[bind(A,$thf( e )),bind(B,$thf( e ))]]) ).
thf(317,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ l1 ) )
| ~ ( D @ ( C @ ( B @ p3 ) ) )
| ( A @ s4 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_299) ).
thf(972,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ l1 ) )
| ~ ( D @ ( C @ ( B @ p3 ) ) )
| ( A @ s4 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[317]) ).
thf(973,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ l1 ) )
| ~ ( D @ ( C @ ( B @ p3 ) ) )
| ( A @ s4 ) ),
inference(cnf,[status(esa)],[972]) ).
thf(71841,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( e @ ( e @ ( a @ p3 ) ) )
!= ( D @ ( C @ ( B @ p3 ) ) ) )
| ~ ( C @ ( A @ l1 ) )
| ~ $true
| ( A @ s4 ) ),
inference(paramod_ordered,[status(thm)],[71772,973]) ).
thf(71842,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( e @ ( e @ ( a @ p3 ) ) )
!= ( D @ ( C @ ( B @ p3 ) ) ) )
| ~ ( C @ ( A @ l1 ) )
| ( A @ s4 ) ),
inference(simp,[status(thm)],[71841]) ).
thf(71843,plain,
! [A: $i] :
( ~ ( e @ ( A @ l1 ) )
| ( A @ s4 ) ),
inference(pattern_uni,[status(thm)],[71842:[bind(A,$thf( A )),bind(B,$thf( a )),bind(C,$thf( e )),bind(D,$thf( e ))]]) ).
thf(72054,plain,
! [A: $i] :
( ( ( e @ ( e @ l1 ) )
!= ( e @ ( A @ l1 ) ) )
| ~ $true
| ( A @ s4 ) ),
inference(paramod_ordered,[status(thm)],[7413,71843]) ).
thf(72055,plain,
! [A: $i] :
( ( ( e @ ( e @ l1 ) )
!= ( e @ ( A @ l1 ) ) )
| ( A @ s4 ) ),
inference(simp,[status(thm)],[72054]) ).
thf(72056,plain,
e @ s4,
inference(pattern_uni,[status(thm)],[72055:[bind(A,$thf( e ))]]) ).
thf(1,negated_conjecture,
~ ( e @ s4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
thf(370,plain,
~ ( e @ s4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(371,plain,
~ ( e @ s4 ),
inference(polarity_switch,[status(thm)],[370]) ).
thf(72077,plain,
$false,
inference(rewrite,[status(thm)],[72056,371]) ).
thf(72078,plain,
$false,
inference(simp,[status(thm)],[72077]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN212-1 : TPTP v9.3.1. Released v1.1.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/5.41 % Computer : n007.cluster.edu
% 0.14/5.41 % Model : x86_64 x86_64
% 0.14/5.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.41 % Memory : 8046.5625MB
% 0.14/5.41 % OS : Linux 6.8.0-71-generic
% 0.14/5.41 % CPULimit : 300
% 0.14/5.41 % WCLimit : 300
% 0.14/5.41 % DateTime : Sat Sep 26 17:20:30 UTC 2026
% 0.14/5.42 % CPUTime :
% 0.14/5.42 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.18/6.01 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.82/6.33 % [INFO] Parsing done (317ms).
% 1.82/6.34 % [INFO] Running in sequential loop mode.
% 2.83/6.74 % [INFO] eprover registered as external prover.
% 2.83/6.75 % [INFO] Scanning for conjecture ...
% 3.03/6.89 % [INFO] Found a conjecture (or negated_conjecture) and 368 axioms. Running axiom selection ...
% 3.73/7.05 % [INFO] Axiom selection finished. Selected 368 axioms (removed 0 axioms).
% 4.25/7.24 % [INFO] Problem is propositional (TPTP CNF).
% 4.25/7.25 % [INFO] Type checking passed.
% 4.25/7.26 % [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 ...
% 206.19/119.00 % [INFO] Killing All external provers ...
% 206.19/119.01 % Time passed: 113442ms (effective reasoning time: 112653ms)
% 206.19/119.01 % Axioms used in derivation (14): axiom_19, rule_299, axiom_20, rule_251, axiom_28, rule_021, axiom_30, rule_154, rule_001, rule_238, rule_176, rule_122, rule_155, rule_002
% 206.19/119.01 % No. of inferences in proof: 89
% 206.19/119.01 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : 113442 ms resp. 112653 ms w/o parsing
% 206.46/119.06 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 206.46/119.06 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------