% COMMAND-LINE: --uf-ho --uf-ho --finite-model-find % EXPECT: % SZS status CounterSatisfiable for fta0328.lfho % TIMEFORMAT='%3R'; { time (exec 2>&1; /Users/blanchette/.isabelle/contrib/e-2.0-2/x86_64-darwin/eprover --auto-schedule --tstp-in --tstp-out --silent --cpu-limit=2 --proof-object=1 /Users/blanchette/hgs/matryoshka/papers/2019-TACAS-ehoh/eval/judgment_day/judgment_day_lifting_32/fta/prob_804__4064966_1 ) ; } % This file was generated by Isabelle (most likely Sledgehammer) % 2018-05-22 19:17:55.732 % Could-be-implicit typings (8) thf(ty_n_t__Polynomial__Opoly_It__Polynomial__Opoly_It__Polynomial__Opoly_It__Complex__Ocomplex_J_J_J, type, poly_p1267267526omplex : $tType). thf(ty_n_t__Polynomial__Opoly_It__Polynomial__Opoly_It__Complex__Ocomplex_J_J, type, poly_poly_complex : $tType). thf(ty_n_t__Polynomial__Opoly_It__Complex__Ocomplex_J, type, poly_complex : $tType). thf(ty_n_t__Polynomial__Opoly_It__Nat__Onat_J, type, poly_nat : $tType). thf(ty_n_t__Complex__Ocomplex, type, complex : $tType). thf(ty_n_t__Real__Oreal, type, real : $tType). thf(ty_n_t__HOL__Obool, type, bool : $tType). thf(ty_n_t__Nat__Onat, type, nat : $tType). % Explicit typings (28) thf(sy_c_Fundamental__Theorem__Algebra__Mirabelle__bptywjkimr_Oconstant_001t__Complex__Ocomplex_001t__Complex__Ocomplex, type, fundam769667258omplex : (complex > complex) > $o). thf(sy_c_Fundamental__Theorem__Algebra__Mirabelle__bptywjkimr_Opsize_001t__Complex__Ocomplex, type, fundam835161864omplex : poly_complex > nat). thf(sy_c_Groups_Oplus__class_Oplus_001t__Complex__Ocomplex, type, plus_plus_complex : complex > complex > complex). thf(sy_c_Groups_Oplus__class_Oplus_001t__Nat__Onat, type, plus_plus_nat : nat > nat > nat). thf(sy_c_Groups_Oplus__class_Oplus_001t__Polynomial__Opoly_It__Complex__Ocomplex_J, type, plus_p1547158847omplex : poly_complex > poly_complex > poly_complex). thf(sy_c_Groups_Oplus__class_Oplus_001t__Polynomial__Opoly_It__Polynomial__Opoly_It__Complex__Ocomplex_J_J, type, plus_p138939463omplex : poly_poly_complex > poly_poly_complex > poly_poly_complex). thf(sy_c_Groups_Ozero__class_Ozero_001t__Complex__Ocomplex, type, zero_zero_complex : complex). thf(sy_c_Groups_Ozero__class_Ozero_001t__Nat__Onat, type, zero_zero_nat : nat). thf(sy_c_Groups_Ozero__class_Ozero_001t__Polynomial__Opoly_It__Complex__Ocomplex_J, type, zero_z1746442943omplex : poly_complex). thf(sy_c_Groups_Ozero__class_Ozero_001t__Polynomial__Opoly_It__Nat__Onat_J, type, zero_zero_poly_nat : poly_nat). thf(sy_c_Groups_Ozero__class_Ozero_001t__Polynomial__Opoly_It__Polynomial__Opoly_It__Complex__Ocomplex_J_J, type, zero_z1040703943omplex : poly_poly_complex). thf(sy_c_Groups_Ozero__class_Ozero_001t__Polynomial__Opoly_It__Polynomial__Opoly_It__Polynomial__Opoly_It__Complex__Ocomplex_J_J_J, type, zero_z1200043727omplex : poly_p1267267526omplex). thf(sy_c_Orderings_Oord__class_Oless_001t__Nat__Onat, type, ord_less_nat : nat > nat > $o). thf(sy_c_Orderings_Oord__class_Oless__eq_001t__Nat__Onat, type, ord_less_eq_nat : nat > nat > $o). thf(sy_c_Orderings_Oord__class_Oless__eq_001t__Real__Oreal, type, ord_less_eq_real : real > real > $o). thf(sy_c_Polynomial_Opoly_001t__Complex__Ocomplex, type, poly_complex2 : poly_complex > complex > complex). thf(sy_c_Polynomial_Opoly_001t__Nat__Onat, type, poly_nat2 : poly_nat > nat > nat). thf(sy_c_Polynomial_Opoly_001t__Polynomial__Opoly_It__Complex__Ocomplex_J, type, poly_poly_complex2 : poly_poly_complex > poly_complex > poly_complex). thf(sy_c_Polynomial_Opoly_001t__Polynomial__Opoly_It__Polynomial__Opoly_It__Complex__Ocomplex_J_J, type, poly_p282434315omplex : poly_p1267267526omplex > poly_poly_complex > poly_poly_complex). thf(sy_c_Real__Vector__Spaces_Onorm__class_Onorm_001t__Complex__Ocomplex, type, real_V638595069omplex : complex > real). thf(sy_c_fFalse, type, fFalse : bool). thf(sy_c_fTrue, type, fTrue : bool). thf(sy_c_pp, type, pp : bool > $o). thf(sy_v_a____, type, a : complex). thf(sy_v_c____, type, c : complex). thf(sy_v_p, type, p : poly_complex). thf(sy_v_pa____, type, pa : poly_complex). thf(sy_v_q____, type, q : poly_complex). % Relevant facts (53) thf(fact_0_kas_I1_J, axiom, ((~ ((a = zero_zero_complex))))). % kas(1) thf(fact_1_q_I2_J, axiom, ((![X : complex]: ((poly_complex2 @ q @ X) = (poly_complex2 @ pa @ (plus_plus_complex @ c @ X)))))). % q(2) thf(fact_2_nc, axiom, ((~ ((fundam769667258omplex @ (poly_complex2 @ p)))))). % nc thf(fact_3_False, axiom, ((~ (((poly_complex2 @ pa @ c) = zero_zero_complex))))). % False thf(fact_4_less_Oprems, axiom, ((~ ((fundam769667258omplex @ (poly_complex2 @ pa)))))). % less.prems thf(fact_5_a00, axiom, ((~ (((poly_complex2 @ q @ zero_zero_complex) = zero_zero_complex))))). % a00 thf(fact_6_pqc0, axiom, (((poly_complex2 @ pa @ c) = (poly_complex2 @ q @ zero_zero_complex)))). % pqc0 thf(fact_7_q_I1_J, axiom, (((fundam835161864omplex @ q) = (fundam835161864omplex @ pa)))). % q(1) thf(fact_8_poly__0, axiom, ((![X2 : poly_poly_complex]: ((poly_p282434315omplex @ zero_z1200043727omplex @ X2) = zero_z1040703943omplex)))). % poly_0 thf(fact_9_poly__0, axiom, ((![X2 : nat]: ((poly_nat2 @ zero_zero_poly_nat @ X2) = zero_zero_nat)))). % poly_0 thf(fact_10_poly__0, axiom, ((![X2 : poly_complex]: ((poly_poly_complex2 @ zero_z1040703943omplex @ X2) = zero_z1746442943omplex)))). % poly_0 thf(fact_11_poly__0, axiom, ((![X2 : complex]: ((poly_complex2 @ zero_z1746442943omplex @ X2) = zero_zero_complex)))). % poly_0 thf(fact_12_poly__all__0__iff__0, axiom, ((![P : poly_p1267267526omplex]: ((![X3 : poly_poly_complex]: ((poly_p282434315omplex @ P @ X3) = zero_z1040703943omplex)) <=> (P = zero_z1200043727omplex))))). % poly_all_0_iff_0 thf(fact_13_poly__all__0__iff__0, axiom, ((![P : poly_complex]: ((![X3 : complex]: ((poly_complex2 @ P @ X3) = zero_zero_complex)) <=> (P = zero_z1746442943omplex))))). % poly_all_0_iff_0 thf(fact_14_poly__all__0__iff__0, axiom, ((![P : poly_poly_complex]: ((![X3 : poly_complex]: ((poly_poly_complex2 @ P @ X3) = zero_z1746442943omplex)) <=> (P = zero_z1040703943omplex))))). % poly_all_0_iff_0 thf(fact_15__092_060open_062_092_060exists_062q_O_Apsize_Aq_A_061_Apsize_Ap_A_092_060and_062_A_I_092_060forall_062x_O_Apoly_Aq_Ax_A_061_Apoly_Ap_A_Ic_A_L_Ax_J_J_092_060close_062, axiom, ((?[Q : poly_complex]: (((fundam835161864omplex @ Q) = (fundam835161864omplex @ pa)) & (![X : complex]: ((poly_complex2 @ Q @ X) = (poly_complex2 @ pa @ (plus_plus_complex @ c @ X)))))))). % \\q. psize q = psize p \ (\x. poly q x = poly p (c + x))\ thf(fact_16__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062q_O_A_092_060lbrakk_062psize_Aq_A_061_Apsize_Ap_059_A_092_060forall_062x_O_Apoly_Aq_Ax_A_061_Apoly_Ap_A_Ic_A_L_Ax_J_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062, axiom, ((~ ((![Q : poly_complex]: (((fundam835161864omplex @ Q) = (fundam835161864omplex @ pa)) => (~ ((![X : complex]: ((poly_complex2 @ Q @ X) = (poly_complex2 @ pa @ (plus_plus_complex @ c @ X)))))))))))). % \\thesis. (\q. \psize q = psize p; \x. poly q x = poly p (c + x)\ \ thesis) \ thesis\ thf(fact_17__092_060open_062constant_A_Ipoly_Aq_J_A_092_060Longrightarrow_062_AFalse_092_060close_062, axiom, ((~ ((fundam769667258omplex @ (poly_complex2 @ q)))))). % \constant (poly q) \ False\ thf(fact_18_qnc, axiom, ((~ ((fundam769667258omplex @ (poly_complex2 @ q)))))). % qnc thf(fact_19_poly__eq__poly__eq__iff, axiom, ((![P : poly_poly_complex, Q2 : poly_poly_complex]: (((poly_poly_complex2 @ P) = (poly_poly_complex2 @ Q2)) <=> (P = Q2))))). % poly_eq_poly_eq_iff thf(fact_20_poly__eq__poly__eq__iff, axiom, ((![P : poly_complex, Q2 : poly_complex]: (((poly_complex2 @ P) = (poly_complex2 @ Q2)) <=> (P = Q2))))). % poly_eq_poly_eq_iff thf(fact_21_c, axiom, ((![W : complex]: (ord_less_eq_real @ (real_V638595069omplex @ (poly_complex2 @ pa @ c)) @ (real_V638595069omplex @ (poly_complex2 @ pa @ W)))))). % c thf(fact_22_zero__reorient, axiom, ((![X2 : poly_poly_complex]: ((zero_z1040703943omplex = X2) <=> (X2 = zero_z1040703943omplex))))). % zero_reorient thf(fact_23_zero__reorient, axiom, ((![X2 : nat]: ((zero_zero_nat = X2) <=> (X2 = zero_zero_nat))))). % zero_reorient thf(fact_24_zero__reorient, axiom, ((![X2 : complex]: ((zero_zero_complex = X2) <=> (X2 = zero_zero_complex))))). % zero_reorient thf(fact_25_zero__reorient, axiom, ((![X2 : poly_complex]: ((zero_z1746442943omplex = X2) <=> (X2 = zero_z1746442943omplex))))). % zero_reorient thf(fact_26_cq0, axiom, ((![W : complex]: (ord_less_eq_real @ (real_V638595069omplex @ (poly_complex2 @ q @ zero_zero_complex)) @ (real_V638595069omplex @ (poly_complex2 @ pa @ W)))))). % cq0 thf(fact_27_less_Ohyps, axiom, ((![P : poly_complex]: ((ord_less_nat @ (fundam835161864omplex @ P) @ (fundam835161864omplex @ pa)) => ((~ ((fundam769667258omplex @ (poly_complex2 @ P)))) => (?[Z : complex]: ((poly_complex2 @ P @ Z) = zero_zero_complex))))))). % less.hyps thf(fact_28_add__left__cancel, axiom, ((![A : poly_complex, B : poly_complex, C : poly_complex]: (((plus_p1547158847omplex @ A @ B) = (plus_p1547158847omplex @ A @ C)) <=> (B = C))))). % add_left_cancel thf(fact_29_add__left__cancel, axiom, ((![A : complex, B : complex, C : complex]: (((plus_plus_complex @ A @ B) = (plus_plus_complex @ A @ C)) <=> (B = C))))). % add_left_cancel thf(fact_30_add__right__cancel, axiom, ((![B : poly_complex, A : poly_complex, C : poly_complex]: (((plus_p1547158847omplex @ B @ A) = (plus_p1547158847omplex @ C @ A)) <=> (B = C))))). % add_right_cancel thf(fact_31_add__right__cancel, axiom, ((![B : complex, A : complex, C : complex]: (((plus_plus_complex @ B @ A) = (plus_plus_complex @ C @ A)) <=> (B = C))))). % add_right_cancel thf(fact_32__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062c_O_A_092_060forall_062w_O_Acmod_A_Ipoly_Ap_Ac_J_A_092_060le_062_Acmod_A_Ipoly_Ap_Aw_J_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062, axiom, ((~ ((![C2 : complex]: (~ ((![W : complex]: (ord_less_eq_real @ (real_V638595069omplex @ (poly_complex2 @ pa @ C2)) @ (real_V638595069omplex @ (poly_complex2 @ pa @ W))))))))))). % \\thesis. (\c. \w. cmod (poly p c) \ cmod (poly p w) \ thesis) \ thesis\ thf(fact_33_le__zero__eq, axiom, ((![N : nat]: ((ord_less_eq_nat @ N @ zero_zero_nat) <=> (N = zero_zero_nat))))). % le_zero_eq thf(fact_34_not__gr__zero, axiom, ((![N : nat]: ((~ ((ord_less_nat @ zero_zero_nat @ N))) <=> (N = zero_zero_nat))))). % not_gr_zero thf(fact_35_zero__eq__add__iff__both__eq__0, axiom, ((![X2 : nat, Y : nat]: ((zero_zero_nat = (plus_plus_nat @ X2 @ Y)) <=> ((X2 = zero_zero_nat) & (Y = zero_zero_nat)))))). % zero_eq_add_iff_both_eq_0 thf(fact_36_add__eq__0__iff__both__eq__0, axiom, ((![X2 : nat, Y : nat]: (((plus_plus_nat @ X2 @ Y) = zero_zero_nat) <=> ((X2 = zero_zero_nat) & (Y = zero_zero_nat)))))). % add_eq_0_iff_both_eq_0 thf(fact_37_add__cancel__right__right, axiom, ((![A : poly_poly_complex, B : poly_poly_complex]: ((A = (plus_p138939463omplex @ A @ B)) <=> (B = zero_z1040703943omplex))))). % add_cancel_right_right thf(fact_38_add__cancel__right__right, axiom, ((![A : nat, B : nat]: ((A = (plus_plus_nat @ A @ B)) <=> (B = zero_zero_nat))))). % add_cancel_right_right thf(fact_39_add__cancel__right__right, axiom, ((![A : complex, B : complex]: ((A = (plus_plus_complex @ A @ B)) <=> (B = zero_zero_complex))))). % add_cancel_right_right thf(fact_40_add__cancel__right__right, axiom, ((![A : poly_complex, B : poly_complex]: ((A = (plus_p1547158847omplex @ A @ B)) <=> (B = zero_z1746442943omplex))))). % add_cancel_right_right thf(fact_41_add__cancel__right__left, axiom, ((![A : poly_poly_complex, B : poly_poly_complex]: ((A = (plus_p138939463omplex @ B @ A)) <=> (B = zero_z1040703943omplex))))). % add_cancel_right_left thf(fact_42_add__cancel__right__left, axiom, ((![A : nat, B : nat]: ((A = (plus_plus_nat @ B @ A)) <=> (B = zero_zero_nat))))). % add_cancel_right_left thf(fact_43_add__cancel__right__left, axiom, ((![A : complex, B : complex]: ((A = (plus_plus_complex @ B @ A)) <=> (B = zero_zero_complex))))). % add_cancel_right_left thf(fact_44_add__cancel__right__left, axiom, ((![A : poly_complex, B : poly_complex]: ((A = (plus_p1547158847omplex @ B @ A)) <=> (B = zero_z1746442943omplex))))). % add_cancel_right_left thf(fact_45_add__cancel__left__right, axiom, ((![A : poly_poly_complex, B : poly_poly_complex]: (((plus_p138939463omplex @ A @ B) = A) <=> (B = zero_z1040703943omplex))))). % add_cancel_left_right thf(fact_46_add__cancel__left__right, axiom, ((![A : nat, B : nat]: (((plus_plus_nat @ A @ B) = A) <=> (B = zero_zero_nat))))). % add_cancel_left_right thf(fact_47_add__cancel__left__right, axiom, ((![A : complex, B : complex]: (((plus_plus_complex @ A @ B) = A) <=> (B = zero_zero_complex))))). % add_cancel_left_right thf(fact_48_add__cancel__left__right, axiom, ((![A : poly_complex, B : poly_complex]: (((plus_p1547158847omplex @ A @ B) = A) <=> (B = zero_z1746442943omplex))))). % add_cancel_left_right thf(fact_49_add__cancel__left__left, axiom, ((![B : poly_poly_complex, A : poly_poly_complex]: (((plus_p138939463omplex @ B @ A) = A) <=> (B = zero_z1040703943omplex))))). % add_cancel_left_left thf(fact_50_add__cancel__left__left, axiom, ((![B : nat, A : nat]: (((plus_plus_nat @ B @ A) = A) <=> (B = zero_zero_nat))))). % add_cancel_left_left thf(fact_51_add__cancel__left__left, axiom, ((![B : complex, A : complex]: (((plus_plus_complex @ B @ A) = A) <=> (B = zero_zero_complex))))). % add_cancel_left_left thf(fact_52_add__cancel__left__left, axiom, ((![B : poly_complex, A : poly_complex]: (((plus_p1547158847omplex @ B @ A) = A) <=> (B = zero_z1746442943omplex))))). % add_cancel_left_left % Helper facts (2) thf(help_pp_2_1_U, axiom, ((pp @ fTrue))). thf(help_pp_1_1_U, axiom, ((~ ((pp @ fFalse))))). % Conjectures (1) thf(conj_0, conjecture, ((?[Z2 : complex]: ((poly_complex2 @ pa @ Z2) = zero_zero_complex)))).