%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWV367+1 : TPTP v9.2.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:22:01 PM UTC 2026
% Result : Theorem 0.35s 1.61s
% Output : CNFRefutation 0.55s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_103)
% Comments :
%------------------------------------------------------------------------------
fof(l3_co,conjecture,
! [X1,X2,X3] :
( contains_pq(i(triple(X1,create_slb,X2)),X3)
=> i(remove_cpq(triple(X1,create_slb,X2),X3)) = remove_pq(i(triple(X1,create_slb,X2)),X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l3_co) ).
fof(ax38,axiom,
! [X1,X2,X3,X4,X5] :
( strictly_less_than(X4,X5)
=> ( check_cpq(triple(X1,insert_slb(X2,pair(X4,X5)),X3))
<=> ~ $true ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax38) ).
fof(ax47,axiom,
! [X1,X2,X3,X4] :
( ( X2 != create_slb
& ~ contains_slb(X2,findmin_pqp_res(X1)) )
=> findmin_cpq_eff(triple(X1,X2,X3)) = triple(X1,update_slb(X2,findmin_pqp_res(X1)),bad) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax47) ).
fof(ax43,axiom,
! [X1,X2,X3,X4] :
( ~ contains_slb(X2,X4)
=> remove_cpq(triple(X1,X2,X3),X4) = triple(X1,X2,bad) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax43) ).
fof(ax40,axiom,
! [X1,X2] :
( ok(triple(X1,X2,bad))
<=> ~ $true ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax40) ).
fof(ax41,axiom,
! [X1,X2,X3] :
( ~ ok(triple(X1,X2,X3))
=> X3 = bad ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax41) ).
fof(ax35,axiom,
! [X1,X2] :
( succ_cpq(X1,X2)
=> succ_cpq(X1,removemin_cpq_eff(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax35) ).
fof(ax52,axiom,
! [X1] : removemin_cpq_eff(X1) = remove_cpq(findmin_cpq_eff(X1),findmin_cpq_res(X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax52) ).
fof(ax22,axiom,
! [X1,X2] : ~ pair_in_list(create_slb,X1,X2),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax22) ).
fof(stricly_smaller_definition,axiom,
! [X1,X2] :
( strictly_less_than(X1,X2)
<=> ( less_than(X1,X2)
& ~ less_than(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+0.ax',stricly_smaller_definition) ).
fof(ax20,axiom,
! [X1] : ~ contains_slb(create_slb,X1),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax20) ).
fof(ax8,axiom,
! [X1] : ~ contains_pq(create_pq,X1),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+1.ax',ax8) ).
fof(ax37,axiom,
! [X1,X2,X3,X4,X5] :
( less_than(X5,X4)
=> ( check_cpq(triple(X1,insert_slb(X2,pair(X4,X5)),X3))
<=> check_cpq(triple(X1,X2,X3)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax37) ).
fof(ax55,axiom,
! [X1,X2,X3,X4,X5] : i(triple(X1,insert_slb(X2,pair(X4,X5)),X3)) = insert_pq(i(triple(X1,X2,X3)),X4),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+4.ax',ax55) ).
fof(ax49,axiom,
! [X1,X2,X3,X4] :
( ( X2 != create_slb
& contains_slb(X2,findmin_pqp_res(X1))
& less_than(lookup_slb(X2,findmin_pqp_res(X1)),findmin_pqp_res(X1)) )
=> findmin_cpq_eff(triple(X1,X2,X3)) = triple(X1,update_slb(X2,findmin_pqp_res(X1)),X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax49) ).
fof(ax48,axiom,
! [X1,X2,X3,X4] :
( ( X2 != create_slb
& contains_slb(X2,findmin_pqp_res(X1))
& strictly_less_than(findmin_pqp_res(X1),lookup_slb(X2,findmin_pqp_res(X1))) )
=> findmin_cpq_eff(triple(X1,X2,X3)) = triple(X1,update_slb(X2,findmin_pqp_res(X1)),bad) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax48) ).
fof(ax44,axiom,
! [X1,X2,X3,X4] :
( ( contains_slb(X2,X4)
& less_than(lookup_slb(X2,X4),X4) )
=> remove_cpq(triple(X1,X2,X3),X4) = triple(remove_pqp(X1,X4),remove_slb(X2,X4),X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax44) ).
fof(ax45,axiom,
! [X1,X2,X3,X4] :
( ( contains_slb(X2,X4)
& strictly_less_than(X4,lookup_slb(X2,X4)) )
=> remove_cpq(triple(X1,X2,X3),X4) = triple(remove_pqp(X1,X4),remove_slb(X2,X4),bad) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax45) ).
fof(ax42,axiom,
! [X1,X2,X3,X4] : insert_cpq(triple(X1,X2,X3),X4) = triple(insert_pqp(X1,X4),insert_slb(X2,pair(X4,bottom)),X3),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax42) ).
fof(ax23,axiom,
! [X1,X2,X3,X4,X5] :
( pair_in_list(insert_slb(X1,pair(X2,X4)),X3,X5)
<=> ( pair_in_list(X1,X3,X5)
| ( X2 = X3
& X4 = X5 ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax23) ).
fof(ax39,axiom,
! [X1,X2,X3,X4] :
( contains_cpq(triple(X1,X2,X3),X4)
<=> contains_slb(X2,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax39) ).
fof(ax25,axiom,
! [X1,X2,X3,X4] :
( ( X2 != X3
& contains_slb(X1,X3) )
=> remove_slb(insert_slb(X1,pair(X2,X4)),X3) = insert_slb(remove_slb(X1,X3),pair(X2,X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax25) ).
fof(ax29,axiom,
! [X1,X2,X3,X4] :
( strictly_less_than(X4,X3)
=> update_slb(insert_slb(X1,pair(X2,X4)),X3) = insert_slb(update_slb(X1,X3),pair(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax29) ).
fof(ax30,axiom,
! [X1,X2,X3,X4] :
( less_than(X3,X4)
=> update_slb(insert_slb(X1,pair(X2,X4)),X3) = insert_slb(update_slb(X1,X3),pair(X2,X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax30) ).
fof(ax21,axiom,
! [X1,X2,X3,X4] :
( contains_slb(insert_slb(X1,pair(X2,X4)),X3)
<=> ( contains_slb(X1,X3)
| X2 = X3 ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax21) ).
fof(ax46,axiom,
! [X1,X2] : findmin_cpq_eff(triple(X1,create_slb,X2)) = triple(X1,create_slb,bad),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax46) ).
fof(ax27,axiom,
! [X1,X2,X3,X4] :
( ( X2 != X3
& contains_slb(X1,X3) )
=> lookup_slb(insert_slb(X1,pair(X2,X4)),X3) = lookup_slb(X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax27) ).
fof(ax51,axiom,
! [X1,X2,X3,X4] :
( X2 != create_slb
=> findmin_cpq_res(triple(X1,X2,X3)) = findmin_pqp_res(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax51) ).
fof(ax36,axiom,
! [X1,X2] : check_cpq(triple(X1,create_slb,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax36) ).
fof(ax54,axiom,
! [X1,X2] : i(triple(X1,create_slb,X2)) = create_pq,
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+4.ax',ax54) ).
fof(ax50,axiom,
! [X1,X2] : findmin_cpq_res(triple(X1,create_slb,X2)) = bottom,
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax50) ).
fof(ax12,axiom,
! [X1,X2,X3] :
( ( contains_pq(X1,X3)
& X2 != X3 )
=> remove_pq(insert_pq(X1,X2),X3) = insert_pq(remove_pq(X1,X3),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+1.ax',ax12) ).
fof(ax26,axiom,
! [X1,X2,X3] : lookup_slb(insert_slb(X1,pair(X2,X3)),X2) = X3,
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax26) ).
fof(ax24,axiom,
! [X1,X2,X3] : remove_slb(insert_slb(X1,pair(X2,X3)),X2) = X1,
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax24) ).
fof(ax19,axiom,
! [X1,X2,X3] : isnonempty_slb(insert_slb(X1,pair(X2,X3))),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax19) ).
fof(ax9,axiom,
! [X1,X2,X3] :
( contains_pq(insert_pq(X1,X2),X3)
<=> ( contains_pq(X1,X3)
| X2 = X3 ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+1.ax',ax9) ).
fof(ax17,axiom,
! [X1,X2,X3] : insert_pq(insert_pq(X1,X2),X3) = insert_pq(insert_pq(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+1.ax',ax17) ).
fof(ax10,axiom,
! [X1,X2] :
( issmallestelement_pq(X1,X2)
<=> ! [X3] :
( contains_pq(X1,X3)
=> less_than(X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+1.ax',ax10) ).
fof(ax15,axiom,
! [X1,X2] :
( ( contains_pq(X1,X2)
& issmallestelement_pq(X1,X2) )
=> removemin_pq_eff(X1,X2) = remove_pq(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+1.ax',ax15) ).
fof(ax33,axiom,
! [X1,X2,X3] :
( succ_cpq(X1,X2)
=> succ_cpq(X1,remove_cpq(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax33) ).
fof(ax32,axiom,
! [X1,X2,X3] :
( succ_cpq(X1,X2)
=> succ_cpq(X1,insert_cpq(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax32) ).
fof(ax16,axiom,
! [X1,X2] :
( ( contains_pq(X1,X2)
& issmallestelement_pq(X1,X2) )
=> removemin_pq_res(X1,X2) = X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+1.ax',ax16) ).
fof(ax14,axiom,
! [X1,X2] :
( ( contains_pq(X1,X2)
& issmallestelement_pq(X1,X2) )
=> findmin_pq_res(X1,X2) = X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+1.ax',ax14) ).
fof(ax13,axiom,
! [X1,X2] :
( ( contains_pq(X1,X2)
& issmallestelement_pq(X1,X2) )
=> findmin_pq_eff(X1,X2) = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+1.ax',ax13) ).
fof(ax60,axiom,
! [X1,X2] :
( pi_sharp_removemin(X1,X2)
<=> ( contains_pq(X1,X2)
& issmallestelement_pq(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+4.ax',ax60) ).
fof(ax58,axiom,
! [X1,X2] :
( pi_sharp_find_min(X1,X2)
<=> ( contains_pq(X1,X2)
& issmallestelement_pq(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+4.ax',ax58) ).
fof(transitivity,axiom,
! [X1,X2,X3] :
( ( less_than(X1,X2)
& less_than(X2,X3) )
=> less_than(X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+0.ax',transitivity) ).
fof(ax57,axiom,
! [X1,X2] :
( pi_remove(X1,X2)
<=> pi_sharp_remove(i(X1),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+4.ax',ax57) ).
fof(ax34,axiom,
! [X1,X2] :
( succ_cpq(X1,X2)
=> succ_cpq(X1,findmin_cpq_eff(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax34) ).
fof(ax62,axiom,
! [X1] :
( phi(X1)
<=> ? [X2] :
( succ_cpq(X1,X2)
& ok(X2)
& check_cpq(X2) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+4.ax',ax62) ).
fof(ax11,axiom,
! [X1,X2] : remove_pq(insert_pq(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+1.ax',ax11) ).
fof(ax56,axiom,
! [X1,X2] :
( pi_sharp_remove(X1,X2)
<=> contains_pq(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+4.ax',ax56) ).
fof(ax61,axiom,
! [X1] :
( pi_removemin(X1)
<=> ? [X2] : pi_sharp_find_min(i(X1),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+4.ax',ax61) ).
fof(ax59,axiom,
! [X1] :
( pi_find_min(X1)
<=> ? [X2] : pi_sharp_find_min(i(X1),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+4.ax',ax59) ).
fof(ax7,axiom,
! [X1,X2] : isnonempty_pq(insert_pq(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+1.ax',ax7) ).
fof(totality,axiom,
! [X1,X2] :
( less_than(X1,X2)
| less_than(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+0.ax',totality) ).
fof(ax31,axiom,
! [X1] : succ_cpq(X1,X1),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax',ax31) ).
fof(reflexivity,axiom,
! [X1] : less_than(X1,X1),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+0.ax',reflexivity) ).
fof(bottom_smallest,axiom,
! [X1] : less_than(bottom,X1),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+0.ax',bottom_smallest) ).
fof(ax28,axiom,
! [X1] : update_slb(create_slb,X1) = create_slb,
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax28) ).
fof(ax18,axiom,
~ isnonempty_slb(create_slb),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax',ax18) ).
fof(ax6,axiom,
~ isnonempty_pq(create_pq),
file('/export/starexec/sandbox/benchmark/Axioms/SWV007+1.ax',ax6) ).
fof(i_0_62,negated_conjecture,
~ ! [X1,X2,X3] :
( contains_pq(i(triple(X1,create_slb,X2)),X3)
=> i(remove_cpq(triple(X1,create_slb,X2),X3)) = remove_pq(i(triple(X1,create_slb,X2)),X3) ),
inference(assume_negation,[status(cth)],[l3_co]) ).
fof(i_0_63,plain,
! [X1,X2,X3,X4,X5] :
( strictly_less_than(X4,X5)
=> ~ check_cpq(triple(X1,insert_slb(X2,pair(X4,X5)),X3)) ),
inference(fof_simplification,[status(thm)],[ax38]) ).
fof(i_0_64,plain,
! [X1,X2,X3,X4] :
( ( X2 != create_slb
& ~ contains_slb(X2,findmin_pqp_res(X1)) )
=> findmin_cpq_eff(triple(X1,X2,X3)) = triple(X1,update_slb(X2,findmin_pqp_res(X1)),bad) ),
inference(fof_simplification,[status(thm)],[ax47]) ).
fof(i_0_65,plain,
! [X1,X2,X3,X4] :
( ~ contains_slb(X2,X4)
=> remove_cpq(triple(X1,X2,X3),X4) = triple(X1,X2,bad) ),
inference(fof_simplification,[status(thm)],[ax43]) ).
fof(i_0_66,plain,
! [X1,X2] : ~ ok(triple(X1,X2,bad)),
inference(fof_simplification,[status(thm)],[ax40]) ).
fof(i_0_67,plain,
! [X1,X2,X3] :
( ~ ok(triple(X1,X2,X3))
=> X3 = bad ),
inference(fof_simplification,[status(thm)],[ax41]) ).
fof(i_0_68,plain,
! [X256,X257] :
( ~ succ_cpq(X256,X257)
| succ_cpq(X256,removemin_cpq_eff(X257)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax35])]) ).
fof(i_0_69,plain,
! [X311] : removemin_cpq_eff(X311) = remove_cpq(findmin_cpq_eff(X311),findmin_cpq_res(X311)),
inference(variable_rename,[status(thm)],[ax52]) ).
fof(i_0_70,plain,
! [X1,X2] : ~ pair_in_list(create_slb,X1,X2),
inference(fof_simplification,[status(thm)],[ax22]) ).
fof(i_0_71,plain,
! [X1,X2] :
( strictly_less_than(X1,X2)
<=> ( less_than(X1,X2)
& ~ less_than(X2,X1) ) ),
inference(fof_simplification,[status(thm)],[stricly_smaller_definition]) ).
fof(i_0_72,plain,
! [X1] : ~ contains_slb(create_slb,X1),
inference(fof_simplification,[status(thm)],[ax20]) ).
fof(i_0_73,plain,
! [X1] : ~ contains_pq(create_pq,X1),
inference(fof_simplification,[status(thm)],[ax8]) ).
fof(i_0_74,negated_conjecture,
( contains_pq(i(triple(esk5_0,create_slb,esk6_0)),esk7_0)
& i(remove_cpq(triple(esk5_0,create_slb,esk6_0),esk7_0)) != remove_pq(i(triple(esk5_0,create_slb,esk6_0)),esk7_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_62])])]) ).
fof(i_0_75,plain,
! [X260,X261,X262,X263,X264] :
( ( ~ check_cpq(triple(X260,insert_slb(X261,pair(X263,X264)),X262))
| check_cpq(triple(X260,X261,X262))
| ~ less_than(X264,X263) )
& ( ~ check_cpq(triple(X260,X261,X262))
| check_cpq(triple(X260,insert_slb(X261,pair(X263,X264)),X262))
| ~ less_than(X264,X263) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax37])])]) ).
fof(i_0_76,plain,
! [X315,X316,X317,X318,X319] : i(triple(X315,insert_slb(X316,pair(X318,X319)),X317)) = insert_pq(i(triple(X315,X316,X317)),X318),
inference(variable_rename,[status(thm)],[ax55]) ).
fof(i_0_77,plain,
! [X265,X266,X267,X268,X269] :
( ~ strictly_less_than(X268,X269)
| ~ check_cpq(triple(X265,insert_slb(X266,pair(X268,X269)),X267)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_63])]) ).
fof(i_0_78,plain,
! [X303,X304,X305] :
( X304 = create_slb
| ~ contains_slb(X304,findmin_pqp_res(X303))
| ~ less_than(lookup_slb(X304,findmin_pqp_res(X303)),findmin_pqp_res(X303))
| findmin_cpq_eff(triple(X303,X304,X305)) = triple(X303,update_slb(X304,findmin_pqp_res(X303)),X305) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[ax49])])]) ).
fof(i_0_79,plain,
! [X300,X301,X302] :
( X301 = create_slb
| ~ contains_slb(X301,findmin_pqp_res(X300))
| ~ strictly_less_than(findmin_pqp_res(X300),lookup_slb(X301,findmin_pqp_res(X300)))
| findmin_cpq_eff(triple(X300,X301,X302)) = triple(X300,update_slb(X301,findmin_pqp_res(X300)),bad) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[ax48])])]) ).
fof(i_0_80,plain,
! [X287,X288,X289,X290] :
( ~ contains_slb(X288,X290)
| ~ less_than(lookup_slb(X288,X290),X290)
| remove_cpq(triple(X287,X288,X289),X290) = triple(remove_pqp(X287,X290),remove_slb(X288,X290),X289) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax44])]) ).
fof(i_0_81,plain,
! [X291,X292,X293,X294] :
( ~ contains_slb(X292,X294)
| ~ strictly_less_than(X294,lookup_slb(X292,X294))
| remove_cpq(triple(X291,X292,X293),X294) = triple(remove_pqp(X291,X294),remove_slb(X292,X294),bad) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax45])]) ).
fof(i_0_82,plain,
! [X279,X280,X281,X282] : insert_cpq(triple(X279,X280,X281),X282) = triple(insert_pqp(X279,X282),insert_slb(X280,pair(X282,bottom)),X281),
inference(variable_rename,[status(thm)],[ax42]) ).
fof(i_0_83,plain,
! [X219,X220,X221,X222,X223] :
( ( X220 = X221
| pair_in_list(X219,X221,X223)
| ~ pair_in_list(insert_slb(X219,pair(X220,X222)),X221,X223) )
& ( X222 = X223
| pair_in_list(X219,X221,X223)
| ~ pair_in_list(insert_slb(X219,pair(X220,X222)),X221,X223) )
& ( ~ pair_in_list(X219,X221,X223)
| pair_in_list(insert_slb(X219,pair(X220,X222)),X221,X223) )
& ( X220 != X221
| X222 != X223
| pair_in_list(insert_slb(X219,pair(X220,X222)),X221,X223) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax23])])]) ).
fof(i_0_84,plain,
! [X297,X298,X299] :
( X298 = create_slb
| contains_slb(X298,findmin_pqp_res(X297))
| findmin_cpq_eff(triple(X297,X298,X299)) = triple(X297,update_slb(X298,findmin_pqp_res(X297)),bad) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[i_0_64])])]) ).
fof(i_0_85,plain,
! [X270,X271,X272,X273] :
( ( ~ contains_cpq(triple(X270,X271,X272),X273)
| contains_slb(X271,X273) )
& ( ~ contains_slb(X271,X273)
| contains_cpq(triple(X270,X271,X272),X273) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax39])]) ).
fof(i_0_86,plain,
! [X283,X284,X285,X286] :
( contains_slb(X284,X286)
| remove_cpq(triple(X283,X284,X285),X286) = triple(X283,X284,bad) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_65])]) ).
fof(i_0_87,plain,
! [X227,X228,X229,X230] :
( X228 = X229
| ~ contains_slb(X227,X229)
| remove_slb(insert_slb(X227,pair(X228,X230)),X229) = insert_slb(remove_slb(X227,X229),pair(X228,X230)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax25])]) ).
fof(i_0_88,plain,
! [X239,X240,X241,X242] :
( ~ strictly_less_than(X242,X241)
| update_slb(insert_slb(X239,pair(X240,X242)),X241) = insert_slb(update_slb(X239,X241),pair(X240,X241)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax29])]) ).
fof(i_0_89,plain,
! [X243,X244,X245,X246] :
( ~ less_than(X245,X246)
| update_slb(insert_slb(X243,pair(X244,X246)),X245) = insert_slb(update_slb(X243,X245),pair(X244,X246)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax30])]) ).
fof(i_0_90,plain,
! [X274,X275] : ~ ok(triple(X274,X275,bad)),
inference(variable_rename,[status(thm)],[i_0_66]) ).
fof(i_0_91,plain,
! [X213,X214,X215,X216] :
( ( ~ contains_slb(insert_slb(X213,pair(X214,X216)),X215)
| contains_slb(X213,X215)
| X214 = X215 )
& ( ~ contains_slb(X213,X215)
| contains_slb(insert_slb(X213,pair(X214,X216)),X215) )
& ( X214 != X215
| contains_slb(insert_slb(X213,pair(X214,X216)),X215) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax21])])]) ).
fof(i_0_92,plain,
! [X295,X296] : findmin_cpq_eff(triple(X295,create_slb,X296)) = triple(X295,create_slb,bad),
inference(variable_rename,[status(thm)],[ax46]) ).
fof(i_0_93,plain,
! [X234,X235,X236,X237] :
( X235 = X236
| ~ contains_slb(X234,X236)
| lookup_slb(insert_slb(X234,pair(X235,X237)),X236) = lookup_slb(X234,X236) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax27])]) ).
fof(i_0_94,plain,
! [X308,X309,X310] :
( X309 = create_slb
| findmin_cpq_res(triple(X308,X309,X310)) = findmin_pqp_res(X308) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[ax51])])]) ).
fof(i_0_95,plain,
! [X276,X277,X278] :
( ok(triple(X276,X277,X278))
| X278 = bad ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_67])]) ).
fof(i_0_96,plain,
! [X258,X259] : check_cpq(triple(X258,create_slb,X259)),
inference(variable_rename,[status(thm)],[ax36]) ).
fof(i_0_97,plain,
! [X313,X314] : i(triple(X313,create_slb,X314)) = create_pq,
inference(variable_rename,[status(thm)],[ax54]) ).
fof(i_0_98,plain,
! [X306,X307] : findmin_cpq_res(triple(X306,create_slb,X307)) = bottom,
inference(variable_rename,[status(thm)],[ax50]) ).
fof(i_0_99,plain,
! [X195,X196,X197] :
( ~ contains_pq(X195,X197)
| X196 = X197
| remove_pq(insert_pq(X195,X196),X197) = insert_pq(remove_pq(X195,X197),X196) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax12])]) ).
fof(i_0_100,plain,
! [X231,X232,X233] : lookup_slb(insert_slb(X231,pair(X232,X233)),X232) = X233,
inference(variable_rename,[status(thm)],[ax26]) ).
fof(i_0_101,plain,
! [X224,X225,X226] : remove_slb(insert_slb(X224,pair(X225,X226)),X225) = X224,
inference(variable_rename,[status(thm)],[ax24]) ).
cnf(i_0_102,plain,
( succ_cpq(X1,removemin_cpq_eff(X2))
| ~ succ_cpq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_68]) ).
cnf(i_0_103,plain,
removemin_cpq_eff(X1) = remove_cpq(findmin_cpq_eff(X1),findmin_cpq_res(X1)),
inference(split_conjunct,[status(thm)],[i_0_69]) ).
fof(i_0_104,plain,
! [X217,X218] : ~ pair_in_list(create_slb,X217,X218),
inference(variable_rename,[status(thm)],[i_0_70]) ).
fof(i_0_105,plain,
! [X209,X210,X211] : isnonempty_slb(insert_slb(X209,pair(X210,X211))),
inference(variable_rename,[status(thm)],[ax19]) ).
fof(i_0_106,plain,
! [X184,X185,X186] :
( ( ~ contains_pq(insert_pq(X184,X185),X186)
| contains_pq(X184,X186)
| X185 = X186 )
& ( ~ contains_pq(X184,X186)
| contains_pq(insert_pq(X184,X185),X186) )
& ( X185 != X186
| contains_pq(insert_pq(X184,X185),X186) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax9])])]) ).
fof(i_0_107,plain,
! [X206,X207,X208] : insert_pq(insert_pq(X206,X207),X208) = insert_pq(insert_pq(X206,X208),X207),
inference(variable_rename,[status(thm)],[ax17]) ).
fof(i_0_108,plain,
! [X187,X188,X189,X190,X191] :
( ( ~ issmallestelement_pq(X187,X188)
| ~ contains_pq(X187,X189)
| less_than(X188,X189) )
& ( contains_pq(X190,esk1_2(X190,X191))
| issmallestelement_pq(X190,X191) )
& ( ~ less_than(X191,esk1_2(X190,X191))
| issmallestelement_pq(X190,X191) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[ax10])])])])])]) ).
fof(i_0_109,plain,
! [X202,X203] :
( ~ contains_pq(X202,X203)
| ~ issmallestelement_pq(X202,X203)
| removemin_pq_eff(X202,X203) = remove_pq(X202,X203) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax15])]) ).
fof(i_0_110,plain,
! [X251,X252,X253] :
( ~ succ_cpq(X251,X252)
| succ_cpq(X251,remove_cpq(X252,X253)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax33])]) ).
fof(i_0_111,plain,
! [X248,X249,X250] :
( ~ succ_cpq(X248,X249)
| succ_cpq(X248,insert_cpq(X249,X250)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax32])]) ).
fof(i_0_112,plain,
! [X204,X205] :
( ~ contains_pq(X204,X205)
| ~ issmallestelement_pq(X204,X205)
| removemin_pq_res(X204,X205) = X205 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax16])]) ).
fof(i_0_113,plain,
! [X200,X201] :
( ~ contains_pq(X200,X201)
| ~ issmallestelement_pq(X200,X201)
| findmin_pq_res(X200,X201) = X201 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax14])]) ).
fof(i_0_114,plain,
! [X198,X199] :
( ~ contains_pq(X198,X199)
| ~ issmallestelement_pq(X198,X199)
| findmin_pq_eff(X198,X199) = X198 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax13])]) ).
fof(i_0_115,plain,
! [X330,X331] :
( ( contains_pq(X330,X331)
| ~ pi_sharp_removemin(X330,X331) )
& ( issmallestelement_pq(X330,X331)
| ~ pi_sharp_removemin(X330,X331) )
& ( ~ contains_pq(X330,X331)
| ~ issmallestelement_pq(X330,X331)
| pi_sharp_removemin(X330,X331) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax60])])]) ).
fof(i_0_116,plain,
! [X324,X325] :
( ( contains_pq(X324,X325)
| ~ pi_sharp_find_min(X324,X325) )
& ( issmallestelement_pq(X324,X325)
| ~ pi_sharp_find_min(X324,X325) )
& ( ~ contains_pq(X324,X325)
| ~ issmallestelement_pq(X324,X325)
| pi_sharp_find_min(X324,X325) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax58])])]) ).
fof(i_0_117,plain,
! [X172,X173,X174] :
( ~ less_than(X172,X173)
| ~ less_than(X173,X174)
| less_than(X172,X174) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitivity])]) ).
fof(i_0_118,plain,
! [X178,X179] :
( ( less_than(X178,X179)
| ~ strictly_less_than(X178,X179) )
& ( ~ less_than(X179,X178)
| ~ strictly_less_than(X178,X179) )
& ( ~ less_than(X178,X179)
| less_than(X179,X178)
| strictly_less_than(X178,X179) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_71])])]) ).
fof(i_0_119,plain,
! [X322,X323] :
( ( ~ pi_remove(X322,X323)
| pi_sharp_remove(i(X322),X323) )
& ( ~ pi_sharp_remove(i(X322),X323)
| pi_remove(X322,X323) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax57])]) ).
fof(i_0_120,plain,
! [X254,X255] :
( ~ succ_cpq(X254,X255)
| succ_cpq(X254,findmin_cpq_eff(X255)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax34])]) ).
fof(i_0_121,plain,
! [X336,X338,X339] :
( ( succ_cpq(X336,esk4_1(X336))
| ~ phi(X336) )
& ( ok(esk4_1(X336))
| ~ phi(X336) )
& ( check_cpq(esk4_1(X336))
| ~ phi(X336) )
& ( ~ succ_cpq(X338,X339)
| ~ ok(X339)
| ~ check_cpq(X339)
| phi(X338) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[ax62])])])])])]) ).
fof(i_0_122,plain,
! [X193,X194] : remove_pq(insert_pq(X193,X194),X194) = X193,
inference(variable_rename,[status(thm)],[ax11]) ).
fof(i_0_123,plain,
! [X320,X321] :
( ( ~ pi_sharp_remove(X320,X321)
| contains_pq(X320,X321) )
& ( ~ contains_pq(X320,X321)
| pi_sharp_remove(X320,X321) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax56])]) ).
fof(i_0_124,plain,
! [X332,X334,X335] :
( ( ~ pi_removemin(X332)
| pi_sharp_find_min(i(X332),esk3_1(X332)) )
& ( ~ pi_sharp_find_min(i(X334),X335)
| pi_removemin(X334) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[ax61])])])])]) ).
fof(i_0_125,plain,
! [X326,X328,X329] :
( ( ~ pi_find_min(X326)
| pi_sharp_find_min(i(X326),esk2_1(X326)) )
& ( ~ pi_sharp_find_min(i(X328),X329)
| pi_find_min(X328) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[ax59])])])])]) ).
fof(i_0_126,plain,
! [X181,X182] : isnonempty_pq(insert_pq(X181,X182)),
inference(variable_rename,[status(thm)],[ax7]) ).
fof(i_0_127,plain,
! [X175,X176] :
( less_than(X175,X176)
| less_than(X176,X175) ),
inference(variable_rename,[status(thm)],[totality]) ).
fof(i_0_128,plain,
! [X212] : ~ contains_slb(create_slb,X212),
inference(variable_rename,[status(thm)],[i_0_72]) ).
fof(i_0_129,plain,
! [X183] : ~ contains_pq(create_pq,X183),
inference(variable_rename,[status(thm)],[i_0_73]) ).
fof(i_0_130,plain,
! [X247] : succ_cpq(X247,X247),
inference(variable_rename,[status(thm)],[ax31]) ).
fof(i_0_131,plain,
! [X177] : less_than(X177,X177),
inference(variable_rename,[status(thm)],[reflexivity]) ).
fof(i_0_132,plain,
! [X180] : less_than(bottom,X180),
inference(variable_rename,[status(thm)],[bottom_smallest]) ).
fof(i_0_133,plain,
! [X238] : update_slb(create_slb,X238) = create_slb,
inference(variable_rename,[status(thm)],[ax28]) ).
fof(i_0_134,plain,
~ isnonempty_slb(create_slb),
inference(fof_simplification,[status(thm)],[ax18]) ).
fof(i_0_135,plain,
~ isnonempty_pq(create_pq),
inference(fof_simplification,[status(thm)],[ax6]) ).
cnf(i_0_136,negated_conjecture,
i(remove_cpq(triple(esk5_0,create_slb,esk6_0),esk7_0)) != remove_pq(i(triple(esk5_0,create_slb,esk6_0)),esk7_0),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_137,plain,
( check_cpq(triple(X1,X2,X5))
| ~ check_cpq(triple(X1,insert_slb(X2,pair(X3,X4)),X5))
| ~ less_than(X4,X3) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_138,plain,
i(triple(X1,insert_slb(X2,pair(X3,X4)),X5)) = insert_pq(i(triple(X1,X2,X5)),X3),
inference(split_conjunct,[status(thm)],[i_0_76]),
[final] ).
cnf(i_0_139,plain,
( check_cpq(triple(X1,insert_slb(X2,pair(X4,X5)),X3))
| ~ check_cpq(triple(X1,X2,X3))
| ~ less_than(X5,X4) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_140,plain,
( ~ strictly_less_than(X1,X2)
| ~ check_cpq(triple(X3,insert_slb(X4,pair(X1,X2)),X5)) ),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_141,plain,
( X1 = create_slb
| findmin_cpq_eff(triple(X2,X1,X3)) = triple(X2,update_slb(X1,findmin_pqp_res(X2)),X3)
| ~ contains_slb(X1,findmin_pqp_res(X2))
| ~ less_than(lookup_slb(X1,findmin_pqp_res(X2)),findmin_pqp_res(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_142,plain,
( X1 = create_slb
| findmin_cpq_eff(triple(X2,X1,X3)) = triple(X2,update_slb(X1,findmin_pqp_res(X2)),bad)
| ~ contains_slb(X1,findmin_pqp_res(X2))
| ~ strictly_less_than(findmin_pqp_res(X2),lookup_slb(X1,findmin_pqp_res(X2))) ),
inference(split_conjunct,[status(thm)],[i_0_79]),
[final] ).
cnf(i_0_143,plain,
( remove_cpq(triple(X3,X1,X4),X2) = triple(remove_pqp(X3,X2),remove_slb(X1,X2),X4)
| ~ contains_slb(X1,X2)
| ~ less_than(lookup_slb(X1,X2),X2) ),
inference(split_conjunct,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_144,plain,
( remove_cpq(triple(X3,X1,X4),X2) = triple(remove_pqp(X3,X2),remove_slb(X1,X2),bad)
| ~ contains_slb(X1,X2)
| ~ strictly_less_than(X2,lookup_slb(X1,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_145,plain,
insert_cpq(triple(X1,X2,X3),X4) = triple(insert_pqp(X1,X4),insert_slb(X2,pair(X4,bottom)),X3),
inference(split_conjunct,[status(thm)],[i_0_82]),
[final] ).
cnf(i_0_146,plain,
( X1 = X2
| pair_in_list(X3,X2,X4)
| ~ pair_in_list(insert_slb(X3,pair(X1,X5)),X2,X4) ),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_147,plain,
( X1 = X2
| pair_in_list(X3,X4,X2)
| ~ pair_in_list(insert_slb(X3,pair(X5,X1)),X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_148,plain,
( X1 = create_slb
| contains_slb(X1,findmin_pqp_res(X2))
| findmin_cpq_eff(triple(X2,X1,X3)) = triple(X2,update_slb(X1,findmin_pqp_res(X2)),bad) ),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_149,plain,
( pair_in_list(insert_slb(X1,pair(X4,X5)),X2,X3)
| ~ pair_in_list(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_150,negated_conjecture,
contains_pq(i(triple(esk5_0,create_slb,esk6_0)),esk7_0),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_151,plain,
( contains_slb(X2,X4)
| ~ contains_cpq(triple(X1,X2,X3),X4) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_152,plain,
( contains_slb(X1,X2)
| remove_cpq(triple(X3,X1,X4),X2) = triple(X3,X1,bad) ),
inference(split_conjunct,[status(thm)],[i_0_86]),
[final] ).
cnf(i_0_153,plain,
( X1 = X2
| remove_slb(insert_slb(X3,pair(X1,X4)),X2) = insert_slb(remove_slb(X3,X2),pair(X1,X4))
| ~ contains_slb(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_154,plain,
( update_slb(insert_slb(X3,pair(X4,X1)),X2) = insert_slb(update_slb(X3,X2),pair(X4,X2))
| ~ strictly_less_than(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_88]),
[final] ).
cnf(i_0_155,plain,
( update_slb(insert_slb(X3,pair(X4,X2)),X1) = insert_slb(update_slb(X3,X1),pair(X4,X2))
| ~ less_than(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_89]),
[final] ).
cnf(i_0_156,plain,
~ ok(triple(X1,X2,bad)),
inference(split_conjunct,[status(thm)],[i_0_90]),
[final] ).
cnf(i_0_157,plain,
( contains_slb(X1,X4)
| X2 = X4
| ~ contains_slb(insert_slb(X1,pair(X2,X3)),X4) ),
inference(split_conjunct,[status(thm)],[i_0_91]),
[final] ).
cnf(i_0_158,plain,
findmin_cpq_eff(triple(X1,create_slb,X2)) = triple(X1,create_slb,bad),
inference(split_conjunct,[status(thm)],[i_0_92]),
[final] ).
cnf(i_0_159,plain,
( contains_cpq(triple(X3,X1,X4),X2)
| ~ contains_slb(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_160,plain,
( pair_in_list(insert_slb(X5,pair(X1,X3)),X2,X4)
| X1 != X2
| X3 != X4 ),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_161,plain,
( X1 = X2
| lookup_slb(insert_slb(X3,pair(X1,X4)),X2) = lookup_slb(X3,X2)
| ~ contains_slb(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_93]),
[final] ).
cnf(i_0_162,plain,
( X1 = create_slb
| findmin_cpq_res(triple(X2,X1,X3)) = findmin_pqp_res(X2) ),
inference(split_conjunct,[status(thm)],[i_0_94]),
[final] ).
cnf(i_0_163,plain,
( contains_slb(insert_slb(X1,pair(X3,X4)),X2)
| ~ contains_slb(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_91]),
[final] ).
cnf(i_0_164,plain,
( ok(triple(X1,X2,X3))
| X3 = bad ),
inference(split_conjunct,[status(thm)],[i_0_95]),
[final] ).
cnf(i_0_165,plain,
check_cpq(triple(X1,create_slb,X2)),
inference(split_conjunct,[status(thm)],[i_0_96]),
[final] ).
cnf(i_0_166,plain,
i(triple(X1,create_slb,X2)) = create_pq,
inference(split_conjunct,[status(thm)],[i_0_97]),
[final] ).
cnf(i_0_167,plain,
findmin_cpq_res(triple(X1,create_slb,X2)) = bottom,
inference(split_conjunct,[status(thm)],[i_0_98]),
[final] ).
cnf(i_0_168,plain,
( X3 = X2
| remove_pq(insert_pq(X1,X3),X2) = insert_pq(remove_pq(X1,X2),X3)
| ~ contains_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_99]),
[final] ).
cnf(i_0_169,plain,
( contains_slb(insert_slb(X3,pair(X1,X4)),X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_91]),
[final] ).
cnf(i_0_170,plain,
lookup_slb(insert_slb(X1,pair(X2,X3)),X2) = X3,
inference(split_conjunct,[status(thm)],[i_0_100]),
[final] ).
cnf(i_0_171,plain,
remove_slb(insert_slb(X1,pair(X2,X3)),X2) = X1,
inference(split_conjunct,[status(thm)],[i_0_101]),
[final] ).
cnf(i_0_172,plain,
( succ_cpq(X1,remove_cpq(findmin_cpq_eff(X2),findmin_cpq_res(X2)))
| ~ succ_cpq(X1,X2) ),
inference(rw,[status(thm)],[i_0_102,c_0_103]),
[final] ).
cnf(i_0_173,plain,
~ pair_in_list(create_slb,X1,X2),
inference(split_conjunct,[status(thm)],[i_0_104]),
[final] ).
cnf(i_0_174,plain,
isnonempty_slb(insert_slb(X1,pair(X2,X3))),
inference(split_conjunct,[status(thm)],[i_0_105]),
[final] ).
cnf(i_0_175,plain,
( contains_pq(X1,X3)
| X2 = X3
| ~ contains_pq(insert_pq(X1,X2),X3) ),
inference(split_conjunct,[status(thm)],[i_0_106]),
[final] ).
cnf(i_0_176,plain,
insert_pq(insert_pq(X1,X2),X3) = insert_pq(insert_pq(X1,X3),X2),
inference(split_conjunct,[status(thm)],[i_0_107]),
[final] ).
cnf(i_0_177,plain,
( issmallestelement_pq(X2,X1)
| ~ less_than(X1,esk1_2(X2,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_108]),
[final] ).
cnf(i_0_178,plain,
( removemin_pq_eff(X1,X2) = remove_pq(X1,X2)
| ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_179,plain,
( contains_pq(insert_pq(X1,X3),X2)
| ~ contains_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_106]),
[final] ).
cnf(i_0_180,plain,
( succ_cpq(X1,remove_cpq(X2,X3))
| ~ succ_cpq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_110]),
[final] ).
cnf(i_0_181,plain,
( succ_cpq(X1,insert_cpq(X2,X3))
| ~ succ_cpq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_111]),
[final] ).
cnf(i_0_182,plain,
( removemin_pq_res(X1,X2) = X2
| ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_112]),
[final] ).
cnf(i_0_183,plain,
( findmin_pq_res(X1,X2) = X2
| ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_113]),
[final] ).
cnf(i_0_184,plain,
( findmin_pq_eff(X1,X2) = X1
| ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_114]),
[final] ).
cnf(i_0_185,plain,
( pi_sharp_removemin(X1,X2)
| ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_115]),
[final] ).
cnf(i_0_186,plain,
( pi_sharp_find_min(X1,X2)
| ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_116]),
[final] ).
cnf(i_0_187,plain,
( less_than(X1,X3)
| ~ less_than(X1,X2)
| ~ less_than(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_117]),
[final] ).
cnf(i_0_188,plain,
( less_than(X2,X3)
| ~ issmallestelement_pq(X1,X2)
| ~ contains_pq(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_108]),
[final] ).
cnf(i_0_189,plain,
( contains_pq(X1,esk1_2(X1,X2))
| issmallestelement_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_108]),
[final] ).
cnf(i_0_190,plain,
( less_than(X2,X1)
| strictly_less_than(X1,X2)
| ~ less_than(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_118]),
[final] ).
cnf(i_0_191,plain,
( pi_remove(X1,X2)
| ~ pi_sharp_remove(i(X1),X2) ),
inference(split_conjunct,[status(thm)],[i_0_119]),
[final] ).
cnf(i_0_192,plain,
( ~ less_than(X1,X2)
| ~ strictly_less_than(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_118]),
[final] ).
cnf(i_0_193,plain,
( contains_pq(insert_pq(X3,X1),X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_106]),
[final] ).
cnf(i_0_194,plain,
( pi_sharp_remove(i(X1),X2)
| ~ pi_remove(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_119]),
[final] ).
cnf(i_0_195,plain,
( succ_cpq(X1,findmin_cpq_eff(X2))
| ~ succ_cpq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_120]),
[final] ).
cnf(i_0_196,plain,
( phi(X1)
| ~ succ_cpq(X1,X2)
| ~ ok(X2)
| ~ check_cpq(X2) ),
inference(split_conjunct,[status(thm)],[i_0_121]),
[final] ).
cnf(i_0_197,plain,
remove_pq(insert_pq(X1,X2),X2) = X1,
inference(split_conjunct,[status(thm)],[i_0_122]),
[final] ).
cnf(i_0_198,plain,
( pi_sharp_remove(X1,X2)
| ~ contains_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_123]),
[final] ).
cnf(i_0_199,plain,
( issmallestelement_pq(X1,X2)
| ~ pi_sharp_removemin(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_115]),
[final] ).
cnf(i_0_200,plain,
( issmallestelement_pq(X1,X2)
| ~ pi_sharp_find_min(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_116]),
[final] ).
cnf(i_0_201,plain,
( contains_pq(X1,X2)
| ~ pi_sharp_removemin(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_115]),
[final] ).
cnf(i_0_202,plain,
( contains_pq(X1,X2)
| ~ pi_sharp_find_min(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_116]),
[final] ).
cnf(i_0_203,plain,
( contains_pq(X1,X2)
| ~ pi_sharp_remove(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_123]),
[final] ).
cnf(i_0_204,plain,
( less_than(X1,X2)
| ~ strictly_less_than(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_118]),
[final] ).
cnf(i_0_205,plain,
( pi_removemin(X1)
| ~ pi_sharp_find_min(i(X1),X2) ),
inference(split_conjunct,[status(thm)],[i_0_124]),
[final] ).
cnf(i_0_206,plain,
( pi_find_min(X1)
| ~ pi_sharp_find_min(i(X1),X2) ),
inference(split_conjunct,[status(thm)],[i_0_125]),
[final] ).
cnf(i_0_207,plain,
( pi_sharp_find_min(i(X1),esk3_1(X1))
| ~ pi_removemin(X1) ),
inference(split_conjunct,[status(thm)],[i_0_124]),
[final] ).
cnf(i_0_208,plain,
( pi_sharp_find_min(i(X1),esk2_1(X1))
| ~ pi_find_min(X1) ),
inference(split_conjunct,[status(thm)],[i_0_125]),
[final] ).
cnf(i_0_209,plain,
isnonempty_pq(insert_pq(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_126]),
[final] ).
cnf(i_0_210,plain,
( less_than(X1,X2)
| less_than(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_127]),
[final] ).
cnf(i_0_211,plain,
( succ_cpq(X1,esk4_1(X1))
| ~ phi(X1) ),
inference(split_conjunct,[status(thm)],[i_0_121]),
[final] ).
cnf(i_0_212,plain,
~ contains_slb(create_slb,X1),
inference(split_conjunct,[status(thm)],[i_0_128]),
[final] ).
cnf(i_0_213,plain,
~ contains_pq(create_pq,X1),
inference(split_conjunct,[status(thm)],[i_0_129]),
[final] ).
cnf(i_0_214,plain,
( ok(esk4_1(X1))
| ~ phi(X1) ),
inference(split_conjunct,[status(thm)],[i_0_121]),
[final] ).
cnf(i_0_215,plain,
( check_cpq(esk4_1(X1))
| ~ phi(X1) ),
inference(split_conjunct,[status(thm)],[i_0_121]),
[final] ).
cnf(i_0_216,plain,
succ_cpq(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_130]),
[final] ).
cnf(i_0_217,plain,
less_than(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_131]),
[final] ).
cnf(i_0_218,plain,
less_than(bottom,X1),
inference(split_conjunct,[status(thm)],[i_0_132]),
[final] ).
cnf(i_0_219,plain,
update_slb(create_slb,X1) = create_slb,
inference(split_conjunct,[status(thm)],[i_0_133]),
[final] ).
cnf(i_0_220,plain,
~ isnonempty_slb(create_slb),
inference(split_conjunct,[status(thm)],[i_0_134]),
[final] ).
cnf(i_0_221,plain,
~ isnonempty_pq(create_pq),
inference(split_conjunct,[status(thm)],[i_0_135]),
[final] ).
cnf(i_0_222,axiom,
X1 = X1 ).
cnf(i_0_223,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_224,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_225,axiom,
( X1 != X2
| i(X1) = i(X2) ) ).
cnf(i_0_226,axiom,
( X1 != X2
| findmin_pqp_res(X1) = findmin_pqp_res(X2) ) ).
cnf(i_0_227,axiom,
( X1 != X2
| lookup_slb(X1,X3) = lookup_slb(X2,X3) ) ).
cnf(i_0_228,axiom,
( X1 != X2
| lookup_slb(X3,X1) = lookup_slb(X3,X2) ) ).
cnf(i_0_229,axiom,
( X1 != X2
| remove_slb(X1,X3) = remove_slb(X2,X3) ) ).
cnf(i_0_230,axiom,
( X1 != X2
| remove_slb(X3,X1) = remove_slb(X3,X2) ) ).
cnf(i_0_231,axiom,
( X1 != X2
| insert_cpq(X1,X3) = insert_cpq(X2,X3) ) ).
cnf(i_0_232,axiom,
( X1 != X2
| insert_cpq(X3,X1) = insert_cpq(X3,X2) ) ).
cnf(i_0_233,axiom,
( X1 != X2
| findmin_cpq_res(X1) = findmin_cpq_res(X2) ) ).
cnf(i_0_234,axiom,
( X1 != X2
| removemin_pq_eff(X1,X3) = removemin_pq_eff(X2,X3) ) ).
cnf(i_0_235,axiom,
( X1 != X2
| removemin_pq_eff(X3,X1) = removemin_pq_eff(X3,X2) ) ).
cnf(i_0_236,axiom,
( X1 != X2
| removemin_pq_res(X1,X3) = removemin_pq_res(X2,X3) ) ).
cnf(i_0_237,axiom,
( X1 != X2
| removemin_pq_res(X3,X1) = removemin_pq_res(X3,X2) ) ).
cnf(i_0_238,axiom,
( X1 != X2
| remove_cpq(X1,X3) = remove_cpq(X2,X3) ) ).
cnf(i_0_239,axiom,
( X1 != X2
| remove_cpq(X3,X1) = remove_cpq(X3,X2) ) ).
cnf(i_0_240,axiom,
( X1 != X2
| findmin_pq_res(X1,X3) = findmin_pq_res(X2,X3) ) ).
cnf(i_0_241,axiom,
( X1 != X2
| findmin_pq_res(X3,X1) = findmin_pq_res(X3,X2) ) ).
cnf(i_0_242,axiom,
( X1 != X2
| findmin_pq_eff(X1,X3) = findmin_pq_eff(X2,X3) ) ).
cnf(i_0_243,axiom,
( X1 != X2
| findmin_pq_eff(X3,X1) = findmin_pq_eff(X3,X2) ) ).
cnf(i_0_244,axiom,
( X1 != X2
| triple(X1,X3,X4) = triple(X2,X3,X4) ) ).
cnf(i_0_245,axiom,
( X1 != X2
| triple(X3,X1,X4) = triple(X3,X2,X4) ) ).
cnf(i_0_246,axiom,
( X1 != X2
| triple(X3,X4,X1) = triple(X3,X4,X2) ) ).
cnf(i_0_247,axiom,
( X1 != X2
| remove_pq(X1,X3) = remove_pq(X2,X3) ) ).
cnf(i_0_248,axiom,
( X1 != X2
| remove_pq(X3,X1) = remove_pq(X3,X2) ) ).
cnf(i_0_249,axiom,
( X1 != X2
| insert_slb(X1,X3) = insert_slb(X2,X3) ) ).
cnf(i_0_250,axiom,
( X1 != X2
| insert_slb(X3,X1) = insert_slb(X3,X2) ) ).
cnf(i_0_251,axiom,
( X1 != X2
| insert_pq(X1,X3) = insert_pq(X2,X3) ) ).
cnf(i_0_252,axiom,
( X1 != X2
| insert_pq(X3,X1) = insert_pq(X3,X2) ) ).
cnf(i_0_253,axiom,
( X1 != X2
| findmin_cpq_eff(X1) = findmin_cpq_eff(X2) ) ).
cnf(i_0_254,axiom,
( X1 != X2
| update_slb(X1,X3) = update_slb(X2,X3) ) ).
cnf(i_0_255,axiom,
( X1 != X2
| update_slb(X3,X1) = update_slb(X3,X2) ) ).
cnf(i_0_256,axiom,
( X1 != X2
| ~ check_cpq(X1)
| check_cpq(X2) ) ).
cnf(i_0_257,axiom,
( X1 != X2
| ~ isnonempty_slb(X1)
| isnonempty_slb(X2) ) ).
cnf(i_0_258,axiom,
( X1 != X2
| ~ issmallestelement_pq(X1,X3)
| issmallestelement_pq(X2,X3) ) ).
cnf(i_0_259,axiom,
( X1 != X2
| ~ issmallestelement_pq(X3,X1)
| issmallestelement_pq(X3,X2) ) ).
cnf(i_0_260,axiom,
( X1 != X2
| ~ pi_sharp_removemin(X1,X3)
| pi_sharp_removemin(X2,X3) ) ).
cnf(i_0_261,axiom,
( X1 != X2
| ~ pi_sharp_removemin(X3,X1)
| pi_sharp_removemin(X3,X2) ) ).
cnf(i_0_262,axiom,
( X1 != X2
| ~ pi_sharp_find_min(X1,X3)
| pi_sharp_find_min(X2,X3) ) ).
cnf(i_0_263,axiom,
( X1 != X2
| ~ pi_sharp_find_min(X3,X1)
| pi_sharp_find_min(X3,X2) ) ).
cnf(i_0_264,axiom,
( X1 != X2
| ~ pi_remove(X1,X3)
| pi_remove(X2,X3) ) ).
cnf(i_0_265,axiom,
( X1 != X2
| ~ pi_remove(X3,X1)
| pi_remove(X3,X2) ) ).
cnf(i_0_266,axiom,
( X1 != X2
| ~ pi_sharp_remove(X1,X3)
| pi_sharp_remove(X2,X3) ) ).
cnf(i_0_267,axiom,
( X1 != X2
| ~ pi_sharp_remove(X3,X1)
| pi_sharp_remove(X3,X2) ) ).
cnf(i_0_268,axiom,
( X1 != X2
| ~ phi(X1)
| phi(X2) ) ).
cnf(i_0_269,axiom,
( X1 != X2
| ~ pi_removemin(X1)
| pi_removemin(X2) ) ).
cnf(i_0_270,axiom,
( X1 != X2
| ~ pi_find_min(X1)
| pi_find_min(X2) ) ).
cnf(i_0_271,axiom,
( X1 != X2
| ~ isnonempty_pq(X1)
| isnonempty_pq(X2) ) ).
cnf(i_0_272,axiom,
( X1 != X2
| ~ less_than(X1,X3)
| less_than(X2,X3) ) ).
cnf(i_0_273,axiom,
( X1 != X2
| ~ less_than(X3,X1)
| less_than(X3,X2) ) ).
cnf(i_0_274,axiom,
( X1 != X2
| ~ strictly_less_than(X1,X3)
| strictly_less_than(X2,X3) ) ).
cnf(i_0_275,axiom,
( X1 != X2
| ~ strictly_less_than(X3,X1)
| strictly_less_than(X3,X2) ) ).
cnf(i_0_276,axiom,
( X1 != X2
| ~ contains_slb(X1,X3)
| contains_slb(X2,X3) ) ).
cnf(i_0_277,axiom,
( X1 != X2
| ~ contains_slb(X3,X1)
| contains_slb(X3,X2) ) ).
cnf(i_0_278,axiom,
( X1 != X2
| ~ pair_in_list(X1,X3,X4)
| pair_in_list(X2,X3,X4) ) ).
cnf(i_0_279,axiom,
( X1 != X2
| ~ pair_in_list(X3,X1,X4)
| pair_in_list(X3,X2,X4) ) ).
cnf(i_0_280,axiom,
( X1 != X2
| ~ pair_in_list(X3,X4,X1)
| pair_in_list(X3,X4,X2) ) ).
cnf(i_0_281,axiom,
( X1 != X2
| ~ contains_pq(X1,X3)
| contains_pq(X2,X3) ) ).
cnf(i_0_282,axiom,
( X1 != X2
| ~ contains_pq(X3,X1)
| contains_pq(X3,X2) ) ).
cnf(i_0_283,axiom,
( X1 != X2
| ~ contains_cpq(X1,X3)
| contains_cpq(X2,X3) ) ).
cnf(i_0_284,axiom,
( X1 != X2
| ~ contains_cpq(X3,X1)
| contains_cpq(X3,X2) ) ).
cnf(i_0_285,axiom,
( X1 != X2
| ~ ok(X1)
| ok(X2) ) ).
cnf(i_0_286,axiom,
( X1 != X2
| ~ succ_cpq(X1,X3)
| succ_cpq(X2,X3) ) ).
cnf(i_0_287,axiom,
( X1 != X2
| ~ succ_cpq(X3,X1)
| succ_cpq(X3,X2) ) ).
cnf(i_0_222_001,axiom,
X1 = X1 ).
cnf(i_0_223_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_224_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_225_004,axiom,
( X1 != X2
| i(X1) = i(X2) ) ).
cnf(i_0_226_005,axiom,
( X1 != X2
| findmin_pqp_res(X1) = findmin_pqp_res(X2) ) ).
cnf(i_0_227_006,axiom,
( X1 != X2
| lookup_slb(X1,X3) = lookup_slb(X2,X3) ) ).
cnf(i_0_228_007,axiom,
( X1 != X2
| lookup_slb(X3,X1) = lookup_slb(X3,X2) ) ).
cnf(i_0_229_008,axiom,
( X1 != X2
| remove_slb(X1,X3) = remove_slb(X2,X3) ) ).
cnf(i_0_230_009,axiom,
( X1 != X2
| remove_slb(X3,X1) = remove_slb(X3,X2) ) ).
cnf(i_0_231_010,axiom,
( X1 != X2
| insert_cpq(X1,X3) = insert_cpq(X2,X3) ) ).
cnf(i_0_232_011,axiom,
( X1 != X2
| insert_cpq(X3,X1) = insert_cpq(X3,X2) ) ).
cnf(i_0_233_012,axiom,
( X1 != X2
| findmin_cpq_res(X1) = findmin_cpq_res(X2) ) ).
cnf(i_0_234_013,axiom,
( X1 != X2
| removemin_pq_eff(X1,X3) = removemin_pq_eff(X2,X3) ) ).
cnf(i_0_235_014,axiom,
( X1 != X2
| removemin_pq_eff(X3,X1) = removemin_pq_eff(X3,X2) ) ).
cnf(i_0_236_015,axiom,
( X1 != X2
| removemin_pq_res(X1,X3) = removemin_pq_res(X2,X3) ) ).
cnf(i_0_237_016,axiom,
( X1 != X2
| removemin_pq_res(X3,X1) = removemin_pq_res(X3,X2) ) ).
cnf(i_0_238_017,axiom,
( X1 != X2
| remove_cpq(X1,X3) = remove_cpq(X2,X3) ) ).
cnf(i_0_239_018,axiom,
( X1 != X2
| remove_cpq(X3,X1) = remove_cpq(X3,X2) ) ).
cnf(i_0_240_019,axiom,
( X1 != X2
| findmin_pq_res(X1,X3) = findmin_pq_res(X2,X3) ) ).
cnf(i_0_241_020,axiom,
( X1 != X2
| findmin_pq_res(X3,X1) = findmin_pq_res(X3,X2) ) ).
cnf(i_0_242_021,axiom,
( X1 != X2
| findmin_pq_eff(X1,X3) = findmin_pq_eff(X2,X3) ) ).
cnf(i_0_243_022,axiom,
( X1 != X2
| findmin_pq_eff(X3,X1) = findmin_pq_eff(X3,X2) ) ).
cnf(i_0_244_023,axiom,
( X1 != X2
| triple(X1,X3,X4) = triple(X2,X3,X4) ) ).
cnf(i_0_245_024,axiom,
( X1 != X2
| triple(X3,X1,X4) = triple(X3,X2,X4) ) ).
cnf(i_0_246_025,axiom,
( X1 != X2
| triple(X3,X4,X1) = triple(X3,X4,X2) ) ).
cnf(i_0_247_026,axiom,
( X1 != X2
| remove_pq(X1,X3) = remove_pq(X2,X3) ) ).
cnf(i_0_248_027,axiom,
( X1 != X2
| remove_pq(X3,X1) = remove_pq(X3,X2) ) ).
cnf(i_0_249_028,axiom,
( X1 != X2
| insert_slb(X1,X3) = insert_slb(X2,X3) ) ).
cnf(i_0_250_029,axiom,
( X1 != X2
| insert_slb(X3,X1) = insert_slb(X3,X2) ) ).
cnf(i_0_251_030,axiom,
( X1 != X2
| insert_pq(X1,X3) = insert_pq(X2,X3) ) ).
cnf(i_0_252_031,axiom,
( X1 != X2
| insert_pq(X3,X1) = insert_pq(X3,X2) ) ).
cnf(i_0_253_032,axiom,
( X1 != X2
| findmin_cpq_eff(X1) = findmin_cpq_eff(X2) ) ).
cnf(i_0_254_033,axiom,
( X1 != X2
| update_slb(X1,X3) = update_slb(X2,X3) ) ).
cnf(i_0_255_034,axiom,
( X1 != X2
| update_slb(X3,X1) = update_slb(X3,X2) ) ).
cnf(i_0_256_035,axiom,
( X1 != X2
| ~ check_cpq(X1)
| check_cpq(X2) ) ).
cnf(i_0_257_036,axiom,
( X1 != X2
| ~ isnonempty_slb(X1)
| isnonempty_slb(X2) ) ).
cnf(i_0_258_037,axiom,
( X1 != X2
| ~ issmallestelement_pq(X1,X3)
| issmallestelement_pq(X2,X3) ) ).
cnf(i_0_259_038,axiom,
( X1 != X2
| ~ issmallestelement_pq(X3,X1)
| issmallestelement_pq(X3,X2) ) ).
cnf(i_0_260_039,axiom,
( X1 != X2
| ~ pi_sharp_removemin(X1,X3)
| pi_sharp_removemin(X2,X3) ) ).
cnf(i_0_261_040,axiom,
( X1 != X2
| ~ pi_sharp_removemin(X3,X1)
| pi_sharp_removemin(X3,X2) ) ).
cnf(i_0_262_041,axiom,
( X1 != X2
| ~ pi_sharp_find_min(X1,X3)
| pi_sharp_find_min(X2,X3) ) ).
cnf(i_0_263_042,axiom,
( X1 != X2
| ~ pi_sharp_find_min(X3,X1)
| pi_sharp_find_min(X3,X2) ) ).
cnf(i_0_264_043,axiom,
( X1 != X2
| ~ pi_remove(X1,X3)
| pi_remove(X2,X3) ) ).
cnf(i_0_265_044,axiom,
( X1 != X2
| ~ pi_remove(X3,X1)
| pi_remove(X3,X2) ) ).
cnf(i_0_266_045,axiom,
( X1 != X2
| ~ pi_sharp_remove(X1,X3)
| pi_sharp_remove(X2,X3) ) ).
cnf(i_0_267_046,axiom,
( X1 != X2
| ~ pi_sharp_remove(X3,X1)
| pi_sharp_remove(X3,X2) ) ).
cnf(i_0_268_047,axiom,
( X1 != X2
| ~ phi(X1)
| phi(X2) ) ).
cnf(i_0_269_048,axiom,
( X1 != X2
| ~ pi_removemin(X1)
| pi_removemin(X2) ) ).
cnf(i_0_270_049,axiom,
( X1 != X2
| ~ pi_find_min(X1)
| pi_find_min(X2) ) ).
cnf(i_0_271_050,axiom,
( X1 != X2
| ~ isnonempty_pq(X1)
| isnonempty_pq(X2) ) ).
cnf(i_0_272_051,axiom,
( X1 != X2
| ~ less_than(X1,X3)
| less_than(X2,X3) ) ).
cnf(i_0_273_052,axiom,
( X1 != X2
| ~ less_than(X3,X1)
| less_than(X3,X2) ) ).
cnf(i_0_274_053,axiom,
( X1 != X2
| ~ strictly_less_than(X1,X3)
| strictly_less_than(X2,X3) ) ).
cnf(i_0_275_054,axiom,
( X1 != X2
| ~ strictly_less_than(X3,X1)
| strictly_less_than(X3,X2) ) ).
cnf(i_0_276_055,axiom,
( X1 != X2
| ~ contains_slb(X1,X3)
| contains_slb(X2,X3) ) ).
cnf(i_0_277_056,axiom,
( X1 != X2
| ~ contains_slb(X3,X1)
| contains_slb(X3,X2) ) ).
cnf(i_0_278_057,axiom,
( X1 != X2
| ~ pair_in_list(X1,X3,X4)
| pair_in_list(X2,X3,X4) ) ).
cnf(i_0_279_058,axiom,
( X1 != X2
| ~ pair_in_list(X3,X1,X4)
| pair_in_list(X3,X2,X4) ) ).
cnf(i_0_280_059,axiom,
( X1 != X2
| ~ pair_in_list(X3,X4,X1)
| pair_in_list(X3,X4,X2) ) ).
cnf(i_0_281_060,axiom,
( X1 != X2
| ~ contains_pq(X1,X3)
| contains_pq(X2,X3) ) ).
cnf(i_0_282_061,axiom,
( X1 != X2
| ~ contains_pq(X3,X1)
| contains_pq(X3,X2) ) ).
cnf(i_0_283_062,axiom,
( X1 != X2
| ~ contains_cpq(X1,X3)
| contains_cpq(X2,X3) ) ).
cnf(i_0_284_063,axiom,
( X1 != X2
| ~ contains_cpq(X3,X1)
| contains_cpq(X3,X2) ) ).
cnf(i_0_285_064,axiom,
( X1 != X2
| ~ ok(X1)
| ok(X2) ) ).
cnf(i_0_286_065,axiom,
( X1 != X2
| ~ succ_cpq(X1,X3)
| succ_cpq(X2,X3) ) ).
cnf(i_0_287_066,axiom,
( X1 != X2
| ~ succ_cpq(X3,X1)
| succ_cpq(X3,X2) ) ).
cnf(i_0_288,plain,
contains_slb(insert_slb(X1,pair(X2,X3)),X2),
inference(equality_inference,[],[169]) ).
cnf(i_0_289,plain,
contains_pq(insert_pq(X1,X2),X2),
inference(equality_inference,[],[193]) ).
cnf(i_0_290,plain,
pi_sharp_remove(i(triple(esk5_0,create_slb,esk6_0)),esk7_0),
inference(scs_inference,[],[i_0_150,i_0_198]) ).
cnf(i_0_291,plain,
( ~ contains_pq(X1,X2)
| pi_sharp_remove(X1,X2) ),
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_292,plain,
X1 = remove_pq(insert_pq(X1,X2),X2),
inference(scs_inference,[],[i_0_150,i_0_197,i_0_198,i_0_223]) ).
cnf(i_0_293,plain,
issmallestelement_pq(X1,bottom),
inference(scs_inference,[],[i_0_150,i_0_218,i_0_197,i_0_198,i_0_223,i_0_177]) ).
cnf(i_0_294,plain,
less_than(bottom,X1),
inference(rename_variables,[],[i_0_218]) ).
cnf(i_0_295,plain,
( ~ less_than(X1,esk1_2(X2,X1))
| issmallestelement_pq(X2,X1) ),
inference(rename_variables,[],[i_0_177]) ).
cnf(i_0_296,plain,
issmallestelement_pq(create_pq,X1),
inference(scs_inference,[],[i_0_150,i_0_213,i_0_218,i_0_197,i_0_198,i_0_223,i_0_177,i_0_189]) ).
cnf(i_0_297,plain,
~ contains_pq(create_pq,X1),
inference(rename_variables,[],[i_0_213]) ).
cnf(i_0_298,plain,
( contains_pq(X1,esk1_2(X1,X2))
| issmallestelement_pq(X1,X2) ),
inference(rename_variables,[],[i_0_189]) ).
cnf(i_0_299,plain,
pi_remove(triple(esk5_0,create_slb,esk6_0),esk7_0),
inference(scs_inference,[],[i_0_150,i_0_213,i_0_218,i_0_197,i_0_198,i_0_223,i_0_177,i_0_189,i_0_191]) ).
cnf(i_0_300,plain,
( ~ pi_sharp_remove(i(X1),X2)
| pi_remove(X1,X2) ),
inference(rename_variables,[],[i_0_191]) ).
cnf(i_0_301,plain,
pi_sharp_removemin(insert_pq(X1,bottom),bottom),
inference(scs_inference,[],[i_0_150,i_0_289,i_0_213,i_0_218,i_0_197,i_0_198,i_0_223,i_0_177,i_0_189,i_0_191,i_0_185]) ).
cnf(i_0_302,plain,
contains_pq(insert_pq(X1,X2),X2),
inference(rename_variables,[],[i_0_289]) ).
cnf(i_0_303,plain,
( ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2)
| pi_sharp_removemin(X1,X2) ),
inference(rename_variables,[],[i_0_185]) ).
cnf(i_0_304,plain,
pi_sharp_find_min(insert_pq(X1,bottom),bottom),
inference(scs_inference,[],[i_0_150,i_0_289,i_0_302,i_0_213,i_0_218,i_0_197,i_0_198,i_0_223,i_0_177,i_0_189,i_0_191,i_0_185,i_0_186]) ).
cnf(i_0_305,plain,
contains_pq(insert_pq(X1,X2),X2),
inference(rename_variables,[],[i_0_289]) ).
cnf(i_0_306,plain,
( ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2)
| pi_sharp_find_min(X1,X2) ),
inference(rename_variables,[],[i_0_186]) ).
cnf(i_0_307,plain,
remove_pq(insert_pq(update_slb(create_slb,X1),X2),X2) = create_slb,
inference(scs_inference,[],[i_0_150,i_0_289,i_0_302,i_0_213,i_0_218,i_0_197,i_0_219,i_0_198,i_0_223,i_0_177,i_0_189,i_0_191,i_0_185,i_0_186,i_0_224]) ).
cnf(i_0_308,plain,
remove_pq(insert_pq(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_309,plain,
~ contains_pq(remove_pq(insert_pq(create_pq,X1),X1),X2),
inference(scs_inference,[],[i_0_150,i_0_289,i_0_302,i_0_213,i_0_297,i_0_218,i_0_197,i_0_308,i_0_219,i_0_198,i_0_223,i_0_177,i_0_189,i_0_191,i_0_185,i_0_186,i_0_224,i_0_281]) ).
cnf(i_0_310,plain,
remove_pq(insert_pq(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_311,plain,
insert_slb(X1,pair(X2,X3)) != create_slb,
inference(scs_inference,[],[i_0_150,i_0_289,i_0_302,i_0_213,i_0_297,i_0_218,i_0_220,i_0_197,i_0_308,i_0_219,i_0_174,i_0_198,i_0_223,i_0_177,i_0_189,i_0_191,i_0_185,i_0_186,i_0_224,i_0_281,i_0_257]) ).
cnf(i_0_312,plain,
insert_pq(X1,X2) != create_pq,
inference(scs_inference,[],[i_0_150,i_0_289,i_0_302,i_0_213,i_0_297,i_0_218,i_0_220,i_0_221,i_0_209,i_0_197,i_0_308,i_0_219,i_0_174,i_0_198,i_0_223,i_0_177,i_0_189,i_0_191,i_0_185,i_0_186,i_0_224,i_0_281,i_0_257,i_0_271]) ).
cnf(i_0_313,plain,
~ contains_slb(remove_pq(insert_pq(create_slb,X1),X1),X2),
inference(scs_inference,[],[i_0_150,i_0_289,i_0_302,i_0_212,i_0_213,i_0_297,i_0_218,i_0_220,i_0_221,i_0_209,i_0_197,i_0_308,i_0_310,i_0_219,i_0_174,i_0_198,i_0_223,i_0_177,i_0_189,i_0_191,i_0_185,i_0_186,i_0_224,i_0_281,i_0_257,i_0_271,i_0_276]) ).
cnf(i_0_314,plain,
remove_pq(insert_pq(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_315,plain,
~ pair_in_list(remove_pq(insert_pq(create_slb,X1),X1),X2,X3),
inference(scs_inference,[],[i_0_150,i_0_289,i_0_302,i_0_173,i_0_212,i_0_213,i_0_297,i_0_218,i_0_220,i_0_221,i_0_209,i_0_197,i_0_308,i_0_310,i_0_314,i_0_219,i_0_174,i_0_198,i_0_223,i_0_177,i_0_189,i_0_191,i_0_185,i_0_186,i_0_224,i_0_281,i_0_257,i_0_271,i_0_276,i_0_278]) ).
cnf(i_0_316,plain,
remove_pq(insert_pq(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_317,plain,
( less_than(X1,esk7_0)
| ~ issmallestelement_pq(i(triple(esk5_0,create_slb,esk6_0)),X1) ),
inference(scs_inference,[],[i_0_150,i_0_289,i_0_302,i_0_173,i_0_212,i_0_213,i_0_297,i_0_218,i_0_220,i_0_221,i_0_209,i_0_197,i_0_308,i_0_310,i_0_314,i_0_219,i_0_174,i_0_198,i_0_223,i_0_177,i_0_189,i_0_191,i_0_185,i_0_186,i_0_224,i_0_281,i_0_257,i_0_271,i_0_276,i_0_278,i_0_188]) ).
cnf(i_0_318,plain,
( ~ contains_pq(X1,X2)
| less_than(X3,X2)
| ~ issmallestelement_pq(X1,X3) ),
inference(rename_variables,[],[i_0_188]) ).
cnf(i_0_319,plain,
( check_cpq(X1)
| triple(X2,create_slb,X3) != X1 ),
inference(scs_inference,[],[i_0_150,i_0_289,i_0_302,i_0_173,i_0_212,i_0_213,i_0_297,i_0_218,i_0_220,i_0_221,i_0_209,i_0_197,i_0_308,i_0_310,i_0_314,i_0_219,i_0_165,i_0_174,i_0_198,i_0_223,i_0_177,i_0_189,i_0_191,i_0_185,i_0_186,i_0_224,i_0_281,i_0_257,i_0_271,i_0_276,i_0_278,i_0_188,i_0_256]) ).
cnf(i_0_320,plain,
( triple(X1,create_slb,X2) != triple(X3,insert_slb(X4,pair(X5,X5)),X6)
| check_cpq(triple(X3,X4,X6)) ),
inference(scs_inference,[],[i_0_150,i_0_289,i_0_302,i_0_217,i_0_173,i_0_212,i_0_213,i_0_297,i_0_218,i_0_220,i_0_221,i_0_209,i_0_197,i_0_308,i_0_310,i_0_314,i_0_219,i_0_165,i_0_174,i_0_198,i_0_223,i_0_177,i_0_189,i_0_191,i_0_185,i_0_186,i_0_224,i_0_281,i_0_257,i_0_271,i_0_276,i_0_278,i_0_188,i_0_256,i_0_137]) ).
cnf(i_0_321,plain,
( ~ check_cpq(triple(X1,insert_slb(X2,pair(X3,X4)),X5))
| check_cpq(triple(X1,X2,X5))
| ~ less_than(X4,X3) ),
inference(rename_variables,[],[i_0_137]) ).
cnf(i_0_323,plain,
check_cpq(triple(X1,create_slb,X2)),
inference(equality_inference,[],[319]) ).
cnf(i_0_324,plain,
check_cpq(remove_pq(insert_pq(triple(X1,create_slb,X2),X3),X3)),
inference(scs_inference,[],[i_0_292,i_0_319]) ).
cnf(i_0_325,plain,
X1 = remove_pq(insert_pq(X1,X2),X2),
inference(rename_variables,[],[i_0_292]) ).
cnf(i_0_326,plain,
issmallestelement_pq(remove_pq(insert_pq(create_pq,X1),X1),X2),
inference(scs_inference,[],[i_0_292,i_0_309,i_0_319,i_0_189]) ).
cnf(i_0_327,plain,
~ contains_pq(remove_pq(insert_pq(create_pq,X1),X1),X2),
inference(rename_variables,[],[i_0_309]) ).
cnf(i_0_328,plain,
( contains_pq(X1,esk1_2(X1,X2))
| issmallestelement_pq(X1,X2) ),
inference(rename_variables,[],[i_0_189]) ).
cnf(i_0_329,plain,
pi_sharp_remove(insert_pq(X1,X2),X2),
inference(scs_inference,[],[i_0_292,i_0_309,i_0_289,i_0_319,i_0_189,i_0_198]) ).
cnf(i_0_330,plain,
( ~ contains_pq(X1,X2)
| pi_sharp_remove(X1,X2) ),
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_331,plain,
create_slb = remove_pq(insert_pq(update_slb(create_slb,X1),X2),X2),
inference(scs_inference,[],[i_0_292,i_0_309,i_0_307,i_0_289,i_0_319,i_0_189,i_0_198,i_0_223]) ).
cnf(i_0_332,plain,
remove_pq(insert_pq(update_slb(create_slb,X1),X2),X2) = remove_pq(insert_pq(create_slb,X3),X3),
inference(scs_inference,[],[i_0_292,i_0_325,i_0_309,i_0_307,i_0_289,i_0_319,i_0_189,i_0_198,i_0_223,i_0_224]) ).
cnf(i_0_333,plain,
X1 = remove_pq(insert_pq(X1,X2),X2),
inference(rename_variables,[],[i_0_292]) ).
cnf(i_0_334,plain,
check_cpq(remove_pq(insert_pq(remove_pq(insert_pq(triple(X1,create_slb,X2),X3),X3),X4),X4)),
inference(scs_inference,[],[i_0_292,i_0_325,i_0_333,i_0_309,i_0_307,i_0_289,i_0_319,i_0_189,i_0_198,i_0_223,i_0_224,i_0_256]) ).
cnf(i_0_335,plain,
X1 = remove_pq(insert_pq(X1,X2),X2),
inference(rename_variables,[],[i_0_292]) ).
cnf(i_0_336,plain,
~ contains_pq(lookup_slb(insert_slb(X1,pair(X2,create_pq)),X2),X3),
inference(scs_inference,[],[i_0_292,i_0_325,i_0_333,i_0_309,i_0_307,i_0_289,i_0_170,i_0_213,i_0_319,i_0_189,i_0_198,i_0_223,i_0_224,i_0_256,i_0_281]) ).
cnf(i_0_337,plain,
lookup_slb(insert_slb(X1,pair(X2,X3)),X2) = X3,
inference(rename_variables,[],[i_0_170]) ).
cnf(i_0_338,plain,
~ contains_slb(remove_pq(insert_pq(update_slb(create_slb,X1),X2),X2),X3),
inference(scs_inference,[],[i_0_292,i_0_325,i_0_333,i_0_309,i_0_307,i_0_289,i_0_212,i_0_170,i_0_213,i_0_319,i_0_189,i_0_198,i_0_223,i_0_224,i_0_256,i_0_281,i_0_276]) ).
cnf(i_0_339,plain,
~ pair_in_list(remove_pq(insert_pq(update_slb(create_slb,X1),X2),X2),X3,X4),
inference(scs_inference,[],[i_0_292,i_0_325,i_0_333,i_0_309,i_0_307,i_0_289,i_0_173,i_0_212,i_0_170,i_0_213,i_0_319,i_0_189,i_0_198,i_0_223,i_0_224,i_0_256,i_0_281,i_0_276,i_0_278]) ).
cnf(i_0_340,plain,
( ~ issmallestelement_pq(i(triple(esk5_0,create_slb,esk6_0)),esk7_0)
| pi_sharp_removemin(i(triple(esk5_0,create_slb,esk6_0)),esk7_0) ),
inference(scs_inference,[],[i_0_150,i_0_292,i_0_325,i_0_333,i_0_309,i_0_307,i_0_289,i_0_173,i_0_212,i_0_170,i_0_213,i_0_319,i_0_189,i_0_198,i_0_223,i_0_224,i_0_256,i_0_281,i_0_276,i_0_278,i_0_185]) ).
cnf(i_0_341,plain,
( ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2)
| pi_sharp_removemin(X1,X2) ),
inference(rename_variables,[],[i_0_185]) ).
cnf(i_0_342,plain,
( pi_sharp_removemin(i(triple(esk5_0,create_slb,esk6_0)),esk7_0)
| ~ issmallestelement_pq(lookup_slb(insert_slb(X1,pair(X2,i(triple(esk5_0,create_slb,esk6_0)))),X2),esk7_0) ),
inference(scs_inference,[],[i_0_150,i_0_292,i_0_325,i_0_333,i_0_309,i_0_307,i_0_289,i_0_173,i_0_212,i_0_170,i_0_337,i_0_213,i_0_319,i_0_189,i_0_198,i_0_223,i_0_224,i_0_256,i_0_281,i_0_276,i_0_278,i_0_185,i_0_258]) ).
cnf(i_0_343,plain,
lookup_slb(insert_slb(X1,pair(X2,X3)),X2) = X3,
inference(rename_variables,[],[i_0_170]) ).
cnf(i_0_344,plain,
( pi_sharp_removemin(i(triple(esk5_0,create_slb,esk6_0)),esk7_0)
| ~ issmallestelement_pq(i(triple(esk5_0,create_slb,esk6_0)),lookup_slb(insert_slb(X1,pair(X2,esk7_0)),X2)) ),
inference(scs_inference,[],[i_0_150,i_0_292,i_0_325,i_0_333,i_0_309,i_0_307,i_0_289,i_0_173,i_0_212,i_0_170,i_0_337,i_0_343,i_0_213,i_0_319,i_0_189,i_0_198,i_0_223,i_0_224,i_0_256,i_0_281,i_0_276,i_0_278,i_0_185,i_0_258,i_0_259]) ).
cnf(i_0_345,plain,
lookup_slb(insert_slb(X1,pair(X2,X3)),X2) = X3,
inference(rename_variables,[],[i_0_170]) ).
cnf(i_0_346,plain,
( ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2)
| pi_sharp_find_min(X1,X2) ),
inference(rename_variables,[],[i_0_186]) ).
cnf(i_0_347,plain,
issmallestelement_pq(X1,bottom),
inference(rename_variables,[],[i_0_293]) ).
cnf(i_0_349,plain,
issmallestelement_pq(lookup_slb(insert_slb(X1,pair(X2,create_pq)),X2),X3),
inference(scs_inference,[],[i_0_336,i_0_189]) ).
cnf(i_0_350,plain,
~ contains_pq(lookup_slb(insert_slb(X1,pair(X2,create_pq)),X2),X3),
inference(rename_variables,[],[i_0_336]) ).
cnf(i_0_351,plain,
( contains_pq(X1,esk1_2(X1,X2))
| issmallestelement_pq(X1,X2) ),
inference(rename_variables,[],[i_0_189]) ).
cnf(i_0_352,plain,
remove_pq(insert_pq(create_slb,X1),X1) = remove_pq(insert_pq(update_slb(create_slb,X2),X3),X3),
inference(scs_inference,[],[i_0_336,i_0_332,i_0_189,i_0_223]) ).
cnf(i_0_353,plain,
remove_pq(insert_pq(update_slb(create_slb,X1),X2),X2) = remove_pq(insert_pq(update_slb(create_slb,X3),X4),X4),
inference(scs_inference,[],[i_0_336,i_0_332,i_0_331,i_0_307,i_0_189,i_0_223,i_0_224]) ).
cnf(i_0_354,plain,
~ contains_pq(remove_slb(insert_slb(lookup_slb(insert_slb(X1,pair(X2,create_pq)),X2),pair(X3,X4)),X3),X5),
inference(scs_inference,[],[i_0_336,i_0_350,i_0_332,i_0_331,i_0_307,i_0_171,i_0_189,i_0_223,i_0_224,i_0_281]) ).
cnf(i_0_355,plain,
remove_slb(insert_slb(X1,pair(X2,X3)),X2) = X1,
inference(rename_variables,[],[i_0_171]) ).
cnf(i_0_356,plain,
( ~ issmallestelement_pq(i(triple(esk5_0,create_slb,esk6_0)),esk7_0)
| pi_sharp_find_min(i(triple(esk5_0,create_slb,esk6_0)),esk7_0) ),
inference(scs_inference,[],[i_0_150,i_0_336,i_0_350,i_0_332,i_0_331,i_0_307,i_0_171,i_0_189,i_0_223,i_0_224,i_0_281,i_0_186]) ).
cnf(i_0_357,plain,
( ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2)
| pi_sharp_find_min(X1,X2) ),
inference(rename_variables,[],[i_0_186]) ).
cnf(i_0_358,plain,
( pi_sharp_find_min(i(triple(esk5_0,create_slb,esk6_0)),esk7_0)
| ~ issmallestelement_pq(remove_slb(insert_slb(i(triple(esk5_0,create_slb,esk6_0)),pair(X1,X2)),X1),esk7_0) ),
inference(scs_inference,[],[i_0_150,i_0_336,i_0_350,i_0_332,i_0_331,i_0_307,i_0_171,i_0_355,i_0_189,i_0_223,i_0_224,i_0_281,i_0_186,i_0_258]) ).
cnf(i_0_359,plain,
remove_slb(insert_slb(X1,pair(X2,X3)),X2) = X1,
inference(rename_variables,[],[i_0_171]) ).
cnf(i_0_360,plain,
( pi_sharp_find_min(i(triple(esk5_0,create_slb,esk6_0)),esk7_0)
| ~ issmallestelement_pq(i(triple(esk5_0,create_slb,esk6_0)),remove_slb(insert_slb(esk7_0,pair(X1,X2)),X1)) ),
inference(scs_inference,[],[i_0_150,i_0_336,i_0_350,i_0_332,i_0_331,i_0_307,i_0_171,i_0_355,i_0_359,i_0_189,i_0_223,i_0_224,i_0_281,i_0_186,i_0_258,i_0_259]) ).
cnf(i_0_361,plain,
remove_slb(insert_slb(X1,pair(X2,X3)),X2) = X1,
inference(rename_variables,[],[i_0_171]) ).
cnf(i_0_362,plain,
( ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2)
| pi_sharp_removemin(X1,X2) ),
inference(rename_variables,[],[i_0_185]) ).
cnf(i_0_363,plain,
issmallestelement_pq(X1,bottom),
inference(rename_variables,[],[i_0_293]) ).
cnf(i_0_364,plain,
X1 = remove_pq(insert_pq(X1,X2),X2),
inference(rename_variables,[],[i_0_292]) ).
cnf(i_0_365,plain,
~ contains_slb(remove_pq(insert_pq(create_slb,X1),X1),X2),
inference(rename_variables,[],[i_0_313]) ).
cnf(i_0_366,plain,
~ pair_in_list(remove_pq(insert_pq(create_slb,X1),X1),X2,X3),
inference(rename_variables,[],[i_0_315]) ).
cnf(i_0_368,plain,
triple(X1,create_slb,bad) = findmin_cpq_eff(triple(X1,create_slb,X2)),
inference(scs_inference,[],[i_0_158,i_0_223]) ).
cnf(i_0_369,plain,
update_slb(create_slb,X1) = remove_pq(insert_pq(create_slb,X2),X2),
inference(scs_inference,[],[i_0_292,i_0_332,i_0_158,i_0_223,i_0_224]) ).
cnf(i_0_370,plain,
remove_pq(insert_pq(update_slb(create_slb,X1),X2),X2) = remove_pq(insert_pq(create_slb,X3),X3),
inference(rename_variables,[],[i_0_332]) ).
cnf(i_0_371,plain,
X1 = remove_pq(insert_pq(X1,X2),X2),
inference(rename_variables,[],[i_0_292]) ).
cnf(i_0_372,plain,
$false,
inference(scs_inference,[],[i_0_150,i_0_292,i_0_332,i_0_213,i_0_158,i_0_166,i_0_223,i_0_224,i_0_281]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWV367+1 : TPTP v9.2.1. Released v3.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.13/0.32 % Computer : n013.cluster.edu
% 0.13/0.32 % Model : x86_64 x86_64
% 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32 % Memory : 8042.1875MB
% 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32 % CPULimit : 300
% 0.13/0.32 % WCLimit : 300
% 0.13/0.32 % DateTime : Tue May 5 05:05:41 EDT 2026
% 0.13/0.32 % CPUTime :
% 0.13/0.34 % start to proof: theBenchmark
% 0.35/1.61 % Version : CSE_E---1.7
% 0.35/1.61 % Problem : theBenchmark.p
% 0.35/1.61 % SZS status Theorem for theBenchmark.p
% 0.35/1.61 % SZS output start CNFRefutation
% See solution above
% 0.55/1.85 % Total time : 1.272s
%------------------------------------------------------------------------------