%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWV365+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.51s 1.62s
% Output : CNFRefutation 0.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWV365+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.16/0.33 % Computer : n007.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 05:05:23 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 0.51/1.62 % Version : CSE_E---1.7
% 0.51/1.62 % Problem : theBenchmark.p
% 0.51/1.62 % SZS status Theorem for theBenchmark.p
% 0.51/1.62 % SZS output start CNFRefutation
% 0.51/1.62 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)).
% 0.51/1.62 fof(l1_co, conjecture, ![X1, X2, X4, X5]:i(triple(X1,create_slb,X4))=i(triple(X2,create_slb,X5)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', l1_co)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 fof(ax40, axiom, ![X1, X2]:(ok(triple(X1,X2,bad))<=>~$true), file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax', ax40)).
% 0.51/1.62 fof(ax41, axiom, ![X1, X2, X3]:(~(ok(triple(X1,X2,X3)))=>X3=bad), file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax', ax41)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 fof(ax22, axiom, ![X1, X2]:~(pair_in_list(create_slb,X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax', ax22)).
% 0.51/1.62 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)).
% 0.51/1.62 fof(ax20, axiom, ![X1]:~(contains_slb(create_slb,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax', ax20)).
% 0.51/1.62 fof(ax8, axiom, ![X1]:~(contains_pq(create_pq,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV007+1.ax', ax8)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 fof(ax36, axiom, ![X1, X2]:check_cpq(triple(X1,create_slb,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax', ax36)).
% 0.51/1.62 fof(ax54, axiom, ![X1, X2]:i(triple(X1,create_slb,X2))=create_pq, file('/export/starexec/sandbox/benchmark/Axioms/SWV007+4.ax', ax54)).
% 0.51/1.62 fof(ax50, axiom, ![X1, X2]:findmin_cpq_res(triple(X1,create_slb,X2))=bottom, file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax', ax50)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 fof(ax19, axiom, ![X1, X2, X3]:isnonempty_slb(insert_slb(X1,pair(X2,X3))), file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax', ax19)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 fof(ax11, axiom, ![X1, X2]:remove_pq(insert_pq(X1,X2),X2)=X1, file('/export/starexec/sandbox/benchmark/Axioms/SWV007+1.ax', ax11)).
% 0.51/1.62 fof(ax56, axiom, ![X1, X2]:(pi_sharp_remove(X1,X2)<=>contains_pq(X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SWV007+4.ax', ax56)).
% 0.51/1.62 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)).
% 0.51/1.62 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)).
% 0.51/1.62 fof(ax7, axiom, ![X1, X2]:isnonempty_pq(insert_pq(X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SWV007+1.ax', ax7)).
% 0.51/1.62 fof(totality, axiom, ![X1, X2]:(less_than(X1,X2)|less_than(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV007+0.ax', totality)).
% 0.51/1.62 fof(ax31, axiom, ![X1]:succ_cpq(X1,X1), file('/export/starexec/sandbox/benchmark/Axioms/SWV007+3.ax', ax31)).
% 0.51/1.62 fof(reflexivity, axiom, ![X1]:less_than(X1,X1), file('/export/starexec/sandbox/benchmark/Axioms/SWV007+0.ax', reflexivity)).
% 0.51/1.62 fof(bottom_smallest, axiom, ![X1]:less_than(bottom,X1), file('/export/starexec/sandbox/benchmark/Axioms/SWV007+0.ax', bottom_smallest)).
% 0.51/1.62 fof(ax28, axiom, ![X1]:update_slb(create_slb,X1)=create_slb, file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax', ax28)).
% 0.51/1.62 fof(ax18, axiom, ~(isnonempty_slb(create_slb)), file('/export/starexec/sandbox/benchmark/Axioms/SWV007+2.ax', ax18)).
% 0.51/1.62 fof(ax6, axiom, ~(isnonempty_pq(create_pq)), file('/export/starexec/sandbox/benchmark/Axioms/SWV007+1.ax', ax6)).
% 0.51/1.62 fof(i_0_62, 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])).
% 0.51/1.62 fof(i_0_63, negated_conjecture, ~(![X1, X2, X4, X5]:i(triple(X1,create_slb,X4))=i(triple(X2,create_slb,X5))), inference(assume_negation,[status(cth)],[l1_co])).
% 0.51/1.62 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])).
% 0.51/1.62 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])).
% 0.51/1.62 fof(i_0_66, plain, ![X1, X2]:~ok(triple(X1,X2,bad)), inference(fof_simplification,[status(thm)],[ax40])).
% 0.51/1.62 fof(i_0_67, plain, ![X1, X2, X3]:(~ok(triple(X1,X2,X3))=>X3=bad), inference(fof_simplification,[status(thm)],[ax41])).
% 0.51/1.62 fof(i_0_68, plain, ![X257, X258]:(~succ_cpq(X257,X258)|succ_cpq(X257,removemin_cpq_eff(X258))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax35])])).
% 0.51/1.62 fof(i_0_69, plain, ![X312]:removemin_cpq_eff(X312)=remove_cpq(findmin_cpq_eff(X312),findmin_cpq_res(X312)), inference(variable_rename,[status(thm)],[ax52])).
% 0.51/1.62 fof(i_0_70, plain, ![X1, X2]:~pair_in_list(create_slb,X1,X2), inference(fof_simplification,[status(thm)],[ax22])).
% 0.51/1.62 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])).
% 0.51/1.62 fof(i_0_72, plain, ![X1]:~contains_slb(create_slb,X1), inference(fof_simplification,[status(thm)],[ax20])).
% 0.51/1.62 fof(i_0_73, plain, ![X1]:~contains_pq(create_pq,X1), inference(fof_simplification,[status(thm)],[ax8])).
% 0.51/1.62 fof(i_0_74, plain, ![X261, X262, X263, X264, X265]:((~check_cpq(triple(X261,insert_slb(X262,pair(X264,X265)),X263))|check_cpq(triple(X261,X262,X263))|~less_than(X265,X264))&(~check_cpq(triple(X261,X262,X263))|check_cpq(triple(X261,insert_slb(X262,pair(X264,X265)),X263))|~less_than(X265,X264))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax37])])])).
% 0.51/1.62 fof(i_0_75, plain, ![X316, X317, X318, X319, X320]:i(triple(X316,insert_slb(X317,pair(X319,X320)),X318))=insert_pq(i(triple(X316,X317,X318)),X319), inference(variable_rename,[status(thm)],[ax55])).
% 0.51/1.62 fof(i_0_76, plain, ![X266, X267, X268, X269, X270]:(~strictly_less_than(X269,X270)|~check_cpq(triple(X266,insert_slb(X267,pair(X269,X270)),X268))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_62])])).
% 0.51/1.62 fof(i_0_77, plain, ![X304, X305, X306]:(X305=create_slb|~contains_slb(X305,findmin_pqp_res(X304))|~less_than(lookup_slb(X305,findmin_pqp_res(X304)),findmin_pqp_res(X304))|findmin_cpq_eff(triple(X304,X305,X306))=triple(X304,update_slb(X305,findmin_pqp_res(X304)),X306)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[ax49])])])).
% 0.51/1.62 fof(i_0_78, plain, ![X301, X302, X303]:(X302=create_slb|~contains_slb(X302,findmin_pqp_res(X301))|~strictly_less_than(findmin_pqp_res(X301),lookup_slb(X302,findmin_pqp_res(X301)))|findmin_cpq_eff(triple(X301,X302,X303))=triple(X301,update_slb(X302,findmin_pqp_res(X301)),bad)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[ax48])])])).
% 0.51/1.62 fof(i_0_79, negated_conjecture, i(triple(esk5_0,create_slb,esk7_0))!=i(triple(esk6_0,create_slb,esk8_0)), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_63])])])).
% 0.51/1.62 fof(i_0_80, plain, ![X288, X289, X290, X291]:(~contains_slb(X289,X291)|~less_than(lookup_slb(X289,X291),X291)|remove_cpq(triple(X288,X289,X290),X291)=triple(remove_pqp(X288,X291),remove_slb(X289,X291),X290)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax44])])).
% 0.51/1.62 fof(i_0_81, plain, ![X292, X293, X294, X295]:(~contains_slb(X293,X295)|~strictly_less_than(X295,lookup_slb(X293,X295))|remove_cpq(triple(X292,X293,X294),X295)=triple(remove_pqp(X292,X295),remove_slb(X293,X295),bad)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax45])])).
% 0.51/1.62 fof(i_0_82, plain, ![X280, X281, X282, X283]:insert_cpq(triple(X280,X281,X282),X283)=triple(insert_pqp(X280,X283),insert_slb(X281,pair(X283,bottom)),X282), inference(variable_rename,[status(thm)],[ax42])).
% 0.51/1.62 fof(i_0_83, plain, ![X220, X221, X222, X223, X224]:(((X221=X222|pair_in_list(X220,X222,X224)|~pair_in_list(insert_slb(X220,pair(X221,X223)),X222,X224))&(X223=X224|pair_in_list(X220,X222,X224)|~pair_in_list(insert_slb(X220,pair(X221,X223)),X222,X224)))&((~pair_in_list(X220,X222,X224)|pair_in_list(insert_slb(X220,pair(X221,X223)),X222,X224))&(X221!=X222|X223!=X224|pair_in_list(insert_slb(X220,pair(X221,X223)),X222,X224)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax23])])])).
% 0.51/1.62 fof(i_0_84, plain, ![X298, X299, X300]:(X299=create_slb|contains_slb(X299,findmin_pqp_res(X298))|findmin_cpq_eff(triple(X298,X299,X300))=triple(X298,update_slb(X299,findmin_pqp_res(X298)),bad)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[i_0_64])])])).
% 0.51/1.62 fof(i_0_85, plain, ![X271, X272, X273, X274]:((~contains_cpq(triple(X271,X272,X273),X274)|contains_slb(X272,X274))&(~contains_slb(X272,X274)|contains_cpq(triple(X271,X272,X273),X274))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax39])])).
% 0.51/1.62 fof(i_0_86, plain, ![X284, X285, X286, X287]:(contains_slb(X285,X287)|remove_cpq(triple(X284,X285,X286),X287)=triple(X284,X285,bad)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_65])])).
% 0.51/1.62 fof(i_0_87, plain, ![X228, X229, X230, X231]:(X229=X230|~contains_slb(X228,X230)|remove_slb(insert_slb(X228,pair(X229,X231)),X230)=insert_slb(remove_slb(X228,X230),pair(X229,X231))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax25])])).
% 0.51/1.62 fof(i_0_88, plain, ![X240, X241, X242, X243]:(~strictly_less_than(X243,X242)|update_slb(insert_slb(X240,pair(X241,X243)),X242)=insert_slb(update_slb(X240,X242),pair(X241,X242))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax29])])).
% 0.51/1.62 fof(i_0_89, plain, ![X244, X245, X246, X247]:(~less_than(X246,X247)|update_slb(insert_slb(X244,pair(X245,X247)),X246)=insert_slb(update_slb(X244,X246),pair(X245,X247))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax30])])).
% 0.51/1.62 fof(i_0_90, plain, ![X275, X276]:~ok(triple(X275,X276,bad)), inference(variable_rename,[status(thm)],[i_0_66])).
% 0.51/1.62 fof(i_0_91, plain, ![X214, X215, X216, X217]:((~contains_slb(insert_slb(X214,pair(X215,X217)),X216)|(contains_slb(X214,X216)|X215=X216))&((~contains_slb(X214,X216)|contains_slb(insert_slb(X214,pair(X215,X217)),X216))&(X215!=X216|contains_slb(insert_slb(X214,pair(X215,X217)),X216)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax21])])])).
% 0.51/1.62 fof(i_0_92, plain, ![X296, X297]:findmin_cpq_eff(triple(X296,create_slb,X297))=triple(X296,create_slb,bad), inference(variable_rename,[status(thm)],[ax46])).
% 0.51/1.62 fof(i_0_93, plain, ![X235, X236, X237, X238]:(X236=X237|~contains_slb(X235,X237)|lookup_slb(insert_slb(X235,pair(X236,X238)),X237)=lookup_slb(X235,X237)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax27])])).
% 0.51/1.62 fof(i_0_94, plain, ![X309, X310, X311]:(X310=create_slb|findmin_cpq_res(triple(X309,X310,X311))=findmin_pqp_res(X309)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[ax51])])])).
% 0.51/1.62 fof(i_0_95, plain, ![X277, X278, X279]:(ok(triple(X277,X278,X279))|X279=bad), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_67])])).
% 0.51/1.62 fof(i_0_96, plain, ![X259, X260]:check_cpq(triple(X259,create_slb,X260)), inference(variable_rename,[status(thm)],[ax36])).
% 0.51/1.62 fof(i_0_97, plain, ![X314, X315]:i(triple(X314,create_slb,X315))=create_pq, inference(variable_rename,[status(thm)],[ax54])).
% 0.51/1.62 fof(i_0_98, plain, ![X307, X308]:findmin_cpq_res(triple(X307,create_slb,X308))=bottom, inference(variable_rename,[status(thm)],[ax50])).
% 0.51/1.62 fof(i_0_99, plain, ![X196, X197, X198]:(~contains_pq(X196,X198)|X197=X198|remove_pq(insert_pq(X196,X197),X198)=insert_pq(remove_pq(X196,X198),X197)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax12])])).
% 0.51/1.62 fof(i_0_100, plain, ![X232, X233, X234]:lookup_slb(insert_slb(X232,pair(X233,X234)),X233)=X234, inference(variable_rename,[status(thm)],[ax26])).
% 0.51/1.62 fof(i_0_101, plain, ![X225, X226, X227]:remove_slb(insert_slb(X225,pair(X226,X227)),X226)=X225, inference(variable_rename,[status(thm)],[ax24])).
% 0.51/1.62 cnf(i_0_102, plain, (succ_cpq(X1,removemin_cpq_eff(X2))|~succ_cpq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_68])).
% 0.51/1.62 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])).
% 0.51/1.62 fof(i_0_104, plain, ![X218, X219]:~pair_in_list(create_slb,X218,X219), inference(variable_rename,[status(thm)],[i_0_70])).
% 0.51/1.62 fof(i_0_105, plain, ![X210, X211, X212]:isnonempty_slb(insert_slb(X210,pair(X211,X212))), inference(variable_rename,[status(thm)],[ax19])).
% 0.51/1.62 fof(i_0_106, plain, ![X185, X186, X187]:((~contains_pq(insert_pq(X185,X186),X187)|(contains_pq(X185,X187)|X186=X187))&((~contains_pq(X185,X187)|contains_pq(insert_pq(X185,X186),X187))&(X186!=X187|contains_pq(insert_pq(X185,X186),X187)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax9])])])).
% 0.51/1.62 fof(i_0_107, plain, ![X207, X208, X209]:insert_pq(insert_pq(X207,X208),X209)=insert_pq(insert_pq(X207,X209),X208), inference(variable_rename,[status(thm)],[ax17])).
% 0.51/1.62 fof(i_0_108, plain, ![X188, X189, X190, X191, X192]:((~issmallestelement_pq(X188,X189)|(~contains_pq(X188,X190)|less_than(X189,X190)))&((contains_pq(X191,esk1_2(X191,X192))|issmallestelement_pq(X191,X192))&(~less_than(X192,esk1_2(X191,X192))|issmallestelement_pq(X191,X192)))), 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])])])])])])).
% 0.51/1.62 fof(i_0_109, plain, ![X203, X204]:(~contains_pq(X203,X204)|~issmallestelement_pq(X203,X204)|removemin_pq_eff(X203,X204)=remove_pq(X203,X204)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax15])])).
% 0.51/1.62 fof(i_0_110, plain, ![X252, X253, X254]:(~succ_cpq(X252,X253)|succ_cpq(X252,remove_cpq(X253,X254))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax33])])).
% 0.51/1.62 fof(i_0_111, plain, ![X249, X250, X251]:(~succ_cpq(X249,X250)|succ_cpq(X249,insert_cpq(X250,X251))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax32])])).
% 0.51/1.62 fof(i_0_112, plain, ![X205, X206]:(~contains_pq(X205,X206)|~issmallestelement_pq(X205,X206)|removemin_pq_res(X205,X206)=X206), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax16])])).
% 0.51/1.62 fof(i_0_113, plain, ![X201, X202]:(~contains_pq(X201,X202)|~issmallestelement_pq(X201,X202)|findmin_pq_res(X201,X202)=X202), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax14])])).
% 0.51/1.62 fof(i_0_114, plain, ![X199, X200]:(~contains_pq(X199,X200)|~issmallestelement_pq(X199,X200)|findmin_pq_eff(X199,X200)=X199), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax13])])).
% 0.51/1.62 fof(i_0_115, plain, ![X331, X332]:(((contains_pq(X331,X332)|~pi_sharp_removemin(X331,X332))&(issmallestelement_pq(X331,X332)|~pi_sharp_removemin(X331,X332)))&(~contains_pq(X331,X332)|~issmallestelement_pq(X331,X332)|pi_sharp_removemin(X331,X332))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax60])])])).
% 0.51/1.62 fof(i_0_116, plain, ![X325, X326]:(((contains_pq(X325,X326)|~pi_sharp_find_min(X325,X326))&(issmallestelement_pq(X325,X326)|~pi_sharp_find_min(X325,X326)))&(~contains_pq(X325,X326)|~issmallestelement_pq(X325,X326)|pi_sharp_find_min(X325,X326))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax58])])])).
% 0.51/1.62 fof(i_0_117, plain, ![X173, X174, X175]:(~less_than(X173,X174)|~less_than(X174,X175)|less_than(X173,X175)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitivity])])).
% 0.51/1.62 fof(i_0_118, plain, ![X179, X180]:(((less_than(X179,X180)|~strictly_less_than(X179,X180))&(~less_than(X180,X179)|~strictly_less_than(X179,X180)))&(~less_than(X179,X180)|less_than(X180,X179)|strictly_less_than(X179,X180))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_71])])])).
% 0.51/1.62 fof(i_0_119, plain, ![X323, X324]:((~pi_remove(X323,X324)|pi_sharp_remove(i(X323),X324))&(~pi_sharp_remove(i(X323),X324)|pi_remove(X323,X324))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax57])])).
% 0.51/1.62 fof(i_0_120, plain, ![X255, X256]:(~succ_cpq(X255,X256)|succ_cpq(X255,findmin_cpq_eff(X256))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax34])])).
% 0.51/1.62 fof(i_0_121, plain, ![X337, X339, X340]:((((succ_cpq(X337,esk4_1(X337))|~phi(X337))&(ok(esk4_1(X337))|~phi(X337)))&(check_cpq(esk4_1(X337))|~phi(X337)))&(~succ_cpq(X339,X340)|~ok(X340)|~check_cpq(X340)|phi(X339))), 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])])])])])])).
% 0.51/1.62 fof(i_0_122, plain, ![X194, X195]:remove_pq(insert_pq(X194,X195),X195)=X194, inference(variable_rename,[status(thm)],[ax11])).
% 0.51/1.62 fof(i_0_123, plain, ![X321, X322]:((~pi_sharp_remove(X321,X322)|contains_pq(X321,X322))&(~contains_pq(X321,X322)|pi_sharp_remove(X321,X322))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax56])])).
% 0.51/1.62 fof(i_0_124, plain, ![X333, X335, X336]:((~pi_removemin(X333)|pi_sharp_find_min(i(X333),esk3_1(X333)))&(~pi_sharp_find_min(i(X335),X336)|pi_removemin(X335))), 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])])])])])).
% 0.51/1.62 fof(i_0_125, plain, ![X327, X329, X330]:((~pi_find_min(X327)|pi_sharp_find_min(i(X327),esk2_1(X327)))&(~pi_sharp_find_min(i(X329),X330)|pi_find_min(X329))), 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])])])])])).
% 0.51/1.62 fof(i_0_126, plain, ![X182, X183]:isnonempty_pq(insert_pq(X182,X183)), inference(variable_rename,[status(thm)],[ax7])).
% 0.51/1.62 fof(i_0_127, plain, ![X176, X177]:(less_than(X176,X177)|less_than(X177,X176)), inference(variable_rename,[status(thm)],[totality])).
% 0.51/1.62 fof(i_0_128, plain, ![X213]:~contains_slb(create_slb,X213), inference(variable_rename,[status(thm)],[i_0_72])).
% 0.51/1.62 fof(i_0_129, plain, ![X184]:~contains_pq(create_pq,X184), inference(variable_rename,[status(thm)],[i_0_73])).
% 0.51/1.62 fof(i_0_130, plain, ![X248]:succ_cpq(X248,X248), inference(variable_rename,[status(thm)],[ax31])).
% 0.51/1.62 fof(i_0_131, plain, ![X178]:less_than(X178,X178), inference(variable_rename,[status(thm)],[reflexivity])).
% 0.51/1.62 fof(i_0_132, plain, ![X181]:less_than(bottom,X181), inference(variable_rename,[status(thm)],[bottom_smallest])).
% 0.51/1.62 fof(i_0_133, plain, ![X239]:update_slb(create_slb,X239)=create_slb, inference(variable_rename,[status(thm)],[ax28])).
% 0.51/1.62 fof(i_0_134, plain, ~isnonempty_slb(create_slb), inference(fof_simplification,[status(thm)],[ax18])).
% 0.51/1.62 fof(i_0_135, plain, ~isnonempty_pq(create_pq), inference(fof_simplification,[status(thm)],[ax6])).
% 0.51/1.62 cnf(i_0_136, 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_74]), ['final']).
% 0.51/1.62 cnf(i_0_137, 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_75]), ['final']).
% 0.51/1.62 cnf(i_0_138, 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_74]), ['final']).
% 0.51/1.62 cnf(i_0_139, plain, (~strictly_less_than(X1,X2)|~check_cpq(triple(X3,insert_slb(X4,pair(X1,X2)),X5))), inference(split_conjunct,[status(thm)],[i_0_76]), ['final']).
% 0.51/1.62 cnf(i_0_140, 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_77]), ['final']).
% 0.51/1.62 cnf(i_0_141, 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_78]), ['final']).
% 0.51/1.62 cnf(i_0_142, negated_conjecture, (i(triple(esk5_0,create_slb,esk7_0))!=i(triple(esk6_0,create_slb,esk8_0))), inference(split_conjunct,[status(thm)],[i_0_79]), ['final']).
% 0.51/1.62 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']).
% 0.51/1.62 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']).
% 0.51/1.62 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']).
% 0.51/1.62 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']).
% 0.51/1.62 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']).
% 0.51/1.62 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']).
% 0.51/1.62 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']).
% 0.51/1.62 cnf(i_0_150, plain, (contains_slb(X2,X4)|~contains_cpq(triple(X1,X2,X3),X4)), inference(split_conjunct,[status(thm)],[i_0_85]), ['final']).
% 0.51/1.62 cnf(i_0_151, 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']).
% 0.51/1.62 cnf(i_0_152, 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']).
% 0.51/1.62 cnf(i_0_153, 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']).
% 0.51/1.62 cnf(i_0_154, 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']).
% 0.51/1.62 cnf(i_0_155, plain, (~ok(triple(X1,X2,bad))), inference(split_conjunct,[status(thm)],[i_0_90]), ['final']).
% 0.51/1.62 cnf(i_0_156, 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']).
% 0.51/1.62 cnf(i_0_157, plain, (findmin_cpq_eff(triple(X1,create_slb,X2))=triple(X1,create_slb,bad)), inference(split_conjunct,[status(thm)],[i_0_92]), ['final']).
% 0.51/1.62 cnf(i_0_158, plain, (contains_cpq(triple(X3,X1,X4),X2)|~contains_slb(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_85]), ['final']).
% 0.51/1.62 cnf(i_0_159, 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']).
% 0.51/1.62 cnf(i_0_160, 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']).
% 0.51/1.62 cnf(i_0_161, plain, (X1=create_slb|findmin_cpq_res(triple(X2,X1,X3))=findmin_pqp_res(X2)), inference(split_conjunct,[status(thm)],[i_0_94]), ['final']).
% 0.51/1.62 cnf(i_0_162, plain, (contains_slb(insert_slb(X1,pair(X3,X4)),X2)|~contains_slb(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_91]), ['final']).
% 0.51/1.62 cnf(i_0_163, plain, (ok(triple(X1,X2,X3))|X3=bad), inference(split_conjunct,[status(thm)],[i_0_95]), ['final']).
% 0.51/1.62 cnf(i_0_164, plain, (check_cpq(triple(X1,create_slb,X2))), inference(split_conjunct,[status(thm)],[i_0_96]), ['final']).
% 0.51/1.62 cnf(i_0_165, plain, (i(triple(X1,create_slb,X2))=create_pq), inference(split_conjunct,[status(thm)],[i_0_97]), ['final']).
% 0.51/1.62 cnf(i_0_166, plain, (findmin_cpq_res(triple(X1,create_slb,X2))=bottom), inference(split_conjunct,[status(thm)],[i_0_98]), ['final']).
% 0.51/1.62 cnf(i_0_167, 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']).
% 0.51/1.62 cnf(i_0_168, plain, (contains_slb(insert_slb(X3,pair(X1,X4)),X2)|X1!=X2), inference(split_conjunct,[status(thm)],[i_0_91]), ['final']).
% 0.51/1.62 cnf(i_0_169, plain, (lookup_slb(insert_slb(X1,pair(X2,X3)),X2)=X3), inference(split_conjunct,[status(thm)],[i_0_100]), ['final']).
% 0.51/1.62 cnf(i_0_170, plain, (remove_slb(insert_slb(X1,pair(X2,X3)),X2)=X1), inference(split_conjunct,[status(thm)],[i_0_101]), ['final']).
% 0.51/1.62 cnf(i_0_171, 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']).
% 0.51/1.62 cnf(i_0_172, plain, (~pair_in_list(create_slb,X1,X2)), inference(split_conjunct,[status(thm)],[i_0_104]), ['final']).
% 0.51/1.62 cnf(i_0_173, plain, (isnonempty_slb(insert_slb(X1,pair(X2,X3)))), inference(split_conjunct,[status(thm)],[i_0_105]), ['final']).
% 0.51/1.62 cnf(i_0_174, plain, (contains_pq(X1,X3)|X2=X3|~contains_pq(insert_pq(X1,X2),X3)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.51/1.62 cnf(i_0_175, plain, (insert_pq(insert_pq(X1,X2),X3)=insert_pq(insert_pq(X1,X3),X2)), inference(split_conjunct,[status(thm)],[i_0_107]), ['final']).
% 0.51/1.62 cnf(i_0_176, plain, (issmallestelement_pq(X2,X1)|~less_than(X1,esk1_2(X2,X1))), inference(split_conjunct,[status(thm)],[i_0_108]), ['final']).
% 0.51/1.62 cnf(i_0_177, 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']).
% 0.51/1.62 cnf(i_0_178, plain, (contains_pq(insert_pq(X1,X3),X2)|~contains_pq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.51/1.62 cnf(i_0_179, plain, (succ_cpq(X1,remove_cpq(X2,X3))|~succ_cpq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_110]), ['final']).
% 0.51/1.62 cnf(i_0_180, plain, (succ_cpq(X1,insert_cpq(X2,X3))|~succ_cpq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_111]), ['final']).
% 0.51/1.62 cnf(i_0_181, plain, (removemin_pq_res(X1,X2)=X2|~contains_pq(X1,X2)|~issmallestelement_pq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_112]), ['final']).
% 0.51/1.62 cnf(i_0_182, plain, (findmin_pq_res(X1,X2)=X2|~contains_pq(X1,X2)|~issmallestelement_pq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.51/1.62 cnf(i_0_183, plain, (findmin_pq_eff(X1,X2)=X1|~contains_pq(X1,X2)|~issmallestelement_pq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.51/1.62 cnf(i_0_184, plain, (pi_sharp_removemin(X1,X2)|~contains_pq(X1,X2)|~issmallestelement_pq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.51/1.62 cnf(i_0_185, plain, (pi_sharp_find_min(X1,X2)|~contains_pq(X1,X2)|~issmallestelement_pq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 0.51/1.62 cnf(i_0_186, plain, (less_than(X1,X3)|~less_than(X1,X2)|~less_than(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 0.51/1.62 cnf(i_0_187, plain, (less_than(X2,X3)|~issmallestelement_pq(X1,X2)|~contains_pq(X1,X3)), inference(split_conjunct,[status(thm)],[i_0_108]), ['final']).
% 0.51/1.62 cnf(i_0_188, plain, (contains_pq(X1,esk1_2(X1,X2))|issmallestelement_pq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_108]), ['final']).
% 0.51/1.62 cnf(i_0_189, plain, (less_than(X2,X1)|strictly_less_than(X1,X2)|~less_than(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_118]), ['final']).
% 0.51/1.62 cnf(i_0_190, plain, (pi_remove(X1,X2)|~pi_sharp_remove(i(X1),X2)), inference(split_conjunct,[status(thm)],[i_0_119]), ['final']).
% 0.51/1.62 cnf(i_0_191, plain, (~less_than(X1,X2)|~strictly_less_than(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_118]), ['final']).
% 0.51/1.62 cnf(i_0_192, plain, (contains_pq(insert_pq(X3,X1),X2)|X1!=X2), inference(split_conjunct,[status(thm)],[i_0_106]), ['final']).
% 0.51/1.62 cnf(i_0_193, plain, (pi_sharp_remove(i(X1),X2)|~pi_remove(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_119]), ['final']).
% 0.51/1.62 cnf(i_0_194, plain, (succ_cpq(X1,findmin_cpq_eff(X2))|~succ_cpq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.51/1.62 cnf(i_0_195, plain, (phi(X1)|~succ_cpq(X1,X2)|~ok(X2)|~check_cpq(X2)), inference(split_conjunct,[status(thm)],[i_0_121]), ['final']).
% 0.51/1.62 cnf(i_0_196, plain, (remove_pq(insert_pq(X1,X2),X2)=X1), inference(split_conjunct,[status(thm)],[i_0_122]), ['final']).
% 0.51/1.62 cnf(i_0_197, plain, (pi_sharp_remove(X1,X2)|~contains_pq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_123]), ['final']).
% 0.51/1.62 cnf(i_0_198, plain, (issmallestelement_pq(X1,X2)|~pi_sharp_removemin(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.51/1.62 cnf(i_0_199, plain, (issmallestelement_pq(X1,X2)|~pi_sharp_find_min(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 0.51/1.62 cnf(i_0_200, plain, (contains_pq(X1,X2)|~pi_sharp_removemin(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.51/1.62 cnf(i_0_201, plain, (contains_pq(X1,X2)|~pi_sharp_find_min(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 0.51/1.62 cnf(i_0_202, plain, (contains_pq(X1,X2)|~pi_sharp_remove(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_123]), ['final']).
% 0.51/1.62 cnf(i_0_203, plain, (less_than(X1,X2)|~strictly_less_than(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_118]), ['final']).
% 0.51/1.62 cnf(i_0_204, plain, (pi_removemin(X1)|~pi_sharp_find_min(i(X1),X2)), inference(split_conjunct,[status(thm)],[i_0_124]), ['final']).
% 0.51/1.62 cnf(i_0_205, plain, (pi_find_min(X1)|~pi_sharp_find_min(i(X1),X2)), inference(split_conjunct,[status(thm)],[i_0_125]), ['final']).
% 0.51/1.62 cnf(i_0_206, plain, (pi_sharp_find_min(i(X1),esk3_1(X1))|~pi_removemin(X1)), inference(split_conjunct,[status(thm)],[i_0_124]), ['final']).
% 0.51/1.62 cnf(i_0_207, plain, (pi_sharp_find_min(i(X1),esk2_1(X1))|~pi_find_min(X1)), inference(split_conjunct,[status(thm)],[i_0_125]), ['final']).
% 0.51/1.62 cnf(i_0_208, plain, (isnonempty_pq(insert_pq(X1,X2))), inference(split_conjunct,[status(thm)],[i_0_126]), ['final']).
% 0.51/1.62 cnf(i_0_209, plain, (less_than(X1,X2)|less_than(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_127]), ['final']).
% 0.51/1.62 cnf(i_0_210, plain, (succ_cpq(X1,esk4_1(X1))|~phi(X1)), inference(split_conjunct,[status(thm)],[i_0_121]), ['final']).
% 0.51/1.62 cnf(i_0_211, plain, (~contains_slb(create_slb,X1)), inference(split_conjunct,[status(thm)],[i_0_128]), ['final']).
% 0.51/1.62 cnf(i_0_212, plain, (~contains_pq(create_pq,X1)), inference(split_conjunct,[status(thm)],[i_0_129]), ['final']).
% 0.51/1.62 cnf(i_0_213, plain, (ok(esk4_1(X1))|~phi(X1)), inference(split_conjunct,[status(thm)],[i_0_121]), ['final']).
% 0.51/1.62 cnf(i_0_214, plain, (check_cpq(esk4_1(X1))|~phi(X1)), inference(split_conjunct,[status(thm)],[i_0_121]), ['final']).
% 0.51/1.62 cnf(i_0_215, plain, (succ_cpq(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_130]), ['final']).
% 0.51/1.62 cnf(i_0_216, plain, (less_than(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_131]), ['final']).
% 0.51/1.62 cnf(i_0_217, plain, (less_than(bottom,X1)), inference(split_conjunct,[status(thm)],[i_0_132]), ['final']).
% 0.51/1.62 cnf(i_0_218, plain, (update_slb(create_slb,X1)=create_slb), inference(split_conjunct,[status(thm)],[i_0_133]), ['final']).
% 0.51/1.62 cnf(i_0_219, plain, (~isnonempty_slb(create_slb)), inference(split_conjunct,[status(thm)],[i_0_134]), ['final']).
% 0.51/1.62 cnf(i_0_220, plain, (~isnonempty_pq(create_pq)), inference(split_conjunct,[status(thm)],[i_0_135]), ['final']).
% 0.51/1.62 cnf(i_0_221, axiom, (X1=X1)).
% 0.51/1.62 cnf(i_0_222, axiom, (X1=X2|X2!=X1)).
% 0.51/1.62 cnf(i_0_223, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.51/1.62 cnf(i_0_224, axiom, (X1!=X2|triple(X1,X3,X4)=triple(X2,X3,X4))).
% 0.51/1.62 cnf(i_0_225, axiom, (X1!=X2|triple(X3,X1,X4)=triple(X3,X2,X4))).
% 0.51/1.62 cnf(i_0_226, axiom, (X1!=X2|triple(X3,X4,X1)=triple(X3,X4,X2))).
% 0.51/1.62 cnf(i_0_227, axiom, (X1!=X2|remove_cpq(X1,X3)=remove_cpq(X2,X3))).
% 0.51/1.62 cnf(i_0_228, axiom, (X1!=X2|remove_cpq(X3,X1)=remove_cpq(X3,X2))).
% 0.51/1.62 cnf(i_0_229, axiom, (X1!=X2|remove_slb(X1,X3)=remove_slb(X2,X3))).
% 0.51/1.62 cnf(i_0_230, axiom, (X1!=X2|remove_slb(X3,X1)=remove_slb(X3,X2))).
% 0.51/1.62 cnf(i_0_231, axiom, (X1!=X2|insert_cpq(X1,X3)=insert_cpq(X2,X3))).
% 0.51/1.62 cnf(i_0_232, axiom, (X1!=X2|insert_cpq(X3,X1)=insert_cpq(X3,X2))).
% 0.51/1.62 cnf(i_0_233, axiom, (X1!=X2|findmin_cpq_res(X1)=findmin_cpq_res(X2))).
% 0.51/1.62 cnf(i_0_234, axiom, (X1!=X2|remove_pq(X1,X3)=remove_pq(X2,X3))).
% 0.51/1.62 cnf(i_0_235, axiom, (X1!=X2|remove_pq(X3,X1)=remove_pq(X3,X2))).
% 0.51/1.62 cnf(i_0_236, axiom, (X1!=X2|removemin_pq_eff(X1,X3)=removemin_pq_eff(X2,X3))).
% 0.51/1.62 cnf(i_0_237, axiom, (X1!=X2|removemin_pq_eff(X3,X1)=removemin_pq_eff(X3,X2))).
% 0.51/1.62 cnf(i_0_238, axiom, (X1!=X2|removemin_pq_res(X1,X3)=removemin_pq_res(X2,X3))).
% 0.51/1.62 cnf(i_0_239, axiom, (X1!=X2|removemin_pq_res(X3,X1)=removemin_pq_res(X3,X2))).
% 0.51/1.62 cnf(i_0_240, axiom, (X1!=X2|insert_slb(X1,X3)=insert_slb(X2,X3))).
% 0.51/1.62 cnf(i_0_241, axiom, (X1!=X2|insert_slb(X3,X1)=insert_slb(X3,X2))).
% 0.51/1.62 cnf(i_0_242, axiom, (X1!=X2|findmin_pq_res(X1,X3)=findmin_pq_res(X2,X3))).
% 0.51/1.62 cnf(i_0_243, axiom, (X1!=X2|findmin_pq_res(X3,X1)=findmin_pq_res(X3,X2))).
% 0.51/1.62 cnf(i_0_244, axiom, (X1!=X2|findmin_pq_eff(X1,X3)=findmin_pq_eff(X2,X3))).
% 0.51/1.62 cnf(i_0_245, axiom, (X1!=X2|findmin_pq_eff(X3,X1)=findmin_pq_eff(X3,X2))).
% 0.51/1.62 cnf(i_0_246, axiom, (X1!=X2|i(X1)=i(X2))).
% 0.51/1.62 cnf(i_0_247, axiom, (X1!=X2|insert_pq(X1,X3)=insert_pq(X2,X3))).
% 0.51/1.62 cnf(i_0_248, axiom, (X1!=X2|insert_pq(X3,X1)=insert_pq(X3,X2))).
% 0.51/1.62 cnf(i_0_249, axiom, (X1!=X2|findmin_cpq_eff(X1)=findmin_cpq_eff(X2))).
% 0.51/1.62 cnf(i_0_250, axiom, (X1!=X2|update_slb(X1,X3)=update_slb(X2,X3))).
% 0.51/1.62 cnf(i_0_251, axiom, (X1!=X2|update_slb(X3,X1)=update_slb(X3,X2))).
% 0.51/1.62 cnf(i_0_252, axiom, (X1!=X2|findmin_pqp_res(X1)=findmin_pqp_res(X2))).
% 0.51/1.62 cnf(i_0_253, axiom, (X1!=X2|lookup_slb(X1,X3)=lookup_slb(X2,X3))).
% 0.51/1.62 cnf(i_0_254, axiom, (X1!=X2|lookup_slb(X3,X1)=lookup_slb(X3,X2))).
% 0.51/1.62 cnf(i_0_255, axiom, (X1!=X2|~check_cpq(X1)|check_cpq(X2))).
% 0.51/1.63 cnf(i_0_256, axiom, (X1!=X2|~isnonempty_slb(X1)|isnonempty_slb(X2))).
% 0.51/1.63 cnf(i_0_257, axiom, (X1!=X2|~issmallestelement_pq(X1,X3)|issmallestelement_pq(X2,X3))).
% 0.51/1.63 cnf(i_0_258, axiom, (X1!=X2|~issmallestelement_pq(X3,X1)|issmallestelement_pq(X3,X2))).
% 0.51/1.63 cnf(i_0_259, axiom, (X1!=X2|~pi_sharp_removemin(X1,X3)|pi_sharp_removemin(X2,X3))).
% 0.51/1.63 cnf(i_0_260, axiom, (X1!=X2|~pi_sharp_removemin(X3,X1)|pi_sharp_removemin(X3,X2))).
% 0.51/1.63 cnf(i_0_261, axiom, (X1!=X2|~pi_sharp_find_min(X1,X3)|pi_sharp_find_min(X2,X3))).
% 0.51/1.63 cnf(i_0_262, axiom, (X1!=X2|~pi_sharp_find_min(X3,X1)|pi_sharp_find_min(X3,X2))).
% 0.51/1.63 cnf(i_0_263, axiom, (X1!=X2|~pi_remove(X1,X3)|pi_remove(X2,X3))).
% 0.51/1.63 cnf(i_0_264, axiom, (X1!=X2|~pi_remove(X3,X1)|pi_remove(X3,X2))).
% 0.51/1.63 cnf(i_0_265, axiom, (X1!=X2|~pi_sharp_remove(X1,X3)|pi_sharp_remove(X2,X3))).
% 0.51/1.63 cnf(i_0_266, axiom, (X1!=X2|~pi_sharp_remove(X3,X1)|pi_sharp_remove(X3,X2))).
% 0.51/1.63 cnf(i_0_267, axiom, (X1!=X2|~phi(X1)|phi(X2))).
% 0.51/1.63 cnf(i_0_268, axiom, (X1!=X2|~pi_removemin(X1)|pi_removemin(X2))).
% 0.51/1.63 cnf(i_0_269, axiom, (X1!=X2|~pi_find_min(X1)|pi_find_min(X2))).
% 0.51/1.63 cnf(i_0_270, axiom, (X1!=X2|~isnonempty_pq(X1)|isnonempty_pq(X2))).
% 0.51/1.63 cnf(i_0_271, axiom, (X1!=X2|~less_than(X1,X3)|less_than(X2,X3))).
% 0.51/1.63 cnf(i_0_272, axiom, (X1!=X2|~less_than(X3,X1)|less_than(X3,X2))).
% 0.51/1.63 cnf(i_0_273, axiom, (X1!=X2|~strictly_less_than(X1,X3)|strictly_less_than(X2,X3))).
% 0.51/1.63 cnf(i_0_274, axiom, (X1!=X2|~strictly_less_than(X3,X1)|strictly_less_than(X3,X2))).
% 0.51/1.63 cnf(i_0_275, axiom, (X1!=X2|~contains_slb(X1,X3)|contains_slb(X2,X3))).
% 0.51/1.63 cnf(i_0_276, axiom, (X1!=X2|~contains_slb(X3,X1)|contains_slb(X3,X2))).
% 0.51/1.63 cnf(i_0_277, axiom, (X1!=X2|~pair_in_list(X1,X3,X4)|pair_in_list(X2,X3,X4))).
% 0.51/1.63 cnf(i_0_278, axiom, (X1!=X2|~pair_in_list(X3,X1,X4)|pair_in_list(X3,X2,X4))).
% 0.51/1.63 cnf(i_0_279, axiom, (X1!=X2|~pair_in_list(X3,X4,X1)|pair_in_list(X3,X4,X2))).
% 0.51/1.63 cnf(i_0_280, axiom, (X1!=X2|~contains_cpq(X1,X3)|contains_cpq(X2,X3))).
% 0.51/1.63 cnf(i_0_281, axiom, (X1!=X2|~contains_cpq(X3,X1)|contains_cpq(X3,X2))).
% 0.51/1.63 cnf(i_0_282, axiom, (X1!=X2|~ok(X1)|ok(X2))).
% 0.51/1.63 cnf(i_0_283, axiom, (X1!=X2|~contains_pq(X1,X3)|contains_pq(X2,X3))).
% 0.51/1.63 cnf(i_0_284, axiom, (X1!=X2|~contains_pq(X3,X1)|contains_pq(X3,X2))).
% 0.51/1.63 cnf(i_0_285, axiom, (X1!=X2|~succ_cpq(X1,X3)|succ_cpq(X2,X3))).
% 0.51/1.63 cnf(i_0_286, axiom, (X1!=X2|~succ_cpq(X3,X1)|succ_cpq(X3,X2))).
% 0.81/1.91 cnf(i_0_221, axiom, (X1=X1)).
% 0.81/1.91 cnf(i_0_222, axiom, (X1=X2|X2!=X1)).
% 0.81/1.91 cnf(i_0_223, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.81/1.91 cnf(i_0_224, axiom, (X1!=X2|triple(X1,X3,X4)=triple(X2,X3,X4))).
% 0.81/1.91 cnf(i_0_225, axiom, (X1!=X2|triple(X3,X1,X4)=triple(X3,X2,X4))).
% 0.81/1.91 cnf(i_0_226, axiom, (X1!=X2|triple(X3,X4,X1)=triple(X3,X4,X2))).
% 0.81/1.91 cnf(i_0_227, axiom, (X1!=X2|remove_cpq(X1,X3)=remove_cpq(X2,X3))).
% 0.81/1.91 cnf(i_0_228, axiom, (X1!=X2|remove_cpq(X3,X1)=remove_cpq(X3,X2))).
% 0.81/1.91 cnf(i_0_229, axiom, (X1!=X2|remove_slb(X1,X3)=remove_slb(X2,X3))).
% 0.81/1.91 cnf(i_0_230, axiom, (X1!=X2|remove_slb(X3,X1)=remove_slb(X3,X2))).
% 0.81/1.91 cnf(i_0_231, axiom, (X1!=X2|insert_cpq(X1,X3)=insert_cpq(X2,X3))).
% 0.81/1.91 cnf(i_0_232, axiom, (X1!=X2|insert_cpq(X3,X1)=insert_cpq(X3,X2))).
% 0.81/1.91 cnf(i_0_233, axiom, (X1!=X2|findmin_cpq_res(X1)=findmin_cpq_res(X2))).
% 0.81/1.91 cnf(i_0_234, axiom, (X1!=X2|remove_pq(X1,X3)=remove_pq(X2,X3))).
% 0.81/1.91 cnf(i_0_235, axiom, (X1!=X2|remove_pq(X3,X1)=remove_pq(X3,X2))).
% 0.81/1.91 cnf(i_0_236, axiom, (X1!=X2|removemin_pq_eff(X1,X3)=removemin_pq_eff(X2,X3))).
% 0.81/1.91 cnf(i_0_237, axiom, (X1!=X2|removemin_pq_eff(X3,X1)=removemin_pq_eff(X3,X2))).
% 0.81/1.91 cnf(i_0_238, axiom, (X1!=X2|removemin_pq_res(X1,X3)=removemin_pq_res(X2,X3))).
% 0.81/1.91 cnf(i_0_239, axiom, (X1!=X2|removemin_pq_res(X3,X1)=removemin_pq_res(X3,X2))).
% 0.81/1.91 cnf(i_0_240, axiom, (X1!=X2|insert_slb(X1,X3)=insert_slb(X2,X3))).
% 0.81/1.91 cnf(i_0_241, axiom, (X1!=X2|insert_slb(X3,X1)=insert_slb(X3,X2))).
% 0.81/1.91 cnf(i_0_242, axiom, (X1!=X2|findmin_pq_res(X1,X3)=findmin_pq_res(X2,X3))).
% 0.81/1.91 cnf(i_0_243, axiom, (X1!=X2|findmin_pq_res(X3,X1)=findmin_pq_res(X3,X2))).
% 0.81/1.91 cnf(i_0_244, axiom, (X1!=X2|findmin_pq_eff(X1,X3)=findmin_pq_eff(X2,X3))).
% 0.81/1.91 cnf(i_0_245, axiom, (X1!=X2|findmin_pq_eff(X3,X1)=findmin_pq_eff(X3,X2))).
% 0.81/1.91 cnf(i_0_246, axiom, (X1!=X2|i(X1)=i(X2))).
% 0.81/1.91 cnf(i_0_247, axiom, (X1!=X2|insert_pq(X1,X3)=insert_pq(X2,X3))).
% 0.81/1.91 cnf(i_0_248, axiom, (X1!=X2|insert_pq(X3,X1)=insert_pq(X3,X2))).
% 0.81/1.91 cnf(i_0_249, axiom, (X1!=X2|findmin_cpq_eff(X1)=findmin_cpq_eff(X2))).
% 0.81/1.91 cnf(i_0_250, axiom, (X1!=X2|update_slb(X1,X3)=update_slb(X2,X3))).
% 0.81/1.91 cnf(i_0_251, axiom, (X1!=X2|update_slb(X3,X1)=update_slb(X3,X2))).
% 0.81/1.91 cnf(i_0_252, axiom, (X1!=X2|findmin_pqp_res(X1)=findmin_pqp_res(X2))).
% 0.81/1.91 cnf(i_0_253, axiom, (X1!=X2|lookup_slb(X1,X3)=lookup_slb(X2,X3))).
% 0.81/1.91 cnf(i_0_254, axiom, (X1!=X2|lookup_slb(X3,X1)=lookup_slb(X3,X2))).
% 0.81/1.91 cnf(i_0_255, axiom, (X1!=X2|~check_cpq(X1)|check_cpq(X2))).
% 0.81/1.91 cnf(i_0_256, axiom, (X1!=X2|~isnonempty_slb(X1)|isnonempty_slb(X2))).
% 0.81/1.91 cnf(i_0_257, axiom, (X1!=X2|~issmallestelement_pq(X1,X3)|issmallestelement_pq(X2,X3))).
% 0.81/1.91 cnf(i_0_258, axiom, (X1!=X2|~issmallestelement_pq(X3,X1)|issmallestelement_pq(X3,X2))).
% 0.81/1.91 cnf(i_0_259, axiom, (X1!=X2|~pi_sharp_removemin(X1,X3)|pi_sharp_removemin(X2,X3))).
% 0.81/1.91 cnf(i_0_260, axiom, (X1!=X2|~pi_sharp_removemin(X3,X1)|pi_sharp_removemin(X3,X2))).
% 0.81/1.91 cnf(i_0_261, axiom, (X1!=X2|~pi_sharp_find_min(X1,X3)|pi_sharp_find_min(X2,X3))).
% 0.81/1.91 cnf(i_0_262, axiom, (X1!=X2|~pi_sharp_find_min(X3,X1)|pi_sharp_find_min(X3,X2))).
% 0.81/1.91 cnf(i_0_263, axiom, (X1!=X2|~pi_remove(X1,X3)|pi_remove(X2,X3))).
% 0.81/1.91 cnf(i_0_264, axiom, (X1!=X2|~pi_remove(X3,X1)|pi_remove(X3,X2))).
% 0.81/1.91 cnf(i_0_265, axiom, (X1!=X2|~pi_sharp_remove(X1,X3)|pi_sharp_remove(X2,X3))).
% 0.81/1.91 cnf(i_0_266, axiom, (X1!=X2|~pi_sharp_remove(X3,X1)|pi_sharp_remove(X3,X2))).
% 0.81/1.91 cnf(i_0_267, axiom, (X1!=X2|~phi(X1)|phi(X2))).
% 0.81/1.91 cnf(i_0_268, axiom, (X1!=X2|~pi_removemin(X1)|pi_removemin(X2))).
% 0.81/1.91 cnf(i_0_269, axiom, (X1!=X2|~pi_find_min(X1)|pi_find_min(X2))).
% 0.81/1.91 cnf(i_0_270, axiom, (X1!=X2|~isnonempty_pq(X1)|isnonempty_pq(X2))).
% 0.81/1.91 cnf(i_0_271, axiom, (X1!=X2|~less_than(X1,X3)|less_than(X2,X3))).
% 0.81/1.91 cnf(i_0_272, axiom, (X1!=X2|~less_than(X3,X1)|less_than(X3,X2))).
% 0.81/1.91 cnf(i_0_273, axiom, (X1!=X2|~strictly_less_than(X1,X3)|strictly_less_than(X2,X3))).
% 0.81/1.91 cnf(i_0_274, axiom, (X1!=X2|~strictly_less_than(X3,X1)|strictly_less_than(X3,X2))).
% 0.81/1.91 cnf(i_0_275, axiom, (X1!=X2|~contains_slb(X1,X3)|contains_slb(X2,X3))).
% 0.81/1.91 cnf(i_0_276, axiom, (X1!=X2|~contains_slb(X3,X1)|contains_slb(X3,X2))).
% 0.81/1.91 cnf(i_0_277, axiom, (X1!=X2|~pair_in_list(X1,X3,X4)|pair_in_list(X2,X3,X4))).
% 0.81/1.91 cnf(i_0_278, axiom, (X1!=X2|~pair_in_list(X3,X1,X4)|pair_in_list(X3,X2,X4))).
% 0.81/1.91 cnf(i_0_279, axiom, (X1!=X2|~pair_in_list(X3,X4,X1)|pair_in_list(X3,X4,X2))).
% 0.81/1.91 cnf(i_0_280, axiom, (X1!=X2|~contains_cpq(X1,X3)|contains_cpq(X2,X3))).
% 0.81/1.91 cnf(i_0_281, axiom, (X1!=X2|~contains_cpq(X3,X1)|contains_cpq(X3,X2))).
% 0.81/1.91 cnf(i_0_282, axiom, (X1!=X2|~ok(X1)|ok(X2))).
% 0.81/1.91 cnf(i_0_283, axiom, (X1!=X2|~contains_pq(X1,X3)|contains_pq(X2,X3))).
% 0.81/1.91 cnf(i_0_284, axiom, (X1!=X2|~contains_pq(X3,X1)|contains_pq(X3,X2))).
% 0.81/1.91 cnf(i_0_285, axiom, (X1!=X2|~succ_cpq(X1,X3)|succ_cpq(X2,X3))).
% 0.81/1.91 cnf(i_0_286, axiom, (X1!=X2|~succ_cpq(X3,X1)|succ_cpq(X3,X2))).
% 0.81/1.91 cnf(i_0_287, plain, (contains_slb(insert_slb(X1,pair(X2,X3)),X2)), inference(equality_inference,[],[168])).
% 0.81/1.91 cnf(i_0_288, plain, (contains_pq(insert_pq(X1,X2),X2)), inference(equality_inference,[],[192])).
% 0.81/1.91 cnf(i_0_289, plain, (X1=remove_pq(insert_pq(X1,X2),X2)), inference(scs_inference,[],[i_0_196,i_0_222])).
% 0.81/1.91 cnf(i_0_290, plain, (triple(esk5_0,create_slb,esk7_0)!=triple(esk6_0,create_slb,esk8_0)), inference(scs_inference,[],[i_0_142,i_0_196,i_0_222,i_0_246])).
% 0.81/1.91 cnf(i_0_291, plain, (issmallestelement_pq(X1,bottom)), inference(scs_inference,[],[i_0_142,i_0_217,i_0_196,i_0_222,i_0_246,i_0_176])).
% 0.81/1.91 cnf(i_0_292, plain, (less_than(bottom,X1)), inference(rename_variables,[],[i_0_217])).
% 0.81/1.91 cnf(i_0_293, plain, (~less_than(X1,esk1_2(X2,X1))|issmallestelement_pq(X2,X1)), inference(rename_variables,[],[i_0_176])).
% 0.81/1.91 cnf(i_0_294, plain, (issmallestelement_pq(create_pq,X1)), inference(scs_inference,[],[i_0_142,i_0_212,i_0_217,i_0_196,i_0_222,i_0_246,i_0_176,i_0_188])).
% 0.81/1.91 cnf(i_0_295, plain, (~contains_pq(create_pq,X1)), inference(rename_variables,[],[i_0_212])).
% 0.81/1.91 cnf(i_0_296, plain, (contains_pq(X1,esk1_2(X1,X2))|issmallestelement_pq(X1,X2)), inference(rename_variables,[],[i_0_188])).
% 0.81/1.91 cnf(i_0_297, plain, (pi_sharp_remove(insert_pq(X1,X2),X2)), inference(scs_inference,[],[i_0_142,i_0_288,i_0_212,i_0_217,i_0_196,i_0_222,i_0_246,i_0_176,i_0_188,i_0_197])).
% 0.81/1.91 cnf(i_0_298, plain, (~contains_pq(X1,X2)|pi_sharp_remove(X1,X2)), inference(rename_variables,[],[i_0_197])).
% 0.81/1.91 cnf(i_0_299, plain, (i(triple(esk5_0,create_slb,esk7_0))!=remove_pq(insert_pq(i(triple(esk6_0,create_slb,esk8_0)),X1),X1)), inference(scs_inference,[],[i_0_142,i_0_288,i_0_212,i_0_217,i_0_196,i_0_222,i_0_246,i_0_176,i_0_188,i_0_197,i_0_223])).
% 0.81/1.91 cnf(i_0_300, plain, (remove_pq(insert_pq(X1,X2),X2)=X1), inference(rename_variables,[],[i_0_196])).
% 0.81/1.91 cnf(i_0_301, plain, (insert_slb(X1,pair(X2,X3))!=create_slb), inference(scs_inference,[],[i_0_142,i_0_288,i_0_212,i_0_217,i_0_219,i_0_196,i_0_173,i_0_222,i_0_246,i_0_176,i_0_188,i_0_197,i_0_223,i_0_256])).
% 0.81/1.91 cnf(i_0_302, plain, (insert_pq(X1,X2)!=create_pq), inference(scs_inference,[],[i_0_142,i_0_288,i_0_212,i_0_217,i_0_219,i_0_220,i_0_208,i_0_196,i_0_173,i_0_222,i_0_246,i_0_176,i_0_188,i_0_197,i_0_223,i_0_256,i_0_270])).
% 0.81/1.91 cnf(i_0_303, plain, (~contains_slb(remove_pq(insert_pq(create_slb,X1),X1),X2)), inference(scs_inference,[],[i_0_142,i_0_288,i_0_211,i_0_212,i_0_217,i_0_219,i_0_220,i_0_208,i_0_196,i_0_300,i_0_173,i_0_222,i_0_246,i_0_176,i_0_188,i_0_197,i_0_223,i_0_256,i_0_270,i_0_275])).
% 0.81/1.91 cnf(i_0_304, plain, (remove_pq(insert_pq(X1,X2),X2)=X1), inference(rename_variables,[],[i_0_196])).
% 0.81/1.91 cnf(i_0_305, plain, (~pair_in_list(remove_pq(insert_pq(create_slb,X1),X1),X2,X3)), inference(scs_inference,[],[i_0_142,i_0_288,i_0_172,i_0_211,i_0_212,i_0_217,i_0_219,i_0_220,i_0_208,i_0_196,i_0_300,i_0_304,i_0_173,i_0_222,i_0_246,i_0_176,i_0_188,i_0_197,i_0_223,i_0_256,i_0_270,i_0_275,i_0_277])).
% 0.81/1.92 cnf(i_0_306, plain, (remove_pq(insert_pq(X1,X2),X2)=X1), inference(rename_variables,[],[i_0_196])).
% 0.81/1.92 cnf(i_0_307, plain, (~contains_pq(remove_pq(insert_pq(create_pq,X1),X1),X2)), inference(scs_inference,[],[i_0_142,i_0_288,i_0_172,i_0_211,i_0_212,i_0_295,i_0_217,i_0_219,i_0_220,i_0_208,i_0_196,i_0_300,i_0_304,i_0_306,i_0_173,i_0_222,i_0_246,i_0_176,i_0_188,i_0_197,i_0_223,i_0_256,i_0_270,i_0_275,i_0_277,i_0_283])).
% 0.81/1.92 cnf(i_0_308, plain, (remove_pq(insert_pq(X1,X2),X2)=X1), inference(rename_variables,[],[i_0_196])).
% 0.81/1.92 cnf(i_0_309, plain, (pi_sharp_removemin(insert_pq(X1,bottom),bottom)), inference(scs_inference,[],[i_0_142,i_0_288,i_0_172,i_0_211,i_0_212,i_0_295,i_0_217,i_0_219,i_0_220,i_0_208,i_0_196,i_0_300,i_0_304,i_0_306,i_0_173,i_0_222,i_0_246,i_0_176,i_0_188,i_0_197,i_0_223,i_0_256,i_0_270,i_0_275,i_0_277,i_0_283,i_0_184])).
% 0.81/1.92 cnf(i_0_310, plain, (contains_pq(insert_pq(X1,X2),X2)), inference(rename_variables,[],[i_0_288])).
% 0.81/1.92 cnf(i_0_311, plain, (~contains_pq(X1,X2)|~issmallestelement_pq(X1,X2)|pi_sharp_removemin(X1,X2)), inference(rename_variables,[],[i_0_184])).
% 0.81/1.92 cnf(i_0_312, plain, (pi_sharp_find_min(insert_pq(X1,bottom),bottom)), inference(scs_inference,[],[i_0_142,i_0_288,i_0_310,i_0_172,i_0_211,i_0_212,i_0_295,i_0_217,i_0_219,i_0_220,i_0_208,i_0_196,i_0_300,i_0_304,i_0_306,i_0_173,i_0_222,i_0_246,i_0_176,i_0_188,i_0_197,i_0_223,i_0_256,i_0_270,i_0_275,i_0_277,i_0_283,i_0_184,i_0_185])).
% 0.81/1.92 cnf(i_0_313, plain, (contains_pq(insert_pq(X1,X2),X2)), inference(rename_variables,[],[i_0_288])).
% 0.81/1.92 cnf(i_0_314, plain, (~contains_pq(X1,X2)|~issmallestelement_pq(X1,X2)|pi_sharp_find_min(X1,X2)), inference(rename_variables,[],[i_0_185])).
% 0.81/1.92 cnf(i_0_315, plain, (check_cpq(X1)|triple(X2,create_slb,X3)!=X1), inference(scs_inference,[],[i_0_142,i_0_288,i_0_310,i_0_172,i_0_211,i_0_212,i_0_295,i_0_217,i_0_219,i_0_220,i_0_208,i_0_196,i_0_300,i_0_304,i_0_306,i_0_164,i_0_173,i_0_222,i_0_246,i_0_176,i_0_188,i_0_197,i_0_223,i_0_256,i_0_270,i_0_275,i_0_277,i_0_283,i_0_184,i_0_185,i_0_255])).
% 0.81/1.92 cnf(i_0_316, 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_142,i_0_288,i_0_310,i_0_216,i_0_172,i_0_211,i_0_212,i_0_295,i_0_217,i_0_219,i_0_220,i_0_208,i_0_196,i_0_300,i_0_304,i_0_306,i_0_164,i_0_173,i_0_222,i_0_246,i_0_176,i_0_188,i_0_197,i_0_223,i_0_256,i_0_270,i_0_275,i_0_277,i_0_283,i_0_184,i_0_185,i_0_255,i_0_136])).
% 0.81/1.92 cnf(i_0_317, 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_136])).
% 0.81/1.92 cnf(i_0_318, 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_142,i_0_288,i_0_310,i_0_216,i_0_172,i_0_211,i_0_212,i_0_295,i_0_217,i_0_219,i_0_220,i_0_208,i_0_196,i_0_300,i_0_304,i_0_306,i_0_164,i_0_173,i_0_222,i_0_246,i_0_176,i_0_188,i_0_197,i_0_223,i_0_256,i_0_270,i_0_275,i_0_277,i_0_283,i_0_184,i_0_185,i_0_255,i_0_136,i_0_139])).
% 0.81/1.92 cnf(i_0_319, plain, (~check_cpq(triple(X1,insert_slb(X2,pair(X3,X4)),X5))|~strictly_less_than(X3,X4)), inference(rename_variables,[],[i_0_139])).
% 0.81/1.92 cnf(i_0_321, plain, (check_cpq(triple(X1,create_slb,X2))), inference(equality_inference,[],[315])).
% 0.81/1.92 cnf(i_0_322, plain, (check_cpq(remove_pq(insert_pq(triple(X1,create_slb,X2),X3),X3))), inference(scs_inference,[],[i_0_289,i_0_315])).
% 0.81/1.92 cnf(i_0_323, plain, (X1=remove_pq(insert_pq(X1,X2),X2)), inference(rename_variables,[],[i_0_289])).
% 0.81/1.92 cnf(i_0_324, plain, (issmallestelement_pq(remove_pq(insert_pq(create_pq,X1),X1),X2)), inference(scs_inference,[],[i_0_289,i_0_307,i_0_315,i_0_188])).
% 0.81/1.92 cnf(i_0_325, plain, (~contains_pq(remove_pq(insert_pq(create_pq,X1),X1),X2)), inference(rename_variables,[],[i_0_307])).
% 0.81/1.92 cnf(i_0_326, plain, (contains_pq(X1,esk1_2(X1,X2))|issmallestelement_pq(X1,X2)), inference(rename_variables,[],[i_0_188])).
% 0.81/1.92 cnf(i_0_327, plain, (create_slb=update_slb(create_slb,X1)), inference(scs_inference,[],[i_0_289,i_0_307,i_0_218,i_0_315,i_0_188,i_0_222])).
% 0.81/1.92 cnf(i_0_328, plain, (insert_slb(X1,pair(X2,X3))!=update_slb(create_slb,X4)), inference(scs_inference,[],[i_0_289,i_0_307,i_0_301,i_0_218,i_0_315,i_0_188,i_0_222,i_0_223])).
% 0.81/1.92 cnf(i_0_329, 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_289,i_0_323,i_0_307,i_0_301,i_0_218,i_0_315,i_0_188,i_0_222,i_0_223,i_0_255])).
% 0.81/1.92 cnf(i_0_330, plain, (X1=remove_pq(insert_pq(X1,X2),X2)), inference(rename_variables,[],[i_0_289])).
% 0.81/1.92 cnf(i_0_331, plain, (~contains_slb(update_slb(create_slb,X1),X2)), inference(scs_inference,[],[i_0_289,i_0_323,i_0_307,i_0_301,i_0_211,i_0_218,i_0_315,i_0_188,i_0_222,i_0_223,i_0_255,i_0_275])).
% 0.81/1.92 cnf(i_0_332, plain, (~contains_pq(lookup_slb(insert_slb(X1,pair(X2,create_pq)),X2),X3)), inference(scs_inference,[],[i_0_289,i_0_323,i_0_307,i_0_301,i_0_211,i_0_218,i_0_169,i_0_212,i_0_315,i_0_188,i_0_222,i_0_223,i_0_255,i_0_275,i_0_283])).
% 0.81/1.92 cnf(i_0_333, plain, (lookup_slb(insert_slb(X1,pair(X2,X3)),X2)=X3), inference(rename_variables,[],[i_0_169])).
% 0.81/1.92 cnf(i_0_334, plain, (~pair_in_list(update_slb(create_slb,X1),X2,X3)), inference(scs_inference,[],[i_0_289,i_0_323,i_0_307,i_0_301,i_0_172,i_0_211,i_0_218,i_0_169,i_0_212,i_0_315,i_0_188,i_0_222,i_0_223,i_0_255,i_0_275,i_0_283,i_0_277])).
% 0.81/1.92 cnf(i_0_335, plain, (issmallestelement_pq(lookup_slb(insert_slb(X1,pair(X2,create_pq)),X2),X3)), inference(scs_inference,[],[i_0_332,i_0_188])).
% 0.81/1.92 cnf(i_0_336, plain, (~contains_pq(lookup_slb(insert_slb(X1,pair(X2,create_pq)),X2),X3)), inference(rename_variables,[],[i_0_332])).
% 0.81/1.92 cnf(i_0_337, plain, (contains_pq(X1,esk1_2(X1,X2))|issmallestelement_pq(X1,X2)), inference(rename_variables,[],[i_0_188])).
% 0.81/1.92 cnf(i_0_338, plain, (triple(X1,create_slb,bad)=findmin_cpq_eff(triple(X1,create_slb,X2))), inference(scs_inference,[],[i_0_332,i_0_157,i_0_188,i_0_222])).
% 0.81/1.92 cnf(i_0_339, plain, (remove_slb(insert_slb(findmin_cpq_eff(triple(X1,create_slb,X2)),pair(X3,X4)),X3)=triple(X1,create_slb,bad)), inference(scs_inference,[],[i_0_332,i_0_157,i_0_170,i_0_188,i_0_222,i_0_223])).
% 0.81/1.92 cnf(i_0_340, plain, (remove_slb(insert_slb(X1,pair(X2,X3)),X2)=X1), inference(rename_variables,[],[i_0_170])).
% 0.81/1.92 cnf(i_0_341, plain, (~contains_slb(remove_slb(insert_slb(create_slb,pair(X1,X2)),X1),X3)), inference(scs_inference,[],[i_0_332,i_0_211,i_0_157,i_0_170,i_0_340,i_0_188,i_0_222,i_0_223,i_0_275])).
% 0.81/1.92 cnf(i_0_342, plain, (remove_slb(insert_slb(X1,pair(X2,X3)),X2)=X1), inference(rename_variables,[],[i_0_170])).
% 0.81/1.92 cnf(i_0_343, 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_332,i_0_336,i_0_211,i_0_157,i_0_170,i_0_340,i_0_342,i_0_188,i_0_222,i_0_223,i_0_275,i_0_283])).
% 0.81/1.92 cnf(i_0_344, plain, (remove_slb(insert_slb(X1,pair(X2,X3)),X2)=X1), inference(rename_variables,[],[i_0_170])).
% 0.81/1.92 cnf(i_0_345, plain, (~pair_in_list(remove_slb(insert_slb(create_slb,pair(X1,X2)),X1),X3,X4)), inference(scs_inference,[],[i_0_332,i_0_336,i_0_172,i_0_211,i_0_157,i_0_170,i_0_340,i_0_342,i_0_344,i_0_188,i_0_222,i_0_223,i_0_275,i_0_283,i_0_277])).
% 0.81/1.92 cnf(i_0_346, plain, (remove_slb(insert_slb(X1,pair(X2,X3)),X2)=X1), inference(rename_variables,[],[i_0_170])).
% 0.81/1.92 cnf(i_0_347, plain, (check_cpq(findmin_cpq_eff(triple(X1,create_slb,X2)))), inference(scs_inference,[],[i_0_332,i_0_336,i_0_172,i_0_211,i_0_157,i_0_170,i_0_340,i_0_342,i_0_344,i_0_188,i_0_222,i_0_223,i_0_275,i_0_283,i_0_277,i_0_315])).
% 0.81/1.92 cnf(i_0_348, plain, (check_cpq(remove_pq(insert_pq(findmin_cpq_eff(triple(X1,create_slb,X2)),X3),X3))), inference(scs_inference,[],[i_0_289,i_0_332,i_0_336,i_0_172,i_0_211,i_0_157,i_0_170,i_0_340,i_0_342,i_0_344,i_0_188,i_0_222,i_0_223,i_0_275,i_0_283,i_0_277,i_0_315,i_0_255])).
% 0.81/1.92 cnf(i_0_349, plain, (X1=remove_pq(insert_pq(X1,X2),X2)), inference(rename_variables,[],[i_0_289])).
% 0.81/1.92 cnf(i_0_350, plain, (triple(X1,create_slb,bad)=remove_slb(insert_slb(findmin_cpq_eff(triple(X1,create_slb,X2)),pair(X3,X4)),X3)), inference(scs_inference,[],[i_0_339,i_0_222])).
% 0.81/1.92 cnf(i_0_351, plain, (remove_slb(insert_slb(findmin_cpq_eff(triple(X1,create_slb,X2)),pair(X3,X4)),X3)=findmin_cpq_eff(triple(X1,create_slb,X5))), inference(scs_inference,[],[i_0_339,i_0_338,i_0_222,i_0_223])).
% 0.81/1.92 cnf(i_0_352, plain, (triple(X1,create_slb,bad)=findmin_cpq_eff(triple(X1,create_slb,X2))), inference(rename_variables,[],[i_0_338])).
% 0.81/1.92 cnf(i_0_353, plain, (~contains_pq(i(triple(X1,create_slb,X2)),X3)), inference(scs_inference,[],[i_0_339,i_0_338,i_0_165,i_0_212,i_0_222,i_0_223,i_0_283])).
% 0.81/1.92 cnf(i_0_354, plain, (~contains_slb(lookup_slb(insert_slb(X1,pair(X2,create_slb)),X2),X3)), inference(scs_inference,[],[i_0_339,i_0_338,i_0_211,i_0_165,i_0_169,i_0_212,i_0_222,i_0_223,i_0_283,i_0_275])).
% 0.81/1.92 cnf(i_0_355, plain, (lookup_slb(insert_slb(X1,pair(X2,X3)),X2)=X3), inference(rename_variables,[],[i_0_169])).
% 0.81/1.92 cnf(i_0_356, plain, (~pair_in_list(lookup_slb(insert_slb(X1,pair(X2,create_slb)),X2),X3,X4)), inference(scs_inference,[],[i_0_339,i_0_338,i_0_172,i_0_211,i_0_165,i_0_169,i_0_355,i_0_212,i_0_222,i_0_223,i_0_283,i_0_275,i_0_277])).
% 0.81/1.92 cnf(i_0_357, plain, (lookup_slb(insert_slb(X1,pair(X2,X3)),X2)=X3), inference(rename_variables,[],[i_0_169])).
% 0.81/1.92 cnf(i_0_358, plain, (issmallestelement_pq(i(triple(X1,create_slb,X2)),X3)), inference(scs_inference,[],[i_0_339,i_0_338,i_0_172,i_0_211,i_0_165,i_0_169,i_0_355,i_0_212,i_0_222,i_0_223,i_0_283,i_0_275,i_0_277,i_0_188])).
% 0.81/1.92 cnf(i_0_359, plain, (contains_pq(X1,esk1_2(X1,X2))|issmallestelement_pq(X1,X2)), inference(rename_variables,[],[i_0_188])).
% 0.81/1.92 cnf(i_0_360, plain, (check_cpq(remove_slb(insert_slb(findmin_cpq_eff(triple(X1,create_slb,X2)),pair(X3,X4)),X3))), inference(scs_inference,[],[i_0_339,i_0_338,i_0_172,i_0_211,i_0_165,i_0_169,i_0_355,i_0_212,i_0_222,i_0_223,i_0_283,i_0_275,i_0_277,i_0_188,i_0_315])).
% 0.81/1.92 cnf(i_0_361, plain, (findmin_cpq_eff(triple(X1,create_slb,X2))=remove_slb(insert_slb(findmin_cpq_eff(triple(X1,create_slb,X3)),pair(X4,X5)),X4)), inference(scs_inference,[],[i_0_351,i_0_222])).
% 0.81/1.92 cnf(i_0_362, plain, (remove_slb(insert_slb(findmin_cpq_eff(triple(X1,create_slb,X2)),pair(X3,X4)),X3)=remove_slb(insert_slb(findmin_cpq_eff(triple(X1,create_slb,X5)),pair(X6,X7)),X6)), inference(scs_inference,[],[i_0_351,i_0_350,i_0_339,i_0_222,i_0_223])).
% 0.81/1.92 cnf(i_0_363, plain, (triple(X1,create_slb,bad)=remove_slb(insert_slb(findmin_cpq_eff(triple(X1,create_slb,X2)),pair(X3,X4)),X3)), inference(rename_variables,[],[i_0_350])).
% 0.81/1.92 cnf(i_0_364, plain, (~contains_pq(remove_slb(insert_slb(i(triple(X1,create_slb,X2)),pair(X3,X4)),X3),X5)), inference(scs_inference,[],[i_0_351,i_0_350,i_0_339,i_0_353,i_0_170,i_0_222,i_0_223,i_0_283])).
% 0.81/1.92 cnf(i_0_365, plain, (remove_slb(insert_slb(X1,pair(X2,X3)),X2)=X1), inference(rename_variables,[],[i_0_170])).
% 0.81/1.92 cnf(i_0_366, plain, (~contains_slb(remove_slb(insert_slb(lookup_slb(insert_slb(X1,pair(X2,create_slb)),X2),pair(X3,X4)),X3),X5)), inference(scs_inference,[],[i_0_351,i_0_350,i_0_339,i_0_354,i_0_353,i_0_170,i_0_365,i_0_222,i_0_223,i_0_283,i_0_275])).
% 0.81/1.92 cnf(i_0_367, plain, (remove_slb(insert_slb(X1,pair(X2,X3)),X2)=X1), inference(rename_variables,[],[i_0_170])).
% 0.81/1.92 cnf(i_0_368, plain, (~pair_in_list(remove_slb(insert_slb(lookup_slb(insert_slb(X1,pair(X2,create_slb)),X2),pair(X3,X4)),X3),X5,X6)), inference(scs_inference,[],[i_0_351,i_0_350,i_0_339,i_0_356,i_0_354,i_0_353,i_0_170,i_0_365,i_0_367,i_0_222,i_0_223,i_0_283,i_0_275,i_0_277])).
% 0.81/1.92 cnf(i_0_369, plain, (remove_slb(insert_slb(X1,pair(X2,X3)),X2)=X1), inference(rename_variables,[],[i_0_170])).
% 0.81/1.92 cnf(i_0_370, plain, (issmallestelement_pq(remove_slb(insert_slb(i(triple(X1,create_slb,X2)),pair(X3,X4)),X3),X5)), inference(scs_inference,[],[i_0_351,i_0_350,i_0_339,i_0_356,i_0_354,i_0_353,i_0_170,i_0_365,i_0_367,i_0_222,i_0_223,i_0_283,i_0_275,i_0_277,i_0_188])).
% 0.81/1.92 cnf(i_0_371, plain, (contains_pq(X1,esk1_2(X1,X2))|issmallestelement_pq(X1,X2)), inference(rename_variables,[],[i_0_188])).
% 0.81/1.92 cnf(i_0_372, plain, (triple(insert_pqp(X1,X2),insert_slb(X3,pair(X2,bottom)),X4)=insert_cpq(triple(X1,X3,X4),X2)), inference(scs_inference,[],[i_0_145,i_0_222])).
% 0.81/1.92 cnf(i_0_373, plain, (remove_pq(insert_pq(insert_cpq(triple(X1,X2,X3),X4),X5),X5)=triple(insert_pqp(X1,X4),insert_slb(X2,pair(X4,bottom)),X3)), inference(scs_inference,[],[i_0_145,i_0_196,i_0_222,i_0_223])).
% 0.81/1.92 cnf(i_0_374, plain, (remove_pq(insert_pq(X1,X2),X2)=X1), inference(rename_variables,[],[i_0_196])).
% 0.81/1.92 cnf(i_0_375, plain, (~contains_pq(remove_pq(insert_pq(lookup_slb(insert_slb(X1,pair(X2,create_pq)),X2),X3),X3),X4)), inference(scs_inference,[],[i_0_332,i_0_145,i_0_196,i_0_374,i_0_222,i_0_223,i_0_283])).
% 0.81/1.92 cnf(i_0_376, plain, (remove_pq(insert_pq(X1,X2),X2)=X1), inference(rename_variables,[],[i_0_196])).
% 0.81/1.92 cnf(i_0_377, plain, (~contains_slb(remove_pq(insert_pq(remove_slb(insert_slb(create_slb,pair(X1,X2)),X1),X3),X3),X4)), inference(scs_inference,[],[i_0_341,i_0_332,i_0_145,i_0_196,i_0_374,i_0_376,i_0_222,i_0_223,i_0_283,i_0_275])).
% 0.81/1.92 cnf(i_0_378, plain, (remove_pq(insert_pq(X1,X2),X2)=X1), inference(rename_variables,[],[i_0_196])).
% 0.81/1.92 cnf(i_0_379, plain, (~pair_in_list(remove_pq(insert_pq(remove_slb(insert_slb(create_slb,pair(X1,X2)),X1),X3),X3),X4,X5)), inference(scs_inference,[],[i_0_345,i_0_341,i_0_332,i_0_145,i_0_196,i_0_374,i_0_376,i_0_378,i_0_222,i_0_223,i_0_283,i_0_275,i_0_277])).
% 0.81/1.92 cnf(i_0_380, plain, (remove_pq(insert_pq(X1,X2),X2)=X1), inference(rename_variables,[],[i_0_196])).
% 0.81/1.92 cnf(i_0_381, plain, (issmallestelement_pq(remove_pq(insert_pq(lookup_slb(insert_slb(X1,pair(X2,create_pq)),X2),X3),X3),X4)), inference(scs_inference,[],[i_0_345,i_0_341,i_0_332,i_0_145,i_0_196,i_0_374,i_0_376,i_0_378,i_0_222,i_0_223,i_0_283,i_0_275,i_0_277,i_0_188])).
% 0.81/1.92 cnf(i_0_382, plain, (contains_pq(X1,esk1_2(X1,X2))|issmallestelement_pq(X1,X2)), inference(rename_variables,[],[i_0_188])).
% 0.81/1.92 cnf(i_0_383, plain, (triple(insert_pqp(X1,X2),insert_slb(X3,pair(X2,bottom)),X4)=remove_pq(insert_pq(insert_cpq(triple(X1,X3,X4),X2),X5),X5)), inference(scs_inference,[],[i_0_373,i_0_222])).
% 0.81/1.92 cnf(i_0_384, plain, (~contains_pq(lookup_slb(insert_slb(X1,pair(X2,i(triple(X3,create_slb,X4)))),X2),X5)), inference(scs_inference,[],[i_0_373,i_0_353,i_0_169,i_0_222,i_0_283])).
% 0.81/1.92 cnf(i_0_385, plain, (lookup_slb(insert_slb(X1,pair(X2,X3)),X2)=X3), inference(rename_variables,[],[i_0_169])).
% 0.81/1.92 cnf(i_0_386, plain, (lookup_slb(insert_slb(X1,pair(X2,findmin_cpq_res(triple(X3,create_slb,X4)))),X2)=bottom), inference(scs_inference,[],[i_0_373,i_0_353,i_0_166,i_0_169,i_0_385,i_0_222,i_0_283,i_0_223])).
% 0.81/1.92 cnf(i_0_387, plain, (lookup_slb(insert_slb(X1,pair(X2,X3)),X2)=X3), inference(rename_variables,[],[i_0_169])).
% 0.81/1.92 cnf(i_0_388, plain, (issmallestelement_pq(lookup_slb(insert_slb(X1,pair(X2,i(triple(X3,create_slb,X4)))),X2),X5)), inference(scs_inference,[],[i_0_373,i_0_353,i_0_166,i_0_169,i_0_385,i_0_222,i_0_283,i_0_223,i_0_188])).
% 0.81/1.92 cnf(i_0_389, plain, (contains_pq(X1,esk1_2(X1,X2))|issmallestelement_pq(X1,X2)), inference(rename_variables,[],[i_0_188])).
% 0.81/1.92 cnf(i_0_390, plain, (bottom=lookup_slb(insert_slb(X1,pair(X2,findmin_cpq_res(triple(X3,create_slb,X4)))),X2)), inference(scs_inference,[],[i_0_386,i_0_222])).
% 0.81/1.92 cnf(i_0_391, plain, (~contains_slb(remove_slb(insert_slb(remove_slb(insert_slb(create_slb,pair(X1,X2)),X1),pair(X3,X4)),X3),X5)), inference(scs_inference,[],[i_0_386,i_0_341,i_0_170,i_0_222,i_0_275])).
% 0.81/1.92 cnf(i_0_392, plain, (remove_slb(insert_slb(X1,pair(X2,X3)),X2)=X1), inference(rename_variables,[],[i_0_170])).
% 0.81/1.92 cnf(i_0_393, plain, (~pair_in_list(remove_slb(insert_slb(remove_slb(insert_slb(create_slb,pair(X1,X2)),X1),pair(X3,X4)),X3),X5,X6)), inference(scs_inference,[],[i_0_386,i_0_345,i_0_341,i_0_170,i_0_392,i_0_222,i_0_275,i_0_277])).
% 0.81/1.92 cnf(i_0_394, plain, (remove_slb(insert_slb(X1,pair(X2,X3)),X2)=X1), inference(rename_variables,[],[i_0_170])).
% 0.81/1.92 cnf(i_0_395, plain, (insert_pq(X1,X2)!=i(triple(X3,create_slb,X4))), inference(scs_inference,[],[i_0_386,i_0_302,i_0_345,i_0_341,i_0_165,i_0_170,i_0_392,i_0_222,i_0_275,i_0_277,i_0_223])).
% 0.81/1.92 cnf(i_0_396, plain, (insert_pq(i(triple(X1,X2,X3)),X4)=i(triple(X1,insert_slb(X2,pair(X4,X5)),X3))), inference(scs_inference,[],[i_0_137,i_0_222])).
% 0.81/1.92 cnf(i_0_397, plain, (~contains_pq(remove_pq(insert_pq(i(triple(X1,create_slb,X2)),X3),X3),X4)), inference(scs_inference,[],[i_0_353,i_0_137,i_0_196,i_0_222,i_0_283])).
% 0.81/1.92 cnf(i_0_398, plain, (remove_pq(insert_pq(X1,X2),X2)=X1), inference(rename_variables,[],[i_0_196])).
% 0.81/1.92 cnf(i_0_399, plain, (~contains_slb(remove_pq(insert_pq(lookup_slb(insert_slb(X1,pair(X2,create_slb)),X2),X3),X3),X4)), inference(scs_inference,[],[i_0_354,i_0_353,i_0_137,i_0_196,i_0_398,i_0_222,i_0_283,i_0_275])).
% 0.81/1.92 cnf(i_0_400, plain, (remove_pq(insert_pq(X1,X2),X2)=X1), inference(rename_variables,[],[i_0_196])).
% 0.81/1.92 cnf(i_0_401, plain, (~pair_in_list(remove_pq(insert_pq(lookup_slb(insert_slb(X1,pair(X2,create_slb)),X2),X3),X3),X4,X5)), inference(scs_inference,[],[i_0_356,i_0_354,i_0_353,i_0_137,i_0_196,i_0_398,i_0_400,i_0_222,i_0_283,i_0_275,i_0_277])).
% 0.81/1.92 cnf(i_0_402, plain, (remove_pq(insert_pq(X1,X2),X2)=X1), inference(rename_variables,[],[i_0_196])).
% 0.81/1.92 cnf(i_0_403, plain, (remove_pq(insert_pq(findmin_cpq_res(triple(X1,create_slb,X2)),X3),X3)=bottom), inference(scs_inference,[],[i_0_356,i_0_354,i_0_353,i_0_137,i_0_166,i_0_196,i_0_398,i_0_400,i_0_402,i_0_222,i_0_283,i_0_275,i_0_277,i_0_223])).
% 0.81/1.92 cnf(i_0_404, plain, (remove_pq(insert_pq(X1,X2),X2)=X1), inference(rename_variables,[],[i_0_196])).
% 0.81/1.92 cnf(i_0_405, plain, (issmallestelement_pq(remove_pq(insert_pq(i(triple(X1,create_slb,X2)),X3),X3),X4)), inference(scs_inference,[],[i_0_356,i_0_354,i_0_353,i_0_137,i_0_166,i_0_196,i_0_398,i_0_400,i_0_402,i_0_222,i_0_283,i_0_275,i_0_277,i_0_223,i_0_188])).
% 0.81/1.92 cnf(i_0_406, plain, (contains_pq(X1,esk1_2(X1,X2))|issmallestelement_pq(X1,X2)), inference(rename_variables,[],[i_0_188])).
% 0.81/1.92 cnf(i_0_407, plain, (bottom=remove_pq(insert_pq(findmin_cpq_res(triple(X1,create_slb,X2)),X3),X3)), inference(scs_inference,[],[i_0_403,i_0_222])).
% 0.81/1.92 cnf(i_0_408, plain, (i(triple(esk5_0,create_slb,esk7_0))!=remove_slb(insert_slb(i(triple(esk6_0,create_slb,esk8_0)),pair(X1,X2)),X1)), inference(scs_inference,[],[i_0_142,i_0_403,i_0_170,i_0_222,i_0_223])).
% 0.81/1.92 cnf(i_0_409, plain, (remove_slb(insert_slb(X1,pair(X2,X3)),X2)=X1), inference(rename_variables,[],[i_0_170])).
% 0.81/1.92 cnf(i_0_410, plain, (create_pq=i(triple(X1,create_slb,X2))), inference(scs_inference,[],[i_0_165,i_0_222])).
% 0.81/1.92 cnf(i_0_411, plain, (i(triple(esk5_0,create_slb,esk7_0))!=create_pq), inference(scs_inference,[],[i_0_142,i_0_165,i_0_222,i_0_223])).
% 0.81/1.92 cnf(i_0_412,plain, ($false), inference(scs_inference,[],[i_0+411, i_0_165]), ['proof']).
% 0.81/1.92 % SZS output end CNFRefutation
% 0.81/1.92 % Total time : 1.273s
%------------------------------------------------------------------------------