%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : ALG248^2 : TPTP v9.2.1. Bugfixed v5.2.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n018.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 : Wed Jun 3 08:06:16 AM UTC 2026 % Result : CounterSatisfiable 148.02s 148.61s % Output : Model 148.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ALG248^2 : TPTP v9.2.1. Bugfixed v5.2.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.17/0.34 % Computer : n018.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Wed Jun 3 01:54:20 EDT 2026 % 0.17/0.34 % CPUTime : % 0.40/0.55 %----Disproving TH0 % 148.02/148.61 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 72s... % 148.02/148.61 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --mbqi-enum-choice-grammar-all --no-cegqi --no-sygus-inst at 30s... % 148.02/148.61 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-mbqi-nested-check --no-cegqi --no-sygus-inst at 18s... % 148.02/148.61 --- Run --ho-elim --full-saturate-quant at 9s... % 148.02/148.61 --- Run --ho-elim --no-e-matching --full-saturate-quant at 9s... % 148.02/148.61 --- Run --ho-elim --no-e-matching --enum-inst-sum --full-saturate-quant at 9s... % 148.02/148.61 --- Run --ho-elim --finite-model-find --uf-ss=no-minimal at 30s... % 148.02/148.61 % SZS status CounterSatisfiable % 148.02/148.61 % SZS output start Model % 148.02/148.61 ( % 148.02/148.61 ; cardinality of $$unsorted is 1 % 148.02/148.61 ; rep: (as @$$unsorted_0 $$unsorted) % 148.02/148.61 ; cardinality of tptp.term is 1 % 148.02/148.61 ; rep: (as @tptp.term_0 tptp.term) % 148.02/148.61 ; cardinality of tptp.subst is 1 % 148.02/148.61 ; rep: (as @tptp.subst_0 tptp.subst) % 148.02/148.61 (define-fun tptp.one () tptp.term (as @tptp.term_0 tptp.term)) % 148.02/148.61 (define-fun tptp.ap ((BOUND_VARIABLE_22284 tptp.term) (BOUND_VARIABLE_22286 tptp.term)) tptp.term (as @tptp.term_0 tptp.term)) % 148.02/148.61 (define-fun tptp.lam ((BOUND_VARIABLE_22294 tptp.term)) tptp.term (as @tptp.term_0 tptp.term)) % 148.02/148.61 (define-fun tptp.sub ((BOUND_VARIABLE_22700 tptp.term) (BOUND_VARIABLE_22702 tptp.subst)) tptp.term (as @tptp.term_0 tptp.term)) % 148.02/148.61 (define-fun tptp.id () tptp.subst (as @tptp.subst_0 tptp.subst)) % 148.02/148.61 (define-fun tptp.sh () tptp.subst (as @tptp.subst_0 tptp.subst)) % 148.02/148.61 (define-fun tptp.push ((BOUND_VARIABLE_23080 tptp.term) (BOUND_VARIABLE_23082 tptp.subst)) tptp.subst (as @tptp.subst_0 tptp.subst)) % 148.02/148.61 (define-fun tptp.comp ((BOUND_VARIABLE_23182 tptp.subst) (BOUND_VARIABLE_23184 tptp.subst)) tptp.subst (as @tptp.subst_0 tptp.subst)) % 148.02/148.61 (define-fun tptp.var ((BOUND_VARIABLE_23216 tptp.term)) Bool (= (as @tptp.term_0 tptp.term) BOUND_VARIABLE_23216)) % 148.02/148.61 (define-fun tptp.pushprop_lem1v2 () Bool (forall ((P (-> tptp.term Bool)) (Q (-> tptp.term Bool)) (A tptp.term) (M tptp.subst)) (or (not (P A)) (not (forall ((X tptp.term)) (= (Q X) (P (ho_7 (ho_6 k_5 X) (ho_4 (ho_3 k_2 A) M)))))) (Q tptp.one)))) % 148.02/148.61 (define-fun tptp.pushprop_lem1_gthm () Bool true) % 148.02/148.61 (define-fun tptp.axmap () Bool true) % 148.02/148.61 (define-fun tptp.pushprop_lem0_gthm () Bool true) % 148.02/148.61 (define-fun tptp.shinj () Bool (forall ((A tptp.term) (B tptp.term)) (or (not (= (ho_7 (ho_6 k_5 A) tptp.sh) (ho_7 (ho_6 k_5 B) tptp.sh))) (= A B)))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem1v2 () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool)) (BOUND_VARIABLE_2756 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (ho_4 (ho_11 k_10 K) N))) (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)) (P M A (ho_4 (ho_11 k_10 K) N))))) (not (forall ((A tptp.term)) (or (not (ho_8 k_9 (ho_7 (ho_6 k_5 A) tptp.id))) (P tptp.id A tptp.id)))) (not (forall ((X tptp.term)) (= (Q X) (P tptp.id X tptp.id)))) (not (ho_8 k_9 BOUND_VARIABLE_2756)) (Q BOUND_VARIABLE_2756)))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem1v2_gthm () Bool true) % 148.02/148.61 (define-fun tptp.hoasap ((BOUND_VARIABLE_24147 tptp.subst) (BOUND_VARIABLE_24149 tptp.term) (BOUND_VARIABLE_24151 tptp.subst) (BOUND_VARIABLE_24153 tptp.term)) tptp.term (as @tptp.term_0 tptp.term)) % 148.02/148.61 (define-fun tptp.induction2lem () Bool (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2340 tptp.term) (BOUND_VARIABLE_2342 tptp.subst)) (or (not (forall ((A tptp.term) (B tptp.term)) (or (not (P A)) (not (P B)) (P (tptp.ap A B))))) (not (forall ((A tptp.term)) (or (not (forall ((B tptp.term)) (or (not (P B)) (P (ho_7 (ho_6 k_5 A) (ho_4 (ho_3 k_2 B) tptp.id)))))) (P (tptp.lam A))))) (not (forall ((B tptp.term)) (or (not (ho_8 k_9 B)) (P (ho_7 (ho_6 k_5 B) BOUND_VARIABLE_2342))))) (P (ho_7 (ho_6 k_5 BOUND_VARIABLE_2340) BOUND_VARIABLE_2342))))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3v2_f () Bool (forall ((B tptp.term)) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (not (forall ((A tptp.term) (M tptp.subst)) (= (F M A) (ho_7 (ho_6 k_5 B) (ho_4 (ho_3 k_2 A) M))))))))) % 148.02/148.61 (define-fun tptp.axvarshift () Bool true) % 148.02/148.61 (define-fun tptp.hoasapinj2 () Bool (forall ((A tptp.term) (B tptp.term) (C tptp.term) (D tptp.term)) (or (not (= (tptp.ap (ho_7 (ho_6 k_5 A) tptp.id) C) (tptp.ap (ho_7 (ho_6 k_5 B) tptp.id) D))) (= C D)))) % 148.02/148.61 (define-fun tptp.hoasapnotvar_gthm () Bool true) % 148.02/148.61 (define-fun tptp.hoasapinj1 () Bool (forall ((A tptp.term) (B tptp.term) (C tptp.term) (D tptp.term)) (or (not (= (tptp.ap (ho_7 (ho_6 k_5 A) tptp.id) C) (tptp.ap (ho_7 (ho_6 k_5 B) tptp.id) D))) (= A B)))) % 148.02/148.61 (define-fun tptp.ulamvar1 () Bool true) % 148.02/148.61 (define-fun tptp.induction2lem_lthm () Bool (=> (forall ((M tptp.subst)) (= M (ho_4 (ho_11 k_10 M) tptp.id))) (=> (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2140 tptp.term)) (or (not (forall ((A tptp.term)) (or (not (ho_8 k_9 A)) (P A)))) (not (forall ((A tptp.term) (B tptp.term)) (or (not (P A)) (not (P B)) (P (tptp.ap A B))))) (not (forall ((A tptp.term)) (or (not (P A)) (P (tptp.lam A))))) (P BOUND_VARIABLE_2140))) (=> (forall ((P (-> tptp.term Bool)) (A tptp.term) (M tptp.subst) (BOUND_VARIABLE_2295 tptp.term)) (or (not (forall ((B tptp.term)) (or (not (ho_8 k_9 B)) (P (ho_7 (ho_6 k_5 B) M))))) (not (P A)) (not (ho_8 k_9 BOUND_VARIABLE_2295)) (P (ho_7 (ho_6 k_5 BOUND_VARIABLE_2295) (ho_4 (ho_3 k_2 A) M))))) (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2340 tptp.term) (BOUND_VARIABLE_2342 tptp.subst)) (or (not (forall ((A tptp.term) (B tptp.term)) (or (not (P A)) (not (P B)) (P (tptp.ap A B))))) (not (forall ((A tptp.term)) (or (not (forall ((B tptp.term)) (or (not (P B)) (P (ho_7 (ho_6 k_5 A) (ho_4 (ho_3 k_2 B) tptp.id)))))) (P (tptp.lam A))))) (not (forall ((B tptp.term)) (or (not (ho_8 k_9 B)) (P (ho_7 (ho_6 k_5 B) BOUND_VARIABLE_2342))))) (P (ho_7 (ho_6 k_5 BOUND_VARIABLE_2340) BOUND_VARIABLE_2342)))))))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3v2_gthm () Bool true) % 148.02/148.61 (define-fun tptp.apnotvar () Bool false) % 148.02/148.61 (define-fun tptp.pushprop_lthm_orig () Bool (forall ((P (-> tptp.term Bool)) (A tptp.term) (M tptp.subst) (BOUND_VARIABLE_2295 tptp.term)) (or (not (forall ((B tptp.term)) (or (not (ho_8 k_9 B)) (P (ho_7 (ho_6 k_5 B) M))))) (not (P A)) (not (ho_8 k_9 BOUND_VARIABLE_2295)) (P (ho_7 (ho_6 k_5 BOUND_VARIABLE_2295) (ho_4 (ho_3 k_2 A) M)))))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3v2_f_lthm () Bool (forall ((B tptp.term)) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (not (forall ((A tptp.term) (M tptp.subst)) (= (F M A) (ho_7 (ho_6 k_5 B) (ho_4 (ho_3 k_2 A) M))))))))) % 148.02/148.61 (define-fun tptp.hoasinduction_lthm () Bool (=> (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2367 tptp.term)) (or (not (forall ((A tptp.term)) (or (not (ho_8 k_9 A)) (P A)))) (not (forall ((A tptp.term) (B tptp.term)) (or (not (P A)) (not (P B)) (P (tptp.ap A B))))) (not (forall ((A tptp.term)) (or (not (forall ((B tptp.term)) (or (not (P B)) (P (ho_7 (ho_6 k_5 A) (ho_4 (ho_3 k_2 B) tptp.id)))))) (P (tptp.lam A))))) (P BOUND_VARIABLE_2367))) (=> (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_2965 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (ho_4 (ho_11 k_10 K) N))) (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)) (P M A (ho_4 (ho_11 k_10 K) N))))) (not (forall ((A tptp.term)) (or (not (ho_8 k_9 (ho_7 (ho_6 k_5 A) tptp.id))) (P tptp.id A tptp.id)))) (not (ho_8 k_9 BOUND_VARIABLE_2965)) (P tptp.id BOUND_VARIABLE_2965 tptp.id))) (=> (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_2999 tptp.term) (BOUND_VARIABLE_3001 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (ho_4 (ho_11 k_10 K) N))) (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)) (P M A (ho_4 (ho_11 k_10 K) N))))) (not (forall ((A tptp.term) (B tptp.term)) (or (not (P tptp.id A tptp.id)) (not (P tptp.id B tptp.id)) (P tptp.id (tptp.ap (ho_7 (ho_6 k_5 A) tptp.id) B) tptp.id)))) (not (P tptp.id BOUND_VARIABLE_2999 tptp.id)) (not (P tptp.id BOUND_VARIABLE_3001 tptp.id)) (P tptp.id (tptp.ap BOUND_VARIABLE_2999 BOUND_VARIABLE_3001) tptp.id))) (=> (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3211 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (ho_4 (ho_11 k_10 K) N))) (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)) (P M A (ho_4 (ho_11 k_10 K) N))))) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (not (forall ((B tptp.term)) (or (not (P tptp.id B tptp.id)) (P tptp.id (ho_7 (ho_6 k_5 BOUND_VARIABLE_3211) (ho_4 (ho_3 k_2 B) tptp.id)) tptp.id)))) (P tptp.id (tptp.lam BOUND_VARIABLE_3211) tptp.id))) (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3283 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (ho_4 (ho_11 k_10 K) N))) (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)) (P M A (ho_4 (ho_11 k_10 K) N))))) (not (forall ((A tptp.term)) (or (not (ho_8 k_9 (ho_7 (ho_6 k_5 A) tptp.id))) (P tptp.id A tptp.id)))) (not (forall ((A tptp.term) (B tptp.term)) (or (not (P tptp.id A tptp.id)) (not (P tptp.id B tptp.id)) (P tptp.id (tptp.ap (ho_7 (ho_6 k_5 A) tptp.id) B) tptp.id)))) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (P tptp.id BOUND_VARIABLE_3283 tptp.id)))))))) % 148.02/148.61 (define-fun tptp.hoasinduction_no_psi_cond_lthm () Bool (=> (forall ((P (-> tptp.subst tptp.term tptp.subst Bool))) (not (forall ((Q (-> tptp.term Bool))) (not (forall ((X tptp.term)) (= (Q X) (P tptp.id X tptp.id))))))) (=> (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2367 tptp.term)) (or (not (forall ((A tptp.term)) (or (not (ho_8 k_9 A)) (P A)))) (not (forall ((A tptp.term) (B tptp.term)) (or (not (P A)) (not (P B)) (P (tptp.ap A B))))) (not (forall ((A tptp.term)) (or (not (forall ((B tptp.term)) (or (not (P B)) (P (ho_7 (ho_6 k_5 A) (ho_4 (ho_3 k_2 B) tptp.id)))))) (P (tptp.lam A))))) (P BOUND_VARIABLE_2367))) (=> (forall ((A tptp.term)) (= A (ho_7 (ho_6 k_5 A) tptp.id))) (=> (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool)) (BOUND_VARIABLE_2931 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (not (forall ((X tptp.term)) (= (Q X) (P tptp.id X tptp.id)))) (not (forall ((B tptp.term)) (or (not (Q B)) (Q (ho_7 (ho_6 k_5 BOUND_VARIABLE_2931) (ho_4 (ho_3 k_2 B) tptp.id)))))) (Q (tptp.lam BOUND_VARIABLE_2931)))) (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3295 tptp.term)) (or (not (forall ((A tptp.term) (B tptp.term)) (or (not (P tptp.id A tptp.id)) (not (P tptp.id B tptp.id)) (P tptp.id (tptp.ap (ho_7 (ho_6 k_5 A) tptp.id) B) tptp.id)))) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (P tptp.id BOUND_VARIABLE_3295 tptp.id)))))))) % 148.02/148.61 (define-fun tptp.hoaslaminj () Bool (forall ((F (-> tptp.subst tptp.term tptp.term)) (BOUND_VARIABLE_2547 (-> tptp.subst tptp.term tptp.term)) (BOUND_VARIABLE_2549 tptp.subst) (BOUND_VARIABLE_2551 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (BOUND_VARIABLE_2547 M A)) N) (BOUND_VARIABLE_2547 (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (= (tptp.lam (F tptp.sh tptp.one)) (tptp.lam (BOUND_VARIABLE_2547 tptp.sh tptp.one)))) (= (F BOUND_VARIABLE_2549 BOUND_VARIABLE_2551) (BOUND_VARIABLE_2547 BOUND_VARIABLE_2549 BOUND_VARIABLE_2551))))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3aaa () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3171 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term)) (BOUND_VARIABLE_3149 tptp.term)) (or (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id) (not (forall ((BOUND_VARIABLE_3072 tptp.subst) (BOUND_VARIABLE_3074 tptp.term) (BOUND_VARIABLE_3076 tptp.subst)) (= (ho_7 (ho_6 k_5 (F BOUND_VARIABLE_3072 BOUND_VARIABLE_3074)) BOUND_VARIABLE_3076) (ho_7 (ho_6 k_5 (ho_7 (ho_6 k_5 BOUND_VARIABLE_3149) (ho_4 (ho_3 k_2 BOUND_VARIABLE_3074) BOUND_VARIABLE_3072))) BOUND_VARIABLE_3076)))) (not (forall ((BOUND_VARIABLE_3090 tptp.subst) (BOUND_VARIABLE_3092 tptp.term) (BOUND_VARIABLE_3094 tptp.subst)) (= (F (ho_4 (ho_11 k_10 BOUND_VARIABLE_3090) BOUND_VARIABLE_3094) (ho_7 (ho_6 k_5 BOUND_VARIABLE_3092) BOUND_VARIABLE_3094)) (ho_7 (ho_6 k_5 BOUND_VARIABLE_3149) (ho_4 (ho_3 k_2 (ho_7 (ho_6 k_5 BOUND_VARIABLE_3092) BOUND_VARIABLE_3094)) (ho_4 (ho_11 k_10 BOUND_VARIABLE_3090) BOUND_VARIABLE_3094))))))))) (not (forall ((B tptp.term)) (or (not (P tptp.id B tptp.id)) (P tptp.id (ho_7 (ho_6 k_5 BOUND_VARIABLE_3171) (ho_4 (ho_3 k_2 B) tptp.id)) tptp.id)))) (P tptp.id (tptp.lam (ho_7 (ho_6 k_5 BOUND_VARIABLE_3171) (ho_4 (ho_3 k_2 tptp.one) tptp.sh))) tptp.id)))) % 148.02/148.61 (define-fun tptp.induction2lem_gthm () Bool true) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3aa_lthm () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3046 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (not (forall ((B tptp.term)) (or (not (P tptp.id B tptp.id)) (P tptp.id (ho_7 (ho_6 k_5 BOUND_VARIABLE_3046) (ho_4 (ho_3 k_2 B) tptp.id)) tptp.id)))) (P tptp.id (tptp.lam (ho_7 (ho_6 k_5 BOUND_VARIABLE_3046) (ho_4 (ho_3 k_2 tptp.one) tptp.sh))) tptp.id)))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3 () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3211 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (ho_4 (ho_11 k_10 K) N))) (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)) (P M A (ho_4 (ho_11 k_10 K) N))))) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (not (forall ((B tptp.term)) (or (not (P tptp.id B tptp.id)) (P tptp.id (ho_7 (ho_6 k_5 BOUND_VARIABLE_3211) (ho_4 (ho_3 k_2 B) tptp.id)) tptp.id)))) (P tptp.id (tptp.lam BOUND_VARIABLE_3211) tptp.id)))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem2 () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_2999 tptp.term) (BOUND_VARIABLE_3001 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (ho_4 (ho_11 k_10 K) N))) (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)) (P M A (ho_4 (ho_11 k_10 K) N))))) (not (forall ((A tptp.term) (B tptp.term)) (or (not (P tptp.id A tptp.id)) (not (P tptp.id B tptp.id)) (P tptp.id (tptp.ap (ho_7 (ho_6 k_5 A) tptp.id) B) tptp.id)))) (not (P tptp.id BOUND_VARIABLE_2999 tptp.id)) (not (P tptp.id BOUND_VARIABLE_3001 tptp.id)) (P tptp.id (tptp.ap BOUND_VARIABLE_2999 BOUND_VARIABLE_3001) tptp.id)))) % 148.02/148.61 (define-fun tptp.termmset_lthm () Bool (=> (forall ((A tptp.term)) (= A (ho_7 (ho_6 k_5 A) tptp.id))) (forall ((A tptp.term)) (= A (ho_7 (ho_6 k_5 A) tptp.id))))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem1 () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_2965 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (ho_4 (ho_11 k_10 K) N))) (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)) (P M A (ho_4 (ho_11 k_10 K) N))))) (not (forall ((A tptp.term)) (or (not (ho_8 k_9 (ho_7 (ho_6 k_5 A) tptp.id))) (P tptp.id A tptp.id)))) (not (ho_8 k_9 BOUND_VARIABLE_2965)) (P tptp.id BOUND_VARIABLE_2965 tptp.id)))) % 148.02/148.61 (define-fun tptp.hoaslamnotap_lthm () Bool true) % 148.02/148.61 (define-fun tptp.pushprop_lem1v2_lthm () Bool (forall ((P (-> tptp.term Bool)) (Q (-> tptp.term Bool)) (A tptp.term) (M tptp.subst)) (or (not (P A)) (not (forall ((X tptp.term)) (= (Q X) (P (ho_7 (ho_6 k_5 X) (ho_4 (ho_3 k_2 A) M)))))) (Q tptp.one)))) % 148.02/148.61 (define-fun tptp.hoasapnotvar () Bool false) % 148.02/148.61 (define-fun tptp.hoasinduction_lem0 () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool))) (not (forall ((Q (-> tptp.term Bool))) (not (forall ((X tptp.term)) (= (Q X) (P tptp.id X tptp.id)))))))) % 148.02/148.61 (define-fun tptp.hoasinduction () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3283 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (ho_4 (ho_11 k_10 K) N))) (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)) (P M A (ho_4 (ho_11 k_10 K) N))))) (not (forall ((A tptp.term)) (or (not (ho_8 k_9 (ho_7 (ho_6 k_5 A) tptp.id))) (P tptp.id A tptp.id)))) (not (forall ((A tptp.term) (B tptp.term)) (or (not (P tptp.id A tptp.id)) (not (P tptp.id B tptp.id)) (P tptp.id (tptp.ap (ho_7 (ho_6 k_5 A) tptp.id) B) tptp.id)))) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (P tptp.id BOUND_VARIABLE_3283 tptp.id)))) % 148.02/148.61 (define-fun tptp.hoasinduction_gthm () Bool true) % 148.02/148.61 (define-fun tptp.axapp () Bool true) % 148.02/148.61 (define-fun tptp.hoaslamnotvar_lthm () Bool true) % 148.02/148.61 (define-fun tptp.pushprop_lem3v2_lthm () Bool (forall ((P (-> tptp.term Bool)) (Q (-> tptp.term Bool)) (A tptp.term) (M tptp.subst) (BOUND_VARIABLE_2273 tptp.term)) (or (not (forall ((X tptp.term)) (= (Q X) (P (ho_7 (ho_6 k_5 X) (ho_4 (ho_3 k_2 A) M)))))) (not (forall ((B tptp.term)) (or (not (ho_8 k_9 B)) (Q B)))) (not (ho_8 k_9 BOUND_VARIABLE_2273)) (P (ho_7 (ho_6 k_5 BOUND_VARIABLE_2273) (ho_4 (ho_3 k_2 A) M)))))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3b_lthm () Bool (forall ((B tptp.term)) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (not (= (F tptp.sh tptp.one) (ho_7 (ho_6 k_5 B) (ho_4 (ho_3 k_2 tptp.one) tptp.sh)))))))) % 148.02/148.61 (define-fun tptp.ulamvarind () Bool true) % 148.02/148.61 (define-fun tptp.induction () Bool (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2140 tptp.term)) (or (not (forall ((A tptp.term)) (or (not (ho_8 k_9 A)) (P A)))) (not (forall ((A tptp.term) (B tptp.term)) (or (not (P A)) (not (P B)) (P (tptp.ap A B))))) (not (forall ((A tptp.term)) (or (not (P A)) (P (tptp.lam A))))) (P BOUND_VARIABLE_2140)))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3a_lthm () Bool (=> (forall ((A tptp.term)) (= A (ho_7 (ho_6 k_5 A) tptp.id))) (=> (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3046 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (not (forall ((B tptp.term)) (or (not (P tptp.id B tptp.id)) (P tptp.id (ho_7 (ho_6 k_5 BOUND_VARIABLE_3046) (ho_4 (ho_3 k_2 B) tptp.id)) tptp.id)))) (P tptp.id (tptp.lam (ho_7 (ho_6 k_5 BOUND_VARIABLE_3046) (ho_4 (ho_3 k_2 tptp.one) tptp.sh))) tptp.id))) (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3232 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (not (forall ((B tptp.term)) (or (not (P tptp.id B tptp.id)) (P tptp.id (ho_7 (ho_6 k_5 BOUND_VARIABLE_3232) (ho_4 (ho_3 k_2 B) tptp.id)) tptp.id)))) (P tptp.id (tptp.lam BOUND_VARIABLE_3232) tptp.id)))))) % 148.02/148.61 (define-fun tptp.termmset_gthm () Bool true) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3aa () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3046 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (not (forall ((B tptp.term)) (or (not (P tptp.id B tptp.id)) (P tptp.id (ho_7 (ho_6 k_5 BOUND_VARIABLE_3046) (ho_4 (ho_3 k_2 B) tptp.id)) tptp.id)))) (P tptp.id (tptp.lam (ho_7 (ho_6 k_5 BOUND_VARIABLE_3046) (ho_4 (ho_3 k_2 tptp.one) tptp.sh))) tptp.id)))) % 148.02/148.61 (define-fun tptp.pushprop_lem1v2_gthm () Bool true) % 148.02/148.61 (define-fun tptp.hoaslamnotap_gthm () Bool true) % 148.02/148.61 (define-fun tptp.hoaslamnotvar_gthm () Bool true) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3b_gthm () Bool true) % 148.02/148.61 (define-fun tptp.pushprop_lem2v2 () Bool true) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3a_gthm () Bool true) % 148.02/148.61 (define-fun tptp.axclos () Bool true) % 148.02/148.61 (define-fun tptp.axassoc () Bool true) % 148.02/148.61 (define-fun tptp.hoasinduction_lem2v2 () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool)) (BOUND_VARIABLE_2820 tptp.term) (BOUND_VARIABLE_2822 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (ho_4 (ho_11 k_10 K) N))) (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)) (P M A (ho_4 (ho_11 k_10 K) N))))) (not (forall ((A tptp.term) (B tptp.term)) (or (not (P tptp.id A tptp.id)) (not (P tptp.id B tptp.id)) (P tptp.id (tptp.ap (ho_7 (ho_6 k_5 A) tptp.id) B) tptp.id)))) (not (forall ((X tptp.term)) (= (Q X) (P tptp.id X tptp.id)))) (not (Q BOUND_VARIABLE_2820)) (not (Q BOUND_VARIABLE_2822)) (Q (tptp.ap BOUND_VARIABLE_2820 BOUND_VARIABLE_2822))))) % 148.02/148.61 (define-fun tptp.pushprop_lthm () Bool (=> (forall ((P (-> tptp.term Bool)) (A tptp.term) (M tptp.subst)) (not (forall ((Q (-> tptp.term Bool))) (not (forall ((X tptp.term)) (= (Q X) (P (ho_7 (ho_6 k_5 X) (ho_4 (ho_3 k_2 A) M))))))))) (forall ((P (-> tptp.term Bool)) (A tptp.term) (M tptp.subst) (BOUND_VARIABLE_2295 tptp.term)) (or (not (forall ((B tptp.term)) (or (not (ho_8 k_9 B)) (P (ho_7 (ho_6 k_5 B) M))))) (not (P A)) (not (ho_8 k_9 BOUND_VARIABLE_2295)) (P (ho_7 (ho_6 k_5 BOUND_VARIABLE_2295) (ho_4 (ho_3 k_2 A) M))))))) % 148.02/148.61 (define-fun tptp.apinj2 () Bool (forall ((A tptp.term) (B tptp.term) (C tptp.term) (D tptp.term)) (or (not (= (tptp.ap A C) (tptp.ap B D))) (= C D)))) % 148.02/148.61 (define-fun tptp.apinj1 () Bool (forall ((A tptp.term) (B tptp.term) (C tptp.term) (D tptp.term)) (or (not (= (tptp.ap A C) (tptp.ap B D))) (= A B)))) % 148.02/148.61 (define-fun tptp.hoasapinj2_lthm () Bool (=> (forall ((A tptp.term) (B tptp.term) (C tptp.term) (D tptp.term)) (or (not (= (tptp.ap A C) (tptp.ap B D))) (= C D))) (forall ((A tptp.term) (B tptp.term) (C tptp.term) (D tptp.term)) (or (not (= (tptp.ap (ho_7 (ho_6 k_5 A) tptp.id) C) (tptp.ap (ho_7 (ho_6 k_5 B) tptp.id) D))) (= C D))))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3v2a () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool)) (BOUND_VARIABLE_2931 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (not (forall ((X tptp.term)) (= (Q X) (P tptp.id X tptp.id)))) (not (forall ((B tptp.term)) (or (not (Q B)) (Q (ho_7 (ho_6 k_5 BOUND_VARIABLE_2931) (ho_4 (ho_3 k_2 B) tptp.id)))))) (Q (tptp.lam BOUND_VARIABLE_2931))))) % 148.02/148.61 (define-fun tptp.hoasapinj1_lthm () Bool (=> (forall ((A tptp.term)) (= A (ho_7 (ho_6 k_5 A) tptp.id))) (=> (forall ((A tptp.term) (B tptp.term) (C tptp.term) (D tptp.term)) (or (not (= (tptp.ap A C) (tptp.ap B D))) (= A B))) (forall ((A tptp.term) (B tptp.term) (C tptp.term) (D tptp.term)) (or (not (= (tptp.ap (ho_7 (ho_6 k_5 A) tptp.id) C) (tptp.ap (ho_7 (ho_6 k_5 B) tptp.id) D))) (= A B)))))) % 148.02/148.61 (define-fun tptp.hoaslaminj_lthm () Bool (=> (forall ((A tptp.term) (B tptp.term)) (or (not (= (tptp.lam A) (tptp.lam B))) (= A B))) (forall ((F (-> tptp.subst tptp.term tptp.term)) (BOUND_VARIABLE_2547 (-> tptp.subst tptp.term tptp.term)) (BOUND_VARIABLE_2549 tptp.subst) (BOUND_VARIABLE_2551 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (BOUND_VARIABLE_2547 M A)) N) (BOUND_VARIABLE_2547 (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (= (tptp.lam (F tptp.sh tptp.one)) (tptp.lam (BOUND_VARIABLE_2547 tptp.sh tptp.one)))) (= (F BOUND_VARIABLE_2549 BOUND_VARIABLE_2551) (BOUND_VARIABLE_2547 BOUND_VARIABLE_2549 BOUND_VARIABLE_2551)))))) % 148.02/148.61 (define-fun tptp.axvarcons () Bool true) % 148.02/148.61 (define-fun tptp.hoaslam ((BOUND_VARIABLE_25313 tptp.subst) (BOUND_VARIABLE_25315 (-> tptp.subst tptp.term tptp.term))) tptp.term (as @tptp.term_0 tptp.term)) % 148.02/148.61 (define-fun tptp.axscons () Bool (forall ((M tptp.subst)) (= M (ho_4 (ho_3 k_2 (ho_7 (ho_6 k_5 tptp.one) M)) (ho_4 (ho_11 k_10 tptp.sh) M))))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem2v2_gthm () Bool true) % 148.02/148.61 (define-fun tptp.axidr () Bool (forall ((M tptp.subst)) (= M (ho_4 (ho_11 k_10 M) tptp.id)))) % 148.02/148.61 (define-fun tptp.pushprop_lem1 () Bool (forall ((P (-> tptp.term Bool)) (K (-> tptp.term Bool)) (A tptp.term) (M tptp.subst) (B tptp.term)) (or (not (P A)) (K (ho_7 (ho_6 k_5 A) (ho_4 (ho_3 k_2 B) M)))))) % 148.02/148.61 (define-fun tptp.laminj () Bool (forall ((A tptp.term) (B tptp.term)) (or (not (= (tptp.lam A) (tptp.lam B))) (= A B)))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3_lthm () Bool (=> (forall ((A tptp.term)) (= A (ho_7 (ho_6 k_5 A) tptp.id))) (=> (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3046 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (not (forall ((B tptp.term)) (or (not (P tptp.id B tptp.id)) (P tptp.id (ho_7 (ho_6 k_5 BOUND_VARIABLE_3046) (ho_4 (ho_3 k_2 B) tptp.id)) tptp.id)))) (P tptp.id (tptp.lam (ho_7 (ho_6 k_5 BOUND_VARIABLE_3046) (ho_4 (ho_3 k_2 tptp.one) tptp.sh))) tptp.id))) (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3211 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (ho_4 (ho_11 k_10 K) N))) (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)) (P M A (ho_4 (ho_11 k_10 K) N))))) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (not (forall ((B tptp.term)) (or (not (P tptp.id B tptp.id)) (P tptp.id (ho_7 (ho_6 k_5 BOUND_VARIABLE_3211) (ho_4 (ho_3 k_2 B) tptp.id)) tptp.id)))) (P tptp.id (tptp.lam BOUND_VARIABLE_3211) tptp.id)))))) % 148.02/148.61 (define-fun tptp.pushprop_lem0 () Bool (forall ((P (-> tptp.term Bool)) (A tptp.term) (M tptp.subst)) (not (forall ((Q (-> tptp.term Bool))) (not (forall ((X tptp.term)) (= (Q X) (P (ho_7 (ho_6 k_5 X) (ho_4 (ho_3 k_2 A) M)))))))))) % 148.02/148.61 (define-fun tptp.pushprop_gthm () Bool true) % 148.02/148.61 (define-fun tptp.axabs () Bool true) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3v2a_lthm () Bool (=> (forall ((B tptp.term)) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (not (forall ((A tptp.term) (M tptp.subst)) (= (F M A) (ho_7 (ho_6 k_5 B) (ho_4 (ho_3 k_2 A) M)))))))) (=> (forall ((A tptp.term)) (= A (ho_7 (ho_6 k_5 A) tptp.id))) (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool)) (BOUND_VARIABLE_2931 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (not (forall ((X tptp.term)) (= (Q X) (P tptp.id X tptp.id)))) (not (forall ((B tptp.term)) (or (not (Q B)) (Q (ho_7 (ho_6 k_5 BOUND_VARIABLE_2931) (ho_4 (ho_3 k_2 B) tptp.id)))))) (Q (tptp.lam BOUND_VARIABLE_2931))))))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem2_lthm () Bool true) % 148.02/148.61 (define-fun tptp.hoasapinj2_gthm () Bool true) % 148.02/148.61 (define-fun tptp.hoasinduction_p_and_p_prime ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool))) Bool (forall ((X tptp.term)) (= (Q X) (P tptp.id X tptp.id)))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem1_lthm () Bool true) % 148.02/148.61 (define-fun tptp.lamnotap () Bool false) % 148.02/148.61 (define-fun tptp.hoasapinj1_gthm () Bool true) % 148.02/148.61 (define-fun tptp.hoaslamnotvar () Bool (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (ho_8 k_9 (ho_7 (ho_6 k_5 (tptp.lam (F tptp.sh tptp.one))) tptp.id)))))) % 148.02/148.61 (define-fun tptp.axidl () Bool (forall ((M tptp.subst)) (= M (ho_4 (ho_11 k_10 tptp.id) M)))) % 148.02/148.61 (define-fun tptp.hoaslaminj_gthm () Bool true) % 148.02/148.61 (define-fun tptp.induction2_lthm () Bool (=> (forall ((A tptp.term)) (= A (ho_7 (ho_6 k_5 A) tptp.id))) (=> (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2340 tptp.term) (BOUND_VARIABLE_2342 tptp.subst)) (or (not (forall ((A tptp.term) (B tptp.term)) (or (not (P A)) (not (P B)) (P (tptp.ap A B))))) (not (forall ((A tptp.term)) (or (not (forall ((B tptp.term)) (or (not (P B)) (P (ho_7 (ho_6 k_5 A) (ho_4 (ho_3 k_2 B) tptp.id)))))) (P (tptp.lam A))))) (not (forall ((B tptp.term)) (or (not (ho_8 k_9 B)) (P (ho_7 (ho_6 k_5 B) BOUND_VARIABLE_2342))))) (P (ho_7 (ho_6 k_5 BOUND_VARIABLE_2340) BOUND_VARIABLE_2342)))) (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2367 tptp.term)) (or (not (forall ((A tptp.term)) (or (not (ho_8 k_9 A)) (P A)))) (not (forall ((A tptp.term) (B tptp.term)) (or (not (P A)) (not (P B)) (P (tptp.ap A B))))) (not (forall ((A tptp.term)) (or (not (forall ((B tptp.term)) (or (not (P B)) (P (ho_7 (ho_6 k_5 A) (ho_4 (ho_3 k_2 B) tptp.id)))))) (P (tptp.lam A))))) (P BOUND_VARIABLE_2367)))))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem0_lthm () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool))) (not (forall ((Q (-> tptp.term Bool))) (not (forall ((X tptp.term)) (= (Q X) (P tptp.id X tptp.id)))))))) % 148.02/148.61 (define-fun tptp.substmonoid_lthm () Bool (=> (forall ((M tptp.subst)) (= M (ho_4 (ho_11 k_10 tptp.id) M))) (=> (forall ((M tptp.subst)) (= M (ho_4 (ho_11 k_10 M) tptp.id))) (and (forall ((M tptp.subst)) (= M (ho_4 (ho_11 k_10 tptp.id) M))) (forall ((M tptp.subst)) (= M (ho_4 (ho_11 k_10 M) tptp.id))))))) % 148.02/148.61 (define-fun tptp.pushprop () Bool (forall ((P (-> tptp.term Bool)) (A tptp.term) (M tptp.subst) (BOUND_VARIABLE_2295 tptp.term)) (or (not (forall ((B tptp.term)) (or (not (ho_8 k_9 B)) (P (ho_7 (ho_6 k_5 B) M))))) (not (P A)) (not (ho_8 k_9 BOUND_VARIABLE_2295)) (P (ho_7 (ho_6 k_5 BOUND_VARIABLE_2295) (ho_4 (ho_3 k_2 A) M)))))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3_gthm () Bool true) % 148.02/148.61 (define-fun tptp.hoasinduction_lem2_gthm () Bool true) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3b () Bool (forall ((B tptp.term)) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (not (= (F tptp.sh tptp.one) (ho_7 (ho_6 k_5 B) (ho_4 (ho_3 k_2 tptp.one) tptp.sh)))))))) % 148.02/148.61 (define-fun tptp.substmonoid () Bool (and (forall ((M tptp.subst)) (= M (ho_4 (ho_11 k_10 tptp.id) M))) (forall ((M tptp.subst)) (= M (ho_4 (ho_11 k_10 M) tptp.id))))) % 148.02/148.61 (define-fun tptp.lamnotvar () Bool false) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3a () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3232 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (not (forall ((B tptp.term)) (or (not (P tptp.id B tptp.id)) (P tptp.id (ho_7 (ho_6 k_5 BOUND_VARIABLE_3232) (ho_4 (ho_3 k_2 B) tptp.id)) tptp.id)))) (P tptp.id (tptp.lam BOUND_VARIABLE_3232) tptp.id)))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem1_gthm () Bool true) % 148.02/148.61 (define-fun tptp.hoasinduction_no_psi_cond () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3295 tptp.term)) (or (not (forall ((A tptp.term) (B tptp.term)) (or (not (P tptp.id A tptp.id)) (not (P tptp.id B tptp.id)) (P tptp.id (tptp.ap (ho_7 (ho_6 k_5 A) tptp.id) B) tptp.id)))) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (P tptp.id BOUND_VARIABLE_3295 tptp.id)))) % 148.02/148.61 (define-fun tptp.induction2_gthm () Bool true) % 148.02/148.61 (define-fun tptp.pushprop_lem2v2_lthm () Bool true) % 148.02/148.61 (define-fun tptp.hoasvar ((BOUND_VARIABLE_25945 tptp.subst) (BOUND_VARIABLE_25947 tptp.term) (BOUND_VARIABLE_25949 tptp.subst)) Bool true) % 148.02/148.61 (define-fun tptp.hoaslamnotap () Bool (forall ((F (-> tptp.subst tptp.term tptp.term)) (BOUND_VARIABLE_2603 tptp.term) (BOUND_VARIABLE_2605 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (= (tptp.lam (F tptp.sh tptp.one)) (tptp.ap (ho_7 (ho_6 k_5 BOUND_VARIABLE_2603) tptp.id) BOUND_VARIABLE_2605)))))) % 148.02/148.61 (define-fun tptp.substmonoid_gthm () Bool true) % 148.02/148.61 (define-fun tptp.ulamvarsh () Bool true) % 148.02/148.61 (define-fun tptp.induction2 () Bool (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2367 tptp.term)) (or (not (forall ((A tptp.term)) (or (not (ho_8 k_9 A)) (P A)))) (not (forall ((A tptp.term) (B tptp.term)) (or (not (P A)) (not (P B)) (P (tptp.ap A B))))) (not (forall ((A tptp.term)) (or (not (forall ((B tptp.term)) (or (not (P B)) (P (ho_7 (ho_6 k_5 A) (ho_4 (ho_3 k_2 B) tptp.id)))))) (P (tptp.lam A))))) (P BOUND_VARIABLE_2367)))) % 148.02/148.61 (define-fun tptp.pushprop_lem3v2 () Bool (forall ((P (-> tptp.term Bool)) (Q (-> tptp.term Bool)) (A tptp.term) (M tptp.subst) (BOUND_VARIABLE_2273 tptp.term)) (or (not (forall ((X tptp.term)) (= (Q X) (P (ho_7 (ho_6 k_5 X) (ho_4 (ho_3 k_2 A) M)))))) (not (forall ((B tptp.term)) (or (not (ho_8 k_9 B)) (Q B)))) (not (ho_8 k_9 BOUND_VARIABLE_2273)) (P (ho_7 (ho_6 k_5 BOUND_VARIABLE_2273) (ho_4 (ho_3 k_2 A) M)))))) % 148.02/148.61 (define-fun tptp.pushprop_lem2v2_gthm () Bool true) % 148.02/148.61 (define-fun tptp.pushprop_lem1_lthm () Bool (forall ((P (-> tptp.term Bool)) (K (-> tptp.term Bool)) (A tptp.term) (M tptp.subst) (B tptp.term)) (or (not (P A)) (K (ho_7 (ho_6 k_5 A) (ho_4 (ho_3 k_2 B) M)))))) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3v2 () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool)) (BOUND_VARIABLE_2910 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (ho_4 (ho_11 k_10 K) N))) (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)) (P M A (ho_4 (ho_11 k_10 K) N))))) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (not (forall ((X tptp.term)) (= (Q X) (P tptp.id X tptp.id)))) (not (forall ((B tptp.term)) (or (not (Q B)) (Q (ho_7 (ho_6 k_5 BOUND_VARIABLE_2910) (ho_4 (ho_3 k_2 B) tptp.id)))))) (Q (tptp.lam BOUND_VARIABLE_2910))))) % 148.02/148.61 (define-fun tptp.axshiftcons () Bool true) % 148.02/148.61 (define-fun tptp.termmset () Bool (forall ((A tptp.term)) (= A (ho_7 (ho_6 k_5 A) tptp.id)))) % 148.02/148.61 (define-fun tptp.pushprop_lem0_lthm () Bool (forall ((P (-> tptp.term Bool)) (A tptp.term) (M tptp.subst)) (not (forall ((Q (-> tptp.term Bool))) (not (forall ((X tptp.term)) (= (Q X) (P (ho_7 (ho_6 k_5 X) (ho_4 (ho_3 k_2 A) M)))))))))) % 148.02/148.61 (define-fun tptp.hoasapnotvar_lthm () Bool true) % 148.02/148.61 (define-fun tptp.hoasinduction_lem3v2_lthm () Bool (=> (forall ((A tptp.term)) (= A (ho_7 (ho_6 k_5 A) tptp.id))) (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool)) (BOUND_VARIABLE_2910 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (ho_4 (ho_11 k_10 K) N))) (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)) (P M A (ho_4 (ho_11 k_10 K) N))))) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (not (forall ((X tptp.term)) (= (Q X) (P tptp.id X tptp.id)))) (not (forall ((B tptp.term)) (or (not (Q B)) (Q (ho_7 (ho_6 k_5 BOUND_VARIABLE_2910) (ho_4 (ho_3 k_2 B) tptp.id)))))) (Q (tptp.lam BOUND_VARIABLE_2910)))))) % 148.02/148.62 (define-fun tptp.pushprop_p_and_p_prime ((A tptp.term) (M tptp.subst) (P (-> tptp.term Bool)) (Q (-> tptp.term Bool))) Bool (forall ((X tptp.term)) (= (Q X) (P (ho_7 (ho_6 k_5 X) (ho_4 (ho_3 k_2 A) M)))))) % 148.02/148.62 (define-fun tptp.axvarid () Bool (forall ((A tptp.term)) (= A (ho_7 (ho_6 k_5 A) tptp.id)))) % 148.02/148.62 (define-fun tptp.hoasinduction_lthm_3 () Bool (=> (forall ((P (-> tptp.subst tptp.term tptp.subst Bool))) (not (forall ((Q (-> tptp.term Bool))) (not (forall ((X tptp.term)) (= (Q X) (P tptp.id X tptp.id))))))) (=> (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2367 tptp.term)) (or (not (forall ((A tptp.term)) (or (not (ho_8 k_9 A)) (P A)))) (not (forall ((A tptp.term) (B tptp.term)) (or (not (P A)) (not (P B)) (P (tptp.ap A B))))) (not (forall ((A tptp.term)) (or (not (forall ((B tptp.term)) (or (not (P B)) (P (ho_7 (ho_6 k_5 A) (ho_4 (ho_3 k_2 B) tptp.id)))))) (P (tptp.lam A))))) (P BOUND_VARIABLE_2367))) (=> (forall ((A tptp.term)) (= A (ho_7 (ho_6 k_5 A) tptp.id))) (=> (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool)) (BOUND_VARIABLE_2931 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (not (forall ((X tptp.term)) (= (Q X) (P tptp.id X tptp.id)))) (not (forall ((B tptp.term)) (or (not (Q B)) (Q (ho_7 (ho_6 k_5 BOUND_VARIABLE_2931) (ho_4 (ho_3 k_2 B) tptp.id)))))) (Q (tptp.lam BOUND_VARIABLE_2931)))) (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3283 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (ho_4 (ho_11 k_10 K) N))) (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (ho_4 (ho_11 k_10 M) K) (ho_7 (ho_6 k_5 A) K) N)) (P M A (ho_4 (ho_11 k_10 K) N))))) (not (forall ((A tptp.term)) (or (not (ho_8 k_9 (ho_7 (ho_6 k_5 A) tptp.id))) (P tptp.id A tptp.id)))) (not (forall ((A tptp.term) (B tptp.term)) (or (not (P tptp.id A tptp.id)) (not (P tptp.id B tptp.id)) (P tptp.id (tptp.ap (ho_7 (ho_6 k_5 A) tptp.id) B) tptp.id)))) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (ho_7 (ho_6 k_5 (F M A)) N) (F (ho_4 (ho_11 k_10 M) N) (ho_7 (ho_6 k_5 A) N))))) (not (forall ((A tptp.term)) (or (not (P tptp.id A tptp.id)) (P tptp.id (F tptp.id A) tptp.id)))) (P tptp.id (tptp.lam (F tptp.sh tptp.one)) tptp.id)))) (P tptp.id BOUND_VARIABLE_3283 tptp.id)))))))) % 148.02/148.62 ) % 148.02/148.62 % SZS output end Model % 148.02/148.62 % cvc5 exiting %------------------------------------------------------------------------------