%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : COM002_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 : n009.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:30 PM UTC 2025 % Result : Satisfiable 13.21s 5.80s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : COM002_10 : TPTP v9.0.0. Released v8.2.0. % 0.11/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.14/0.35 % Computer : n009.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Mon Apr 7 16:09:11 EDT 2025 % 0.14/0.35 % CPUTime : % 13.21/5.79 % 13.21/5.80 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.21/5.80 % 13.21/5.80 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.21/5.80 %$ succeeds > labels > has > follows > times > plus > ifthen > equal_function > assign > #nlpp > goto > register_k > register_j > p8 > p7 > p6 > p5 > p4 > p3 > p2 > p1 > out > n2 > n1 > n0 > n > loop % 13.21/5.80 % 13.21/5.80 %Foreground sorts: % 13.21/5.80 tff(label, type, label: $tType ). % 13.21/5.80 tff(state, type, state: $tType ). % 13.21/5.80 tff(statement, type, statement: $tType ). % 13.21/5.80 tff(boolean, type, boolean: $tType ). % 13.21/5.80 tff(register, type, register: $tType ). % 13.21/5.80 tff(number, type, number: $tType ). % 13.21/5.80 % 13.21/5.80 %Background operators: % 13.21/5.80 % 13.21/5.80 % 13.21/5.80 %Foreground operators: % 13.21/5.80 tff(n1, type, n1: number). % 13.21/5.80 tff(out, type, out: label). % 13.21/5.80 tff(register_k, type, register_k: register). % 13.21/5.80 tff(goto, type, goto: label > statement). % 13.21/5.80 tff(equal_function, type, equal_function: (register * number) > boolean). % 13.21/5.80 tff(register_j, type, register_j: register). % 13.21/5.80 tff(n0, type, n0: number). % 13.21/5.80 tff(p8, type, p8: state). % 13.21/5.80 tff(labels, type, labels: (label * state) > $o). % 13.21/5.80 tff(p6, type, p6: state). % 13.21/5.80 tff(p7, type, p7: state). % 13.21/5.80 tff(assign, type, assign: (register * number) > statement). % 13.21/5.80 tff(ifthen, type, ifthen: (boolean * state) > statement). % 13.21/5.80 tff(p2, type, p2: state). % 13.21/5.80 tff(times, type, times: (number * register) > number). % 13.21/5.80 tff(p5, type, p5: state). % 13.21/5.80 tff(n2, type, n2: number). % 13.21/5.80 tff(has, type, has: (state * statement) > $o). % 13.21/5.80 tff(plus, type, plus: (register * number) > number). % 13.21/5.80 tff(succeeds, type, succeeds: (state * state) > $o). % 13.21/5.80 tff(n, type, n: number). % 13.21/5.80 tff(p1, type, p1: state). % 13.21/5.80 tff(loop, type, loop: label). % 13.21/5.80 tff(p3, type, p3: state). % 13.21/5.80 tff(follows, type, follows: (state * state) > $o). % 13.21/5.80 tff(p4, type, p4: state). % 13.21/5.80 % 13.21/5.80 %Saturated clause set: % 13.21/5.81 tff(c_40987, plain, (![Goal_state_2:state, Start_state_672:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_672) | ~follows(p1, Start_state_672) | ~follows(Start_state_1, p3) | ~follows(Goal_state_2, Start_state_1)))). % 13.21/5.81 tff(c_40620, plain, (![Goal_state_2:state, Start_state_669:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_669) | ~follows(p2, Start_state_669) | ~follows(Start_state_1, p4) | ~follows(Goal_state_2, Start_state_1)))). % 13.21/5.81 tff(c_40258, plain, (![Goal_state_2:state, Start_state_663:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_663) | ~follows(p2, Start_state_663) | ~follows(Start_state_1, p8) | ~follows(Goal_state_2, Start_state_1)))). % 13.21/5.81 tff(c_39627, plain, (![Goal_state_2:state, Start_state_659:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_659) | ~follows(p2, Start_state_659) | ~follows(Start_state_1, p6) | ~follows(Goal_state_2, Start_state_1)))). % 13.21/5.81 tff(c_23689, plain, (![Goal_state_5:state, Start_state_351:state, Goal_state_350:state]: (succeeds(Goal_state_5, Start_state_351) | ~succeeds(Goal_state_5, Goal_state_350) | ~follows(p1, Start_state_351) | ~follows(Goal_state_350, p3)))). % 13.21/5.81 tff(c_25969, plain, (![Goal_state_5:state, Start_state_369:state, Goal_state_368:state]: (succeeds(Goal_state_5, Start_state_369) | ~succeeds(Goal_state_5, Goal_state_368) | ~follows(p2, Start_state_369) | ~follows(Goal_state_368, p4)))). % 13.21/5.81 tff(c_25443, plain, (![Goal_state_364:state, Start_state_1:state, Start_state_365:state]: (succeeds(Goal_state_364, Start_state_1) | ~follows(Start_state_365, Start_state_1) | ~follows(p2, Start_state_365) | ~follows(Goal_state_364, p6)))). % 13.21/5.81 tff(c_24786, plain, (![Goal_state_5:state, Start_state_361:state, Goal_state_360:state]: (succeeds(Goal_state_5, Start_state_361) | ~succeeds(Goal_state_5, Goal_state_360) | ~follows(p2, Start_state_361) | ~follows(Goal_state_360, p8)))). % 13.21/5.81 tff(c_39282, plain, (![Start_state_1:state]: (~succeeds(Start_state_1, p7) | ~follows(p1, Start_state_1)))). % 13.21/5.81 tff(c_25445, plain, (![Goal_state_5:state, Start_state_365:state, Goal_state_364:state]: (succeeds(Goal_state_5, Start_state_365) | ~succeeds(Goal_state_5, Goal_state_364) | ~follows(p2, Start_state_365) | ~follows(Goal_state_364, p6)))). % 13.21/5.81 tff(c_24784, plain, (![Goal_state_360:state, Start_state_1:state, Start_state_361:state]: (succeeds(Goal_state_360, Start_state_1) | ~follows(Start_state_361, Start_state_1) | ~follows(p2, Start_state_361) | ~follows(Goal_state_360, p8)))). % 13.21/5.81 tff(c_25967, plain, (![Goal_state_368:state, Start_state_1:state, Start_state_369:state]: (succeeds(Goal_state_368, Start_state_1) | ~follows(Start_state_369, Start_state_1) | ~follows(p2, Start_state_369) | ~follows(Goal_state_368, p4)))). % 13.21/5.81 tff(c_38879, plain, (![Goal_state_2:state, Start_state_634:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_634) | ~follows(p2, Start_state_634) | ~follows(Start_state_1, p5) | ~follows(Goal_state_2, Start_state_1)))). % 13.21/5.81 tff(c_23687, plain, (![Goal_state_350:state, Start_state_1:state, Start_state_351:state]: (succeeds(Goal_state_350, Start_state_1) | ~follows(Start_state_351, Start_state_1) | ~follows(p1, Start_state_351) | ~follows(Goal_state_350, p3)))). % 13.21/5.81 tff(c_38495, plain, (![Goal_state_2:state, Start_state_622:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_622) | ~follows(p1, Start_state_622) | ~follows(Start_state_1, p7) | ~follows(Goal_state_2, Start_state_1)))). % 13.21/5.81 tff(c_38116, plain, (![Goal_state_2:state, Start_state_613:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_613) | ~follows(p3, Start_state_613) | ~follows(Start_state_1, p7) | ~follows(Goal_state_2, Start_state_1)))). % 13.21/5.81 tff(c_38899, plain, (![Start_state_1:state]: (~succeeds(Start_state_1, p6) | ~follows(p1, Start_state_1)))). % 13.21/5.81 tff(c_21293, plain, (![Goal_state_329:state, Start_state_1:state, Start_state_330:state]: (succeeds(Goal_state_329, Start_state_1) | ~follows(Start_state_330, Start_state_1) | ~follows(p1, Start_state_330) | ~follows(Goal_state_329, p7)))). % 13.21/5.81 tff(c_22649, plain, (![Goal_state_5:state, Start_state_342:state, Goal_state_341:state]: (succeeds(Goal_state_5, Start_state_342) | ~succeeds(Goal_state_5, Goal_state_341) | ~follows(p2, Start_state_342) | ~follows(Goal_state_341, p5)))). % 13.21/5.81 tff(c_18982, plain, (![Goal_state_313:state, Start_state_1:state, Start_state_314:state]: (succeeds(Goal_state_313, Start_state_1) | ~follows(Start_state_314, Start_state_1) | ~follows(p3, Start_state_314) | ~follows(Goal_state_313, p7)))). % 13.21/5.81 tff(c_22647, plain, (![Goal_state_341:state, Start_state_1:state, Start_state_342:state]: (succeeds(Goal_state_341, Start_state_1) | ~follows(Start_state_342, Start_state_1) | ~follows(p2, Start_state_342) | ~follows(Goal_state_341, p5)))). % 13.21/5.81 tff(c_37088, plain, (![Goal_state_2:state, Start_state_597:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_597) | ~follows(p6, Start_state_597) | ~follows(Start_state_1, p5) | ~follows(Goal_state_2, Start_state_1)))). % 13.21/5.81 tff(c_21295, plain, (![Goal_state_5:state, Start_state_330:state, Goal_state_329:state]: (succeeds(Goal_state_5, Start_state_330) | ~succeeds(Goal_state_5, Goal_state_329) | ~follows(p1, Start_state_330) | ~follows(Goal_state_329, p7)))). % 13.21/5.81 tff(c_37431, plain, (![Goal_state_2:state, Start_state_600:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_600) | ~follows(p6, Start_state_600) | ~follows(Start_state_1, p4) | ~follows(Goal_state_2, Start_state_1)))). % 13.21/5.81 tff(c_36381, plain, (![Goal_state_2:state, Start_state_588:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_588) | ~follows(p6, Start_state_588) | ~follows(Start_state_1, p3) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.81 tff(c_18984, plain, (![Goal_state_5:state, Start_state_314:state, Goal_state_313:state]: (succeeds(Goal_state_5, Start_state_314) | ~succeeds(Goal_state_5, Goal_state_313) | ~follows(p3, Start_state_314) | ~follows(Goal_state_313, p7)))). % 13.28/5.81 tff(c_37475, plain, (![Start_state_1:state]: (~succeeds(Start_state_1, p4) | ~follows(p1, Start_state_1)))). % 13.28/5.81 tff(c_36745, plain, (![Goal_state_2:state, Start_state_594:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_594) | ~follows(p6, Start_state_594) | ~follows(Start_state_1, p8) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.81 tff(c_15984, plain, (![Goal_state_267:state, Start_state_1:state, Start_state_268:state]: (succeeds(Goal_state_267, Start_state_1) | ~follows(Start_state_268, Start_state_1) | ~follows(p6, Start_state_268) | ~follows(Goal_state_267, p3)))). % 13.28/5.81 tff(c_15415, plain, (![Goal_state_263:state, Start_state_1:state, Start_state_264:state]: (succeeds(Goal_state_263, Start_state_1) | ~follows(Start_state_264, Start_state_1) | ~follows(p6, Start_state_264) | ~follows(Goal_state_263, p5)))). % 13.28/5.81 tff(c_16198, plain, (![Goal_state_5:state, Start_state_273:state, Goal_state_272:state]: (succeeds(Goal_state_5, Start_state_273) | ~succeeds(Goal_state_5, Goal_state_272) | ~follows(p6, Start_state_273) | ~follows(Goal_state_272, p4)))). % 13.28/5.81 tff(c_15417, plain, (![Goal_state_5:state, Start_state_264:state, Goal_state_263:state]: (succeeds(Goal_state_5, Start_state_264) | ~succeeds(Goal_state_5, Goal_state_263) | ~follows(p6, Start_state_264) | ~follows(Goal_state_263, p5)))). % 13.28/5.81 tff(c_15213, plain, (![Goal_state_5:state, Start_state_262:state, Goal_state_261:state]: (succeeds(Goal_state_5, Start_state_262) | ~succeeds(Goal_state_5, Goal_state_261) | ~follows(p6, Start_state_262) | ~follows(Goal_state_261, p8)))). % 13.28/5.81 tff(c_16196, plain, (![Goal_state_272:state, Start_state_1:state, Start_state_273:state]: (succeeds(Goal_state_272, Start_state_1) | ~follows(Start_state_273, Start_state_1) | ~follows(p6, Start_state_273) | ~follows(Goal_state_272, p4)))). % 13.28/5.81 tff(c_15986, plain, (![Goal_state_5:state, Start_state_268:state, Goal_state_267:state]: (succeeds(Goal_state_5, Start_state_268) | ~succeeds(Goal_state_5, Goal_state_267) | ~follows(p6, Start_state_268) | ~follows(Goal_state_267, p3)))). % 13.28/5.81 tff(c_15211, plain, (![Goal_state_261:state, Start_state_1:state, Start_state_262:state]: (succeeds(Goal_state_261, Start_state_1) | ~follows(Start_state_262, Start_state_1) | ~follows(p6, Start_state_262) | ~follows(Goal_state_261, p8)))). % 13.28/5.81 tff(c_34114, plain, (![Goal_state_2:state, Start_state_525:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_525) | ~follows(p1, Start_state_525) | ~follows(Start_state_1, p6) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_34804, plain, (![Goal_state_2:state, Start_state_534:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_534) | ~follows(p1, Start_state_534) | ~follows(Start_state_1, p4) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_34461, plain, (![Goal_state_2:state, Start_state_531:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_531) | ~follows(p3, Start_state_531) | ~follows(Start_state_1, p8) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_35899, plain, (![Goal_state_2:state, Start_state_549:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_549) | ~follows(p1, Start_state_549) | ~follows(Start_state_1, p5) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_35556, plain, (![Goal_state_2:state, Start_state_546:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_546) | ~follows(p1, Start_state_546) | ~follows(Start_state_1, p8) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_10541, plain, (![Goal_state_206:state, Start_state_1:state, Start_state_207:state]: (succeeds(Goal_state_206, Start_state_1) | ~follows(Start_state_207, Start_state_1) | ~follows(p2, Start_state_207) | ~follows(Goal_state_206, p7)))). % 13.28/5.82 tff(c_35213, plain, (![Goal_state_2:state, Start_state_543:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_543) | ~follows(p2, Start_state_543) | ~follows(Start_state_1, p7) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_14186, plain, (![Goal_state_250:state, Start_state_1:state, Start_state_251:state]: (succeeds(Goal_state_250, Start_state_1) | ~follows(Start_state_251, Start_state_1) | ~follows(p1, Start_state_251) | ~follows(Goal_state_250, p5)))). % 13.28/5.82 tff(c_10887, plain, (![Goal_state_210:state, Start_state_1:state, Start_state_211:state]: (succeeds(Goal_state_210, Start_state_1) | ~follows(Start_state_211, Start_state_1) | ~follows(p3, Start_state_211) | ~follows(Goal_state_210, p8)))). % 13.28/5.82 tff(c_32216, plain, (![Goal_state_2:state, Start_state_474:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_474) | ~follows(p8, Start_state_474) | ~follows(Start_state_1, p5) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_13699, plain, (![Goal_state_243:state, Start_state_1:state, Start_state_244:state]: (succeeds(Goal_state_243, Start_state_1) | ~follows(Start_state_244, Start_state_1) | ~follows(p1, Start_state_244) | ~follows(Goal_state_243, p4)))). % 13.28/5.82 tff(c_14188, plain, (![Goal_state_5:state, Start_state_251:state, Goal_state_250:state]: (succeeds(Goal_state_5, Start_state_251) | ~succeeds(Goal_state_5, Goal_state_250) | ~follows(p1, Start_state_251) | ~follows(Goal_state_250, p5)))). % 13.28/5.82 tff(c_13524, plain, (![Goal_state_5:state, Start_state_241:state, Goal_state_240:state]: (succeeds(Goal_state_5, Start_state_241) | ~succeeds(Goal_state_5, Goal_state_240) | ~follows(p1, Start_state_241) | ~follows(Goal_state_240, p8)))). % 13.28/5.82 tff(c_10543, plain, (![Goal_state_5:state, Start_state_207:state, Goal_state_206:state]: (succeeds(Goal_state_5, Start_state_207) | ~succeeds(Goal_state_5, Goal_state_206) | ~follows(p2, Start_state_207) | ~follows(Goal_state_206, p7)))). % 13.28/5.82 tff(c_13522, plain, (![Goal_state_240:state, Start_state_1:state, Start_state_241:state]: (succeeds(Goal_state_240, Start_state_1) | ~follows(Start_state_241, Start_state_1) | ~follows(p1, Start_state_241) | ~follows(Goal_state_240, p8)))). % 13.28/5.82 tff(c_9147, plain, (![Goal_state_191:state, Start_state_1:state, Start_state_192:state]: (succeeds(Goal_state_191, Start_state_1) | ~follows(Start_state_192, Start_state_1) | ~follows(p1, Start_state_192) | ~follows(Goal_state_191, p6)))). % 13.28/5.82 tff(c_13701, plain, (![Goal_state_5:state, Start_state_244:state, Goal_state_243:state]: (succeeds(Goal_state_5, Start_state_244) | ~succeeds(Goal_state_5, Goal_state_243) | ~follows(p1, Start_state_244) | ~follows(Goal_state_243, p4)))). % 13.28/5.82 tff(c_10889, plain, (![Goal_state_5:state, Start_state_211:state, Goal_state_210:state]: (succeeds(Goal_state_5, Start_state_211) | ~succeeds(Goal_state_5, Goal_state_210) | ~follows(p3, Start_state_211) | ~follows(Goal_state_210, p8)))). % 13.28/5.82 tff(c_32977, plain, (![Goal_state_2:state, Start_state_492:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_492) | ~follows(p8, Start_state_492) | ~follows(Start_state_1, p7) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_9149, plain, (![Goal_state_5:state, Start_state_192:state, Goal_state_191:state]: (succeeds(Goal_state_5, Start_state_192) | ~succeeds(Goal_state_5, Goal_state_191) | ~follows(p1, Start_state_192) | ~follows(Goal_state_191, p6)))). % 13.28/5.82 tff(c_33386, plain, (![Goal_state_2:state, Start_state_501:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_501) | ~follows(p8, Start_state_501) | ~follows(Start_state_1, p3) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_33757, plain, (![Goal_state_2:state, Start_state_513:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_513) | ~follows(p8, Start_state_513) | ~follows(Start_state_1, p6) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_32605, plain, (![Goal_state_2:state, Start_state_486:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_486) | ~follows(p8, Start_state_486) | ~follows(Start_state_1, p4) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_4103, plain, (![Goal_state_5:state, Start_state_127:state, Goal_state_126:state]: (succeeds(Goal_state_5, Start_state_127) | ~succeeds(Goal_state_5, Goal_state_126) | ~follows(p8, Start_state_127) | ~follows(Goal_state_126, p6)))). % 13.28/5.82 tff(c_4598, plain, (![Goal_state_134:state, Start_state_1:state, Start_state_135:state]: (succeeds(Goal_state_134, Start_state_1) | ~follows(Start_state_135, Start_state_1) | ~follows(p8, Start_state_135) | ~follows(Goal_state_134, p7)))). % 13.28/5.82 tff(c_6907, plain, (![Goal_state_2:state, Start_state_178:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_178) | ~follows(p1, Start_state_178) | ~follows(Start_state_1, p2) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_18770, plain, (![Goal_state_2:state, Start_state_311:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_311) | ~follows(p3, Start_state_311) | ~follows(Start_state_1, p5) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_3985, plain, (![Goal_state_5:state, Start_state_124:state, Goal_state_123:state]: (succeeds(Goal_state_5, Start_state_124) | ~succeeds(Goal_state_5, Goal_state_123) | ~follows(p8, Start_state_124) | ~follows(Goal_state_123, p3)))). % 13.28/5.82 tff(c_4511, plain, (![Goal_state_132:state, Start_state_1:state, Start_state_133:state]: (succeeds(Goal_state_132, Start_state_1) | ~follows(Start_state_133, Start_state_1) | ~follows(p8, Start_state_133) | ~follows(Goal_state_132, p4)))). % 13.28/5.82 tff(c_4185, plain, (![Goal_state_128:state, Start_state_1:state, Start_state_129:state]: (succeeds(Goal_state_128, Start_state_1) | ~follows(Start_state_129, Start_state_1) | ~follows(p8, Start_state_129) | ~follows(Goal_state_128, p5)))). % 13.28/5.82 tff(c_4600, plain, (![Goal_state_5:state, Start_state_135:state, Goal_state_134:state]: (succeeds(Goal_state_5, Start_state_135) | ~succeeds(Goal_state_5, Goal_state_134) | ~follows(p8, Start_state_135) | ~follows(Goal_state_134, p7)))). % 13.28/5.82 tff(c_8600, plain, (![Goal_state_2:state, Start_state_187:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_187) | ~follows(p4, Start_state_187) | ~follows(Start_state_1, p5) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_4513, plain, (![Goal_state_5:state, Start_state_133:state, Goal_state_132:state]: (succeeds(Goal_state_5, Start_state_133) | ~succeeds(Goal_state_5, Goal_state_132) | ~follows(p8, Start_state_133) | ~follows(Goal_state_132, p4)))). % 13.28/5.82 tff(c_26512, plain, (![Goal_state_2:state, Start_state_374:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_374) | ~follows(p2, Start_state_374) | ~follows(Start_state_1, p3) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_4101, plain, (![Goal_state_126:state, Start_state_1:state, Start_state_127:state]: (succeeds(Goal_state_126, Start_state_1) | ~follows(Start_state_127, Start_state_1) | ~follows(p8, Start_state_127) | ~follows(Goal_state_126, p6)))). % 13.28/5.82 tff(c_3983, plain, (![Goal_state_123:state, Start_state_1:state, Start_state_124:state]: (succeeds(Goal_state_123, Start_state_1) | ~follows(Start_state_124, Start_state_1) | ~follows(p8, Start_state_124) | ~follows(Goal_state_123, p3)))). % 13.28/5.82 tff(c_4187, plain, (![Goal_state_5:state, Start_state_129:state, Goal_state_128:state]: (succeeds(Goal_state_5, Start_state_129) | ~succeeds(Goal_state_5, Goal_state_128) | ~follows(p8, Start_state_129) | ~follows(Goal_state_128, p5)))). % 13.28/5.82 tff(c_14008, plain, (![Goal_state_2:state, Start_state_246:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_246) | ~follows(p3, Start_state_246) | ~follows(Start_state_1, p4) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_31388, plain, (![Goal_state_2:state, Start_state_440:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_440) | ~follows(p6, Start_state_440) | ~follows(Start_state_1, p7) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_28221, plain, (![Goal_state_2:state, Start_state_401:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_401) | ~follows(p3, Start_state_401) | ~follows(Start_state_1, p6) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_1694, plain, (![Goal_state_87:state, Start_state_1:state, Start_state_88:state]: (succeeds(Goal_state_87, Start_state_1) | ~follows(Start_state_88, Start_state_1) | ~follows(p3, Start_state_88) | ~follows(Goal_state_87, p5)))). % 13.28/5.82 tff(c_31778, plain, (![Goal_state_2:state, Start_state_447:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_447) | ~follows(p7, Start_state_447) | ~follows(Start_state_1, p8) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.82 tff(c_314, plain, (![Goal_state_50:state, Start_state_1:state, Start_state_51:state]: (succeeds(Goal_state_50, Start_state_1) | ~follows(Start_state_51, Start_state_1) | ~follows(p3, Start_state_51) | ~follows(Goal_state_50, p4)))). % 13.28/5.82 tff(c_1187, plain, (![Goal_state_73:state, Start_state_1:state, Start_state_74:state]: (succeeds(Goal_state_73, Start_state_1) | ~follows(Start_state_74, Start_state_1) | ~follows(p3, Start_state_74) | ~follows(Goal_state_73, p6)))). % 13.28/5.82 tff(c_1746, plain, (![Goal_state_89:state, Start_state_1:state, Start_state_90:state]: (succeeds(Goal_state_89, Start_state_1) | ~follows(Start_state_90, Start_state_1) | ~follows(p4, Start_state_90) | ~follows(Goal_state_89, p5)))). % 13.28/5.82 tff(c_2691, plain, (![Goal_state_5:state, Start_state_107:state, Goal_state_106:state]: (succeeds(Goal_state_5, Start_state_107) | ~succeeds(Goal_state_5, Goal_state_106) | ~follows(p7, Start_state_107) | ~follows(Goal_state_106, p8)))). % 13.28/5.82 tff(c_6597, plain, (![Start_state_1:state, Start_state_174:state]: (succeeds(p7, Start_state_1) | ~follows(Start_state_174, Start_state_1) | ~follows(p2, Start_state_174)))). % 13.28/5.82 tff(c_8308, plain, (![Start_state_1:state, Start_state_185:state]: (succeeds(p8, Start_state_1) | ~follows(Start_state_185, Start_state_1) | ~follows(p3, Start_state_185)))). % 13.28/5.82 tff(c_1421, plain, (![Goal_state_5:state, Start_state_81:state, Goal_state_80:state]: (succeeds(Goal_state_5, Start_state_81) | ~succeeds(Goal_state_5, Goal_state_80) | ~follows(p6, Start_state_81) | ~follows(Goal_state_80, p7)))). % 13.28/5.82 tff(c_7910, plain, (![Start_state_1:state, Start_state_183:state]: (succeeds(p8, Start_state_1) | ~follows(Start_state_183, Start_state_1) | ~follows(p1, Start_state_183)))). % 13.28/5.82 tff(c_6347, plain, (![Start_state_1:state, Start_state_172:state]: (succeeds(p7, Start_state_1) | ~follows(Start_state_172, Start_state_1) | ~follows(p1, Start_state_172)))). % 13.28/5.82 tff(c_30970, plain, (![Start_state_1:state]: (~follows(Start_state_1, p8) | ~follows(p4, Start_state_1)))). % 13.28/5.82 tff(c_6350, plain, (![Goal_state_5:state, Start_state_172:state]: (succeeds(Goal_state_5, Start_state_172) | ~succeeds(Goal_state_5, p7) | ~follows(p1, Start_state_172)))). % 13.28/5.82 tff(c_9013, plain, (![Goal_state_5:state, Start_state_190:state]: (succeeds(Goal_state_5, Start_state_190) | ~succeeds(Goal_state_5, p8) | ~follows(p2, Start_state_190)))). % 13.28/5.83 tff(c_9010, plain, (![Start_state_1:state, Start_state_190:state]: (succeeds(p8, Start_state_1) | ~follows(Start_state_190, Start_state_1) | ~follows(p2, Start_state_190)))). % 13.28/5.83 tff(c_8311, plain, (![Goal_state_5:state, Start_state_185:state]: (succeeds(Goal_state_5, Start_state_185) | ~succeeds(Goal_state_5, p8) | ~follows(p3, Start_state_185)))). % 13.28/5.83 tff(c_6472, plain, (![Start_state_1:state, Start_state_173:state]: (succeeds(p7, Start_state_1) | ~follows(Start_state_173, Start_state_1) | ~follows(p3, Start_state_173)))). % 13.28/5.83 tff(c_6475, plain, (![Goal_state_5:state, Start_state_173:state]: (succeeds(Goal_state_5, Start_state_173) | ~succeeds(Goal_state_5, p7) | ~follows(p3, Start_state_173)))). % 13.28/5.83 tff(c_7913, plain, (![Goal_state_5:state, Start_state_183:state]: (succeeds(Goal_state_5, Start_state_183) | ~succeeds(Goal_state_5, p8) | ~follows(p1, Start_state_183)))). % 13.28/5.83 tff(c_6600, plain, (![Goal_state_5:state, Start_state_174:state]: (succeeds(Goal_state_5, Start_state_174) | ~succeeds(Goal_state_5, p7) | ~follows(p2, Start_state_174)))). % 13.28/5.83 tff(c_3898, plain, (![Goal_state_5:state, Start_state_120:state]: (succeeds(Goal_state_5, Start_state_120) | ~succeeds(Goal_state_5, p6) | ~follows(p2, Start_state_120)))). % 13.28/5.83 tff(c_23430, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p2) | ~follows(Start_state_1, p8) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.83 tff(c_29201, plain, (![Goal_state_2:state]: (~follows(p1, Goal_state_2) | ~follows(Goal_state_2, p3)))). % 13.28/5.83 tff(c_29196, plain, (![Goal_state_32:state]: (~follows(p1, Goal_state_32) | ~follows(Goal_state_32, p6)))). % 13.28/5.83 tff(c_28877, plain, (![Start_state_1:state]: (~succeeds(Start_state_1, p3) | ~follows(p1, Start_state_1)))). % 13.28/5.83 tff(c_5687, plain, (![Goal_state_5:state, Start_state_168:state]: (succeeds(Goal_state_5, Start_state_168) | ~succeeds(Goal_state_5, p7) | ~follows(p6, Start_state_168)))). % 13.28/5.83 tff(c_5684, plain, (![Start_state_1:state, Start_state_168:state]: (succeeds(p7, Start_state_1) | ~follows(Start_state_168, Start_state_1) | ~follows(p6, Start_state_168)))). % 13.28/5.83 tff(c_23052, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p8) | ~succeeds(Start_state_1, p7) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.83 tff(c_7770, plain, (![Start_state_1:state, Start_state_182:state]: (succeeds(p8, Start_state_1) | ~follows(Start_state_182, Start_state_1) | ~follows(p6, Start_state_182)))). % 13.28/5.83 tff(c_28222, plain, (~succeeds(p1, p7))). % 13.28/5.83 tff(c_1189, plain, (![Goal_state_5:state, Start_state_74:state, Goal_state_73:state]: (succeeds(Goal_state_5, Start_state_74) | ~succeeds(Goal_state_5, Goal_state_73) | ~follows(p3, Start_state_74) | ~follows(Goal_state_73, p6)))). % 13.28/5.83 tff(c_27146, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p2) | ~follows(Start_state_1, p4) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.83 tff(c_3895, plain, (![Start_state_1:state, Start_state_120:state]: (succeeds(p6, Start_state_1) | ~follows(Start_state_120, Start_state_1) | ~follows(p2, Start_state_120)))). % 13.28/5.83 tff(c_7773, plain, (![Goal_state_5:state, Start_state_182:state]: (succeeds(Goal_state_5, Start_state_182) | ~succeeds(Goal_state_5, p8) | ~follows(p6, Start_state_182)))). % 13.28/5.83 tff(c_25172, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p2) | ~follows(Start_state_1, p6) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.83 tff(c_24089, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p1) | ~follows(Start_state_1, p3) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.83 tff(c_27559, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p1) | ~follows(Start_state_1, p7) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.83 tff(c_2620, plain, (![Start_state_1:state, Start_state_105:state]: (succeeds(p4, Start_state_1) | ~follows(Start_state_105, Start_state_1) | ~follows(p2, Start_state_105)))). % 13.28/5.83 tff(c_1644, plain, (![Goal_state_5:state, Goal_state_86:state]: (succeeds(Goal_state_5, p1) | ~succeeds(Goal_state_5, Goal_state_86) | ~follows(Goal_state_86, p7)))). % 13.28/5.83 tff(c_2548, plain, (![Goal_state_5:state, Goal_state_104:state]: (succeeds(Goal_state_5, p2) | ~succeeds(Goal_state_5, Goal_state_104) | ~follows(Goal_state_104, p4)))). % 13.28/5.83 tff(c_5397, plain, (![Start_state_1:state, Start_state_166:state]: (succeeds(p7, Start_state_1) | ~follows(Start_state_166, Start_state_1) | ~follows(p8, Start_state_166)))). % 13.28/5.83 tff(c_18422, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p3) | ~follows(Start_state_1, p7) | ~follows(Goal_state_2, Start_state_1)))). % 13.28/5.83 tff(c_26465, plain, (![Goal_state_5:state, Start_state_374:state]: (succeeds(Goal_state_5, Start_state_374) | ~follows(p2, Start_state_374) | ~succeeds(Goal_state_5, p4)))). % 13.28/5.83 tff(c_2354, plain, (![Goal_state_5:state, Start_state_101:state, Goal_state_100:state]: (succeeds(Goal_state_5, Start_state_101) | ~succeeds(Goal_state_5, Goal_state_100) | ~follows(p2, Start_state_101) | ~follows(Goal_state_100, p3)))). % 13.35/5.83 tff(c_25991, plain, (~succeeds(p1, p6))). % 13.35/5.83 tff(c_1419, plain, (![Goal_state_80:state, Start_state_1:state, Start_state_81:state]: (succeeds(Goal_state_80, Start_state_1) | ~follows(Start_state_81, Start_state_1) | ~follows(p6, Start_state_81) | ~follows(Goal_state_80, p7)))). % 13.35/5.83 tff(c_2547, plain, (![Goal_state_104:state, Start_state_1:state]: (succeeds(Goal_state_104, Start_state_1) | ~follows(p2, Start_state_1) | ~follows(Goal_state_104, p4)))). % 13.35/5.83 tff(c_19418, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p8) | ~succeeds(Start_state_1, p6) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.83 tff(c_2752, plain, (![Goal_state_109:state, Start_state_1:state]: (succeeds(Goal_state_109, Start_state_1) | ~follows(p2, Start_state_1) | ~follows(Goal_state_109, p6)))). % 13.35/5.83 tff(c_2753, plain, (![Goal_state_5:state, Goal_state_109:state]: (succeeds(Goal_state_5, p2) | ~succeeds(Goal_state_5, Goal_state_109) | ~follows(Goal_state_109, p6)))). % 13.35/5.83 tff(c_19594, plain, (![Goal_state_32:state, Start_state_318:state]: (succeeds(Goal_state_32, Start_state_318) | ~follows(p2, Start_state_318) | ~follows(Goal_state_32, p8)))). % 13.35/5.83 tff(c_20819, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p2) | ~follows(Start_state_1, p5) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.83 tff(c_5298, plain, (![Goal_state_165:state, Start_state_1:state]: (succeeds(Goal_state_165, Start_state_1) | ~follows(p8, Start_state_1) | ~succeeds(Goal_state_165, p7)))). % 13.35/5.83 tff(c_20028, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p6) | ~succeeds(Start_state_1, p4) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.83 tff(c_1563, plain, (![Goal_state_5:state, Goal_state_84:state]: (succeeds(Goal_state_5, p1) | ~succeeds(Goal_state_5, Goal_state_84) | ~follows(Goal_state_84, p3)))). % 13.35/5.83 tff(c_1562, plain, (![Goal_state_84:state, Start_state_1:state]: (succeeds(Goal_state_84, Start_state_1) | ~follows(p1, Start_state_1) | ~follows(Goal_state_84, p3)))). % 13.35/5.83 tff(c_2722, plain, (![Goal_state_5:state, Goal_state_108:state]: (succeeds(Goal_state_5, p2) | ~succeeds(Goal_state_5, Goal_state_108) | ~follows(Goal_state_108, p8)))). % 13.35/5.83 tff(c_5299, plain, (![Goal_state_5:state, Goal_state_165:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, Goal_state_165) | ~succeeds(Goal_state_165, p7)))). % 13.35/5.83 tff(c_22673, plain, (![Start_state_107:state]: (~follows(Start_state_107, p5) | ~follows(p7, Start_state_107)))). % 13.35/5.83 tff(c_2420, plain, (![Start_state_1:state, Start_state_102:state]: (succeeds(p3, Start_state_1) | ~follows(Start_state_102, Start_state_1) | ~follows(p2, Start_state_102)))). % 13.35/5.83 tff(c_2290, plain, (![Goal_state_99:state, Start_state_1:state]: (succeeds(Goal_state_99, Start_state_1) | ~follows(p2, Start_state_1) | ~follows(Goal_state_99, p5)))). % 13.35/5.83 tff(c_4863, plain, (![Goal_state_5:state, Goal_state_144:state]: (succeeds(Goal_state_5, p6) | ~succeeds(Goal_state_5, Goal_state_144) | ~follows(Goal_state_144, p4)))). % 13.35/5.83 tff(c_4913, plain, (![Goal_state_5:state, Goal_state_145:state]: (succeeds(Goal_state_5, p6) | ~succeeds(Goal_state_5, Goal_state_145) | ~follows(Goal_state_145, p3)))). % 13.35/5.83 tff(c_12903, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p1) | ~follows(Start_state_1, p4) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.83 tff(c_3801, plain, (![Start_state_1:state, Start_state_119:state]: (succeeds(p6, Start_state_1) | ~follows(Start_state_119, Start_state_1) | ~follows(p1, Start_state_119)))). % 13.35/5.83 tff(c_21296, plain, (~succeeds(p1, p4))). % 13.35/5.83 tff(c_15780, 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)))). % 13.35/5.83 tff(c_6830, plain, (![Goal_state_32:state, Start_state_178:state]: (succeeds(Goal_state_32, Start_state_178) | ~follows(p1, Start_state_178) | ~follows(Goal_state_32, p7)))). % 13.35/5.83 tff(c_1619, plain, (![Goal_state_5:state, Start_state_85:state]: (succeeds(Goal_state_5, Start_state_85) | ~succeeds(Goal_state_5, p3) | ~follows(p1, Start_state_85)))). % 13.35/5.83 tff(c_2291, plain, (![Goal_state_5:state, Goal_state_99:state]: (succeeds(Goal_state_5, p2) | ~succeeds(Goal_state_5, Goal_state_99) | ~follows(Goal_state_99, p5)))). % 13.35/5.83 tff(c_3804, plain, (![Goal_state_5:state, Start_state_119:state]: (succeeds(Goal_state_5, Start_state_119) | ~succeeds(Goal_state_5, p6) | ~follows(p1, Start_state_119)))). % 13.35/5.83 tff(c_1445, plain, (![Goal_state_82:state, Start_state_1:state]: (succeeds(Goal_state_82, Start_state_1) | ~follows(p6, Start_state_1) | ~succeeds(Goal_state_82, p4)))). % 13.35/5.83 tff(c_1446, plain, (![Goal_state_5:state, Goal_state_82:state]: (succeeds(Goal_state_5, p6) | ~succeeds(Goal_state_5, Goal_state_82) | ~succeeds(Goal_state_82, p4)))). % 13.35/5.83 tff(c_2423, plain, (![Goal_state_5:state, Start_state_102:state]: (succeeds(Goal_state_5, Start_state_102) | ~succeeds(Goal_state_5, p3) | ~follows(p2, Start_state_102)))). % 13.35/5.83 tff(c_3371, plain, (![Goal_state_5:state, Goal_state_115:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, Goal_state_115) | ~succeeds(Goal_state_115, p6)))). % 13.35/5.83 tff(c_16791, plain, (![Goal_state_32:state, Start_state_279:state]: (succeeds(Goal_state_32, Start_state_279) | ~follows(p3, Start_state_279) | ~follows(Goal_state_32, p7)))). % 13.35/5.83 tff(c_1696, plain, (![Goal_state_5:state, Start_state_88:state, Goal_state_87:state]: (succeeds(Goal_state_5, Start_state_88) | ~succeeds(Goal_state_5, Goal_state_87) | ~follows(p3, Start_state_88) | ~follows(Goal_state_87, p5)))). % 13.35/5.83 tff(c_18447, plain, (![Start_state_102:state]: (~follows(Start_state_102, p5) | ~follows(p2, Start_state_102)))). % 13.35/5.83 tff(c_15927, plain, (![Goal_state_2:state, Goal_state_267:state]: (succeeds(Goal_state_2, p6) | ~follows(Goal_state_2, Goal_state_267) | ~follows(Goal_state_267, p3)))). % 13.35/5.83 tff(c_3711, plain, (![Goal_state_5:state, Goal_state_118:state]: (succeeds(Goal_state_5, p3) | ~succeeds(Goal_state_5, Goal_state_118) | ~follows(Goal_state_118, p7)))). % 13.35/5.83 tff(c_13303, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p1) | ~follows(Start_state_1, p8) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.83 tff(c_1367, plain, (![Start_state_1:state, Start_state_79:state]: (succeeds(p4, Start_state_1) | ~follows(Start_state_79, Start_state_1) | ~follows(p6, Start_state_79)))). % 13.35/5.83 tff(c_1616, plain, (![Start_state_1:state, Start_state_85:state]: (succeeds(p3, Start_state_1) | ~follows(Start_state_85, Start_state_1) | ~follows(p1, Start_state_85)))). % 13.35/5.83 tff(c_14631, plain, (![Goal_state_257:state, Goal_state_2:state]: (succeeds(Goal_state_257, p6) | ~follows(Goal_state_257, Goal_state_2) | ~follows(Goal_state_2, p4)))). % 13.35/5.83 tff(c_16571, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p1) | ~follows(Start_state_1, p5) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.83 tff(c_17533, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p6) | ~follows(Start_state_1, p8) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.83 tff(c_17163, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p6) | ~follows(Start_state_1, p5) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.83 tff(c_695, plain, (![Start_state_1:state, Start_state_64:state]: (succeeds(p3, Start_state_1) | ~follows(Start_state_64, Start_state_1) | ~follows(p6, Start_state_64)))). % 13.35/5.83 tff(c_3252, plain, (![Start_state_1:state, Start_state_112:state]: (succeeds(p6, Start_state_1) | ~follows(Start_state_112, Start_state_1) | ~follows(p8, Start_state_112)))). % 13.35/5.83 tff(c_4812, plain, (![Goal_state_5:state, Goal_state_141:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, Goal_state_141) | ~follows(Goal_state_141, p4)))). % 13.35/5.83 tff(c_17534, plain, (![Start_state_62:state]: (~follows(Start_state_62, p4) | ~follows(p1, Start_state_62)))). % 13.35/5.84 tff(c_4973, plain, (![Goal_state_5:state, Goal_state_150:state]: (succeeds(Goal_state_5, p6) | ~succeeds(Goal_state_5, Goal_state_150) | ~follows(Goal_state_150, p8)))). % 13.35/5.84 tff(c_1318, plain, (![Goal_state_5:state, Goal_state_78:state]: (succeeds(Goal_state_5, p6) | ~succeeds(Goal_state_5, Goal_state_78) | ~follows(Goal_state_78, p5)))). % 13.35/5.84 tff(c_3336, plain, (![Goal_state_5:state, Start_state_113:state]: (succeeds(Goal_state_5, Start_state_113) | ~succeeds(Goal_state_5, p6) | ~follows(p3, Start_state_113)))). % 13.35/5.84 tff(c_295, plain, (![Goal_state_5:state, Goal_state_49:state]: (succeeds(Goal_state_5, p1) | ~succeeds(Goal_state_5, Goal_state_49) | ~follows(Goal_state_49, p5)))). % 13.35/5.84 tff(c_11611, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p2) | ~follows(Start_state_1, p7) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.84 tff(c_10734, plain, (![Goal_state_2:state, Start_state_209:state]: (succeeds(Goal_state_2, Start_state_209) | ~follows(p6, Start_state_209) | ~follows(Goal_state_2, p4)))). % 13.35/5.84 tff(c_15991, plain, (![Start_state_1:state]: (~follows(Start_state_1, p8) | ~follows(p6, Start_state_1)))). % 13.35/5.84 tff(c_12144, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p1) | ~follows(Start_state_1, p6) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.84 tff(c_10736, plain, (![Goal_state_2:state, Start_state_209:state]: (succeeds(Goal_state_2, Start_state_209) | ~follows(p6, Start_state_209) | ~follows(Goal_state_2, p3)))). % 13.35/5.84 tff(c_1291, plain, (![Goal_state_5:state, Goal_state_77:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, Goal_state_77) | ~succeeds(Goal_state_77, p4)))). % 13.35/5.84 tff(c_10730, plain, (![Goal_state_35:state, Start_state_209:state]: (succeeds(Goal_state_35, Start_state_209) | ~follows(p6, Start_state_209) | ~follows(Goal_state_35, p5)))). % 13.35/5.84 tff(c_10723, plain, (![Goal_state_32:state, Start_state_209:state]: (succeeds(Goal_state_32, Start_state_209) | ~follows(p6, Start_state_209) | ~follows(Goal_state_32, p8)))). % 13.35/5.84 tff(c_4776, plain, (![Goal_state_5:state, Goal_state_140:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, Goal_state_140) | ~follows(Goal_state_140, p3)))). % 13.35/5.84 tff(c_12555, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p6) | ~succeeds(Start_state_1, p3) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.84 tff(c_3255, plain, (![Goal_state_5:state, Start_state_112:state]: (succeeds(Goal_state_5, Start_state_112) | ~succeeds(Goal_state_5, p6) | ~follows(p8, Start_state_112)))). % 13.35/5.84 tff(c_3333, plain, (![Start_state_1:state, Start_state_113:state]: (succeeds(p6, Start_state_1) | ~follows(Start_state_113, Start_state_1) | ~follows(p3, Start_state_113)))). % 13.35/5.84 tff(c_14189, plain, (![Start_state_62:state]: (~follows(Start_state_62, p7) | ~follows(p1, Start_state_62)))). % 13.35/5.84 tff(c_6888, plain, (![Goal_state_35:state, Start_state_178:state]: (succeeds(Goal_state_35, Start_state_178) | ~follows(p1, Start_state_178) | ~follows(Goal_state_35, p5)))). % 13.35/5.84 tff(c_10008, 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)))). % 13.35/5.84 tff(c_316, plain, (![Goal_state_5:state, Start_state_51:state, Goal_state_50:state]: (succeeds(Goal_state_5, Start_state_51) | ~succeeds(Goal_state_5, Goal_state_50) | ~follows(p3, Start_state_51) | ~follows(Goal_state_50, p4)))). % 13.35/5.84 tff(c_6903, plain, (![Goal_state_2:state, Start_state_178:state]: (succeeds(Goal_state_2, Start_state_178) | ~follows(p1, Start_state_178) | ~follows(Goal_state_2, p4)))). % 13.35/5.84 tff(c_13525, plain, (![Start_state_1:state]: (~follows(Start_state_1, p5) | ~follows(p1, Start_state_1)))). % 13.35/5.84 tff(c_6875, plain, (![Goal_state_32:state, Start_state_178:state]: (succeeds(Goal_state_32, Start_state_178) | ~follows(p1, Start_state_178) | ~follows(Goal_state_32, p8)))). % 13.35/5.84 tff(c_2689, plain, (![Goal_state_106:state, Start_state_1:state, Start_state_107:state]: (succeeds(Goal_state_106, Start_state_1) | ~follows(Start_state_107, Start_state_1) | ~follows(p7, Start_state_107) | ~follows(Goal_state_106, p8)))). % 13.35/5.84 tff(c_13328, plain, (~follows(p4, p4))). % 13.35/5.84 tff(c_4738, plain, (![Goal_state_138:state, Goal_state_2:state]: (succeeds(Goal_state_138, p8) | ~follows(Goal_state_138, Goal_state_2) | ~follows(Goal_state_2, p4)))). % 13.35/5.84 tff(c_12955, plain, (![Start_state_1:state]: (~follows(Start_state_1, p8) | ~follows(p1, Start_state_1)))). % 13.35/5.84 tff(c_1264, plain, (![Goal_state_5:state, Goal_state_76:state]: (succeeds(Goal_state_5, p1) | ~succeeds(Goal_state_5, Goal_state_76) | ~follows(Goal_state_76, p8)))). % 13.35/5.84 tff(c_12953, plain, (![Start_state_81:state]: (~follows(Start_state_81, p5) | ~follows(p6, Start_state_81)))). % 13.35/5.84 tff(c_1236, plain, (![Start_state_1:state, Start_state_75:state]: (succeeds(p4, Start_state_1) | ~follows(Start_state_75, Start_state_1) | ~follows(p8, Start_state_75)))). % 13.35/5.84 tff(c_12928, plain, (~follows(p4, p7))). % 13.35/5.84 tff(c_4720, plain, (![Goal_state_138:state, Goal_state_39:state]: (succeeds(Goal_state_138, p8) | ~follows(Goal_state_138, Goal_state_39) | ~follows(Goal_state_39, p7)))). % 13.35/5.84 tff(c_265, plain, (![Goal_state_5:state, Goal_state_47:state]: (succeeds(Goal_state_5, p1) | ~succeeds(Goal_state_5, Goal_state_47) | ~follows(Goal_state_47, p4)))). % 13.35/5.84 tff(c_660, plain, (![Goal_state_5:state, Goal_state_63:state]: (succeeds(Goal_state_5, p6) | ~succeeds(Goal_state_5, Goal_state_63) | ~succeeds(Goal_state_63, p3)))). % 13.35/5.84 tff(c_12145, plain, (![Start_state_101:state]: (~follows(Start_state_101, p8) | ~follows(p2, Start_state_101)))). % 13.35/5.84 tff(c_522, plain, (![Goal_state_5:state, Goal_state_58:state]: (succeeds(Goal_state_5, p1) | ~succeeds(Goal_state_5, Goal_state_58) | ~follows(Goal_state_58, p6)))). % 13.35/5.84 tff(c_285, plain, (![Start_state_1:state, Start_state_48:state]: (succeeds(p4, Start_state_1) | ~follows(Start_state_48, Start_state_1) | ~follows(p1, Start_state_48)))). % 13.35/5.84 tff(c_288, plain, (![Goal_state_5:state, Start_state_48:state]: (succeeds(Goal_state_5, Start_state_48) | ~succeeds(Goal_state_5, p4) | ~follows(p1, Start_state_48)))). % 13.35/5.84 tff(c_2124, plain, (![Goal_state_5:state, Goal_state_95:state]: (succeeds(Goal_state_5, p2) | ~succeeds(Goal_state_5, Goal_state_95) | ~follows(Goal_state_95, p7)))). % 13.35/5.84 tff(c_4020, plain, (![Goal_state_5:state, Goal_state_125:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, Goal_state_125) | ~follows(Goal_state_125, p6)))). % 13.35/5.84 tff(c_799, plain, (![Goal_state_67:state, Start_state_1:state]: (succeeds(Goal_state_67, Start_state_1) | ~follows(p3, Start_state_1) | ~follows(Goal_state_67, p8)))). % 13.35/5.84 tff(c_659, plain, (![Goal_state_63:state, Start_state_1:state]: (succeeds(Goal_state_63, Start_state_1) | ~follows(p6, Start_state_1) | ~succeeds(Goal_state_63, p3)))). % 13.35/5.84 tff(c_2123, plain, (![Goal_state_95:state, Start_state_1:state]: (succeeds(Goal_state_95, Start_state_1) | ~follows(p2, Start_state_1) | ~follows(Goal_state_95, p7)))). % 13.35/5.84 tff(c_985, plain, (![Goal_state_5:state, Goal_state_72:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, Goal_state_72) | ~follows(Goal_state_72, p5)))). % 13.35/5.84 tff(c_10051, plain, (~follows(p4, p5))). % 13.35/5.84 tff(c_639, plain, (![Goal_state_61:state, Start_state_1:state, Start_state_62:state]: (succeeds(Goal_state_61, Start_state_1) | ~follows(Start_state_62, Start_state_1) | ~follows(p1, Start_state_62) | ~follows(Goal_state_61, p2)))). % 13.35/5.84 tff(c_4734, plain, (![Goal_state_138:state, Goal_state_35:state]: (succeeds(Goal_state_138, p8) | ~follows(Goal_state_138, Goal_state_35) | ~follows(Goal_state_35, p5)))). % 13.35/5.84 tff(c_800, plain, (![Goal_state_5:state, Goal_state_67:state]: (succeeds(Goal_state_5, p3) | ~succeeds(Goal_state_5, Goal_state_67) | ~follows(Goal_state_67, p8)))). % 13.35/5.84 tff(c_2896, plain, (![Goal_state_5:state, Goal_state_110:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, Goal_state_110) | ~follows(Goal_state_110, p7)))). % 13.35/5.84 tff(c_1239, plain, (![Goal_state_5:state, Start_state_75:state]: (succeeds(Goal_state_5, Start_state_75) | ~succeeds(Goal_state_5, p4) | ~follows(p8, Start_state_75)))). % 13.35/5.84 tff(c_521, plain, (![Goal_state_58:state, Start_state_1:state]: (succeeds(Goal_state_58, Start_state_1) | ~follows(p1, Start_state_1) | ~follows(Goal_state_58, p6)))). % 13.35/5.84 tff(c_7142, plain, (![Start_state_1:state]: (succeeds(p8, Start_state_1) | ~follows(p2, Start_state_1)))). % 13.35/5.84 tff(c_7100, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p3) | ~succeeds(Goal_state_5, p8)))). % 13.35/5.84 tff(c_1748, plain, (![Goal_state_5:state, Start_state_90:state, Goal_state_89:state]: (succeeds(Goal_state_5, Start_state_90) | ~succeeds(Goal_state_5, Goal_state_89) | ~follows(p4, Start_state_90) | ~follows(Goal_state_89, p5)))). % 13.35/5.84 tff(c_7099, plain, (![Start_state_1:state]: (succeeds(p8, Start_state_1) | ~follows(p3, Start_state_1)))). % 13.35/5.84 tff(c_7038, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p1) | ~succeeds(Goal_state_5, p8)))). % 13.35/5.84 tff(c_7037, plain, (![Start_state_1:state]: (succeeds(p8, Start_state_1) | ~follows(p1, Start_state_1)))). % 13.35/5.84 tff(c_6998, plain, (![Start_state_1:state]: (succeeds(p8, Start_state_1) | ~follows(p6, Start_state_1)))). % 13.35/5.84 tff(c_7143, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p2) | ~succeeds(Goal_state_5, p8)))). % 13.35/5.84 tff(c_6999, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p6) | ~succeeds(Goal_state_5, p8)))). % 13.35/5.84 tff(c_6987, plain, (succeeds(p8, p2))). % 13.35/5.84 tff(c_6984, plain, (succeeds(p8, p3))). % 13.35/5.84 tff(c_7039, plain, (~follows(p4, p6))). % 13.35/5.84 tff(c_6983, plain, (succeeds(p8, p1))). % 13.35/5.84 tff(c_6941, plain, (succeeds(p8, p6))). % 13.35/5.84 tff(c_6624, plain, (succeeds(p8, p8))). % 13.35/5.84 tff(c_641, plain, (![Goal_state_5:state, Start_state_62:state, Goal_state_61:state]: (succeeds(Goal_state_5, Start_state_62) | ~succeeds(Goal_state_5, Goal_state_61) | ~follows(p1, Start_state_62) | ~follows(Goal_state_61, p2)))). % 13.35/5.84 tff(c_4735, plain, (![Goal_state_138:state, Goal_state_32:state]: (succeeds(Goal_state_138, p8) | ~follows(Goal_state_138, Goal_state_32) | ~follows(Goal_state_32, p6)))). % 13.35/5.84 tff(c_5258, plain, (![Start_state_1:state]: (succeeds(p7, Start_state_1) | ~follows(p2, Start_state_1)))). % 13.35/5.84 tff(c_5218, plain, (![Start_state_1:state]: (succeeds(p7, Start_state_1) | ~follows(p3, Start_state_1)))). % 13.35/5.84 tff(c_5161, plain, (![Start_state_1:state]: (succeeds(p7, Start_state_1) | ~follows(p1, Start_state_1)))). % 13.35/5.84 tff(c_5162, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p1) | ~succeeds(Goal_state_5, p7)))). % 13.35/5.84 tff(c_5219, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p3) | ~succeeds(Goal_state_5, p7)))). % 13.35/5.84 tff(c_5259, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p2) | ~succeeds(Goal_state_5, p7)))). % 13.35/5.84 tff(c_5125, plain, (![Start_state_1:state]: (succeeds(p7, Start_state_1) | ~follows(p6, Start_state_1)))). % 13.35/5.84 tff(c_5126, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p6) | ~succeeds(Goal_state_5, p7)))). % 13.35/5.84 tff(c_5075, plain, (![Start_state_1:state]: (succeeds(p7, Start_state_1) | ~follows(p8, Start_state_1)))). % 13.35/5.84 tff(c_5076, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, p7)))). % 13.35/5.84 tff(c_5262, plain, (~follows(p4, p3))). % 13.35/5.84 tff(c_5114, plain, (succeeds(p7, p2))). % 13.35/5.84 tff(c_5111, plain, (succeeds(p7, p3))). % 13.35/5.84 tff(c_5163, plain, (~follows(p7, p3))). % 13.35/5.84 tff(c_5110, plain, (succeeds(p7, p1))). % 13.35/5.84 tff(c_5071, plain, (succeeds(p7, p6))). % 13.35/5.84 tff(c_5020, plain, (succeeds(p7, p8))). % 13.35/5.84 tff(c_2352, plain, (![Goal_state_100:state, Start_state_1:state, Start_state_101:state]: (succeeds(Goal_state_100, Start_state_1) | ~follows(Start_state_101, Start_state_1) | ~follows(p2, Start_state_101) | ~follows(Goal_state_100, p3)))). % 13.35/5.84 tff(c_4740, plain, (![Goal_state_138:state, Goal_state_2:state]: (succeeds(Goal_state_138, p8) | ~follows(Goal_state_138, Goal_state_2) | ~follows(Goal_state_2, p3)))). % 13.35/5.84 tff(c_4995, plain, (![Start_state_28:state]: (~follows(Start_state_28, p8) | ~follows(p8, Start_state_28)))). % 13.35/5.84 tff(c_4992, plain, (![Start_state_28:state]: (~follows(Start_state_28, p8) | ~follows(p3, Start_state_28)))). % 13.35/5.84 tff(c_4427, 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)))). % 13.35/5.85 tff(c_378, 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)))). % 13.35/5.85 tff(c_4982, plain, (![Start_state_28:state]: (~follows(Start_state_28, p5) | ~follows(p3, Start_state_28)))). % 13.35/5.85 tff(c_4979, plain, (~follows(p7, p5))). % 13.35/5.85 tff(c_2021, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p2) | ~follows(Start_state_1, p3) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.85 tff(c_4974, plain, (~follows(p4, p8))). % 13.35/5.85 tff(c_4923, plain, (![Goal_state_148:state]: (succeeds(Goal_state_148, p6) | ~follows(Goal_state_148, p8)))). % 13.35/5.85 tff(c_587, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p6) | ~follows(Start_state_1, p7) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.85 tff(c_776, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p3) | ~follows(Start_state_1, p6) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.85 tff(c_4771, plain, (![Goal_state_140:state]: (succeeds(Goal_state_140, p6) | ~follows(Goal_state_140, p3)))). % 13.35/5.85 tff(c_4807, plain, (![Goal_state_141:state]: (succeeds(Goal_state_141, p6) | ~follows(Goal_state_141, p4)))). % 13.35/5.85 tff(c_436, 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)))). % 13.35/5.85 tff(c_4739, plain, (![Goal_state_138:state]: (succeeds(Goal_state_138, p8) | ~follows(Goal_state_138, p4)))). % 13.35/5.85 tff(c_4726, plain, (![Goal_state_138:state]: (succeeds(Goal_state_138, p8) | ~follows(Goal_state_138, p3)))). % 13.35/5.85 tff(c_883, 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)))). % 13.35/5.85 tff(c_1878, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p7) | ~follows(Start_state_1, p8) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.85 tff(c_1407, plain, (![Goal_state_80:state, Start_state_28:state]: (succeeds(Goal_state_80, Start_state_28) | ~follows(p8, Start_state_28) | ~follows(Goal_state_80, p7)))). % 13.35/5.85 tff(c_4514, plain, (~follows(p7, p7))). % 13.35/5.85 tff(c_956, plain, (![Goal_state_2:state, Start_state_71:state]: (succeeds(Goal_state_2, Start_state_71) | ~follows(p8, Start_state_71) | ~follows(Goal_state_2, p4)))). % 13.35/5.85 tff(c_189, plain, (![Goal_state_5:state, Goal_state_41:state]: (succeeds(Goal_state_5, p3) | ~succeeds(Goal_state_5, Goal_state_41) | ~follows(Goal_state_41, p5)))). % 13.35/5.85 tff(c_952, plain, (![Goal_state_35:state, Start_state_71:state]: (succeeds(Goal_state_35, Start_state_71) | ~follows(p8, Start_state_71) | ~follows(Goal_state_35, p5)))). % 13.35/5.85 tff(c_953, plain, (![Goal_state_32:state, Start_state_71:state]: (succeeds(Goal_state_32, Start_state_71) | ~follows(p8, Start_state_71) | ~follows(Goal_state_32, p6)))). % 13.35/5.85 tff(c_3987, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p8) | ~follows(Goal_state_32, p6)))). % 13.35/5.85 tff(c_958, plain, (![Goal_state_2:state, Start_state_71:state]: (succeeds(Goal_state_2, Start_state_71) | ~follows(p8, Start_state_71) | ~follows(Goal_state_2, p3)))). % 13.35/5.85 tff(c_505, plain, (![Goal_state_2:state, Start_state_1:state]: (succeeds(Goal_state_2, p1) | ~follows(Start_state_1, p2) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.85 tff(c_3172, plain, (![Start_state_1:state]: (succeeds(p6, Start_state_1) | ~follows(p2, Start_state_1)))). % 13.35/5.85 tff(c_2964, plain, (![Start_state_1:state]: (succeeds(p6, Start_state_1) | ~follows(p1, Start_state_1)))). % 13.35/5.85 tff(c_3131, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p3) | ~follows(Goal_state_32, p7)))). % 13.35/5.85 tff(c_3173, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p2) | ~succeeds(Goal_state_5, p6)))). % 13.35/5.85 tff(c_2965, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p1) | ~succeeds(Goal_state_5, p6)))). % 13.35/5.85 tff(c_2931, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, p6)))). % 13.35/5.85 tff(c_3337, plain, (![Start_state_28:state]: (~follows(Start_state_28, p5) | ~follows(p8, Start_state_28)))). % 13.35/5.85 tff(c_2862, plain, (![Start_state_1:state]: (succeeds(p6, Start_state_1) | ~follows(p3, Start_state_1)))). % 13.35/5.85 tff(c_2849, plain, (![Start_state_28:state]: (succeeds(p6, Start_state_28) | ~follows(p8, Start_state_28)))). % 13.35/5.85 tff(c_2988, plain, (succeeds(p6, p2))). % 13.35/5.85 tff(c_2863, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p3) | ~succeeds(Goal_state_5, p6)))). % 13.35/5.85 tff(c_2925, plain, (succeeds(p6, p6))). % 13.35/5.85 tff(c_2858, plain, (succeeds(p6, p1))). % 13.35/5.85 tff(c_2852, plain, (succeeds(p6, p8))). % 13.35/5.85 tff(c_2815, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p8) | ~follows(Goal_state_32, p7)))). % 13.35/5.85 tff(c_2816, plain, (succeeds(p6, p3))). % 13.35/5.85 tff(c_2754, plain, (~follows(p2, p7))). % 13.35/5.85 tff(c_2251, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p2) | ~follows(Goal_state_32, p6)))). % 13.35/5.85 tff(c_2242, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p2) | ~follows(Goal_state_32, p8)))). % 13.35/5.85 tff(c_181, plain, (![Goal_state_40:state, Start_state_1:state]: (succeeds(Goal_state_40, Start_state_1) | ~follows(p7, Start_state_1) | ~follows(Goal_state_40, p8)))). % 13.35/5.85 tff(c_2092, plain, (![Start_state_1:state]: (succeeds(p4, Start_state_1) | ~follows(p2, Start_state_1)))). % 13.35/5.85 tff(c_2256, plain, (![Goal_state_2:state]: (succeeds(Goal_state_2, p2) | ~follows(Goal_state_2, p4)))). % 13.35/5.85 tff(c_2093, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p2) | ~succeeds(Goal_state_5, p4)))). % 13.35/5.85 tff(c_2424, plain, (~follows(p2, p5))). % 13.35/5.85 tff(c_2056, plain, (![Start_state_1:state]: (succeeds(p3, Start_state_1) | ~follows(p2, Start_state_1)))). % 13.35/5.85 tff(c_167, plain, (![Goal_state_38:state, Start_state_1:state]: (succeeds(Goal_state_38, Start_state_1) | ~follows(p2, Start_state_1) | ~follows(Goal_state_38, p3)))). % 13.35/5.85 tff(c_1979, plain, (![Goal_state_72:state]: (succeeds(Goal_state_72, p2) | ~follows(Goal_state_72, p5)))). % 13.35/5.85 tff(c_2260, plain, (~follows(p2, p8))). % 13.35/5.85 tff(c_2057, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p2) | ~succeeds(Goal_state_5, p3)))). % 13.35/5.85 tff(c_2150, plain, (~follows(p6, p8))). % 13.35/5.85 tff(c_114, plain, (![Start_state_1:state, Start_state_31:state]: (succeeds(p3, Start_state_1) | ~follows(Start_state_31, Start_state_1) | ~follows(p8, Start_state_31)))). % 13.35/5.85 tff(c_2010, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p2) | ~follows(Goal_state_32, p7)))). % 13.35/5.85 tff(c_1987, plain, (succeeds(p4, p2))). % 13.35/5.85 tff(c_1999, plain, (succeeds(p3, p2))). % 13.35/5.85 tff(c_168, plain, (![Goal_state_5:state, Goal_state_38:state]: (succeeds(Goal_state_5, p2) | ~succeeds(Goal_state_5, Goal_state_38) | ~follows(Goal_state_38, p3)))). % 13.35/5.85 tff(c_1879, plain, (~follows(p8, p8))). % 13.35/5.85 tff(c_182, plain, (![Goal_state_5:state, Goal_state_40:state]: (succeeds(Goal_state_5, p7) | ~succeeds(Goal_state_5, Goal_state_40) | ~follows(Goal_state_40, p8)))). % 13.35/5.85 tff(c_145, plain, (![Goal_state_35:state, Start_state_1:state]: (succeeds(Goal_state_35, Start_state_1) | ~follows(p4, Start_state_1) | ~follows(Goal_state_35, p5)))). % 13.35/5.85 tff(c_233, plain, (![Goal_state_32:state, Start_state_45:state]: (succeeds(Goal_state_32, Start_state_45) | ~follows(p3, Start_state_45) | ~follows(Goal_state_32, p5)))). % 13.35/5.85 tff(c_1512, plain, (![Goal_state_39:state]: (succeeds(Goal_state_39, p1) | ~follows(Goal_state_39, p7)))). % 13.35/5.85 tff(c_1141, plain, (![Start_state_1:state]: (succeeds(p3, Start_state_1) | ~follows(p1, Start_state_1)))). % 13.35/5.85 tff(c_1538, plain, (![Goal_state_2:state]: (succeeds(Goal_state_2, p1) | ~follows(Goal_state_2, p3)))). % 13.35/5.85 tff(c_1142, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p1) | ~succeeds(Goal_state_5, p3)))). % 13.35/5.85 tff(c_1113, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p6) | ~succeeds(Goal_state_5, p4)))). % 13.35/5.85 tff(c_174, plain, (![Goal_state_39:state, Start_state_1:state]: (succeeds(Goal_state_39, Start_state_1) | ~follows(p6, Start_state_1) | ~follows(Goal_state_39, p7)))). % 13.35/5.85 tff(c_1112, plain, (![Start_state_1:state]: (succeeds(p4, Start_state_1) | ~follows(p6, Start_state_1)))). % 13.35/5.85 tff(c_980, plain, (![Goal_state_72:state]: (succeeds(Goal_state_72, p6) | ~follows(Goal_state_72, p5)))). % 13.35/5.85 tff(c_1050, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, p4)))). % 13.35/5.85 tff(c_796, plain, (![Goal_state_67:state]: (succeeds(Goal_state_67, p1) | ~follows(Goal_state_67, p8)))). % 13.35/5.85 tff(c_957, plain, (![Start_state_71:state]: (succeeds(p4, Start_state_71) | ~follows(p8, Start_state_71)))). % 13.35/5.85 tff(c_160, plain, (![Goal_state_37:state, Start_state_1:state]: (succeeds(Goal_state_37, Start_state_1) | ~follows(p3, Start_state_1) | ~follows(Goal_state_37, p6)))). % 13.35/5.85 tff(c_1079, plain, (succeeds(p3, p1))). % 13.35/5.85 tff(c_1043, plain, (succeeds(p4, p6))). % 13.35/5.85 tff(c_1020, plain, (succeeds(p3, p3))). % 13.35/5.85 tff(c_1019, plain, (succeeds(p4, p8))). % 13.35/5.85 tff(c_874, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p8) | ~follows(Goal_state_32, p5)))). % 13.35/5.85 tff(c_912, plain, (~follows(p1, p3))). % 13.35/5.85 tff(c_87, plain, (![Goal_state_5:state, Start_state_28:state]: (succeeds(Goal_state_5, Start_state_28) | ~follows(p8, Start_state_28) | ~succeeds(Goal_state_5, p3)))). % 13.35/5.85 tff(c_911, plain, (~follows(p1, p4))). % 13.35/5.85 tff(c_910, plain, (~follows(p1, p6))). % 13.35/5.85 tff(c_906, plain, (~follows(p1, p8))). % 13.35/5.85 tff(c_884, plain, (~succeeds(p1, p3))). % 13.35/5.85 tff(c_75, plain, (![Goal_state_5:state, Goal_state_26:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, Goal_state_26) | ~succeeds(Goal_state_26, p3)))). % 13.35/5.85 tff(c_801, plain, (~follows(p8, p6))). % 13.35/5.85 tff(c_762, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p3) | ~follows(Goal_state_32, p8)))). % 13.35/5.85 tff(c_161, plain, (![Goal_state_5:state, Goal_state_37:state]: (succeeds(Goal_state_5, p3) | ~succeeds(Goal_state_5, Goal_state_37) | ~follows(Goal_state_37, p6)))). % 13.35/5.85 tff(c_605, plain, (![Start_state_1:state]: (succeeds(p3, Start_state_1) | ~follows(p6, Start_state_1)))). % 13.35/5.85 tff(c_663, plain, (~follows(p6, p4))). % 13.35/5.85 tff(c_662, plain, (~follows(p6, p5))). % 13.35/5.85 tff(c_661, plain, (~follows(p8, p2))). % 13.35/5.85 tff(c_581, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p6) | ~succeeds(Goal_state_5, p3)))). % 13.35/5.85 tff(c_153, plain, (![Goal_state_36:state, Start_state_1:state]: (succeeds(Goal_state_36, Start_state_1) | ~follows(p1, Start_state_1) | ~follows(Goal_state_36, p2)))). % 13.35/5.85 tff(c_608, plain, (~follows(p1, p7))). % 13.35/5.85 tff(c_607, plain, (~follows(p8, p5))). % 13.35/5.85 tff(c_584, plain, (succeeds(p3, p6))). % 13.35/5.85 tff(c_175, plain, (![Goal_state_5:state, Goal_state_39:state]: (succeeds(Goal_state_5, p6) | ~succeeds(Goal_state_5, Goal_state_39) | ~follows(Goal_state_39, p7)))). % 13.35/5.85 tff(c_491, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p1) | ~follows(Goal_state_32, p6)))). % 13.35/5.85 tff(c_506, plain, (~follows(p1, p5))). % 13.35/5.85 tff(c_154, plain, (![Goal_state_5:state, Goal_state_36:state]: (succeeds(Goal_state_5, p1) | ~succeeds(Goal_state_5, Goal_state_36) | ~follows(Goal_state_36, p2)))). % 13.35/5.85 tff(c_147, plain, (![Goal_state_5:state, Goal_state_35:state]: (succeeds(Goal_state_5, p4) | ~succeeds(Goal_state_5, Goal_state_35) | ~follows(Goal_state_35, p5)))). % 13.35/5.85 tff(c_63, plain, (![Goal_state_5:state, Goal_state_24:state]: (succeeds(Goal_state_5, p3) | ~succeeds(Goal_state_5, Goal_state_24) | ~follows(Goal_state_24, p4)))). % 13.35/5.85 tff(c_236, plain, (![Goal_state_2:state, Start_state_45:state]: (succeeds(Goal_state_2, Start_state_45) | ~follows(p3, Start_state_45) | ~follows(Goal_state_2, p4)))). % 13.35/5.86 tff(c_254, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p1) | ~follows(Goal_state_32, p5)))). % 13.35/5.86 tff(c_216, plain, (![Start_state_1:state]: (succeeds(p4, Start_state_1) | ~follows(p1, Start_state_1)))). % 13.35/5.86 tff(c_258, plain, (![Goal_state_2:state]: (succeeds(Goal_state_2, p1) | ~follows(Goal_state_2, p4)))). % 13.35/5.86 tff(c_217, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p1) | ~succeeds(Goal_state_5, p4)))). % 13.35/5.86 tff(c_237, plain, (~follows(p3, p3))). % 13.35/5.86 tff(c_104, plain, (![Goal_state_5:state, Start_state_30:state]: (succeeds(Goal_state_5, Start_state_30) | ~succeeds(Goal_state_5, p4) | ~follows(p3, Start_state_30)))). % 13.35/5.86 tff(c_220, plain, (~follows(p3, p7))). % 13.35/5.86 tff(c_219, plain, (~follows(p3, p8))). % 13.35/5.86 tff(c_218, plain, (~follows(p3, p5))). % 13.35/5.86 tff(c_206, plain, (succeeds(p4, p1))). % 13.35/5.86 tff(c_101, plain, (![Start_state_1:state, Start_state_30:state]: (succeeds(p4, Start_state_1) | ~follows(Start_state_30, Start_state_1) | ~follows(p3, Start_state_30)))). % 13.35/5.86 tff(c_146, plain, (![Goal_state_35:state]: (succeeds(Goal_state_35, p3) | ~follows(Goal_state_35, p5)))). % 13.35/5.86 tff(c_136, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p7) | ~follows(Goal_state_32, p8)))). % 13.35/5.86 tff(c_135, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p6) | ~follows(Goal_state_32, p7)))). % 13.35/5.86 tff(c_134, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p2) | ~follows(Goal_state_32, p3)))). % 13.35/5.86 tff(c_133, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p3) | ~follows(Goal_state_32, p6)))). % 13.35/5.86 tff(c_132, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p1) | ~follows(Goal_state_32, p2)))). % 13.35/5.86 tff(c_131, plain, (![Goal_state_32:state]: (succeeds(Goal_state_32, p4) | ~follows(Goal_state_32, p5)))). % 13.35/5.86 tff(c_91, plain, (![Goal_state_2:state, Start_state_28:state, Start_state_1:state]: (succeeds(Goal_state_2, Start_state_28) | ~follows(Start_state_1, Start_state_28) | ~follows(Goal_state_2, Start_state_1)))). % 13.35/5.86 tff(c_117, plain, (~follows(p8, p4))). % 13.35/5.86 tff(c_88, plain, (![Start_state_28:state]: (succeeds(p3, Start_state_28) | ~follows(p8, Start_state_28)))). % 13.35/5.86 tff(c_90, plain, (![Start_state_28:state]: (succeeds(p4, Start_state_28) | ~follows(p3, Start_state_28)))). % 13.35/5.86 tff(c_49, 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)))). % 13.35/5.86 tff(c_71, plain, (![Goal_state_5:state]: (succeeds(Goal_state_5, p8) | ~succeeds(Goal_state_5, p3)))). % 13.35/5.86 tff(c_68, plain, (succeeds(p3, p8))). % 13.35/5.86 tff(c_59, plain, (![Start_state_22:state]: (succeeds(p3, Start_state_22) | ~has(Start_state_22, goto(loop))))). % 13.35/5.86 tff(c_55, plain, (![Goal_state_2:state]: (succeeds(Goal_state_2, p3) | ~follows(Goal_state_2, p4)))). % 13.35/5.86 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))))). % 13.35/5.86 tff(c_48, plain, (![Goal_state_17:state]: (succeeds(Goal_state_17, p3) | ~succeeds(Goal_state_17, p4)))). % 13.35/5.86 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)))). % 13.35/5.86 tff(c_42, plain, (succeeds(p4, p3))). % 13.35/5.86 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))))). % 13.35/5.86 tff(c_32, plain, (has(p7, assign(register_j, plus(register_j, n1))))). % 13.35/5.86 tff(c_28, plain, (has(p6, assign(register_k, times(n2, register_k))))). % 13.35/5.86 tff(c_20, plain, (has(p3, ifthen(equal_function(register_j, n), p4)))). % 13.35/5.86 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)))). % 13.35/5.86 tff(c_14, plain, (has(p2, assign(register_k, n1)))). % 13.35/5.86 tff(c_10, plain, (has(p1, assign(register_j, n0)))). % 13.35/5.86 tff(c_36, plain, (has(p8, goto(loop)))). % 13.35/5.86 tff(c_22, plain, (has(p4, goto(out)))). % 13.35/5.86 tff(c_24, plain, (follows(p5, p4))). % 13.35/5.86 tff(c_12, plain, (follows(p2, p1))). % 13.35/5.86 tff(c_26, plain, (follows(p6, p3))). % 13.35/5.86 tff(c_16, plain, (labels(loop, p3))). % 13.35/5.86 tff(c_18, plain, (follows(p3, p2))). % 13.35/5.86 tff(c_30, plain, (follows(p7, p6))). % 13.35/5.86 tff(c_34, plain, (follows(p8, p7))). % 13.35/5.86 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.35/5.86 %------------------------------------------------------------------------------