%------------------------------------------------------------------------------ % File : Z3---4.15.1 % Problem : COM003_10 : TPTP v9.0.0. Released v8.2.0. % Transfm : none % Format : tptp % Command : run_E %s %d THM % Computer : n011.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:55 AM UTC 2025 % Result : Satisfiable 0.19s 0.39s % Output : Model 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : COM003_10 : TPTP v9.0.0. Released v8.2.0. % 0.12/0.12 % Command : run_E %s %d THM % 0.12/0.34 % Computer : n011.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Jun 19 12:20:11 EDT 2025 % 0.19/0.34 % CPUTime : % 0.19/0.39 % SZS status Satisfiable % 0.19/0.39 % SZS output start Model % 0.19/0.39 tff(output_val_0_type, type, ( % 0.19/0.39 output_val_0: output)). % 0.19/0.39 tff(bad_type, type, ( % 0.19/0.39 bad: output)). % 0.19/0.39 tff(good_type, type, ( % 0.19/0.39 good: output)). % 0.19/0.39 tff(input_val_1_type, type, ( % 0.19/0.39 input_val_1: input)). % 0.19/0.39 tff(as_input_type, type, ( % 0.19/0.39 as_input: program > input)). % 0.19/0.39 tff(program_val_2_type, type, ( % 0.19/0.39 program_val_2: program)). % 0.19/0.39 tff(input_val_0_type, type, ( % 0.19/0.39 input_val_0: input)). % 0.19/0.39 tff(program_val_3_type, type, ( % 0.19/0.39 program_val_3: program)). % 0.19/0.39 tff(program_val_1_type, type, ( % 0.19/0.39 program_val_1: program)). % 0.19/0.39 tff(halts2_type, type, ( % 0.19/0.39 halts2: ( program * input ) > $o)). % 0.19/0.39 tff(algorithm_val_4_type, type, ( % 0.19/0.39 algorithm_val_4: algorithm)). % 0.19/0.39 tff(algorithm_of_type, type, ( % 0.19/0.39 algorithm_of: program > algorithm)). % 0.19/0.39 tff(algorithm_val_0_type, type, ( % 0.19/0.39 algorithm_val_0: algorithm)). % 0.19/0.39 tff(algorithm_val_2_type, type, ( % 0.19/0.39 algorithm_val_2: algorithm)). % 0.19/0.39 tff(algorithm_val_3_type, type, ( % 0.19/0.39 algorithm_val_3: algorithm)). % 0.19/0.39 tff(halts3_type, type, ( % 0.19/0.39 halts3: ( program * program * input ) > $o)). % 0.19/0.39 tff(outputs_type, type, ( % 0.19/0.39 outputs: ( program * output ) > $o)). % 0.19/0.39 tff(decides_type, type, ( % 0.19/0.39 decides: ( algorithm * program * input ) > $o)). % 0.19/0.39 tff(formula1, axiom, % 0.19/0.39 bad = output!val!0). % 0.19/0.39 tff(formula2, axiom, % 0.19/0.39 good = output!val!0). % 0.19/0.39 tff(formula3, axiom, % 0.19/0.39 as_input(program!val!2) = input!val!1). % 0.19/0.39 tff(formula4, axiom, % 0.19/0.39 ![X0: program] : ((~((program!val!2 = X0))) => (as_input(X0) = input!val!0))). % 0.19/0.39 tff(formula5, axiom, % 0.19/0.39 ![X0: program, X1: input] : (halts2(X0, X1) <=> ((X1 = program!val!1) & (~(X1 = program!val!3)) & (~(X1 = program!val!2)) & (X0 = input!val!0)))). % 0.19/0.39 tff(formula6, axiom, % 0.19/0.39 algorithm_of(program!val!2) = algorithm!val!4). % 0.19/0.39 tff(formula7, axiom, % 0.19/0.39 ![X0: program] : ((~((program!val!2 = X0))) => (algorithm_of(X0) = ite_t(((X0 = program!val!1) & (~(X0 = program!val!3)) & (~(X0 = program!val!2))), algorithm!val!3, ite_t(((~(X0 = program!val!1)) & (~(X0 = program!val!3)) & (~(X0 = program!val!2))), algorithm!val!2, algorithm!val!0))))). % 0.19/0.39 tff(formula8, axiom, % 0.19/0.39 ![X0: program, X1: program, X2: input] : (halts3(X0, X1, X2) <=> $false)). % 0.19/0.39 tff(formula9, axiom, % 0.19/0.39 ![X0: program, X1: output] : (outputs(X0, X1) <=> $false)). % 0.19/0.39 tff(formula10, axiom, % 0.19/0.39 ![X0: algorithm, X1: program, X2: input] : (decides(X0, X1, X2) <=> $false)). % 0.19/0.39 % SZS output end Model % 0.19/0.40 % E exiting %------------------------------------------------------------------------------