%------------------------------------------------------------------------------ % File : Z3---4.15.1 % Problem : COM001_10 : TPTP v9.0.0. Released v8.2.0. % Transfm : none % Format : tptp % Command : run_E %s %d THM % Computer : n015.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:00:54 AM UTC 2025 % Result : Satisfiable 0.23s 0.41s % Output : Model 0.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.14 % Problem : COM001_10 : TPTP v9.0.0. Released v8.2.0. % 0.04/0.14 % Command : run_E %s %d THM % 0.14/0.36 % Computer : n015.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Thu Jun 19 12:20:10 EDT 2025 % 0.14/0.37 % CPUTime : % 0.23/0.41 % SZS status Satisfiable % 0.23/0.41 % SZS output start Model % 0.23/0.41 tff(register_val_0_type, type, ( % 0.23/0.41 register_val_0: register)). % 0.23/0.41 tff(register_j_type, type, ( % 0.23/0.41 register_j: register)). % 0.23/0.41 tff(label_val_1_type, type, ( % 0.23/0.41 label_val_1: label)). % 0.23/0.41 tff(out_type, type, ( % 0.23/0.41 out: label)). % 0.23/0.41 tff(state_val_0_type, type, ( % 0.23/0.41 state_val_0: state)). % 0.23/0.41 tff(p3_type, type, ( % 0.23/0.41 p3: state)). % 0.23/0.41 tff(state_val_2_type, type, ( % 0.23/0.41 state_val_2: state)). % 0.23/0.41 tff(p5_type, type, ( % 0.23/0.41 p5: state)). % 0.23/0.41 tff(state_val_1_type, type, ( % 0.23/0.41 state_val_1: state)). % 0.23/0.41 tff(p4_type, type, ( % 0.23/0.41 p4: state)). % 0.23/0.41 tff(state_val_3_type, type, ( % 0.23/0.41 state_val_3: state)). % 0.23/0.41 tff(p8_type, type, ( % 0.23/0.41 p8: state)). % 0.23/0.41 tff(label_val_0_type, type, ( % 0.23/0.41 label_val_0: label)). % 0.23/0.41 tff(loop_type, type, ( % 0.23/0.41 loop: label)). % 0.23/0.41 tff(number_val_0_type, type, ( % 0.23/0.41 number_val_0: number)). % 0.23/0.41 tff(n_type, type, ( % 0.23/0.41 n: number)). % 0.23/0.41 tff(boolean_val_0_type, type, ( % 0.23/0.41 boolean_val_0: boolean)). % 0.23/0.41 tff(equal_function_type, type, ( % 0.23/0.41 equal_function: ( register * number ) > boolean)). % 0.23/0.41 tff(statement_val_1_type, type, ( % 0.23/0.41 statement_val_1: statement)). % 0.23/0.41 tff(goto_type, type, ( % 0.23/0.41 goto: label > statement)). % 0.23/0.41 tff(statement_val_2_type, type, ( % 0.23/0.41 statement_val_2: statement)). % 0.23/0.41 tff(statement_val_4_type, type, ( % 0.23/0.41 statement_val_4: statement)). % 0.23/0.41 tff(statement_val_0_type, type, ( % 0.23/0.41 statement_val_0: statement)). % 0.23/0.41 tff(ifthen_type, type, ( % 0.23/0.41 ifthen: ( boolean * state ) > statement)). % 0.23/0.41 tff(labels_type, type, ( % 0.23/0.41 labels: ( label * state ) > $o)). % 0.23/0.41 tff(has_type, type, ( % 0.23/0.41 has: ( state * statement ) > $o)). % 0.23/0.41 tff(succeeds_type, type, ( % 0.23/0.41 succeeds: ( state * state ) > $o)). % 0.23/0.41 tff(follows_type, type, ( % 0.23/0.41 follows: ( state * state ) > $o)). % 0.23/0.41 tff(formula1, axiom, % 0.23/0.41 register_j = register!val!0). % 0.23/0.41 tff(formula2, axiom, % 0.23/0.41 out = label!val!1). % 0.23/0.41 tff(formula3, axiom, % 0.23/0.41 p3 = state!val!0). % 0.23/0.41 tff(formula4, axiom, % 0.23/0.41 p5 = state!val!2). % 0.23/0.41 tff(formula5, axiom, % 0.23/0.41 p4 = state!val!1). % 0.23/0.41 tff(formula6, axiom, % 0.23/0.41 p8 = state!val!3). % 0.23/0.41 tff(formula7, axiom, % 0.23/0.41 loop = label!val!0). % 0.23/0.41 tff(formula8, axiom, % 0.23/0.41 n = number!val!0). % 0.23/0.41 tff(formula9, axiom, % 0.23/0.41 ![X0: register, X1: number] : (equal_function(X0, X1) = boolean!val!0)). % 0.23/0.41 tff(formula10, axiom, % 0.23/0.41 goto(label!val!1) = statement!val!1). % 0.23/0.41 tff(formula11, axiom, % 0.23/0.41 ![X0: label] : ((~((label!val!1 = X0))) => (goto(X0) = statement!val!2))). % 0.23/0.41 tff(formula12, axiom, % 0.23/0.41 ![X0: boolean, X1: state] : (ifthen(X0, X1) = ite_t((X0 = state!val!1), statement!val!0, statement!val!4))). % 0.23/0.41 tff(formula13, axiom, % 0.23/0.41 ![X0: label, X1: state] : (labels(X0, X1) <=> $true)). % 0.23/0.41 tff(formula14, axiom, % 0.23/0.41 ![X0: state, X1: statement] : (has(X0, X1) <=> $true)). % 0.23/0.41 tff(formula15, axiom, % 0.23/0.41 ![X0: state, X1: state] : (succeeds(X0, X1) <=> $true)). % 0.23/0.41 tff(formula16, axiom, % 0.23/0.41 ![X0: state, X1: state] : (follows(X0, X1) <=> $true)). % 0.23/0.41 % SZS output end Model % 0.23/0.41 % E exiting %------------------------------------------------------------------------------