%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : COM003+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 : n004.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 06:57:50 AM UTC 2026
% Result : Theorem 202.68s 51.25s
% Output : Refutation 202.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 17
% Syntax : Number of formulae : 395 ( 17 unt; 0 typ; 12 def)
% Number of atoms : 2403 ( 361 equ; 0 cnn)
% Maximal formula atoms : 44 ( 6 avg)
% Number of connectives : 5811 (1138 ~;1406 |; 144 &;3059 @)
% ( 0 <=>; 64 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 8 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 27 ( 24 usr; 9 con; 0-3 aty)
% Number of variables : 488 ( 8 ^; 448 !; 20 ?; 488 :)
% ( 0 !>; 0 ?*; 0 @-; 12 @+)
% Comments :
%------------------------------------------------------------------------------
thf(algorithm_decl,type,
algorithm: $i > $o ).
thf(program_decl,type,
program: $i > $o ).
thf(decides_decl,type,
decides: $i > $i > $i > $o ).
thf(halts2_decl,type,
halts2: $i > $i > $o ).
thf(halts3_decl,type,
halts3: $i > $i > $i > $o ).
thf(outputs_decl,type,
outputs: $i > $i > $o ).
thf(good_decl,type,
good: $i ).
thf(bad_decl,type,
bad: $i ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i > $i ).
thf(sk3_decl,type,
sk3: $i > $i ).
thf(sk4_decl,type,
sk4: $i ).
thf(sk5_decl,type,
sk5: $i > $o ).
thf(sk6_decl,type,
sk6: $i > $i ).
thf(sk7_decl,type,
sk7: $i > $i ).
thf(sk8_decl,type,
sk8: $o ).
thf(sk9_decl,type,
sk9: $i > $o ).
thf(sk10_decl,type,
sk10: $i > $i ).
thf(sk11_decl,type,
sk11: $i > $i ).
thf(sk12_decl,type,
sk12: $i ).
thf(sk13_decl,type,
sk13: $i ).
thf(sk14_decl,type,
sk14: $i > $o ).
thf(sk15_decl,type,
sk15: $i > $i ).
thf(sk16_decl,type,
sk16: $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
( ! [B: $i] :
( ( B @ program )
=> ! [C: $i] : ( C @ ( B @ ( A @ decides ) ) ) )
& ( A @ algorithm ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ program )
=> ! [C: $i] : ( C @ ( B @ ( A @ decides ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: $i] :
@+[B: $i] :
~ ( B @ ( A @ sk2 @ ( A @ decides ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] :
( ! [B: $i] :
( ( B @ program )
=> ! [C: $i] : ( C @ ( B @ ( A @ decides ) ) ) )
& ( A @ program ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ program )
=> ! [C: $i] : ( C @ ( B @ ( A @ decides ) ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: $i] :
@+[B: $i] :
~ ( B @ ( A @ sk6 @ ( A @ decides ) ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( good @ ( A @ outputs ) )
& ( B @ ( B @ ( A @ halts3 ) ) ) ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( ~ ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( B @ ( B @ ( A @ halts3 ) ) ) ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( @+[A: $i] :
( ! [B: $i] :
( ( ~ ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) )
& ! [B: $i] :
( ( ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( good @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) )
& ( A @ program ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( @+[A: $i] :
( ! [B: $i] :
( ( ~ ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) )
& ! [B: $i] :
( ( ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ~ ( B @ ( A @ halts2 ) ) )
& ( A @ program ) ) ) ) ).
thf(sk15_def,definition,
( sk15
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( good @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) ) ) ) ).
thf(sk16_def,definition,
( sk16
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( ~ ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) ) ) ) ).
thf(1,conjecture,
~ ? [A: $i] :
( ! [B: $i] :
( ( B @ program )
=> ! [C: $i] : ( C @ ( B @ ( A @ decides ) ) ) )
& ( A @ algorithm ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
thf(2,negated_conjecture,
~ ~ ? [A: $i] :
( ! [B: $i] :
( ( B @ program )
=> ! [C: $i] : ( C @ ( B @ ( A @ decides ) ) ) )
& ( A @ algorithm ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(7,plain,
~ ~ ? [A: $i] :
( ! [B: $i] :
( ( B @ program )
=> ! [C: $i] : ( C @ ( B @ ( A @ decides ) ) ) )
& ( A @ algorithm ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(8,plain,
? [A: $i] :
( ! [B: $i] :
( ( B @ program )
=> ! [C: $i] : ( C @ ( B @ ( A @ decides ) ) ) )
& ( A @ algorithm ) ),
inference(polarity_switch,[status(thm)],[7]) ).
thf(9,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( sk1 @ decides ) ) )
| ~ ( A @ program ) )
& ( sk1 @ algorithm ) ),
inference(cnf,[status(esa)],[8]) ).
thf(10,plain,
sk1 @ algorithm,
inference(cnfConj,[status(thm)],[9]) ).
thf(3,axiom,
( ? [A: $i] :
( ! [B: $i] :
( ( B @ program )
=> ! [C: $i] : ( C @ ( B @ ( A @ decides ) ) ) )
& ( A @ algorithm ) )
=> ? [A: $i] :
( ! [B: $i] :
( ( B @ program )
=> ! [C: $i] : ( C @ ( B @ ( A @ decides ) ) ) )
& ( A @ program ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p1) ).
thf(12,plain,
( ? [A: $i] :
( ! [B: $i] :
( ( B @ program )
=> ! [C: $i] : ( C @ ( B @ ( A @ decides ) ) ) )
& ( A @ algorithm ) )
=> ? [A: $i] :
( ! [B: $i] :
( ( B @ program )
=> ! [C: $i] : ( C @ ( B @ ( A @ decides ) ) ) )
& ( A @ program ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(13,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( sk4 @ decides ) ) )
| ~ ( B @ program )
| ~ ( A @ sk3 @ ( A @ sk2 @ ( A @ decides ) ) )
| ~ ( A @ algorithm ) )
& ( ( sk4 @ program )
| ~ ( A @ sk3 @ ( A @ sk2 @ ( A @ decides ) ) )
| ~ ( A @ algorithm ) )
& ( ( C @ ( B @ ( sk4 @ decides ) ) )
| ~ ( B @ program )
| ( A @ sk2 @ program )
| ~ ( A @ algorithm ) )
& ( ( sk4 @ program )
| ( A @ sk2 @ program )
| ~ ( A @ algorithm ) ) ),
inference(cnf,[status(esa)],[12]) ).
thf(14,plain,
! [A: $i] :
( ( sk4 @ program )
| ( A @ sk2 @ program )
| ~ ( A @ algorithm ) ),
inference(cnfConj,[status(thm)],[13]) ).
thf(102,plain,
! [A: $i] :
( ( ( sk1 @ algorithm )
!= ( A @ algorithm ) )
| ( sk4 @ program )
| ( A @ sk2 @ program )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[10,14]) ).
thf(103,plain,
! [A: $i] :
( ( ( sk1 @ algorithm )
!= ( A @ algorithm ) )
| ( sk4 @ program )
| ( A @ sk2 @ program ) ),
inference(simp,[status(thm)],[102]) ).
thf(104,plain,
( ( sk4 @ program )
| ( sk1 @ sk2 @ program ) ),
inference(pattern_uni,[status(thm)],[103:[bind(A,$thf( sk1 ))]]) ).
thf(11,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( sk1 @ decides ) ) )
| ~ ( A @ program ) ),
inference(cnfConj,[status(thm)],[9]) ).
thf(126,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ sk2 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ~ $true
| ( sk4 @ program ) ),
inference(paramod_ordered,[status(thm)],[104,11]) ).
thf(127,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ sk2 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ( sk4 @ program ) ),
inference(simp,[status(thm)],[126]) ).
thf(128,plain,
! [A: $i] :
( ( A @ ( sk1 @ sk2 @ ( sk1 @ decides ) ) )
| ( sk4 @ program ) ),
inference(pattern_uni,[status(thm)],[127:[bind(A,$thf( sk1 @ sk2 )),bind(B,$thf( B ))]]) ).
thf(132,plain,
! [A: $i] :
( ( A @ ( sk1 @ sk2 @ ( sk1 @ decides ) ) )
| ( sk4 @ program ) ),
inference(simp,[status(thm)],[128]) ).
thf(16,plain,
! [A: $i] :
( ( sk4 @ program )
| ~ ( A @ sk3 @ ( A @ sk2 @ ( A @ decides ) ) )
| ~ ( A @ algorithm ) ),
inference(cnfConj,[status(thm)],[13]) ).
thf(348,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk1 @ sk2 @ ( sk1 @ decides ) ) )
!= ( B @ sk3 @ ( B @ sk2 @ ( B @ decides ) ) ) )
| ( sk4 @ program )
| ~ $true
| ~ ( B @ algorithm )
| ( sk4 @ program ) ),
inference(paramod_ordered,[status(thm)],[132,16]) ).
thf(349,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk1 @ sk2 @ ( sk1 @ decides ) ) )
!= ( B @ sk3 @ ( B @ sk2 @ ( B @ decides ) ) ) )
| ~ ( B @ algorithm )
| ( sk4 @ program ) ),
inference(simp,[status(thm)],[348]) ).
thf(350,plain,
( ~ ( sk1 @ algorithm )
| ( sk4 @ program ) ),
inference(pattern_uni,[status(thm)],[349:[bind(A,$thf( sk1 @ sk3 )),bind(B,$thf( sk1 ))]]) ).
thf(369,plain,
( ~ $true
| ( sk4 @ program ) ),
inference(rewrite,[status(thm)],[350,10]) ).
thf(370,plain,
sk4 @ program,
inference(simp,[status(thm)],[369]) ).
thf(5,axiom,
( ? [A: $i] :
( ! [B: $i] :
( ( ( ~ ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( B @ ( B @ ( A @ halts3 ) ) ) ) )
& ( ( ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( good @ ( A @ outputs ) )
& ( B @ ( B @ ( A @ halts3 ) ) ) ) ) )
& ( A @ program ) )
=> ? [A: $i] :
( ! [B: $i] :
( ( ( ~ ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) )
& ( ( ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( good @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) ) )
& ( A @ program ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p3) ).
thf(29,plain,
( ? [A: $i] :
( ! [B: $i] :
( ( ( ~ ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( B @ ( B @ ( A @ halts3 ) ) ) ) )
& ( ( ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( good @ ( A @ outputs ) )
& ( B @ ( B @ ( A @ halts3 ) ) ) ) ) )
& ( A @ program ) )
=> ? [A: $i] :
( ! [B: $i] :
( ( ( ~ ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) )
& ( ( ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( good @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) ) )
& ( A @ program ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(30,plain,
( ? [A: $i] :
( ! [B: $i] :
( ( ~ ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( B @ ( B @ ( A @ halts3 ) ) ) ) )
& ! [B: $i] :
( ( ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( good @ ( A @ outputs ) )
& ( B @ ( B @ ( A @ halts3 ) ) ) ) )
& ( A @ program ) )
=> ? [A: $i] :
( ! [B: $i] :
( ( ~ ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) )
& ! [B: $i] :
( ( ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( good @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) )
& ( A @ program ) ) ),
inference(miniscope,[status(thm)],[29]) ).
thf(31,plain,
! [C: $i,B: $i,A: $i] :
( ( ( bad @ ( sk12 @ outputs ) )
| ( C @ ( C @ halts2 ) )
| ~ ( C @ program )
| ~ sk8 )
& ( ( C @ ( sk12 @ halts2 ) )
| ( C @ ( C @ halts2 ) )
| ~ ( C @ program )
| ~ sk8 )
& ( ( good @ ( sk12 @ outputs ) )
| ~ ( B @ ( B @ halts2 ) )
| ~ ( B @ program )
| ~ sk8 )
& ( ( B @ ( sk12 @ halts2 ) )
| ~ ( B @ ( B @ halts2 ) )
| ~ ( B @ program )
| ~ sk8 )
& ( ( sk12 @ program )
| ~ sk8 )
& ( sk8
| ~ ( bad @ ( A @ outputs ) )
| ~ ( A @ sk11 @ ( A @ sk11 @ ( A @ halts3 ) ) )
| ( A @ sk9 )
| ~ ( A @ program ) )
& ( sk8
| ~ ( A @ sk11 @ ( A @ sk11 @ halts2 ) )
| ( A @ sk9 )
| ~ ( A @ program ) )
& ( sk8
| ( A @ sk11 @ program )
| ( A @ sk9 )
| ~ ( A @ program ) )
& ( sk8
| ~ ( A @ sk9 )
| ~ ( good @ ( A @ outputs ) )
| ~ ( A @ sk10 @ ( A @ sk10 @ ( A @ halts3 ) ) )
| ~ ( A @ program ) )
& ( sk8
| ~ ( A @ sk9 )
| ( A @ sk10 @ ( A @ sk10 @ halts2 ) )
| ~ ( A @ program ) )
& ( sk8
| ~ ( A @ sk9 )
| ( A @ sk10 @ program )
| ~ ( A @ program ) ) ),
inference(cnf,[status(esa)],[30]) ).
thf(35,plain,
! [A: $i] :
( sk8
| ~ ( A @ sk9 )
| ( A @ sk10 @ program )
| ~ ( A @ program ) ),
inference(cnfConj,[status(thm)],[31]) ).
thf(2554,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| sk8
| ~ ( A @ sk9 )
| ( A @ sk10 @ program )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[370,35]) ).
thf(2555,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| sk8
| ~ ( A @ sk9 )
| ( A @ sk10 @ program ) ),
inference(simp,[status(thm)],[2554]) ).
thf(2556,plain,
( sk8
| ~ ( sk4 @ sk9 )
| ( sk4 @ sk10 @ program ) ),
inference(pattern_uni,[status(thm)],[2555:[bind(A,$thf( sk4 ))]]) ).
thf(4,axiom,
! [A: $i] :
( ( ! [B: $i] :
( ( B @ program )
=> ! [C: $i] : ( C @ ( B @ ( A @ decides ) ) ) )
& ( A @ program ) )
=> ! [B: $i,C: $i] :
( ( ( ~ ( C @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( C @ ( B @ ( A @ halts3 ) ) ) ) )
& ( ( ( C @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( good @ ( A @ outputs ) )
& ( C @ ( B @ ( A @ halts3 ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2) ).
thf(18,plain,
! [A: $i] :
( ( ! [B: $i] :
( ( B @ program )
=> ! [C: $i] : ( C @ ( B @ ( A @ decides ) ) ) )
& ( A @ program ) )
=> ! [B: $i,C: $i] :
( ( ( ~ ( C @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( C @ ( B @ ( A @ halts3 ) ) ) ) )
& ( ( ( C @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( good @ ( A @ outputs ) )
& ( C @ ( B @ ( A @ halts3 ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(19,plain,
! [A: $i] :
( ( ! [B: $i] :
( ( B @ program )
=> ! [C: $i] : ( C @ ( B @ ( A @ decides ) ) ) )
& ( A @ program ) )
=> ( ! [B: $i,C: $i] :
( ( ~ ( C @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( C @ ( B @ ( A @ halts3 ) ) ) ) )
& ! [B: $i,C: $i] :
( ( ( C @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( good @ ( A @ outputs ) )
& ( C @ ( B @ ( A @ halts3 ) ) ) ) ) ) ),
inference(miniscope,[status(thm)],[18]) ).
thf(20,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( A @ outputs ) )
| ( E @ ( D @ halts2 ) )
| ~ ( D @ program )
| ~ ( A @ sk5 ) )
& ( ( E @ ( D @ ( A @ halts3 ) ) )
| ( E @ ( D @ halts2 ) )
| ~ ( D @ program )
| ~ ( A @ sk5 ) )
& ( ( good @ ( A @ outputs ) )
| ~ ( C @ ( B @ halts2 ) )
| ~ ( B @ program )
| ~ ( A @ sk5 ) )
& ( ( C @ ( B @ ( A @ halts3 ) ) )
| ~ ( C @ ( B @ halts2 ) )
| ~ ( B @ program )
| ~ ( A @ sk5 ) )
& ( ( A @ sk5 )
| ~ ( A @ sk7 @ ( A @ sk6 @ ( A @ decides ) ) )
| ~ ( A @ program ) )
& ( ( A @ sk5 )
| ( A @ sk6 @ program )
| ~ ( A @ program ) ) ),
inference(cnf,[status(esa)],[19]) ).
thf(25,plain,
! [A: $i] :
( ( A @ sk5 )
| ( A @ sk6 @ program )
| ~ ( A @ program ) ),
inference(cnfConj,[status(thm)],[20]) ).
thf(21,plain,
! [A: $i] :
( ( A @ sk5 )
| ~ ( A @ sk7 @ ( A @ sk6 @ ( A @ decides ) ) )
| ~ ( A @ program ) ),
inference(cnfConj,[status(thm)],[20]) ).
thf(624,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( sk1 @ decides ) ) )
!= ( C @ sk7 @ ( C @ sk6 @ ( C @ decides ) ) ) )
| ( C @ sk5 )
| ~ $true
| ~ ( C @ program )
| ~ ( A @ program ) ),
inference(paramod_ordered,[status(thm)],[11,21]) ).
thf(625,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( sk1 @ decides ) ) )
!= ( C @ sk7 @ ( C @ sk6 @ ( C @ decides ) ) ) )
| ( C @ sk5 )
| ~ ( C @ program )
| ~ ( A @ program ) ),
inference(simp,[status(thm)],[624]) ).
thf(626,plain,
( ( sk1 @ sk5 )
| ~ ( sk1 @ program )
| ~ ( sk1 @ sk6 @ program ) ),
inference(pattern_uni,[status(thm)],[625:[bind(A,$thf( sk1 @ sk6 )),bind(B,$thf( sk1 @ sk7 )),bind(C,$thf( sk1 ))]]) ).
thf(854,plain,
! [A: $i] :
( ( ( A @ sk6 @ program )
!= ( sk1 @ sk6 @ program ) )
| ( sk1 @ sk5 )
| ~ ( sk1 @ program )
| ~ $true
| ( A @ sk5 )
| ~ ( A @ program ) ),
inference(paramod_ordered,[status(thm)],[25,626]) ).
thf(855,plain,
! [A: $i] :
( ( ( A @ sk6 @ program )
!= ( sk1 @ sk6 @ program ) )
| ( sk1 @ sk5 )
| ~ ( sk1 @ program )
| ( A @ sk5 )
| ~ ( A @ program ) ),
inference(simp,[status(thm)],[854]) ).
thf(856,plain,
( ( sk1 @ sk5 )
| ~ ( sk1 @ program )
| ( sk1 @ sk5 )
| ~ ( sk1 @ program ) ),
inference(pattern_uni,[status(thm)],[855:[bind(A,$thf( sk1 ))]]) ).
thf(929,plain,
( ( sk1 @ sk5 )
| ~ ( sk1 @ program ) ),
inference(simp,[status(thm)],[856]) ).
thf(2667,plain,
( ( ( sk4 @ sk10 @ program )
!= ( sk1 @ program ) )
| ( sk1 @ sk5 )
| ~ $true
| sk8
| ~ ( sk4 @ sk9 ) ),
inference(paramod_ordered,[status(thm)],[2556,929]) ).
thf(2668,plain,
( ( ( sk4 @ sk10 @ program )
!= ( sk1 @ program ) )
| ( sk1 @ sk5 )
| sk8
| ~ ( sk4 @ sk9 ) ),
inference(simp,[status(thm)],[2667]) ).
thf(2682,plain,
( ( ( sk4 @ sk10 )
!= sk1 )
| ~ ( sk4 @ sk9 )
| ( sk1 @ sk5 )
| sk8 ),
inference(simp,[status(thm)],[2668]) ).
thf(41,plain,
! [A: $i] :
( sk8
| ( A @ sk11 @ program )
| ( A @ sk9 )
| ~ ( A @ program ) ),
inference(cnfConj,[status(thm)],[31]) ).
thf(374,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| sk8
| ( A @ sk11 @ program )
| ( A @ sk9 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[370,41]) ).
thf(375,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| sk8
| ( A @ sk11 @ program )
| ( A @ sk9 ) ),
inference(simp,[status(thm)],[374]) ).
thf(376,plain,
( sk8
| ( sk4 @ sk11 @ program )
| ( sk4 @ sk9 ) ),
inference(pattern_uni,[status(thm)],[375:[bind(A,$thf( sk4 ))]]) ).
thf(42,plain,
! [A: $i] :
( sk8
| ~ ( A @ sk9 )
| ( A @ sk10 @ ( A @ sk10 @ halts2 ) )
| ~ ( A @ program ) ),
inference(cnfConj,[status(thm)],[31]) ).
thf(3612,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| sk8
| ~ ( A @ sk9 )
| ( A @ sk10 @ ( A @ sk10 @ halts2 ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[370,42]) ).
thf(3613,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| sk8
| ~ ( A @ sk9 )
| ( A @ sk10 @ ( A @ sk10 @ halts2 ) ) ),
inference(simp,[status(thm)],[3612]) ).
thf(3614,plain,
( sk8
| ~ ( sk4 @ sk9 )
| ( sk4 @ sk10 @ ( sk4 @ sk10 @ halts2 ) ) ),
inference(pattern_uni,[status(thm)],[3613:[bind(A,$thf( sk4 ))]]) ).
thf(3677,plain,
( ( ( sk4 @ sk9 )
!= ( sk4 @ sk9 ) )
| sk8
| ~ $true
| ( sk4 @ sk10 @ ( sk4 @ sk10 @ halts2 ) )
| sk8
| ( sk4 @ sk11 @ program ) ),
inference(paramod_ordered,[status(thm)],[376,3614]) ).
thf(3678,plain,
( ( ( sk4 @ sk9 )
!= ( sk4 @ sk9 ) )
| ( sk4 @ sk10 @ ( sk4 @ sk10 @ halts2 ) )
| sk8
| ( sk4 @ sk11 @ program ) ),
inference(simp,[status(thm)],[3677]) ).
thf(3679,plain,
( ( sk4 @ sk10 @ ( sk4 @ sk10 @ halts2 ) )
| sk8
| ( sk4 @ sk11 @ program ) ),
inference(pattern_uni,[status(thm)],[3678:[]]) ).
thf(505,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ( A @ sk6 @ program )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[370,25]) ).
thf(506,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ( A @ sk6 @ program ) ),
inference(simp,[status(thm)],[505]) ).
thf(507,plain,
( ( sk4 @ sk5 )
| ( sk4 @ sk6 @ program ) ),
inference(pattern_uni,[status(thm)],[506:[bind(A,$thf( sk4 ))]]) ).
thf(545,plain,
! [A: $i] :
( ( ( sk4 @ sk6 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ( A @ sk6 @ program )
| ~ $true
| ( sk4 @ sk5 ) ),
inference(paramod_ordered,[status(thm)],[507,25]) ).
thf(546,plain,
! [A: $i] :
( ( ( sk4 @ sk6 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ( A @ sk6 @ program )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[545]) ).
thf(547,plain,
( ( sk4 @ sk6 @ sk5 )
| ( sk4 @ sk6 @ sk6 @ program )
| ( sk4 @ sk5 ) ),
inference(pattern_uni,[status(thm)],[546:[bind(A,$thf( sk4 @ sk6 ))]]) ).
thf(15,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( sk4 @ decides ) ) )
| ~ ( B @ program )
| ( A @ sk2 @ program )
| ~ ( A @ algorithm ) ),
inference(cnfConj,[status(thm)],[13]) ).
thf(6,axiom,
( ? [A: $i] :
( ! [B: $i] :
( ( ( ~ ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) )
& ( ( ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( good @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) ) )
& ( A @ program ) )
=> ? [A: $i] :
( ! [B: $i] :
( ( ( ~ ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) )
& ( ( ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ~ ( B @ ( A @ halts2 ) ) ) )
& ( A @ program ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p4) ).
thf(47,plain,
( ? [A: $i] :
( ! [B: $i] :
( ( ( ~ ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) )
& ( ( ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( good @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) ) )
& ( A @ program ) )
=> ? [A: $i] :
( ! [B: $i] :
( ( ( ~ ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) )
& ( ( ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ~ ( B @ ( A @ halts2 ) ) ) )
& ( A @ program ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(48,plain,
( ? [A: $i] :
( ! [B: $i] :
( ( ~ ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) )
& ! [B: $i] :
( ( ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( good @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) )
& ( A @ program ) )
=> ? [A: $i] :
( ! [B: $i] :
( ( ~ ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ( ( bad @ ( A @ outputs ) )
& ( B @ ( A @ halts2 ) ) ) )
& ! [B: $i] :
( ( ( B @ ( B @ halts2 ) )
& ( B @ program ) )
=> ~ ( B @ ( A @ halts2 ) ) )
& ( A @ program ) ) ),
inference(miniscope,[status(thm)],[47]) ).
thf(49,plain,
! [C: $i,B: $i,A: $i] :
( ( ~ ( bad @ ( C @ outputs ) )
| ~ ( C @ sk16 @ ( C @ halts2 ) )
| ( C @ sk14 )
| ~ ( C @ program )
| sk8 )
& ( ~ ( C @ sk16 @ ( C @ sk16 @ halts2 ) )
| ( C @ sk14 )
| ~ ( C @ program )
| sk8 )
& ( ( C @ sk16 @ program )
| ( C @ sk14 )
| ~ ( C @ program )
| sk8 )
& ( ~ ( C @ sk14 )
| ~ ( good @ ( C @ outputs ) )
| ~ ( C @ sk15 @ ( C @ halts2 ) )
| ~ ( C @ program )
| sk8 )
& ( ~ ( C @ sk14 )
| ( C @ sk15 @ ( C @ sk15 @ halts2 ) )
| ~ ( C @ program )
| sk8 )
& ( ~ ( C @ sk14 )
| ( C @ sk15 @ program )
| ~ ( C @ program )
| sk8 )
& ( ( bad @ ( sk13 @ outputs ) )
| ( B @ ( B @ halts2 ) )
| ~ ( B @ program )
| ~ sk8 )
& ( ( B @ ( sk13 @ halts2 ) )
| ( B @ ( B @ halts2 ) )
| ~ ( B @ program )
| ~ sk8 )
& ( ~ ( A @ ( sk13 @ halts2 ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ ( A @ program )
| ~ sk8 )
& ( ( sk13 @ program )
| ~ sk8 ) ),
inference(cnf,[status(esa)],[48]) ).
thf(53,plain,
! [A: $i] :
( ~ ( A @ ( sk13 @ halts2 ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ ( A @ program )
| ~ sk8 ),
inference(cnfConj,[status(thm)],[49]) ).
thf(171,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ sk2 @ program )
!= ( D @ program ) )
| ~ ( D @ ( sk13 @ halts2 ) )
| ~ ( D @ ( D @ halts2 ) )
| ~ $true
| ~ sk8
| ( C @ ( B @ ( sk4 @ decides ) ) )
| ~ ( B @ program )
| ~ ( A @ algorithm ) ),
inference(paramod_ordered,[status(thm)],[15,53]) ).
thf(172,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ sk2 @ program )
!= ( D @ program ) )
| ~ ( D @ ( sk13 @ halts2 ) )
| ~ ( D @ ( D @ halts2 ) )
| ~ sk8
| ( C @ ( B @ ( sk4 @ decides ) ) )
| ~ ( B @ program )
| ~ ( A @ algorithm ) ),
inference(simp,[status(thm)],[171]) ).
thf(173,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( C @ sk2 @ ( C @ sk2 @ halts2 ) )
| ~ sk8
| ( B @ ( A @ ( sk4 @ decides ) ) )
| ~ ( A @ program )
| ~ ( C @ algorithm ) ),
inference(pattern_uni,[status(thm)],[172:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( E @ sk2 ))]]) ).
thf(211,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( C @ sk2 @ ( C @ sk2 @ halts2 ) )
| ~ sk8
| ( B @ ( A @ ( sk4 @ decides ) ) )
| ~ ( A @ program )
| ~ ( C @ algorithm ) ),
inference(simp,[status(thm)],[173]) ).
thf(54,plain,
( ( sk13 @ program )
| ~ sk8 ),
inference(cnfConj,[status(thm)],[49]) ).
thf(653,plain,
! [A: $i] :
( ( ( sk13 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ~ ( A @ sk7 @ ( A @ sk6 @ ( A @ decides ) ) )
| ~ $true
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[54,21]) ).
thf(654,plain,
! [A: $i] :
( ( ( sk13 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ~ ( A @ sk7 @ ( A @ sk6 @ ( A @ decides ) ) )
| ~ sk8 ),
inference(simp,[status(thm)],[653]) ).
thf(655,plain,
( ( sk13 @ sk5 )
| ~ ( sk13 @ sk7 @ ( sk13 @ sk6 @ ( sk13 @ decides ) ) )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[654:[bind(A,$thf( sk13 ))]]) ).
thf(1499,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( sk4 @ decides ) ) )
!= ( sk13 @ sk7 @ ( sk13 @ sk6 @ ( sk13 @ decides ) ) ) )
| ( sk13 @ sk5 )
| ~ $true
| ~ sk8
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( C @ sk2 @ ( C @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm ) ),
inference(paramod_ordered,[status(thm)],[211,655]) ).
thf(1500,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( sk4 @ decides ) ) )
!= ( sk13 @ sk7 @ ( sk13 @ sk6 @ ( sk13 @ decides ) ) ) )
| ( sk13 @ sk5 )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( C @ sk2 @ ( C @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm ) ),
inference(simp,[status(thm)],[1499]) ).
thf(1525,plain,
! [C: $i,B: $i,A: $i] :
( ( B
!= ( sk13 @ sk7 ) )
| ( A
!= ( sk13 @ sk6 ) )
| ( sk13 != sk4 )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( C @ sk2 @ ( C @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm )
| ( sk13 @ sk5 ) ),
inference(simp,[status(thm)],[1500]) ).
thf(1533,plain,
! [A: $i] :
( ( sk13 != sk4 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( A @ sk2 @ ( A @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( sk13 @ sk6 @ program )
| ~ ( A @ algorithm )
| ( sk13 @ sk5 ) ),
inference(simp,[status(thm)],[1525]) ).
thf(4337,plain,
! [B: $i,A: $i] :
( ( ( A @ sk6 @ program )
!= ( sk13 @ sk6 @ program ) )
| ( sk13 != sk4 )
| ~ ( B @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( B @ sk2 @ ( B @ sk2 @ halts2 ) )
| ~ sk8
| ~ $true
| ~ ( B @ algorithm )
| ( sk13 @ sk5 )
| ( A @ sk5 )
| ~ ( A @ program ) ),
inference(paramod_ordered,[status(thm)],[25,1533]) ).
thf(4338,plain,
! [B: $i,A: $i] :
( ( ( A @ sk6 @ program )
!= ( sk13 @ sk6 @ program ) )
| ( sk13 != sk4 )
| ~ ( B @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( B @ sk2 @ ( B @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( B @ algorithm )
| ( sk13 @ sk5 )
| ( A @ sk5 )
| ~ ( A @ program ) ),
inference(simp,[status(thm)],[4337]) ).
thf(4339,plain,
! [A: $i] :
( ( sk13 != sk4 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( A @ sk2 @ ( A @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( A @ algorithm )
| ( sk13 @ sk5 )
| ( sk13 @ sk5 )
| ~ ( sk13 @ program ) ),
inference(pattern_uni,[status(thm)],[4338:[bind(A,$thf( sk13 ))]]) ).
thf(4424,plain,
! [A: $i] :
( ( sk13 != sk4 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( A @ sk2 @ ( A @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( A @ algorithm )
| ( sk13 @ sk5 )
| ~ ( sk13 @ program ) ),
inference(simp,[status(thm)],[4339]) ).
thf(643,plain,
! [A: $i] :
( ( ( sk4 @ sk6 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ~ ( A @ sk7 @ ( A @ sk6 @ ( A @ decides ) ) )
| ~ $true
| ( sk4 @ sk5 ) ),
inference(paramod_ordered,[status(thm)],[507,21]) ).
thf(644,plain,
! [A: $i] :
( ( ( sk4 @ sk6 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ~ ( A @ sk7 @ ( A @ sk6 @ ( A @ decides ) ) )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[643]) ).
thf(645,plain,
( ( sk4 @ sk6 @ sk5 )
| ~ ( sk4 @ sk6 @ sk7 @ ( sk4 @ sk6 @ sk6 @ ( sk4 @ sk6 @ decides ) ) )
| ( sk4 @ sk5 ) ),
inference(pattern_uni,[status(thm)],[644:[bind(A,$thf( sk4 @ sk6 ))]]) ).
thf(938,plain,
( ( ( sk4 @ program )
!= ( sk1 @ program ) )
| ( sk1 @ sk5 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[370,929]) ).
thf(939,plain,
( ( ( sk4 @ program )
!= ( sk1 @ program ) )
| ( sk1 @ sk5 ) ),
inference(simp,[status(thm)],[938]) ).
thf(962,plain,
( ( sk4 != sk1 )
| ( sk1 @ sk5 ) ),
inference(simp,[status(thm)],[939]) ).
thf(580,plain,
! [A: $i] :
( ( ( sk4 @ sk6 @ sk6 @ program )
!= ( A @ program ) )
| sk8
| ( A @ sk11 @ program )
| ( A @ sk9 )
| ~ $true
| ( sk4 @ sk6 @ sk5 )
| ( sk4 @ sk5 ) ),
inference(paramod_ordered,[status(thm)],[547,41]) ).
thf(581,plain,
! [A: $i] :
( ( ( sk4 @ sk6 @ sk6 @ program )
!= ( A @ program ) )
| sk8
| ( A @ sk11 @ program )
| ( A @ sk9 )
| ( sk4 @ sk6 @ sk5 )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[580]) ).
thf(582,plain,
( sk8
| ( sk4 @ sk6 @ sk6 @ sk11 @ program )
| ( sk4 @ sk6 @ sk6 @ sk9 )
| ( sk4 @ sk6 @ sk5 )
| ( sk4 @ sk5 ) ),
inference(pattern_uni,[status(thm)],[581:[bind(A,$thf( sk4 @ sk6 @ sk6 ))]]) ).
thf(583,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ sk6 @ sk6 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ~ $true
| ( sk4 @ sk6 @ sk5 )
| ( sk4 @ sk5 ) ),
inference(paramod_ordered,[status(thm)],[547,11]) ).
thf(584,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ sk6 @ sk6 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ( sk4 @ sk6 @ sk5 )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[583]) ).
thf(585,plain,
! [A: $i] :
( ( A @ ( sk4 @ sk6 @ sk6 @ ( sk1 @ decides ) ) )
| ( sk4 @ sk6 @ sk5 )
| ( sk4 @ sk5 ) ),
inference(pattern_uni,[status(thm)],[584:[bind(A,$thf( sk4 @ sk6 @ sk6 )),bind(B,$thf( B ))]]) ).
thf(603,plain,
! [A: $i] :
( ( A @ ( sk4 @ sk6 @ sk6 @ ( sk1 @ decides ) ) )
| ( sk4 @ sk6 @ sk5 )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[585]) ).
thf(2275,plain,
! [A: $i] :
( ( ( A @ ( sk4 @ sk6 @ sk6 @ ( sk1 @ decides ) ) )
!= ( sk4 @ sk6 @ sk7 @ ( sk4 @ sk6 @ sk6 @ ( sk4 @ sk6 @ decides ) ) ) )
| ( sk4 @ sk6 @ sk5 )
| ~ $true
| ( sk4 @ sk5 )
| ( sk4 @ sk6 @ sk5 )
| ( sk4 @ sk5 ) ),
inference(paramod_ordered,[status(thm)],[603,645]) ).
thf(2276,plain,
! [A: $i] :
( ( ( A @ ( sk4 @ sk6 @ sk6 @ ( sk1 @ decides ) ) )
!= ( sk4 @ sk6 @ sk7 @ ( sk4 @ sk6 @ sk6 @ ( sk4 @ sk6 @ decides ) ) ) )
| ( sk4 @ sk6 @ sk5 )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[2275]) ).
thf(2286,plain,
! [A: $i] :
( ( A
!= ( sk4 @ sk6 @ sk7 ) )
| ( ( sk4 @ sk6 @ sk6 )
!= ( sk4 @ sk6 @ sk6 ) )
| ( ( sk4 @ sk6 )
!= sk1 )
| ( sk4 @ sk6 @ sk5 )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[2276]) ).
thf(2300,plain,
( ( ( sk4 @ sk6 )
!= sk1 )
| ( sk4 @ sk6 @ sk5 )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[2286]) ).
thf(2775,plain,
( ~ $true
| ( ( sk4 @ sk6 @ sk5 )
!= ( sk4 @ sk5 ) )
| ( ( sk4 @ sk6 )
!= sk1 )
| ( sk4 @ sk5 ) ),
inference(eqfactor_ordered,[status(thm)],[2300]) ).
thf(2776,plain,
( ( ( sk4 @ sk6 @ sk5 )
!= ( sk4 @ sk5 ) )
| ( ( sk4 @ sk6 )
!= sk1 )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[2775]) ).
thf(265,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ( ( C @ sk2 @ ( C @ sk2 @ halts2 ) )
!= ( C @ sk2 @ ( sk13 @ halts2 ) ) )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ( B @ ( A @ ( sk4 @ decides ) ) )
| ~ ( A @ program )
| ~ ( C @ algorithm ) ),
inference(eqfactor_ordered,[status(thm)],[211]) ).
thf(267,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ sk2 )
!= ( C @ sk2 ) )
| ( ( C @ sk2 )
!= sk13 )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm )
| ( B @ ( A @ ( sk4 @ decides ) ) ) ),
inference(simp,[status(thm)],[265]) ).
thf(271,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ sk2 )
!= sk13 )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm )
| ( B @ ( A @ ( sk4 @ decides ) ) ) ),
inference(simp,[status(thm)],[267]) ).
thf(39,plain,
( ( sk12 @ program )
| ~ sk8 ),
inference(cnfConj,[status(thm)],[31]) ).
thf(658,plain,
! [A: $i] :
( ( ( sk12 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ~ ( A @ sk7 @ ( A @ sk6 @ ( A @ decides ) ) )
| ~ $true
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[39,21]) ).
thf(659,plain,
! [A: $i] :
( ( ( sk12 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ~ ( A @ sk7 @ ( A @ sk6 @ ( A @ decides ) ) )
| ~ sk8 ),
inference(simp,[status(thm)],[658]) ).
thf(660,plain,
( ( sk12 @ sk5 )
| ~ ( sk12 @ sk7 @ ( sk12 @ sk6 @ ( sk12 @ decides ) ) )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[659:[bind(A,$thf( sk12 ))]]) ).
thf(1547,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( sk4 @ decides ) ) )
!= ( sk12 @ sk7 @ ( sk12 @ sk6 @ ( sk12 @ decides ) ) ) )
| ( sk12 @ sk5 )
| ~ $true
| ~ sk8
| ( ( C @ sk2 )
!= sk13 )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm ) ),
inference(paramod_ordered,[status(thm)],[271,660]) ).
thf(1548,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( sk4 @ decides ) ) )
!= ( sk12 @ sk7 @ ( sk12 @ sk6 @ ( sk12 @ decides ) ) ) )
| ( sk12 @ sk5 )
| ( ( C @ sk2 )
!= sk13 )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm ) ),
inference(simp,[status(thm)],[1547]) ).
thf(1560,plain,
! [C: $i,B: $i,A: $i] :
( ( B
!= ( sk12 @ sk7 ) )
| ( A
!= ( sk12 @ sk6 ) )
| ( sk12 != sk4 )
| ( ( C @ sk2 )
!= sk13 )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm )
| ( sk12 @ sk5 ) ),
inference(simp,[status(thm)],[1548]) ).
thf(1569,plain,
! [A: $i] :
( ( sk12 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( sk12 @ sk6 @ program )
| ~ ( A @ algorithm )
| ( sk12 @ sk5 ) ),
inference(simp,[status(thm)],[1560]) ).
thf(2664,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ sk10 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ~ $true
| sk8
| ~ ( sk4 @ sk9 ) ),
inference(paramod_ordered,[status(thm)],[2556,11]) ).
thf(2665,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ sk10 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| sk8
| ~ ( sk4 @ sk9 ) ),
inference(simp,[status(thm)],[2664]) ).
thf(2666,plain,
! [A: $i] :
( ( A @ ( sk4 @ sk10 @ ( sk1 @ decides ) ) )
| sk8
| ~ ( sk4 @ sk9 ) ),
inference(pattern_uni,[status(thm)],[2665:[bind(A,$thf( sk4 @ sk10 )),bind(B,$thf( B ))]]) ).
thf(2686,plain,
! [A: $i] :
( ( A @ ( sk4 @ sk10 @ ( sk1 @ decides ) ) )
| sk8
| ~ ( sk4 @ sk9 ) ),
inference(simp,[status(thm)],[2666]) ).
thf(554,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ sk6 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ~ $true
| ( sk4 @ sk5 ) ),
inference(paramod_ordered,[status(thm)],[507,11]) ).
thf(555,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ sk6 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[554]) ).
thf(556,plain,
! [A: $i] :
( ( A @ ( sk4 @ sk6 @ ( sk1 @ decides ) ) )
| ( sk4 @ sk5 ) ),
inference(pattern_uni,[status(thm)],[555:[bind(A,$thf( sk4 @ sk6 )),bind(B,$thf( B ))]]) ).
thf(572,plain,
! [A: $i] :
( ( A @ ( sk4 @ sk6 @ ( sk1 @ decides ) ) )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[556]) ).
thf(621,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ~ ( A @ sk7 @ ( A @ sk6 @ ( A @ decides ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[370,21]) ).
thf(622,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ~ ( A @ sk7 @ ( A @ sk6 @ ( A @ decides ) ) ) ),
inference(simp,[status(thm)],[621]) ).
thf(623,plain,
( ( sk4 @ sk5 )
| ~ ( sk4 @ sk7 @ ( sk4 @ sk6 @ ( sk4 @ decides ) ) ) ),
inference(pattern_uni,[status(thm)],[622:[bind(A,$thf( sk4 ))]]) ).
thf(698,plain,
! [A: $i] :
( ( ( A @ ( sk4 @ sk6 @ ( sk1 @ decides ) ) )
!= ( sk4 @ sk7 @ ( sk4 @ sk6 @ ( sk4 @ decides ) ) ) )
| ( sk4 @ sk5 )
| ~ $true
| ( sk4 @ sk5 ) ),
inference(paramod_ordered,[status(thm)],[572,623]) ).
thf(699,plain,
! [A: $i] :
( ( ( A @ ( sk4 @ sk6 @ ( sk1 @ decides ) ) )
!= ( sk4 @ sk7 @ ( sk4 @ sk6 @ ( sk4 @ decides ) ) ) )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[698]) ).
thf(706,plain,
! [A: $i] :
( ( A
!= ( sk4 @ sk7 ) )
| ( ( sk4 @ sk6 )
!= ( sk4 @ sk6 ) )
| ( sk4 != sk1 )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[699]) ).
thf(712,plain,
( ( sk4 != sk1 )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[706]) ).
thf(24,plain,
! [C: $i,B: $i,A: $i] :
( ( good @ ( A @ outputs ) )
| ~ ( C @ ( B @ halts2 ) )
| ~ ( B @ program )
| ~ ( A @ sk5 ) ),
inference(cnfConj,[status(thm)],[20]) ).
thf(1164,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk4 @ program )
!= ( B @ program ) )
| ( good @ ( A @ outputs ) )
| ~ ( C @ ( B @ halts2 ) )
| ~ $true
| ~ ( A @ sk5 ) ),
inference(paramod_ordered,[status(thm)],[370,24]) ).
thf(1165,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk4 @ program )
!= ( B @ program ) )
| ( good @ ( A @ outputs ) )
| ~ ( C @ ( B @ halts2 ) )
| ~ ( A @ sk5 ) ),
inference(simp,[status(thm)],[1164]) ).
thf(1166,plain,
! [B: $i,A: $i] :
( ( good @ ( A @ outputs ) )
| ~ ( B @ ( sk4 @ halts2 ) )
| ~ ( A @ sk5 ) ),
inference(pattern_uni,[status(thm)],[1165:[bind(A,$thf( A )),bind(B,$thf( sk4 ))]]) ).
thf(1219,plain,
! [B: $i,A: $i] :
( ( good @ ( A @ outputs ) )
| ~ ( B @ ( sk4 @ halts2 ) )
| ~ ( A @ sk5 ) ),
inference(simp,[status(thm)],[1166]) ).
thf(3341,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ sk5 )
!= ( A @ sk5 ) )
| ( good @ ( A @ outputs ) )
| ~ ( B @ ( sk4 @ halts2 ) )
| ~ $true
| ( sk4 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[712,1219]) ).
thf(3342,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ sk5 )
!= ( A @ sk5 ) )
| ( good @ ( A @ outputs ) )
| ~ ( B @ ( sk4 @ halts2 ) )
| ( sk4 != sk1 ) ),
inference(simp,[status(thm)],[3341]) ).
thf(3343,plain,
! [A: $i] :
( ( good @ ( sk4 @ outputs ) )
| ~ ( A @ ( sk4 @ halts2 ) )
| ( sk4 != sk1 ) ),
inference(pattern_uni,[status(thm)],[3342:[bind(A,$thf( sk4 ))]]) ).
thf(3367,plain,
! [A: $i] :
( ( good @ ( sk4 @ outputs ) )
| ~ ( A @ ( sk4 @ halts2 ) )
| ( sk4 != sk1 ) ),
inference(simp,[status(thm)],[3343]) ).
thf(3306,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ sk5 )
!= ( A @ sk5 ) )
| ( good @ ( A @ outputs ) )
| ~ ( B @ ( sk4 @ halts2 ) )
| ~ $true
| ( sk4 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[962,1219]) ).
thf(3307,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ sk5 )
!= ( A @ sk5 ) )
| ( good @ ( A @ outputs ) )
| ~ ( B @ ( sk4 @ halts2 ) )
| ( sk4 != sk1 ) ),
inference(simp,[status(thm)],[3306]) ).
thf(3308,plain,
! [A: $i] :
( ( good @ ( sk1 @ outputs ) )
| ~ ( A @ ( sk4 @ halts2 ) )
| ( sk4 != sk1 ) ),
inference(pattern_uni,[status(thm)],[3307:[bind(A,$thf( sk1 ))]]) ).
thf(3365,plain,
! [A: $i] :
( ( good @ ( sk1 @ outputs ) )
| ~ ( A @ ( sk4 @ halts2 ) )
| ( sk4 != sk1 ) ),
inference(simp,[status(thm)],[3308]) ).
thf(526,plain,
! [A: $i] :
( ( ( sk13 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ( A @ sk6 @ program )
| ~ $true
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[54,25]) ).
thf(527,plain,
! [A: $i] :
( ( ( sk13 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ( A @ sk6 @ program )
| ~ sk8 ),
inference(simp,[status(thm)],[526]) ).
thf(528,plain,
( ( sk13 @ sk5 )
| ( sk13 @ sk6 @ program )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[527:[bind(A,$thf( sk13 ))]]) ).
thf(729,plain,
! [B: $i,A: $i] :
( ( ( sk13 @ sk6 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ~ $true
| ( sk13 @ sk5 )
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[528,11]) ).
thf(730,plain,
! [B: $i,A: $i] :
( ( ( sk13 @ sk6 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ( sk13 @ sk5 )
| ~ sk8 ),
inference(simp,[status(thm)],[729]) ).
thf(731,plain,
! [A: $i] :
( ( A @ ( sk13 @ sk6 @ ( sk1 @ decides ) ) )
| ( sk13 @ sk5 )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[730:[bind(A,$thf( sk13 @ sk6 )),bind(B,$thf( B ))]]) ).
thf(747,plain,
! [A: $i] :
( ( A @ ( sk13 @ sk6 @ ( sk1 @ decides ) ) )
| ( sk13 @ sk5 )
| ~ sk8 ),
inference(simp,[status(thm)],[731]) ).
thf(1509,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( sk4 @ decides ) ) )
!= ( sk13 @ sk7 @ ( sk13 @ sk6 @ ( sk13 @ decides ) ) ) )
| ( sk13 @ sk5 )
| ~ $true
| ~ sk8
| ( ( C @ sk2 )
!= sk13 )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm ) ),
inference(paramod_ordered,[status(thm)],[271,655]) ).
thf(1510,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( sk4 @ decides ) ) )
!= ( sk13 @ sk7 @ ( sk13 @ sk6 @ ( sk13 @ decides ) ) ) )
| ( sk13 @ sk5 )
| ( ( C @ sk2 )
!= sk13 )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm ) ),
inference(simp,[status(thm)],[1509]) ).
thf(1521,plain,
! [C: $i,B: $i,A: $i] :
( ( B
!= ( sk13 @ sk7 ) )
| ( A
!= ( sk13 @ sk6 ) )
| ( sk13 != sk4 )
| ( ( C @ sk2 )
!= sk13 )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm )
| ( sk13 @ sk5 ) ),
inference(simp,[status(thm)],[1510]) ).
thf(1529,plain,
! [A: $i] :
( ( sk13 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( sk13 @ sk6 @ program )
| ~ ( A @ algorithm )
| ( sk13 @ sk5 ) ),
inference(simp,[status(thm)],[1521]) ).
thf(37,plain,
! [A: $i] :
( sk8
| ~ ( A @ sk9 )
| ~ ( good @ ( A @ outputs ) )
| ~ ( A @ sk10 @ ( A @ sk10 @ ( A @ halts3 ) ) )
| ~ ( A @ program ) ),
inference(cnfConj,[status(thm)],[31]) ).
thf(3321,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ sk5 )
!= ( A @ sk5 ) )
| ( good @ ( A @ outputs ) )
| ~ ( B @ ( sk4 @ halts2 ) )
| ~ $true
| ( sk4 @ sk6 @ program ) ),
inference(paramod_ordered,[status(thm)],[507,1219]) ).
thf(3322,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ sk5 )
!= ( A @ sk5 ) )
| ( good @ ( A @ outputs ) )
| ~ ( B @ ( sk4 @ halts2 ) )
| ( sk4 @ sk6 @ program ) ),
inference(simp,[status(thm)],[3321]) ).
thf(3323,plain,
! [A: $i] :
( ( good @ ( sk4 @ outputs ) )
| ~ ( A @ ( sk4 @ halts2 ) )
| ( sk4 @ sk6 @ program ) ),
inference(pattern_uni,[status(thm)],[3322:[bind(A,$thf( sk4 ))]]) ).
thf(3374,plain,
! [A: $i] :
( ( good @ ( sk4 @ outputs ) )
| ~ ( A @ ( sk4 @ halts2 ) )
| ( sk4 @ sk6 @ program ) ),
inference(simp,[status(thm)],[3323]) ).
thf(32,plain,
! [A: $i] :
( ( A @ ( sk12 @ halts2 ) )
| ( A @ ( A @ halts2 ) )
| ~ ( A @ program )
| ~ sk8 ),
inference(cnfConj,[status(thm)],[31]) ).
thf(46,plain,
! [A: $i] :
( ( A @ ( sk12 @ halts2 ) )
| ( A @ ( A @ halts2 ) )
| ~ ( A @ program )
| ~ sk8 ),
inference(simp,[status(thm)],[32]) ).
thf(1537,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( sk4 @ decides ) ) )
!= ( sk12 @ sk7 @ ( sk12 @ sk6 @ ( sk12 @ decides ) ) ) )
| ( sk12 @ sk5 )
| ~ $true
| ~ sk8
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( C @ sk2 @ ( C @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm ) ),
inference(paramod_ordered,[status(thm)],[211,660]) ).
thf(1538,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( sk4 @ decides ) ) )
!= ( sk12 @ sk7 @ ( sk12 @ sk6 @ ( sk12 @ decides ) ) ) )
| ( sk12 @ sk5 )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( C @ sk2 @ ( C @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm ) ),
inference(simp,[status(thm)],[1537]) ).
thf(1563,plain,
! [C: $i,B: $i,A: $i] :
( ( B
!= ( sk12 @ sk7 ) )
| ( A
!= ( sk12 @ sk6 ) )
| ( sk12 != sk4 )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( C @ sk2 @ ( C @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm )
| ( sk12 @ sk5 ) ),
inference(simp,[status(thm)],[1538]) ).
thf(1572,plain,
! [A: $i] :
( ( sk12 != sk4 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( A @ sk2 @ ( A @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( sk12 @ sk6 @ program )
| ~ ( A @ algorithm )
| ( sk12 @ sk5 ) ),
inference(simp,[status(thm)],[1563]) ).
thf(598,plain,
( ~ $true
| ( ( sk4 @ sk6 @ sk5 )
!= ( sk4 @ sk5 ) )
| ( sk4 @ sk6 @ sk6 @ program )
| ( sk4 @ sk5 ) ),
inference(eqfactor_ordered,[status(thm)],[547]) ).
thf(600,plain,
( ( ( sk4 @ sk6 )
!= sk4 )
| ( sk4 @ sk6 @ sk6 @ program )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[598]) ).
thf(1479,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ sk6 @ sk6 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ~ $true
| ( ( sk4 @ sk6 )
!= sk4 )
| ( sk4 @ sk5 ) ),
inference(paramod_ordered,[status(thm)],[600,11]) ).
thf(1480,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ sk6 @ sk6 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ( ( sk4 @ sk6 )
!= sk4 )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[1479]) ).
thf(1481,plain,
! [A: $i] :
( ( A @ ( sk4 @ sk6 @ sk6 @ ( sk1 @ decides ) ) )
| ( ( sk4 @ sk6 )
!= sk4 )
| ( sk4 @ sk5 ) ),
inference(pattern_uni,[status(thm)],[1480:[bind(A,$thf( sk4 @ sk6 @ sk6 )),bind(B,$thf( B ))]]) ).
thf(1494,plain,
! [A: $i] :
( ( A @ ( sk4 @ sk6 @ sk6 @ ( sk1 @ decides ) ) )
| ( ( sk4 @ sk6 )
!= sk4 )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[1481]) ).
thf(1857,plain,
! [A: $i] :
( ( ( A @ ( sk13 @ sk6 @ ( sk1 @ decides ) ) )
!= ( sk13 @ sk7 @ ( sk13 @ sk6 @ ( sk13 @ decides ) ) ) )
| ( sk13 @ sk5 )
| ~ $true
| ~ sk8
| ( sk13 @ sk5 )
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[747,655]) ).
thf(1858,plain,
! [A: $i] :
( ( ( A @ ( sk13 @ sk6 @ ( sk1 @ decides ) ) )
!= ( sk13 @ sk7 @ ( sk13 @ sk6 @ ( sk13 @ decides ) ) ) )
| ( sk13 @ sk5 )
| ~ sk8 ),
inference(simp,[status(thm)],[1857]) ).
thf(1870,plain,
! [A: $i] :
( ( A
!= ( sk13 @ sk7 ) )
| ( ( sk13 @ sk6 )
!= ( sk13 @ sk6 ) )
| ( sk13 != sk1 )
| ~ sk8
| ( sk13 @ sk5 ) ),
inference(simp,[status(thm)],[1858]) ).
thf(1875,plain,
( ( sk13 != sk1 )
| ~ sk8
| ( sk13 @ sk5 ) ),
inference(simp,[status(thm)],[1870]) ).
thf(517,plain,
! [A: $i] :
( ( ( sk4 @ sk11 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ( A @ sk6 @ program )
| ~ $true
| sk8
| ( sk4 @ sk9 ) ),
inference(paramod_ordered,[status(thm)],[376,25]) ).
thf(518,plain,
! [A: $i] :
( ( ( sk4 @ sk11 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ( A @ sk6 @ program )
| sk8
| ( sk4 @ sk9 ) ),
inference(simp,[status(thm)],[517]) ).
thf(519,plain,
( ( sk4 @ sk11 @ sk5 )
| ( sk4 @ sk11 @ sk6 @ program )
| sk8
| ( sk4 @ sk9 ) ),
inference(pattern_uni,[status(thm)],[518:[bind(A,$thf( sk4 @ sk11 ))]]) ).
thf(1098,plain,
! [A: $i] :
( ( ( sk4 @ sk11 @ sk6 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ( A @ sk6 @ program )
| ~ $true
| ( sk4 @ sk11 @ sk5 )
| sk8
| ( sk4 @ sk9 ) ),
inference(paramod_ordered,[status(thm)],[519,25]) ).
thf(1099,plain,
! [A: $i] :
( ( ( sk4 @ sk11 @ sk6 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ( A @ sk6 @ program )
| ( sk4 @ sk11 @ sk5 )
| sk8
| ( sk4 @ sk9 ) ),
inference(simp,[status(thm)],[1098]) ).
thf(1100,plain,
( ( sk4 @ sk11 @ sk6 @ sk5 )
| ( sk4 @ sk11 @ sk6 @ sk6 @ program )
| ( sk4 @ sk11 @ sk5 )
| sk8
| ( sk4 @ sk9 ) ),
inference(pattern_uni,[status(thm)],[1099:[bind(A,$thf( sk4 @ sk11 @ sk6 ))]]) ).
thf(76,plain,
! [A: $i] :
( ( ( sk13 @ program )
!= ( A @ program ) )
| ~ ( A @ ( sk13 @ halts2 ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ $true
| ~ sk8
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[54,53]) ).
thf(77,plain,
! [A: $i] :
( ( ( sk13 @ program )
!= ( A @ program ) )
| ~ ( A @ ( sk13 @ halts2 ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[76]) ).
thf(78,plain,
( ~ ( sk13 @ ( sk13 @ halts2 ) )
| ~ ( sk13 @ ( sk13 @ halts2 ) )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[77:[bind(A,$thf( sk13 ))]]) ).
thf(84,plain,
( ~ ( sk13 @ ( sk13 @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[78]) ).
thf(2777,plain,
( ( ( sk4 @ sk6 )
!= sk4 )
| ( ( sk4 @ sk6 )
!= sk1 )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[2775]) ).
thf(403,plain,
! [A: $i] :
( ( ( sk4 @ sk11 @ program )
!= ( A @ program ) )
| sk8
| ( A @ sk11 @ program )
| ( A @ sk9 )
| ~ $true
| sk8
| ( sk4 @ sk9 ) ),
inference(paramod_ordered,[status(thm)],[376,41]) ).
thf(404,plain,
! [A: $i] :
( ( ( sk4 @ sk11 @ program )
!= ( A @ program ) )
| ( A @ sk11 @ program )
| ( A @ sk9 )
| sk8
| ( sk4 @ sk9 ) ),
inference(simp,[status(thm)],[403]) ).
thf(405,plain,
( ( sk4 @ sk11 @ sk11 @ program )
| ( sk4 @ sk11 @ sk9 )
| sk8
| ( sk4 @ sk9 ) ),
inference(pattern_uni,[status(thm)],[404:[bind(A,$thf( sk4 @ sk11 ))]]) ).
thf(819,plain,
! [A: $i] :
( ( ( sk4 @ sk11 @ sk11 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ( A @ sk6 @ program )
| ~ $true
| ( sk4 @ sk11 @ sk9 )
| sk8
| ( sk4 @ sk9 ) ),
inference(paramod_ordered,[status(thm)],[405,25]) ).
thf(820,plain,
! [A: $i] :
( ( ( sk4 @ sk11 @ sk11 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ( A @ sk6 @ program )
| ( sk4 @ sk11 @ sk9 )
| sk8
| ( sk4 @ sk9 ) ),
inference(simp,[status(thm)],[819]) ).
thf(821,plain,
( ( sk4 @ sk11 @ sk11 @ sk5 )
| ( sk4 @ sk11 @ sk11 @ sk6 @ program )
| ( sk4 @ sk11 @ sk9 )
| sk8
| ( sk4 @ sk9 ) ),
inference(pattern_uni,[status(thm)],[820:[bind(A,$thf( sk4 @ sk11 @ sk11 ))]]) ).
thf(79,plain,
! [A: $i] :
( ( ( sk12 @ program )
!= ( A @ program ) )
| ~ ( A @ ( sk13 @ halts2 ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ $true
| ~ sk8
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[39,53]) ).
thf(80,plain,
! [A: $i] :
( ( ( sk12 @ program )
!= ( A @ program ) )
| ~ ( A @ ( sk13 @ halts2 ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[79]) ).
thf(81,plain,
( ~ ( sk12 @ ( sk13 @ halts2 ) )
| ~ ( sk12 @ ( sk12 @ halts2 ) )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[80:[bind(A,$thf( sk12 ))]]) ).
thf(146,plain,
( ~ $true
| ( ( sk12 @ ( sk13 @ halts2 ) )
!= ( sk12 @ ( sk12 @ halts2 ) ) )
| ~ ( sk12 @ ( sk12 @ halts2 ) )
| ~ sk8 ),
inference(eqfactor_ordered,[status(thm)],[81]) ).
thf(147,plain,
( ( ( sk12 @ ( sk13 @ halts2 ) )
!= ( sk12 @ ( sk12 @ halts2 ) ) )
| ~ ( sk12 @ ( sk12 @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[146]) ).
thf(371,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| ~ ( A @ ( sk13 @ halts2 ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ $true
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[370,53]) ).
thf(372,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| ~ ( A @ ( sk13 @ halts2 ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[371]) ).
thf(373,plain,
( ~ ( sk4 @ ( sk13 @ halts2 ) )
| ~ ( sk4 @ ( sk4 @ halts2 ) )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[372:[bind(A,$thf( sk4 ))]]) ).
thf(396,plain,
( ~ $true
| ( ( sk4 @ ( sk13 @ halts2 ) )
!= ( sk4 @ ( sk4 @ halts2 ) ) )
| ~ ( sk4 @ ( sk4 @ halts2 ) )
| ~ sk8 ),
inference(eqfactor_ordered,[status(thm)],[373]) ).
thf(397,plain,
( ( ( sk4 @ ( sk13 @ halts2 ) )
!= ( sk4 @ ( sk4 @ halts2 ) ) )
| ~ ( sk4 @ ( sk4 @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[396]) ).
thf(40,plain,
! [A: $i] :
( ( bad @ ( sk12 @ outputs ) )
| ( A @ ( A @ halts2 ) )
| ~ ( A @ program )
| ~ sk8 ),
inference(cnfConj,[status(thm)],[31]) ).
thf(43,plain,
! [A: $i] :
( ( bad @ ( sk12 @ outputs ) )
| ( A @ ( A @ halts2 ) )
| ~ ( A @ program )
| ~ sk8 ),
inference(simp,[status(thm)],[40]) ).
thf(4085,plain,
! [A: $i] :
( ( ( sk13 @ program )
!= ( A @ program ) )
| ( bad @ ( sk12 @ outputs ) )
| ( A @ ( A @ halts2 ) )
| ~ $true
| ~ sk8
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[54,43]) ).
thf(4086,plain,
! [A: $i] :
( ( ( sk13 @ program )
!= ( A @ program ) )
| ( bad @ ( sk12 @ outputs ) )
| ( A @ ( A @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[4085]) ).
thf(4087,plain,
( ( bad @ ( sk12 @ outputs ) )
| ( sk13 @ ( sk13 @ halts2 ) )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[4086:[bind(A,$thf( sk13 ))]]) ).
thf(2618,plain,
( ( ( sk4 @ sk9 )
!= ( sk4 @ sk9 ) )
| sk8
| ~ $true
| ( sk4 @ sk10 @ program )
| sk8
| ( sk4 @ sk11 @ program ) ),
inference(paramod_ordered,[status(thm)],[376,2556]) ).
thf(2619,plain,
( ( ( sk4 @ sk9 )
!= ( sk4 @ sk9 ) )
| ( sk4 @ sk10 @ program )
| sk8
| ( sk4 @ sk11 @ program ) ),
inference(simp,[status(thm)],[2618]) ).
thf(2620,plain,
( ( sk4 @ sk10 @ program )
| sk8
| ( sk4 @ sk11 @ program ) ),
inference(pattern_uni,[status(thm)],[2619:[]]) ).
thf(2749,plain,
( ~ $true
| ( ( sk4 @ sk11 @ program )
!= ( sk4 @ sk10 @ program ) )
| ( sk4 @ sk10 @ program )
| sk8 ),
inference(eqfactor_ordered,[status(thm)],[2620]) ).
thf(2750,plain,
( ( ( sk4 @ sk11 @ program )
!= ( sk4 @ sk10 @ program ) )
| ( sk4 @ sk10 @ program )
| sk8 ),
inference(simp,[status(thm)],[2749]) ).
thf(3224,plain,
! [A: $i] :
( ( ( sk4 @ sk9 )
!= ( sk4 @ sk9 ) )
| ( A @ ( sk4 @ sk10 @ ( sk1 @ decides ) ) )
| sk8
| ~ $true
| sk8
| ( sk4 @ sk11 @ program ) ),
inference(paramod_ordered,[status(thm)],[376,2686]) ).
thf(3225,plain,
! [A: $i] :
( ( ( sk4 @ sk9 )
!= ( sk4 @ sk9 ) )
| ( A @ ( sk4 @ sk10 @ ( sk1 @ decides ) ) )
| sk8
| ( sk4 @ sk11 @ program ) ),
inference(simp,[status(thm)],[3224]) ).
thf(3226,plain,
! [A: $i] :
( ( A @ ( sk4 @ sk10 @ ( sk1 @ decides ) ) )
| sk8
| ( sk4 @ sk11 @ program ) ),
inference(pattern_uni,[status(thm)],[3225:[]]) ).
thf(68,plain,
! [B: $i,A: $i] :
( ( ( sk13 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ~ $true
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[54,11]) ).
thf(69,plain,
! [B: $i,A: $i] :
( ( ( sk13 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ~ sk8 ),
inference(simp,[status(thm)],[68]) ).
thf(70,plain,
! [A: $i] :
( ( A @ ( sk13 @ ( sk1 @ decides ) ) )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[69:[bind(A,$thf( sk13 ))]]) ).
thf(74,plain,
! [A: $i] :
( ( A @ ( sk13 @ ( sk1 @ decides ) ) )
| ~ sk8 ),
inference(simp,[status(thm)],[70]) ).
thf(529,plain,
! [A: $i] :
( ( ( sk12 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ( A @ sk6 @ program )
| ~ $true
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[39,25]) ).
thf(530,plain,
! [A: $i] :
( ( ( sk12 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ( A @ sk6 @ program )
| ~ sk8 ),
inference(simp,[status(thm)],[529]) ).
thf(531,plain,
( ( sk12 @ sk5 )
| ( sk12 @ sk6 @ program )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[530:[bind(A,$thf( sk12 ))]]) ).
thf(936,plain,
( ( ( sk12 @ sk6 @ program )
!= ( sk1 @ program ) )
| ( sk1 @ sk5 )
| ~ $true
| ( sk12 @ sk5 )
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[531,929]) ).
thf(937,plain,
( ( ( sk12 @ sk6 @ program )
!= ( sk1 @ program ) )
| ( sk1 @ sk5 )
| ( sk12 @ sk5 )
| ~ sk8 ),
inference(simp,[status(thm)],[936]) ).
thf(957,plain,
( ( ( sk12 @ sk6 )
!= sk1 )
| ~ sk8
| ( sk1 @ sk5 )
| ( sk12 @ sk5 ) ),
inference(simp,[status(thm)],[937]) ).
thf(23,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ halts3 ) ) )
| ( C @ ( B @ halts2 ) )
| ~ ( B @ program )
| ~ ( A @ sk5 ) ),
inference(cnfConj,[status(thm)],[20]) ).
thf(28,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ halts3 ) ) )
| ( C @ ( B @ halts2 ) )
| ~ ( B @ program )
| ~ ( A @ sk5 ) ),
inference(simp,[status(thm)],[23]) ).
thf(3347,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ sk5 )
!= ( A @ sk5 ) )
| ( good @ ( A @ outputs ) )
| ~ ( B @ ( sk4 @ halts2 ) )
| ~ $true
| ~ ( sk1 @ program ) ),
inference(paramod_ordered,[status(thm)],[929,1219]) ).
thf(3348,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ sk5 )
!= ( A @ sk5 ) )
| ( good @ ( A @ outputs ) )
| ~ ( B @ ( sk4 @ halts2 ) )
| ~ ( sk1 @ program ) ),
inference(simp,[status(thm)],[3347]) ).
thf(3349,plain,
! [A: $i] :
( ( good @ ( sk1 @ outputs ) )
| ~ ( A @ ( sk4 @ halts2 ) )
| ~ ( sk1 @ program ) ),
inference(pattern_uni,[status(thm)],[3348:[bind(A,$thf( sk1 ))]]) ).
thf(3371,plain,
! [A: $i] :
( ( good @ ( sk1 @ outputs ) )
| ~ ( A @ ( sk4 @ halts2 ) )
| ~ ( sk1 @ program ) ),
inference(simp,[status(thm)],[3349]) ).
thf(761,plain,
! [B: $i,A: $i] :
( ( ( sk12 @ sk6 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ~ $true
| ( sk12 @ sk5 )
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[531,11]) ).
thf(762,plain,
! [B: $i,A: $i] :
( ( ( sk12 @ sk6 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ( sk12 @ sk5 )
| ~ sk8 ),
inference(simp,[status(thm)],[761]) ).
thf(763,plain,
! [A: $i] :
( ( A @ ( sk12 @ sk6 @ ( sk1 @ decides ) ) )
| ( sk12 @ sk5 )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[762:[bind(A,$thf( sk12 @ sk6 )),bind(B,$thf( B ))]]) ).
thf(779,plain,
! [A: $i] :
( ( A @ ( sk12 @ sk6 @ ( sk1 @ decides ) ) )
| ( sk12 @ sk5 )
| ~ sk8 ),
inference(simp,[status(thm)],[763]) ).
thf(1897,plain,
! [A: $i] :
( ( ( A @ ( sk12 @ sk6 @ ( sk1 @ decides ) ) )
!= ( sk12 @ sk7 @ ( sk12 @ sk6 @ ( sk12 @ decides ) ) ) )
| ( sk12 @ sk5 )
| ~ $true
| ~ sk8
| ( sk12 @ sk5 )
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[779,660]) ).
thf(1898,plain,
! [A: $i] :
( ( ( A @ ( sk12 @ sk6 @ ( sk1 @ decides ) ) )
!= ( sk12 @ sk7 @ ( sk12 @ sk6 @ ( sk12 @ decides ) ) ) )
| ( sk12 @ sk5 )
| ~ sk8 ),
inference(simp,[status(thm)],[1897]) ).
thf(1906,plain,
! [A: $i] :
( ( A
!= ( sk12 @ sk7 ) )
| ( ( sk12 @ sk6 )
!= ( sk12 @ sk6 ) )
| ( sk12 != sk1 )
| ~ sk8
| ( sk12 @ sk5 ) ),
inference(simp,[status(thm)],[1898]) ).
thf(1910,plain,
( ( sk12 != sk1 )
| ~ sk8
| ( sk12 @ sk5 ) ),
inference(simp,[status(thm)],[1906]) ).
thf(1104,plain,
! [A: $i] :
( ( ( sk4 @ sk11 @ sk6 @ program )
!= ( A @ program ) )
| sk8
| ( A @ sk11 @ program )
| ( A @ sk9 )
| ~ $true
| ( sk4 @ sk11 @ sk5 )
| sk8
| ( sk4 @ sk9 ) ),
inference(paramod_ordered,[status(thm)],[519,41]) ).
thf(1105,plain,
! [A: $i] :
( ( ( sk4 @ sk11 @ sk6 @ program )
!= ( A @ program ) )
| ( A @ sk11 @ program )
| ( A @ sk9 )
| ( sk4 @ sk11 @ sk5 )
| sk8
| ( sk4 @ sk9 ) ),
inference(simp,[status(thm)],[1104]) ).
thf(1106,plain,
( ( sk4 @ sk11 @ sk6 @ sk11 @ program )
| ( sk4 @ sk11 @ sk6 @ sk9 )
| ( sk4 @ sk11 @ sk5 )
| sk8
| ( sk4 @ sk9 ) ),
inference(pattern_uni,[status(thm)],[1105:[bind(A,$thf( sk4 @ sk11 @ sk6 ))]]) ).
thf(1957,plain,
! [A: $i] :
( ( ( sk12 @ sk6 @ program )
!= ( sk12 @ program ) )
| ( sk12 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ $true
| ~ ( A @ algorithm )
| ( sk12 @ sk5 )
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[39,1569]) ).
thf(1958,plain,
! [A: $i] :
( ( ( sk12 @ sk6 @ program )
!= ( sk12 @ program ) )
| ( sk12 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( A @ algorithm )
| ( sk12 @ sk5 )
| ~ sk8 ),
inference(simp,[status(thm)],[1957]) ).
thf(1983,plain,
! [A: $i] :
( ( ( sk12 @ sk6 )
!= sk12 )
| ( sk12 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( A @ algorithm )
| ~ sk8
| ( sk12 @ sk5 ) ),
inference(simp,[status(thm)],[1958]) ).
thf(36,plain,
! [A: $i] :
( sk8
| ~ ( A @ sk11 @ ( A @ sk11 @ halts2 ) )
| ( A @ sk9 )
| ~ ( A @ program ) ),
inference(cnfConj,[status(thm)],[31]) ).
thf(3003,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| sk8
| ~ ( A @ sk11 @ ( A @ sk11 @ halts2 ) )
| ( A @ sk9 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[370,36]) ).
thf(3004,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| sk8
| ~ ( A @ sk11 @ ( A @ sk11 @ halts2 ) )
| ( A @ sk9 ) ),
inference(simp,[status(thm)],[3003]) ).
thf(3005,plain,
( sk8
| ~ ( sk4 @ sk11 @ ( sk4 @ sk11 @ halts2 ) )
| ( sk4 @ sk9 ) ),
inference(pattern_uni,[status(thm)],[3004:[bind(A,$thf( sk4 ))]]) ).
thf(2632,plain,
( ( ( sk4 @ sk9 )
!= ( sk4 @ sk9 ) )
| sk8
| ~ $true
| ( sk4 @ sk10 @ program )
| ( sk4 @ sk11 @ sk5 )
| ( sk4 @ sk11 @ sk6 @ program )
| sk8 ),
inference(paramod_ordered,[status(thm)],[519,2556]) ).
thf(2633,plain,
( ( ( sk4 @ sk9 )
!= ( sk4 @ sk9 ) )
| ( sk4 @ sk10 @ program )
| ( sk4 @ sk11 @ sk5 )
| ( sk4 @ sk11 @ sk6 @ program )
| sk8 ),
inference(simp,[status(thm)],[2632]) ).
thf(2634,plain,
( ( sk4 @ sk10 @ program )
| ( sk4 @ sk11 @ sk5 )
| ( sk4 @ sk11 @ sk6 @ program )
| sk8 ),
inference(pattern_uni,[status(thm)],[2633:[]]) ).
thf(1582,plain,
! [A: $i] :
( ( ( sk13 @ sk6 @ program )
!= ( sk4 @ program ) )
| ( sk13 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ $true
| ~ ( A @ algorithm )
| ( sk13 @ sk5 ) ),
inference(paramod_ordered,[status(thm)],[370,1529]) ).
thf(1583,plain,
! [A: $i] :
( ( ( sk13 @ sk6 @ program )
!= ( sk4 @ program ) )
| ( sk13 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ algorithm )
| ( sk13 @ sk5 ) ),
inference(simp,[status(thm)],[1582]) ).
thf(1616,plain,
! [A: $i] :
( ( ( sk13 @ sk6 )
!= sk4 )
| ( sk13 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ algorithm )
| ( sk13 @ sk5 ) ),
inference(simp,[status(thm)],[1583]) ).
thf(34,plain,
! [A: $i] :
( sk8
| ~ ( bad @ ( A @ outputs ) )
| ~ ( A @ sk11 @ ( A @ sk11 @ ( A @ halts3 ) ) )
| ( A @ sk9 )
| ~ ( A @ program ) ),
inference(cnfConj,[status(thm)],[31]) ).
thf(33,plain,
! [A: $i] :
( ( A @ ( sk12 @ halts2 ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ ( A @ program )
| ~ sk8 ),
inference(cnfConj,[status(thm)],[31]) ).
thf(45,plain,
! [A: $i] :
( ( A @ ( sk12 @ halts2 ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ ( A @ program )
| ~ sk8 ),
inference(simp,[status(thm)],[33]) ).
thf(17,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( sk4 @ decides ) ) )
| ~ ( B @ program )
| ~ ( A @ sk3 @ ( A @ sk2 @ ( A @ decides ) ) )
| ~ ( A @ algorithm ) ),
inference(cnfConj,[status(thm)],[13]) ).
thf(4114,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| ( bad @ ( sk12 @ outputs ) )
| ( A @ ( A @ halts2 ) )
| ~ $true
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[370,43]) ).
thf(4115,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| ( bad @ ( sk12 @ outputs ) )
| ( A @ ( A @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[4114]) ).
thf(4116,plain,
( ( bad @ ( sk12 @ outputs ) )
| ( sk4 @ ( sk4 @ halts2 ) )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[4115:[bind(A,$thf( sk4 ))]]) ).
thf(38,plain,
! [A: $i] :
( ( good @ ( sk12 @ outputs ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ ( A @ program )
| ~ sk8 ),
inference(cnfConj,[status(thm)],[31]) ).
thf(44,plain,
! [A: $i] :
( ( good @ ( sk12 @ outputs ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ ( A @ program )
| ~ sk8 ),
inference(simp,[status(thm)],[38]) ).
thf(1596,plain,
! [A: $i] :
( ( ( sk13 @ sk6 @ program )
!= ( sk13 @ program ) )
| ( sk13 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ $true
| ~ ( A @ algorithm )
| ( sk13 @ sk5 )
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[54,1529]) ).
thf(1597,plain,
! [A: $i] :
( ( ( sk13 @ sk6 @ program )
!= ( sk13 @ program ) )
| ( sk13 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( A @ algorithm )
| ( sk13 @ sk5 )
| ~ sk8 ),
inference(simp,[status(thm)],[1596]) ).
thf(1620,plain,
! [A: $i] :
( ( ( sk13 @ sk6 )
!= sk13 )
| ( sk13 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( A @ algorithm )
| ~ sk8
| ( sk13 @ sk5 ) ),
inference(simp,[status(thm)],[1597]) ).
thf(2714,plain,
! [A: $i] :
( ( ( sk4 @ sk11 @ program )
!= ( A @ program ) )
| sk8
| ( A @ sk11 @ program )
| ( A @ sk9 )
| ~ $true
| ( sk4 @ sk10 @ program )
| sk8 ),
inference(paramod_ordered,[status(thm)],[2620,41]) ).
thf(2715,plain,
! [A: $i] :
( ( ( sk4 @ sk11 @ program )
!= ( A @ program ) )
| ( A @ sk11 @ program )
| ( A @ sk9 )
| ( sk4 @ sk10 @ program )
| sk8 ),
inference(simp,[status(thm)],[2714]) ).
thf(2716,plain,
( ( sk4 @ sk11 @ sk11 @ program )
| ( sk4 @ sk11 @ sk9 )
| ( sk4 @ sk10 @ program )
| sk8 ),
inference(pattern_uni,[status(thm)],[2715:[bind(A,$thf( sk4 @ sk11 ))]]) ).
thf(26,plain,
! [C: $i,B: $i,A: $i] :
( ( bad @ ( A @ outputs ) )
| ( C @ ( B @ halts2 ) )
| ~ ( B @ program )
| ~ ( A @ sk5 ) ),
inference(cnfConj,[status(thm)],[20]) ).
thf(27,plain,
! [C: $i,B: $i,A: $i] :
( ( bad @ ( A @ outputs ) )
| ( C @ ( B @ halts2 ) )
| ~ ( B @ program )
| ~ ( A @ sk5 ) ),
inference(simp,[status(thm)],[26]) ).
thf(22,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ halts3 ) ) )
| ~ ( C @ ( B @ halts2 ) )
| ~ ( B @ program )
| ~ ( A @ sk5 ) ),
inference(cnfConj,[status(thm)],[20]) ).
thf(1598,plain,
! [A: $i] :
( ( ( sk13 @ sk6 @ program )
!= ( sk12 @ program ) )
| ( sk13 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ $true
| ~ ( A @ algorithm )
| ( sk13 @ sk5 )
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[39,1529]) ).
thf(1599,plain,
! [A: $i] :
( ( ( sk13 @ sk6 @ program )
!= ( sk12 @ program ) )
| ( sk13 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( A @ algorithm )
| ( sk13 @ sk5 )
| ~ sk8 ),
inference(simp,[status(thm)],[1598]) ).
thf(1615,plain,
! [A: $i] :
( ( ( sk13 @ sk6 )
!= sk12 )
| ( sk13 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( A @ algorithm )
| ~ sk8
| ( sk13 @ sk5 ) ),
inference(simp,[status(thm)],[1599]) ).
thf(377,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[370,11]) ).
thf(378,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) ) ),
inference(simp,[status(thm)],[377]) ).
thf(379,plain,
! [A: $i] : ( A @ ( sk4 @ ( sk1 @ decides ) ) ),
inference(pattern_uni,[status(thm)],[378:[bind(A,$thf( sk4 ))]]) ).
thf(391,plain,
! [A: $i] : ( A @ ( sk4 @ ( sk1 @ decides ) ) ),
inference(simp,[status(thm)],[379]) ).
thf(599,plain,
( ( ( sk4 @ sk6 @ sk5 )
!= ( sk4 @ sk5 ) )
| ( sk4 @ sk6 @ sk6 @ program )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[598]) ).
thf(2735,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ sk11 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ~ $true
| ( sk4 @ sk10 @ program )
| sk8 ),
inference(paramod_ordered,[status(thm)],[2620,11]) ).
thf(2736,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ sk11 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ( sk4 @ sk10 @ program )
| sk8 ),
inference(simp,[status(thm)],[2735]) ).
thf(2737,plain,
! [A: $i] :
( ( A @ ( sk4 @ sk11 @ ( sk1 @ decides ) ) )
| ( sk4 @ sk10 @ program )
| sk8 ),
inference(pattern_uni,[status(thm)],[2736:[bind(A,$thf( sk4 @ sk11 )),bind(B,$thf( B ))]]) ).
thf(2757,plain,
! [A: $i] :
( ( A @ ( sk4 @ sk11 @ ( sk1 @ decides ) ) )
| ( sk4 @ sk10 @ program )
| sk8 ),
inference(simp,[status(thm)],[2737]) ).
thf(398,plain,
( ( sk4 != sk4 )
| ( sk13 != sk4 )
| ~ ( sk4 @ ( sk4 @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[396]) ).
thf(399,plain,
( ( sk13 != sk4 )
| ~ ( sk4 @ ( sk4 @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[398]) ).
thf(825,plain,
! [A: $i] :
( ( ( sk4 @ sk11 @ sk11 @ program )
!= ( A @ program ) )
| sk8
| ( A @ sk11 @ program )
| ( A @ sk9 )
| ~ $true
| ( sk4 @ sk11 @ sk9 )
| sk8
| ( sk4 @ sk9 ) ),
inference(paramod_ordered,[status(thm)],[405,41]) ).
thf(826,plain,
! [A: $i] :
( ( ( sk4 @ sk11 @ sk11 @ program )
!= ( A @ program ) )
| ( A @ sk11 @ program )
| ( A @ sk9 )
| ( sk4 @ sk11 @ sk9 )
| sk8
| ( sk4 @ sk9 ) ),
inference(simp,[status(thm)],[825]) ).
thf(827,plain,
( ( sk4 @ sk11 @ sk11 @ sk11 @ program )
| ( sk4 @ sk11 @ sk11 @ sk9 )
| ( sk4 @ sk11 @ sk9 )
| sk8
| ( sk4 @ sk9 ) ),
inference(pattern_uni,[status(thm)],[826:[bind(A,$thf( sk4 @ sk11 @ sk11 ))]]) ).
thf(551,plain,
! [A: $i] :
( ( ( sk4 @ sk6 @ program )
!= ( A @ program ) )
| sk8
| ( A @ sk11 @ program )
| ( A @ sk9 )
| ~ $true
| ( sk4 @ sk5 ) ),
inference(paramod_ordered,[status(thm)],[507,41]) ).
thf(552,plain,
! [A: $i] :
( ( ( sk4 @ sk6 @ program )
!= ( A @ program ) )
| sk8
| ( A @ sk11 @ program )
| ( A @ sk9 )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[551]) ).
thf(553,plain,
( sk8
| ( sk4 @ sk6 @ sk11 @ program )
| ( sk4 @ sk6 @ sk9 )
| ( sk4 @ sk5 ) ),
inference(pattern_uni,[status(thm)],[552:[bind(A,$thf( sk4 @ sk6 ))]]) ).
thf(940,plain,
( ( ( sk4 @ sk11 @ program )
!= ( sk1 @ program ) )
| ( sk1 @ sk5 )
| ~ $true
| sk8
| ( sk4 @ sk9 ) ),
inference(paramod_ordered,[status(thm)],[376,929]) ).
thf(941,plain,
( ( ( sk4 @ sk11 @ program )
!= ( sk1 @ program ) )
| ( sk1 @ sk5 )
| sk8
| ( sk4 @ sk9 ) ),
inference(simp,[status(thm)],[940]) ).
thf(954,plain,
( ( ( sk4 @ sk11 )
!= sk1 )
| ( sk1 @ sk5 )
| sk8
| ( sk4 @ sk9 ) ),
inference(simp,[status(thm)],[941]) ).
thf(1964,plain,
! [A: $i] :
( ( ( sk12 @ sk6 @ program )
!= ( sk4 @ program ) )
| ( sk12 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ $true
| ~ ( A @ algorithm )
| ( sk12 @ sk5 ) ),
inference(paramod_ordered,[status(thm)],[370,1569]) ).
thf(1965,plain,
! [A: $i] :
( ( ( sk12 @ sk6 @ program )
!= ( sk4 @ program ) )
| ( sk12 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ algorithm )
| ( sk12 @ sk5 ) ),
inference(simp,[status(thm)],[1964]) ).
thf(1980,plain,
! [A: $i] :
( ( ( sk12 @ sk6 )
!= sk4 )
| ( sk12 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ algorithm )
| ( sk12 @ sk5 ) ),
inference(simp,[status(thm)],[1965]) ).
thf(574,plain,
! [A: $i] :
( ( ( sk4 @ sk6 @ sk6 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ( A @ sk6 @ program )
| ~ $true
| ( sk4 @ sk6 @ sk5 )
| ( sk4 @ sk5 ) ),
inference(paramod_ordered,[status(thm)],[547,25]) ).
thf(575,plain,
! [A: $i] :
( ( ( sk4 @ sk6 @ sk6 @ program )
!= ( A @ program ) )
| ( A @ sk5 )
| ( A @ sk6 @ program )
| ( sk4 @ sk6 @ sk5 )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[574]) ).
thf(576,plain,
( ( sk4 @ sk6 @ sk6 @ sk5 )
| ( sk4 @ sk6 @ sk6 @ sk6 @ program )
| ( sk4 @ sk6 @ sk5 )
| ( sk4 @ sk5 ) ),
inference(pattern_uni,[status(thm)],[575:[bind(A,$thf( sk4 @ sk6 @ sk6 ))]]) ).
thf(4693,plain,
! [A: $i] :
( ( ( sk12 @ program )
!= ( A @ program ) )
| ( good @ ( sk12 @ outputs ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ $true
| ~ sk8
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[39,44]) ).
thf(4694,plain,
! [A: $i] :
( ( ( sk12 @ program )
!= ( A @ program ) )
| ( good @ ( sk12 @ outputs ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[4693]) ).
thf(4695,plain,
( ( good @ ( sk12 @ outputs ) )
| ~ ( sk12 @ ( sk12 @ halts2 ) )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[4694:[bind(A,$thf( sk12 ))]]) ).
thf(661,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( sk4 @ decides ) ) )
!= ( D @ sk7 @ ( D @ sk6 @ ( D @ decides ) ) ) )
| ( D @ sk5 )
| ~ $true
| ~ ( D @ program )
| ( ( C @ sk2 )
!= sk13 )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm ) ),
inference(paramod_ordered,[status(thm)],[271,21]) ).
thf(662,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( sk4 @ decides ) ) )
!= ( D @ sk7 @ ( D @ sk6 @ ( D @ decides ) ) ) )
| ( D @ sk5 )
| ~ ( D @ program )
| ( ( C @ sk2 )
!= sk13 )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm ) ),
inference(simp,[status(thm)],[661]) ).
thf(663,plain,
! [A: $i] :
( ( sk4 @ sk5 )
| ~ ( sk4 @ program )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( sk4 @ sk6 @ program )
| ~ ( A @ algorithm ) ),
inference(pattern_uni,[status(thm)],[662:[bind(A,$thf( sk4 @ sk6 )),bind(B,$thf( sk4 @ sk7 )),bind(C,$thf( C )),bind(D,$thf( sk4 ))]]) ).
thf(672,plain,
! [A: $i] :
( ( sk4 @ sk5 )
| ~ ( sk4 @ program )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( sk4 @ sk6 @ program )
| ~ ( A @ algorithm ) ),
inference(simp,[status(thm)],[663]) ).
thf(782,plain,
! [A: $i] :
( ( sk4 @ sk5 )
| ~ $true
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( sk4 @ sk6 @ program )
| ~ ( A @ algorithm ) ),
inference(rewrite,[status(thm)],[672,370]) ).
thf(783,plain,
! [A: $i] :
( ( sk4 @ sk5 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( sk4 @ sk6 @ program )
| ~ ( A @ algorithm ) ),
inference(simp,[status(thm)],[782]) ).
thf(787,plain,
! [B: $i,A: $i] :
( ( ( A @ sk6 @ program )
!= ( sk4 @ sk6 @ program ) )
| ( sk4 @ sk5 )
| ( ( B @ sk2 )
!= sk13 )
| ~ ( B @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ $true
| ~ ( B @ algorithm )
| ( A @ sk5 )
| ~ ( A @ program ) ),
inference(paramod_ordered,[status(thm)],[25,783]) ).
thf(788,plain,
! [B: $i,A: $i] :
( ( ( A @ sk6 @ program )
!= ( sk4 @ sk6 @ program ) )
| ( sk4 @ sk5 )
| ( ( B @ sk2 )
!= sk13 )
| ~ ( B @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( B @ algorithm )
| ( A @ sk5 )
| ~ ( A @ program ) ),
inference(simp,[status(thm)],[787]) ).
thf(789,plain,
! [A: $i] :
( ( sk4 @ sk5 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ algorithm )
| ( sk4 @ sk5 )
| ~ ( sk4 @ program ) ),
inference(pattern_uni,[status(thm)],[788:[bind(A,$thf( sk4 ))]]) ).
thf(818,plain,
! [A: $i] :
( ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ algorithm )
| ( sk4 @ sk5 )
| ~ ( sk4 @ program ) ),
inference(simp,[status(thm)],[789]) ).
thf(1239,plain,
! [A: $i] :
( ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ algorithm )
| ( sk4 @ sk5 )
| ~ $true ),
inference(rewrite,[status(thm)],[818,370]) ).
thf(1240,plain,
! [A: $i] :
( ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ algorithm )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[1239]) ).
thf(942,plain,
( ( ( sk4 @ sk6 @ program )
!= ( sk1 @ program ) )
| ( sk1 @ sk5 )
| ~ $true
| ( sk4 @ sk5 ) ),
inference(paramod_ordered,[status(thm)],[507,929]) ).
thf(943,plain,
( ( ( sk4 @ sk6 @ program )
!= ( sk1 @ program ) )
| ( sk1 @ sk5 )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[942]) ).
thf(961,plain,
( ( ( sk4 @ sk6 )
!= sk1 )
| ( sk1 @ sk5 )
| ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[943]) ).
thf(406,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ sk11 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ~ $true
| sk8
| ( sk4 @ sk9 ) ),
inference(paramod_ordered,[status(thm)],[376,11]) ).
thf(407,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ sk11 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| sk8
| ( sk4 @ sk9 ) ),
inference(simp,[status(thm)],[406]) ).
thf(408,plain,
! [A: $i] :
( ( A @ ( sk4 @ sk11 @ ( sk1 @ decides ) ) )
| sk8
| ( sk4 @ sk9 ) ),
inference(pattern_uni,[status(thm)],[407:[bind(A,$thf( sk4 @ sk11 )),bind(B,$thf( B ))]]) ).
thf(418,plain,
! [A: $i] :
( ( A @ ( sk4 @ sk11 @ ( sk1 @ decides ) ) )
| sk8
| ( sk4 @ sk9 ) ),
inference(simp,[status(thm)],[408]) ).
thf(5978,plain,
! [A: $i] :
( ( ( sk12 @ program )
!= ( A @ program ) )
| ( A @ ( sk12 @ halts2 ) )
| ( A @ ( A @ halts2 ) )
| ~ $true
| ~ sk8
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[39,46]) ).
thf(5979,plain,
! [A: $i] :
( ( ( sk12 @ program )
!= ( A @ program ) )
| ( A @ ( sk12 @ halts2 ) )
| ( A @ ( A @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[5978]) ).
thf(5980,plain,
( ( sk12 @ ( sk12 @ halts2 ) )
| ( sk12 @ ( sk12 @ halts2 ) )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[5979:[bind(A,$thf( sk12 ))]]) ).
thf(6166,plain,
( ( sk12 @ ( sk12 @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[5980]) ).
thf(6320,plain,
( ( ( sk12 @ ( sk12 @ halts2 ) )
!= ( sk12 @ ( sk12 @ halts2 ) ) )
| ~ ( sk12 @ ( sk13 @ halts2 ) )
| ~ $true
| ~ sk8
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[6166,81]) ).
thf(6321,plain,
( ( ( sk12 @ ( sk12 @ halts2 ) )
!= ( sk12 @ ( sk12 @ halts2 ) ) )
| ~ ( sk12 @ ( sk13 @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[6320]) ).
thf(6322,plain,
( ~ ( sk12 @ ( sk13 @ halts2 ) )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[6321:[]]) ).
thf(950,plain,
( ( ( sk13 @ sk6 @ program )
!= ( sk1 @ program ) )
| ( sk1 @ sk5 )
| ~ $true
| ( sk13 @ sk5 )
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[528,929]) ).
thf(951,plain,
( ( ( sk13 @ sk6 @ program )
!= ( sk1 @ program ) )
| ( sk1 @ sk5 )
| ( sk13 @ sk5 )
| ~ sk8 ),
inference(simp,[status(thm)],[950]) ).
thf(963,plain,
( ( ( sk13 @ sk6 )
!= sk1 )
| ~ sk8
| ( sk1 @ sk5 )
| ( sk13 @ sk5 ) ),
inference(simp,[status(thm)],[951]) ).
thf(71,plain,
! [B: $i,A: $i] :
( ( ( sk12 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ~ $true
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[39,11]) ).
thf(72,plain,
! [B: $i,A: $i] :
( ( ( sk12 @ program )
!= ( A @ program ) )
| ( B @ ( A @ ( sk1 @ decides ) ) )
| ~ sk8 ),
inference(simp,[status(thm)],[71]) ).
thf(73,plain,
! [A: $i] :
( ( A @ ( sk12 @ ( sk1 @ decides ) ) )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[72:[bind(A,$thf( sk12 ))]]) ).
thf(75,plain,
! [A: $i] :
( ( A @ ( sk12 @ ( sk1 @ decides ) ) )
| ~ sk8 ),
inference(simp,[status(thm)],[73]) ).
thf(3703,plain,
( ( ( sk4 @ sk9 )
!= ( sk4 @ sk9 ) )
| sk8
| ~ $true
| ( sk4 @ sk10 @ ( sk4 @ sk10 @ halts2 ) )
| ( sk4 @ sk11 @ sk5 )
| ( sk4 @ sk11 @ sk6 @ program )
| sk8 ),
inference(paramod_ordered,[status(thm)],[519,3614]) ).
thf(3704,plain,
( ( ( sk4 @ sk9 )
!= ( sk4 @ sk9 ) )
| ( sk4 @ sk10 @ ( sk4 @ sk10 @ halts2 ) )
| ( sk4 @ sk11 @ sk5 )
| ( sk4 @ sk11 @ sk6 @ program )
| sk8 ),
inference(simp,[status(thm)],[3703]) ).
thf(3705,plain,
( ( sk4 @ sk10 @ ( sk4 @ sk10 @ halts2 ) )
| ( sk4 @ sk11 @ sk5 )
| ( sk4 @ sk11 @ sk6 @ program )
| sk8 ),
inference(pattern_uni,[status(thm)],[3704:[]]) ).
thf(4717,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| ( good @ ( sk12 @ outputs ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ $true
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[370,44]) ).
thf(4718,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| ( good @ ( sk12 @ outputs ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[4717]) ).
thf(4719,plain,
( ( good @ ( sk12 @ outputs ) )
| ~ ( sk4 @ ( sk4 @ halts2 ) )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[4718:[bind(A,$thf( sk4 ))]]) ).
thf(1941,plain,
! [B: $i,A: $i] :
( ( ( A @ sk6 @ program )
!= ( sk12 @ sk6 @ program ) )
| ( sk12 != sk4 )
| ( ( B @ sk2 )
!= sk13 )
| ~ ( B @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ $true
| ~ ( B @ algorithm )
| ( sk12 @ sk5 )
| ( A @ sk5 )
| ~ ( A @ program ) ),
inference(paramod_ordered,[status(thm)],[25,1569]) ).
thf(1942,plain,
! [B: $i,A: $i] :
( ( ( A @ sk6 @ program )
!= ( sk12 @ sk6 @ program ) )
| ( sk12 != sk4 )
| ( ( B @ sk2 )
!= sk13 )
| ~ ( B @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( B @ algorithm )
| ( sk12 @ sk5 )
| ( A @ sk5 )
| ~ ( A @ program ) ),
inference(simp,[status(thm)],[1941]) ).
thf(1943,plain,
! [A: $i] :
( ( sk12 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ algorithm )
| ( sk12 @ sk5 )
| ( sk12 @ sk5 )
| ~ ( sk12 @ program ) ),
inference(pattern_uni,[status(thm)],[1942:[bind(A,$thf( sk12 ))]]) ).
thf(1986,plain,
! [A: $i] :
( ( sk12 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ algorithm )
| ( sk12 @ sk5 )
| ~ ( sk12 @ program ) ),
inference(simp,[status(thm)],[1943]) ).
thf(6277,plain,
( ( ( sk12 @ ( sk12 @ halts2 ) )
!= ( sk4 @ ( sk4 @ halts2 ) ) )
| ( ( sk4 @ ( sk13 @ halts2 ) )
!= ( sk4 @ ( sk4 @ halts2 ) ) )
| ~ $true
| ~ sk8
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[6166,397]) ).
thf(6278,plain,
( ( ( sk12 @ ( sk12 @ halts2 ) )
!= ( sk4 @ ( sk4 @ halts2 ) ) )
| ( ( sk4 @ ( sk13 @ halts2 ) )
!= ( sk4 @ ( sk4 @ halts2 ) ) )
| ~ sk8 ),
inference(simp,[status(thm)],[6277]) ).
thf(6370,plain,
( ( sk12 != sk4 )
| ( sk12 != sk4 )
| ( sk4 != sk4 )
| ( sk13 != sk4 )
| ~ sk8 ),
inference(simp,[status(thm)],[6278]) ).
thf(6411,plain,
( ( sk12 != sk4 )
| ( sk13 != sk4 )
| ~ sk8 ),
inference(simp,[status(thm)],[6370]) ).
thf(2751,plain,
( ( ( sk4 @ sk11 )
!= ( sk4 @ sk10 ) )
| ( sk4 @ sk10 @ program )
| sk8 ),
inference(simp,[status(thm)],[2749]) ).
thf(640,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( sk4 @ decides ) ) )
!= ( D @ sk7 @ ( D @ sk6 @ ( D @ decides ) ) ) )
| ( D @ sk5 )
| ~ $true
| ~ ( D @ program )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( C @ sk2 @ ( C @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm ) ),
inference(paramod_ordered,[status(thm)],[211,21]) ).
thf(641,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( sk4 @ decides ) ) )
!= ( D @ sk7 @ ( D @ sk6 @ ( D @ decides ) ) ) )
| ( D @ sk5 )
| ~ ( D @ program )
| ~ ( C @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( C @ sk2 @ ( C @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( A @ program )
| ~ ( C @ algorithm ) ),
inference(simp,[status(thm)],[640]) ).
thf(642,plain,
! [A: $i] :
( ( sk4 @ sk5 )
| ~ ( sk4 @ program )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( A @ sk2 @ ( A @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( sk4 @ sk6 @ program )
| ~ ( A @ algorithm ) ),
inference(pattern_uni,[status(thm)],[641:[bind(A,$thf( sk4 @ sk6 )),bind(B,$thf( sk4 @ sk7 )),bind(C,$thf( C )),bind(D,$thf( sk4 ))]]) ).
thf(669,plain,
! [A: $i] :
( ( sk4 @ sk5 )
| ~ ( sk4 @ program )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( A @ sk2 @ ( A @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( sk4 @ sk6 @ program )
| ~ ( A @ algorithm ) ),
inference(simp,[status(thm)],[642]) ).
thf(1055,plain,
! [A: $i] :
( ( sk4 @ sk5 )
| ~ $true
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( A @ sk2 @ ( A @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( sk4 @ sk6 @ program )
| ~ ( A @ algorithm ) ),
inference(rewrite,[status(thm)],[669,370]) ).
thf(1056,plain,
! [A: $i] :
( ( sk4 @ sk5 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( A @ sk2 @ ( A @ sk2 @ halts2 ) )
| ~ sk8
| ~ ( sk4 @ sk6 @ program )
| ~ ( A @ algorithm ) ),
inference(simp,[status(thm)],[1055]) ).
thf(946,plain,
( ( ( sk12 @ program )
!= ( sk1 @ program ) )
| ( sk1 @ sk5 )
| ~ $true
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[39,929]) ).
thf(947,plain,
( ( ( sk12 @ program )
!= ( sk1 @ program ) )
| ( sk1 @ sk5 )
| ~ sk8 ),
inference(simp,[status(thm)],[946]) ).
thf(960,plain,
( ( sk12 != sk1 )
| ~ sk8
| ( sk1 @ sk5 ) ),
inference(simp,[status(thm)],[947]) ).
thf(944,plain,
( ( ( sk13 @ program )
!= ( sk1 @ program ) )
| ( sk1 @ sk5 )
| ~ $true
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[54,929]) ).
thf(945,plain,
( ( ( sk13 @ program )
!= ( sk1 @ program ) )
| ( sk1 @ sk5 )
| ~ sk8 ),
inference(simp,[status(thm)],[944]) ).
thf(955,plain,
( ( sk13 != sk1 )
| ~ sk8
| ( sk1 @ sk5 ) ),
inference(simp,[status(thm)],[945]) ).
thf(148,plain,
( ( sk12 != sk12 )
| ( sk13 != sk12 )
| ~ ( sk12 @ ( sk12 @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[146]) ).
thf(149,plain,
( ( sk13 != sk12 )
| ~ ( sk12 @ ( sk12 @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[148]) ).
thf(6307,plain,
( ( ( sk12 @ ( sk12 @ halts2 ) )
!= ( sk12 @ ( sk12 @ halts2 ) ) )
| ( sk13 != sk12 )
| ~ $true
| ~ sk8
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[6166,149]) ).
thf(6308,plain,
( ( ( sk12 @ ( sk12 @ halts2 ) )
!= ( sk12 @ ( sk12 @ halts2 ) ) )
| ( sk13 != sk12 )
| ~ sk8 ),
inference(simp,[status(thm)],[6307]) ).
thf(6309,plain,
( ( sk13 != sk12 )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[6308:[]]) ).
thf(5273,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| ( A @ ( sk12 @ halts2 ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ $true
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[370,45]) ).
thf(5274,plain,
! [A: $i] :
( ( ( sk4 @ program )
!= ( A @ program ) )
| ( A @ ( sk12 @ halts2 ) )
| ~ ( A @ ( A @ halts2 ) )
| ~ sk8 ),
inference(simp,[status(thm)],[5273]) ).
thf(5275,plain,
( ( sk4 @ ( sk12 @ halts2 ) )
| ~ ( sk4 @ ( sk4 @ halts2 ) )
| ~ sk8 ),
inference(pattern_uni,[status(thm)],[5274:[bind(A,$thf( sk4 ))]]) ).
thf(1955,plain,
! [A: $i] :
( ( ( sk12 @ sk6 @ program )
!= ( sk13 @ program ) )
| ( sk12 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ $true
| ~ ( A @ algorithm )
| ( sk12 @ sk5 )
| ~ sk8 ),
inference(paramod_ordered,[status(thm)],[54,1569]) ).
thf(1956,plain,
! [A: $i] :
( ( ( sk12 @ sk6 @ program )
!= ( sk13 @ program ) )
| ( sk12 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( A @ algorithm )
| ( sk12 @ sk5 )
| ~ sk8 ),
inference(simp,[status(thm)],[1955]) ).
thf(1976,plain,
! [A: $i] :
( ( ( sk12 @ sk6 )
!= sk13 )
| ( sk12 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ ( A @ algorithm )
| ~ sk8
| ( sk12 @ sk5 ) ),
inference(simp,[status(thm)],[1956]) ).
thf(1584,plain,
! [B: $i,A: $i] :
( ( ( A @ sk6 @ program )
!= ( sk13 @ sk6 @ program ) )
| ( sk13 != sk4 )
| ( ( B @ sk2 )
!= sk13 )
| ~ ( B @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ $true
| ~ ( B @ algorithm )
| ( sk13 @ sk5 )
| ( A @ sk5 )
| ~ ( A @ program ) ),
inference(paramod_ordered,[status(thm)],[25,1529]) ).
thf(1585,plain,
! [B: $i,A: $i] :
( ( ( A @ sk6 @ program )
!= ( sk13 @ sk6 @ program ) )
| ( sk13 != sk4 )
| ( ( B @ sk2 )
!= sk13 )
| ~ ( B @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( B @ algorithm )
| ( sk13 @ sk5 )
| ( A @ sk5 )
| ~ ( A @ program ) ),
inference(simp,[status(thm)],[1584]) ).
thf(1586,plain,
! [A: $i] :
( ( sk13 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ algorithm )
| ( sk13 @ sk5 )
| ( sk13 @ sk5 )
| ~ ( sk13 @ program ) ),
inference(pattern_uni,[status(thm)],[1585:[bind(A,$thf( sk13 ))]]) ).
thf(1621,plain,
! [A: $i] :
( ( sk13 != sk4 )
| ( ( A @ sk2 )
!= sk13 )
| ~ ( A @ sk2 @ ( sk13 @ halts2 ) )
| ~ sk8
| ~ ( A @ algorithm )
| ( sk13 @ sk5 )
| ~ ( sk13 @ program ) ),
inference(simp,[status(thm)],[1586]) ).
thf(108352,plain,
$false,
inference(e,[status(thm)],[2682,3679,547,4424,645,962,582,2776,1569,655,1533,10,2686,3367,3365,747,42,24,1529,37,25,3374,46,1572,1494,1875,1100,29,376,623,211,84,2777,821,147,397,4087,660,2750,3226,507,74,957,28,3371,21,1910,1106,1983,53,519,2300,41,779,3005,2634,1616,1219,34,45,17,2556,4116,44,1620,2716,27,22,1615,391,12,54,572,7,39,271,599,2757,3614,399,827,2620,35,531,553,712,18,954,370,1980,576,600,11,4695,43,1240,961,418,6322,963,75,929,6166,3705,36,4719,405,1986,373,603,6411,2751,1056,960,955,6309,5275,528,1976,47,15,1621]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM003+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.09 % 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.15/0.41 % Computer : n004.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Sat Sep 26 23:19:39 UTC 2026
% 0.15/0.41 % CPUTime :
% 0.15/0.41 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.89/1.04 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.43/1.29 % [INFO] Parsing done (246ms).
% 1.67/1.31 % [INFO] Running in sequential loop mode.
% 2.58/1.86 % [INFO] eprover registered as external prover.
% 2.58/1.87 % [INFO] Scanning for conjecture ...
% 2.82/1.96 % [INFO] Found a conjecture (or negated_conjecture) and 4 axioms. Running axiom selection ...
% 2.82/2.01 % [INFO] Axiom selection finished. Selected 4 axioms (removed 0 axioms).
% 3.11/2.08 % [INFO] Problem is first-order (TPTP FOF).
% 3.11/2.09 % [INFO] Type checking passed.
% 3.11/2.10 % [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 ...
% 202.68/51.24 % External prover 'e' found a proof!
% 202.68/51.24 % [INFO] Killing All external provers ...
% 202.68/51.25 % Time passed: 50690ms (effective reasoning time: 49928ms)
% 202.68/51.25 % 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)>
% 202.68/51.25 % Axioms used in derivation (4): p1, p3, p2, p4
% 202.68/51.25 % No. of inferences in proof: 383
% 202.68/51.25 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 50690 ms resp. 49928 ms w/o parsing
% 202.26/51.43 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 202.26/51.43 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------