%------------------------------------------------------------------------------ % File : Z3---4.15.1 % Problem : NUM923_10 : TPTP v9.0.0. Released v8.2.0. % Transfm : none % Format : tptp % Command : run_E %s %d THM % Computer : n005.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 : Sat Jun 21 05:22:19 AM UTC 2025 % Result : Satisfiable 0.19s 0.41s % Output : Model 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM923_10 : TPTP v9.0.0. Released v8.2.0. % 0.03/0.12 % Command : run_E %s %d THM % 0.11/0.34 % Computer : n005.cluster.edu % 0.11/0.34 % Model : x86_64 x86_64 % 0.11/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.34 % Memory : 8042.1875MB % 0.11/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.34 % CPULimit : 300 % 0.11/0.34 % WCLimit : 300 % 0.11/0.34 % DateTime : Fri Jun 20 02:03:20 EDT 2025 % 0.11/0.34 % CPUTime : % 0.19/0.41 % SZS status Satisfiable % 0.19/0.41 % SZS output start Model % 0.19/0.41 tff(bool_val_1_type, type, ( % 0.19/0.41 bool_val_1: bool)). % 0.19/0.41 tff(hAPP_P603027463t_bool_type, type, ( % 0.19/0.41 hAPP_P603027463t_bool: ( fun_Pr974702441t_bool * product_prod_int_int ) > bool)). % 0.19/0.41 tff(bool_val_2_type, type, ( % 0.19/0.41 bool_val_2: bool)). % 0.19/0.41 tff(produc262399358t_bool_type, type, ( % 0.19/0.41 produc262399358t_bool: ( fun_Pr974702441t_bool * int * int ) > bool)). % 0.19/0.41 tff(product_prod_int_int_val_0_type, type, ( % 0.19/0.41 product_prod_int_int_val_0: product_prod_int_int)). % 0.19/0.41 tff(product_Pair_int_int_type, type, ( % 0.19/0.41 product_Pair_int_int: ( int * int ) > product_prod_int_int)). % 0.19/0.41 tff(int_val_0_type, type, ( % 0.19/0.41 int_val_0: int)). % 0.19/0.41 tff(twoSqu1319573848sum2sq_type, type, ( % 0.19/0.41 twoSqu1319573848sum2sq: product_prod_int_int > int)). % 0.19/0.41 tff(plus_plus_int_type, type, ( % 0.19/0.41 plus_plus_int: ( int * int ) > int)). % 0.19/0.41 tff(hBOOL_type, type, ( % 0.19/0.41 hBOOL: bool > $o)). % 0.19/0.41 tff(minus_minus_int_type, type, ( % 0.19/0.41 minus_minus_int: ( int * int ) > int)). % 0.19/0.41 tff(times_times_int_type, type, ( % 0.19/0.41 times_times_int: ( int * int ) > int)). % 0.19/0.41 tff(bool_val_0_type, type, ( % 0.19/0.41 bool_val_0: bool)). % 0.19/0.41 tff(ord_less_eq_int_type, type, ( % 0.19/0.41 ord_less_eq_int: ( int * int ) > bool)). % 0.19/0.41 tff(bool_val_3_type, type, ( % 0.19/0.41 bool_val_3: bool)). % 0.19/0.41 tff(twoSqu1431725154sum2sq_type, type, ( % 0.19/0.41 twoSqu1431725154sum2sq: int > bool)). % 0.19/0.41 tff(formula1, axiom, % 0.19/0.41 ![X0: fun_Pr974702441t_bool, X1: product_prod_int_int] : (hAPP_P603027463t_bool(X0, X1) = bool!val!1)). % 0.19/0.41 tff(formula2, axiom, % 0.19/0.41 ![X0: fun_Pr974702441t_bool, X1: int, X2: int] : (produc262399358t_bool(X0, X1, X2) = bool!val!2)). % 0.19/0.41 tff(formula3, axiom, % 0.19/0.41 ![X0: int, X1: int] : (product_Pair_int_int(X0, X1) = product_prod_int_int!val!0)). % 0.19/0.41 tff(formula4, axiom, % 0.19/0.41 ![X0: product_prod_int_int] : (twoSqu1319573848sum2sq(X0) = int!val!0)). % 0.19/0.41 tff(formula5, axiom, % 0.19/0.41 ![X0: int, X1: int] : (plus_plus_int(X0, X1) = int!val!0)). % 0.19/0.41 tff(formula6, axiom, % 0.19/0.41 ![X0: bool] : (hBOOL(X0) <=> $true)). % 0.19/0.41 tff(formula7, axiom, % 0.19/0.41 ![X0: int, X1: int] : (minus_minus_int(X0, X1) = int!val!0)). % 0.19/0.41 tff(formula8, axiom, % 0.19/0.41 ![X0: int, X1: int] : (times_times_int(X0, X1) = int!val!0)). % 0.19/0.41 tff(formula9, axiom, % 0.19/0.41 ![X0: int, X1: int] : (ord_less_eq_int(X0, X1) = bool!val!0)). % 0.19/0.41 tff(formula10, axiom, % 0.19/0.41 ![X0: int] : (twoSqu1431725154sum2sq(X0) = bool!val!3)). % 0.19/0.41 % SZS output end Model % 0.19/0.41 % E exiting %------------------------------------------------------------------------------