%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : ALG444^1 : TPTP v9.2.1. Released v6.4.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n026.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:29 AM UTC 2026 % Result : Satisfiable 0.40s 0.66s % Output : Model 0.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ALG444^1 : TPTP v9.2.1. Released v6.4.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.16/0.34 % Computer : n026.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Wed Jun 3 02:13:55 EDT 2026 % 0.16/0.34 % CPUTime : % 0.30/0.55 %----Disproving TH0 % 0.40/0.56 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 72s... % 0.40/0.66 % SZS status Satisfiable % 0.40/0.66 % SZS output start Model % 0.40/0.68 ( % 0.40/0.68 ; cardinality of $$unsorted is 1 % 0.40/0.68 ; rep: (as @$$unsorted_0 $$unsorted) % 0.40/0.68 ; cardinality of tptp.term is 1 % 0.40/0.68 ; rep: (as @tptp.term_0 tptp.term) % 0.40/0.68 ; cardinality of tptp.subst is 1 % 0.40/0.68 ; rep: (as @tptp.subst_0 tptp.subst) % 0.40/0.68 (define-fun tptp.one () tptp.term (as @tptp.term_0 tptp.term)) % 0.40/0.68 (define-fun tptp.ap ((BOUND_VARIABLE_4416 tptp.term) (BOUND_VARIABLE_4418 tptp.term)) tptp.term (as @tptp.term_0 tptp.term)) % 0.40/0.68 (define-fun tptp.lam ((BOUND_VARIABLE_4426 tptp.term)) tptp.term (as @tptp.term_0 tptp.term)) % 0.40/0.68 (define-fun tptp.sub ((BOUND_VARIABLE_4441 tptp.term) (BOUND_VARIABLE_4443 tptp.subst)) tptp.term (as @tptp.term_0 tptp.term)) % 0.40/0.68 (define-fun tptp.id () tptp.subst (as @tptp.subst_0 tptp.subst)) % 0.40/0.68 (define-fun tptp.sh () tptp.subst (as @tptp.subst_0 tptp.subst)) % 0.40/0.68 (define-fun tptp.push ((BOUND_VARIABLE_4458 tptp.term) (BOUND_VARIABLE_4460 tptp.subst)) tptp.subst (as @tptp.subst_0 tptp.subst)) % 0.40/0.68 (define-fun tptp.comp ((BOUND_VARIABLE_4473 tptp.subst) (BOUND_VARIABLE_4475 tptp.subst)) tptp.subst (as @tptp.subst_0 tptp.subst)) % 0.40/0.68 (define-fun tptp.var ((BOUND_VARIABLE_4485 tptp.term)) Bool false) % 0.40/0.68 (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 (tptp.sub X (tptp.push A M)))))) (Q tptp.one)))) % 0.40/0.68 (define-fun tptp.pushprop_lem1_gthm () Bool true) % 0.40/0.68 (define-fun tptp.axmap () Bool true) % 0.40/0.68 (define-fun tptp.pushprop_lem0_gthm () Bool true) % 0.40/0.68 (define-fun tptp.shinj () Bool (forall ((A tptp.term) (B tptp.term)) (or (not (= (tptp.sub A tptp.sh) (tptp.sub B tptp.sh))) (= A B)))) % 0.40/0.68 (define-fun tptp.hoasinduction_lem1v2 () Bool true) % 0.40/0.68 (define-fun tptp.hoasinduction_lem1v2_gthm () Bool true) % 0.40/0.68 (define-fun tptp.hoasap ((BOUND_VARIABLE_4706 tptp.subst) (BOUND_VARIABLE_4708 tptp.term) (BOUND_VARIABLE_4710 tptp.subst) (BOUND_VARIABLE_4713 tptp.term)) tptp.term (as @tptp.term_0 tptp.term)) % 0.40/0.68 (define-fun tptp.induction2lem () Bool (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2338 tptp.term) (BOUND_VARIABLE_2340 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 (tptp.sub A (tptp.push B tptp.id)))))) (P (tptp.lam A))))) (not (forall ((B tptp.term)) (or (not (tptp.var B)) (P (tptp.sub B BOUND_VARIABLE_2340))))) (P (tptp.sub BOUND_VARIABLE_2338 BOUND_VARIABLE_2340))))) % 0.40/0.68 (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)) (= (tptp.sub B (tptp.push A M)) (F M A)))))))) % 0.40/0.68 (define-fun tptp.axvarshift () Bool true) % 0.40/0.68 (define-fun tptp.hoasapinj2 () Bool (forall ((A tptp.term) (B tptp.term) (C tptp.term) (D tptp.term)) (or (not (= (tptp.ap (tptp.sub A tptp.id) C) (tptp.ap (tptp.sub B tptp.id) D))) (= C D)))) % 0.40/0.68 (define-fun tptp.hoasapnotvar_gthm () Bool true) % 0.40/0.68 (define-fun tptp.hoasapinj1 () Bool (forall ((A tptp.term) (B tptp.term) (C tptp.term) (D tptp.term)) (or (not (= (tptp.ap (tptp.sub A tptp.id) C) (tptp.ap (tptp.sub B tptp.id) D))) (= A B)))) % 0.40/0.68 (define-fun tptp.ulamvar1 () Bool false) % 0.40/0.68 (define-fun tptp.induction2lem_lthm () Bool (=> (forall ((A tptp.term) (M tptp.subst)) (= A (tptp.sub tptp.one (tptp.push A M)))) (=> (forall ((A tptp.term) (M tptp.subst)) (= M (tptp.comp tptp.sh (tptp.push A M)))) (=> (forall ((M tptp.subst)) (= M (tptp.comp M tptp.id))) (=> (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2138 tptp.term)) (or (not (forall ((A tptp.term)) (or (not (tptp.var 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_2138))) (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2338 tptp.term) (BOUND_VARIABLE_2340 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 (tptp.sub A (tptp.push B tptp.id)))))) (P (tptp.lam A))))) (not (forall ((B tptp.term)) (or (not (tptp.var B)) (P (tptp.sub B BOUND_VARIABLE_2340))))) (P (tptp.sub BOUND_VARIABLE_2338 BOUND_VARIABLE_2340))))))))) % 0.40/0.68 (define-fun tptp.hoasinduction_lem3v2_gthm () Bool true) % 0.40/0.68 (define-fun tptp.apnotvar () Bool true) % 0.40/0.68 (define-fun tptp.pushprop_lthm_orig () Bool true) % 0.40/0.68 (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)) (= (tptp.sub B (tptp.push A M)) (F M A)))))))) % 0.40/0.68 (define-fun tptp.hoasinduction_lthm () Bool (=> (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2365 tptp.term)) (or (not (forall ((A tptp.term)) (or (not (tptp.var 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 (tptp.sub A (tptp.push B tptp.id)))))) (P (tptp.lam A))))) (P BOUND_VARIABLE_2365))) (=> (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_2997 tptp.term) (BOUND_VARIABLE_2999 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (tptp.comp K N))) (P (tptp.comp M K) (tptp.sub A K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (tptp.comp M K) (tptp.sub A K) N)) (P M A (tptp.comp 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 (tptp.sub A tptp.id) B) tptp.id)))) (not (P tptp.id BOUND_VARIABLE_2997 tptp.id)) (not (P tptp.id BOUND_VARIABLE_2999 tptp.id)) (P tptp.id (tptp.ap BOUND_VARIABLE_2997 BOUND_VARIABLE_2999) tptp.id))) (=> (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3209 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (tptp.comp K N))) (P (tptp.comp M K) (tptp.sub A K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (tptp.comp M K) (tptp.sub A K) N)) (P M A (tptp.comp K N))))) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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 (tptp.sub BOUND_VARIABLE_3209 (tptp.push B tptp.id)) tptp.id)))) (P tptp.id (tptp.lam BOUND_VARIABLE_3209) tptp.id))) (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3281 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (tptp.comp K N))) (P (tptp.comp M K) (tptp.sub A K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (tptp.comp M K) (tptp.sub A K) N)) (P M A (tptp.comp K N))))) (not (forall ((A tptp.term)) (or (not (tptp.var (tptp.sub 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 (tptp.sub 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)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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_3281 tptp.id))))))) % 0.40/0.68 (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_2365 tptp.term)) (or (not (forall ((A tptp.term)) (or (not (tptp.var 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 (tptp.sub A (tptp.push B tptp.id)))))) (P (tptp.lam A))))) (P BOUND_VARIABLE_2365))) (=> (forall ((A tptp.term)) (= A (tptp.sub A tptp.id))) (=> (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool)) (BOUND_VARIABLE_2929 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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 (tptp.sub BOUND_VARIABLE_2929 (tptp.push B tptp.id)))))) (Q (tptp.lam BOUND_VARIABLE_2929)))) (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3293 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 (tptp.sub 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)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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_3293 tptp.id)))))))) % 0.40/0.68 (define-fun tptp.hoaslaminj () Bool (forall ((F (-> tptp.subst tptp.term tptp.term)) (BOUND_VARIABLE_2545 (-> tptp.subst tptp.term tptp.term)) (BOUND_VARIABLE_2547 tptp.subst) (BOUND_VARIABLE_2549 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub A N))))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (BOUND_VARIABLE_2545 M A) N) (BOUND_VARIABLE_2545 (tptp.comp M N) (tptp.sub A N))))) (not (= (tptp.lam (F tptp.sh tptp.one)) (tptp.lam (BOUND_VARIABLE_2545 tptp.sh tptp.one)))) (= (F BOUND_VARIABLE_2547 BOUND_VARIABLE_2549) (BOUND_VARIABLE_2545 BOUND_VARIABLE_2547 BOUND_VARIABLE_2549))))) % 0.40/0.68 (define-fun tptp.hoasinduction_lem3aaa () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3169 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term)) (BOUND_VARIABLE_3147 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_3070 tptp.subst) (BOUND_VARIABLE_3072 tptp.term) (BOUND_VARIABLE_3074 tptp.subst)) (= (tptp.sub (F BOUND_VARIABLE_3070 BOUND_VARIABLE_3072) BOUND_VARIABLE_3074) (tptp.sub (tptp.sub BOUND_VARIABLE_3147 (tptp.push BOUND_VARIABLE_3072 BOUND_VARIABLE_3070)) BOUND_VARIABLE_3074)))) (not (forall ((BOUND_VARIABLE_3088 tptp.subst) (BOUND_VARIABLE_3090 tptp.term) (BOUND_VARIABLE_3092 tptp.subst)) (= (F (tptp.comp BOUND_VARIABLE_3088 BOUND_VARIABLE_3092) (tptp.sub BOUND_VARIABLE_3090 BOUND_VARIABLE_3092)) (tptp.sub BOUND_VARIABLE_3147 (tptp.push (tptp.sub BOUND_VARIABLE_3090 BOUND_VARIABLE_3092) (tptp.comp BOUND_VARIABLE_3088 BOUND_VARIABLE_3092))))))))) (not (forall ((B tptp.term)) (or (not (P tptp.id B tptp.id)) (P tptp.id (tptp.sub BOUND_VARIABLE_3169 (tptp.push B tptp.id)) tptp.id)))) (P tptp.id (tptp.lam (tptp.sub BOUND_VARIABLE_3169 (tptp.push tptp.one tptp.sh))) tptp.id)))) % 0.40/0.68 (define-fun tptp.induction2lem_gthm () Bool true) % 0.40/0.68 (define-fun tptp.hoasinduction_lem3aa_lthm () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3044 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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 (tptp.sub BOUND_VARIABLE_3044 (tptp.push B tptp.id)) tptp.id)))) (P tptp.id (tptp.lam (tptp.sub BOUND_VARIABLE_3044 (tptp.push tptp.one tptp.sh))) tptp.id)))) % 0.40/0.68 (define-fun tptp.hoasinduction_lem3 () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3209 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (tptp.comp K N))) (P (tptp.comp M K) (tptp.sub A K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (tptp.comp M K) (tptp.sub A K) N)) (P M A (tptp.comp K N))))) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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 (tptp.sub BOUND_VARIABLE_3209 (tptp.push B tptp.id)) tptp.id)))) (P tptp.id (tptp.lam BOUND_VARIABLE_3209) tptp.id)))) % 0.40/0.68 (define-fun tptp.hoasinduction_lem2 () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_2997 tptp.term) (BOUND_VARIABLE_2999 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (tptp.comp K N))) (P (tptp.comp M K) (tptp.sub A K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (tptp.comp M K) (tptp.sub A K) N)) (P M A (tptp.comp 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 (tptp.sub A tptp.id) B) tptp.id)))) (not (P tptp.id BOUND_VARIABLE_2997 tptp.id)) (not (P tptp.id BOUND_VARIABLE_2999 tptp.id)) (P tptp.id (tptp.ap BOUND_VARIABLE_2997 BOUND_VARIABLE_2999) tptp.id)))) % 0.40/0.68 (define-fun tptp.termmset_lthm () Bool (=> (forall ((A tptp.term)) (= A (tptp.sub A tptp.id))) (forall ((A tptp.term)) (= A (tptp.sub A tptp.id))))) % 0.40/0.68 (define-fun tptp.hoasinduction_lem1 () Bool true) % 0.40/0.68 (define-fun tptp.hoaslamnotap_lthm () Bool true) % 0.40/0.68 (define-fun tptp.pushprop_lem1v2_lthm () Bool (=> (forall ((A tptp.term) (M tptp.subst)) (= A (tptp.sub tptp.one (tptp.push A M)))) (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 (tptp.sub X (tptp.push A M)))))) (Q tptp.one))))) % 0.40/0.68 (define-fun tptp.hoasapnotvar () Bool true) % 0.40/0.68 (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)))))))) % 0.40/0.68 (define-fun tptp.hoasinduction () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3281 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (tptp.comp K N))) (P (tptp.comp M K) (tptp.sub A K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (tptp.comp M K) (tptp.sub A K) N)) (P M A (tptp.comp K N))))) (not (forall ((A tptp.term)) (or (not (tptp.var (tptp.sub 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 (tptp.sub 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)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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_3281 tptp.id)))) % 0.40/0.68 (define-fun tptp.hoasinduction_gthm () Bool true) % 0.40/0.68 (define-fun tptp.axapp () Bool true) % 0.40/0.68 (define-fun tptp.hoaslamnotvar_lthm () Bool true) % 0.40/0.68 (define-fun tptp.pushprop_lem3v2_lthm () Bool true) % 0.40/0.68 (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) (tptp.sub B (tptp.push tptp.one tptp.sh)))))))) % 0.40/0.68 (define-fun tptp.ulamvarind () Bool true) % 0.40/0.68 (define-fun tptp.induction () Bool (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2138 tptp.term)) (or (not (forall ((A tptp.term)) (or (not (tptp.var 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_2138)))) % 0.40/0.68 (define-fun tptp.hoasinduction_lem3a_lthm () Bool (=> (forall ((A tptp.term)) (= A (tptp.sub A tptp.id))) (=> (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3044 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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 (tptp.sub BOUND_VARIABLE_3044 (tptp.push B tptp.id)) tptp.id)))) (P tptp.id (tptp.lam (tptp.sub BOUND_VARIABLE_3044 (tptp.push tptp.one tptp.sh))) tptp.id))) (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3230 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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 (tptp.sub BOUND_VARIABLE_3230 (tptp.push B tptp.id)) tptp.id)))) (P tptp.id (tptp.lam BOUND_VARIABLE_3230) tptp.id)))))) % 0.40/0.68 (define-fun tptp.termmset_gthm () Bool true) % 0.40/0.68 (define-fun tptp.hoasinduction_lem3aa () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3044 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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 (tptp.sub BOUND_VARIABLE_3044 (tptp.push B tptp.id)) tptp.id)))) (P tptp.id (tptp.lam (tptp.sub BOUND_VARIABLE_3044 (tptp.push tptp.one tptp.sh))) tptp.id)))) % 0.40/0.68 (define-fun tptp.pushprop_lem1v2_gthm () Bool true) % 0.40/0.68 (define-fun tptp.hoaslamnotap_gthm () Bool true) % 0.40/0.68 (define-fun tptp.hoaslamnotvar_gthm () Bool true) % 0.40/0.68 (define-fun tptp.hoasinduction_lem3b_gthm () Bool true) % 0.40/0.68 (define-fun tptp.pushprop_lem2v2 () Bool true) % 0.40/0.68 (define-fun tptp.hoasinduction_lem3a_gthm () Bool true) % 0.40/0.68 (define-fun tptp.axclos () Bool true) % 0.40/0.68 (define-fun tptp.axassoc () Bool true) % 0.40/0.68 (define-fun tptp.hoasinduction_lem2v2 () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool)) (BOUND_VARIABLE_2818 tptp.term) (BOUND_VARIABLE_2820 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (tptp.comp K N))) (P (tptp.comp M K) (tptp.sub A K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (tptp.comp M K) (tptp.sub A K) N)) (P M A (tptp.comp 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 (tptp.sub A tptp.id) B) tptp.id)))) (not (forall ((X tptp.term)) (= (Q X) (P tptp.id X tptp.id)))) (not (Q BOUND_VARIABLE_2818)) (not (Q BOUND_VARIABLE_2820)) (Q (tptp.ap BOUND_VARIABLE_2818 BOUND_VARIABLE_2820))))) % 0.40/0.68 (define-fun tptp.pushprop_lthm () Bool true) % 0.40/0.68 (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)))) % 0.40/0.68 (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)))) % 0.40/0.68 (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 (tptp.sub A tptp.id) C) (tptp.ap (tptp.sub B tptp.id) D))) (= C D))))) % 0.40/0.68 (define-fun tptp.hoasinduction_lem3v2a () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool)) (BOUND_VARIABLE_2929 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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 (tptp.sub BOUND_VARIABLE_2929 (tptp.push B tptp.id)))))) (Q (tptp.lam BOUND_VARIABLE_2929))))) % 0.40/0.68 (define-fun tptp.hoasapinj1_lthm () Bool (=> (forall ((A tptp.term)) (= A (tptp.sub 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 (tptp.sub A tptp.id) C) (tptp.ap (tptp.sub B tptp.id) D))) (= A B)))))) % 0.40/0.68 (define-fun tptp.hoaslaminj_lthm () Bool (=> (forall ((A tptp.term) (M tptp.subst)) (= A (tptp.sub tptp.one (tptp.push A M)))) (=> (forall ((A tptp.term) (M tptp.subst)) (= M (tptp.comp tptp.sh (tptp.push A M)))) (=> (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_2545 (-> tptp.subst tptp.term tptp.term)) (BOUND_VARIABLE_2547 tptp.subst) (BOUND_VARIABLE_2549 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub A N))))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (BOUND_VARIABLE_2545 M A) N) (BOUND_VARIABLE_2545 (tptp.comp M N) (tptp.sub A N))))) (not (= (tptp.lam (F tptp.sh tptp.one)) (tptp.lam (BOUND_VARIABLE_2545 tptp.sh tptp.one)))) (= (F BOUND_VARIABLE_2547 BOUND_VARIABLE_2549) (BOUND_VARIABLE_2545 BOUND_VARIABLE_2547 BOUND_VARIABLE_2549)))))))) % 0.40/0.68 (define-fun tptp.axvarcons () Bool (forall ((A tptp.term) (M tptp.subst)) (= A (tptp.sub tptp.one (tptp.push A M))))) % 0.40/0.68 (define-fun tptp.hoaslam ((BOUND_VARIABLE_4911 tptp.subst) (BOUND_VARIABLE_4913 (-> tptp.subst tptp.term tptp.term))) tptp.term (as @tptp.term_0 tptp.term)) % 0.40/0.68 (define-fun tptp.axscons () Bool (forall ((M tptp.subst)) (= M (tptp.push (tptp.sub tptp.one M) (tptp.comp tptp.sh M))))) % 0.40/0.68 (define-fun tptp.hoasinduction_lem2v2_gthm () Bool true) % 0.40/0.68 (define-fun tptp.axidr () Bool (forall ((M tptp.subst)) (= M (tptp.comp M tptp.id)))) % 0.40/0.68 (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 (tptp.sub A (tptp.push B M)))))) % 0.40/0.68 (define-fun tptp.laminj () Bool (forall ((A tptp.term) (B tptp.term)) (or (not (= (tptp.lam A) (tptp.lam B))) (= A B)))) % 0.40/0.68 (define-fun tptp.hoasinduction_lem3_lthm () Bool (=> (forall ((A tptp.term)) (= A (tptp.sub A tptp.id))) (=> (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3044 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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 (tptp.sub BOUND_VARIABLE_3044 (tptp.push B tptp.id)) tptp.id)))) (P tptp.id (tptp.lam (tptp.sub BOUND_VARIABLE_3044 (tptp.push tptp.one tptp.sh))) tptp.id))) (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3209 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (tptp.comp K N))) (P (tptp.comp M K) (tptp.sub A K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (tptp.comp M K) (tptp.sub A K) N)) (P M A (tptp.comp K N))))) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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 (tptp.sub BOUND_VARIABLE_3209 (tptp.push B tptp.id)) tptp.id)))) (P tptp.id (tptp.lam BOUND_VARIABLE_3209) tptp.id)))))) % 0.40/0.68 (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 (tptp.sub X (tptp.push A M)))))))))) % 0.40/0.68 (define-fun tptp.pushprop_gthm () Bool true) % 0.40/0.68 (define-fun tptp.axabs () Bool true) % 0.40/0.68 (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)) (= (tptp.sub B (tptp.push A M)) (F M A))))))) (=> (forall ((A tptp.term)) (= A (tptp.sub A tptp.id))) (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool)) (BOUND_VARIABLE_2929 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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 (tptp.sub BOUND_VARIABLE_2929 (tptp.push B tptp.id)))))) (Q (tptp.lam BOUND_VARIABLE_2929))))))) % 0.40/0.68 (define-fun tptp.hoasinduction_lem2_lthm () Bool true) % 0.40/0.68 (define-fun tptp.hoasapinj2_gthm () Bool true) % 0.40/0.68 (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)))) % 0.40/0.68 (define-fun tptp.hoasinduction_lem1_lthm () Bool true) % 0.40/0.68 (define-fun tptp.lamnotap () Bool false) % 0.40/0.68 (define-fun tptp.hoasapinj1_gthm () Bool true) % 0.40/0.68 (define-fun tptp.hoaslamnotvar () Bool true) % 0.40/0.68 (define-fun tptp.axidl () Bool (forall ((M tptp.subst)) (= M (tptp.comp tptp.id M)))) % 0.40/0.68 (define-fun tptp.hoaslaminj_gthm () Bool true) % 0.40/0.68 (define-fun tptp.induction2_lthm () Bool (=> (forall ((A tptp.term)) (= A (tptp.sub A tptp.id))) (=> (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2338 tptp.term) (BOUND_VARIABLE_2340 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 (tptp.sub A (tptp.push B tptp.id)))))) (P (tptp.lam A))))) (not (forall ((B tptp.term)) (or (not (tptp.var B)) (P (tptp.sub B BOUND_VARIABLE_2340))))) (P (tptp.sub BOUND_VARIABLE_2338 BOUND_VARIABLE_2340)))) (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2365 tptp.term)) (or (not (forall ((A tptp.term)) (or (not (tptp.var 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 (tptp.sub A (tptp.push B tptp.id)))))) (P (tptp.lam A))))) (P BOUND_VARIABLE_2365)))))) % 0.40/0.68 (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)))))))) % 0.40/0.68 (define-fun tptp.substmonoid_lthm () Bool (=> (forall ((M tptp.subst)) (= M (tptp.comp tptp.id M))) (=> (forall ((M tptp.subst)) (= M (tptp.comp M tptp.id))) (and (forall ((M tptp.subst)) (= M (tptp.comp tptp.id M))) (forall ((M tptp.subst)) (= M (tptp.comp M tptp.id))))))) % 0.40/0.68 (define-fun tptp.pushprop () Bool true) % 0.40/0.68 (define-fun tptp.hoasinduction_lem3_gthm () Bool true) % 0.40/0.68 (define-fun tptp.hoasinduction_lem2_gthm () Bool true) % 0.40/0.68 (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) (tptp.sub B (tptp.push tptp.one tptp.sh)))))))) % 0.40/0.68 (define-fun tptp.substmonoid () Bool (and (forall ((M tptp.subst)) (= M (tptp.comp tptp.id M))) (forall ((M tptp.subst)) (= M (tptp.comp M tptp.id))))) % 0.40/0.68 (define-fun tptp.lamnotvar () Bool true) % 0.40/0.68 (define-fun tptp.hoasinduction_lem3a () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3230 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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 (tptp.sub BOUND_VARIABLE_3230 (tptp.push B tptp.id)) tptp.id)))) (P tptp.id (tptp.lam BOUND_VARIABLE_3230) tptp.id)))) % 0.40/0.68 (define-fun tptp.hoasinduction_lem1_gthm () Bool true) % 0.40/0.68 (define-fun tptp.hoasinduction_no_psi_cond () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3293 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 (tptp.sub 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)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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_3293 tptp.id)))) % 0.40/0.68 (define-fun tptp.induction2_gthm () Bool true) % 0.40/0.68 (define-fun tptp.pushprop_lem2v2_lthm () Bool true) % 0.40/0.68 (define-fun tptp.hoasvar ((BOUND_VARIABLE_5002 tptp.subst) (BOUND_VARIABLE_5004 tptp.term) (BOUND_VARIABLE_5006 tptp.subst)) Bool false) % 0.40/0.68 (define-fun tptp.hoaslamnotap () Bool (forall ((F (-> tptp.subst tptp.term tptp.term)) (BOUND_VARIABLE_2601 tptp.term) (BOUND_VARIABLE_2603 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub A N))))) (not (= (tptp.lam (F tptp.sh tptp.one)) (tptp.ap (tptp.sub BOUND_VARIABLE_2601 tptp.id) BOUND_VARIABLE_2603)))))) % 0.40/0.68 (define-fun tptp.substmonoid_gthm () Bool true) % 0.40/0.68 (define-fun tptp.ulamvarsh () Bool true) % 0.40/0.68 (define-fun tptp.induction2 () Bool (forall ((P (-> tptp.term Bool)) (BOUND_VARIABLE_2365 tptp.term)) (or (not (forall ((A tptp.term)) (or (not (tptp.var 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 (tptp.sub A (tptp.push B tptp.id)))))) (P (tptp.lam A))))) (P BOUND_VARIABLE_2365)))) % 0.40/0.68 (define-fun tptp.pushprop_lem3v2 () Bool true) % 0.40/0.68 (define-fun tptp.pushprop_lem2v2_gthm () Bool true) % 0.40/0.68 (define-fun tptp.pushprop_lem1_lthm () Bool (=> (forall ((A tptp.term) (M tptp.subst)) (= A (tptp.sub tptp.one (tptp.push A M)))) (=> (forall ((A tptp.term) (M tptp.subst)) (= M (tptp.comp tptp.sh (tptp.push A M)))) (forall ((P (-> tptp.term Bool)) (K (-> tptp.term Bool)) (A tptp.term) (M tptp.subst) (B tptp.term)) (or (not (P A)) (K (tptp.sub A (tptp.push B M)))))))) % 0.40/0.68 (define-fun tptp.hoasinduction_lem3v2 () Bool (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool)) (BOUND_VARIABLE_2908 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (tptp.comp K N))) (P (tptp.comp M K) (tptp.sub A K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (tptp.comp M K) (tptp.sub A K) N)) (P M A (tptp.comp K N))))) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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 (tptp.sub BOUND_VARIABLE_2908 (tptp.push B tptp.id)))))) (Q (tptp.lam BOUND_VARIABLE_2908))))) % 0.40/0.68 (define-fun tptp.axshiftcons () Bool (forall ((A tptp.term) (M tptp.subst)) (= M (tptp.comp tptp.sh (tptp.push A M))))) % 0.40/0.68 (define-fun tptp.termmset () Bool (forall ((A tptp.term)) (= A (tptp.sub A tptp.id)))) % 0.40/0.68 (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 (tptp.sub X (tptp.push A M)))))))))) % 0.40/0.68 (define-fun tptp.hoasapnotvar_lthm () Bool true) % 0.40/0.68 (define-fun tptp.hoasinduction_lem3v2_lthm () Bool (=> (forall ((A tptp.term)) (= A (tptp.sub A tptp.id))) (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool)) (BOUND_VARIABLE_2908 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (tptp.comp K N))) (P (tptp.comp M K) (tptp.sub A K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (tptp.comp M K) (tptp.sub A K) N)) (P M A (tptp.comp K N))))) (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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 (tptp.sub BOUND_VARIABLE_2908 (tptp.push B tptp.id)))))) (Q (tptp.lam BOUND_VARIABLE_2908)))))) % 0.40/0.68 (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 (tptp.sub X (tptp.push A M)))))) % 0.40/0.68 (define-fun tptp.axvarid () Bool (forall ((A tptp.term)) (= A (tptp.sub A tptp.id)))) % 0.40/0.68 (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_2365 tptp.term)) (or (not (forall ((A tptp.term)) (or (not (tptp.var 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 (tptp.sub A (tptp.push B tptp.id)))))) (P (tptp.lam A))))) (P BOUND_VARIABLE_2365))) (=> (forall ((A tptp.term)) (= A (tptp.sub A tptp.id))) (=> (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool)) (BOUND_VARIABLE_2929 tptp.term)) (or (not (forall ((F (-> tptp.subst tptp.term tptp.term))) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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 (tptp.sub BOUND_VARIABLE_2929 (tptp.push B tptp.id)))))) (Q (tptp.lam BOUND_VARIABLE_2929)))) (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (BOUND_VARIABLE_3281 tptp.term)) (or (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P M A (tptp.comp K N))) (P (tptp.comp M K) (tptp.sub A K) N)))) (not (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (or (not (P (tptp.comp M K) (tptp.sub A K) N)) (P M A (tptp.comp K N))))) (not (forall ((A tptp.term)) (or (not (tptp.var (tptp.sub 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 (tptp.sub 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)) (= (tptp.sub (F M A) N) (F (tptp.comp M N) (tptp.sub 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_3281 tptp.id)))))))) % 0.40/0.68 ) % 0.40/0.68 % SZS output end Model % 0.40/0.68 % cvc5 exiting %------------------------------------------------------------------------------