%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : COM001_10 : TPTP v9.0.0. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n003.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 Apr 9 05:50:29 PM UTC 2025 % Result : Satisfiable 5.10s 2.37s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : COM001_10 : TPTP v9.0.0. Released v8.2.0. % 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n003.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Mon Apr 7 16:09:33 EDT 2025 % 0.13/0.34 % CPUTime : % 5.10/2.37 % 5.10/2.37 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.10/2.37 % 5.10/2.37 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.49/2.38 %$ succeeds > labels > has > follows > ifthen > equal_function > #nlpp > goto > register_j > p8 > p5 > p4 > p3 > out > n > loop % 5.49/2.38 % 5.49/2.38 %Foreground sorts: % 5.49/2.38 tff(label, type, label: $tType ). % 5.49/2.38 tff(state, type, state: $tType ). % 5.49/2.38 tff(statement, type, statement: $tType ). % 5.49/2.38 tff(boolean, type, boolean: $tType ). % 5.49/2.38 tff(register, type, register: $tType ). % 5.49/2.38 tff(number, type, number: $tType ). % 5.49/2.38 % 5.49/2.38 %Background operators: % 5.49/2.38 % 5.49/2.38 % 5.49/2.38 %Foreground operators: % 5.49/2.38 tff(out, type, out: label). % 5.49/2.38 tff(goto, type, goto: label > statement). % 5.49/2.38 tff(equal_function, type, equal_function: (register * number) > boolean). % 5.49/2.38 tff(register_j, type, register_j: register). % 5.49/2.38 tff(p8, type, p8: state). % 5.49/2.38 tff(labels, type, labels: (label * state) > $o). % 5.49/2.38 tff(ifthen, type, ifthen: (boolean * state) > statement). % 5.49/2.38 tff(p5, type, p5: state). % 5.49/2.38 tff(has, type, has: (state * statement) > $o). % 5.49/2.38 tff(succeeds, type, succeeds: (state * state) > $o). % 5.49/2.38 tff(n, type, n: number). % 5.49/2.38 tff(loop, type, loop: label). % 5.49/2.38 tff(p3, type, p3: state). % 5.49/2.38 tff(follows, type, follows: (state * state) > $o). % 5.49/2.38 tff(p4, type, p4: state). % 5.49/2.38 % 5.49/2.38 %Saturated clause set: % 5.49/2.38 tff(c_1981, plain, (![Goal_state_2:state, Start_state_149:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_149) | ~follows(p8, Start_state_149) | ~follows(Start_state_1, p4) | ~follows(Goal_state_2, Start_state_1)))). % 5.49/2.38 tff(c_1906, plain, (![Goal_state_2:state, Start_state_140:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_140) | ~follows(p8, Start_state_140) | ~follows(Start_state_1, p3) | ~follows(Goal_state_2, Start_state_1)))). % 5.49/2.38 tff(c_1819, plain, (![Goal_state_2:state, Start_state_137:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_137) | ~follows(p8, Start_state_137) | ~follows(Start_state_1, p5) | ~follows(Goal_state_2, Start_state_1)))). % 5.49/2.38 tff(c_728, plain, (![Goal_state_74:state, Start_state_1:state, Start_state_75:state]: (succeeds(Goal_state_74, Start_state_1) | ~follows(Start_state_75, Start_state_1) | ~follows(p8, Start_state_75) | ~follows(Goal_state_74, p5)))). % 5.49/2.38 tff(c_1578, plain, (![Goal_state_2:state, Start_state_116:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_116) | ~follows(p3, Start_state_116) | ~follows(Start_state_1, p4) | ~follows(Goal_state_2, Start_state_1)))). % 5.49/2.38 tff(c_689, plain, (![Goal_state_68:state, Start_state_1:state, Start_state_69:state]: (succeeds(Goal_state_68, Start_state_1) | ~follows(Start_state_69, Start_state_1) | ~follows(p8, Start_state_69) | ~follows(Goal_state_68, p4)))). % 5.49/2.38 tff(c_864, plain, (![Goal_state_82:state, Start_state_1:state, Start_state_83:state]: (succeeds(Goal_state_82, Start_state_1) | ~follows(Start_state_83, Start_state_1) | ~follows(p8, Start_state_83) | ~follows(Goal_state_82, p3)))). % 5.49/2.38 tff(c_691, plain, (![Goal_state_5:state, Start_state_69:state, Goal_state_68:state]: (succeeds(Goal_state_5, Start_state_69) | ~succeeds(Goal_state_5, Goal_state_68) | ~follows(p8, Start_state_69) | ~follows(Goal_state_68, p4)))). % 5.49/2.38 tff(c_1658, plain, (![Goal_state_2:state, Start_state_122:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_122) | ~follows(p3, Start_state_122) | ~follows(Start_state_1, p8) | ~follows(Goal_state_2, Start_state_1)))). % 5.49/2.39 tff(c_1505, plain, (![Goal_state_2:state, Start_state_113:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_113) | ~follows(p4, Start_state_113) | ~follows(Start_state_1, p5) | ~follows(Goal_state_2, Start_state_1)))). % 5.49/2.39 tff(c_866, plain, (![Goal_state_5:state, Start_state_83:state, Goal_state_82:state]: (succeeds(Goal_state_5, Start_state_83) | ~succeeds(Goal_state_5, Goal_state_82) | ~follows(p8, Start_state_83) | ~follows(Goal_state_82, p3)))). % 5.49/2.39 tff(c_730, plain, (![Goal_state_5:state, Start_state_75:state, Goal_state_74:state]: (succeeds(Goal_state_5, Start_state_75) | ~succeeds(Goal_state_5, Goal_state_74) | ~follows(p8, Start_state_75) | ~follows(Goal_state_74, p5)))). % 5.49/2.39 tff(c_1745, plain, (![Goal_state_2:state, Start_state_131:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_131) | ~follows(p3, Start_state_131) | ~follows(Start_state_1, p5) | ~follows(Goal_state_2, Start_state_1)))). % 5.49/2.39 tff(c_655, plain, (![Goal_state_5:state, Start_state_66:state, Goal_state_65:state]: (succeeds(Goal_state_5, Start_state_66) | ~succeeds(Goal_state_5, Goal_state_65) | ~follows(p3, Start_state_66) | ~follows(Goal_state_65, p5)))). % 5.49/2.39 tff(c_653, plain, (![Goal_state_65:state, Start_state_1:state, Start_state_66:state]: (succeeds(Goal_state_65, Start_state_1) | ~follows(Start_state_66, Start_state_1) | ~follows(p3, Start_state_66) | ~follows(Goal_state_65, p5)))). % 5.49/2.39 tff(c_246, plain, (![Goal_state_47:state, Start_state_1:state, Start_state_48:state]: (succeeds(Goal_state_47, Start_state_1) | ~follows(Start_state_48, Start_state_1) | ~follows(p3, Start_state_48) | ~follows(Goal_state_47, p8)))). % 5.49/2.39 tff(c_248, plain, (![Goal_state_5:state, Start_state_48:state, Goal_state_47:state]: (succeeds(Goal_state_5, Start_state_48) | ~succeeds(Goal_state_5, Goal_state_47) | ~follows(p3, Start_state_48) | ~follows(Goal_state_47, p8)))). % 5.49/2.39 tff(c_226, plain, (![Goal_state_45:state, Start_state_1:state, Start_state_46:state]: (succeeds(Goal_state_45, Start_state_1) | ~follows(Start_state_46, Start_state_1) | ~follows(p4, Start_state_46) | ~follows(Goal_state_45, p5)))). % 5.49/2.39 tff(c_268, plain, (![Goal_state_5:state, Start_state_50:state, Goal_state_49:state]: (succeeds(Goal_state_5, Start_state_50) | ~succeeds(Goal_state_5, Goal_state_49) | ~follows(p3, Start_state_50) | ~follows(Goal_state_49, p4)))). % 5.49/2.39 tff(c_228, plain, (![Goal_state_5:state, Start_state_46:state, Goal_state_45:state]: (succeeds(Goal_state_5, Start_state_46) | ~succeeds(Goal_state_5, Goal_state_45) | ~follows(p4, Start_state_46) | ~follows(Goal_state_45, p5)))). % 5.49/2.39 tff(c_1292, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p8) | ~succeeds(Start_state_1, p4) | ~follows(Goal_state_2, Start_state_1)))). % 5.49/2.39 tff(c_961, plain, (![Goal_state_5:state, Goal_state_86:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, Goal_state_86) | ~follows(Goal_state_86, p3)))). % 5.49/2.39 tff(c_497, plain, (![Goal_state_5:state, Goal_state_58:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, Goal_state_58) | ~succeeds(Goal_state_58, p4)))). % 5.49/2.39 tff(c_754, plain, (![Goal_state_5:state, Goal_state_79:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, Goal_state_79) | ~follows(Goal_state_79, p4)))). % 5.49/2.39 tff(c_1132, plain, (~follows(p3, p3))). % 5.49/2.39 tff(c_1131, plain, (~follows(p4, p3))). % 5.49/2.39 tff(c_939, plain, (![Goal_state_84:state, Goal_state_2:state]: (succeeds(Goal_state_84, p8) | ~follows(Goal_state_84, Goal_state_2) | ~follows(Goal_state_2, p3)))). % 5.49/2.39 tff(c_208, plain, (![Goal_state_5:state, Start_state_44:state]: (succeeds(Goal_state_5, Start_state_44) | ~succeeds(Goal_state_5, p4) | ~follows(p8, Start_state_44)))). % 5.49/2.39 tff(c_829, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p3) | ~follows(Start_state_1, p5) | ~follows(Goal_state_2, Start_state_1)))). % 5.49/2.39 tff(c_1074, plain, (~follows(p3, p4))). % 5.49/2.39 tff(c_1066, plain, (~follows(p4, p4))). % 5.49/2.39 tff(c_266, plain, (![Goal_state_49:state, Start_state_1:state, Start_state_50:state]: (succeeds(Goal_state_49, Start_state_1) | ~follows(Start_state_50, Start_state_1) | ~follows(p3, Start_state_50) | ~follows(Goal_state_49, p4)))). % 5.49/2.39 tff(c_937, plain, (![Goal_state_84:state, Goal_state_2:state]: (succeeds(Goal_state_84, p8) | ~follows(Goal_state_84, Goal_state_2) | ~follows(Goal_state_2, p4)))). % 5.49/2.39 tff(c_1058, plain, (~follows(p4, p5))). % 5.49/2.39 tff(c_919, plain, (![Goal_state_84:state, Goal_state_32:state]: (succeeds(Goal_state_84, p8) | ~follows(Goal_state_84, Goal_state_32) | ~follows(Goal_state_32, p5)))). % 5.49/2.39 tff(c_484, plain, (![Goal_state_5:state, Goal_state_57:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, Goal_state_57) | ~follows(Goal_state_57, p5)))). % 5.49/2.39 tff(c_205, plain, (![Start_state_1:state, Start_state_44:state]: (succeeds(p4, Start_state_1) | ~follows(Start_state_44, Start_state_1) | ~follows(p8, Start_state_44)))). % 5.49/2.39 tff(c_924, plain, (![Goal_state_84:state]: (succeeds(Goal_state_84, p8) | ~follows(Goal_state_84, p3)))). % 5.49/2.39 tff(c_361, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p8) | ~succeeds(Start_state_1, p3) | ~follows(Goal_state_2, Start_state_1)))). % 5.49/2.39 tff(c_185, plain, (![Goal_state_2:state, Start_state_43:state]: (succeeds(Goal_state_2, Start_state_43) | ~follows(p8, Start_state_43) | ~follows(Goal_state_2, p3)))). % 5.49/2.39 tff(c_102, plain, (![Goal_state_5:state, Goal_state_34:state]: (succeeds(Goal_state_5, p3) | ~succeeds(Goal_state_5, Goal_state_34) | ~follows(Goal_state_34, p5)))). % 5.49/2.39 tff(c_735, plain, (![Goal_state_2:state]: (succeeds(Goal_state_2, p8) | ~follows(Goal_state_2, p4)))). % 5.49/2.39 tff(c_552, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p4) | ~follows(Start_state_1, p5) | ~follows(Goal_state_2, Start_state_1)))). % 5.49/2.39 tff(c_731, plain, (![Start_state_23:state]: (~follows(Start_state_23, p5) | ~follows(p3, Start_state_23)))). % 5.49/2.39 tff(c_180, plain, (![Goal_state_32:state, Start_state_43:state]: (succeeds(Goal_state_32, Start_state_43) | ~follows(p8, Start_state_43) | ~follows(Goal_state_32, p5)))). % 5.49/2.39 tff(c_314, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p3) | ~follows(Start_state_1, p8) | ~follows(Goal_state_2, Start_state_1)))). % 5.49/2.39 tff(c_615, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p3) | ~follows(Start_state_1, p4) | ~follows(Goal_state_2, Start_state_1)))). % 5.49/2.39 tff(c_183, plain, (![Goal_state_2:state, Start_state_43:state]: (succeeds(Goal_state_2, Start_state_43) | ~follows(p8, Start_state_43) | ~follows(Goal_state_2, p4)))). % 5.49/2.40 tff(c_656, plain, (![Start_state_1:state]: (~follows(Start_state_1, p5) | ~follows(p8, Start_state_1)))). % 5.49/2.40 tff(c_156, plain, (![Goal_state_26:state, Start_state_41:state]: (succeeds(Goal_state_26, Start_state_41) | ~follows(p3, Start_state_41) | ~follows(Goal_state_26, p5)))). % 5.49/2.40 tff(c_123, plain, (![Start_state_1:state, Start_state_36:state]: (succeeds(p3, Start_state_1) | ~follows(Start_state_36, Start_state_1) | ~follows(p8, Start_state_36)))). % 5.49/2.40 tff(c_43, plain, (![Goal_state_5:state, Goal_state_21:state]: (succeeds(Goal_state_5, p3) | ~succeeds(Goal_state_5, Goal_state_21) | ~follows(Goal_state_21, p4)))). % 5.49/2.40 tff(c_553, plain, (~follows(p8, p5))). % 5.57/2.40 tff(c_88, plain, (![Goal_state_5:state, Goal_state_32:state]: (succeeds(Goal_state_5, p4) | ~succeeds(Goal_state_5, Goal_state_32) | ~follows(Goal_state_32, p5)))). % 5.57/2.40 tff(c_453, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, p4)))). % 5.57/2.40 tff(c_357, plain, (![Goal_state_26:state]: (succeeds(Goal_state_26, p8) | ~follows(Goal_state_26, p5)))). % 5.57/2.40 tff(c_439, plain, (succeeds(p3, p3))). % 5.57/2.40 tff(c_438, plain, (succeeds(p4, p8))). % 5.57/2.40 tff(c_362, plain, (~follows(p8, p8))). % 5.57/2.40 tff(c_132, plain, (![Goal_state_5:state, Goal_state_37:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, Goal_state_37) | ~succeeds(Goal_state_37, p3)))). % 5.57/2.40 tff(c_95, plain, (![Goal_state_5:state, Goal_state_33:state]: (succeeds(Goal_state_5, p3) | ~succeeds(Goal_state_5, Goal_state_33) | ~follows(Goal_state_33, p8)))). % 5.57/2.40 tff(c_51, plain, (![Goal_state_2:state, Start_state_23:state]: (succeeds(Goal_state_2, Start_state_23) | ~follows(p3, Start_state_23) | ~follows(Goal_state_2, p4)))). % 5.57/2.40 tff(c_94, plain, (![Goal_state_33:state, Start_state_1:state]: (succeeds(Goal_state_33, Start_state_1) | ~follows(p3, Start_state_1) | ~follows(Goal_state_33, p8)))). % 5.57/2.40 tff(c_86, plain, (![Goal_state_32:state, Start_state_1:state]: (succeeds(Goal_state_32, Start_state_1) | ~follows(p4, Start_state_1) | ~follows(Goal_state_32, p5)))). % 5.57/2.40 tff(c_184, plain, (![Start_state_43:state]: (succeeds(p4, Start_state_43) | ~follows(p8, Start_state_43)))). % 5.57/2.40 tff(c_125, plain, (![Goal_state_5:state, Start_state_36:state]: (succeeds(Goal_state_5, Start_state_36) | ~succeeds(Goal_state_5, p3) | ~follows(p8, Start_state_36)))). % 5.57/2.40 tff(c_66, plain, (![Goal_state_5:state, Start_state_25:state]: (succeeds(Goal_state_5, Start_state_25) | ~succeeds(Goal_state_5, p4) | ~follows(p3, Start_state_25)))). % 5.57/2.40 tff(c_142, plain, (~follows(p3, p5))). % 5.57/2.40 tff(c_63, plain, (![Start_state_1:state, Start_state_25:state]: (succeeds(p4, Start_state_1) | ~follows(Start_state_25, Start_state_1) | ~follows(p3, Start_state_25)))). % 5.57/2.40 tff(c_133, plain, (~follows(p8, p4))). % 5.57/2.40 tff(c_113, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, p3)))). % 5.57/2.40 tff(c_112, plain, (![Start_state_1:state]: (succeeds(p3, Start_state_1) | ~follows(p8, Start_state_1)))). % 5.57/2.40 tff(c_107, plain, (succeeds(p3, p8))). % 5.57/2.40 tff(c_77, plain, (![Start_state_30:state]: (succeeds(p3, Start_state_30) | ~has(Start_state_30, goto(loop))))). % 5.57/2.40 tff(c_87, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p3) | ~follows(Goal_state_32, p5)))). % 5.57/2.40 tff(c_73, plain, (![Goal_state_26:state]: (succeeds(Goal_state_26, p3) | ~follows(Goal_state_26, p8)))). % 5.57/2.40 tff(c_72, plain, (![Goal_state_26:state]: (succeeds(Goal_state_26, p4) | ~follows(Goal_state_26, p5)))). % 5.57/2.40 tff(c_6, plain, (![Goal_state_6:state, Start_state_8:state, Label_7:label]: (succeeds(Goal_state_6, Start_state_8) | ~labels(Label_7, Goal_state_6) | ~has(Start_state_8, goto(Label_7))))). % 5.57/2.40 tff(c_53, plain, (![Goal_state_2:state, Start_state_23:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_23) | ~follows(Start_state_1, Start_state_23) | ~follows(Goal_state_2, Start_state_1)))). % 5.57/2.40 tff(c_52, plain, (![Start_state_23:state]: (succeeds(p4, Start_state_23) | ~follows(p3, Start_state_23)))). % 5.57/2.40 tff(c_33, plain, (![Goal_state_17:state, Start_state_1:state, Goal_state_2:state]: (succeeds(Goal_state_17, Start_state_1) | ~succeeds(Goal_state_17, Goal_state_2) | ~follows(Goal_state_2, Start_state_1)))). % 5.57/2.40 tff(c_39, plain, (![Goal_state_2:state]: (succeeds(Goal_state_2, p3) | ~follows(Goal_state_2, p4)))). % 5.57/2.40 tff(c_32, plain, (![Goal_state_17:state]: (succeeds(Goal_state_17, p3) | ~succeeds(Goal_state_17, p4)))). % 5.57/2.40 tff(c_4, plain, (![Goal_state_5:state, Start_state_3:state, Intermediate_state_4:state]: (succeeds(Goal_state_5, Start_state_3) | ~succeeds(Intermediate_state_4, Start_state_3) | ~succeeds(Goal_state_5, Intermediate_state_4)))). % 5.57/2.40 tff(c_26, plain, (succeeds(p4, p3))). % 5.57/2.40 tff(c_8, plain, (![Goal_state_9:state, Start_state_11:state, Condition_10:boolean]: (succeeds(Goal_state_9, Start_state_11) | ~has(Start_state_11, ifthen(Condition_10, Goal_state_9))))). % 5.57/2.40 tff(c_12, plain, (has(p3, ifthen(equal_function(register_j, n), p4)))). % 5.57/2.40 tff(c_2, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_1) | ~follows(Goal_state_2, Start_state_1)))). % 5.57/2.40 tff(c_14, plain, (has(p4, goto(out)))). % 5.57/2.40 tff(c_20, plain, (has(p8, goto(loop)))). % 5.57/2.40 tff(c_10, plain, (labels(loop, p3))). % 5.57/2.40 tff(c_16, plain, (follows(p5, p4))). % 5.57/2.40 tff(c_18, plain, (follows(p8, p3))). % 5.57/2.40 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.57/2.40 %------------------------------------------------------------------------------