%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWW679_1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:30:08 PM UTC 2026
% Result : Theorem 2.12s 1.29s
% Output : CNFRefutation 2.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW679_1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n015.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 22:53:11 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.40 Running TFA theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s tfa_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 2.12/1.29 % SZS status Started for theBenchmark.p
% 2.12/1.29 ERROR - "ProverProcess:heur/schedule_none:304.9999725818634" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("undefined enum value")
% 2.12/1.29 Fatal error: exception Failure("undefined enum value")
% 2.12/1.29 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --schedule none --sub_typing false --suppress_sat_res true --tptp_safe_out true --stats_out none --out_options none --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 101.67 --show_fool true" --time_out_real 305.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_4j3i12dt/f53m9fg5 2>> /export/starexec/sandbox/tmp/iprover_out_4j3i12dt/f53m9fg5_error
% 2.12/1.29 ERROR - "ProverProcess:heur/vip_65520:11.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("undefined enum value")
% 2.12/1.29 Fatal error: exception Failure("undefined enum value")
% 2.12/1.29 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --comb_mode time_based --comb_res_mult 6 --comb_sup_deep_mult 0 --comb_sup_mult 6 --conj_cone_tolerance 1.8969679945890683 --demod_completeness_check fullold --demod_use_ground false --extra_neg_conj all_neg --instantiation_flag false --out_options none --preprocessed_out false --preprocessing_flag false --prolific_symb_bound 1024 --proof_out true --prop_solver_per_cl 512 --res_to_smt_solver false --resolution_flag true --schedule none --share_sel_clauses true --stats_out none --subs_bck_mult 16 --sup_bw_gjoin_interval 100 --sup_cache_sim none --sup_full_bw "[Subsumption;SubsumptionRes;UnitSubsAndRes]" --sup_full_fixpoint false --sup_full_fw "[]" --sup_fun_splitting false --sup_immed_bw_immed "[Subsumption;SubsumptionRes;UnitSubsAndRes]" --sup_immed_bw_main "[SubsumptionRes;UnitSubsAndRes;FullSubsAndRes;Demod;ACDemod]" --sup_immed_fixpoint false --sup_immed_fw_immed "[Subsumption;SubsumptionRes;FullSubsAndRes;Demod;LightNorm;ACDemod]" --sup_immed_fw_main "[Subsumption;UnitSubsAndRes;FullSubsAndRes;Demod;LightNorm;ACNormalisation;GroundJoinability;Connectedness]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_fixpoint false --sup_main_fixpoint true --sup_ordering lpo --sup_passive_queue_type priority_queues --sup_passive_queues "[[+has_eq;-has_eq];[-num_var;-num_var];[+conj_dist;+ground;-max_atom_input_occur]]" --sup_passive_queues_freq "[1;4;4]" --sup_prop_simpl_given false --sup_prop_simpl_new false --sup_score sim_d_gen --sup_share_max_num_cl 10 --sup_share_score_frac 0.2 --sup_smt_interval 32 --sup_symb_ordering invfreq_arity --sup_term_weight default --sup_to_prop_solver passive --sup_unprocessed_bound 10 --superposition_flag true --suppress_sat_res true --tptp_safe_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 3.67 --show_fool true" --time_out_real 11.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_4j3i12dt/jp61ph1s 2>> /export/starexec/sandbox/tmp/iprover_out_4j3i12dt/jp61ph1s_error
% 2.12/1.29 ERROR - "ProverProcess:heur/vip_65097:3.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("undefined enum value")
% 2.12/1.29 Fatal error: exception Failure("undefined enum value")
% 2.12/1.29 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --comb_inst_mult 3 --comb_mode clause_based --comb_res_mult 3 --comb_sup_deep_mult 0 --comb_sup_mult 0 --conj_cone_tolerance 4.0357851670394345 --extra_neg_conj none --inst_activity_threshold 512 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp true --inst_learning_factor 2 --inst_learning_loop_flag true --inst_learning_start 2048 --inst_lit_activity_flag true --inst_lit_sel "[+split;-sign;-depth]" --inst_lit_sel_side none --inst_orphan_elimination true --inst_passive_queue_type queue --inst_passive_queues "[[+age;+num_lits;-age];[-age;-min_def_symb;+bc_imp_inh]]" --inst_passive_queues_freq "[2;2]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given true --inst_sel_renew solver --inst_solver_calls_frac 1.0 --inst_solver_per_active 1024 --inst_sos_flag true --inst_sos_phase false --inst_sos_sth_lit_sel "[+split;-ground;-depth]" --inst_start_prop_sim_after_learn 3 --inst_subs_given true --inst_subs_new false --instantiation_flag true --out_options none --prep_sup_sim_all true --prep_sup_sim_sup false --preprocessed_out false --preprocessing_flag true --prolific_symb_bound 256 --proof_out true --prop_solver_per_cl 16384 --resolution_flag true --schedule none --share_sel_clauses false --stats_out none --subs_bck_mult 8 --suppress_sat_res true --tptp_safe_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 1.00 --show_fool true" --time_out_real 3.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_4j3i12dt/5a2ocuqb 2>> /export/starexec/sandbox/tmp/iprover_out_4j3i12dt/5a2ocuqb_error
% 2.12/1.29 ERROR - "ProverProcess:heur/vip_65080:40.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("undefined enum value")
% 2.12/1.29 Fatal error: exception Failure("undefined enum value")
% 2.12/1.29 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --comb_mode time_based --comb_res_mult 6 --comb_sup_deep_mult 4 --comb_sup_mult 6 --conj_cone_tolerance 1.895766803319499 --demod_completeness_check fullold --demod_use_ground false --extra_neg_conj all_pos_neg --instantiation_flag false --out_options none --preprocessed_out false --preprocessing_flag false --prolific_symb_bound 1024 --proof_out true --prop_solver_per_cl 128 --res_to_smt_solver false --resolution_flag true --schedule none --share_sel_clauses true --stats_out none --subs_bck_mult 16 --sup_bw_gjoin_interval 100 --sup_cache_sim none --sup_full_bw "[Subsumption;SubsumptionRes;UnitSubsAndRes]" --sup_full_fixpoint false --sup_full_fw "[]" --sup_fun_splitting false --sup_immed_bw_immed "[Subsumption;SubsumptionRes;UnitSubsAndRes]" --sup_immed_bw_main "[SubsumptionRes;UnitSubsAndRes;FullSubsAndRes;Demod;ACDemod]" --sup_immed_fixpoint false --sup_immed_fw_immed "[Subsumption;SubsumptionRes;FullSubsAndRes;Demod;LightNorm;ACDemod]" --sup_immed_fw_main "[Subsumption;UnitSubsAndRes;FullSubsAndRes;Demod;LightNorm;ACNormalisation;GroundJoinability;Connectedness]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_fixpoint false --sup_iter_deepening 2 --sup_main_fixpoint true --sup_ordering lpo --sup_passive_queue_type priority_queues --sup_passive_queues "[[+has_eq;-has_eq];[-num_var;-num_var];[+conj_dist;+ground;-max_atom_input_occur]]" --sup_passive_queues_freq "[1;4;4]" --sup_prop_simpl_given false --sup_prop_simpl_new false --sup_restarts_mult 4 --sup_score sim_d_gen --sup_share_max_num_cl 10 --sup_share_score_frac 0.2 --sup_smt_interval 32 --sup_symb_ordering invfreq_arity --sup_term_weight default --sup_to_prop_solver passive --sup_unprocessed_bound 10 --superposition_flag true --suppress_sat_res true --tptp_safe_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 13.33 --show_fool true" --time_out_real 40.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_4j3i12dt/pu6m7dm4 2>> /export/starexec/sandbox/tmp/iprover_out_4j3i12dt/pu6m7dm4_error
% 2.12/1.29 % SZS status Theorem for theBenchmark.p
% 2.12/1.29
% 2.12/1.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.12/1.29
% 2.12/1.29 % ------ iProver source info
% 2.12/1.29
% 2.12/1.29 % git: date: 2026-07-19 20:42:38 +0200
% 2.12/1.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.12/1.29 % git: non_committed_changes: false
% 2.12/1.29
% 2.12/1.29 % ------ Parsing...
% 2.12/1.29 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 2.12/1.29 % ------ Proving...
% 2.12/1.29 % ------ Problem Properties
% 2.12/1.29
% 2.12/1.29 %
% 2.12/1.29 % clauses 40
% 2.12/1.29 % conjectures 6
% 2.12/1.29 % EPR 10
% 2.12/1.29 % Horn 26
% 2.12/1.29 % unary 17
% 2.12/1.29 % binary 10
% 2.12/1.29 % lits 88
% 2.12/1.29 % lits eq 24
% 2.12/1.29 % fd_pure 0
% 2.12/1.29 % fd_pseudo 0
% 2.12/1.29 % fd_cond 7
% 2.12/1.29 % fd_pseudo_cond 2
% 2.12/1.29 % AC symbols 1
% 2.12/1.29
% 2.12/1.29 % ------ Input Options Time Limit: Unbounded
% 2.12/1.29
% 2.12/1.29
% 2.12/1.29 % ------
% 2.12/1.29 % Current options:
% 2.12/1.29 % ------
% 2.12/1.29
% 2.12/1.29
% 2.12/1.29 %
% 2.12/1.29
% 2.12/1.29 % ------ Proving...
% 2.12/1.29 %
% 2.12/1.29
% 2.12/1.29 % SZS status Theorem for theBenchmark.p
% 2.12/1.29
% 2.12/1.29 % SZS output start CNFRefutation for theBenchmark.p
% 2.12/1.29
% 2.12/1.29 tff(func_def_0, type, 'empty:Tree': 'Tree').
% 2.12/1.29 tff(pred_def_1, type, searchtree: 'Tree' > $o).
% 2.12/1.29 tff(pred_def_2, type, in: ($int * 'Tree') > $o).
% 2.12/1.29 tff(func_def_3, type, 'node:(Int*Tree*Tree)>Tree': ($int * 'Tree' * 'Tree') > 'Tree').
% 2.12/1.29 tff(func_def_4, type, 'right:(Tree)>Tree': 'Tree' > 'Tree').
% 2.12/1.29 tff(type_def_5, type, 'Tree': $tType).
% 2.12/1.29 tff(pred_def_6, type, sP0: 'Tree' > $o).
% 2.12/1.29 tff(func_def_9, type, sK1: 'Tree' > $int).
% 2.12/1.29 tff(func_def_10, type, sK2: 'Tree' > $int).
% 2.12/1.29 tff(func_def_11, type, sK3: 'Tree').
% 2.12/1.29 tff(func_def_12, type, sK4: $int).
% 2.12/1.29 tff(f7,axiom,(
% 2.12/1.29 ! [X0 : 'Tree'] : (searchtree(X0) <=> ((X0 = 'empty:Tree' => $true) & (X0 != 'empty:Tree' => (searchtree('left:(Tree)>Tree'(X0)) & searchtree('right:(Tree)>Tree'(X0)) & ! [X1 : $int] : (in(X1,'left:(Tree)>Tree'(X0)) => $lesseq(X1,'val:(Tree)>Int'(X0))) & ! [X1 : $int] : (in(X1,'right:(Tree)>Tree'(X0)) => $greater(X1,'val:(Tree)>Int'(X0)))))))),
% 2.12/1.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_006)).
% 2.12/1.29
% 2.12/1.29 tff(f8,conjecture,(
% 2.12/1.29 ! [X0 : 'Tree',X1 : $int] : (searchtree(X0) => ((X0 = 'empty:Tree' => $true) & (X0 != 'empty:Tree' => ((X1 = 'val:(Tree)>Int'(X0) => $true) & (X1 != 'val:(Tree)>Int'(X0) => (($less(X1,'val:(Tree)>Int'(X0)) => ? [X2 : 'Tree'] : (X2 = 'left:(Tree)>Tree'(X0) & searchtree(X2))) & (~$less(X1,'val:(Tree)>Int'(X0)) => ? [X3 : 'Tree'] : (X3 = 'right:(Tree)>Tree'(X0) & searchtree(X3)))))))))),
% 2.12/1.29 file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_007)).
% 2.12/1.29
% 2.12/1.29 tff(f9,negated_conjecture,(
% 2.12/1.29 ~ ! [X0 : 'Tree',X1 : $int] : (searchtree(X0) => ((X0 = 'empty:Tree' => $true) & (X0 != 'empty:Tree' => ((X1 = 'val:(Tree)>Int'(X0) => $true) & (X1 != 'val:(Tree)>Int'(X0) => (($less(X1,'val:(Tree)>Int'(X0)) => ? [X2 : 'Tree'] : (X2 = 'left:(Tree)>Tree'(X0) & searchtree(X2))) & (~$less(X1,'val:(Tree)>Int'(X0)) => ? [X3 : 'Tree'] : (X3 = 'right:(Tree)>Tree'(X0) & searchtree(X3)))))))))),
% 2.12/1.29 inference(negated_conjecture,[status(cth)],[f8])).
% 2.12/1.29
% 2.12/1.29 tff(f10,plain,(
% 2.12/1.29 ! [X0 : 'Tree'] : (searchtree(X0) <=> ((X0 = 'empty:Tree' => $true) & (X0 != 'empty:Tree' => (searchtree('left:(Tree)>Tree'(X0)) & searchtree('right:(Tree)>Tree'(X0)) & ! [X1 : $int] : (in(X1,'left:(Tree)>Tree'(X0)) => ~$less('val:(Tree)>Int'(X0),X1)) & ! [X1 : $int] : (in(X1,'right:(Tree)>Tree'(X0)) => $less('val:(Tree)>Int'(X0),X1))))))),
% 2.12/1.29 inference(theory_normalization,[],[f7])).
% 2.12/1.29
% 2.12/1.29 tff(f25,plain,(
% 2.12/1.29 ! [X0 : 'Tree'] : (searchtree(X0) <=> ((X0 = 'empty:Tree' => $true) & (X0 != 'empty:Tree' => (searchtree('left:(Tree)>Tree'(X0)) & searchtree('right:(Tree)>Tree'(X0)) & ! [X1 : $int] : (in(X1,'left:(Tree)>Tree'(X0)) => ~$less('val:(Tree)>Int'(X0),X1)) & ! [X2 : $int] : (in(X2,'right:(Tree)>Tree'(X0)) => $less('val:(Tree)>Int'(X0),X2))))))),
% 2.12/1.29 inference(rectify,[],[f10])).
% 2.12/1.29
% 2.12/1.29 tff(f26,plain,(
% 2.12/1.29 ! [X0 : 'Tree'] : (searchtree(X0) <=> (X0 != 'empty:Tree' => (searchtree('left:(Tree)>Tree'(X0)) & searchtree('right:(Tree)>Tree'(X0)) & ! [X1 : $int] : (in(X1,'left:(Tree)>Tree'(X0)) => ~$less('val:(Tree)>Int'(X0),X1)) & ! [X2 : $int] : (in(X2,'right:(Tree)>Tree'(X0)) => $less('val:(Tree)>Int'(X0),X2)))))),
% 2.12/1.29 inference(true_and_false_elimination,[],[f25])).
% 2.12/1.29
% 2.12/1.29 tff(f27,plain,(
% 2.12/1.29 ~ ! [X0 : 'Tree',X1 : $int] : (searchtree(X0) => (X0 != 'empty:Tree' => (X1 != 'val:(Tree)>Int'(X0) => (($less(X1,'val:(Tree)>Int'(X0)) => ? [X2 : 'Tree'] : (X2 = 'left:(Tree)>Tree'(X0) & searchtree(X2))) & (~$less(X1,'val:(Tree)>Int'(X0)) => ? [X3 : 'Tree'] : (X3 = 'right:(Tree)>Tree'(X0) & searchtree(X3)))))))),
% 2.12/1.29 inference(true_and_false_elimination,[],[f9])).
% 2.12/1.29
% 2.12/1.29 tff(f30,plain,(
% 2.12/1.29 ! [X0 : 'Tree'] : (searchtree(X0) <=> ((searchtree('left:(Tree)>Tree'(X0)) & searchtree('right:(Tree)>Tree'(X0)) & ! [X1 : $int] : (~$less('val:(Tree)>Int'(X0),X1) | ~in(X1,'left:(Tree)>Tree'(X0))) & ! [X2 : $int] : ($less('val:(Tree)>Int'(X0),X2) | ~in(X2,'right:(Tree)>Tree'(X0)))) | 'empty:Tree' = X0))),
% 2.12/1.29 inference(ennf_transformation,[],[f26])).
% 2.12/1.29
% 2.12/1.29 tff(f31,plain,(
% 2.12/1.29 ? [X0 : 'Tree',X1 : $int] : (((((! [X2 : 'Tree'] : ('left:(Tree)>Tree'(X0) != X2 | ~searchtree(X2)) & $less(X1,'val:(Tree)>Int'(X0))) | (! [X3 : 'Tree'] : ('right:(Tree)>Tree'(X0) != X3 | ~searchtree(X3)) & ~$less(X1,'val:(Tree)>Int'(X0)))) & X1 != 'val:(Tree)>Int'(X0)) & X0 != 'empty:Tree') & searchtree(X0))),
% 2.12/1.29 inference(ennf_transformation,[],[f27])).
% 2.12/1.29
% 2.12/1.29 tff(f32,plain,(
% 2.12/1.29 ? [X0 : 'Tree',X1 : $int] : (((! [X2 : 'Tree'] : ('left:(Tree)>Tree'(X0) != X2 | ~searchtree(X2)) & $less(X1,'val:(Tree)>Int'(X0))) | (! [X3 : 'Tree'] : ('right:(Tree)>Tree'(X0) != X3 | ~searchtree(X3)) & ~$less(X1,'val:(Tree)>Int'(X0)))) & X1 != 'val:(Tree)>Int'(X0) & X0 != 'empty:Tree' & searchtree(X0))),
% 2.12/1.29 inference(flattening,[],[f31])).
% 2.12/1.29
% 2.12/1.29 tff(f41,plain,(
% 2.12/1.29 ! [X0 : 'Tree'] : ((searchtree(X0) | ~sP0(X0)) & (sP0(X0) | ~searchtree(X0)))),
% 2.12/1.29 inference(nnf_transformation,[],[f34])).
% 2.12/1.29
% 2.12/1.29 tff(f42,plain,(
% 2.12/1.29 ((! [X2 : 'Tree'] : ('left:(Tree)>Tree'(sK3) != X2 | ~searchtree(X2)) & $less(sK4,'val:(Tree)>Int'(sK3))) | (! [X3 : 'Tree'] : ('right:(Tree)>Tree'(sK3) != X3 | ~searchtree(X3)) & ~$less(sK4,'val:(Tree)>Int'(sK3)))) & sK4 != 'val:(Tree)>Int'(sK3) & 'empty:Tree' != sK3 & searchtree(sK3)),
% 2.12/1.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4]),skolemize(X0,sK3),skolemize(X1,sK4)],[f32])).
% 2.12/1.29
% 2.12/1.29 tff(f63,plain,(
% 2.12/1.29 ( ! [X0 : 'Tree'] : (sP0(X0) | ~searchtree(X0)) )),
% 2.12/1.29 inference(cnf_transformation,[],[f41])).
% 2.12/1.29
% 2.12/1.29 tff(f65,plain,(
% 2.12/1.29 searchtree(sK3)),
% 2.12/1.29 inference(cnf_transformation,[],[f42])).
% 2.12/1.29
% 2.12/1.29 tff(f66,plain,(
% 2.12/1.29 'empty:Tree' != sK3),
% 2.12/1.29 inference(cnf_transformation,[],[f42])).
% 2.12/1.29
% 2.12/1.29 tff(f71,plain,(
% 2.12/1.29 ( ! [X2 : 'Tree',X3 : 'Tree'] : ('left:(Tree)>Tree'(sK3) != X2 | ~searchtree(X2) | 'right:(Tree)>Tree'(sK3) != X3 | ~searchtree(X3)) )),
% 2.12/1.29 inference(cnf_transformation,[],[f42])).
% 2.12/1.29
% 2.12/1.29 tff(f76,plain,(
% 2.12/1.29 ( ! [X3 : 'Tree'] : (~searchtree('left:(Tree)>Tree'(sK3)) | 'right:(Tree)>Tree'(sK3) != X3 | ~searchtree(X3)) )),
% 2.12/1.29 inference(equality_resolution,[],[f71])).
% 2.12/1.29
% 2.12/1.29 tff(f77,plain,(
% 2.12/1.29 ~searchtree('left:(Tree)>Tree'(sK3)) | ~searchtree('right:(Tree)>Tree'(sK3))),
% 2.12/1.29 inference(equality_resolution,[],[f76])).
% 2.12/1.29
% 2.12/1.29 tcf(c_81,plain,![X0_'Tree':'Tree']:
% 2.12/1.29 (~searchtree(X0_'Tree')|sP0(X0_'Tree')),
% 2.12/1.29 inference(cnf_transformation,[],[f63])).
% 2.12/1.29
% 2.12/1.29 tcf(c_82,negated_conjecture,
% 2.12/1.29 (~searchtree('left:(Tree)>Tree'(sK3))|~searchtree('right:(Tree)>Tree'(sK3))),
% 2.12/1.29 inference(cnf_transformation,[],[f77])).
% 2.12/1.29
% 2.12/1.29 tcf(c_86,negated_conjecture,
% 2.12/1.29 ('empty:Tree' != sK3),
% 2.12/1.29 inference(cnf_transformation,[],[f66])).
% 2.12/1.29
% 2.12/1.29 tcf(c_87,negated_conjecture,
% 2.12/1.29 (searchtree(sK3)),
% 2.12/1.29 inference(cnf_transformation,[],[f65])).
% 2.12/1.29
% 2.12/1.29 tcf(c_91,plain,![X0_'Tree':'Tree']:
% 2.12/1.29 (X0_'Tree' = X0_'Tree'),
% 2.12/1.29 theory(equality)).
% 2.12/1.29
% 2.12/1.29 tcf(c_93,plain,![X0_'Tree':'Tree',X1_'Tree':'Tree',X2_'Tree':'Tree']:
% 2.12/1.29 (X0_'Tree' != X1_'Tree'|X2_'Tree' != X1_'Tree'|X2_'Tree' = X0_'Tree'),
% 2.12/1.29 theory(equality)).
% 2.12/1.29
% 2.12/1.29 tcf(c_106,plain,
% 2.12/1.29 ('empty:Tree' = 'empty:Tree'),
% 2.12/1.29 inference(instantiation,[status(thm)],[c_91])).
% 2.12/1.29
% 2.12/1.29 tcf(c_131,plain,![X0_'Tree':'Tree']:
% 2.12/1.29 ('empty:Tree' != X0_'Tree'|sK3 != X0_'Tree'|'empty:Tree' = sK3),
% 2.12/1.29 inference(instantiation,[status(thm)],[c_93])).
% 2.12/1.29
% 2.12/1.29 tcf(c_132,plain,
% 2.12/1.29 ('empty:Tree' != 'empty:Tree'|sK3 != 'empty:Tree'|'empty:Tree' = sK3),
% 2.12/1.29 inference(instantiation,[status(thm)],[c_131])).
% 2.12/1.29
% 2.12/1.29 tcf(c_605,plain,
% 2.12/1.29 (~searchtree(sK3)|sP0(sK3)),
% 2.12/1.29 inference(instantiation,[status(thm)],[c_81])).
% 2.12/1.29
% 2.12/1.29 tff(f33,definition,(
% 2.12/1.29 ! [X0 : 'Tree'] : (sP0(X0) <=> ((searchtree('left:(Tree)>Tree'(X0)) & searchtree('right:(Tree)>Tree'(X0)) & ! [X1 : $int] : (~$less('val:(Tree)>Int'(X0),X1) | ~in(X1,'left:(Tree)>Tree'(X0))) & ! [X2 : $int] : ($less('val:(Tree)>Int'(X0),X2) | ~in(X2,'right:(Tree)>Tree'(X0)))) | 'empty:Tree' = X0))),
% 2.12/1.29 introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction])).
% 2.12/1.29 tff(f34,plain,(
% 2.12/1.29 ! [X0 : 'Tree'] : (searchtree(X0) <=> sP0(X0))),
% 2.12/1.29 inference(definition_folding,[],[f30,f33])).
% 2.12/1.29
% 2.12/1.29 tff(f37,plain,(
% 2.12/1.29 ! [X0 : 'Tree'] : ((sP0(X0) | ((~searchtree('left:(Tree)>Tree'(X0)) | ~searchtree('right:(Tree)>Tree'(X0)) | ? [X1 : $int] : ($less('val:(Tree)>Int'(X0),X1) & in(X1,'left:(Tree)>Tree'(X0))) | ? [X2 : $int] : (~$less('val:(Tree)>Int'(X0),X2) & in(X2,'right:(Tree)>Tree'(X0)))) & 'empty:Tree' != X0)) & (((searchtree('left:(Tree)>Tree'(X0)) & searchtree('right:(Tree)>Tree'(X0)) & ! [X1 : $int] : (~$less('val:(Tree)>Int'(X0),X1) | ~in(X1,'left:(Tree)>Tree'(X0))) & ! [X2 : $int] : ($less('val:(Tree)>Int'(X0),X2) | ~in(X2,'right:(Tree)>Tree'(X0)))) | 'empty:Tree' = X0) | ~sP0(X0)))),
% 2.12/1.29 inference(nnf_transformation,[],[f33])).
% 2.12/1.29
% 2.12/1.29 tff(f38,plain,(
% 2.12/1.29 ! [X0 : 'Tree'] : ((sP0(X0) | ((~searchtree('left:(Tree)>Tree'(X0)) | ~searchtree('right:(Tree)>Tree'(X0)) | ? [X1 : $int] : ($less('val:(Tree)>Int'(X0),X1) & in(X1,'left:(Tree)>Tree'(X0))) | ? [X2 : $int] : (~$less('val:(Tree)>Int'(X0),X2) & in(X2,'right:(Tree)>Tree'(X0)))) & 'empty:Tree' != X0)) & ((searchtree('left:(Tree)>Tree'(X0)) & searchtree('right:(Tree)>Tree'(X0)) & ! [X1 : $int] : (~$less('val:(Tree)>Int'(X0),X1) | ~in(X1,'left:(Tree)>Tree'(X0))) & ! [X2 : $int] : ($less('val:(Tree)>Int'(X0),X2) | ~in(X2,'right:(Tree)>Tree'(X0)))) | 'empty:Tree' = X0 | ~sP0(X0)))),
% 2.12/1.29 inference(flattening,[],[f37])).
% 2.12/1.29
% 2.12/1.29 tff(f39,plain,(
% 2.12/1.29 ! [X0 : 'Tree'] : ((sP0(X0) | ((~searchtree('left:(Tree)>Tree'(X0)) | ~searchtree('right:(Tree)>Tree'(X0)) | ? [X1 : $int] : ($less('val:(Tree)>Int'(X0),X1) & in(X1,'left:(Tree)>Tree'(X0))) | ? [X2 : $int] : (~$less('val:(Tree)>Int'(X0),X2) & in(X2,'right:(Tree)>Tree'(X0)))) & 'empty:Tree' != X0)) & ((searchtree('left:(Tree)>Tree'(X0)) & searchtree('right:(Tree)>Tree'(X0)) & ! [X3 : $int] : (~$less('val:(Tree)>Int'(X0),X3) | ~in(X3,'left:(Tree)>Tree'(X0))) & ! [X4 : $int] : ($less('val:(Tree)>Int'(X0),X4) | ~in(X4,'right:(Tree)>Tree'(X0)))) | 'empty:Tree' = X0 | ~sP0(X0)))),
% 2.12/1.29 inference(rectify,[],[f38])).
% 2.12/1.29
% 2.12/1.29 tff(f40,plain,(
% 2.12/1.29 ! [X0 : 'Tree'] : ((sP0(X0) | ((~searchtree('left:(Tree)>Tree'(X0)) | ~searchtree('right:(Tree)>Tree'(X0)) | ($less('val:(Tree)>Int'(X0),sK1(X0)) & in(sK1(X0),'left:(Tree)>Tree'(X0))) | (~$less('val:(Tree)>Int'(X0),sK2(X0)) & in(sK2(X0),'right:(Tree)>Tree'(X0)))) & 'empty:Tree' != X0)) & ((searchtree('left:(Tree)>Tree'(X0)) & searchtree('right:(Tree)>Tree'(X0)) & ! [X3 : $int] : (~$less('val:(Tree)>Int'(X0),X3) | ~in(X3,'left:(Tree)>Tree'(X0))) & ! [X4 : $int] : ($less('val:(Tree)>Int'(X0),X4) | ~in(X4,'right:(Tree)>Tree'(X0)))) | 'empty:Tree' = X0 | ~sP0(X0)))),
% 2.12/1.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(X1,sK1(X0)),skolemize(X2,sK2(X0))],[f39])).
% 2.12/1.29
% 2.12/1.29 tff(f56,plain,(
% 2.12/1.29 ( ! [X0 : 'Tree'] : (searchtree('right:(Tree)>Tree'(X0)) | 'empty:Tree' = X0 | ~sP0(X0)) )),
% 2.12/1.29 inference(cnf_transformation,[],[f40])).
% 2.12/1.29
% 2.12/1.29 tff(f57,plain,(
% 2.12/1.29 ( ! [X0 : 'Tree'] : (searchtree('left:(Tree)>Tree'(X0)) | 'empty:Tree' = X0 | ~sP0(X0)) )),
% 2.12/1.29 inference(cnf_transformation,[],[f40])).
% 2.12/1.29
% 2.12/1.29 tcf(c_76,plain,![X0_'Tree':'Tree']:
% 2.12/1.29 (~sP0(X0_'Tree')|X0_'Tree' = 'empty:Tree'|searchtree('left:(Tree)>Tree'(X0_'Tree'))),
% 2.12/1.29 inference(cnf_transformation,[],[f57])).
% 2.12/1.29
% 2.12/1.29 tcf(c_77,plain,![X0_'Tree':'Tree']:
% 2.12/1.29 (~sP0(X0_'Tree')|X0_'Tree' = 'empty:Tree'|searchtree('right:(Tree)>Tree'(X0_'Tree'))),
% 2.12/1.29 inference(cnf_transformation,[],[f56])).
% 2.12/1.29
% 2.12/1.29 tcf(c_207,plain,
% 2.12/1.29 (~sP0(sK3)|sK3 = 'empty:Tree'|searchtree('left:(Tree)>Tree'(sK3))),
% 2.12/1.29 inference(instantiation,[status(thm)],[c_76])).
% 2.12/1.29
% 2.12/1.29 tcf(c_208,plain,
% 2.12/1.29 (~sP0(sK3)|sK3 = 'empty:Tree'|searchtree('right:(Tree)>Tree'(sK3))),
% 2.12/1.29 inference(instantiation,[status(thm)],[c_77])).
% 2.12/1.29
% 2.12/1.29 tcf(c_606,plain,
% 2.12/1.29 ($false),
% 2.12/1.29 inference(prop_impl_just,
% 2.12/1.29 [status(thm)],
% 2.12/1.29 [c_605,c_207,c_208,c_132,c_82,c_86,c_106,c_87])).
% 2.12/1.29
% 2.12/1.29
% 2.12/1.29 % SZS output end CNFRefutation for theBenchmark.p
% 2.12/1.29
% 2.12/1.29
%------------------------------------------------------------------------------