%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYN067+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n020.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:42 AM UTC 2026
% Result : Theorem 45.83s 10.71s
% Output : Refutation 45.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 12
% Syntax : Number of formulae : 153 ( 19 unt; 0 typ; 11 def)
% Number of atoms : 906 ( 63 equ; 0 cnn)
% Maximal formula atoms : 82 ( 5 avg)
% Number of connectives : 1986 ( 423 ~; 515 |; 103 &; 925 @)
% ( 2 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 39 ( 7 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 20 ( 17 usr; 10 con; 0-2 aty)
% Number of variables : 219 ( 6 ^; 143 !; 59 ?; 219 :)
% ( 0 !>; 0 ?*; 0 @-; 11 @+)
% Comments :
%------------------------------------------------------------------------------
thf(big_p_decl,type,
big_p: $i > $o ).
thf(a_decl,type,
a: $i ).
thf(big_r_decl,type,
big_r: $i > $i > $o ).
thf(sk1_decl,type,
sk1: $o ).
thf(sk2_decl,type,
sk2: $i > $o ).
thf(sk3_decl,type,
sk3: $i > $i ).
thf(sk4_decl,type,
sk4: $i > $i ).
thf(sk5_decl,type,
sk5: $o ).
thf(sk6_decl,type,
sk6: $i ).
thf(sk7_decl,type,
sk7: $i ).
thf(sk8_decl,type,
sk8: $i ).
thf(sk9_decl,type,
sk9: $i > $i ).
thf(sk10_decl,type,
sk10: $i > $i ).
thf(sk11_decl,type,
sk11: $i > $i ).
thf(sk12_decl,type,
sk12: $i > $i ).
thf(sk13_decl,type,
sk13: $i ).
thf(sk14_decl,type,
sk14: $i ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: $i] :
@+[B: $i] :
( ? [C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) ) )
& ( B @ big_p ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( ^ [A: $i] :
@+[B: $i] :
( ( A @ sk3 @ ( B @ big_r ) )
& ( B @ ( A @ big_r ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( @+[A: $i] :
~ ( ? [B: $i] :
( ? [C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) ) )
& ( B @ big_p ) )
| ( A @ big_p ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( @+[A: $i] :
~ ( ? [B: $i] :
( ? [C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) ) )
& ( B @ big_p ) )
| ~ ? [B: $i] :
( ( B @ ( A @ big_r ) )
& ( B @ big_p ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( @+[A: $i] :
( ( A @ ( sk7 @ big_r ) )
& ( A @ big_p ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( ^ [A: $i] :
@+[B: $i] :
( ? [C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) ) )
& ( B @ big_p ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [A: $i] :
@+[B: $i] :
( ( A @ sk9 @ ( B @ big_r ) )
& ( B @ ( A @ big_r ) ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( ^ [A: $i] :
@+[B: $i] :
( ? [C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) ) )
& ( B @ big_p ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( ^ [A: $i] :
@+[B: $i] :
( ( A @ sk11 @ ( B @ big_r ) )
& ( B @ ( A @ big_r ) ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( @+[A: $i] :
~ ( ( ( ( A @ big_p )
=> ? [B: $i] :
( ( B @ ( A @ big_r ) )
& ( B @ big_p ) ) )
& ( a @ big_p ) )
=> ? [B: $i] :
( ? [C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) ) )
& ( B @ big_p ) ) ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( @+[A: $i] :
( ( A @ ( sk13 @ big_r ) )
& ( A @ big_p ) ) ) ) ).
thf(1,conjecture,
( ! [A: $i] :
( ( ( ( A @ big_p )
=> ? [B: $i] :
( ( B @ ( A @ big_r ) )
& ( B @ big_p ) ) )
& ( a @ big_p ) )
=> ? [B: $i,C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) )
& ( B @ big_p ) ) )
<=> ! [A: $i] :
( ( ? [B: $i,C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) )
& ( B @ big_p ) )
| ~ ? [B: $i] :
( ( B @ ( A @ big_r ) )
& ( B @ big_p ) )
| ~ ( a @ big_p ) )
& ( ? [B: $i,C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) )
& ( B @ big_p ) )
| ( A @ big_p )
| ~ ( a @ big_p ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',pel38) ).
thf(2,negated_conjecture,
~ ( ! [A: $i] :
( ( ( ( A @ big_p )
=> ? [B: $i] :
( ( B @ ( A @ big_r ) )
& ( B @ big_p ) ) )
& ( a @ big_p ) )
=> ? [B: $i,C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) )
& ( B @ big_p ) ) )
<=> ! [A: $i] :
( ( ? [B: $i,C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) )
& ( B @ big_p ) )
| ~ ? [B: $i] :
( ( B @ ( A @ big_r ) )
& ( B @ big_p ) )
| ~ ( a @ big_p ) )
& ( ? [B: $i,C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) )
& ( B @ big_p ) )
| ( A @ big_p )
| ~ ( a @ big_p ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ( ( ! [A: $i] :
( ( ? [B: $i,C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) )
& ( B @ big_p ) )
| ~ ? [B: $i] :
( ( B @ ( A @ big_r ) )
& ( B @ big_p ) )
| ~ ( a @ big_p ) )
& ( ? [B: $i,C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) )
& ( B @ big_p ) )
| ( A @ big_p )
| ~ ( a @ big_p ) ) )
=> ! [A: $i] :
( ( ( ( A @ big_p )
=> ? [B: $i] :
( ( B @ ( A @ big_r ) )
& ( B @ big_p ) ) )
& ( a @ big_p ) )
=> ? [B: $i,C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) )
& ( B @ big_p ) ) ) )
& ( ! [A: $i] :
( ( ( ( A @ big_p )
=> ? [B: $i] :
( ( B @ ( A @ big_r ) )
& ( B @ big_p ) ) )
& ( a @ big_p ) )
=> ? [B: $i,C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) )
& ( B @ big_p ) ) )
=> ! [A: $i] :
( ( ? [B: $i,C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) )
& ( B @ big_p ) )
| ~ ? [B: $i] :
( ( B @ ( A @ big_r ) )
& ( B @ big_p ) )
| ~ ( a @ big_p ) )
& ( ? [B: $i,C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) )
& ( B @ big_p ) )
| ( A @ big_p )
| ~ ( a @ big_p ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
~ ( ( ( ( ! [A: $i] :
( ? [B: $i] :
( ? [C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) ) )
& ( B @ big_p ) )
| ~ ? [B: $i] :
( ( B @ ( A @ big_r ) )
& ( B @ big_p ) ) )
| ~ ( a @ big_p ) )
& ( ! [A: $i] :
( ? [B: $i] :
( ? [C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) ) )
& ( B @ big_p ) )
| ( A @ big_p ) )
| ~ ( a @ big_p ) ) )
=> ! [A: $i] :
( ( ( ( A @ big_p )
=> ? [B: $i] :
( ( B @ ( A @ big_r ) )
& ( B @ big_p ) ) )
& ( a @ big_p ) )
=> ? [B: $i] :
( ? [C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) ) )
& ( B @ big_p ) ) ) )
& ( ! [A: $i] :
( ( ( ( A @ big_p )
=> ? [B: $i] :
( ( B @ ( A @ big_r ) )
& ( B @ big_p ) ) )
& ( a @ big_p ) )
=> ? [B: $i] :
( ? [C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) ) )
& ( B @ big_p ) ) )
=> ( ( ! [A: $i] :
( ? [B: $i] :
( ? [C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) ) )
& ( B @ big_p ) )
| ~ ? [B: $i] :
( ( B @ ( A @ big_r ) )
& ( B @ big_p ) ) )
| ~ ( a @ big_p ) )
& ( ! [A: $i] :
( ? [B: $i] :
( ? [C: $i] :
( ( B @ ( C @ big_r ) )
& ( C @ ( A @ big_r ) ) )
& ( B @ big_p ) )
| ( A @ big_p ) )
| ~ ( a @ big_p ) ) ) ) ),
inference(miniscope,[status(thm)],[3]) ).
thf(5,plain,
! [K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ~ ( J @ ( K @ big_r ) )
| ~ ( K @ ( sk13 @ big_r ) )
| ~ ( J @ big_p )
| sk1 )
& ( ( sk14 @ ( sk13 @ big_r ) )
| ~ ( sk13 @ big_p )
| sk1 )
& ( ( sk14 @ big_p )
| ~ ( sk13 @ big_p )
| sk1 )
& ( ( a @ big_p )
| sk1 )
& ( ( H @ sk11 @ ( H @ sk12 @ big_r ) )
| ~ ( I @ ( H @ big_r ) )
| ~ ( I @ big_p )
| ~ ( a @ big_p )
| sk1 )
& ( ( H @ sk12 @ ( H @ big_r ) )
| ~ ( I @ ( H @ big_r ) )
| ~ ( I @ big_p )
| ~ ( a @ big_p )
| sk1 )
& ( ( H @ sk11 @ big_p )
| ~ ( I @ ( H @ big_r ) )
| ~ ( I @ big_p )
| ~ ( a @ big_p )
| sk1 )
& ( ( G @ sk9 @ ( G @ sk10 @ big_r ) )
| ( G @ big_p )
| ~ ( a @ big_p )
| sk1 )
& ( ( G @ sk10 @ ( G @ big_r ) )
| ( G @ big_p )
| ~ ( a @ big_p )
| sk1 )
& ( ( G @ sk9 @ big_p )
| ( G @ big_p )
| ~ ( a @ big_p )
| sk1 )
& ( ~ sk1
| ~ ( E @ ( F @ big_r ) )
| ~ ( F @ ( sk7 @ big_r ) )
| ~ ( E @ big_p )
| sk5 )
& ( ~ sk1
| ( sk8 @ ( sk7 @ big_r ) )
| sk5 )
& ( ~ sk1
| ( sk8 @ big_p )
| sk5 )
& ( ~ sk1
| ( a @ big_p )
| sk5 )
& ( ~ sk1
| ~ sk5
| ~ ( C @ ( D @ big_r ) )
| ~ ( D @ ( sk6 @ big_r ) )
| ~ ( C @ big_p ) )
& ( ~ sk1
| ~ sk5
| ~ ( sk6 @ big_p ) )
& ( ~ sk1
| ~ sk5
| ( a @ big_p ) )
& ( ~ sk1
| ( A @ sk3 @ ( A @ sk4 @ big_r ) )
| ~ ( A @ sk2 ) )
& ( ~ sk1
| ( A @ sk4 @ ( A @ big_r ) )
| ~ ( A @ sk2 ) )
& ( ~ sk1
| ( A @ sk3 @ big_p )
| ~ ( A @ sk2 ) )
& ( ~ sk1
| ( A @ sk2 )
| ~ ( B @ ( A @ big_r ) )
| ~ ( B @ big_p )
| ~ ( a @ big_p ) )
& ( ~ sk1
| ( A @ sk2 )
| ( A @ big_p )
| ~ ( a @ big_p ) ) ),
inference(cnf,[status(esa)],[4]) ).
thf(9,plain,
( ( sk14 @ ( sk13 @ big_r ) )
| ~ ( sk13 @ big_p )
| sk1 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(17,plain,
! [B: $i,A: $i] :
( ( A @ sk12 @ ( A @ big_r ) )
| ~ ( B @ ( A @ big_r ) )
| ~ ( B @ big_p )
| ~ ( a @ big_p )
| sk1 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(31,plain,
! [B: $i,A: $i] :
( ( A @ sk12 @ ( A @ big_r ) )
| ~ ( B @ ( A @ big_r ) )
| ~ ( B @ big_p )
| ~ ( a @ big_p )
| sk1 ),
inference(simp,[status(thm)],[17]) ).
thf(1083,plain,
! [B: $i,A: $i] :
( ( ( sk14 @ ( sk13 @ big_r ) )
!= ( B @ ( A @ big_r ) ) )
| ( A @ sk12 @ ( A @ big_r ) )
| ~ $true
| ~ ( B @ big_p )
| ~ ( a @ big_p )
| sk1
| ~ ( sk13 @ big_p )
| sk1 ),
inference(paramod_ordered,[status(thm)],[9,31]) ).
thf(1084,plain,
! [B: $i,A: $i] :
( ( ( sk14 @ ( sk13 @ big_r ) )
!= ( B @ ( A @ big_r ) ) )
| ( A @ sk12 @ ( A @ big_r ) )
| ~ ( B @ big_p )
| ~ ( a @ big_p )
| ~ ( sk13 @ big_p )
| sk1 ),
inference(simp,[status(thm)],[1083]) ).
thf(1085,plain,
( ( sk13 @ sk12 @ ( sk13 @ big_r ) )
| ~ ( sk14 @ big_p )
| ~ ( a @ big_p )
| ~ ( sk13 @ big_p )
| sk1 ),
inference(pattern_uni,[status(thm)],[1084:[bind(A,$thf( sk13 )),bind(B,$thf( sk14 ))]]) ).
thf(19,plain,
( ( a @ big_p )
| sk1 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(27,plain,
! [A: $i] :
( ( A @ sk9 @ big_p )
| ( A @ big_p )
| ~ ( a @ big_p )
| sk1 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(35,plain,
! [A: $i] :
( ( A @ sk9 @ big_p )
| ( A @ big_p )
| ~ ( a @ big_p )
| sk1 ),
inference(simp,[status(thm)],[27]) ).
thf(69,plain,
! [A: $i] :
( ( ( a @ big_p )
!= ( a @ big_p ) )
| ( A @ sk9 @ big_p )
| ( A @ big_p )
| ~ $true
| sk1
| sk1 ),
inference(paramod_ordered,[status(thm)],[19,35]) ).
thf(70,plain,
! [A: $i] :
( ( ( a @ big_p )
!= ( a @ big_p ) )
| ( A @ sk9 @ big_p )
| ( A @ big_p )
| sk1 ),
inference(simp,[status(thm)],[69]) ).
thf(71,plain,
! [A: $i] :
( ( A @ sk9 @ big_p )
| ( A @ big_p )
| sk1 ),
inference(pattern_uni,[status(thm)],[70:[]]) ).
thf(25,plain,
( ~ sk1
| ( sk8 @ big_p )
| sk5 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(8,plain,
( ~ sk1
| ( a @ big_p )
| sk5 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(7,plain,
( ~ sk1
| ( sk8 @ ( sk7 @ big_r ) )
| sk5 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(21,plain,
! [B: $i,A: $i] :
( ~ sk1
| ( A @ sk2 )
| ~ ( B @ ( A @ big_r ) )
| ~ ( B @ big_p )
| ~ ( a @ big_p ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(299,plain,
! [B: $i,A: $i] :
( ( ( sk8 @ ( sk7 @ big_r ) )
!= ( B @ ( A @ big_r ) ) )
| ~ sk1
| ( A @ sk2 )
| ~ $true
| ~ ( B @ big_p )
| ~ ( a @ big_p )
| ~ sk1
| sk5 ),
inference(paramod_ordered,[status(thm)],[7,21]) ).
thf(300,plain,
! [B: $i,A: $i] :
( ( ( sk8 @ ( sk7 @ big_r ) )
!= ( B @ ( A @ big_r ) ) )
| ( A @ sk2 )
| ~ ( B @ big_p )
| ~ ( a @ big_p )
| ~ sk1
| sk5 ),
inference(simp,[status(thm)],[299]) ).
thf(301,plain,
( ( sk7 @ sk2 )
| ~ ( sk8 @ big_p )
| ~ ( a @ big_p )
| ~ sk1
| sk5 ),
inference(pattern_uni,[status(thm)],[300:[bind(A,$thf( sk7 )),bind(B,$thf( sk8 ))]]) ).
thf(671,plain,
( ( ( a @ big_p )
!= ( a @ big_p ) )
| ( sk7 @ sk2 )
| ~ ( sk8 @ big_p )
| ~ $true
| ~ sk1
| sk5
| ~ sk1
| sk5 ),
inference(paramod_ordered,[status(thm)],[8,301]) ).
thf(672,plain,
( ( ( a @ big_p )
!= ( a @ big_p ) )
| ( sk7 @ sk2 )
| ~ ( sk8 @ big_p )
| ~ sk1
| sk5 ),
inference(simp,[status(thm)],[671]) ).
thf(673,plain,
( ( sk7 @ sk2 )
| ~ ( sk8 @ big_p )
| ~ sk1
| sk5 ),
inference(pattern_uni,[status(thm)],[672:[]]) ).
thf(718,plain,
( ( ( sk8 @ big_p )
!= ( sk8 @ big_p ) )
| ( sk7 @ sk2 )
| ~ $true
| ~ sk1
| sk5
| ~ sk1
| sk5 ),
inference(paramod_ordered,[status(thm)],[25,673]) ).
thf(719,plain,
( ( ( sk8 @ big_p )
!= ( sk8 @ big_p ) )
| ( sk7 @ sk2 )
| ~ sk1
| sk5 ),
inference(simp,[status(thm)],[718]) ).
thf(720,plain,
( ( sk7 @ sk2 )
| ~ sk1
| sk5 ),
inference(pattern_uni,[status(thm)],[719:[]]) ).
thf(20,plain,
! [A: $i] :
( ~ sk1
| ( A @ sk3 @ big_p )
| ~ ( A @ sk2 ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(802,plain,
! [A: $i] :
( ( ( sk7 @ sk2 )
!= ( A @ sk2 ) )
| ~ sk1
| ( A @ sk3 @ big_p )
| ~ $true
| ~ sk1
| sk5 ),
inference(paramod_ordered,[status(thm)],[720,20]) ).
thf(803,plain,
! [A: $i] :
( ( ( sk7 @ sk2 )
!= ( A @ sk2 ) )
| ( A @ sk3 @ big_p )
| ~ sk1
| sk5 ),
inference(simp,[status(thm)],[802]) ).
thf(804,plain,
( ( sk7 @ sk3 @ big_p )
| ~ sk1
| sk5 ),
inference(pattern_uni,[status(thm)],[803:[bind(A,$thf( sk7 ))]]) ).
thf(24,plain,
! [A: $i] :
( ~ sk1
| ( A @ sk4 @ ( A @ big_r ) )
| ~ ( A @ sk2 ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(799,plain,
! [A: $i] :
( ( ( sk7 @ sk2 )
!= ( A @ sk2 ) )
| ~ sk1
| ( A @ sk4 @ ( A @ big_r ) )
| ~ $true
| ~ sk1
| sk5 ),
inference(paramod_ordered,[status(thm)],[720,24]) ).
thf(800,plain,
! [A: $i] :
( ( ( sk7 @ sk2 )
!= ( A @ sk2 ) )
| ( A @ sk4 @ ( A @ big_r ) )
| ~ sk1
| sk5 ),
inference(simp,[status(thm)],[799]) ).
thf(801,plain,
( ( sk7 @ sk4 @ ( sk7 @ big_r ) )
| ~ sk1
| sk5 ),
inference(pattern_uni,[status(thm)],[800:[bind(A,$thf( sk7 ))]]) ).
thf(18,plain,
! [A: $i] :
( ~ sk1
| ( A @ sk3 @ ( A @ sk4 @ big_r ) )
| ~ ( A @ sk2 ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(796,plain,
! [A: $i] :
( ( ( sk7 @ sk2 )
!= ( A @ sk2 ) )
| ~ sk1
| ( A @ sk3 @ ( A @ sk4 @ big_r ) )
| ~ $true
| ~ sk1
| sk5 ),
inference(paramod_ordered,[status(thm)],[720,18]) ).
thf(797,plain,
! [A: $i] :
( ( ( sk7 @ sk2 )
!= ( A @ sk2 ) )
| ( A @ sk3 @ ( A @ sk4 @ big_r ) )
| ~ sk1
| sk5 ),
inference(simp,[status(thm)],[796]) ).
thf(798,plain,
( ( sk7 @ sk3 @ ( sk7 @ sk4 @ big_r ) )
| ~ sk1
| sk5 ),
inference(pattern_uni,[status(thm)],[797:[bind(A,$thf( sk7 ))]]) ).
thf(6,plain,
! [B: $i,A: $i] :
( ~ sk1
| ~ ( A @ ( B @ big_r ) )
| ~ ( B @ ( sk7 @ big_r ) )
| ~ ( A @ big_p )
| sk5 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(29,plain,
! [B: $i,A: $i] :
( ~ sk1
| ~ ( A @ ( B @ big_r ) )
| ~ ( B @ ( sk7 @ big_r ) )
| ~ ( A @ big_p )
| sk5 ),
inference(simp,[status(thm)],[6]) ).
thf(842,plain,
! [B: $i,A: $i] :
( ( ( sk7 @ sk3 @ ( sk7 @ sk4 @ big_r ) )
!= ( A @ ( B @ big_r ) ) )
| ~ sk1
| ~ $true
| ~ ( B @ ( sk7 @ big_r ) )
| ~ ( A @ big_p )
| sk5
| ~ sk1
| sk5 ),
inference(paramod_ordered,[status(thm)],[798,29]) ).
thf(843,plain,
! [B: $i,A: $i] :
( ( ( sk7 @ sk3 @ ( sk7 @ sk4 @ big_r ) )
!= ( A @ ( B @ big_r ) ) )
| ~ ( B @ ( sk7 @ big_r ) )
| ~ ( A @ big_p )
| ~ sk1
| sk5 ),
inference(simp,[status(thm)],[842]) ).
thf(844,plain,
( ~ ( sk7 @ sk4 @ ( sk7 @ big_r ) )
| ~ ( sk7 @ sk3 @ big_p )
| ~ sk1
| sk5 ),
inference(pattern_uni,[status(thm)],[843:[bind(A,$thf( sk7 @ sk3 )),bind(B,$thf( sk7 @ sk4 ))]]) ).
thf(2870,plain,
( ( ( sk7 @ sk4 @ ( sk7 @ big_r ) )
!= ( sk7 @ sk4 @ ( sk7 @ big_r ) ) )
| ~ $true
| ~ ( sk7 @ sk3 @ big_p )
| ~ sk1
| sk5
| ~ sk1
| sk5 ),
inference(paramod_ordered,[status(thm)],[801,844]) ).
thf(2871,plain,
( ( ( sk7 @ sk4 @ ( sk7 @ big_r ) )
!= ( sk7 @ sk4 @ ( sk7 @ big_r ) ) )
| ~ ( sk7 @ sk3 @ big_p )
| ~ sk1
| sk5 ),
inference(simp,[status(thm)],[2870]) ).
thf(2872,plain,
( ~ ( sk7 @ sk3 @ big_p )
| ~ sk1
| sk5 ),
inference(pattern_uni,[status(thm)],[2871:[]]) ).
thf(2894,plain,
( ( ( sk7 @ sk3 @ big_p )
!= ( sk7 @ sk3 @ big_p ) )
| ~ $true
| ~ sk1
| sk5
| ~ sk1
| sk5 ),
inference(paramod_ordered,[status(thm)],[804,2872]) ).
thf(2895,plain,
( ( ( sk7 @ sk3 @ big_p )
!= ( sk7 @ sk3 @ big_p ) )
| ~ sk1
| sk5 ),
inference(simp,[status(thm)],[2894]) ).
thf(2896,plain,
( ~ sk1
| sk5 ),
inference(pattern_uni,[status(thm)],[2895:[]]) ).
thf(16,plain,
( ~ sk1
| ~ sk5
| ( a @ big_p ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(10,plain,
! [A: $i] :
( ~ sk1
| ( A @ sk2 )
| ( A @ big_p )
| ~ ( a @ big_p ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(191,plain,
! [A: $i] :
( ( ( a @ big_p )
!= ( a @ big_p ) )
| ~ sk1
| ( A @ sk2 )
| ( A @ big_p )
| ~ $true
| ~ sk1
| ~ sk5 ),
inference(paramod_ordered,[status(thm)],[16,10]) ).
thf(192,plain,
! [A: $i] :
( ( ( a @ big_p )
!= ( a @ big_p ) )
| ( A @ sk2 )
| ( A @ big_p )
| ~ sk1
| ~ sk5 ),
inference(simp,[status(thm)],[191]) ).
thf(193,plain,
! [A: $i] :
( ( A @ sk2 )
| ( A @ big_p )
| ~ sk1
| ~ sk5 ),
inference(pattern_uni,[status(thm)],[192:[]]) ).
thf(23,plain,
! [B: $i,A: $i] :
( ~ sk1
| ~ sk5
| ~ ( A @ ( B @ big_r ) )
| ~ ( B @ ( sk6 @ big_r ) )
| ~ ( A @ big_p ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(36,plain,
! [B: $i,A: $i] :
( ~ sk1
| ~ sk5
| ~ ( A @ ( B @ big_r ) )
| ~ ( B @ ( sk6 @ big_r ) )
| ~ ( A @ big_p ) ),
inference(simp,[status(thm)],[23]) ).
thf(207,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ sk4 @ ( A @ big_r ) )
!= ( C @ ( sk6 @ big_r ) ) )
| ~ sk1
| ~ sk5
| ~ ( B @ ( C @ big_r ) )
| ~ $true
| ~ ( B @ big_p )
| ~ sk1
| ~ ( A @ sk2 ) ),
inference(paramod_ordered,[status(thm)],[24,36]) ).
thf(208,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ sk4 @ ( A @ big_r ) )
!= ( C @ ( sk6 @ big_r ) ) )
| ~ sk5
| ~ ( B @ ( C @ big_r ) )
| ~ ( B @ big_p )
| ~ sk1
| ~ ( A @ sk2 ) ),
inference(simp,[status(thm)],[207]) ).
thf(209,plain,
! [A: $i] :
( ~ sk5
| ~ ( A @ ( sk6 @ sk4 @ big_r ) )
| ~ ( A @ big_p )
| ~ sk1
| ~ ( sk6 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[208:[bind(A,$thf( sk6 )),bind(B,$thf( B )),bind(C,$thf( sk6 @ sk4 ))]]) ).
thf(213,plain,
! [A: $i] :
( ~ sk5
| ~ ( A @ ( sk6 @ sk4 @ big_r ) )
| ~ ( A @ big_p )
| ~ sk1
| ~ ( sk6 @ sk2 ) ),
inference(simp,[status(thm)],[209]) ).
thf(455,plain,
! [B: $i,A: $i] :
( ( ( A @ sk3 @ ( A @ sk4 @ big_r ) )
!= ( B @ ( sk6 @ sk4 @ big_r ) ) )
| ~ sk5
| ~ $true
| ~ ( B @ big_p )
| ~ sk1
| ~ ( sk6 @ sk2 )
| ~ sk1
| ~ ( A @ sk2 ) ),
inference(paramod_ordered,[status(thm)],[18,213]) ).
thf(456,plain,
! [B: $i,A: $i] :
( ( ( A @ sk3 @ ( A @ sk4 @ big_r ) )
!= ( B @ ( sk6 @ sk4 @ big_r ) ) )
| ~ sk5
| ~ ( B @ big_p )
| ~ ( sk6 @ sk2 )
| ~ sk1
| ~ ( A @ sk2 ) ),
inference(simp,[status(thm)],[455]) ).
thf(457,plain,
( ~ sk5
| ~ ( sk6 @ sk3 @ big_p )
| ~ ( sk6 @ sk2 )
| ~ sk1
| ~ ( sk6 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[456:[bind(A,$thf( sk6 )),bind(B,$thf( sk6 @ sk3 ))]]) ).
thf(486,plain,
( ~ sk5
| ~ ( sk6 @ sk3 @ big_p )
| ~ sk1
| ~ ( sk6 @ sk2 ) ),
inference(simp,[status(thm)],[457]) ).
thf(507,plain,
! [A: $i] :
( ( ( A @ sk3 @ big_p )
!= ( sk6 @ sk3 @ big_p ) )
| ~ sk5
| ~ $true
| ~ sk1
| ~ ( sk6 @ sk2 )
| ~ sk1
| ~ ( A @ sk2 ) ),
inference(paramod_ordered,[status(thm)],[20,486]) ).
thf(508,plain,
! [A: $i] :
( ( ( A @ sk3 @ big_p )
!= ( sk6 @ sk3 @ big_p ) )
| ~ sk5
| ~ ( sk6 @ sk2 )
| ~ sk1
| ~ ( A @ sk2 ) ),
inference(simp,[status(thm)],[507]) ).
thf(509,plain,
( ~ sk5
| ~ ( sk6 @ sk2 )
| ~ sk1
| ~ ( sk6 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[508:[bind(A,$thf( sk6 ))]]) ).
thf(518,plain,
( ~ sk5
| ~ sk1
| ~ ( sk6 @ sk2 ) ),
inference(simp,[status(thm)],[509]) ).
thf(522,plain,
! [A: $i] :
( ( ( A @ sk2 )
!= ( sk6 @ sk2 ) )
| ~ sk5
| ~ sk1
| ~ $true
| ( A @ big_p )
| ~ sk1
| ~ sk5 ),
inference(paramod_ordered,[status(thm)],[193,518]) ).
thf(523,plain,
! [A: $i] :
( ( ( A @ sk2 )
!= ( sk6 @ sk2 ) )
| ( A @ big_p )
| ~ sk1
| ~ sk5 ),
inference(simp,[status(thm)],[522]) ).
thf(524,plain,
( ( sk6 @ big_p )
| ~ sk1
| ~ sk5 ),
inference(pattern_uni,[status(thm)],[523:[bind(A,$thf( sk6 ))]]) ).
thf(11,plain,
( ~ sk1
| ~ sk5
| ~ ( sk6 @ big_p ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(627,plain,
( ( ( sk6 @ big_p )
!= ( sk6 @ big_p ) )
| ~ sk1
| ~ sk5
| ~ $true
| ~ sk1
| ~ sk5 ),
inference(paramod_ordered,[status(thm)],[524,11]) ).
thf(628,plain,
( ( ( sk6 @ big_p )
!= ( sk6 @ big_p ) )
| ~ sk1
| ~ sk5 ),
inference(simp,[status(thm)],[627]) ).
thf(629,plain,
( ~ sk1
| ~ sk5 ),
inference(pattern_uni,[status(thm)],[628:[]]) ).
thf(3256,plain,
( ( sk5 != sk5 )
| ~ sk1
| ~ $true
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[2896,629]) ).
thf(3257,plain,
( ( sk5 != sk5 )
| ~ sk1 ),
inference(simp,[status(thm)],[3256]) ).
thf(3258,plain,
~ sk1,
inference(pattern_uni,[status(thm)],[3257:[]]) ).
thf(3271,plain,
! [A: $i] :
( ( A @ sk9 @ big_p )
| ( A @ big_p )
| $false ),
inference(rewrite,[status(thm)],[71,3258]) ).
thf(3272,plain,
! [A: $i] :
( ( A @ sk9 @ big_p )
| ( A @ big_p ) ),
inference(simp,[status(thm)],[3271]) ).
thf(22,plain,
! [A: $i] :
( ( A @ sk9 @ ( A @ sk10 @ big_r ) )
| ( A @ big_p )
| ~ ( a @ big_p )
| sk1 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(34,plain,
! [A: $i] :
( ( A @ sk9 @ ( A @ sk10 @ big_r ) )
| ( A @ big_p )
| ~ ( a @ big_p )
| sk1 ),
inference(simp,[status(thm)],[22]) ).
thf(1508,plain,
! [A: $i] :
( ( ( a @ big_p )
!= ( a @ big_p ) )
| ( A @ sk9 @ ( A @ sk10 @ big_r ) )
| ( A @ big_p )
| ~ $true
| sk1
| sk1 ),
inference(paramod_ordered,[status(thm)],[19,34]) ).
thf(1509,plain,
! [A: $i] :
( ( ( a @ big_p )
!= ( a @ big_p ) )
| ( A @ sk9 @ ( A @ sk10 @ big_r ) )
| ( A @ big_p )
| sk1 ),
inference(simp,[status(thm)],[1508]) ).
thf(1510,plain,
! [A: $i] :
( ( A @ sk9 @ ( A @ sk10 @ big_r ) )
| ( A @ big_p )
| sk1 ),
inference(pattern_uni,[status(thm)],[1509:[]]) ).
thf(3303,plain,
! [A: $i] :
( ( A @ sk9 @ ( A @ sk10 @ big_r ) )
| ( A @ big_p )
| $false ),
inference(rewrite,[status(thm)],[1510,3258]) ).
thf(3304,plain,
! [A: $i] :
( ( A @ sk9 @ ( A @ sk10 @ big_r ) )
| ( A @ big_p ) ),
inference(simp,[status(thm)],[3303]) ).
thf(15,plain,
! [A: $i] :
( ( A @ sk10 @ ( A @ big_r ) )
| ( A @ big_p )
| ~ ( a @ big_p )
| sk1 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(33,plain,
! [A: $i] :
( ( A @ sk10 @ ( A @ big_r ) )
| ( A @ big_p )
| ~ ( a @ big_p )
| sk1 ),
inference(simp,[status(thm)],[15]) ).
thf(1067,plain,
! [A: $i] :
( ( ( a @ big_p )
!= ( a @ big_p ) )
| ( A @ sk10 @ ( A @ big_r ) )
| ( A @ big_p )
| ~ $true
| sk1
| sk1 ),
inference(paramod_ordered,[status(thm)],[19,33]) ).
thf(1068,plain,
! [A: $i] :
( ( ( a @ big_p )
!= ( a @ big_p ) )
| ( A @ sk10 @ ( A @ big_r ) )
| ( A @ big_p )
| sk1 ),
inference(simp,[status(thm)],[1067]) ).
thf(1069,plain,
! [A: $i] :
( ( A @ sk10 @ ( A @ big_r ) )
| ( A @ big_p )
| sk1 ),
inference(pattern_uni,[status(thm)],[1068:[]]) ).
thf(3285,plain,
! [A: $i] :
( ( A @ sk10 @ ( A @ big_r ) )
| ( A @ big_p )
| $false ),
inference(rewrite,[status(thm)],[1069,3258]) ).
thf(3286,plain,
! [A: $i] :
( ( A @ sk10 @ ( A @ big_r ) )
| ( A @ big_p ) ),
inference(simp,[status(thm)],[3285]) ).
thf(12,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ big_r ) )
| ~ ( B @ ( sk13 @ big_r ) )
| ~ ( A @ big_p )
| sk1 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(32,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ big_r ) )
| ~ ( B @ ( sk13 @ big_r ) )
| ~ ( A @ big_p )
| sk1 ),
inference(simp,[status(thm)],[12]) ).
thf(3305,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ big_r ) )
| ~ ( B @ ( sk13 @ big_r ) )
| ~ ( A @ big_p )
| $false ),
inference(rewrite,[status(thm)],[32,3258]) ).
thf(3306,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ big_r ) )
| ~ ( B @ ( sk13 @ big_r ) )
| ~ ( A @ big_p ) ),
inference(simp,[status(thm)],[3305]) ).
thf(3751,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ sk10 @ ( A @ big_r ) )
!= ( C @ ( sk13 @ big_r ) ) )
| ~ ( B @ ( C @ big_r ) )
| ~ $true
| ~ ( B @ big_p )
| ( A @ big_p ) ),
inference(paramod_ordered,[status(thm)],[3286,3306]) ).
thf(3752,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ sk10 @ ( A @ big_r ) )
!= ( C @ ( sk13 @ big_r ) ) )
| ~ ( B @ ( C @ big_r ) )
| ~ ( B @ big_p )
| ( A @ big_p ) ),
inference(simp,[status(thm)],[3751]) ).
thf(3753,plain,
! [A: $i] :
( ~ ( A @ ( sk13 @ sk10 @ big_r ) )
| ~ ( A @ big_p )
| ( sk13 @ big_p ) ),
inference(pattern_uni,[status(thm)],[3752:[bind(A,$thf( sk13 )),bind(B,$thf( B )),bind(C,$thf( sk13 @ sk10 ))]]) ).
thf(3794,plain,
! [A: $i] :
( ~ ( A @ ( sk13 @ sk10 @ big_r ) )
| ~ ( A @ big_p )
| ( sk13 @ big_p ) ),
inference(simp,[status(thm)],[3753]) ).
thf(4007,plain,
! [B: $i,A: $i] :
( ( ( A @ sk9 @ ( A @ sk10 @ big_r ) )
!= ( B @ ( sk13 @ sk10 @ big_r ) ) )
| ~ $true
| ~ ( B @ big_p )
| ( sk13 @ big_p )
| ( A @ big_p ) ),
inference(paramod_ordered,[status(thm)],[3304,3794]) ).
thf(4008,plain,
! [B: $i,A: $i] :
( ( ( A @ sk9 @ ( A @ sk10 @ big_r ) )
!= ( B @ ( sk13 @ sk10 @ big_r ) ) )
| ~ ( B @ big_p )
| ( sk13 @ big_p )
| ( A @ big_p ) ),
inference(simp,[status(thm)],[4007]) ).
thf(4009,plain,
( ~ ( sk13 @ sk9 @ big_p )
| ( sk13 @ big_p )
| ( sk13 @ big_p ) ),
inference(pattern_uni,[status(thm)],[4008:[bind(A,$thf( sk13 )),bind(B,$thf( sk13 @ sk9 ))]]) ).
thf(4019,plain,
( ~ ( sk13 @ sk9 @ big_p )
| ( sk13 @ big_p ) ),
inference(simp,[status(thm)],[4009]) ).
thf(4025,plain,
! [A: $i] :
( ( ( A @ sk9 @ big_p )
!= ( sk13 @ sk9 @ big_p ) )
| ~ $true
| ( sk13 @ big_p )
| ( A @ big_p ) ),
inference(paramod_ordered,[status(thm)],[3272,4019]) ).
thf(4026,plain,
! [A: $i] :
( ( ( A @ sk9 @ big_p )
!= ( sk13 @ sk9 @ big_p ) )
| ( sk13 @ big_p )
| ( A @ big_p ) ),
inference(simp,[status(thm)],[4025]) ).
thf(4027,plain,
( ( sk13 @ big_p )
| ( sk13 @ big_p ) ),
inference(pattern_uni,[status(thm)],[4026:[bind(A,$thf( sk13 ))]]) ).
thf(4032,plain,
sk13 @ big_p,
inference(simp,[status(thm)],[4027]) ).
thf(14,plain,
! [B: $i,A: $i] :
( ( A @ sk11 @ ( A @ sk12 @ big_r ) )
| ~ ( B @ ( A @ big_r ) )
| ~ ( B @ big_p )
| ~ ( a @ big_p )
| sk1 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(28,plain,
! [B: $i,A: $i] :
( ( A @ sk11 @ ( A @ sk12 @ big_r ) )
| ~ ( B @ ( A @ big_r ) )
| ~ ( B @ big_p )
| ~ ( a @ big_p )
| sk1 ),
inference(simp,[status(thm)],[14]) ).
thf(540,plain,
! [B: $i,A: $i] :
( ( ( sk14 @ ( sk13 @ big_r ) )
!= ( B @ ( A @ big_r ) ) )
| ( A @ sk11 @ ( A @ sk12 @ big_r ) )
| ~ $true
| ~ ( B @ big_p )
| ~ ( a @ big_p )
| sk1
| ~ ( sk13 @ big_p )
| sk1 ),
inference(paramod_ordered,[status(thm)],[9,28]) ).
thf(541,plain,
! [B: $i,A: $i] :
( ( ( sk14 @ ( sk13 @ big_r ) )
!= ( B @ ( A @ big_r ) ) )
| ( A @ sk11 @ ( A @ sk12 @ big_r ) )
| ~ ( B @ big_p )
| ~ ( a @ big_p )
| ~ ( sk13 @ big_p )
| sk1 ),
inference(simp,[status(thm)],[540]) ).
thf(542,plain,
( ( sk13 @ sk11 @ ( sk13 @ sk12 @ big_r ) )
| ~ ( sk14 @ big_p )
| ~ ( a @ big_p )
| ~ ( sk13 @ big_p )
| sk1 ),
inference(pattern_uni,[status(thm)],[541:[bind(A,$thf( sk13 )),bind(B,$thf( sk14 ))]]) ).
thf(26,plain,
( ( sk14 @ big_p )
| ~ ( sk13 @ big_p )
| sk1 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(3281,plain,
( ( sk14 @ big_p )
| ~ ( sk13 @ big_p )
| $false ),
inference(rewrite,[status(thm)],[26,3258]) ).
thf(3282,plain,
( ( sk14 @ big_p )
| ~ ( sk13 @ big_p ) ),
inference(simp,[status(thm)],[3281]) ).
thf(4037,plain,
( ( sk14 @ big_p )
| ~ $true ),
inference(rewrite,[status(thm)],[3282,4032]) ).
thf(4038,plain,
sk14 @ big_p,
inference(simp,[status(thm)],[4037]) ).
thf(3323,plain,
( ( a @ big_p )
| $false ),
inference(rewrite,[status(thm)],[19,3258]) ).
thf(3324,plain,
a @ big_p,
inference(simp,[status(thm)],[3323]) ).
thf(5329,plain,
( ( sk13 @ sk11 @ ( sk13 @ sk12 @ big_r ) )
| ~ $true
| ~ $true
| ~ $true
| $false ),
inference(rewrite,[status(thm)],[542,4032,4038,3258,3324]) ).
thf(5330,plain,
sk13 @ sk11 @ ( sk13 @ sk12 @ big_r ),
inference(simp,[status(thm)],[5329]) ).
thf(5333,plain,
! [B: $i,A: $i] :
( ( ( sk13 @ sk11 @ ( sk13 @ sk12 @ big_r ) )
!= ( A @ ( B @ big_r ) ) )
| ~ $true
| ~ ( B @ ( sk13 @ big_r ) )
| ~ ( A @ big_p ) ),
inference(paramod_ordered,[status(thm)],[5330,3306]) ).
thf(5334,plain,
! [B: $i,A: $i] :
( ( ( sk13 @ sk11 @ ( sk13 @ sk12 @ big_r ) )
!= ( A @ ( B @ big_r ) ) )
| ~ ( B @ ( sk13 @ big_r ) )
| ~ ( A @ big_p ) ),
inference(simp,[status(thm)],[5333]) ).
thf(5335,plain,
( ~ ( sk13 @ sk12 @ ( sk13 @ big_r ) )
| ~ ( sk13 @ sk11 @ big_p ) ),
inference(pattern_uni,[status(thm)],[5334:[bind(A,$thf( sk13 @ sk11 )),bind(B,$thf( sk13 @ sk12 ))]]) ).
thf(13,plain,
! [B: $i,A: $i] :
( ( A @ sk11 @ big_p )
| ~ ( B @ ( A @ big_r ) )
| ~ ( B @ big_p )
| ~ ( a @ big_p )
| sk1 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(30,plain,
! [B: $i,A: $i] :
( ( A @ sk11 @ big_p )
| ~ ( B @ ( A @ big_r ) )
| ~ ( B @ big_p )
| ~ ( a @ big_p )
| sk1 ),
inference(simp,[status(thm)],[13]) ).
thf(879,plain,
! [B: $i,A: $i] :
( ( ( sk14 @ ( sk13 @ big_r ) )
!= ( B @ ( A @ big_r ) ) )
| ( A @ sk11 @ big_p )
| ~ $true
| ~ ( B @ big_p )
| ~ ( a @ big_p )
| sk1
| ~ ( sk13 @ big_p )
| sk1 ),
inference(paramod_ordered,[status(thm)],[9,30]) ).
thf(880,plain,
! [B: $i,A: $i] :
( ( ( sk14 @ ( sk13 @ big_r ) )
!= ( B @ ( A @ big_r ) ) )
| ( A @ sk11 @ big_p )
| ~ ( B @ big_p )
| ~ ( a @ big_p )
| ~ ( sk13 @ big_p )
| sk1 ),
inference(simp,[status(thm)],[879]) ).
thf(881,plain,
( ( sk13 @ sk11 @ big_p )
| ~ ( sk14 @ big_p )
| ~ ( a @ big_p )
| ~ ( sk13 @ big_p )
| sk1 ),
inference(pattern_uni,[status(thm)],[880:[bind(A,$thf( sk13 )),bind(B,$thf( sk14 ))]]) ).
thf(9398,plain,
( ( sk13 @ sk11 @ big_p )
| ~ $true
| ~ $true
| ~ $true
| $false ),
inference(rewrite,[status(thm)],[881,4032,4038,3258,3324]) ).
thf(9399,plain,
sk13 @ sk11 @ big_p,
inference(simp,[status(thm)],[9398]) ).
thf(9410,plain,
( ~ ( sk13 @ sk12 @ ( sk13 @ big_r ) )
| ~ $true ),
inference(rewrite,[status(thm)],[5335,9399]) ).
thf(9411,plain,
~ ( sk13 @ sk12 @ ( sk13 @ big_r ) ),
inference(simp,[status(thm)],[9410]) ).
thf(15854,plain,
( $false
| ~ $true
| ~ $true
| ~ $true
| $false ),
inference(rewrite,[status(thm)],[1085,4032,9411,4038,3258,3324]) ).
thf(15855,plain,
$false,
inference(simp,[status(thm)],[15854]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYN067+1 : TPTP v9.3.1. Released v2.0.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.23/0.50 % Computer : n020.cluster.edu
% 0.23/0.50 % Model : x86_64 x86_64
% 0.23/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.23/0.50 % Memory : 8046.5625MB
% 0.23/0.50 % OS : Linux 6.8.0-71-generic
% 0.23/0.50 % CPULimit : 300
% 0.23/0.50 % WCLimit : 300
% 0.23/0.50 % DateTime : Sat Sep 26 17:09:19 UTC 2026
% 0.28/0.50 % CPUTime :
% 0.28/0.50 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
% 1.24/1.16 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.59/1.32 % [INFO] Parsing done (160ms).
% 1.59/1.33 % [INFO] Running in sequential loop mode.
% 2.32/1.73 % [INFO] eprover registered as external prover.
% 2.32/1.74 % [INFO] Scanning for conjecture ...
% 2.72/1.90 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.72/1.96 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.72/1.96 % [INFO] Problem is first-order (TPTP FOF).
% 2.72/1.97 % [INFO] Type checking passed.
% 2.72/1.98 % [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 ...
% 45.83/10.70 % [INFO] Killing All external provers ...
% 45.83/10.71 % Time passed: 10013ms (effective reasoning time: 9368ms)
% 45.83/10.71 % Solved by 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)>
% 45.83/10.71 % Axioms used in derivation (0):
% 45.83/10.71 % No. of inferences in proof: 142
% 45.83/10.71 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 10013 ms resp. 9368 ms w/o parsing
% 45.83/10.77 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 45.83/10.77 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------