%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SWV391+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n012.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 08:59:15 AM UTC 2026
% Result : Theorem 98.18s 24.41s
% Output : Refutation 92.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 50
% Syntax : Number of formulae : 615 ( 283 unt; 0 typ; 4 def)
% Number of atoms : 1533 ( 429 equ; 0 cnn)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 6538 ( 519 ~; 403 |; 60 &;5469 @)
% ( 8 <=>; 79 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 8 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 34 ( 31 usr; 9 con; 0-3 aty)
% Number of variables : 1544 ( 0 ^;1530 !; 10 ?;1544 :)
% ( 0 !>; 0 ?*; 0 @-; 4 @+)
% Comments :
%------------------------------------------------------------------------------
thf(check_cpq_decl,type,
check_cpq: $i > $o ).
thf(remove_cpq_decl,type,
remove_cpq: $i > $i > $i ).
thf(triple_decl,type,
triple: $i > $i > $i > $i ).
thf(ok_decl,type,
ok: $i > $o ).
thf(succ_cpq_decl,type,
succ_cpq: $i > $i > $o ).
thf(removemin_cpq_eff_decl,type,
removemin_cpq_eff: $i > $i ).
thf(strictly_less_than_decl,type,
strictly_less_than: $i > $i > $o ).
thf(less_than_decl,type,
less_than: $i > $i > $o ).
thf(isnonempty_slb_decl,type,
isnonempty_slb: $i > $o ).
thf(insert_slb_decl,type,
insert_slb: $i > $i > $i ).
thf(pair_decl,type,
pair: $i > $i > $i ).
thf(contains_slb_decl,type,
contains_slb: $i > $i > $o ).
thf(create_slb_decl,type,
create_slb: $i ).
thf(insert_cpq_decl,type,
insert_cpq: $i > $i > $i ).
thf(remove_slb_decl,type,
remove_slb: $i > $i > $i ).
thf(bottom_decl,type,
bottom: $i ).
thf(update_slb_decl,type,
update_slb: $i > $i > $i ).
thf(pair_in_list_decl,type,
pair_in_list: $i > $i > $i > $o ).
thf(findmin_cpq_eff_decl,type,
findmin_cpq_eff: $i > $i ).
thf(lookup_slb_decl,type,
lookup_slb: $i > $i > $i ).
thf(removemin_cpq_res_decl,type,
removemin_cpq_res: $i > $i ).
thf(findmin_cpq_res_decl,type,
findmin_cpq_res: $i > $i ).
thf(bad_decl,type,
bad: $i ).
thf(remove_pqp_decl,type,
remove_pqp: $i > $i > $i ).
thf(findmin_pqp_res_decl,type,
findmin_pqp_res: $i > $i ).
thf(insert_pqp_decl,type,
insert_pqp: $i > $i > $i ).
thf(contains_cpq_decl,type,
contains_cpq: $i > $i > $o ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ! [B: $i,C: $i] :
( ? [D: $i] :
( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) @ ok )
& ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) @ check_cpq ) )
=> ( C @ ( B @ ( A @ triple ) ) @ check_cpq ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ! [B: $i] :
( ? [C: $i] :
( ( C @ ( B @ ( A @ ( sk1 @ triple ) ) @ remove_cpq ) @ ok )
& ( C @ ( B @ ( A @ ( sk1 @ triple ) ) @ remove_cpq ) @ check_cpq ) )
=> ( B @ ( A @ ( sk1 @ triple ) ) @ check_cpq ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ( ? [B: $i] :
( ( B @ ( A @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ ok )
& ( B @ ( A @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ check_cpq ) )
=> ( A @ ( sk2 @ ( sk1 @ triple ) ) @ check_cpq ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] :
( ( A @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ ok )
& ( A @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ check_cpq ) ) ) ) ).
thf(26,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ ( A @ contains_slb ) )
& ( B != C ) )
=> ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ lookup_slb ) )
= ( C @ ( A @ lookup_slb ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax27) ).
thf(135,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ ( A @ contains_slb ) )
& ( B != C ) )
=> ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ lookup_slb ) )
= ( C @ ( A @ lookup_slb ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(136,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( A @ contains_slb ) )
& ( B != C ) )
=> ! [D: $i] :
( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ lookup_slb ) )
= ( C @ ( A @ lookup_slb ) ) ) ),
inference(miniscope,[status(thm)],[135]) ).
thf(137,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ lookup_slb ) )
= ( C @ ( A @ lookup_slb ) ) )
| ~ ( C @ ( A @ contains_slb ) )
| ( B = C ) ),
inference(cnf,[status(esa)],[136]) ).
thf(138,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ contains_slb ) )
| ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ lookup_slb ) )
= ( C @ ( A @ lookup_slb ) ) )
| ( B = C ) ),
inference(lifteq,[status(thm)],[137]) ).
thf(27,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ~ ( D @ ( B @ contains_slb ) )
=> ( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) )
= ( bad @ ( B @ ( A @ triple ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax43) ).
thf(139,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ~ ( D @ ( B @ contains_slb ) )
=> ( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) )
= ( bad @ ( B @ ( A @ triple ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(140,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) )
= ( bad @ ( B @ ( A @ triple ) ) ) )
| ( D @ ( B @ contains_slb ) ) ),
inference(cnf,[status(esa)],[139]) ).
thf(141,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ contains_slb ) )
| ( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) )
= ( bad @ ( B @ ( A @ triple ) ) ) ) ),
inference(lifteq,[status(thm)],[140]) ).
thf(1,conjecture,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) @ ok )
& ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) @ check_cpq ) )
=> ( C @ ( B @ ( A @ triple ) ) @ check_cpq ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l27_co) ).
thf(2,negated_conjecture,
~ ! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) @ ok )
& ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) @ check_cpq ) )
=> ( C @ ( B @ ( A @ triple ) ) @ check_cpq ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(48,plain,
~ ! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) @ ok )
& ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) @ check_cpq ) )
=> ( C @ ( B @ ( A @ triple ) ) @ check_cpq ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(49,plain,
~ ! [A: $i,B: $i,C: $i] :
( ? [D: $i] :
( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) @ ok )
& ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) @ check_cpq ) )
=> ( C @ ( B @ ( A @ triple ) ) @ check_cpq ) ),
inference(miniscope,[status(thm)],[48]) ).
thf(50,plain,
( ~ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ check_cpq )
& ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ ok )
& ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ check_cpq ) ),
inference(cnf,[status(esa)],[49]) ).
thf(52,plain,
sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ ok,
inference(cnfConj,[status(thm)],[50]) ).
thf(20718,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) )
!= ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) ) )
| ( bad @ ( B @ ( A @ triple ) ) @ ok )
| ( D @ ( B @ contains_slb ) ) ),
inference(paramod_ordered,[status(thm)],[141,52]) ).
thf(20719,plain,
( ( bad @ ( sk2 @ ( sk1 @ triple ) ) @ ok )
| ( sk4 @ ( sk2 @ contains_slb ) ) ),
inference(pattern_uni,[status(thm)],[20718:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk3 )),bind(D,$thf( sk4 ))]]) ).
thf(41,axiom,
! [A: $i,B: $i] :
( ( bad @ ( B @ ( A @ triple ) ) @ ok )
<=> $false ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax40) ).
thf(188,plain,
! [A: $i,B: $i] :
~ ( bad @ ( B @ ( A @ triple ) ) @ ok ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(189,plain,
~ ? [A: $i,B: $i] : ( bad @ ( B @ ( A @ triple ) ) @ ok ),
inference(miniscope,[status(thm)],[188]) ).
thf(190,plain,
! [B: $i,A: $i] :
~ ( bad @ ( B @ ( A @ triple ) ) @ ok ),
inference(cnf,[status(esa)],[189]) ).
thf(22327,plain,
( $false
| ( sk4 @ ( sk2 @ contains_slb ) ) ),
inference(rewrite,[status(thm)],[20719,190]) ).
thf(22328,plain,
sk4 @ ( sk2 @ contains_slb ),
inference(simp,[status(thm)],[22327]) ).
thf(17,axiom,
! [A: $i] : ( A @ ( A @ succ_cpq ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax31) ).
thf(102,plain,
! [A: $i] : ( A @ ( A @ succ_cpq ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(103,plain,
! [A: $i] : ( A @ ( A @ succ_cpq ) ),
inference(cnf,[status(esa)],[102]) ).
thf(18,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ succ_cpq ) )
=> ( B @ findmin_cpq_eff @ ( A @ succ_cpq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax34) ).
thf(104,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ succ_cpq ) )
=> ( B @ findmin_cpq_eff @ ( A @ succ_cpq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(105,plain,
! [B: $i,A: $i] :
( ( B @ findmin_cpq_eff @ ( A @ succ_cpq ) )
| ~ ( B @ ( A @ succ_cpq ) ) ),
inference(cnf,[status(esa)],[104]) ).
thf(6300,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[103,105]) ).
thf(6301,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[6300]) ).
thf(6302,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[6301:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(6370,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6302,105]) ).
thf(6371,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[6370]) ).
thf(6372,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[6371:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ findmin_cpq_eff ))]]) ).
thf(6383,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[6372]) ).
thf(6439,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6383,105]) ).
thf(6440,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[6439]) ).
thf(6441,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[6440:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ findmin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(6460,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[6441]) ).
thf(7154,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6460,105]) ).
thf(7155,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7154]) ).
thf(7156,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7155:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(7188,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7156]) ).
thf(11968,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7188,105]) ).
thf(11969,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[11968]) ).
thf(11970,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[11969:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(11998,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[11970]) ).
thf(12,axiom,
! [A: $i] : ( A @ ( bottom @ less_than ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bottom_smallest) ).
thf(88,plain,
! [A: $i] : ( A @ ( bottom @ less_than ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(16,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ pair_in_list ) ) )
=> ! [D: $i] :
( ( D @ ( A @ contains_slb ) )
=> ( ( B = D )
| ( C @ ( B @ ( D @ ( A @ remove_slb ) @ pair_in_list ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l27_li2829) ).
thf(99,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ pair_in_list ) ) )
=> ! [D: $i] :
( ( D @ ( A @ contains_slb ) )
=> ( ( B = D )
| ( C @ ( B @ ( D @ ( A @ remove_slb ) @ pair_in_list ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(100,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B = D )
| ( C @ ( B @ ( D @ ( A @ remove_slb ) @ pair_in_list ) ) )
| ~ ( D @ ( A @ contains_slb ) )
| ~ ( C @ ( B @ ( A @ pair_in_list ) ) ) ),
inference(cnf,[status(esa)],[99]) ).
thf(101,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( D @ ( A @ remove_slb ) @ pair_in_list ) ) )
| ~ ( D @ ( A @ contains_slb ) )
| ~ ( C @ ( B @ ( A @ pair_in_list ) ) )
| ( B = D ) ),
inference(lifteq,[status(thm)],[100]) ).
thf(3,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ succ_cpq ) )
=> ( B @ removemin_cpq_eff @ ( A @ succ_cpq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax35) ).
thf(54,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ succ_cpq ) )
=> ( B @ removemin_cpq_eff @ ( A @ succ_cpq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(55,plain,
! [B: $i,A: $i] :
( ( B @ removemin_cpq_eff @ ( A @ succ_cpq ) )
| ~ ( B @ ( A @ succ_cpq ) ) ),
inference(cnf,[status(esa)],[54]) ).
thf(221,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[103,55]) ).
thf(222,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[221]) ).
thf(223,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[222:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(230,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[223,55]) ).
thf(231,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[230]) ).
thf(232,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[231:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ removemin_cpq_eff ))]]) ).
thf(233,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[232]) ).
thf(10,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ succ_cpq ) )
=> ( C @ ( B @ insert_cpq ) @ ( A @ succ_cpq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax32) ).
thf(82,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ succ_cpq ) )
=> ( C @ ( B @ insert_cpq ) @ ( A @ succ_cpq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(83,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ succ_cpq ) )
=> ! [C: $i] : ( C @ ( B @ insert_cpq ) @ ( A @ succ_cpq ) ) ),
inference(miniscope,[status(thm)],[82]) ).
thf(84,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ insert_cpq ) @ ( A @ succ_cpq ) )
| ~ ( B @ ( A @ succ_cpq ) ) ),
inference(cnf,[status(esa)],[83]) ).
thf(2095,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( D @ ( C @ insert_cpq ) @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[233,84]) ).
thf(2096,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( D @ ( C @ insert_cpq ) @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[2095]) ).
thf(2097,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ ( B @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[2096:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ removemin_cpq_eff @ removemin_cpq_eff )),bind(D,$thf( D ))]]) ).
thf(2131,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ ( B @ succ_cpq ) ),
inference(simp,[status(thm)],[2097]) ).
thf(35,axiom,
! [A: $i,B: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_res )
= bottom ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax50) ).
thf(170,plain,
! [A: $i,B: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_res )
= bottom ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(40,axiom,
! [A: $i,B: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
= ( bad @ ( create_slb @ ( A @ triple ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax46) ).
thf(185,plain,
! [A: $i,B: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
= ( bad @ ( create_slb @ ( A @ triple ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(186,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
= ( bad @ ( create_slb @ ( A @ triple ) ) ) ),
inference(cnf,[status(esa)],[185]) ).
thf(187,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
= ( bad @ ( create_slb @ ( A @ triple ) ) ) ),
inference(lifteq,[status(thm)],[186]) ).
thf(1100,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( bad @ ( D @ ( C @ triple ) ) ) )
| ~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ ok ) ),
inference(paramod_ordered,[status(thm)],[187,190]) ).
thf(1101,plain,
! [B: $i,A: $i] :
~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ ok ),
inference(pattern_uni,[status(thm)],[1100:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( create_slb ))]]) ).
thf(1195,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ ok ) ),
inference(paramod_ordered,[status(thm)],[187,1101]) ).
thf(1196,plain,
! [B: $i,A: $i] :
~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ ok ),
inference(pattern_uni,[status(thm)],[1195:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(1430,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ) ),
inference(paramod_ordered,[status(thm)],[187,1196]) ).
thf(1431,plain,
! [B: $i,A: $i] :
~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ),
inference(pattern_uni,[status(thm)],[1430:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(1568,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ ok )
!= ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[52,1431]) ).
thf(1569,plain,
! [B: $i,A: $i] :
( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ ok )
!= ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ) ),
inference(simp,[status(thm)],[1568]) ).
thf(1596,plain,
! [B: $i,A: $i] :
( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) )
!= ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff ) ),
inference(simp,[status(thm)],[1569]) ).
thf(240,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[233,55]) ).
thf(241,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[240]) ).
thf(242,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[241:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(243,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[242]) ).
thf(245,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[243,55]) ).
thf(246,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[245]) ).
thf(247,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[246:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(248,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[247]) ).
thf(251,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[248,55]) ).
thf(252,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[251]) ).
thf(253,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[252:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(254,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[253]) ).
thf(273,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[254,55]) ).
thf(274,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[273]) ).
thf(275,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[274:[bind(A,$thf( H )),bind(B,$thf( H )),bind(C,$thf( H @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(276,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[275]) ).
thf(6273,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[233,105]) ).
thf(6274,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[6273]) ).
thf(6275,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[6274:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(6331,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[6275]) ).
thf(6669,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6331,105]) ).
thf(6670,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[6669]) ).
thf(6671,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[6670:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(6695,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[6671]) ).
thf(7615,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6695,105]) ).
thf(7616,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7615]) ).
thf(7617,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7616:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(7641,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7617]) ).
thf(6303,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[223,105]) ).
thf(6304,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[6303]) ).
thf(6305,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[6304:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ removemin_cpq_eff ))]]) ).
thf(6344,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[6305]) ).
thf(6413,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6344,55]) ).
thf(6414,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[6413]) ).
thf(6415,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[6414:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ removemin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(6423,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[6415]) ).
thf(7120,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6423,55]) ).
thf(7121,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7120]) ).
thf(7122,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7121:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(7132,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7122]) ).
thf(33,axiom,
! [A: $i,B: $i] : ( B @ ( create_slb @ ( A @ triple ) ) @ check_cpq ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax36) ).
thf(165,plain,
! [A: $i,B: $i] : ( B @ ( create_slb @ ( A @ triple ) ) @ check_cpq ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(166,plain,
! [B: $i,A: $i] : ( B @ ( create_slb @ ( A @ triple ) ) @ check_cpq ),
inference(cnf,[status(esa)],[165]) ).
thf(1068,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ check_cpq ) ),
inference(paramod_ordered,[status(thm)],[187,166]) ).
thf(1069,plain,
! [B: $i,A: $i] : ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ check_cpq ),
inference(pattern_uni,[status(thm)],[1068:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(1169,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq ) ),
inference(paramod_ordered,[status(thm)],[187,1069]) ).
thf(1170,plain,
! [B: $i,A: $i] : ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq ),
inference(pattern_uni,[status(thm)],[1169:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(1396,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq ) ),
inference(paramod_ordered,[status(thm)],[187,1170]) ).
thf(1397,plain,
! [B: $i,A: $i] : ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq ),
inference(pattern_uni,[status(thm)],[1396:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(53,plain,
~ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ check_cpq ),
inference(cnfConj,[status(thm)],[50]) ).
thf(1526,plain,
! [B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ check_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1397,53]) ).
thf(1527,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ check_cpq ) ),
inference(simp,[status(thm)],[1526]) ).
thf(1556,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ),
inference(simp,[status(thm)],[1527]) ).
thf(2589,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( D @ ( create_slb @ ( C @ triple ) ) @ findmin_cpq_eff ) )
| ( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[187,1556]) ).
thf(2590,plain,
! [A: $i] :
( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ),
inference(pattern_uni,[status(thm)],[2589:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(7173,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6460,55]) ).
thf(7174,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7173]) ).
thf(7175,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7174:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(7182,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7175]) ).
thf(6453,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6383,55]) ).
thf(6454,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[6453]) ).
thf(6455,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[6454:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ findmin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(6466,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[6455]) ).
thf(7209,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6466,105]) ).
thf(7210,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7209]) ).
thf(7211,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7210:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(7235,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7211]) ).
thf(15517,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7235,105]) ).
thf(15518,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[15517]) ).
thf(15519,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[15518:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(15579,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[15519]) ).
thf(6,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) )
<=> ( ( B = C )
| ( C @ ( A @ contains_slb ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax21) ).
thf(65,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( ( B = C )
| ( C @ ( A @ contains_slb ) ) )
=> ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) ) )
& ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) )
=> ( ( B = C )
| ( C @ ( A @ contains_slb ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(66,plain,
( ! [A: $i,B: $i,C: $i] :
( ( ( B = C )
| ( C @ ( A @ contains_slb ) ) )
=> ! [D: $i] : ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) ) )
& ! [A: $i,B: $i,C: $i] :
( ? [D: $i] : ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) )
=> ( ( B = C )
| ( C @ ( A @ contains_slb ) ) ) ) ),
inference(miniscope,[status(thm)],[65]) ).
thf(67,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( G @ ( H @ ( F @ pair ) @ ( E @ insert_slb ) @ contains_slb ) )
| ( F != G ) )
& ( ( G @ ( H @ ( F @ pair ) @ ( E @ insert_slb ) @ contains_slb ) )
| ~ ( G @ ( E @ contains_slb ) ) )
& ( ( B = C )
| ( C @ ( A @ contains_slb ) )
| ~ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) ) ) ),
inference(cnf,[status(esa)],[66]) ).
thf(70,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) )
| ( B != C ) ),
inference(cnfConj,[status(thm)],[67]) ).
thf(73,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) )
| ( B != C ) ),
inference(lifteq,[status(thm)],[70]) ).
thf(74,plain,
! [C: $i,B: $i,A: $i] : ( B @ ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) ),
inference(simp,[status(thm)],[73]) ).
thf(8,axiom,
! [A: $i] :
~ ( A @ ( create_slb @ contains_slb ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax20) ).
thf(77,plain,
! [A: $i] :
~ ( A @ ( create_slb @ contains_slb ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(78,plain,
~ ? [A: $i] : ( A @ ( create_slb @ contains_slb ) ),
inference(miniscope,[status(thm)],[77]) ).
thf(79,plain,
! [A: $i] :
~ ( A @ ( create_slb @ contains_slb ) ),
inference(cnf,[status(esa)],[78]) ).
thf(1515,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) )
!= ( D @ ( create_slb @ contains_slb ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[74,79]) ).
thf(1516,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) )
!= ( D @ ( create_slb @ contains_slb ) ) ),
inference(simp,[status(thm)],[1515]) ).
thf(1517,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B != D )
| ( ( C @ ( B @ pair ) @ ( A @ insert_slb ) )
!= create_slb ) ),
inference(simp,[status(thm)],[1516]) ).
thf(1522,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ pair ) @ ( A @ insert_slb ) )
!= create_slb ),
inference(simp,[status(thm)],[1517]) ).
thf(4,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ strictly_less_than ) )
<=> ( ~ ( A @ ( B @ less_than ) )
& ( B @ ( A @ less_than ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',stricly_smaller_definition) ).
thf(56,plain,
! [A: $i,B: $i] :
( ( ( ~ ( A @ ( B @ less_than ) )
& ( B @ ( A @ less_than ) ) )
=> ( B @ ( A @ strictly_less_than ) ) )
& ( ( B @ ( A @ strictly_less_than ) )
=> ( ~ ( A @ ( B @ less_than ) )
& ( B @ ( A @ less_than ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(1552,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq ) ),
inference(paramod_ordered,[status(thm)],[187,1397]) ).
thf(1553,plain,
! [B: $i,A: $i] : ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq ),
inference(pattern_uni,[status(thm)],[1552:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(1945,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq ) ),
inference(paramod_ordered,[status(thm)],[187,1553]) ).
thf(1946,plain,
! [B: $i,A: $i] : ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq ),
inference(pattern_uni,[status(thm)],[1945:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(2494,plain,
! [B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ check_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1946,53]) ).
thf(2495,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ check_cpq ) ),
inference(simp,[status(thm)],[2494]) ).
thf(2532,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ),
inference(simp,[status(thm)],[2495]) ).
thf(6938,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( D @ ( create_slb @ ( C @ triple ) ) @ findmin_cpq_eff ) )
| ( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[187,2532]) ).
thf(6939,plain,
! [A: $i] :
( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ),
inference(pattern_uni,[status(thm)],[6938:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(2431,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ ( B @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2131,55]) ).
thf(2432,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ ( B @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) ) ),
inference(simp,[status(thm)],[2431]) ).
thf(2433,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ ( B @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[2432:[bind(A,$thf( F )),bind(B,$thf( H )),bind(C,$thf( H )),bind(D,$thf( F @ ( H @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) ))]]) ).
thf(2434,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ ( B @ succ_cpq ) ),
inference(simp,[status(thm)],[2433]) ).
thf(2111,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( D @ ( C @ insert_cpq ) @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[223,84]) ).
thf(2112,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( D @ ( C @ insert_cpq ) @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[2111]) ).
thf(2113,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ insert_cpq ) @ ( B @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[2112:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ removemin_cpq_eff ))]]) ).
thf(2123,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ insert_cpq ) @ ( B @ succ_cpq ) ),
inference(simp,[status(thm)],[2113]) ).
thf(2163,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ removemin_cpq_eff @ insert_cpq ) @ ( B @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2123,55]) ).
thf(2164,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ removemin_cpq_eff @ insert_cpq ) @ ( B @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) ) ),
inference(simp,[status(thm)],[2163]) ).
thf(2165,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ ( B @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[2164:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( G )),bind(D,$thf( F @ ( G @ removemin_cpq_eff @ insert_cpq ) ))]]) ).
thf(2168,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ ( B @ succ_cpq ) ),
inference(simp,[status(thm)],[2165]) ).
thf(31,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ~ ( A @ findmin_pqp_res @ ( B @ contains_slb ) )
& ( B != create_slb ) )
=> ( ( C @ ( B @ ( A @ triple ) ) @ findmin_cpq_eff )
= ( bad @ ( A @ findmin_pqp_res @ ( B @ update_slb ) @ ( A @ triple ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax47) ).
thf(153,plain,
! [A: $i,B: $i,C: $i] :
( ( ~ ( A @ findmin_pqp_res @ ( B @ contains_slb ) )
& ( B != create_slb ) )
=> ( ( C @ ( B @ ( A @ triple ) ) @ findmin_cpq_eff )
= ( bad @ ( A @ findmin_pqp_res @ ( B @ update_slb ) @ ( A @ triple ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(1594,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ) ),
inference(paramod_ordered,[status(thm)],[187,1431]) ).
thf(1595,plain,
! [B: $i,A: $i] :
~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ),
inference(pattern_uni,[status(thm)],[1594:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(1641,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ) ),
inference(paramod_ordered,[status(thm)],[187,1595]) ).
thf(1642,plain,
! [B: $i,A: $i] :
~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ),
inference(pattern_uni,[status(thm)],[1641:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(1963,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ ok )
!= ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[52,1642]) ).
thf(1964,plain,
! [B: $i,A: $i] :
( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ ok )
!= ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ) ),
inference(simp,[status(thm)],[1963]) ).
thf(2001,plain,
! [B: $i,A: $i] :
( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) )
!= ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff ) ),
inference(simp,[status(thm)],[1964]) ).
thf(18594,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( D @ ( create_slb @ ( C @ triple ) ) @ findmin_cpq_eff ) )
| ( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) ) ) ),
inference(paramod_ordered,[status(thm)],[187,2001]) ).
thf(18595,plain,
! [A: $i] :
( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) ) ),
inference(pattern_uni,[status(thm)],[18594:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(28,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( D @ ( B @ lookup_slb ) @ less_than ) )
& ( D @ ( B @ contains_slb ) ) )
=> ( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) )
= ( C @ ( D @ ( B @ remove_slb ) @ ( D @ ( A @ remove_pqp ) @ triple ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax44) ).
thf(142,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( D @ ( B @ lookup_slb ) @ less_than ) )
& ( D @ ( B @ contains_slb ) ) )
=> ( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) )
= ( C @ ( D @ ( B @ remove_slb ) @ ( D @ ( A @ remove_pqp ) @ triple ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(6401,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6344,105]) ).
thf(6402,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[6401]) ).
thf(6403,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[6402:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ removemin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(6418,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[6403]) ).
thf(7069,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6418,55]) ).
thf(7070,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7069]) ).
thf(7071,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7070:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(7088,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7071]) ).
thf(11406,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7088,55]) ).
thf(11407,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[11406]) ).
thf(11408,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[11407:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(11417,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[11408]) ).
thf(237,plain,
! [B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ check_cpq )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ check_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[166,53]) ).
thf(238,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ check_cpq )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ check_cpq ) ),
inference(simp,[status(thm)],[237]) ).
thf(239,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ),
inference(simp,[status(thm)],[238]) ).
thf(1102,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[187,239]) ).
thf(1103,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ),
inference(pattern_uni,[status(thm)],[1102:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(1279,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[187,1103]) ).
thf(1280,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ),
inference(pattern_uni,[status(thm)],[1279:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(1760,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( D @ ( create_slb @ ( C @ triple ) ) @ findmin_cpq_eff ) )
| ( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[187,1280]) ).
thf(1761,plain,
! [A: $i] :
( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ),
inference(pattern_uni,[status(thm)],[1760:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(34,axiom,
! [A: $i] :
( ( A @ removemin_cpq_eff )
= ( A @ findmin_cpq_res @ ( A @ findmin_cpq_eff @ remove_cpq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax52) ).
thf(167,plain,
! [A: $i] :
( ( A @ removemin_cpq_eff )
= ( A @ findmin_cpq_res @ ( A @ findmin_cpq_eff @ remove_cpq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(168,plain,
! [A: $i] :
( ( A @ removemin_cpq_eff )
= ( A @ findmin_cpq_res @ ( A @ findmin_cpq_eff @ remove_cpq ) ) ),
inference(cnf,[status(esa)],[167]) ).
thf(169,plain,
! [A: $i] :
( ( A @ findmin_cpq_res @ ( A @ findmin_cpq_eff @ remove_cpq ) )
= ( A @ removemin_cpq_eff ) ),
inference(lifteq,[status(thm)],[168]) ).
thf(25,axiom,
! [A: $i] :
( ( A @ removemin_cpq_res )
= ( A @ findmin_cpq_res ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax53) ).
thf(132,plain,
! [A: $i] :
( ( A @ removemin_cpq_res )
= ( A @ findmin_cpq_res ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(133,plain,
! [A: $i] :
( ( A @ removemin_cpq_res )
= ( A @ findmin_cpq_res ) ),
inference(cnf,[status(esa)],[132]) ).
thf(134,plain,
! [A: $i] :
( ( A @ findmin_cpq_res )
= ( A @ removemin_cpq_res ) ),
inference(lifteq,[status(thm)],[133]) ).
thf(281,plain,
! [A: $i] :
( ( A @ removemin_cpq_res @ ( A @ findmin_cpq_eff @ remove_cpq ) )
= ( A @ removemin_cpq_eff ) ),
inference(rewrite,[status(thm)],[169,134]) ).
thf(51,plain,
sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ check_cpq,
inference(cnfConj,[status(thm)],[50]) ).
thf(211,plain,
( ( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ check_cpq )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ check_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[51,53]) ).
thf(212,plain,
( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ check_cpq )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ check_cpq ) ),
inference(simp,[status(thm)],[211]) ).
thf(213,plain,
( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ),
inference(simp,[status(thm)],[212]) ).
thf(286,plain,
! [A: $i] :
( ( ( A @ removemin_cpq_res @ ( A @ findmin_cpq_eff @ remove_cpq ) )
!= ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) ) )
| ( ( A @ removemin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[281,213]) ).
thf(288,plain,
! [A: $i] :
( ( ( A @ removemin_cpq_res )
!= sk4 )
| ( ( A @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) )
| ( ( A @ removemin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ) ),
inference(simp,[status(thm)],[286]) ).
thf(1610,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ ok )
!= ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[52,1595]) ).
thf(1611,plain,
! [B: $i,A: $i] :
( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ ok )
!= ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ) ),
inference(simp,[status(thm)],[1610]) ).
thf(1645,plain,
! [B: $i,A: $i] :
( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) )
!= ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff ) ),
inference(simp,[status(thm)],[1611]) ).
thf(2108,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( D @ ( C @ insert_cpq ) @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[103,84]) ).
thf(2109,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( D @ ( C @ insert_cpq ) @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[2108]) ).
thf(2110,plain,
! [B: $i,A: $i] : ( B @ ( A @ insert_cpq ) @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[2109:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(2136,plain,
! [B: $i,A: $i] : ( B @ ( A @ insert_cpq ) @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[2110]) ).
thf(5,axiom,
! [A: $i,B: $i,C: $i] : ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ isnonempty_slb ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax19) ).
thf(63,plain,
! [A: $i,B: $i,C: $i] : ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ isnonempty_slb ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(64,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ isnonempty_slb ),
inference(cnf,[status(esa)],[63]) ).
thf(15,axiom,
~ ( create_slb @ isnonempty_slb ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax18) ).
thf(97,plain,
~ ( create_slb @ isnonempty_slb ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(98,plain,
~ ( create_slb @ isnonempty_slb ),
inference(polarity_switch,[status(thm)],[97]) ).
thf(255,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ isnonempty_slb )
!= ( create_slb @ isnonempty_slb ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[64,98]) ).
thf(256,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ isnonempty_slb )
!= ( create_slb @ isnonempty_slb ) ),
inference(simp,[status(thm)],[255]) ).
thf(257,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ pair ) @ ( A @ insert_slb ) )
!= create_slb ),
inference(simp,[status(thm)],[256]) ).
thf(2530,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq ) ),
inference(paramod_ordered,[status(thm)],[187,1946]) ).
thf(2531,plain,
! [B: $i,A: $i] : ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq ),
inference(pattern_uni,[status(thm)],[2530:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(6270,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[243,105]) ).
thf(6271,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[6270]) ).
thf(6272,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[6271:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(6330,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[6272]) ).
thf(7573,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6330,55]) ).
thf(7574,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7573]) ).
thf(7575,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7574:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(7592,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7575]) ).
thf(3178,plain,
! [B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ check_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2531,53]) ).
thf(3179,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ check_cpq ) ),
inference(simp,[status(thm)],[3178]) ).
thf(3221,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ),
inference(simp,[status(thm)],[3179]) ).
thf(22,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( E @ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ pair_in_list ) ) )
<=> ( ( ( D = E )
& ( B = C ) )
| ( E @ ( C @ ( A @ pair_in_list ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax23) ).
thf(114,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( ( ( D = E )
& ( B = C ) )
| ( E @ ( C @ ( A @ pair_in_list ) ) ) )
=> ( E @ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ pair_in_list ) ) ) )
& ( ( E @ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ pair_in_list ) ) )
=> ( ( ( D = E )
& ( B = C ) )
| ( E @ ( C @ ( A @ pair_in_list ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(115,plain,
( ! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( ( D = E )
& ( B = C ) )
| ( E @ ( C @ ( A @ pair_in_list ) ) ) )
=> ( E @ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ pair_in_list ) ) ) )
& ! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( E @ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ pair_in_list ) ) )
=> ( ( ( D = E )
& ( B = C ) )
| ( E @ ( C @ ( A @ pair_in_list ) ) ) ) ) ),
inference(miniscope,[status(thm)],[114]) ).
thf(116,plain,
! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( J @ ( H @ ( I @ ( G @ pair ) @ ( F @ insert_slb ) @ pair_in_list ) ) )
| ( I != J )
| ( G != H ) )
& ( ( J @ ( H @ ( I @ ( G @ pair ) @ ( F @ insert_slb ) @ pair_in_list ) ) )
| ~ ( J @ ( H @ ( F @ pair_in_list ) ) ) )
& ( ( D = E )
| ( E @ ( C @ ( A @ pair_in_list ) ) )
| ~ ( E @ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ pair_in_list ) ) ) )
& ( ( B = C )
| ( E @ ( C @ ( A @ pair_in_list ) ) )
| ~ ( E @ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ pair_in_list ) ) ) ) ),
inference(cnf,[status(esa)],[115]) ).
thf(120,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ pair_in_list ) ) )
| ( D != E )
| ( B != C ) ),
inference(cnfConj,[status(thm)],[116]) ).
thf(124,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ pair_in_list ) ) )
| ( D != E )
| ( B != C ) ),
inference(lifteq,[status(thm)],[120]) ).
thf(125,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ pair_in_list ) ) ),
inference(simp,[status(thm)],[124]) ).
thf(2145,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ insert_cpq ) @ ( A @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2136,55]) ).
thf(2146,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ insert_cpq ) @ ( A @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) ) ),
inference(simp,[status(thm)],[2145]) ).
thf(2147,plain,
! [B: $i,A: $i] : ( B @ ( A @ insert_cpq ) @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[2146:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ insert_cpq ) ))]]) ).
thf(2149,plain,
! [B: $i,A: $i] : ( B @ ( A @ insert_cpq ) @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[2147]) ).
thf(2183,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ insert_cpq ) @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2149,55]) ).
thf(2184,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ insert_cpq ) @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) ) ),
inference(simp,[status(thm)],[2183]) ).
thf(2185,plain,
! [B: $i,A: $i] : ( B @ ( A @ insert_cpq ) @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[2184:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( F )),bind(D,$thf( G @ ( F @ insert_cpq ) @ removemin_cpq_eff ))]]) ).
thf(2190,plain,
! [B: $i,A: $i] : ( B @ ( A @ insert_cpq ) @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[2185]) ).
thf(2483,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ insert_cpq ) @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2190,55]) ).
thf(2484,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ insert_cpq ) @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) ) ),
inference(simp,[status(thm)],[2483]) ).
thf(2485,plain,
! [B: $i,A: $i] : ( B @ ( A @ insert_cpq ) @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[2484:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( G )),bind(D,$thf( H @ ( G @ insert_cpq ) @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(2488,plain,
! [B: $i,A: $i] : ( B @ ( A @ insert_cpq ) @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[2485]) ).
thf(6276,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[248,105]) ).
thf(6277,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[6276]) ).
thf(6278,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[6277:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(6332,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[6278]) ).
thf(32,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ triple ) ) @ check_cpq )
<=> ! [D: $i,E: $i] :
( ( E @ ( D @ ( B @ pair_in_list ) ) )
=> ( D @ ( E @ less_than ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l27_li4142) ).
thf(157,plain,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i,E: $i] :
( ( E @ ( D @ ( B @ pair_in_list ) ) )
=> ( D @ ( E @ less_than ) ) )
=> ( C @ ( B @ ( A @ triple ) ) @ check_cpq ) )
& ( ( C @ ( B @ ( A @ triple ) ) @ check_cpq )
=> ! [D: $i,E: $i] :
( ( E @ ( D @ ( B @ pair_in_list ) ) )
=> ( D @ ( E @ less_than ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(7104,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6423,105]) ).
thf(7105,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7104]) ).
thf(7106,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7105:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(7124,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7106]) ).
thf(171,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_res )
= bottom ),
inference(cnf,[status(esa)],[170]) ).
thf(172,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_res )
= bottom ),
inference(lifteq,[status(thm)],[171]) ).
thf(244,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ removemin_cpq_res )
= bottom ),
inference(rewrite,[status(thm)],[172,134]) ).
thf(1066,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ removemin_cpq_res )
= bottom ) ),
inference(paramod_ordered,[status(thm)],[187,244]) ).
thf(1067,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ removemin_cpq_res )
= bottom ),
inference(pattern_uni,[status(thm)],[1066:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(1235,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_res )
= bottom ) ),
inference(paramod_ordered,[status(thm)],[187,1067]) ).
thf(1236,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_res )
= bottom ),
inference(pattern_uni,[status(thm)],[1235:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(1482,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_res )
= bottom ) ),
inference(paramod_ordered,[status(thm)],[187,1236]) ).
thf(1483,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_res )
= bottom ),
inference(pattern_uni,[status(thm)],[1482:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(1703,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_res )
= bottom ) ),
inference(paramod_ordered,[status(thm)],[187,1483]) ).
thf(1704,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_res )
= bottom ),
inference(pattern_uni,[status(thm)],[1703:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(14,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ ( A @ contains_slb ) )
& ( B != C ) )
=> ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ remove_slb ) )
= ( D @ ( B @ pair ) @ ( C @ ( A @ remove_slb ) @ insert_slb ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax25) ).
thf(93,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ ( A @ contains_slb ) )
& ( B != C ) )
=> ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ remove_slb ) )
= ( D @ ( B @ pair ) @ ( C @ ( A @ remove_slb ) @ insert_slb ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(1409,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ ok )
!= ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ ok ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[52,1196]) ).
thf(1410,plain,
! [B: $i,A: $i] :
( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ ok )
!= ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ ok ) ),
inference(simp,[status(thm)],[1409]) ).
thf(1433,plain,
! [B: $i,A: $i] :
( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) )
!= ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff ) ),
inference(simp,[status(thm)],[1410]) ).
thf(3013,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( D @ ( create_slb @ ( C @ triple ) ) @ findmin_cpq_eff ) )
| ( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) ) ) ),
inference(paramod_ordered,[status(thm)],[187,1433]) ).
thf(3014,plain,
! [A: $i] :
( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) ) ),
inference(pattern_uni,[status(thm)],[3013:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(282,plain,
! [A: $i] :
( ( ( A @ removemin_cpq_res @ ( A @ findmin_cpq_eff @ remove_cpq ) )
!= ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) ) )
| ( A @ removemin_cpq_eff @ ok ) ),
inference(paramod_ordered,[status(thm)],[281,52]) ).
thf(289,plain,
! [A: $i] :
( ( ( A @ removemin_cpq_res )
!= sk4 )
| ( ( A @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) )
| ( A @ removemin_cpq_eff @ ok ) ),
inference(simp,[status(thm)],[282]) ).
thf(214,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ ok )
!= ( bad @ ( B @ ( A @ triple ) ) @ ok ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[52,190]) ).
thf(215,plain,
! [B: $i,A: $i] :
( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) @ ok )
!= ( bad @ ( B @ ( A @ triple ) ) @ ok ) ),
inference(simp,[status(thm)],[214]) ).
thf(216,plain,
! [B: $i,A: $i] :
( ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) )
!= ( bad @ ( B @ ( A @ triple ) ) ) ),
inference(simp,[status(thm)],[215]) ).
thf(8028,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( D @ ( create_slb @ ( C @ triple ) ) @ findmin_cpq_eff ) )
| ( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) ) ) ),
inference(paramod_ordered,[status(thm)],[187,1645]) ).
thf(8029,plain,
! [A: $i] :
( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) ) ),
inference(pattern_uni,[status(thm)],[8028:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(7227,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6466,55]) ).
thf(7228,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7227]) ).
thf(7229,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7228:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(7245,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7229]) ).
thf(19,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ lookup_slb ) )
= C ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax26) ).
thf(106,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ lookup_slb ) )
= C ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(6379,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6302,55]) ).
thf(6380,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[6379]) ).
thf(6381,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[6380:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ findmin_cpq_eff ))]]) ).
thf(6388,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[6381]) ).
thf(6493,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6388,55]) ).
thf(6494,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[6493]) ).
thf(6495,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[6494:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ findmin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(6507,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[6495]) ).
thf(7515,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6507,55]) ).
thf(7516,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7515]) ).
thf(7517,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7516:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(7532,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7517]) ).
thf(117,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B = C )
| ( E @ ( C @ ( A @ pair_in_list ) ) )
| ~ ( E @ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ pair_in_list ) ) ) ),
inference(cnfConj,[status(thm)],[116]) ).
thf(121,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ ( A @ pair_in_list ) ) )
| ~ ( E @ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ pair_in_list ) ) )
| ( B = C ) ),
inference(lifteq,[status(thm)],[117]) ).
thf(277,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[276,55]) ).
thf(278,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[277]) ).
thf(279,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[278:[bind(A,$thf( I )),bind(B,$thf( I )),bind(C,$thf( I @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(280,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[279]) ).
thf(89,plain,
! [A: $i] : ( A @ ( bottom @ less_than ) ),
inference(cnf,[status(esa)],[88]) ).
thf(46,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( B @ lookup_slb ) @ ( D @ strictly_less_than ) )
& ( D @ ( B @ contains_slb ) ) )
=> ( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) )
= ( bad @ ( D @ ( B @ remove_slb ) @ ( D @ ( A @ remove_pqp ) @ triple ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax45) ).
thf(206,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( B @ lookup_slb ) @ ( D @ strictly_less_than ) )
& ( D @ ( B @ contains_slb ) ) )
=> ( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) )
= ( bad @ ( D @ ( B @ remove_slb ) @ ( D @ ( A @ remove_pqp ) @ triple ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(11992,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7188,55]) ).
thf(11993,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[11992]) ).
thf(11994,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[11993:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(12008,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[11994]) ).
thf(57,plain,
( ! [A: $i,B: $i] :
( ( ~ ( A @ ( B @ less_than ) )
& ( B @ ( A @ less_than ) ) )
=> ( B @ ( A @ strictly_less_than ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ strictly_less_than ) )
=> ( ~ ( A @ ( B @ less_than ) )
& ( B @ ( A @ less_than ) ) ) ) ),
inference(miniscope,[status(thm)],[56]) ).
thf(58,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ strictly_less_than ) )
| ( C @ ( D @ less_than ) )
| ~ ( D @ ( C @ less_than ) ) )
& ( ~ ( A @ ( B @ less_than ) )
| ~ ( B @ ( A @ strictly_less_than ) ) )
& ( ( B @ ( A @ less_than ) )
| ~ ( B @ ( A @ strictly_less_than ) ) ) ),
inference(cnf,[status(esa)],[57]) ).
thf(60,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ less_than ) )
| ~ ( B @ ( A @ strictly_less_than ) ) ),
inference(cnfConj,[status(thm)],[58]) ).
thf(15632,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7245,105]) ).
thf(15633,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[15632]) ).
thf(15634,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[15633:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(15682,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[15634]) ).
thf(1999,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ) ),
inference(paramod_ordered,[status(thm)],[187,1642]) ).
thf(2000,plain,
! [B: $i,A: $i] :
~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ),
inference(pattern_uni,[status(thm)],[1999:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(1056,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( bad @ ( D @ ( C @ triple ) ) ) )
| ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) ) ) ),
inference(paramod_ordered,[status(thm)],[187,216]) ).
thf(1057,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) ) ),
inference(pattern_uni,[status(thm)],[1056:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( create_slb ))]]) ).
thf(2855,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ) ),
inference(paramod_ordered,[status(thm)],[187,2000]) ).
thf(2856,plain,
! [B: $i,A: $i] :
~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ),
inference(pattern_uni,[status(thm)],[2855:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(6072,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ) ),
inference(paramod_ordered,[status(thm)],[187,2856]) ).
thf(6073,plain,
! [B: $i,A: $i] :
~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ),
inference(pattern_uni,[status(thm)],[6072:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(7813,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ) ),
inference(paramod_ordered,[status(thm)],[187,6073]) ).
thf(7814,plain,
! [B: $i,A: $i] :
~ ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ok ),
inference(pattern_uni,[status(thm)],[7813:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(11,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ remove_slb ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax24) ).
thf(85,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ remove_slb ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(6685,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6331,55]) ).
thf(6686,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[6685]) ).
thf(6687,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[6686:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(6703,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[6687]) ).
thf(7679,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6703,105]) ).
thf(7680,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7679]) ).
thf(7681,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7680:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(7703,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7681]) ).
thf(15654,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7245,55]) ).
thf(15655,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[15654]) ).
thf(15656,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[15655:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(15692,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[15656]) ).
thf(2098,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( D @ ( C @ insert_cpq ) @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[248,84]) ).
thf(2099,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( D @ ( C @ insert_cpq ) @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[2098]) ).
thf(2100,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ ( B @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[2099:[bind(A,$thf( H )),bind(B,$thf( H )),bind(C,$thf( H @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff )),bind(D,$thf( D ))]]) ).
thf(2132,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ ( B @ succ_cpq ) ),
inference(simp,[status(thm)],[2100]) ).
thf(1914,plain,
! [B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ check_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1553,53]) ).
thf(1915,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ check_cpq )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ check_cpq ) ),
inference(simp,[status(thm)],[1914]) ).
thf(1947,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ),
inference(simp,[status(thm)],[1915]) ).
thf(3285,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( D @ ( create_slb @ ( C @ triple ) ) @ findmin_cpq_eff ) )
| ( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[187,1947]) ).
thf(3286,plain,
! [A: $i] :
( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ),
inference(pattern_uni,[status(thm)],[3285:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(13,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( C @ ( D @ strictly_less_than ) )
=> ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ update_slb ) )
= ( C @ ( B @ pair ) @ ( C @ ( A @ update_slb ) @ insert_slb ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax29) ).
thf(90,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( C @ ( D @ strictly_less_than ) )
=> ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ update_slb ) )
= ( C @ ( B @ pair ) @ ( C @ ( A @ update_slb ) @ insert_slb ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(91,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ update_slb ) )
= ( C @ ( B @ pair ) @ ( C @ ( A @ update_slb ) @ insert_slb ) ) )
| ~ ( C @ ( D @ strictly_less_than ) ) ),
inference(cnf,[status(esa)],[90]) ).
thf(92,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( D @ strictly_less_than ) )
| ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ update_slb ) )
= ( C @ ( B @ pair ) @ ( C @ ( A @ update_slb ) @ insert_slb ) ) ) ),
inference(lifteq,[status(thm)],[91]) ).
thf(7,axiom,
! [A: $i] : ( A @ ( A @ less_than ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
thf(75,plain,
! [A: $i] : ( A @ ( A @ less_than ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(76,plain,
! [A: $i] : ( A @ ( A @ less_than ) ),
inference(cnf,[status(esa)],[75]) ).
thf(227,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ less_than ) )
!= ( B @ ( C @ less_than ) ) )
| ~ $true
| ~ ( C @ ( B @ strictly_less_than ) ) ),
inference(paramod_ordered,[status(thm)],[76,60]) ).
thf(228,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ less_than ) )
!= ( B @ ( C @ less_than ) ) )
| ~ ( C @ ( B @ strictly_less_than ) ) ),
inference(simp,[status(thm)],[227]) ).
thf(229,plain,
! [A: $i] :
~ ( A @ ( A @ strictly_less_than ) ),
inference(pattern_uni,[status(thm)],[228:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(44,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ triple ) ) @ contains_cpq ) )
<=> ( D @ ( B @ contains_slb ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax39) ).
thf(197,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( B @ contains_slb ) )
=> ( D @ ( C @ ( B @ ( A @ triple ) ) @ contains_cpq ) ) )
& ( ( D @ ( C @ ( B @ ( A @ triple ) ) @ contains_cpq ) )
=> ( D @ ( B @ contains_slb ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(11561,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7132,105]) ).
thf(11562,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[11561]) ).
thf(11563,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[11562:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(11602,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[11563]) ).
thf(16086,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( D @ ( create_slb @ ( C @ triple ) ) @ findmin_cpq_eff ) )
| ( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[187,3221]) ).
thf(16087,plain,
! [A: $i] :
( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ),
inference(pattern_uni,[status(thm)],[16086:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(11385,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7088,105]) ).
thf(11386,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[11385]) ).
thf(11387,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[11386:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(11435,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[11387]) ).
thf(20,axiom,
! [A: $i,B: $i] :
~ ( B @ ( A @ ( create_slb @ pair_in_list ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax22) ).
thf(109,plain,
! [A: $i,B: $i] :
~ ( B @ ( A @ ( create_slb @ pair_in_list ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(43,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( A @ findmin_pqp_res @ ( B @ lookup_slb ) @ ( A @ findmin_pqp_res @ strictly_less_than ) )
& ( A @ findmin_pqp_res @ ( B @ contains_slb ) )
& ( B != create_slb ) )
=> ( ( C @ ( B @ ( A @ triple ) ) @ findmin_cpq_eff )
= ( bad @ ( A @ findmin_pqp_res @ ( B @ update_slb ) @ ( A @ triple ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax48) ).
thf(193,plain,
! [A: $i,B: $i,C: $i] :
( ( ( A @ findmin_pqp_res @ ( B @ lookup_slb ) @ ( A @ findmin_pqp_res @ strictly_less_than ) )
& ( A @ findmin_pqp_res @ ( B @ contains_slb ) )
& ( B != create_slb ) )
=> ( ( C @ ( B @ ( A @ triple ) ) @ findmin_cpq_eff )
= ( bad @ ( A @ findmin_pqp_res @ ( B @ update_slb ) @ ( A @ triple ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(6480,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6388,105]) ).
thf(6481,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[6480]) ).
thf(6482,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[6481:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ findmin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(6501,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[6482]) ).
thf(7498,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6507,105]) ).
thf(7499,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7498]) ).
thf(7500,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7499:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(7523,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7500]) ).
thf(7414,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6501,105]) ).
thf(7415,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7414]) ).
thf(7416,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7415:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(7448,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7416]) ).
thf(94,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( A @ contains_slb ) )
& ( B != C ) )
=> ! [D: $i] :
( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ remove_slb ) )
= ( D @ ( B @ pair ) @ ( C @ ( A @ remove_slb ) @ insert_slb ) ) ) ),
inference(miniscope,[status(thm)],[93]) ).
thf(95,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ remove_slb ) )
= ( D @ ( B @ pair ) @ ( C @ ( A @ remove_slb ) @ insert_slb ) ) )
| ~ ( C @ ( A @ contains_slb ) )
| ( B = C ) ),
inference(cnf,[status(esa)],[94]) ).
thf(96,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ contains_slb ) )
| ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ remove_slb ) )
= ( D @ ( B @ pair ) @ ( C @ ( A @ remove_slb ) @ insert_slb ) ) )
| ( B = C ) ),
inference(lifteq,[status(thm)],[95]) ).
thf(7699,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6703,55]) ).
thf(7700,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7699]) ).
thf(7701,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7700:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(7717,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7701]) ).
thf(69,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) )
| ~ ( C @ ( A @ contains_slb ) ) ),
inference(cnfConj,[status(thm)],[67]) ).
thf(72,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) )
| ~ ( C @ ( A @ contains_slb ) ) ),
inference(simp,[status(thm)],[69]) ).
thf(22366,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( sk2 @ contains_slb ) )
!= ( C @ ( A @ contains_slb ) ) )
| ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22328,72]) ).
thf(22367,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( sk2 @ contains_slb ) )
!= ( C @ ( A @ contains_slb ) ) )
| ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) ) ),
inference(simp,[status(thm)],[22366]) ).
thf(22368,plain,
! [B: $i,A: $i] : ( sk4 @ ( B @ ( A @ pair ) @ ( sk2 @ insert_slb ) @ contains_slb ) ),
inference(pattern_uni,[status(thm)],[22367:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( sk4 ))]]) ).
thf(22396,plain,
! [B: $i,A: $i] : ( sk4 @ ( B @ ( A @ pair ) @ ( sk2 @ insert_slb ) @ contains_slb ) ),
inference(simp,[status(thm)],[22368]) ).
thf(22471,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( B @ ( A @ pair ) @ ( sk2 @ insert_slb ) @ contains_slb ) )
!= ( C @ ( create_slb @ contains_slb ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22396,79]) ).
thf(22472,plain,
! [C: $i,B: $i,A: $i] :
( ( sk4 @ ( B @ ( A @ pair ) @ ( sk2 @ insert_slb ) @ contains_slb ) )
!= ( C @ ( create_slb @ contains_slb ) ) ),
inference(simp,[status(thm)],[22471]) ).
thf(22490,plain,
! [C: $i,B: $i,A: $i] :
( ( sk4 != C )
| ( ( B @ ( A @ pair ) @ ( sk2 @ insert_slb ) )
!= create_slb ) ),
inference(simp,[status(thm)],[22472]) ).
thf(22511,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pair ) @ ( sk2 @ insert_slb ) )
!= create_slb ),
inference(simp,[status(thm)],[22490]) ).
thf(2457,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ ( B @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2168,55]) ).
thf(2458,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ ( B @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) ) ),
inference(simp,[status(thm)],[2457]) ).
thf(2459,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ removemin_cpq_eff @ ( B @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[2458:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( H )),bind(D,$thf( G @ ( H @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff ))]]) ).
thf(2465,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ removemin_cpq_eff @ ( B @ succ_cpq ) ),
inference(simp,[status(thm)],[2459]) ).
thf(36,axiom,
! [A: $i,B: $i,C: $i] :
( ~ ( C @ ( B @ ( A @ triple ) ) @ ok )
=> ( C = bad ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax41) ).
thf(173,plain,
! [A: $i,B: $i,C: $i] :
( ~ ( C @ ( B @ ( A @ triple ) ) @ ok )
=> ( C = bad ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(24,axiom,
! [A: $i] :
( ( A @ ( create_slb @ update_slb ) )
= create_slb ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax28) ).
thf(129,plain,
! [A: $i] :
( ( A @ ( create_slb @ update_slb ) )
= create_slb ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(23,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ less_than ) )
=> ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ update_slb ) )
= ( D @ ( B @ pair ) @ ( C @ ( A @ update_slb ) @ insert_slb ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax30) ).
thf(126,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ less_than ) )
=> ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ update_slb ) )
= ( D @ ( B @ pair ) @ ( C @ ( A @ update_slb ) @ insert_slb ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(127,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ update_slb ) )
= ( D @ ( B @ pair ) @ ( C @ ( A @ update_slb ) @ insert_slb ) ) )
| ~ ( D @ ( C @ less_than ) ) ),
inference(cnf,[status(esa)],[126]) ).
thf(128,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( C @ less_than ) )
| ( ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ update_slb ) )
= ( D @ ( B @ pair ) @ ( C @ ( A @ update_slb ) @ insert_slb ) ) ) ),
inference(lifteq,[status(thm)],[127]) ).
thf(2367,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_res )
= bottom ) ),
inference(paramod_ordered,[status(thm)],[187,1704]) ).
thf(2368,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_res )
= bottom ),
inference(pattern_uni,[status(thm)],[2367:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(11494,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7124,55]) ).
thf(11495,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[11494]) ).
thf(11496,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[11495:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(11516,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[11496]) ).
thf(1277,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( D @ ( create_slb @ ( C @ triple ) ) @ findmin_cpq_eff ) )
| ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[187,1103]) ).
thf(1278,plain,
! [A: $i] :
( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ),
inference(pattern_uni,[status(thm)],[1277:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(30,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( D @ ( E @ less_than ) )
=> ( ( C @ ( E @ ( D @ pair ) @ ( B @ insert_slb ) @ ( A @ triple ) ) @ check_cpq )
<=> ( C @ ( B @ ( A @ triple ) ) @ check_cpq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax37) ).
thf(149,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( D @ ( E @ less_than ) )
=> ( ( ( C @ ( B @ ( A @ triple ) ) @ check_cpq )
=> ( C @ ( E @ ( D @ pair ) @ ( B @ insert_slb ) @ ( A @ triple ) ) @ check_cpq ) )
& ( ( C @ ( E @ ( D @ pair ) @ ( B @ insert_slb ) @ ( A @ triple ) ) @ check_cpq )
=> ( C @ ( B @ ( A @ triple ) ) @ check_cpq ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(38,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ triple ) ) @ insert_cpq ) )
= ( C @ ( bottom @ ( D @ pair ) @ ( B @ insert_slb ) @ ( D @ ( A @ insert_pqp ) @ triple ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax42) ).
thf(180,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ triple ) ) @ insert_cpq ) )
= ( C @ ( bottom @ ( D @ pair ) @ ( B @ insert_slb ) @ ( D @ ( A @ insert_pqp ) @ triple ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(293,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[280,55]) ).
thf(294,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[293]) ).
thf(295,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[294:[bind(A,$thf( J )),bind(B,$thf( J )),bind(C,$thf( J @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(296,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[295]) ).
thf(37,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( A @ findmin_pqp_res @ ( A @ findmin_pqp_res @ ( B @ lookup_slb ) @ less_than ) )
& ( A @ findmin_pqp_res @ ( B @ contains_slb ) )
& ( B != create_slb ) )
=> ( ( C @ ( B @ ( A @ triple ) ) @ findmin_cpq_eff )
= ( C @ ( A @ findmin_pqp_res @ ( B @ update_slb ) @ ( A @ triple ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax49) ).
thf(176,plain,
! [A: $i,B: $i,C: $i] :
( ( ( A @ findmin_pqp_res @ ( A @ findmin_pqp_res @ ( B @ lookup_slb ) @ less_than ) )
& ( A @ findmin_pqp_res @ ( B @ contains_slb ) )
& ( B != create_slb ) )
=> ( ( C @ ( B @ ( A @ triple ) ) @ findmin_cpq_eff )
= ( C @ ( A @ findmin_pqp_res @ ( B @ update_slb ) @ ( A @ triple ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(42,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) @ ok )
& ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) @ check_cpq ) )
=> ! [E: $i] :
( ( E @ ( D @ ( B @ pair_in_list ) ) )
=> ( D @ ( E @ less_than ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l27_l30) ).
thf(191,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) @ ok )
& ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) @ check_cpq ) )
=> ! [E: $i] :
( ( E @ ( D @ ( B @ pair_in_list ) ) )
=> ( D @ ( E @ less_than ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(16089,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( D @ ( create_slb @ ( C @ triple ) ) ) )
| ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[187,3221]) ).
thf(16090,plain,
! [B: $i,A: $i] :
( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ),
inference(pattern_uni,[status(thm)],[16089:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( bad ))]]) ).
thf(21804,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( D @ ( create_slb @ ( C @ triple ) ) @ findmin_cpq_eff ) )
| ( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[187,16090]) ).
thf(21805,plain,
! [A: $i] :
( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) ),
inference(pattern_uni,[status(thm)],[21804:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(59,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ less_than ) )
| ~ ( B @ ( A @ strictly_less_than ) ) ),
inference(cnfConj,[status(thm)],[58]) ).
thf(68,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B = C )
| ( C @ ( A @ contains_slb ) )
| ~ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) ) ),
inference(cnfConj,[status(thm)],[67]) ).
thf(71,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( A @ contains_slb ) )
| ~ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) )
| ( B = C ) ),
inference(lifteq,[status(thm)],[68]) ).
thf(143,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) )
= ( C @ ( D @ ( B @ remove_slb ) @ ( D @ ( A @ remove_pqp ) @ triple ) ) ) )
| ~ ( D @ ( D @ ( B @ lookup_slb ) @ less_than ) )
| ~ ( D @ ( B @ contains_slb ) ) ),
inference(cnf,[status(esa)],[142]) ).
thf(144,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( D @ ( B @ lookup_slb ) @ less_than ) )
| ~ ( D @ ( B @ contains_slb ) )
| ( ( C @ ( D @ ( B @ remove_slb ) @ ( D @ ( A @ remove_pqp ) @ triple ) ) )
= ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) ) ) ),
inference(lifteq,[status(thm)],[143]) ).
thf(234,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ less_than ) )
!= ( C @ ( D @ less_than ) ) )
| ~ $true
| ~ ( D @ ( C @ strictly_less_than ) )
| ~ ( B @ ( A @ strictly_less_than ) ) ),
inference(paramod_ordered,[status(thm)],[59,60]) ).
thf(235,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ less_than ) )
!= ( C @ ( D @ less_than ) ) )
| ~ ( D @ ( C @ strictly_less_than ) )
| ~ ( B @ ( A @ strictly_less_than ) ) ),
inference(simp,[status(thm)],[234]) ).
thf(236,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ strictly_less_than ) )
| ~ ( B @ ( A @ strictly_less_than ) ) ),
inference(pattern_uni,[status(thm)],[235:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(21,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ less_than ) )
| ( B @ ( A @ less_than ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',totality) ).
thf(112,plain,
! [A: $i,B: $i] :
( ( A @ ( B @ less_than ) )
| ( B @ ( A @ less_than ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(113,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ less_than ) )
| ( B @ ( A @ less_than ) ) ),
inference(cnf,[status(esa)],[112]) ).
thf(9,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ less_than ) )
& ( B @ ( A @ less_than ) ) )
=> ( C @ ( A @ less_than ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity) ).
thf(80,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ less_than ) )
& ( B @ ( A @ less_than ) ) )
=> ( C @ ( A @ less_than ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(81,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less_than ) )
| ~ ( C @ ( B @ less_than ) )
| ~ ( B @ ( A @ less_than ) ) ),
inference(cnf,[status(esa)],[80]) ).
thf(249,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ( sk2 != create_slb )
| ( A != sk1 ) ),
inference(simp,[status(thm)],[239]) ).
thf(250,plain,
sk2 != create_slb,
inference(simp,[status(thm)],[249]) ).
thf(441,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C != sk2 )
| ( B != create_slb )
| ( C @ ( A @ contains_slb ) )
| ~ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) ) ),
inference(paramod_ordered,[status(thm)],[71,250]) ).
thf(442,plain,
! [C: $i,B: $i,A: $i] :
( ( B != create_slb )
| ( sk2 @ ( A @ contains_slb ) )
| ~ ( sk2 @ ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) ) ),
inference(pattern_uni,[status(thm)],[441:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( sk2 ))]]) ).
thf(964,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( A @ contains_slb ) )
| ~ ( sk2 @ ( B @ ( create_slb @ pair ) @ ( A @ insert_slb ) @ contains_slb ) ) ),
inference(simp,[status(thm)],[442]) ).
thf(107,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ lookup_slb ) )
= C ),
inference(cnf,[status(esa)],[106]) ).
thf(108,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ lookup_slb ) )
= C ),
inference(lifteq,[status(thm)],[107]) ).
thf(224,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( bottom @ less_than ) )
!= ( B @ ( C @ less_than ) ) )
| ~ $true
| ~ ( C @ ( B @ strictly_less_than ) ) ),
inference(paramod_ordered,[status(thm)],[89,60]) ).
thf(225,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( bottom @ less_than ) )
!= ( B @ ( C @ less_than ) ) )
| ~ ( C @ ( B @ strictly_less_than ) ) ),
inference(simp,[status(thm)],[224]) ).
thf(226,plain,
! [A: $i] :
~ ( bottom @ ( A @ strictly_less_than ) ),
inference(pattern_uni,[status(thm)],[225:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( bottom ))]]) ).
thf(7052,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6418,105]) ).
thf(7053,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7052]) ).
thf(7054,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7053:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(7080,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7054]) ).
thf(7882,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7080,105]) ).
thf(7883,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7882]) ).
thf(7884,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7883:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(7916,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7884]) ).
thf(11473,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7124,105]) ).
thf(11474,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[11473]) ).
thf(11475,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[11474:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(11507,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[11475]) ).
thf(7553,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6330,105]) ).
thf(7554,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7553]) ).
thf(7555,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7554:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(7578,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7555]) ).
thf(47,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( E @ ( D @ strictly_less_than ) )
=> ( ( C @ ( E @ ( D @ pair ) @ ( B @ insert_slb ) @ ( A @ triple ) ) @ check_cpq )
<=> $false ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax38) ).
thf(209,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( E @ ( D @ strictly_less_than ) )
=> ~ ( C @ ( E @ ( D @ pair ) @ ( B @ insert_slb ) @ ( A @ triple ) ) @ check_cpq ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(119,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ pair_in_list ) ) )
| ~ ( E @ ( C @ ( A @ pair_in_list ) ) ) ),
inference(cnfConj,[status(thm)],[116]) ).
thf(123,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ pair_in_list ) ) )
| ~ ( E @ ( C @ ( A @ pair_in_list ) ) ) ),
inference(simp,[status(thm)],[119]) ).
thf(29,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( B != create_slb )
=> ( ( C @ ( B @ ( A @ triple ) ) @ findmin_cpq_res )
= ( A @ findmin_pqp_res ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax51) ).
thf(145,plain,
! [A: $i,B: $i,C: $i] :
( ( B != create_slb )
=> ( ( C @ ( B @ ( A @ triple ) ) @ findmin_cpq_res )
= ( A @ findmin_pqp_res ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(11581,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7132,55]) ).
thf(11582,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[11581]) ).
thf(11583,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[11582:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(11611,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[11583]) ).
thf(61,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ strictly_less_than ) )
| ( A @ ( B @ less_than ) )
| ~ ( B @ ( A @ less_than ) ) ),
inference(cnfConj,[status(thm)],[58]) ).
thf(62,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ strictly_less_than ) )
| ( A @ ( B @ less_than ) )
| ~ ( B @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[61]) ).
thf(261,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( bottom @ less_than ) )
!= ( C @ ( B @ less_than ) ) )
| ( C @ ( B @ strictly_less_than ) )
| ( B @ ( C @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[89,62]) ).
thf(262,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( bottom @ less_than ) )
!= ( C @ ( B @ less_than ) ) )
| ( C @ ( B @ strictly_less_than ) )
| ( B @ ( C @ less_than ) ) ),
inference(simp,[status(thm)],[261]) ).
thf(263,plain,
! [A: $i] :
( ( A @ ( bottom @ strictly_less_than ) )
| ( bottom @ ( A @ less_than ) ) ),
inference(pattern_uni,[status(thm)],[262:[bind(A,$thf( A )),bind(B,$thf( bottom )),bind(C,$thf( A ))]]) ).
thf(7636,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6695,55]) ).
thf(7637,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7636]) ).
thf(7638,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7637:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(7655,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7638]) ).
thf(999,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[296,55]) ).
thf(1000,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[999]) ).
thf(1001,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[1000:[bind(A,$thf( K )),bind(B,$thf( K )),bind(C,$thf( K @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(1038,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[1001]) ).
thf(6600,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( D @ ( create_slb @ ( C @ triple ) ) @ findmin_cpq_eff ) )
| ( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) ) ) ),
inference(paramod_ordered,[status(thm)],[187,1596]) ).
thf(6601,plain,
! [A: $i] :
( ( bad @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff @ findmin_cpq_eff )
!= ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) ) ),
inference(pattern_uni,[status(thm)],[6600:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(2801,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ removemin_cpq_eff @ ( B @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2465,55]) ).
thf(2802,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ removemin_cpq_eff @ ( B @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) ) ),
inference(simp,[status(thm)],[2801]) ).
thf(2803,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( B @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[2802:[bind(A,$thf( H )),bind(B,$thf( I )),bind(C,$thf( I )),bind(D,$thf( H @ ( I @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(2807,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( B @ succ_cpq ) ),
inference(simp,[status(thm)],[2803]) ).
thf(45,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ succ_cpq ) )
=> ( C @ ( B @ remove_cpq ) @ ( A @ succ_cpq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax33) ).
thf(203,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ succ_cpq ) )
=> ( C @ ( B @ remove_cpq ) @ ( A @ succ_cpq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(2769,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ ( B @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2434,55]) ).
thf(2770,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ ( B @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) ) ),
inference(simp,[status(thm)],[2769]) ).
thf(2771,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ removemin_cpq_eff @ ( B @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[2770:[bind(A,$thf( G )),bind(B,$thf( I )),bind(C,$thf( I )),bind(D,$thf( G @ ( I @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff ))]]) ).
thf(2775,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ removemin_cpq_eff @ ( B @ succ_cpq ) ),
inference(simp,[status(thm)],[2771]) ).
thf(86,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ remove_slb ) )
= A ),
inference(cnf,[status(esa)],[85]) ).
thf(87,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( B @ pair ) @ ( A @ insert_slb ) @ remove_slb ) )
= A ),
inference(lifteq,[status(thm)],[86]) ).
thf(2092,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( D @ ( C @ insert_cpq ) @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[243,84]) ).
thf(2093,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( D @ ( C @ insert_cpq ) @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[2092]) ).
thf(2094,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ ( B @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[2093:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff )),bind(D,$thf( D ))]]) ).
thf(2130,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ ( B @ succ_cpq ) ),
inference(simp,[status(thm)],[2094]) ).
thf(2737,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ ( B @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2130,55]) ).
thf(2738,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ ( B @ succ_cpq ) )
!= ( D @ ( C @ succ_cpq ) ) )
| ( D @ removemin_cpq_eff @ ( C @ succ_cpq ) ) ),
inference(simp,[status(thm)],[2737]) ).
thf(2739,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ ( B @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[2738:[bind(A,$thf( F )),bind(B,$thf( I )),bind(C,$thf( I )),bind(D,$thf( F @ ( I @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) ))]]) ).
thf(2743,plain,
! [B: $i,A: $i] : ( A @ ( B @ removemin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ insert_cpq ) @ removemin_cpq_eff @ ( B @ succ_cpq ) ),
inference(simp,[status(thm)],[2739]) ).
thf(439,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B != sk2 )
| ( C != create_slb )
| ( C @ ( A @ contains_slb ) )
| ~ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ contains_slb ) ) ),
inference(paramod_ordered,[status(thm)],[71,250]) ).
thf(440,plain,
! [C: $i,B: $i,A: $i] :
( ( B != create_slb )
| ( B @ ( A @ contains_slb ) )
| ~ ( B @ ( C @ ( sk2 @ pair ) @ ( A @ insert_slb ) @ contains_slb ) ) ),
inference(pattern_uni,[status(thm)],[439:[bind(A,$thf( A )),bind(B,$thf( sk2 ))]]) ).
thf(963,plain,
! [B: $i,A: $i] :
( ( create_slb @ ( A @ contains_slb ) )
| ~ ( create_slb @ ( B @ ( sk2 @ pair ) @ ( A @ insert_slb ) @ contains_slb ) ) ),
inference(simp,[status(thm)],[440]) ).
thf(15540,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7235,55]) ).
thf(15541,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[15540]) ).
thf(15542,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[15541:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(15589,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[15542]) ).
thf(7904,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7080,55]) ).
thf(7905,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7904]) ).
thf(7906,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7905:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(7912,plain,
! [A: $i] : ( A @ removemin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7906]) ).
thf(287,plain,
! [A: $i] :
( ( ( A @ removemin_cpq_res @ ( A @ findmin_cpq_eff @ remove_cpq ) )
!= ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) ) )
| ( A @ removemin_cpq_eff @ check_cpq ) ),
inference(paramod_ordered,[status(thm)],[281,51]) ).
thf(290,plain,
! [A: $i] :
( ( ( A @ removemin_cpq_res )
!= sk4 )
| ( ( A @ findmin_cpq_eff )
!= ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) ) )
| ( A @ removemin_cpq_eff @ check_cpq ) ),
inference(simp,[status(thm)],[287]) ).
thf(11670,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7182,55]) ).
thf(11671,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[11670]) ).
thf(11672,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[11671:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(11685,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[11672]) ).
thf(2229,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( create_slb @ ( A @ triple ) ) @ findmin_cpq_eff )
!= ( D @ ( create_slb @ ( C @ triple ) ) @ findmin_cpq_eff ) )
| ( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) ) ) ),
inference(paramod_ordered,[status(thm)],[187,1057]) ).
thf(2230,plain,
! [A: $i] :
( ( bad @ ( create_slb @ ( A @ triple ) ) )
!= ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ triple ) ) @ remove_cpq ) ) ),
inference(pattern_uni,[status(thm)],[2229:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(39,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) @ ok )
=> ( D @ ( B @ contains_slb ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l27_l33) ).
thf(183,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ triple ) ) @ remove_cpq ) @ ok )
=> ( D @ ( B @ contains_slb ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(130,plain,
! [A: $i] :
( ( A @ ( create_slb @ update_slb ) )
= create_slb ),
inference(cnf,[status(esa)],[129]) ).
thf(131,plain,
! [A: $i] :
( ( A @ ( create_slb @ update_slb ) )
= create_slb ),
inference(lifteq,[status(thm)],[130]) ).
thf(11647,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7182,105]) ).
thf(11648,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ findmin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[11647]) ).
thf(11649,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[11648:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff ))]]) ).
thf(11675,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ findmin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[11649]) ).
thf(118,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D = E )
| ( E @ ( C @ ( A @ pair_in_list ) ) )
| ~ ( E @ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ pair_in_list ) ) ) ),
inference(cnfConj,[status(thm)],[116]) ).
thf(122,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ ( A @ pair_in_list ) ) )
| ~ ( E @ ( C @ ( D @ ( B @ pair ) @ ( A @ insert_slb ) @ pair_in_list ) ) )
| ( D = E ) ),
inference(lifteq,[status(thm)],[118]) ).
thf(7432,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6501,55]) ).
thf(7433,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ ( A @ succ_cpq ) )
!= ( C @ ( B @ succ_cpq ) ) )
| ( C @ removemin_cpq_eff @ ( B @ succ_cpq ) ) ),
inference(simp,[status(thm)],[7432]) ).
thf(7434,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(pattern_uni,[status(thm)],[7433:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff ))]]) ).
thf(7442,plain,
! [A: $i] : ( A @ findmin_cpq_eff @ removemin_cpq_eff @ findmin_cpq_eff @ removemin_cpq_eff @ ( A @ succ_cpq ) ),
inference(simp,[status(thm)],[7434]) ).
thf(110,plain,
~ ? [A: $i,B: $i] : ( B @ ( A @ ( create_slb @ pair_in_list ) ) ),
inference(miniscope,[status(thm)],[109]) ).
thf(111,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ ( create_slb @ pair_in_list ) ) ),
inference(cnf,[status(esa)],[110]) ).
thf(37389,plain,
$false,
inference(e,[status(thm)],[138,22328,11998,88,101,2131,170,1596,276,7641,7132,2590,7182,15579,1522,6695,56,6939,2434,2168,153,18595,142,11417,1761,7188,1196,185,6466,7235,288,1645,2136,257,2531,7592,52,3221,6423,125,2488,6332,157,7124,1704,93,3014,289,216,1946,8029,7245,106,84,7532,121,280,2190,89,1433,243,74,206,132,12008,233,248,60,15682,6388,102,1067,2000,1057,7814,85,7703,15692,165,2132,3286,92,229,197,65,97,11602,188,16087,141,1397,11435,53,109,77,193,6501,7523,7448,96,7717,22511,6331,2465,173,6418,1947,129,134,128,1170,2368,105,244,11516,1278,2001,6507,22396,1103,2149,166,1483,64,1595,149,180,296,176,191,281,21805,59,6344,71,54,144,6302,236,187,113,81,76,2856,98,6460,16090,103,213,964,1556,108,223,135,226,80,167,7916,11507,7578,209,112,123,145,48,63,11611,263,7655,1038,6330,6073,6601,72,2807,250,99,203,2775,1553,87,2743,104,963,2532,1101,139,2130,15589,7912,55,114,75,290,11685,2230,7080,82,6703,2123,1642,1280,51,190,183,239,126,79,1236,6383,131,7088,62,1431,254,11675,122,1069,7442,90,111]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV391+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.11/0.38 % Computer : n012.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sat Sep 26 13:40:20 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 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.74/0.86 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.22/1.05 % [INFO] Parsing done (191ms).
% 1.22/1.06 % [INFO] Running in sequential loop mode.
% 1.74/1.38 % [INFO] eprover registered as external prover.
% 1.74/1.39 % [INFO] Scanning for conjecture ...
% 1.95/1.48 % [INFO] Found a conjecture (or negated_conjecture) and 45 axioms. Running axiom selection ...
% 2.11/1.56 % [INFO] Axiom selection finished. Selected 45 axioms (removed 0 axioms).
% 2.34/1.63 % [INFO] Problem is first-order (TPTP FOF).
% 2.34/1.64 % [INFO] Type checking passed.
% 2.34/1.65 % [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 ...
% 98.18/24.41 % External prover 'e' found a proof!
% 98.18/24.41 % [INFO] Killing All external provers ...
% 98.18/24.41 % Time passed: 23901ms (effective reasoning time: 23343ms)
% 98.18/24.41 % 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)>
% 98.18/24.41 % Axioms used in derivation (45): ax28, ax39, ax32, l27_li4142, l27_li2829, ax22, ax43, ax19, ax49, ax25, ax53, ax20, ax52, ax24, ax47, ax41, stricly_smaller_definition, ax31, ax45, ax40, ax35, ax27, l27_l33, ax51, ax48, ax21, ax38, ax44, reflexivity, ax33, ax26, bottom_smallest, ax50, ax37, totality, ax46, ax34, ax23, l27_l30, transitivity, ax30, ax42, ax18, ax36, ax29
% 98.18/24.41 % No. of inferences in proof: 611
% 98.18/24.41 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 23901 ms resp. 23343 ms w/o parsing
% 92.63/24.53 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 92.63/24.53 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------