%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWV371+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 : n007.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.34s 1.61s
% Output : CNFRefutation 0.54s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_107)
% Comments :
%------------------------------------------------------------------------------
fof(l7_co,conjecture,
! [X1,X2,X3] :
( phi(findmin_cpq_eff(triple(X1,X2,X3)))
=> pi_sharp_find_min(i(triple(X1,X2,X3)),findmin_cpq_res(triple(X1,X2,X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l7_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(l7_lX,lemma,
! [X1,X2,X3] :
( phi(findmin_cpq_eff(triple(X1,X2,X3)))
=> issmallestelement_pq(i(triple(X1,X2,X3)),findmin_cpq_res(triple(X1,X2,X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l7_lX) ).
fof(l7_l8,lemma,
! [X1,X2,X3] :
( phi(findmin_cpq_eff(triple(X1,X2,X3)))
=> contains_pq(i(triple(X1,X2,X3)),findmin_cpq_res(triple(X1,X2,X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l7_l8) ).
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_64,negated_conjecture,
~ ! [X1,X2,X3] :
( phi(findmin_cpq_eff(triple(X1,X2,X3)))
=> pi_sharp_find_min(i(triple(X1,X2,X3)),findmin_cpq_res(triple(X1,X2,X3))) ),
inference(assume_negation,[status(cth)],[l7_co]) ).
fof(i_0_65,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_66,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_67,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_68,plain,
! [X1,X2] : ~ ok(triple(X1,X2,bad)),
inference(fof_simplification,[status(thm)],[ax40]) ).
fof(i_0_69,plain,
! [X1,X2,X3] :
( ~ ok(triple(X1,X2,X3))
=> X3 = bad ),
inference(fof_simplification,[status(thm)],[ax41]) ).
fof(i_0_70,plain,
! [X262,X263] :
( ~ succ_cpq(X262,X263)
| succ_cpq(X262,removemin_cpq_eff(X263)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax35])]) ).
fof(i_0_71,plain,
! [X317] : removemin_cpq_eff(X317) = remove_cpq(findmin_cpq_eff(X317),findmin_cpq_res(X317)),
inference(variable_rename,[status(thm)],[ax52]) ).
fof(i_0_72,plain,
! [X1,X2] : ~ pair_in_list(create_slb,X1,X2),
inference(fof_simplification,[status(thm)],[ax22]) ).
fof(i_0_73,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_74,plain,
! [X1] : ~ contains_slb(create_slb,X1),
inference(fof_simplification,[status(thm)],[ax20]) ).
fof(i_0_75,plain,
! [X1] : ~ contains_pq(create_pq,X1),
inference(fof_simplification,[status(thm)],[ax8]) ).
fof(i_0_76,lemma,
! [X349,X350,X351] :
( ~ phi(findmin_cpq_eff(triple(X349,X350,X351)))
| issmallestelement_pq(i(triple(X349,X350,X351)),findmin_cpq_res(triple(X349,X350,X351))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[l7_lX])]) ).
fof(i_0_77,lemma,
! [X346,X347,X348] :
( ~ phi(findmin_cpq_eff(triple(X346,X347,X348)))
| contains_pq(i(triple(X346,X347,X348)),findmin_cpq_res(triple(X346,X347,X348))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[l7_l8])]) ).
fof(i_0_78,negated_conjecture,
( phi(findmin_cpq_eff(triple(esk5_0,esk6_0,esk7_0)))
& ~ pi_sharp_find_min(i(triple(esk5_0,esk6_0,esk7_0)),findmin_cpq_res(triple(esk5_0,esk6_0,esk7_0))) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_64])])]) ).
fof(i_0_79,plain,
! [X266,X267,X268,X269,X270] :
( ( ~ check_cpq(triple(X266,insert_slb(X267,pair(X269,X270)),X268))
| check_cpq(triple(X266,X267,X268))
| ~ less_than(X270,X269) )
& ( ~ check_cpq(triple(X266,X267,X268))
| check_cpq(triple(X266,insert_slb(X267,pair(X269,X270)),X268))
| ~ less_than(X270,X269) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax37])])]) ).
fof(i_0_80,plain,
! [X321,X322,X323,X324,X325] : i(triple(X321,insert_slb(X322,pair(X324,X325)),X323)) = insert_pq(i(triple(X321,X322,X323)),X324),
inference(variable_rename,[status(thm)],[ax55]) ).
fof(i_0_81,plain,
! [X271,X272,X273,X274,X275] :
( ~ strictly_less_than(X274,X275)
| ~ check_cpq(triple(X271,insert_slb(X272,pair(X274,X275)),X273)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_65])]) ).
fof(i_0_82,plain,
! [X309,X310,X311] :
( X310 = create_slb
| ~ contains_slb(X310,findmin_pqp_res(X309))
| ~ less_than(lookup_slb(X310,findmin_pqp_res(X309)),findmin_pqp_res(X309))
| findmin_cpq_eff(triple(X309,X310,X311)) = triple(X309,update_slb(X310,findmin_pqp_res(X309)),X311) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[ax49])])]) ).
fof(i_0_83,plain,
! [X306,X307,X308] :
( X307 = create_slb
| ~ contains_slb(X307,findmin_pqp_res(X306))
| ~ strictly_less_than(findmin_pqp_res(X306),lookup_slb(X307,findmin_pqp_res(X306)))
| findmin_cpq_eff(triple(X306,X307,X308)) = triple(X306,update_slb(X307,findmin_pqp_res(X306)),bad) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[ax48])])]) ).
fof(i_0_84,plain,
! [X293,X294,X295,X296] :
( ~ contains_slb(X294,X296)
| ~ less_than(lookup_slb(X294,X296),X296)
| remove_cpq(triple(X293,X294,X295),X296) = triple(remove_pqp(X293,X296),remove_slb(X294,X296),X295) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax44])]) ).
fof(i_0_85,plain,
! [X297,X298,X299,X300] :
( ~ contains_slb(X298,X300)
| ~ strictly_less_than(X300,lookup_slb(X298,X300))
| remove_cpq(triple(X297,X298,X299),X300) = triple(remove_pqp(X297,X300),remove_slb(X298,X300),bad) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax45])]) ).
fof(i_0_86,plain,
! [X285,X286,X287,X288] : insert_cpq(triple(X285,X286,X287),X288) = triple(insert_pqp(X285,X288),insert_slb(X286,pair(X288,bottom)),X287),
inference(variable_rename,[status(thm)],[ax42]) ).
fof(i_0_87,plain,
! [X225,X226,X227,X228,X229] :
( ( X226 = X227
| pair_in_list(X225,X227,X229)
| ~ pair_in_list(insert_slb(X225,pair(X226,X228)),X227,X229) )
& ( X228 = X229
| pair_in_list(X225,X227,X229)
| ~ pair_in_list(insert_slb(X225,pair(X226,X228)),X227,X229) )
& ( ~ pair_in_list(X225,X227,X229)
| pair_in_list(insert_slb(X225,pair(X226,X228)),X227,X229) )
& ( X226 != X227
| X228 != X229
| pair_in_list(insert_slb(X225,pair(X226,X228)),X227,X229) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax23])])]) ).
fof(i_0_88,plain,
! [X303,X304,X305] :
( X304 = create_slb
| contains_slb(X304,findmin_pqp_res(X303))
| findmin_cpq_eff(triple(X303,X304,X305)) = triple(X303,update_slb(X304,findmin_pqp_res(X303)),bad) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[i_0_66])])]) ).
fof(i_0_89,plain,
! [X276,X277,X278,X279] :
( ( ~ contains_cpq(triple(X276,X277,X278),X279)
| contains_slb(X277,X279) )
& ( ~ contains_slb(X277,X279)
| contains_cpq(triple(X276,X277,X278),X279) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax39])]) ).
fof(i_0_90,plain,
! [X289,X290,X291,X292] :
( contains_slb(X290,X292)
| remove_cpq(triple(X289,X290,X291),X292) = triple(X289,X290,bad) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_67])]) ).
fof(i_0_91,plain,
! [X233,X234,X235,X236] :
( X234 = X235
| ~ contains_slb(X233,X235)
| remove_slb(insert_slb(X233,pair(X234,X236)),X235) = insert_slb(remove_slb(X233,X235),pair(X234,X236)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax25])]) ).
fof(i_0_92,plain,
! [X245,X246,X247,X248] :
( ~ strictly_less_than(X248,X247)
| update_slb(insert_slb(X245,pair(X246,X248)),X247) = insert_slb(update_slb(X245,X247),pair(X246,X247)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax29])]) ).
fof(i_0_93,plain,
! [X249,X250,X251,X252] :
( ~ less_than(X251,X252)
| update_slb(insert_slb(X249,pair(X250,X252)),X251) = insert_slb(update_slb(X249,X251),pair(X250,X252)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax30])]) ).
fof(i_0_94,plain,
! [X280,X281] : ~ ok(triple(X280,X281,bad)),
inference(variable_rename,[status(thm)],[i_0_68]) ).
fof(i_0_95,plain,
! [X219,X220,X221,X222] :
( ( ~ contains_slb(insert_slb(X219,pair(X220,X222)),X221)
| contains_slb(X219,X221)
| X220 = X221 )
& ( ~ contains_slb(X219,X221)
| contains_slb(insert_slb(X219,pair(X220,X222)),X221) )
& ( X220 != X221
| contains_slb(insert_slb(X219,pair(X220,X222)),X221) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax21])])]) ).
fof(i_0_96,plain,
! [X301,X302] : findmin_cpq_eff(triple(X301,create_slb,X302)) = triple(X301,create_slb,bad),
inference(variable_rename,[status(thm)],[ax46]) ).
fof(i_0_97,plain,
! [X240,X241,X242,X243] :
( X241 = X242
| ~ contains_slb(X240,X242)
| lookup_slb(insert_slb(X240,pair(X241,X243)),X242) = lookup_slb(X240,X242) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax27])]) ).
fof(i_0_98,plain,
! [X314,X315,X316] :
( X315 = create_slb
| findmin_cpq_res(triple(X314,X315,X316)) = findmin_pqp_res(X314) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[ax51])])]) ).
fof(i_0_99,plain,
! [X282,X283,X284] :
( ok(triple(X282,X283,X284))
| X284 = bad ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_69])]) ).
fof(i_0_100,plain,
! [X264,X265] : check_cpq(triple(X264,create_slb,X265)),
inference(variable_rename,[status(thm)],[ax36]) ).
fof(i_0_101,plain,
! [X319,X320] : i(triple(X319,create_slb,X320)) = create_pq,
inference(variable_rename,[status(thm)],[ax54]) ).
fof(i_0_102,plain,
! [X312,X313] : findmin_cpq_res(triple(X312,create_slb,X313)) = bottom,
inference(variable_rename,[status(thm)],[ax50]) ).
fof(i_0_103,plain,
! [X201,X202,X203] :
( ~ contains_pq(X201,X203)
| X202 = X203
| remove_pq(insert_pq(X201,X202),X203) = insert_pq(remove_pq(X201,X203),X202) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax12])]) ).
fof(i_0_104,plain,
! [X237,X238,X239] : lookup_slb(insert_slb(X237,pair(X238,X239)),X238) = X239,
inference(variable_rename,[status(thm)],[ax26]) ).
fof(i_0_105,plain,
! [X230,X231,X232] : remove_slb(insert_slb(X230,pair(X231,X232)),X231) = X230,
inference(variable_rename,[status(thm)],[ax24]) ).
cnf(i_0_106,plain,
( succ_cpq(X1,removemin_cpq_eff(X2))
| ~ succ_cpq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_70]) ).
cnf(i_0_107,plain,
removemin_cpq_eff(X1) = remove_cpq(findmin_cpq_eff(X1),findmin_cpq_res(X1)),
inference(split_conjunct,[status(thm)],[i_0_71]) ).
fof(i_0_108,plain,
! [X223,X224] : ~ pair_in_list(create_slb,X223,X224),
inference(variable_rename,[status(thm)],[i_0_72]) ).
fof(i_0_109,plain,
! [X215,X216,X217] : isnonempty_slb(insert_slb(X215,pair(X216,X217))),
inference(variable_rename,[status(thm)],[ax19]) ).
fof(i_0_110,plain,
! [X190,X191,X192] :
( ( ~ contains_pq(insert_pq(X190,X191),X192)
| contains_pq(X190,X192)
| X191 = X192 )
& ( ~ contains_pq(X190,X192)
| contains_pq(insert_pq(X190,X191),X192) )
& ( X191 != X192
| contains_pq(insert_pq(X190,X191),X192) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax9])])]) ).
fof(i_0_111,plain,
! [X212,X213,X214] : insert_pq(insert_pq(X212,X213),X214) = insert_pq(insert_pq(X212,X214),X213),
inference(variable_rename,[status(thm)],[ax17]) ).
fof(i_0_112,plain,
! [X193,X194,X195,X196,X197] :
( ( ~ issmallestelement_pq(X193,X194)
| ~ contains_pq(X193,X195)
| less_than(X194,X195) )
& ( contains_pq(X196,esk1_2(X196,X197))
| issmallestelement_pq(X196,X197) )
& ( ~ less_than(X197,esk1_2(X196,X197))
| issmallestelement_pq(X196,X197) ) ),
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_113,plain,
! [X208,X209] :
( ~ contains_pq(X208,X209)
| ~ issmallestelement_pq(X208,X209)
| removemin_pq_eff(X208,X209) = remove_pq(X208,X209) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax15])]) ).
fof(i_0_114,plain,
! [X257,X258,X259] :
( ~ succ_cpq(X257,X258)
| succ_cpq(X257,remove_cpq(X258,X259)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax33])]) ).
fof(i_0_115,plain,
! [X254,X255,X256] :
( ~ succ_cpq(X254,X255)
| succ_cpq(X254,insert_cpq(X255,X256)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax32])]) ).
fof(i_0_116,plain,
! [X210,X211] :
( ~ contains_pq(X210,X211)
| ~ issmallestelement_pq(X210,X211)
| removemin_pq_res(X210,X211) = X211 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax16])]) ).
fof(i_0_117,plain,
! [X206,X207] :
( ~ contains_pq(X206,X207)
| ~ issmallestelement_pq(X206,X207)
| findmin_pq_res(X206,X207) = X207 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax14])]) ).
fof(i_0_118,plain,
! [X204,X205] :
( ~ contains_pq(X204,X205)
| ~ issmallestelement_pq(X204,X205)
| findmin_pq_eff(X204,X205) = X204 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax13])]) ).
fof(i_0_119,plain,
! [X336,X337] :
( ( contains_pq(X336,X337)
| ~ pi_sharp_removemin(X336,X337) )
& ( issmallestelement_pq(X336,X337)
| ~ pi_sharp_removemin(X336,X337) )
& ( ~ contains_pq(X336,X337)
| ~ issmallestelement_pq(X336,X337)
| pi_sharp_removemin(X336,X337) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax60])])]) ).
fof(i_0_120,plain,
! [X330,X331] :
( ( contains_pq(X330,X331)
| ~ pi_sharp_find_min(X330,X331) )
& ( issmallestelement_pq(X330,X331)
| ~ pi_sharp_find_min(X330,X331) )
& ( ~ contains_pq(X330,X331)
| ~ issmallestelement_pq(X330,X331)
| pi_sharp_find_min(X330,X331) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax58])])]) ).
fof(i_0_121,plain,
! [X178,X179,X180] :
( ~ less_than(X178,X179)
| ~ less_than(X179,X180)
| less_than(X178,X180) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitivity])]) ).
fof(i_0_122,plain,
! [X184,X185] :
( ( less_than(X184,X185)
| ~ strictly_less_than(X184,X185) )
& ( ~ less_than(X185,X184)
| ~ strictly_less_than(X184,X185) )
& ( ~ less_than(X184,X185)
| less_than(X185,X184)
| strictly_less_than(X184,X185) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_73])])]) ).
fof(i_0_123,plain,
! [X328,X329] :
( ( ~ pi_remove(X328,X329)
| pi_sharp_remove(i(X328),X329) )
& ( ~ pi_sharp_remove(i(X328),X329)
| pi_remove(X328,X329) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax57])]) ).
fof(i_0_124,plain,
! [X260,X261] :
( ~ succ_cpq(X260,X261)
| succ_cpq(X260,findmin_cpq_eff(X261)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax34])]) ).
fof(i_0_125,plain,
! [X342,X344,X345] :
( ( succ_cpq(X342,esk4_1(X342))
| ~ phi(X342) )
& ( ok(esk4_1(X342))
| ~ phi(X342) )
& ( check_cpq(esk4_1(X342))
| ~ phi(X342) )
& ( ~ succ_cpq(X344,X345)
| ~ ok(X345)
| ~ check_cpq(X345)
| phi(X344) ) ),
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_126,plain,
! [X199,X200] : remove_pq(insert_pq(X199,X200),X200) = X199,
inference(variable_rename,[status(thm)],[ax11]) ).
fof(i_0_127,plain,
! [X326,X327] :
( ( ~ pi_sharp_remove(X326,X327)
| contains_pq(X326,X327) )
& ( ~ contains_pq(X326,X327)
| pi_sharp_remove(X326,X327) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax56])]) ).
fof(i_0_128,plain,
! [X338,X340,X341] :
( ( ~ pi_removemin(X338)
| pi_sharp_find_min(i(X338),esk3_1(X338)) )
& ( ~ pi_sharp_find_min(i(X340),X341)
| pi_removemin(X340) ) ),
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_129,plain,
! [X332,X334,X335] :
( ( ~ pi_find_min(X332)
| pi_sharp_find_min(i(X332),esk2_1(X332)) )
& ( ~ pi_sharp_find_min(i(X334),X335)
| pi_find_min(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)],[ax59])])])])]) ).
fof(i_0_130,plain,
! [X187,X188] : isnonempty_pq(insert_pq(X187,X188)),
inference(variable_rename,[status(thm)],[ax7]) ).
fof(i_0_131,plain,
! [X181,X182] :
( less_than(X181,X182)
| less_than(X182,X181) ),
inference(variable_rename,[status(thm)],[totality]) ).
fof(i_0_132,plain,
! [X218] : ~ contains_slb(create_slb,X218),
inference(variable_rename,[status(thm)],[i_0_74]) ).
fof(i_0_133,plain,
! [X189] : ~ contains_pq(create_pq,X189),
inference(variable_rename,[status(thm)],[i_0_75]) ).
fof(i_0_134,plain,
! [X253] : succ_cpq(X253,X253),
inference(variable_rename,[status(thm)],[ax31]) ).
fof(i_0_135,plain,
! [X183] : less_than(X183,X183),
inference(variable_rename,[status(thm)],[reflexivity]) ).
fof(i_0_136,plain,
! [X186] : less_than(bottom,X186),
inference(variable_rename,[status(thm)],[bottom_smallest]) ).
fof(i_0_137,plain,
! [X244] : update_slb(create_slb,X244) = create_slb,
inference(variable_rename,[status(thm)],[ax28]) ).
fof(i_0_138,plain,
~ isnonempty_slb(create_slb),
inference(fof_simplification,[status(thm)],[ax18]) ).
fof(i_0_139,plain,
~ isnonempty_pq(create_pq),
inference(fof_simplification,[status(thm)],[ax6]) ).
cnf(i_0_140,lemma,
( issmallestelement_pq(i(triple(X1,X2,X3)),findmin_cpq_res(triple(X1,X2,X3)))
| ~ phi(findmin_cpq_eff(triple(X1,X2,X3))) ),
inference(split_conjunct,[status(thm)],[i_0_76]),
[final] ).
cnf(i_0_141,lemma,
( contains_pq(i(triple(X1,X2,X3)),findmin_cpq_res(triple(X1,X2,X3)))
| ~ phi(findmin_cpq_eff(triple(X1,X2,X3))) ),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_142,negated_conjecture,
~ pi_sharp_find_min(i(triple(esk5_0,esk6_0,esk7_0)),findmin_cpq_res(triple(esk5_0,esk6_0,esk7_0))),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_143,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_79]),
[final] ).
cnf(i_0_144,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_80]),
[final] ).
cnf(i_0_145,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_79]),
[final] ).
cnf(i_0_146,plain,
( ~ strictly_less_than(X1,X2)
| ~ check_cpq(triple(X3,insert_slb(X4,pair(X1,X2)),X5)) ),
inference(split_conjunct,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_147,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_82]),
[final] ).
cnf(i_0_148,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_83]),
[final] ).
cnf(i_0_149,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_84]),
[final] ).
cnf(i_0_150,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_85]),
[final] ).
cnf(i_0_151,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_86]),
[final] ).
cnf(i_0_152,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_87]),
[final] ).
cnf(i_0_153,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_87]),
[final] ).
cnf(i_0_154,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_88]),
[final] ).
cnf(i_0_155,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_87]),
[final] ).
cnf(i_0_156,negated_conjecture,
phi(findmin_cpq_eff(triple(esk5_0,esk6_0,esk7_0))),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_157,plain,
( contains_slb(X2,X4)
| ~ contains_cpq(triple(X1,X2,X3),X4) ),
inference(split_conjunct,[status(thm)],[i_0_89]),
[final] ).
cnf(i_0_158,plain,
( contains_slb(X1,X2)
| remove_cpq(triple(X3,X1,X4),X2) = triple(X3,X1,bad) ),
inference(split_conjunct,[status(thm)],[i_0_90]),
[final] ).
cnf(i_0_159,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_91]),
[final] ).
cnf(i_0_160,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_92]),
[final] ).
cnf(i_0_161,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_93]),
[final] ).
cnf(i_0_162,plain,
~ ok(triple(X1,X2,bad)),
inference(split_conjunct,[status(thm)],[i_0_94]),
[final] ).
cnf(i_0_163,plain,
( contains_slb(X1,X4)
| X2 = X4
| ~ contains_slb(insert_slb(X1,pair(X2,X3)),X4) ),
inference(split_conjunct,[status(thm)],[i_0_95]),
[final] ).
cnf(i_0_164,plain,
findmin_cpq_eff(triple(X1,create_slb,X2)) = triple(X1,create_slb,bad),
inference(split_conjunct,[status(thm)],[i_0_96]),
[final] ).
cnf(i_0_165,plain,
( contains_cpq(triple(X3,X1,X4),X2)
| ~ contains_slb(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_89]),
[final] ).
cnf(i_0_166,plain,
( pair_in_list(insert_slb(X5,pair(X1,X3)),X2,X4)
| X1 != X2
| X3 != X4 ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_167,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_97]),
[final] ).
cnf(i_0_168,plain,
( X1 = create_slb
| findmin_cpq_res(triple(X2,X1,X3)) = findmin_pqp_res(X2) ),
inference(split_conjunct,[status(thm)],[i_0_98]),
[final] ).
cnf(i_0_169,plain,
( contains_slb(insert_slb(X1,pair(X3,X4)),X2)
| ~ contains_slb(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_95]),
[final] ).
cnf(i_0_170,plain,
( ok(triple(X1,X2,X3))
| X3 = bad ),
inference(split_conjunct,[status(thm)],[i_0_99]),
[final] ).
cnf(i_0_171,plain,
check_cpq(triple(X1,create_slb,X2)),
inference(split_conjunct,[status(thm)],[i_0_100]),
[final] ).
cnf(i_0_172,plain,
i(triple(X1,create_slb,X2)) = create_pq,
inference(split_conjunct,[status(thm)],[i_0_101]),
[final] ).
cnf(i_0_173,plain,
findmin_cpq_res(triple(X1,create_slb,X2)) = bottom,
inference(split_conjunct,[status(thm)],[i_0_102]),
[final] ).
cnf(i_0_174,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_103]),
[final] ).
cnf(i_0_175,plain,
( contains_slb(insert_slb(X3,pair(X1,X4)),X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_95]),
[final] ).
cnf(i_0_176,plain,
lookup_slb(insert_slb(X1,pair(X2,X3)),X2) = X3,
inference(split_conjunct,[status(thm)],[i_0_104]),
[final] ).
cnf(i_0_177,plain,
remove_slb(insert_slb(X1,pair(X2,X3)),X2) = X1,
inference(split_conjunct,[status(thm)],[i_0_105]),
[final] ).
cnf(i_0_178,plain,
( succ_cpq(X1,remove_cpq(findmin_cpq_eff(X2),findmin_cpq_res(X2)))
| ~ succ_cpq(X1,X2) ),
inference(rw,[status(thm)],[i_0_106,c_0_107]),
[final] ).
cnf(i_0_179,plain,
~ pair_in_list(create_slb,X1,X2),
inference(split_conjunct,[status(thm)],[i_0_108]),
[final] ).
cnf(i_0_180,plain,
isnonempty_slb(insert_slb(X1,pair(X2,X3))),
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_181,plain,
( contains_pq(X1,X3)
| X2 = X3
| ~ contains_pq(insert_pq(X1,X2),X3) ),
inference(split_conjunct,[status(thm)],[i_0_110]),
[final] ).
cnf(i_0_182,plain,
insert_pq(insert_pq(X1,X2),X3) = insert_pq(insert_pq(X1,X3),X2),
inference(split_conjunct,[status(thm)],[i_0_111]),
[final] ).
cnf(i_0_183,plain,
( issmallestelement_pq(X2,X1)
| ~ less_than(X1,esk1_2(X2,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_112]),
[final] ).
cnf(i_0_184,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_113]),
[final] ).
cnf(i_0_185,plain,
( contains_pq(insert_pq(X1,X3),X2)
| ~ contains_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_110]),
[final] ).
cnf(i_0_186,plain,
( succ_cpq(X1,remove_cpq(X2,X3))
| ~ succ_cpq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_114]),
[final] ).
cnf(i_0_187,plain,
( succ_cpq(X1,insert_cpq(X2,X3))
| ~ succ_cpq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_115]),
[final] ).
cnf(i_0_188,plain,
( removemin_pq_res(X1,X2) = X2
| ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_116]),
[final] ).
cnf(i_0_189,plain,
( findmin_pq_res(X1,X2) = X2
| ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_117]),
[final] ).
cnf(i_0_190,plain,
( findmin_pq_eff(X1,X2) = X1
| ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_118]),
[final] ).
cnf(i_0_191,plain,
( pi_sharp_removemin(X1,X2)
| ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_119]),
[final] ).
cnf(i_0_192,plain,
( pi_sharp_find_min(X1,X2)
| ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_120]),
[final] ).
cnf(i_0_193,plain,
( less_than(X1,X3)
| ~ less_than(X1,X2)
| ~ less_than(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_121]),
[final] ).
cnf(i_0_194,plain,
( less_than(X2,X3)
| ~ issmallestelement_pq(X1,X2)
| ~ contains_pq(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_112]),
[final] ).
cnf(i_0_195,plain,
( contains_pq(X1,esk1_2(X1,X2))
| issmallestelement_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_112]),
[final] ).
cnf(i_0_196,plain,
( less_than(X2,X1)
| strictly_less_than(X1,X2)
| ~ less_than(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_122]),
[final] ).
cnf(i_0_197,plain,
( pi_remove(X1,X2)
| ~ pi_sharp_remove(i(X1),X2) ),
inference(split_conjunct,[status(thm)],[i_0_123]),
[final] ).
cnf(i_0_198,plain,
( ~ less_than(X1,X2)
| ~ strictly_less_than(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_122]),
[final] ).
cnf(i_0_199,plain,
( contains_pq(insert_pq(X3,X1),X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_110]),
[final] ).
cnf(i_0_200,plain,
( pi_sharp_remove(i(X1),X2)
| ~ pi_remove(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_123]),
[final] ).
cnf(i_0_201,plain,
( succ_cpq(X1,findmin_cpq_eff(X2))
| ~ succ_cpq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_124]),
[final] ).
cnf(i_0_202,plain,
( phi(X1)
| ~ succ_cpq(X1,X2)
| ~ ok(X2)
| ~ check_cpq(X2) ),
inference(split_conjunct,[status(thm)],[i_0_125]),
[final] ).
cnf(i_0_203,plain,
remove_pq(insert_pq(X1,X2),X2) = X1,
inference(split_conjunct,[status(thm)],[i_0_126]),
[final] ).
cnf(i_0_204,plain,
( pi_sharp_remove(X1,X2)
| ~ contains_pq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_127]),
[final] ).
cnf(i_0_205,plain,
( issmallestelement_pq(X1,X2)
| ~ pi_sharp_removemin(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_119]),
[final] ).
cnf(i_0_206,plain,
( issmallestelement_pq(X1,X2)
| ~ pi_sharp_find_min(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_120]),
[final] ).
cnf(i_0_207,plain,
( contains_pq(X1,X2)
| ~ pi_sharp_removemin(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_119]),
[final] ).
cnf(i_0_208,plain,
( contains_pq(X1,X2)
| ~ pi_sharp_find_min(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_120]),
[final] ).
cnf(i_0_209,plain,
( contains_pq(X1,X2)
| ~ pi_sharp_remove(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_127]),
[final] ).
cnf(i_0_210,plain,
( less_than(X1,X2)
| ~ strictly_less_than(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_122]),
[final] ).
cnf(i_0_211,plain,
( pi_removemin(X1)
| ~ pi_sharp_find_min(i(X1),X2) ),
inference(split_conjunct,[status(thm)],[i_0_128]),
[final] ).
cnf(i_0_212,plain,
( pi_find_min(X1)
| ~ pi_sharp_find_min(i(X1),X2) ),
inference(split_conjunct,[status(thm)],[i_0_129]),
[final] ).
cnf(i_0_213,plain,
( pi_sharp_find_min(i(X1),esk3_1(X1))
| ~ pi_removemin(X1) ),
inference(split_conjunct,[status(thm)],[i_0_128]),
[final] ).
cnf(i_0_214,plain,
( pi_sharp_find_min(i(X1),esk2_1(X1))
| ~ pi_find_min(X1) ),
inference(split_conjunct,[status(thm)],[i_0_129]),
[final] ).
cnf(i_0_215,plain,
isnonempty_pq(insert_pq(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_130]),
[final] ).
cnf(i_0_216,plain,
( less_than(X1,X2)
| less_than(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_131]),
[final] ).
cnf(i_0_217,plain,
( succ_cpq(X1,esk4_1(X1))
| ~ phi(X1) ),
inference(split_conjunct,[status(thm)],[i_0_125]),
[final] ).
cnf(i_0_218,plain,
~ contains_slb(create_slb,X1),
inference(split_conjunct,[status(thm)],[i_0_132]),
[final] ).
cnf(i_0_219,plain,
~ contains_pq(create_pq,X1),
inference(split_conjunct,[status(thm)],[i_0_133]),
[final] ).
cnf(i_0_220,plain,
( ok(esk4_1(X1))
| ~ phi(X1) ),
inference(split_conjunct,[status(thm)],[i_0_125]),
[final] ).
cnf(i_0_221,plain,
( check_cpq(esk4_1(X1))
| ~ phi(X1) ),
inference(split_conjunct,[status(thm)],[i_0_125]),
[final] ).
cnf(i_0_222,plain,
succ_cpq(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_134]),
[final] ).
cnf(i_0_223,plain,
less_than(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_135]),
[final] ).
cnf(i_0_224,plain,
less_than(bottom,X1),
inference(split_conjunct,[status(thm)],[i_0_136]),
[final] ).
cnf(i_0_225,plain,
update_slb(create_slb,X1) = create_slb,
inference(split_conjunct,[status(thm)],[i_0_137]),
[final] ).
cnf(i_0_226,plain,
~ isnonempty_slb(create_slb),
inference(split_conjunct,[status(thm)],[i_0_138]),
[final] ).
cnf(i_0_227,plain,
~ isnonempty_pq(create_pq),
inference(split_conjunct,[status(thm)],[i_0_139]),
[final] ).
cnf(i_0_228,axiom,
X1 = X1 ).
cnf(i_0_229,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_230,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_231,axiom,
( X1 != X2
| i(X1) = i(X2) ) ).
cnf(i_0_232,axiom,
( X1 != X2
| lookup_slb(X1,X3) = lookup_slb(X2,X3) ) ).
cnf(i_0_233,axiom,
( X1 != X2
| lookup_slb(X3,X1) = lookup_slb(X3,X2) ) ).
cnf(i_0_234,axiom,
( X1 != X2
| remove_cpq(X1,X3) = remove_cpq(X2,X3) ) ).
cnf(i_0_235,axiom,
( X1 != X2
| remove_cpq(X3,X1) = remove_cpq(X3,X2) ) ).
cnf(i_0_236,axiom,
( X1 != X2
| remove_slb(X1,X3) = remove_slb(X2,X3) ) ).
cnf(i_0_237,axiom,
( X1 != X2
| remove_slb(X3,X1) = remove_slb(X3,X2) ) ).
cnf(i_0_238,axiom,
( X1 != X2
| insert_cpq(X1,X3) = insert_cpq(X2,X3) ) ).
cnf(i_0_239,axiom,
( X1 != X2
| insert_cpq(X3,X1) = insert_cpq(X3,X2) ) ).
cnf(i_0_240,axiom,
( X1 != X2
| remove_pq(X1,X3) = remove_pq(X2,X3) ) ).
cnf(i_0_241,axiom,
( X1 != X2
| remove_pq(X3,X1) = remove_pq(X3,X2) ) ).
cnf(i_0_242,axiom,
( X1 != X2
| removemin_pq_eff(X1,X3) = removemin_pq_eff(X2,X3) ) ).
cnf(i_0_243,axiom,
( X1 != X2
| removemin_pq_eff(X3,X1) = removemin_pq_eff(X3,X2) ) ).
cnf(i_0_244,axiom,
( X1 != X2
| removemin_pq_res(X1,X3) = removemin_pq_res(X2,X3) ) ).
cnf(i_0_245,axiom,
( X1 != X2
| removemin_pq_res(X3,X1) = removemin_pq_res(X3,X2) ) ).
cnf(i_0_246,axiom,
( X1 != X2
| triple(X1,X3,X4) = triple(X2,X3,X4) ) ).
cnf(i_0_247,axiom,
( X1 != X2
| triple(X3,X1,X4) = triple(X3,X2,X4) ) ).
cnf(i_0_248,axiom,
( X1 != X2
| triple(X3,X4,X1) = triple(X3,X4,X2) ) ).
cnf(i_0_249,axiom,
( X1 != X2
| findmin_pq_res(X1,X3) = findmin_pq_res(X2,X3) ) ).
cnf(i_0_250,axiom,
( X1 != X2
| findmin_pq_res(X3,X1) = findmin_pq_res(X3,X2) ) ).
cnf(i_0_251,axiom,
( X1 != X2
| findmin_pq_eff(X1,X3) = findmin_pq_eff(X2,X3) ) ).
cnf(i_0_252,axiom,
( X1 != X2
| findmin_pq_eff(X3,X1) = findmin_pq_eff(X3,X2) ) ).
cnf(i_0_253,axiom,
( X1 != X2
| findmin_cpq_res(X1) = findmin_cpq_res(X2) ) ).
cnf(i_0_254,axiom,
( X1 != X2
| findmin_cpq_eff(X1) = findmin_cpq_eff(X2) ) ).
cnf(i_0_255,axiom,
( X1 != X2
| insert_slb(X1,X3) = insert_slb(X2,X3) ) ).
cnf(i_0_256,axiom,
( X1 != X2
| insert_slb(X3,X1) = insert_slb(X3,X2) ) ).
cnf(i_0_257,axiom,
( X1 != X2
| insert_pq(X1,X3) = insert_pq(X2,X3) ) ).
cnf(i_0_258,axiom,
( X1 != X2
| insert_pq(X3,X1) = insert_pq(X3,X2) ) ).
cnf(i_0_259,axiom,
( X1 != X2
| update_slb(X1,X3) = update_slb(X2,X3) ) ).
cnf(i_0_260,axiom,
( X1 != X2
| update_slb(X3,X1) = update_slb(X3,X2) ) ).
cnf(i_0_261,axiom,
( X1 != X2
| findmin_pqp_res(X1) = findmin_pqp_res(X2) ) ).
cnf(i_0_262,axiom,
( X1 != X2
| ~ issmallestelement_pq(X1,X3)
| issmallestelement_pq(X2,X3) ) ).
cnf(i_0_263,axiom,
( X1 != X2
| ~ issmallestelement_pq(X3,X1)
| issmallestelement_pq(X3,X2) ) ).
cnf(i_0_264,axiom,
( X1 != X2
| ~ contains_cpq(X1,X3)
| contains_cpq(X2,X3) ) ).
cnf(i_0_265,axiom,
( X1 != X2
| ~ contains_cpq(X3,X1)
| contains_cpq(X3,X2) ) ).
cnf(i_0_266,axiom,
( X1 != X2
| ~ ok(X1)
| ok(X2) ) ).
cnf(i_0_267,axiom,
( X1 != X2
| ~ succ_cpq(X1,X3)
| succ_cpq(X2,X3) ) ).
cnf(i_0_268,axiom,
( X1 != X2
| ~ succ_cpq(X3,X1)
| succ_cpq(X3,X2) ) ).
cnf(i_0_269,axiom,
( X1 != X2
| ~ isnonempty_slb(X1)
| isnonempty_slb(X2) ) ).
cnf(i_0_270,axiom,
( X1 != X2
| ~ pi_sharp_removemin(X1,X3)
| pi_sharp_removemin(X2,X3) ) ).
cnf(i_0_271,axiom,
( X1 != X2
| ~ pi_sharp_removemin(X3,X1)
| pi_sharp_removemin(X3,X2) ) ).
cnf(i_0_272,axiom,
( X1 != X2
| ~ pi_remove(X1,X3)
| pi_remove(X2,X3) ) ).
cnf(i_0_273,axiom,
( X1 != X2
| ~ pi_remove(X3,X1)
| pi_remove(X3,X2) ) ).
cnf(i_0_274,axiom,
( X1 != X2
| ~ pi_sharp_remove(X1,X3)
| pi_sharp_remove(X2,X3) ) ).
cnf(i_0_275,axiom,
( X1 != X2
| ~ pi_sharp_remove(X3,X1)
| pi_sharp_remove(X3,X2) ) ).
cnf(i_0_276,axiom,
( X1 != X2
| ~ pi_removemin(X1)
| pi_removemin(X2) ) ).
cnf(i_0_277,axiom,
( X1 != X2
| ~ pi_find_min(X1)
| pi_find_min(X2) ) ).
cnf(i_0_278,axiom,
( X1 != X2
| ~ isnonempty_pq(X1)
| isnonempty_pq(X2) ) ).
cnf(i_0_279,axiom,
( X1 != X2
| ~ phi(X1)
| phi(X2) ) ).
cnf(i_0_280,axiom,
( X1 != X2
| ~ contains_pq(X1,X3)
| contains_pq(X2,X3) ) ).
cnf(i_0_281,axiom,
( X1 != X2
| ~ contains_pq(X3,X1)
| contains_pq(X3,X2) ) ).
cnf(i_0_282,axiom,
( X1 != X2
| ~ pi_sharp_find_min(X1,X3)
| pi_sharp_find_min(X2,X3) ) ).
cnf(i_0_283,axiom,
( X1 != X2
| ~ pi_sharp_find_min(X3,X1)
| pi_sharp_find_min(X3,X2) ) ).
cnf(i_0_284,axiom,
( X1 != X2
| ~ check_cpq(X1)
| check_cpq(X2) ) ).
cnf(i_0_285,axiom,
( X1 != X2
| ~ less_than(X1,X3)
| less_than(X2,X3) ) ).
cnf(i_0_286,axiom,
( X1 != X2
| ~ less_than(X3,X1)
| less_than(X3,X2) ) ).
cnf(i_0_287,axiom,
( X1 != X2
| ~ strictly_less_than(X1,X3)
| strictly_less_than(X2,X3) ) ).
cnf(i_0_288,axiom,
( X1 != X2
| ~ strictly_less_than(X3,X1)
| strictly_less_than(X3,X2) ) ).
cnf(i_0_289,axiom,
( X1 != X2
| ~ contains_slb(X1,X3)
| contains_slb(X2,X3) ) ).
cnf(i_0_290,axiom,
( X1 != X2
| ~ contains_slb(X3,X1)
| contains_slb(X3,X2) ) ).
cnf(i_0_291,axiom,
( X1 != X2
| ~ pair_in_list(X1,X3,X4)
| pair_in_list(X2,X3,X4) ) ).
cnf(i_0_292,axiom,
( X1 != X2
| ~ pair_in_list(X3,X1,X4)
| pair_in_list(X3,X2,X4) ) ).
cnf(i_0_293,axiom,
( X1 != X2
| ~ pair_in_list(X3,X4,X1)
| pair_in_list(X3,X4,X2) ) ).
cnf(i_0_228_001,axiom,
X1 = X1 ).
cnf(i_0_229_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_230_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_231_004,axiom,
( X1 != X2
| i(X1) = i(X2) ) ).
cnf(i_0_232_005,axiom,
( X1 != X2
| lookup_slb(X1,X3) = lookup_slb(X2,X3) ) ).
cnf(i_0_233_006,axiom,
( X1 != X2
| lookup_slb(X3,X1) = lookup_slb(X3,X2) ) ).
cnf(i_0_234_007,axiom,
( X1 != X2
| remove_cpq(X1,X3) = remove_cpq(X2,X3) ) ).
cnf(i_0_235_008,axiom,
( X1 != X2
| remove_cpq(X3,X1) = remove_cpq(X3,X2) ) ).
cnf(i_0_236_009,axiom,
( X1 != X2
| remove_slb(X1,X3) = remove_slb(X2,X3) ) ).
cnf(i_0_237_010,axiom,
( X1 != X2
| remove_slb(X3,X1) = remove_slb(X3,X2) ) ).
cnf(i_0_238_011,axiom,
( X1 != X2
| insert_cpq(X1,X3) = insert_cpq(X2,X3) ) ).
cnf(i_0_239_012,axiom,
( X1 != X2
| insert_cpq(X3,X1) = insert_cpq(X3,X2) ) ).
cnf(i_0_240_013,axiom,
( X1 != X2
| remove_pq(X1,X3) = remove_pq(X2,X3) ) ).
cnf(i_0_241_014,axiom,
( X1 != X2
| remove_pq(X3,X1) = remove_pq(X3,X2) ) ).
cnf(i_0_242_015,axiom,
( X1 != X2
| removemin_pq_eff(X1,X3) = removemin_pq_eff(X2,X3) ) ).
cnf(i_0_243_016,axiom,
( X1 != X2
| removemin_pq_eff(X3,X1) = removemin_pq_eff(X3,X2) ) ).
cnf(i_0_244_017,axiom,
( X1 != X2
| removemin_pq_res(X1,X3) = removemin_pq_res(X2,X3) ) ).
cnf(i_0_245_018,axiom,
( X1 != X2
| removemin_pq_res(X3,X1) = removemin_pq_res(X3,X2) ) ).
cnf(i_0_246_019,axiom,
( X1 != X2
| triple(X1,X3,X4) = triple(X2,X3,X4) ) ).
cnf(i_0_247_020,axiom,
( X1 != X2
| triple(X3,X1,X4) = triple(X3,X2,X4) ) ).
cnf(i_0_248_021,axiom,
( X1 != X2
| triple(X3,X4,X1) = triple(X3,X4,X2) ) ).
cnf(i_0_249_022,axiom,
( X1 != X2
| findmin_pq_res(X1,X3) = findmin_pq_res(X2,X3) ) ).
cnf(i_0_250_023,axiom,
( X1 != X2
| findmin_pq_res(X3,X1) = findmin_pq_res(X3,X2) ) ).
cnf(i_0_251_024,axiom,
( X1 != X2
| findmin_pq_eff(X1,X3) = findmin_pq_eff(X2,X3) ) ).
cnf(i_0_252_025,axiom,
( X1 != X2
| findmin_pq_eff(X3,X1) = findmin_pq_eff(X3,X2) ) ).
cnf(i_0_253_026,axiom,
( X1 != X2
| findmin_cpq_res(X1) = findmin_cpq_res(X2) ) ).
cnf(i_0_254_027,axiom,
( X1 != X2
| findmin_cpq_eff(X1) = findmin_cpq_eff(X2) ) ).
cnf(i_0_255_028,axiom,
( X1 != X2
| insert_slb(X1,X3) = insert_slb(X2,X3) ) ).
cnf(i_0_256_029,axiom,
( X1 != X2
| insert_slb(X3,X1) = insert_slb(X3,X2) ) ).
cnf(i_0_257_030,axiom,
( X1 != X2
| insert_pq(X1,X3) = insert_pq(X2,X3) ) ).
cnf(i_0_258_031,axiom,
( X1 != X2
| insert_pq(X3,X1) = insert_pq(X3,X2) ) ).
cnf(i_0_259_032,axiom,
( X1 != X2
| update_slb(X1,X3) = update_slb(X2,X3) ) ).
cnf(i_0_260_033,axiom,
( X1 != X2
| update_slb(X3,X1) = update_slb(X3,X2) ) ).
cnf(i_0_261_034,axiom,
( X1 != X2
| findmin_pqp_res(X1) = findmin_pqp_res(X2) ) ).
cnf(i_0_262_035,axiom,
( X1 != X2
| ~ issmallestelement_pq(X1,X3)
| issmallestelement_pq(X2,X3) ) ).
cnf(i_0_263_036,axiom,
( X1 != X2
| ~ issmallestelement_pq(X3,X1)
| issmallestelement_pq(X3,X2) ) ).
cnf(i_0_264_037,axiom,
( X1 != X2
| ~ contains_cpq(X1,X3)
| contains_cpq(X2,X3) ) ).
cnf(i_0_265_038,axiom,
( X1 != X2
| ~ contains_cpq(X3,X1)
| contains_cpq(X3,X2) ) ).
cnf(i_0_266_039,axiom,
( X1 != X2
| ~ ok(X1)
| ok(X2) ) ).
cnf(i_0_267_040,axiom,
( X1 != X2
| ~ succ_cpq(X1,X3)
| succ_cpq(X2,X3) ) ).
cnf(i_0_268_041,axiom,
( X1 != X2
| ~ succ_cpq(X3,X1)
| succ_cpq(X3,X2) ) ).
cnf(i_0_269_042,axiom,
( X1 != X2
| ~ isnonempty_slb(X1)
| isnonempty_slb(X2) ) ).
cnf(i_0_270_043,axiom,
( X1 != X2
| ~ pi_sharp_removemin(X1,X3)
| pi_sharp_removemin(X2,X3) ) ).
cnf(i_0_271_044,axiom,
( X1 != X2
| ~ pi_sharp_removemin(X3,X1)
| pi_sharp_removemin(X3,X2) ) ).
cnf(i_0_272_045,axiom,
( X1 != X2
| ~ pi_remove(X1,X3)
| pi_remove(X2,X3) ) ).
cnf(i_0_273_046,axiom,
( X1 != X2
| ~ pi_remove(X3,X1)
| pi_remove(X3,X2) ) ).
cnf(i_0_274_047,axiom,
( X1 != X2
| ~ pi_sharp_remove(X1,X3)
| pi_sharp_remove(X2,X3) ) ).
cnf(i_0_275_048,axiom,
( X1 != X2
| ~ pi_sharp_remove(X3,X1)
| pi_sharp_remove(X3,X2) ) ).
cnf(i_0_276_049,axiom,
( X1 != X2
| ~ pi_removemin(X1)
| pi_removemin(X2) ) ).
cnf(i_0_277_050,axiom,
( X1 != X2
| ~ pi_find_min(X1)
| pi_find_min(X2) ) ).
cnf(i_0_278_051,axiom,
( X1 != X2
| ~ isnonempty_pq(X1)
| isnonempty_pq(X2) ) ).
cnf(i_0_279_052,axiom,
( X1 != X2
| ~ phi(X1)
| phi(X2) ) ).
cnf(i_0_280_053,axiom,
( X1 != X2
| ~ contains_pq(X1,X3)
| contains_pq(X2,X3) ) ).
cnf(i_0_281_054,axiom,
( X1 != X2
| ~ contains_pq(X3,X1)
| contains_pq(X3,X2) ) ).
cnf(i_0_282_055,axiom,
( X1 != X2
| ~ pi_sharp_find_min(X1,X3)
| pi_sharp_find_min(X2,X3) ) ).
cnf(i_0_283_056,axiom,
( X1 != X2
| ~ pi_sharp_find_min(X3,X1)
| pi_sharp_find_min(X3,X2) ) ).
cnf(i_0_284_057,axiom,
( X1 != X2
| ~ check_cpq(X1)
| check_cpq(X2) ) ).
cnf(i_0_285_058,axiom,
( X1 != X2
| ~ less_than(X1,X3)
| less_than(X2,X3) ) ).
cnf(i_0_286_059,axiom,
( X1 != X2
| ~ less_than(X3,X1)
| less_than(X3,X2) ) ).
cnf(i_0_287_060,axiom,
( X1 != X2
| ~ strictly_less_than(X1,X3)
| strictly_less_than(X2,X3) ) ).
cnf(i_0_288_061,axiom,
( X1 != X2
| ~ strictly_less_than(X3,X1)
| strictly_less_than(X3,X2) ) ).
cnf(i_0_289_062,axiom,
( X1 != X2
| ~ contains_slb(X1,X3)
| contains_slb(X2,X3) ) ).
cnf(i_0_290_063,axiom,
( X1 != X2
| ~ contains_slb(X3,X1)
| contains_slb(X3,X2) ) ).
cnf(i_0_291_064,axiom,
( X1 != X2
| ~ pair_in_list(X1,X3,X4)
| pair_in_list(X2,X3,X4) ) ).
cnf(i_0_292_065,axiom,
( X1 != X2
| ~ pair_in_list(X3,X1,X4)
| pair_in_list(X3,X2,X4) ) ).
cnf(i_0_293_066,axiom,
( X1 != X2
| ~ pair_in_list(X3,X4,X1)
| pair_in_list(X3,X4,X2) ) ).
cnf(i_0_294,plain,
contains_slb(insert_slb(X1,pair(X2,X3)),X2),
inference(equality_inference,[],[175]) ).
cnf(i_0_295,plain,
contains_pq(insert_pq(X1,X2),X2),
inference(equality_inference,[],[199]) ).
cnf(i_0_296,plain,
issmallestelement_pq(i(triple(esk5_0,esk6_0,esk7_0)),findmin_cpq_res(triple(esk5_0,esk6_0,esk7_0))),
inference(scs_inference,[],[i_0_156,i_0_140]) ).
cnf(i_0_297,plain,
( ~ phi(findmin_cpq_eff(triple(X1,X2,X3)))
| issmallestelement_pq(i(triple(X1,X2,X3)),findmin_cpq_res(triple(X1,X2,X3))) ),
inference(rename_variables,[],[i_0_140]) ).
cnf(i_0_298,plain,
contains_pq(i(triple(esk5_0,esk6_0,esk7_0)),findmin_cpq_res(triple(esk5_0,esk6_0,esk7_0))),
inference(scs_inference,[],[i_0_156,i_0_140,i_0_141]) ).
cnf(i_0_299,plain,
( ~ phi(findmin_cpq_eff(triple(X1,X2,X3)))
| contains_pq(i(triple(X1,X2,X3)),findmin_cpq_res(triple(X1,X2,X3))) ),
inference(rename_variables,[],[i_0_141]) ).
cnf(i_0_300,plain,
issmallestelement_pq(X1,bottom),
inference(scs_inference,[],[i_0_156,i_0_224,i_0_140,i_0_141,i_0_183]) ).
cnf(i_0_301,plain,
less_than(bottom,X1),
inference(rename_variables,[],[i_0_224]) ).
cnf(i_0_302,plain,
( ~ less_than(X1,esk1_2(X2,X1))
| issmallestelement_pq(X2,X1) ),
inference(rename_variables,[],[i_0_183]) ).
cnf(i_0_303,plain,
issmallestelement_pq(create_pq,X1),
inference(scs_inference,[],[i_0_156,i_0_219,i_0_224,i_0_140,i_0_141,i_0_183,i_0_195]) ).
cnf(i_0_304,plain,
~ contains_pq(create_pq,X1),
inference(rename_variables,[],[i_0_219]) ).
cnf(i_0_305,plain,
( contains_pq(X1,esk1_2(X1,X2))
| issmallestelement_pq(X1,X2) ),
inference(rename_variables,[],[i_0_195]) ).
cnf(i_0_306,plain,
pi_sharp_remove(insert_pq(X1,X2),X2),
inference(scs_inference,[],[i_0_156,i_0_295,i_0_219,i_0_224,i_0_140,i_0_141,i_0_183,i_0_195,i_0_204]) ).
cnf(i_0_307,plain,
( ~ contains_pq(X1,X2)
| pi_sharp_remove(X1,X2) ),
inference(rename_variables,[],[i_0_204]) ).
cnf(i_0_308,plain,
X1 = remove_pq(insert_pq(X1,X2),X2),
inference(scs_inference,[],[i_0_156,i_0_295,i_0_219,i_0_203,i_0_224,i_0_140,i_0_141,i_0_183,i_0_195,i_0_204,i_0_229]) ).
cnf(i_0_309,plain,
pi_sharp_find_min(insert_pq(X1,bottom),bottom),
inference(scs_inference,[],[i_0_156,i_0_295,i_0_219,i_0_203,i_0_224,i_0_140,i_0_141,i_0_183,i_0_195,i_0_204,i_0_229,i_0_192]) ).
cnf(i_0_310,plain,
contains_pq(insert_pq(X1,X2),X2),
inference(rename_variables,[],[i_0_295]) ).
cnf(i_0_311,plain,
( ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2)
| pi_sharp_find_min(X1,X2) ),
inference(rename_variables,[],[i_0_192]) ).
cnf(i_0_312,plain,
phi(remove_pq(insert_pq(findmin_cpq_eff(triple(esk5_0,esk6_0,esk7_0)),X1),X1)),
inference(scs_inference,[],[i_0_156,i_0_295,i_0_219,i_0_203,i_0_224,i_0_140,i_0_141,i_0_183,i_0_195,i_0_204,i_0_229,i_0_192,i_0_279]) ).
cnf(i_0_313,plain,
pi_sharp_removemin(insert_pq(X1,bottom),bottom),
inference(scs_inference,[],[i_0_156,i_0_295,i_0_310,i_0_219,i_0_203,i_0_224,i_0_140,i_0_141,i_0_183,i_0_195,i_0_204,i_0_229,i_0_192,i_0_279,i_0_191]) ).
cnf(i_0_314,plain,
contains_pq(insert_pq(X1,X2),X2),
inference(rename_variables,[],[i_0_295]) ).
cnf(i_0_315,plain,
( ~ contains_pq(X1,X2)
| ~ issmallestelement_pq(X1,X2)
| pi_sharp_removemin(X1,X2) ),
inference(rename_variables,[],[i_0_191]) ).
cnf(i_0_316,plain,
lookup_slb(insert_slb(X1,pair(X2,update_slb(create_slb,X3))),X2) = create_slb,
inference(scs_inference,[],[i_0_156,i_0_295,i_0_310,i_0_219,i_0_203,i_0_225,i_0_176,i_0_224,i_0_140,i_0_141,i_0_183,i_0_195,i_0_204,i_0_229,i_0_192,i_0_279,i_0_191,i_0_230]) ).
cnf(i_0_317,plain,
lookup_slb(insert_slb(X1,pair(X2,X3)),X2) = X3,
inference(rename_variables,[],[i_0_176]) ).
cnf(i_0_318,plain,
~ contains_pq(lookup_slb(insert_slb(X1,pair(X2,create_pq)),X2),X3),
inference(scs_inference,[],[i_0_156,i_0_295,i_0_310,i_0_219,i_0_304,i_0_203,i_0_225,i_0_176,i_0_317,i_0_224,i_0_140,i_0_141,i_0_183,i_0_195,i_0_204,i_0_229,i_0_192,i_0_279,i_0_191,i_0_230,i_0_280]) ).
cnf(i_0_319,plain,
lookup_slb(insert_slb(X1,pair(X2,X3)),X2) = X3,
inference(rename_variables,[],[i_0_176]) ).
cnf(i_0_320,plain,
insert_slb(X1,pair(X2,X3)) != create_slb,
inference(scs_inference,[],[i_0_156,i_0_295,i_0_310,i_0_219,i_0_304,i_0_203,i_0_225,i_0_176,i_0_317,i_0_224,i_0_226,i_0_180,i_0_140,i_0_141,i_0_183,i_0_195,i_0_204,i_0_229,i_0_192,i_0_279,i_0_191,i_0_230,i_0_280,i_0_269]) ).
cnf(i_0_321,plain,
insert_pq(X1,X2) != create_pq,
inference(scs_inference,[],[i_0_156,i_0_295,i_0_310,i_0_219,i_0_304,i_0_203,i_0_225,i_0_176,i_0_317,i_0_224,i_0_226,i_0_227,i_0_215,i_0_180,i_0_140,i_0_141,i_0_183,i_0_195,i_0_204,i_0_229,i_0_192,i_0_279,i_0_191,i_0_230,i_0_280,i_0_269,i_0_278]) ).
cnf(i_0_322,plain,
~ contains_slb(update_slb(create_slb,X1),X2),
inference(scs_inference,[],[i_0_156,i_0_295,i_0_310,i_0_219,i_0_304,i_0_203,i_0_225,i_0_176,i_0_317,i_0_218,i_0_224,i_0_226,i_0_227,i_0_215,i_0_180,i_0_140,i_0_141,i_0_183,i_0_195,i_0_204,i_0_229,i_0_192,i_0_279,i_0_191,i_0_230,i_0_280,i_0_269,i_0_278,i_0_289]) ).
cnf(i_0_323,plain,
~ pair_in_list(update_slb(create_slb,X1),X2,X3),
inference(scs_inference,[],[i_0_156,i_0_295,i_0_310,i_0_219,i_0_304,i_0_203,i_0_225,i_0_176,i_0_317,i_0_179,i_0_218,i_0_224,i_0_226,i_0_227,i_0_215,i_0_180,i_0_140,i_0_141,i_0_183,i_0_195,i_0_204,i_0_229,i_0_192,i_0_279,i_0_191,i_0_230,i_0_280,i_0_269,i_0_278,i_0_289,i_0_291]) ).
cnf(i_0_324,plain,
( check_cpq(X1)
| triple(X2,create_slb,X3) != X1 ),
inference(scs_inference,[],[i_0_156,i_0_295,i_0_310,i_0_219,i_0_304,i_0_203,i_0_225,i_0_176,i_0_317,i_0_179,i_0_218,i_0_224,i_0_226,i_0_227,i_0_215,i_0_171,i_0_180,i_0_140,i_0_141,i_0_183,i_0_195,i_0_204,i_0_229,i_0_192,i_0_279,i_0_191,i_0_230,i_0_280,i_0_269,i_0_278,i_0_289,i_0_291,i_0_284]) ).
cnf(i_0_325,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_156,i_0_295,i_0_310,i_0_219,i_0_304,i_0_203,i_0_225,i_0_176,i_0_317,i_0_223,i_0_179,i_0_218,i_0_224,i_0_226,i_0_227,i_0_215,i_0_171,i_0_180,i_0_140,i_0_141,i_0_183,i_0_195,i_0_204,i_0_229,i_0_192,i_0_279,i_0_191,i_0_230,i_0_280,i_0_269,i_0_278,i_0_289,i_0_291,i_0_284,i_0_143]) ).
cnf(i_0_326,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_143]) ).
cnf(i_0_327,plain,
( ~ strictly_less_than(X1,X1)
| triple(X2,create_slb,X3) != triple(X4,insert_slb(X5,pair(X1,X1)),X6) ),
inference(scs_inference,[],[i_0_156,i_0_295,i_0_310,i_0_219,i_0_304,i_0_203,i_0_225,i_0_176,i_0_317,i_0_223,i_0_179,i_0_218,i_0_224,i_0_226,i_0_227,i_0_215,i_0_171,i_0_180,i_0_140,i_0_141,i_0_183,i_0_195,i_0_204,i_0_229,i_0_192,i_0_279,i_0_191,i_0_230,i_0_280,i_0_269,i_0_278,i_0_289,i_0_291,i_0_284,i_0_143,i_0_146]) ).
cnf(i_0_328,plain,
( ~ check_cpq(triple(X1,insert_slb(X2,pair(X3,X4)),X5))
| ~ strictly_less_than(X3,X4) ),
inference(rename_variables,[],[i_0_146]) ).
cnf(i_0_330,plain,
check_cpq(triple(X1,create_slb,X2)),
inference(equality_inference,[],[324]) ).
cnf(i_0_331,plain,
check_cpq(remove_pq(insert_pq(triple(X1,create_slb,X2),X3),X3)),
inference(scs_inference,[],[i_0_308,i_0_324]) ).
cnf(i_0_332,plain,
X1 = remove_pq(insert_pq(X1,X2),X2),
inference(rename_variables,[],[i_0_308]) ).
cnf(i_0_333,plain,
issmallestelement_pq(lookup_slb(insert_slb(X1,pair(X2,create_pq)),X2),X3),
inference(scs_inference,[],[i_0_308,i_0_318,i_0_324,i_0_195]) ).
cnf(i_0_334,plain,
~ contains_pq(lookup_slb(insert_slb(X1,pair(X2,create_pq)),X2),X3),
inference(rename_variables,[],[i_0_318]) ).
cnf(i_0_335,plain,
( contains_pq(X1,esk1_2(X1,X2))
| issmallestelement_pq(X1,X2) ),
inference(rename_variables,[],[i_0_195]) ).
cnf(i_0_336,plain,
pi_sharp_remove(i(triple(esk5_0,esk6_0,esk7_0)),findmin_cpq_res(triple(esk5_0,esk6_0,esk7_0))),
inference(scs_inference,[],[i_0_298,i_0_308,i_0_318,i_0_324,i_0_195,i_0_204]) ).
cnf(i_0_337,plain,
( ~ contains_pq(X1,X2)
| pi_sharp_remove(X1,X2) ),
inference(rename_variables,[],[i_0_204]) ).
cnf(i_0_338,plain,
create_slb = lookup_slb(insert_slb(X1,pair(X2,update_slb(create_slb,X3))),X2),
inference(scs_inference,[],[i_0_298,i_0_308,i_0_318,i_0_316,i_0_324,i_0_195,i_0_204,i_0_229]) ).
cnf(i_0_339,plain,
~ pi_sharp_find_min(remove_slb(insert_slb(i(triple(esk5_0,esk6_0,esk7_0)),pair(X1,X2)),X1),findmin_cpq_res(triple(esk5_0,esk6_0,esk7_0))),
inference(scs_inference,[],[i_0_142,i_0_298,i_0_308,i_0_318,i_0_316,i_0_177,i_0_324,i_0_195,i_0_204,i_0_229,i_0_282]) ).
cnf(i_0_340,plain,
remove_slb(insert_slb(X1,pair(X2,X3)),X2) = X1,
inference(rename_variables,[],[i_0_177]) ).
cnf(i_0_341,plain,
~ pi_sharp_find_min(i(triple(esk5_0,esk6_0,esk7_0)),remove_slb(insert_slb(findmin_cpq_res(triple(esk5_0,esk6_0,esk7_0)),pair(X1,X2)),X1)),
inference(scs_inference,[],[i_0_142,i_0_298,i_0_308,i_0_318,i_0_316,i_0_177,i_0_340,i_0_324,i_0_195,i_0_204,i_0_229,i_0_282,i_0_283]) ).
cnf(i_0_342,plain,
remove_slb(insert_slb(X1,pair(X2,X3)),X2) = X1,
inference(rename_variables,[],[i_0_177]) ).
cnf(i_0_343,plain,
$false,
inference(scs_inference,[],[i_0_142,i_0_296,i_0_298,i_0_308,i_0_318,i_0_316,i_0_177,i_0_340,i_0_324,i_0_195,i_0_204,i_0_229,i_0_282,i_0_283,i_0_192]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWV371+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.15/0.33 % Computer : n007.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 05:04:53 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 0.34/1.61 % Version : CSE_E---1.7
% 0.34/1.61 % Problem : theBenchmark.p
% 0.34/1.61 % SZS status Theorem for theBenchmark.p
% 0.34/1.61 % SZS output start CNFRefutation
% See solution above
% 0.54/1.80 % Total time : 1.273s
%------------------------------------------------------------------------------