%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : GRA014+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n022.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 : 600s % DateTime : Sat Jul 16 07:15:33 EDT 2022 % Result : Theorem 8.13s 2.57s % Output : Proof 12.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : GRA014+1 : TPTP v8.1.0. Released v3.2.0. % 0.07/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.34 % Computer : n022.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 : 600 % 0.13/0.34 % DateTime : Tue May 31 03:55:22 EDT 2022 % 0.13/0.34 % CPUTime : % 0.20/0.59 ____ _ % 0.20/0.59 ___ / __ \_____(_)___ ________ __________ % 0.20/0.59 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.20/0.59 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.20/0.59 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.20/0.59 % 0.20/0.59 A Theorem Prover for First-Order Logic % 0.20/0.59 (ePrincess v.1.0) % 0.20/0.59 % 0.20/0.59 (c) Philipp Rümmer, 2009-2015 % 0.20/0.59 (c) Peter Backeman, 2014-2015 % 0.20/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.20/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.20/0.59 Bug reports to peter@backeman.se % 0.20/0.59 % 0.20/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.20/0.59 % 0.20/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.71/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.36/0.89 Prover 0: Preprocessing ... % 1.50/0.96 Prover 0: Constructing countermodel ... % 8.13/2.56 Prover 0: proved (1922ms) % 8.13/2.57 % 8.13/2.57 No countermodel exists, formula is valid % 8.13/2.57 % SZS status Theorem for theBenchmark % 8.13/2.57 % 8.13/2.57 Generating proof ... found it (size 853) % 11.94/3.45 % 11.94/3.45 % SZS output start Proof for theBenchmark % 11.94/3.45 Assumed formulas after preprocessing and simplification: % 11.94/3.45 | (0) less_than(n5, n6) & less_than(n4, n5) & less_than(n3, n4) & less_than(n2, n3) & less_than(n1, n2) & ~ goal & ! [v0] : ! [v1] : ! [v2] : ( ~ less_than(v1, v2) | ~ less_than(v0, v1) | less_than(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ green(v1, v2) | ~ green(v0, v2) | ~ green(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ red(v1, v2) | ~ red(v0, v2) | ~ red(v0, v1)) & ! [v0] : ! [v1] : ( ~ less_than(v0, v1) | green(v0, v1) | red(v0, v1)) % 11.94/3.46 | Applying alpha-rule on (0) yields: % 11.94/3.46 | (1) less_than(n4, n5) % 11.94/3.46 | (2) ! [v0] : ! [v1] : ! [v2] : ( ~ green(v1, v2) | ~ green(v0, v2) | ~ green(v0, v1)) % 11.94/3.46 | (3) ! [v0] : ! [v1] : ! [v2] : ( ~ less_than(v1, v2) | ~ less_than(v0, v1) | less_than(v0, v2)) % 11.94/3.46 | (4) less_than(n1, n2) % 11.94/3.46 | (5) less_than(n3, n4) % 11.94/3.46 | (6) less_than(n2, n3) % 11.94/3.46 | (7) ~ goal % 11.94/3.46 | (8) ! [v0] : ! [v1] : ( ~ less_than(v0, v1) | green(v0, v1) | red(v0, v1)) % 11.94/3.46 | (9) less_than(n5, n6) % 11.94/3.46 | (10) ! [v0] : ! [v1] : ! [v2] : ( ~ red(v1, v2) | ~ red(v0, v2) | ~ red(v0, v1)) % 11.94/3.46 | % 11.94/3.46 | Instantiating formula (8) with n6, n5 and discharging atoms less_than(n5, n6), yields: % 11.94/3.46 | (11) green(n5, n6) | red(n5, n6) % 11.94/3.46 | % 11.94/3.46 | Instantiating formula (3) with n6, n5, n4 and discharging atoms less_than(n5, n6), less_than(n4, n5), yields: % 11.94/3.46 | (12) less_than(n4, n6) % 11.94/3.46 | % 11.94/3.46 | Instantiating formula (8) with n5, n4 and discharging atoms less_than(n4, n5), yields: % 11.94/3.46 | (13) green(n4, n5) | red(n4, n5) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (3) with n5, n4, n3 and discharging atoms less_than(n4, n5), less_than(n3, n4), yields: % 11.94/3.47 | (14) less_than(n3, n5) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (8) with n4, n3 and discharging atoms less_than(n3, n4), yields: % 11.94/3.47 | (15) green(n3, n4) | red(n3, n4) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (3) with n4, n3, n2 and discharging atoms less_than(n3, n4), less_than(n2, n3), yields: % 11.94/3.47 | (16) less_than(n2, n4) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (8) with n3, n2 and discharging atoms less_than(n2, n3), yields: % 11.94/3.47 | (17) green(n2, n3) | red(n2, n3) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (3) with n3, n2, n1 and discharging atoms less_than(n2, n3), less_than(n1, n2), yields: % 11.94/3.47 | (18) less_than(n1, n3) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (8) with n2, n1 and discharging atoms less_than(n1, n2), yields: % 11.94/3.47 | (19) green(n1, n2) | red(n1, n2) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (8) with n6, n4 and discharging atoms less_than(n4, n6), yields: % 11.94/3.47 | (20) green(n4, n6) | red(n4, n6) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (3) with n6, n5, n3 and discharging atoms less_than(n5, n6), less_than(n3, n5), yields: % 11.94/3.47 | (21) less_than(n3, n6) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (8) with n5, n3 and discharging atoms less_than(n3, n5), yields: % 11.94/3.47 | (22) green(n3, n5) | red(n3, n5) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (3) with n5, n4, n2 and discharging atoms less_than(n4, n5), less_than(n2, n4), yields: % 11.94/3.47 | (23) less_than(n2, n5) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (3) with n6, n4, n2 and discharging atoms less_than(n4, n6), less_than(n2, n4), yields: % 11.94/3.47 | (24) less_than(n2, n6) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (8) with n4, n2 and discharging atoms less_than(n2, n4), yields: % 11.94/3.47 | (25) green(n2, n4) | red(n2, n4) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (3) with n4, n3, n1 and discharging atoms less_than(n3, n4), less_than(n1, n3), yields: % 11.94/3.47 | (26) less_than(n1, n4) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (3) with n5, n3, n1 and discharging atoms less_than(n3, n5), less_than(n1, n3), yields: % 11.94/3.47 | (27) less_than(n1, n5) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (8) with n3, n1 and discharging atoms less_than(n1, n3), yields: % 11.94/3.47 | (28) green(n1, n3) | red(n1, n3) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (8) with n6, n3 and discharging atoms less_than(n3, n6), yields: % 11.94/3.47 | (29) green(n3, n6) | red(n3, n6) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (8) with n6, n2 and discharging atoms less_than(n2, n6), yields: % 11.94/3.47 | (30) green(n2, n6) | red(n2, n6) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (8) with n5, n2 and discharging atoms less_than(n2, n5), yields: % 11.94/3.47 | (31) green(n2, n5) | red(n2, n5) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (8) with n5, n1 and discharging atoms less_than(n1, n5), yields: % 11.94/3.47 | (32) green(n1, n5) | red(n1, n5) % 11.94/3.47 | % 11.94/3.47 | Instantiating formula (3) with n6, n4, n1 and discharging atoms less_than(n4, n6), less_than(n1, n4), yields: % 11.94/3.48 | (33) less_than(n1, n6) % 11.94/3.48 | % 11.94/3.48 | Instantiating formula (8) with n4, n1 and discharging atoms less_than(n1, n4), yields: % 11.94/3.48 | (34) green(n1, n4) | red(n1, n4) % 11.94/3.48 | % 11.94/3.48 | Instantiating formula (8) with n6, n1 and discharging atoms less_than(n1, n6), yields: % 11.94/3.48 | (35) green(n1, n6) | red(n1, n6) % 11.94/3.48 | % 11.94/3.48 +-Applying beta-rule and splitting (15), into two cases. % 11.94/3.48 |-Branch one: % 11.94/3.48 | (36) green(n3, n4) % 11.94/3.48 | % 11.94/3.48 +-Applying beta-rule and splitting (19), into two cases. % 11.94/3.48 |-Branch one: % 11.94/3.48 | (37) green(n1, n2) % 11.94/3.48 | % 11.94/3.48 +-Applying beta-rule and splitting (17), into two cases. % 11.94/3.48 |-Branch one: % 11.94/3.48 | (38) green(n2, n3) % 11.94/3.48 | % 11.94/3.48 +-Applying beta-rule and splitting (11), into two cases. % 11.94/3.48 |-Branch one: % 11.94/3.48 | (39) green(n5, n6) % 11.94/3.48 | % 11.94/3.48 +-Applying beta-rule and splitting (13), into two cases. % 11.94/3.48 |-Branch one: % 11.94/3.48 | (40) green(n4, n5) % 11.94/3.48 | % 11.94/3.48 +-Applying beta-rule and splitting (25), into two cases. % 11.94/3.48 |-Branch one: % 11.94/3.48 | (41) green(n2, n4) % 11.94/3.48 | % 11.94/3.48 | Instantiating formula (2) with n4, n3, n2 and discharging atoms green(n3, n4), green(n2, n4), green(n2, n3), yields: % 11.94/3.48 | (42) $false % 11.94/3.48 | % 11.94/3.48 |-The branch is then unsatisfiable % 11.94/3.48 |-Branch two: % 11.94/3.48 | (43) ~ green(n2, n4) % 11.94/3.48 | (44) red(n2, n4) % 11.94/3.48 | % 11.94/3.48 +-Applying beta-rule and splitting (20), into two cases. % 11.94/3.48 |-Branch one: % 11.94/3.48 | (45) green(n4, n6) % 11.94/3.48 | % 11.94/3.48 | Instantiating formula (2) with n6, n5, n4 and discharging atoms green(n5, n6), green(n4, n6), green(n4, n5), yields: % 11.94/3.48 | (42) $false % 11.94/3.48 | % 11.94/3.48 |-The branch is then unsatisfiable % 11.94/3.48 |-Branch two: % 11.94/3.48 | (47) ~ green(n4, n6) % 11.94/3.48 | (48) red(n4, n6) % 11.94/3.48 | % 11.94/3.48 +-Applying beta-rule and splitting (28), into two cases. % 11.94/3.48 |-Branch one: % 11.94/3.48 | (49) green(n1, n3) % 11.94/3.48 | % 11.94/3.48 | Instantiating formula (2) with n3, n2, n1 and discharging atoms green(n2, n3), green(n1, n3), green(n1, n2), yields: % 11.94/3.48 | (42) $false % 11.94/3.48 | % 11.94/3.48 |-The branch is then unsatisfiable % 11.94/3.48 |-Branch two: % 11.94/3.48 | (51) ~ green(n1, n3) % 11.94/3.48 | (52) red(n1, n3) % 11.94/3.48 | % 11.94/3.48 +-Applying beta-rule and splitting (29), into two cases. % 11.94/3.48 |-Branch one: % 11.94/3.48 | (53) green(n3, n6) % 11.94/3.48 | % 11.94/3.48 +-Applying beta-rule and splitting (30), into two cases. % 11.94/3.48 |-Branch one: % 11.94/3.48 | (54) green(n2, n6) % 11.94/3.48 | % 11.94/3.48 | Instantiating formula (2) with n6, n3, n2 and discharging atoms green(n3, n6), green(n2, n6), green(n2, n3), yields: % 11.94/3.48 | (42) $false % 11.94/3.48 | % 11.94/3.48 |-The branch is then unsatisfiable % 11.94/3.48 |-Branch two: % 11.94/3.48 | (56) ~ green(n2, n6) % 11.94/3.48 | (57) red(n2, n6) % 11.94/3.48 | % 11.94/3.48 | Instantiating formula (10) with n6, n4, n2 and discharging atoms red(n4, n6), red(n2, n6), red(n2, n4), yields: % 11.94/3.48 | (42) $false % 11.94/3.48 | % 11.94/3.48 |-The branch is then unsatisfiable % 11.94/3.48 |-Branch two: % 11.94/3.48 | (59) ~ green(n3, n6) % 11.94/3.48 | (60) red(n3, n6) % 11.94/3.48 | % 11.94/3.48 +-Applying beta-rule and splitting (30), into two cases. % 11.94/3.48 |-Branch one: % 11.94/3.48 | (54) green(n2, n6) % 11.94/3.48 | % 11.94/3.48 +-Applying beta-rule and splitting (35), into two cases. % 11.94/3.48 |-Branch one: % 11.94/3.48 | (62) green(n1, n6) % 11.94/3.48 | % 11.94/3.48 | Instantiating formula (2) with n6, n2, n1 and discharging atoms green(n2, n6), green(n1, n6), green(n1, n2), yields: % 11.94/3.48 | (42) $false % 11.94/3.48 | % 11.94/3.48 |-The branch is then unsatisfiable % 11.94/3.48 |-Branch two: % 11.94/3.48 | (64) ~ green(n1, n6) % 11.94/3.48 | (65) red(n1, n6) % 11.94/3.48 | % 11.94/3.48 | Instantiating formula (10) with n6, n3, n1 and discharging atoms red(n3, n6), red(n1, n6), red(n1, n3), yields: % 11.94/3.48 | (42) $false % 11.94/3.48 | % 11.94/3.48 |-The branch is then unsatisfiable % 11.94/3.48 |-Branch two: % 11.94/3.48 | (56) ~ green(n2, n6) % 11.94/3.48 | (57) red(n2, n6) % 11.94/3.48 | % 11.94/3.48 | Instantiating formula (10) with n6, n4, n2 and discharging atoms red(n4, n6), red(n2, n6), red(n2, n4), yields: % 11.94/3.49 | (42) $false % 11.94/3.49 | % 11.94/3.49 |-The branch is then unsatisfiable % 11.94/3.49 |-Branch two: % 11.94/3.49 | (70) ~ green(n4, n5) % 11.94/3.49 | (71) red(n4, n5) % 11.94/3.49 | % 11.94/3.49 +-Applying beta-rule and splitting (25), into two cases. % 11.94/3.49 |-Branch one: % 11.94/3.49 | (41) green(n2, n4) % 11.94/3.49 | % 11.94/3.49 | Instantiating formula (2) with n4, n3, n2 and discharging atoms green(n3, n4), green(n2, n4), green(n2, n3), yields: % 11.94/3.49 | (42) $false % 11.94/3.49 | % 11.94/3.49 |-The branch is then unsatisfiable % 11.94/3.49 |-Branch two: % 11.94/3.49 | (43) ~ green(n2, n4) % 11.94/3.49 | (44) red(n2, n4) % 11.94/3.49 | % 11.94/3.49 +-Applying beta-rule and splitting (22), into two cases. % 11.94/3.49 |-Branch one: % 11.94/3.49 | (76) green(n3, n5) % 11.94/3.49 | % 11.94/3.49 +-Applying beta-rule and splitting (31), into two cases. % 11.94/3.49 |-Branch one: % 11.94/3.49 | (77) green(n2, n5) % 12.33/3.49 | % 12.33/3.49 | Instantiating formula (2) with n5, n3, n2 and discharging atoms green(n3, n5), green(n2, n5), green(n2, n3), yields: % 12.33/3.49 | (42) $false % 12.33/3.49 | % 12.33/3.49 |-The branch is then unsatisfiable % 12.33/3.49 |-Branch two: % 12.33/3.49 | (79) ~ green(n2, n5) % 12.33/3.49 | (80) red(n2, n5) % 12.33/3.49 | % 12.33/3.49 | Instantiating formula (10) with n5, n4, n2 and discharging atoms red(n4, n5), red(n2, n5), red(n2, n4), yields: % 12.33/3.49 | (42) $false % 12.33/3.49 | % 12.33/3.49 |-The branch is then unsatisfiable % 12.33/3.49 |-Branch two: % 12.33/3.49 | (82) ~ green(n3, n5) % 12.33/3.49 | (83) red(n3, n5) % 12.33/3.49 | % 12.33/3.49 +-Applying beta-rule and splitting (28), into two cases. % 12.33/3.49 |-Branch one: % 12.33/3.49 | (49) green(n1, n3) % 12.33/3.49 | % 12.33/3.49 | Instantiating formula (2) with n3, n2, n1 and discharging atoms green(n2, n3), green(n1, n3), green(n1, n2), yields: % 12.33/3.49 | (42) $false % 12.33/3.49 | % 12.33/3.49 |-The branch is then unsatisfiable % 12.33/3.49 |-Branch two: % 12.33/3.49 | (51) ~ green(n1, n3) % 12.33/3.49 | (52) red(n1, n3) % 12.33/3.49 | % 12.33/3.49 +-Applying beta-rule and splitting (32), into two cases. % 12.33/3.49 |-Branch one: % 12.33/3.49 | (88) green(n1, n5) % 12.33/3.49 | % 12.33/3.49 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.49 |-Branch one: % 12.33/3.49 | (77) green(n2, n5) % 12.33/3.49 | % 12.33/3.49 | Instantiating formula (2) with n5, n2, n1 and discharging atoms green(n2, n5), green(n1, n5), green(n1, n2), yields: % 12.33/3.49 | (42) $false % 12.33/3.49 | % 12.33/3.49 |-The branch is then unsatisfiable % 12.33/3.49 |-Branch two: % 12.33/3.49 | (79) ~ green(n2, n5) % 12.33/3.49 | (80) red(n2, n5) % 12.33/3.49 | % 12.33/3.49 | Instantiating formula (10) with n5, n4, n2 and discharging atoms red(n4, n5), red(n2, n5), red(n2, n4), yields: % 12.33/3.49 | (42) $false % 12.33/3.49 | % 12.33/3.49 |-The branch is then unsatisfiable % 12.33/3.49 |-Branch two: % 12.33/3.49 | (94) ~ green(n1, n5) % 12.33/3.49 | (95) red(n1, n5) % 12.33/3.49 | % 12.33/3.49 | Instantiating formula (10) with n5, n3, n1 and discharging atoms red(n3, n5), red(n1, n5), red(n1, n3), yields: % 12.33/3.49 | (42) $false % 12.33/3.49 | % 12.33/3.49 |-The branch is then unsatisfiable % 12.33/3.49 |-Branch two: % 12.33/3.49 | (97) ~ green(n5, n6) % 12.33/3.49 | (98) red(n5, n6) % 12.33/3.49 | % 12.33/3.49 +-Applying beta-rule and splitting (13), into two cases. % 12.33/3.49 |-Branch one: % 12.33/3.49 | (40) green(n4, n5) % 12.33/3.49 | % 12.33/3.49 +-Applying beta-rule and splitting (25), into two cases. % 12.33/3.49 |-Branch one: % 12.33/3.49 | (41) green(n2, n4) % 12.33/3.49 | % 12.33/3.49 | Instantiating formula (2) with n4, n3, n2 and discharging atoms green(n3, n4), green(n2, n4), green(n2, n3), yields: % 12.33/3.49 | (42) $false % 12.33/3.49 | % 12.33/3.49 |-The branch is then unsatisfiable % 12.33/3.49 |-Branch two: % 12.33/3.49 | (43) ~ green(n2, n4) % 12.33/3.49 | (44) red(n2, n4) % 12.33/3.49 | % 12.33/3.49 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.49 |-Branch one: % 12.33/3.49 | (76) green(n3, n5) % 12.33/3.49 | % 12.33/3.49 | Instantiating formula (2) with n5, n4, n3 and discharging atoms green(n4, n5), green(n3, n5), green(n3, n4), yields: % 12.33/3.49 | (42) $false % 12.33/3.49 | % 12.33/3.49 |-The branch is then unsatisfiable % 12.33/3.49 |-Branch two: % 12.33/3.49 | (82) ~ green(n3, n5) % 12.33/3.49 | (83) red(n3, n5) % 12.33/3.49 | % 12.33/3.49 +-Applying beta-rule and splitting (20), into two cases. % 12.33/3.49 |-Branch one: % 12.33/3.49 | (45) green(n4, n6) % 12.33/3.49 | % 12.33/3.49 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.49 |-Branch one: % 12.33/3.49 | (53) green(n3, n6) % 12.33/3.49 | % 12.33/3.49 | Instantiating formula (2) with n6, n4, n3 and discharging atoms green(n4, n6), green(n3, n6), green(n3, n4), yields: % 12.33/3.49 | (42) $false % 12.33/3.49 | % 12.33/3.49 |-The branch is then unsatisfiable % 12.33/3.49 |-Branch two: % 12.33/3.49 | (59) ~ green(n3, n6) % 12.33/3.49 | (60) red(n3, n6) % 12.33/3.49 | % 12.33/3.49 | Instantiating formula (10) with n6, n5, n3 and discharging atoms red(n5, n6), red(n3, n6), red(n3, n5), yields: % 12.33/3.49 | (42) $false % 12.33/3.49 | % 12.33/3.49 |-The branch is then unsatisfiable % 12.33/3.49 |-Branch two: % 12.33/3.49 | (47) ~ green(n4, n6) % 12.33/3.49 | (48) red(n4, n6) % 12.33/3.49 | % 12.33/3.49 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.49 |-Branch one: % 12.33/3.49 | (53) green(n3, n6) % 12.33/3.49 | % 12.33/3.49 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.49 |-Branch one: % 12.33/3.49 | (54) green(n2, n6) % 12.33/3.49 | % 12.33/3.49 | Instantiating formula (2) with n6, n3, n2 and discharging atoms green(n3, n6), green(n2, n6), green(n2, n3), yields: % 12.33/3.50 | (42) $false % 12.33/3.50 | % 12.33/3.50 |-The branch is then unsatisfiable % 12.33/3.50 |-Branch two: % 12.33/3.50 | (56) ~ green(n2, n6) % 12.33/3.50 | (57) red(n2, n6) % 12.33/3.50 | % 12.33/3.50 | Instantiating formula (10) with n6, n4, n2 and discharging atoms red(n4, n6), red(n2, n6), red(n2, n4), yields: % 12.33/3.50 | (42) $false % 12.33/3.50 | % 12.33/3.50 |-The branch is then unsatisfiable % 12.33/3.50 |-Branch two: % 12.33/3.50 | (59) ~ green(n3, n6) % 12.33/3.50 | (60) red(n3, n6) % 12.33/3.50 | % 12.33/3.50 | Instantiating formula (10) with n6, n5, n3 and discharging atoms red(n5, n6), red(n3, n6), red(n3, n5), yields: % 12.33/3.50 | (42) $false % 12.33/3.50 | % 12.33/3.50 |-The branch is then unsatisfiable % 12.33/3.50 |-Branch two: % 12.33/3.50 | (70) ~ green(n4, n5) % 12.33/3.50 | (71) red(n4, n5) % 12.33/3.50 | % 12.33/3.50 +-Applying beta-rule and splitting (25), into two cases. % 12.33/3.50 |-Branch one: % 12.33/3.50 | (41) green(n2, n4) % 12.33/3.50 | % 12.33/3.50 | Instantiating formula (2) with n4, n3, n2 and discharging atoms green(n3, n4), green(n2, n4), green(n2, n3), yields: % 12.33/3.50 | (42) $false % 12.33/3.50 | % 12.33/3.50 |-The branch is then unsatisfiable % 12.33/3.50 |-Branch two: % 12.33/3.50 | (43) ~ green(n2, n4) % 12.33/3.50 | (44) red(n2, n4) % 12.33/3.50 | % 12.33/3.50 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.50 |-Branch one: % 12.33/3.50 | (76) green(n3, n5) % 12.33/3.50 | % 12.33/3.50 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.50 |-Branch one: % 12.33/3.50 | (77) green(n2, n5) % 12.33/3.50 | % 12.33/3.50 | Instantiating formula (2) with n5, n3, n2 and discharging atoms green(n3, n5), green(n2, n5), green(n2, n3), yields: % 12.33/3.50 | (42) $false % 12.33/3.50 | % 12.33/3.50 |-The branch is then unsatisfiable % 12.33/3.50 |-Branch two: % 12.33/3.50 | (79) ~ green(n2, n5) % 12.33/3.50 | (80) red(n2, n5) % 12.33/3.50 | % 12.33/3.50 | Instantiating formula (10) with n5, n4, n2 and discharging atoms red(n4, n5), red(n2, n5), red(n2, n4), yields: % 12.33/3.50 | (42) $false % 12.33/3.50 | % 12.33/3.50 |-The branch is then unsatisfiable % 12.33/3.50 |-Branch two: % 12.33/3.50 | (82) ~ green(n3, n5) % 12.33/3.50 | (83) red(n3, n5) % 12.33/3.50 | % 12.33/3.50 +-Applying beta-rule and splitting (20), into two cases. % 12.33/3.50 |-Branch one: % 12.33/3.50 | (45) green(n4, n6) % 12.33/3.50 | % 12.33/3.50 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.50 |-Branch one: % 12.33/3.50 | (53) green(n3, n6) % 12.33/3.50 | % 12.33/3.50 | Instantiating formula (2) with n6, n4, n3 and discharging atoms green(n4, n6), green(n3, n6), green(n3, n4), yields: % 12.33/3.50 | (42) $false % 12.33/3.50 | % 12.33/3.50 |-The branch is then unsatisfiable % 12.33/3.50 |-Branch two: % 12.33/3.50 | (59) ~ green(n3, n6) % 12.33/3.50 | (60) red(n3, n6) % 12.33/3.50 | % 12.33/3.50 | Instantiating formula (10) with n6, n5, n3 and discharging atoms red(n5, n6), red(n3, n6), red(n3, n5), yields: % 12.33/3.50 | (42) $false % 12.33/3.50 | % 12.33/3.50 |-The branch is then unsatisfiable % 12.33/3.50 |-Branch two: % 12.33/3.50 | (47) ~ green(n4, n6) % 12.33/3.50 | (48) red(n4, n6) % 12.33/3.50 | % 12.33/3.50 | Instantiating formula (10) with n6, n5, n4 and discharging atoms red(n5, n6), red(n4, n6), red(n4, n5), yields: % 12.33/3.50 | (42) $false % 12.33/3.50 | % 12.33/3.50 |-The branch is then unsatisfiable % 12.33/3.50 |-Branch two: % 12.33/3.50 | (148) ~ green(n2, n3) % 12.33/3.50 | (149) red(n2, n3) % 12.33/3.50 | % 12.33/3.50 +-Applying beta-rule and splitting (11), into two cases. % 12.33/3.50 |-Branch one: % 12.33/3.50 | (39) green(n5, n6) % 12.33/3.50 | % 12.33/3.50 +-Applying beta-rule and splitting (13), into two cases. % 12.33/3.50 |-Branch one: % 12.33/3.50 | (40) green(n4, n5) % 12.33/3.50 | % 12.33/3.50 +-Applying beta-rule and splitting (25), into two cases. % 12.33/3.50 |-Branch one: % 12.33/3.50 | (41) green(n2, n4) % 12.33/3.50 | % 12.33/3.50 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.50 |-Branch one: % 12.33/3.50 | (76) green(n3, n5) % 12.33/3.50 | % 12.33/3.50 | Instantiating formula (2) with n5, n4, n3 and discharging atoms green(n4, n5), green(n3, n5), green(n3, n4), yields: % 12.33/3.50 | (42) $false % 12.33/3.50 | % 12.33/3.50 |-The branch is then unsatisfiable % 12.33/3.50 |-Branch two: % 12.33/3.50 | (82) ~ green(n3, n5) % 12.33/3.50 | (83) red(n3, n5) % 12.33/3.50 | % 12.33/3.50 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.50 |-Branch one: % 12.33/3.50 | (77) green(n2, n5) % 12.33/3.50 | % 12.33/3.50 | Instantiating formula (2) with n5, n4, n2 and discharging atoms green(n4, n5), green(n2, n5), green(n2, n4), yields: % 12.33/3.50 | (42) $false % 12.33/3.50 | % 12.33/3.50 |-The branch is then unsatisfiable % 12.33/3.50 |-Branch two: % 12.33/3.50 | (79) ~ green(n2, n5) % 12.33/3.50 | (80) red(n2, n5) % 12.33/3.50 | % 12.33/3.50 | Instantiating formula (10) with n5, n3, n2 and discharging atoms red(n3, n5), red(n2, n5), red(n2, n3), yields: % 12.33/3.50 | (42) $false % 12.33/3.50 | % 12.33/3.50 |-The branch is then unsatisfiable % 12.33/3.50 |-Branch two: % 12.33/3.50 | (43) ~ green(n2, n4) % 12.33/3.50 | (44) red(n2, n4) % 12.33/3.50 | % 12.33/3.50 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.50 |-Branch one: % 12.33/3.50 | (76) green(n3, n5) % 12.33/3.50 | % 12.33/3.50 | Instantiating formula (2) with n5, n4, n3 and discharging atoms green(n4, n5), green(n3, n5), green(n3, n4), yields: % 12.33/3.50 | (42) $false % 12.33/3.50 | % 12.33/3.50 |-The branch is then unsatisfiable % 12.33/3.50 |-Branch two: % 12.33/3.50 | (82) ~ green(n3, n5) % 12.33/3.50 | (83) red(n3, n5) % 12.33/3.50 | % 12.33/3.50 +-Applying beta-rule and splitting (20), into two cases. % 12.33/3.50 |-Branch one: % 12.33/3.50 | (45) green(n4, n6) % 12.33/3.50 | % 12.33/3.50 | Instantiating formula (2) with n6, n5, n4 and discharging atoms green(n5, n6), green(n4, n6), green(n4, n5), yields: % 12.33/3.51 | (42) $false % 12.33/3.51 | % 12.33/3.51 |-The branch is then unsatisfiable % 12.33/3.51 |-Branch two: % 12.33/3.51 | (47) ~ green(n4, n6) % 12.33/3.51 | (48) red(n4, n6) % 12.33/3.51 | % 12.33/3.51 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.51 |-Branch one: % 12.33/3.51 | (54) green(n2, n6) % 12.33/3.51 | % 12.33/3.51 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.51 |-Branch one: % 12.33/3.51 | (77) green(n2, n5) % 12.33/3.51 | % 12.33/3.51 | Instantiating formula (2) with n6, n5, n2 and discharging atoms green(n5, n6), green(n2, n6), green(n2, n5), yields: % 12.33/3.51 | (42) $false % 12.33/3.51 | % 12.33/3.51 |-The branch is then unsatisfiable % 12.33/3.51 |-Branch two: % 12.33/3.51 | (79) ~ green(n2, n5) % 12.33/3.51 | (80) red(n2, n5) % 12.33/3.51 | % 12.33/3.51 | Instantiating formula (10) with n5, n3, n2 and discharging atoms red(n3, n5), red(n2, n5), red(n2, n3), yields: % 12.33/3.51 | (42) $false % 12.33/3.51 | % 12.33/3.51 |-The branch is then unsatisfiable % 12.33/3.51 |-Branch two: % 12.33/3.51 | (56) ~ green(n2, n6) % 12.33/3.51 | (57) red(n2, n6) % 12.33/3.51 | % 12.33/3.51 | Instantiating formula (10) with n6, n4, n2 and discharging atoms red(n4, n6), red(n2, n6), red(n2, n4), yields: % 12.33/3.51 | (42) $false % 12.33/3.51 | % 12.33/3.51 |-The branch is then unsatisfiable % 12.33/3.51 |-Branch two: % 12.33/3.51 | (70) ~ green(n4, n5) % 12.33/3.51 | (71) red(n4, n5) % 12.33/3.51 | % 12.33/3.51 +-Applying beta-rule and splitting (25), into two cases. % 12.33/3.51 |-Branch one: % 12.33/3.51 | (41) green(n2, n4) % 12.33/3.51 | % 12.33/3.51 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.51 |-Branch one: % 12.33/3.51 | (76) green(n3, n5) % 12.33/3.51 | % 12.33/3.51 +-Applying beta-rule and splitting (28), into two cases. % 12.33/3.51 |-Branch one: % 12.33/3.51 | (49) green(n1, n3) % 12.33/3.51 | % 12.33/3.51 +-Applying beta-rule and splitting (32), into two cases. % 12.33/3.51 |-Branch one: % 12.33/3.51 | (88) green(n1, n5) % 12.33/3.51 | % 12.33/3.51 | Instantiating formula (2) with n5, n3, n1 and discharging atoms green(n3, n5), green(n1, n5), green(n1, n3), yields: % 12.33/3.51 | (42) $false % 12.33/3.51 | % 12.33/3.51 |-The branch is then unsatisfiable % 12.33/3.51 |-Branch two: % 12.33/3.51 | (94) ~ green(n1, n5) % 12.33/3.51 | (95) red(n1, n5) % 12.33/3.51 | % 12.33/3.51 +-Applying beta-rule and splitting (34), into two cases. % 12.33/3.51 |-Branch one: % 12.33/3.51 | (190) green(n1, n4) % 12.33/3.51 | % 12.33/3.51 | Instantiating formula (2) with n4, n2, n1 and discharging atoms green(n2, n4), green(n1, n4), green(n1, n2), yields: % 12.33/3.51 | (42) $false % 12.33/3.51 | % 12.33/3.51 |-The branch is then unsatisfiable % 12.33/3.51 |-Branch two: % 12.33/3.51 | (192) ~ green(n1, n4) % 12.33/3.51 | (193) red(n1, n4) % 12.33/3.51 | % 12.33/3.51 | Instantiating formula (10) with n5, n4, n1 and discharging atoms red(n4, n5), red(n1, n5), red(n1, n4), yields: % 12.33/3.51 | (42) $false % 12.33/3.51 | % 12.33/3.51 |-The branch is then unsatisfiable % 12.33/3.51 |-Branch two: % 12.33/3.51 | (51) ~ green(n1, n3) % 12.33/3.51 | (52) red(n1, n3) % 12.33/3.51 | % 12.33/3.51 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.51 |-Branch one: % 12.33/3.51 | (53) green(n3, n6) % 12.33/3.51 | % 12.33/3.51 | Instantiating formula (2) with n6, n5, n3 and discharging atoms green(n5, n6), green(n3, n6), green(n3, n5), yields: % 12.33/3.51 | (42) $false % 12.33/3.51 | % 12.33/3.51 |-The branch is then unsatisfiable % 12.33/3.51 |-Branch two: % 12.33/3.51 | (59) ~ green(n3, n6) % 12.33/3.51 | (60) red(n3, n6) % 12.33/3.51 | % 12.33/3.51 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.51 |-Branch one: % 12.33/3.51 | (54) green(n2, n6) % 12.33/3.51 | % 12.33/3.51 +-Applying beta-rule and splitting (35), into two cases. % 12.33/3.51 |-Branch one: % 12.33/3.51 | (62) green(n1, n6) % 12.33/3.51 | % 12.33/3.51 | Instantiating formula (2) with n6, n2, n1 and discharging atoms green(n2, n6), green(n1, n6), green(n1, n2), yields: % 12.33/3.51 | (42) $false % 12.33/3.51 | % 12.33/3.51 |-The branch is then unsatisfiable % 12.33/3.51 |-Branch two: % 12.33/3.51 | (64) ~ green(n1, n6) % 12.33/3.51 | (65) red(n1, n6) % 12.33/3.51 | % 12.33/3.51 | Instantiating formula (10) with n6, n3, n1 and discharging atoms red(n3, n6), red(n1, n6), red(n1, n3), yields: % 12.33/3.51 | (42) $false % 12.33/3.51 | % 12.33/3.51 |-The branch is then unsatisfiable % 12.33/3.51 |-Branch two: % 12.33/3.51 | (56) ~ green(n2, n6) % 12.33/3.51 | (57) red(n2, n6) % 12.33/3.51 | % 12.33/3.51 | Instantiating formula (10) with n6, n3, n2 and discharging atoms red(n3, n6), red(n2, n6), red(n2, n3), yields: % 12.33/3.51 | (42) $false % 12.33/3.51 | % 12.33/3.51 |-The branch is then unsatisfiable % 12.33/3.51 |-Branch two: % 12.33/3.51 | (82) ~ green(n3, n5) % 12.33/3.51 | (83) red(n3, n5) % 12.33/3.51 | % 12.33/3.51 +-Applying beta-rule and splitting (32), into two cases. % 12.33/3.51 |-Branch one: % 12.33/3.51 | (88) green(n1, n5) % 12.33/3.51 | % 12.33/3.51 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.51 |-Branch one: % 12.33/3.51 | (77) green(n2, n5) % 12.33/3.51 | % 12.33/3.51 | Instantiating formula (2) with n5, n2, n1 and discharging atoms green(n2, n5), green(n1, n5), green(n1, n2), yields: % 12.33/3.51 | (42) $false % 12.33/3.51 | % 12.33/3.51 |-The branch is then unsatisfiable % 12.33/3.51 |-Branch two: % 12.33/3.51 | (79) ~ green(n2, n5) % 12.33/3.51 | (80) red(n2, n5) % 12.33/3.51 | % 12.33/3.51 | Instantiating formula (10) with n5, n3, n2 and discharging atoms red(n3, n5), red(n2, n5), red(n2, n3), yields: % 12.33/3.51 | (42) $false % 12.33/3.51 | % 12.33/3.51 |-The branch is then unsatisfiable % 12.33/3.51 |-Branch two: % 12.33/3.51 | (94) ~ green(n1, n5) % 12.33/3.51 | (95) red(n1, n5) % 12.33/3.51 | % 12.33/3.51 +-Applying beta-rule and splitting (34), into two cases. % 12.33/3.51 |-Branch one: % 12.33/3.51 | (190) green(n1, n4) % 12.33/3.51 | % 12.33/3.51 | Instantiating formula (2) with n4, n2, n1 and discharging atoms green(n2, n4), green(n1, n4), green(n1, n2), yields: % 12.33/3.51 | (42) $false % 12.33/3.51 | % 12.33/3.51 |-The branch is then unsatisfiable % 12.33/3.51 |-Branch two: % 12.33/3.51 | (192) ~ green(n1, n4) % 12.33/3.51 | (193) red(n1, n4) % 12.33/3.51 | % 12.33/3.51 | Instantiating formula (10) with n5, n4, n1 and discharging atoms red(n4, n5), red(n1, n5), red(n1, n4), yields: % 12.33/3.52 | (42) $false % 12.33/3.52 | % 12.33/3.52 |-The branch is then unsatisfiable % 12.33/3.52 |-Branch two: % 12.33/3.52 | (43) ~ green(n2, n4) % 12.33/3.52 | (44) red(n2, n4) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (76) green(n3, n5) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (53) green(n3, n6) % 12.33/3.52 | % 12.33/3.52 | Instantiating formula (2) with n6, n5, n3 and discharging atoms green(n5, n6), green(n3, n6), green(n3, n5), yields: % 12.33/3.52 | (42) $false % 12.33/3.52 | % 12.33/3.52 |-The branch is then unsatisfiable % 12.33/3.52 |-Branch two: % 12.33/3.52 | (59) ~ green(n3, n6) % 12.33/3.52 | (60) red(n3, n6) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (54) green(n2, n6) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (77) green(n2, n5) % 12.33/3.52 | % 12.33/3.52 | Instantiating formula (2) with n6, n5, n2 and discharging atoms green(n5, n6), green(n2, n6), green(n2, n5), yields: % 12.33/3.52 | (42) $false % 12.33/3.52 | % 12.33/3.52 |-The branch is then unsatisfiable % 12.33/3.52 |-Branch two: % 12.33/3.52 | (79) ~ green(n2, n5) % 12.33/3.52 | (80) red(n2, n5) % 12.33/3.52 | % 12.33/3.52 | Instantiating formula (10) with n5, n4, n2 and discharging atoms red(n4, n5), red(n2, n5), red(n2, n4), yields: % 12.33/3.52 | (42) $false % 12.33/3.52 | % 12.33/3.52 |-The branch is then unsatisfiable % 12.33/3.52 |-Branch two: % 12.33/3.52 | (56) ~ green(n2, n6) % 12.33/3.52 | (57) red(n2, n6) % 12.33/3.52 | % 12.33/3.52 | Instantiating formula (10) with n6, n3, n2 and discharging atoms red(n3, n6), red(n2, n6), red(n2, n3), yields: % 12.33/3.52 | (42) $false % 12.33/3.52 | % 12.33/3.52 |-The branch is then unsatisfiable % 12.33/3.52 |-Branch two: % 12.33/3.52 | (82) ~ green(n3, n5) % 12.33/3.52 | (83) red(n3, n5) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (20), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (45) green(n4, n6) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (53) green(n3, n6) % 12.33/3.52 | % 12.33/3.52 | Instantiating formula (2) with n6, n4, n3 and discharging atoms green(n4, n6), green(n3, n6), green(n3, n4), yields: % 12.33/3.52 | (42) $false % 12.33/3.52 | % 12.33/3.52 |-The branch is then unsatisfiable % 12.33/3.52 |-Branch two: % 12.33/3.52 | (59) ~ green(n3, n6) % 12.33/3.52 | (60) red(n3, n6) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (54) green(n2, n6) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (77) green(n2, n5) % 12.33/3.52 | % 12.33/3.52 | Instantiating formula (2) with n6, n5, n2 and discharging atoms green(n5, n6), green(n2, n6), green(n2, n5), yields: % 12.33/3.52 | (42) $false % 12.33/3.52 | % 12.33/3.52 |-The branch is then unsatisfiable % 12.33/3.52 |-Branch two: % 12.33/3.52 | (79) ~ green(n2, n5) % 12.33/3.52 | (80) red(n2, n5) % 12.33/3.52 | % 12.33/3.52 | Instantiating formula (10) with n5, n3, n2 and discharging atoms red(n3, n5), red(n2, n5), red(n2, n3), yields: % 12.33/3.52 | (42) $false % 12.33/3.52 | % 12.33/3.52 |-The branch is then unsatisfiable % 12.33/3.52 |-Branch two: % 12.33/3.52 | (56) ~ green(n2, n6) % 12.33/3.52 | (57) red(n2, n6) % 12.33/3.52 | % 12.33/3.52 | Instantiating formula (10) with n6, n3, n2 and discharging atoms red(n3, n6), red(n2, n6), red(n2, n3), yields: % 12.33/3.52 | (42) $false % 12.33/3.52 | % 12.33/3.52 |-The branch is then unsatisfiable % 12.33/3.52 |-Branch two: % 12.33/3.52 | (47) ~ green(n4, n6) % 12.33/3.52 | (48) red(n4, n6) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (54) green(n2, n6) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (77) green(n2, n5) % 12.33/3.52 | % 12.33/3.52 | Instantiating formula (2) with n6, n5, n2 and discharging atoms green(n5, n6), green(n2, n6), green(n2, n5), yields: % 12.33/3.52 | (42) $false % 12.33/3.52 | % 12.33/3.52 |-The branch is then unsatisfiable % 12.33/3.52 |-Branch two: % 12.33/3.52 | (79) ~ green(n2, n5) % 12.33/3.52 | (80) red(n2, n5) % 12.33/3.52 | % 12.33/3.52 | Instantiating formula (10) with n5, n3, n2 and discharging atoms red(n3, n5), red(n2, n5), red(n2, n3), yields: % 12.33/3.52 | (42) $false % 12.33/3.52 | % 12.33/3.52 |-The branch is then unsatisfiable % 12.33/3.52 |-Branch two: % 12.33/3.52 | (56) ~ green(n2, n6) % 12.33/3.52 | (57) red(n2, n6) % 12.33/3.52 | % 12.33/3.52 | Instantiating formula (10) with n6, n4, n2 and discharging atoms red(n4, n6), red(n2, n6), red(n2, n4), yields: % 12.33/3.52 | (42) $false % 12.33/3.52 | % 12.33/3.52 |-The branch is then unsatisfiable % 12.33/3.52 |-Branch two: % 12.33/3.52 | (97) ~ green(n5, n6) % 12.33/3.52 | (98) red(n5, n6) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (13), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (40) green(n4, n5) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (25), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (41) green(n2, n4) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (76) green(n3, n5) % 12.33/3.52 | % 12.33/3.52 | Instantiating formula (2) with n5, n4, n3 and discharging atoms green(n4, n5), green(n3, n5), green(n3, n4), yields: % 12.33/3.52 | (42) $false % 12.33/3.52 | % 12.33/3.52 |-The branch is then unsatisfiable % 12.33/3.52 |-Branch two: % 12.33/3.52 | (82) ~ green(n3, n5) % 12.33/3.52 | (83) red(n3, n5) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (77) green(n2, n5) % 12.33/3.52 | % 12.33/3.52 | Instantiating formula (2) with n5, n4, n2 and discharging atoms green(n4, n5), green(n2, n5), green(n2, n4), yields: % 12.33/3.52 | (42) $false % 12.33/3.52 | % 12.33/3.52 |-The branch is then unsatisfiable % 12.33/3.52 |-Branch two: % 12.33/3.52 | (79) ~ green(n2, n5) % 12.33/3.52 | (80) red(n2, n5) % 12.33/3.52 | % 12.33/3.52 | Instantiating formula (10) with n5, n3, n2 and discharging atoms red(n3, n5), red(n2, n5), red(n2, n3), yields: % 12.33/3.52 | (42) $false % 12.33/3.52 | % 12.33/3.52 |-The branch is then unsatisfiable % 12.33/3.52 |-Branch two: % 12.33/3.52 | (43) ~ green(n2, n4) % 12.33/3.52 | (44) red(n2, n4) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (76) green(n3, n5) % 12.33/3.52 | % 12.33/3.52 | Instantiating formula (2) with n5, n4, n3 and discharging atoms green(n4, n5), green(n3, n5), green(n3, n4), yields: % 12.33/3.52 | (42) $false % 12.33/3.52 | % 12.33/3.52 |-The branch is then unsatisfiable % 12.33/3.52 |-Branch two: % 12.33/3.52 | (82) ~ green(n3, n5) % 12.33/3.52 | (83) red(n3, n5) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (20), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (45) green(n4, n6) % 12.33/3.52 | % 12.33/3.52 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.52 |-Branch one: % 12.33/3.52 | (53) green(n3, n6) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (2) with n6, n4, n3 and discharging atoms green(n4, n6), green(n3, n6), green(n3, n4), yields: % 12.33/3.53 | (42) $false % 12.33/3.53 | % 12.33/3.53 |-The branch is then unsatisfiable % 12.33/3.53 |-Branch two: % 12.33/3.53 | (59) ~ green(n3, n6) % 12.33/3.53 | (60) red(n3, n6) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (10) with n6, n5, n3 and discharging atoms red(n5, n6), red(n3, n6), red(n3, n5), yields: % 12.33/3.53 | (42) $false % 12.33/3.53 | % 12.33/3.53 |-The branch is then unsatisfiable % 12.33/3.53 |-Branch two: % 12.33/3.53 | (47) ~ green(n4, n6) % 12.33/3.53 | (48) red(n4, n6) % 12.33/3.53 | % 12.33/3.53 +-Applying beta-rule and splitting (28), into two cases. % 12.33/3.53 |-Branch one: % 12.33/3.53 | (49) green(n1, n3) % 12.33/3.53 | % 12.33/3.53 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.53 |-Branch one: % 12.33/3.53 | (54) green(n2, n6) % 12.33/3.53 | % 12.33/3.53 +-Applying beta-rule and splitting (34), into two cases. % 12.33/3.53 |-Branch one: % 12.33/3.53 | (190) green(n1, n4) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (2) with n4, n3, n1 and discharging atoms green(n3, n4), green(n1, n4), green(n1, n3), yields: % 12.33/3.53 | (42) $false % 12.33/3.53 | % 12.33/3.53 |-The branch is then unsatisfiable % 12.33/3.53 |-Branch two: % 12.33/3.53 | (192) ~ green(n1, n4) % 12.33/3.53 | (193) red(n1, n4) % 12.33/3.53 | % 12.33/3.53 +-Applying beta-rule and splitting (35), into two cases. % 12.33/3.53 |-Branch one: % 12.33/3.53 | (62) green(n1, n6) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (2) with n6, n2, n1 and discharging atoms green(n2, n6), green(n1, n6), green(n1, n2), yields: % 12.33/3.53 | (42) $false % 12.33/3.53 | % 12.33/3.53 |-The branch is then unsatisfiable % 12.33/3.53 |-Branch two: % 12.33/3.53 | (64) ~ green(n1, n6) % 12.33/3.53 | (65) red(n1, n6) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (10) with n6, n4, n1 and discharging atoms red(n4, n6), red(n1, n6), red(n1, n4), yields: % 12.33/3.53 | (42) $false % 12.33/3.53 | % 12.33/3.53 |-The branch is then unsatisfiable % 12.33/3.53 |-Branch two: % 12.33/3.53 | (56) ~ green(n2, n6) % 12.33/3.53 | (57) red(n2, n6) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (10) with n6, n4, n2 and discharging atoms red(n4, n6), red(n2, n6), red(n2, n4), yields: % 12.33/3.53 | (42) $false % 12.33/3.53 | % 12.33/3.53 |-The branch is then unsatisfiable % 12.33/3.53 |-Branch two: % 12.33/3.53 | (51) ~ green(n1, n3) % 12.33/3.53 | (52) red(n1, n3) % 12.33/3.53 | % 12.33/3.53 +-Applying beta-rule and splitting (32), into two cases. % 12.33/3.53 |-Branch one: % 12.33/3.53 | (88) green(n1, n5) % 12.33/3.53 | % 12.33/3.53 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.53 |-Branch one: % 12.33/3.53 | (77) green(n2, n5) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (2) with n5, n2, n1 and discharging atoms green(n2, n5), green(n1, n5), green(n1, n2), yields: % 12.33/3.53 | (42) $false % 12.33/3.53 | % 12.33/3.53 |-The branch is then unsatisfiable % 12.33/3.53 |-Branch two: % 12.33/3.53 | (79) ~ green(n2, n5) % 12.33/3.53 | (80) red(n2, n5) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (10) with n5, n3, n2 and discharging atoms red(n3, n5), red(n2, n5), red(n2, n3), yields: % 12.33/3.53 | (42) $false % 12.33/3.53 | % 12.33/3.53 |-The branch is then unsatisfiable % 12.33/3.53 |-Branch two: % 12.33/3.53 | (94) ~ green(n1, n5) % 12.33/3.53 | (95) red(n1, n5) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (10) with n5, n3, n1 and discharging atoms red(n3, n5), red(n1, n5), red(n1, n3), yields: % 12.33/3.53 | (42) $false % 12.33/3.53 | % 12.33/3.53 |-The branch is then unsatisfiable % 12.33/3.53 |-Branch two: % 12.33/3.53 | (70) ~ green(n4, n5) % 12.33/3.53 | (71) red(n4, n5) % 12.33/3.53 | % 12.33/3.53 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.53 |-Branch one: % 12.33/3.53 | (76) green(n3, n5) % 12.33/3.53 | % 12.33/3.53 +-Applying beta-rule and splitting (20), into two cases. % 12.33/3.53 |-Branch one: % 12.33/3.53 | (45) green(n4, n6) % 12.33/3.53 | % 12.33/3.53 +-Applying beta-rule and splitting (28), into two cases. % 12.33/3.53 |-Branch one: % 12.33/3.53 | (49) green(n1, n3) % 12.33/3.53 | % 12.33/3.53 +-Applying beta-rule and splitting (32), into two cases. % 12.33/3.53 |-Branch one: % 12.33/3.53 | (88) green(n1, n5) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (2) with n5, n3, n1 and discharging atoms green(n3, n5), green(n1, n5), green(n1, n3), yields: % 12.33/3.53 | (42) $false % 12.33/3.53 | % 12.33/3.53 |-The branch is then unsatisfiable % 12.33/3.53 |-Branch two: % 12.33/3.53 | (94) ~ green(n1, n5) % 12.33/3.53 | (95) red(n1, n5) % 12.33/3.53 | % 12.33/3.53 +-Applying beta-rule and splitting (34), into two cases. % 12.33/3.53 |-Branch one: % 12.33/3.53 | (190) green(n1, n4) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (2) with n4, n3, n1 and discharging atoms green(n3, n4), green(n1, n4), green(n1, n3), yields: % 12.33/3.53 | (42) $false % 12.33/3.53 | % 12.33/3.53 |-The branch is then unsatisfiable % 12.33/3.53 |-Branch two: % 12.33/3.53 | (192) ~ green(n1, n4) % 12.33/3.53 | (193) red(n1, n4) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (10) with n5, n4, n1 and discharging atoms red(n4, n5), red(n1, n5), red(n1, n4), yields: % 12.33/3.53 | (42) $false % 12.33/3.53 | % 12.33/3.53 |-The branch is then unsatisfiable % 12.33/3.53 |-Branch two: % 12.33/3.53 | (51) ~ green(n1, n3) % 12.33/3.53 | (52) red(n1, n3) % 12.33/3.53 | % 12.33/3.53 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.53 |-Branch one: % 12.33/3.53 | (53) green(n3, n6) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (2) with n6, n4, n3 and discharging atoms green(n4, n6), green(n3, n6), green(n3, n4), yields: % 12.33/3.53 | (42) $false % 12.33/3.53 | % 12.33/3.53 |-The branch is then unsatisfiable % 12.33/3.53 |-Branch two: % 12.33/3.53 | (59) ~ green(n3, n6) % 12.33/3.53 | (60) red(n3, n6) % 12.33/3.53 | % 12.33/3.53 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.53 |-Branch one: % 12.33/3.53 | (54) green(n2, n6) % 12.33/3.53 | % 12.33/3.53 +-Applying beta-rule and splitting (35), into two cases. % 12.33/3.53 |-Branch one: % 12.33/3.53 | (62) green(n1, n6) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (2) with n6, n2, n1 and discharging atoms green(n2, n6), green(n1, n6), green(n1, n2), yields: % 12.33/3.53 | (42) $false % 12.33/3.53 | % 12.33/3.53 |-The branch is then unsatisfiable % 12.33/3.53 |-Branch two: % 12.33/3.53 | (64) ~ green(n1, n6) % 12.33/3.53 | (65) red(n1, n6) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (10) with n6, n3, n1 and discharging atoms red(n3, n6), red(n1, n6), red(n1, n3), yields: % 12.33/3.53 | (42) $false % 12.33/3.53 | % 12.33/3.53 |-The branch is then unsatisfiable % 12.33/3.53 |-Branch two: % 12.33/3.53 | (56) ~ green(n2, n6) % 12.33/3.53 | (57) red(n2, n6) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (10) with n6, n3, n2 and discharging atoms red(n3, n6), red(n2, n6), red(n2, n3), yields: % 12.33/3.53 | (42) $false % 12.33/3.53 | % 12.33/3.53 |-The branch is then unsatisfiable % 12.33/3.53 |-Branch two: % 12.33/3.53 | (47) ~ green(n4, n6) % 12.33/3.53 | (48) red(n4, n6) % 12.33/3.53 | % 12.33/3.53 | Instantiating formula (10) with n6, n5, n4 and discharging atoms red(n5, n6), red(n4, n6), red(n4, n5), yields: % 12.33/3.54 | (42) $false % 12.33/3.54 | % 12.33/3.54 |-The branch is then unsatisfiable % 12.33/3.54 |-Branch two: % 12.33/3.54 | (82) ~ green(n3, n5) % 12.33/3.54 | (83) red(n3, n5) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (20), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (45) green(n4, n6) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (53) green(n3, n6) % 12.33/3.54 | % 12.33/3.54 | Instantiating formula (2) with n6, n4, n3 and discharging atoms green(n4, n6), green(n3, n6), green(n3, n4), yields: % 12.33/3.54 | (42) $false % 12.33/3.54 | % 12.33/3.54 |-The branch is then unsatisfiable % 12.33/3.54 |-Branch two: % 12.33/3.54 | (59) ~ green(n3, n6) % 12.33/3.54 | (60) red(n3, n6) % 12.33/3.54 | % 12.33/3.54 | Instantiating formula (10) with n6, n5, n3 and discharging atoms red(n5, n6), red(n3, n6), red(n3, n5), yields: % 12.33/3.54 | (42) $false % 12.33/3.54 | % 12.33/3.54 |-The branch is then unsatisfiable % 12.33/3.54 |-Branch two: % 12.33/3.54 | (47) ~ green(n4, n6) % 12.33/3.54 | (48) red(n4, n6) % 12.33/3.54 | % 12.33/3.54 | Instantiating formula (10) with n6, n5, n4 and discharging atoms red(n5, n6), red(n4, n6), red(n4, n5), yields: % 12.33/3.54 | (42) $false % 12.33/3.54 | % 12.33/3.54 |-The branch is then unsatisfiable % 12.33/3.54 |-Branch two: % 12.33/3.54 | (363) ~ green(n1, n2) % 12.33/3.54 | (364) red(n1, n2) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (17), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (38) green(n2, n3) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (11), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (39) green(n5, n6) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (13), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (40) green(n4, n5) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (25), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (41) green(n2, n4) % 12.33/3.54 | % 12.33/3.54 | Instantiating formula (2) with n4, n3, n2 and discharging atoms green(n3, n4), green(n2, n4), green(n2, n3), yields: % 12.33/3.54 | (42) $false % 12.33/3.54 | % 12.33/3.54 |-The branch is then unsatisfiable % 12.33/3.54 |-Branch two: % 12.33/3.54 | (43) ~ green(n2, n4) % 12.33/3.54 | (44) red(n2, n4) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (76) green(n3, n5) % 12.33/3.54 | % 12.33/3.54 | Instantiating formula (2) with n5, n4, n3 and discharging atoms green(n4, n5), green(n3, n5), green(n3, n4), yields: % 12.33/3.54 | (42) $false % 12.33/3.54 | % 12.33/3.54 |-The branch is then unsatisfiable % 12.33/3.54 |-Branch two: % 12.33/3.54 | (82) ~ green(n3, n5) % 12.33/3.54 | (83) red(n3, n5) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (28), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (49) green(n1, n3) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (34), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (190) green(n1, n4) % 12.33/3.54 | % 12.33/3.54 | Instantiating formula (2) with n4, n3, n1 and discharging atoms green(n3, n4), green(n1, n4), green(n1, n3), yields: % 12.33/3.54 | (42) $false % 12.33/3.54 | % 12.33/3.54 |-The branch is then unsatisfiable % 12.33/3.54 |-Branch two: % 12.33/3.54 | (192) ~ green(n1, n4) % 12.33/3.54 | (193) red(n1, n4) % 12.33/3.54 | % 12.33/3.54 | Instantiating formula (10) with n4, n2, n1 and discharging atoms red(n2, n4), red(n1, n4), red(n1, n2), yields: % 12.33/3.54 | (42) $false % 12.33/3.54 | % 12.33/3.54 |-The branch is then unsatisfiable % 12.33/3.54 |-Branch two: % 12.33/3.54 | (51) ~ green(n1, n3) % 12.33/3.54 | (52) red(n1, n3) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (32), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (88) green(n1, n5) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (34), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (190) green(n1, n4) % 12.33/3.54 | % 12.33/3.54 | Instantiating formula (2) with n5, n4, n1 and discharging atoms green(n4, n5), green(n1, n5), green(n1, n4), yields: % 12.33/3.54 | (42) $false % 12.33/3.54 | % 12.33/3.54 |-The branch is then unsatisfiable % 12.33/3.54 |-Branch two: % 12.33/3.54 | (192) ~ green(n1, n4) % 12.33/3.54 | (193) red(n1, n4) % 12.33/3.54 | % 12.33/3.54 | Instantiating formula (10) with n4, n2, n1 and discharging atoms red(n2, n4), red(n1, n4), red(n1, n2), yields: % 12.33/3.54 | (42) $false % 12.33/3.54 | % 12.33/3.54 |-The branch is then unsatisfiable % 12.33/3.54 |-Branch two: % 12.33/3.54 | (94) ~ green(n1, n5) % 12.33/3.54 | (95) red(n1, n5) % 12.33/3.54 | % 12.33/3.54 | Instantiating formula (10) with n5, n3, n1 and discharging atoms red(n3, n5), red(n1, n5), red(n1, n3), yields: % 12.33/3.54 | (42) $false % 12.33/3.54 | % 12.33/3.54 |-The branch is then unsatisfiable % 12.33/3.54 |-Branch two: % 12.33/3.54 | (70) ~ green(n4, n5) % 12.33/3.54 | (71) red(n4, n5) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (25), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (41) green(n2, n4) % 12.33/3.54 | % 12.33/3.54 | Instantiating formula (2) with n4, n3, n2 and discharging atoms green(n3, n4), green(n2, n4), green(n2, n3), yields: % 12.33/3.54 | (42) $false % 12.33/3.54 | % 12.33/3.54 |-The branch is then unsatisfiable % 12.33/3.54 |-Branch two: % 12.33/3.54 | (43) ~ green(n2, n4) % 12.33/3.54 | (44) red(n2, n4) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (20), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (45) green(n4, n6) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (54) green(n2, n6) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (77) green(n2, n5) % 12.33/3.54 | % 12.33/3.54 | Instantiating formula (2) with n6, n5, n2 and discharging atoms green(n5, n6), green(n2, n6), green(n2, n5), yields: % 12.33/3.54 | (42) $false % 12.33/3.54 | % 12.33/3.54 |-The branch is then unsatisfiable % 12.33/3.54 |-Branch two: % 12.33/3.54 | (79) ~ green(n2, n5) % 12.33/3.54 | (80) red(n2, n5) % 12.33/3.54 | % 12.33/3.54 | Instantiating formula (10) with n5, n4, n2 and discharging atoms red(n4, n5), red(n2, n5), red(n2, n4), yields: % 12.33/3.54 | (42) $false % 12.33/3.54 | % 12.33/3.54 |-The branch is then unsatisfiable % 12.33/3.54 |-Branch two: % 12.33/3.54 | (56) ~ green(n2, n6) % 12.33/3.54 | (57) red(n2, n6) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (34), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (190) green(n1, n4) % 12.33/3.54 | % 12.33/3.54 +-Applying beta-rule and splitting (35), into two cases. % 12.33/3.54 |-Branch one: % 12.33/3.54 | (62) green(n1, n6) % 12.33/3.54 | % 12.33/3.54 | Instantiating formula (2) with n6, n4, n1 and discharging atoms green(n4, n6), green(n1, n6), green(n1, n4), yields: % 12.33/3.54 | (42) $false % 12.33/3.54 | % 12.33/3.54 |-The branch is then unsatisfiable % 12.33/3.54 |-Branch two: % 12.33/3.54 | (64) ~ green(n1, n6) % 12.33/3.54 | (65) red(n1, n6) % 12.33/3.54 | % 12.33/3.54 | Instantiating formula (10) with n6, n2, n1 and discharging atoms red(n2, n6), red(n1, n6), red(n1, n2), yields: % 12.33/3.54 | (42) $false % 12.33/3.54 | % 12.33/3.54 |-The branch is then unsatisfiable % 12.33/3.54 |-Branch two: % 12.33/3.54 | (192) ~ green(n1, n4) % 12.33/3.54 | (193) red(n1, n4) % 12.33/3.54 | % 12.33/3.54 | Instantiating formula (10) with n4, n2, n1 and discharging atoms red(n2, n4), red(n1, n4), red(n1, n2), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (47) ~ green(n4, n6) % 12.33/3.55 | (48) red(n4, n6) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (54) green(n2, n6) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (77) green(n2, n5) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (2) with n6, n5, n2 and discharging atoms green(n5, n6), green(n2, n6), green(n2, n5), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (79) ~ green(n2, n5) % 12.33/3.55 | (80) red(n2, n5) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (10) with n5, n4, n2 and discharging atoms red(n4, n5), red(n2, n5), red(n2, n4), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (56) ~ green(n2, n6) % 12.33/3.55 | (57) red(n2, n6) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (10) with n6, n4, n2 and discharging atoms red(n4, n6), red(n2, n6), red(n2, n4), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (97) ~ green(n5, n6) % 12.33/3.55 | (98) red(n5, n6) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (13), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (40) green(n4, n5) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (25), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (41) green(n2, n4) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (2) with n4, n3, n2 and discharging atoms green(n3, n4), green(n2, n4), green(n2, n3), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (43) ~ green(n2, n4) % 12.33/3.55 | (44) red(n2, n4) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (76) green(n3, n5) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (2) with n5, n4, n3 and discharging atoms green(n4, n5), green(n3, n5), green(n3, n4), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (82) ~ green(n3, n5) % 12.33/3.55 | (83) red(n3, n5) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (20), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (45) green(n4, n6) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (53) green(n3, n6) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (2) with n6, n4, n3 and discharging atoms green(n4, n6), green(n3, n6), green(n3, n4), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (59) ~ green(n3, n6) % 12.33/3.55 | (60) red(n3, n6) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (10) with n6, n5, n3 and discharging atoms red(n5, n6), red(n3, n6), red(n3, n5), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (47) ~ green(n4, n6) % 12.33/3.55 | (48) red(n4, n6) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (53) green(n3, n6) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (54) green(n2, n6) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (2) with n6, n3, n2 and discharging atoms green(n3, n6), green(n2, n6), green(n2, n3), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (56) ~ green(n2, n6) % 12.33/3.55 | (57) red(n2, n6) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (10) with n6, n4, n2 and discharging atoms red(n4, n6), red(n2, n6), red(n2, n4), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (59) ~ green(n3, n6) % 12.33/3.55 | (60) red(n3, n6) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (10) with n6, n5, n3 and discharging atoms red(n5, n6), red(n3, n6), red(n3, n5), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (70) ~ green(n4, n5) % 12.33/3.55 | (71) red(n4, n5) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (25), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (41) green(n2, n4) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (2) with n4, n3, n2 and discharging atoms green(n3, n4), green(n2, n4), green(n2, n3), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (43) ~ green(n2, n4) % 12.33/3.55 | (44) red(n2, n4) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (76) green(n3, n5) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (77) green(n2, n5) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (2) with n5, n3, n2 and discharging atoms green(n3, n5), green(n2, n5), green(n2, n3), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (79) ~ green(n2, n5) % 12.33/3.55 | (80) red(n2, n5) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (10) with n5, n4, n2 and discharging atoms red(n4, n5), red(n2, n5), red(n2, n4), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (82) ~ green(n3, n5) % 12.33/3.55 | (83) red(n3, n5) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (20), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (45) green(n4, n6) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (53) green(n3, n6) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (2) with n6, n4, n3 and discharging atoms green(n4, n6), green(n3, n6), green(n3, n4), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (59) ~ green(n3, n6) % 12.33/3.55 | (60) red(n3, n6) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (10) with n6, n5, n3 and discharging atoms red(n5, n6), red(n3, n6), red(n3, n5), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (47) ~ green(n4, n6) % 12.33/3.55 | (48) red(n4, n6) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (10) with n6, n5, n4 and discharging atoms red(n5, n6), red(n4, n6), red(n4, n5), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (148) ~ green(n2, n3) % 12.33/3.55 | (149) red(n2, n3) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (11), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (39) green(n5, n6) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (76) green(n3, n5) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (28), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (49) green(n1, n3) % 12.33/3.55 | % 12.33/3.55 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.55 |-Branch one: % 12.33/3.55 | (53) green(n3, n6) % 12.33/3.55 | % 12.33/3.55 | Instantiating formula (2) with n6, n5, n3 and discharging atoms green(n5, n6), green(n3, n6), green(n3, n5), yields: % 12.33/3.55 | (42) $false % 12.33/3.55 | % 12.33/3.55 |-The branch is then unsatisfiable % 12.33/3.55 |-Branch two: % 12.33/3.55 | (59) ~ green(n3, n6) % 12.33/3.56 | (60) red(n3, n6) % 12.33/3.56 | % 12.33/3.56 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.56 |-Branch one: % 12.33/3.56 | (54) green(n2, n6) % 12.33/3.56 | % 12.33/3.56 +-Applying beta-rule and splitting (32), into two cases. % 12.33/3.56 |-Branch one: % 12.33/3.56 | (88) green(n1, n5) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (2) with n5, n3, n1 and discharging atoms green(n3, n5), green(n1, n5), green(n1, n3), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (94) ~ green(n1, n5) % 12.33/3.56 | (95) red(n1, n5) % 12.33/3.56 | % 12.33/3.56 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.56 |-Branch one: % 12.33/3.56 | (77) green(n2, n5) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (2) with n6, n5, n2 and discharging atoms green(n5, n6), green(n2, n6), green(n2, n5), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (79) ~ green(n2, n5) % 12.33/3.56 | (80) red(n2, n5) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (10) with n5, n2, n1 and discharging atoms red(n2, n5), red(n1, n5), red(n1, n2), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (56) ~ green(n2, n6) % 12.33/3.56 | (57) red(n2, n6) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (10) with n6, n3, n2 and discharging atoms red(n3, n6), red(n2, n6), red(n2, n3), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (51) ~ green(n1, n3) % 12.33/3.56 | (52) red(n1, n3) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (10) with n3, n2, n1 and discharging atoms red(n2, n3), red(n1, n3), red(n1, n2), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (82) ~ green(n3, n5) % 12.33/3.56 | (83) red(n3, n5) % 12.33/3.56 | % 12.33/3.56 +-Applying beta-rule and splitting (28), into two cases. % 12.33/3.56 |-Branch one: % 12.33/3.56 | (49) green(n1, n3) % 12.33/3.56 | % 12.33/3.56 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.56 |-Branch one: % 12.33/3.56 | (53) green(n3, n6) % 12.33/3.56 | % 12.33/3.56 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.56 |-Branch one: % 12.33/3.56 | (54) green(n2, n6) % 12.33/3.56 | % 12.33/3.56 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.56 |-Branch one: % 12.33/3.56 | (77) green(n2, n5) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (2) with n6, n5, n2 and discharging atoms green(n5, n6), green(n2, n6), green(n2, n5), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (79) ~ green(n2, n5) % 12.33/3.56 | (80) red(n2, n5) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (10) with n5, n3, n2 and discharging atoms red(n3, n5), red(n2, n5), red(n2, n3), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (56) ~ green(n2, n6) % 12.33/3.56 | (57) red(n2, n6) % 12.33/3.56 | % 12.33/3.56 +-Applying beta-rule and splitting (35), into two cases. % 12.33/3.56 |-Branch one: % 12.33/3.56 | (62) green(n1, n6) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (2) with n6, n3, n1 and discharging atoms green(n3, n6), green(n1, n6), green(n1, n3), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (64) ~ green(n1, n6) % 12.33/3.56 | (65) red(n1, n6) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (10) with n6, n2, n1 and discharging atoms red(n2, n6), red(n1, n6), red(n1, n2), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (59) ~ green(n3, n6) % 12.33/3.56 | (60) red(n3, n6) % 12.33/3.56 | % 12.33/3.56 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.56 |-Branch one: % 12.33/3.56 | (54) green(n2, n6) % 12.33/3.56 | % 12.33/3.56 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.56 |-Branch one: % 12.33/3.56 | (77) green(n2, n5) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (2) with n6, n5, n2 and discharging atoms green(n5, n6), green(n2, n6), green(n2, n5), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (79) ~ green(n2, n5) % 12.33/3.56 | (80) red(n2, n5) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (10) with n5, n3, n2 and discharging atoms red(n3, n5), red(n2, n5), red(n2, n3), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (56) ~ green(n2, n6) % 12.33/3.56 | (57) red(n2, n6) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (10) with n6, n3, n2 and discharging atoms red(n3, n6), red(n2, n6), red(n2, n3), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (51) ~ green(n1, n3) % 12.33/3.56 | (52) red(n1, n3) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (10) with n3, n2, n1 and discharging atoms red(n2, n3), red(n1, n3), red(n1, n2), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (97) ~ green(n5, n6) % 12.33/3.56 | (98) red(n5, n6) % 12.33/3.56 | % 12.33/3.56 +-Applying beta-rule and splitting (13), into two cases. % 12.33/3.56 |-Branch one: % 12.33/3.56 | (40) green(n4, n5) % 12.33/3.56 | % 12.33/3.56 +-Applying beta-rule and splitting (25), into two cases. % 12.33/3.56 |-Branch one: % 12.33/3.56 | (41) green(n2, n4) % 12.33/3.56 | % 12.33/3.56 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.56 |-Branch one: % 12.33/3.56 | (76) green(n3, n5) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (2) with n5, n4, n3 and discharging atoms green(n4, n5), green(n3, n5), green(n3, n4), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (82) ~ green(n3, n5) % 12.33/3.56 | (83) red(n3, n5) % 12.33/3.56 | % 12.33/3.56 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.56 |-Branch one: % 12.33/3.56 | (77) green(n2, n5) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (2) with n5, n4, n2 and discharging atoms green(n4, n5), green(n2, n5), green(n2, n4), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (79) ~ green(n2, n5) % 12.33/3.56 | (80) red(n2, n5) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (10) with n5, n3, n2 and discharging atoms red(n3, n5), red(n2, n5), red(n2, n3), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (43) ~ green(n2, n4) % 12.33/3.56 | (44) red(n2, n4) % 12.33/3.56 | % 12.33/3.56 +-Applying beta-rule and splitting (28), into two cases. % 12.33/3.56 |-Branch one: % 12.33/3.56 | (49) green(n1, n3) % 12.33/3.56 | % 12.33/3.56 +-Applying beta-rule and splitting (34), into two cases. % 12.33/3.56 |-Branch one: % 12.33/3.56 | (190) green(n1, n4) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (2) with n4, n3, n1 and discharging atoms green(n3, n4), green(n1, n4), green(n1, n3), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.56 |-Branch two: % 12.33/3.56 | (192) ~ green(n1, n4) % 12.33/3.56 | (193) red(n1, n4) % 12.33/3.56 | % 12.33/3.56 | Instantiating formula (10) with n4, n2, n1 and discharging atoms red(n2, n4), red(n1, n4), red(n1, n2), yields: % 12.33/3.56 | (42) $false % 12.33/3.56 | % 12.33/3.56 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (51) ~ green(n1, n3) % 12.33/3.57 | (52) red(n1, n3) % 12.33/3.57 | % 12.33/3.57 | Instantiating formula (10) with n3, n2, n1 and discharging atoms red(n2, n3), red(n1, n3), red(n1, n2), yields: % 12.33/3.57 | (42) $false % 12.33/3.57 | % 12.33/3.57 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (70) ~ green(n4, n5) % 12.33/3.57 | (71) red(n4, n5) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (25), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (41) green(n2, n4) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (20), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (45) green(n4, n6) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (53) green(n3, n6) % 12.33/3.57 | % 12.33/3.57 | Instantiating formula (2) with n6, n4, n3 and discharging atoms green(n4, n6), green(n3, n6), green(n3, n4), yields: % 12.33/3.57 | (42) $false % 12.33/3.57 | % 12.33/3.57 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (59) ~ green(n3, n6) % 12.33/3.57 | (60) red(n3, n6) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (54) green(n2, n6) % 12.33/3.57 | % 12.33/3.57 | Instantiating formula (2) with n6, n4, n2 and discharging atoms green(n4, n6), green(n2, n6), green(n2, n4), yields: % 12.33/3.57 | (42) $false % 12.33/3.57 | % 12.33/3.57 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (56) ~ green(n2, n6) % 12.33/3.57 | (57) red(n2, n6) % 12.33/3.57 | % 12.33/3.57 | Instantiating formula (10) with n6, n3, n2 and discharging atoms red(n3, n6), red(n2, n6), red(n2, n3), yields: % 12.33/3.57 | (42) $false % 12.33/3.57 | % 12.33/3.57 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (47) ~ green(n4, n6) % 12.33/3.57 | (48) red(n4, n6) % 12.33/3.57 | % 12.33/3.57 | Instantiating formula (10) with n6, n5, n4 and discharging atoms red(n5, n6), red(n4, n6), red(n4, n5), yields: % 12.33/3.57 | (42) $false % 12.33/3.57 | % 12.33/3.57 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (43) ~ green(n2, n4) % 12.33/3.57 | (44) red(n2, n4) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (28), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (49) green(n1, n3) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (34), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (190) green(n1, n4) % 12.33/3.57 | % 12.33/3.57 | Instantiating formula (2) with n4, n3, n1 and discharging atoms green(n3, n4), green(n1, n4), green(n1, n3), yields: % 12.33/3.57 | (42) $false % 12.33/3.57 | % 12.33/3.57 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (192) ~ green(n1, n4) % 12.33/3.57 | (193) red(n1, n4) % 12.33/3.57 | % 12.33/3.57 | Instantiating formula (10) with n4, n2, n1 and discharging atoms red(n2, n4), red(n1, n4), red(n1, n2), yields: % 12.33/3.57 | (42) $false % 12.33/3.57 | % 12.33/3.57 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (51) ~ green(n1, n3) % 12.33/3.57 | (52) red(n1, n3) % 12.33/3.57 | % 12.33/3.57 | Instantiating formula (10) with n3, n2, n1 and discharging atoms red(n2, n3), red(n1, n3), red(n1, n2), yields: % 12.33/3.57 | (42) $false % 12.33/3.57 | % 12.33/3.57 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (586) ~ green(n3, n4) % 12.33/3.57 | (587) red(n3, n4) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (19), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (37) green(n1, n2) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (17), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (38) green(n2, n3) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (11), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (39) green(n5, n6) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (13), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (40) green(n4, n5) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (25), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (41) green(n2, n4) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (28), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (49) green(n1, n3) % 12.33/3.57 | % 12.33/3.57 | Instantiating formula (2) with n3, n2, n1 and discharging atoms green(n2, n3), green(n1, n3), green(n1, n2), yields: % 12.33/3.57 | (42) $false % 12.33/3.57 | % 12.33/3.57 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (51) ~ green(n1, n3) % 12.33/3.57 | (52) red(n1, n3) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (34), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (190) green(n1, n4) % 12.33/3.57 | % 12.33/3.57 | Instantiating formula (2) with n4, n2, n1 and discharging atoms green(n2, n4), green(n1, n4), green(n1, n2), yields: % 12.33/3.57 | (42) $false % 12.33/3.57 | % 12.33/3.57 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (192) ~ green(n1, n4) % 12.33/3.57 | (193) red(n1, n4) % 12.33/3.57 | % 12.33/3.57 | Instantiating formula (10) with n4, n3, n1 and discharging atoms red(n3, n4), red(n1, n4), red(n1, n3), yields: % 12.33/3.57 | (42) $false % 12.33/3.57 | % 12.33/3.57 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (43) ~ green(n2, n4) % 12.33/3.57 | (44) red(n2, n4) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (20), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (45) green(n4, n6) % 12.33/3.57 | % 12.33/3.57 | Instantiating formula (2) with n6, n5, n4 and discharging atoms green(n5, n6), green(n4, n6), green(n4, n5), yields: % 12.33/3.57 | (42) $false % 12.33/3.57 | % 12.33/3.57 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (47) ~ green(n4, n6) % 12.33/3.57 | (48) red(n4, n6) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (53) green(n3, n6) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (54) green(n2, n6) % 12.33/3.57 | % 12.33/3.57 | Instantiating formula (2) with n6, n3, n2 and discharging atoms green(n3, n6), green(n2, n6), green(n2, n3), yields: % 12.33/3.57 | (42) $false % 12.33/3.57 | % 12.33/3.57 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (56) ~ green(n2, n6) % 12.33/3.57 | (57) red(n2, n6) % 12.33/3.57 | % 12.33/3.57 | Instantiating formula (10) with n6, n4, n2 and discharging atoms red(n4, n6), red(n2, n6), red(n2, n4), yields: % 12.33/3.57 | (42) $false % 12.33/3.57 | % 12.33/3.57 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (59) ~ green(n3, n6) % 12.33/3.57 | (60) red(n3, n6) % 12.33/3.57 | % 12.33/3.57 | Instantiating formula (10) with n6, n4, n3 and discharging atoms red(n4, n6), red(n3, n6), red(n3, n4), yields: % 12.33/3.57 | (42) $false % 12.33/3.57 | % 12.33/3.57 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (70) ~ green(n4, n5) % 12.33/3.57 | (71) red(n4, n5) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (25), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (41) green(n2, n4) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (28), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.57 | (49) green(n1, n3) % 12.33/3.57 | % 12.33/3.57 | Instantiating formula (2) with n3, n2, n1 and discharging atoms green(n2, n3), green(n1, n3), green(n1, n2), yields: % 12.33/3.57 | (42) $false % 12.33/3.57 | % 12.33/3.57 |-The branch is then unsatisfiable % 12.33/3.57 |-Branch two: % 12.33/3.57 | (51) ~ green(n1, n3) % 12.33/3.57 | (52) red(n1, n3) % 12.33/3.57 | % 12.33/3.57 +-Applying beta-rule and splitting (34), into two cases. % 12.33/3.57 |-Branch one: % 12.33/3.58 | (190) green(n1, n4) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (2) with n4, n2, n1 and discharging atoms green(n2, n4), green(n1, n4), green(n1, n2), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (192) ~ green(n1, n4) % 12.33/3.58 | (193) red(n1, n4) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (10) with n4, n3, n1 and discharging atoms red(n3, n4), red(n1, n4), red(n1, n3), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (43) ~ green(n2, n4) % 12.33/3.58 | (44) red(n2, n4) % 12.33/3.58 | % 12.33/3.58 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.58 |-Branch one: % 12.33/3.58 | (76) green(n3, n5) % 12.33/3.58 | % 12.33/3.58 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.58 |-Branch one: % 12.33/3.58 | (77) green(n2, n5) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (2) with n5, n3, n2 and discharging atoms green(n3, n5), green(n2, n5), green(n2, n3), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (79) ~ green(n2, n5) % 12.33/3.58 | (80) red(n2, n5) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (10) with n5, n4, n2 and discharging atoms red(n4, n5), red(n2, n5), red(n2, n4), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (82) ~ green(n3, n5) % 12.33/3.58 | (83) red(n3, n5) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (10) with n5, n4, n3 and discharging atoms red(n4, n5), red(n3, n5), red(n3, n4), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (97) ~ green(n5, n6) % 12.33/3.58 | (98) red(n5, n6) % 12.33/3.58 | % 12.33/3.58 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.58 |-Branch one: % 12.33/3.58 | (76) green(n3, n5) % 12.33/3.58 | % 12.33/3.58 +-Applying beta-rule and splitting (28), into two cases. % 12.33/3.58 |-Branch one: % 12.33/3.58 | (49) green(n1, n3) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (2) with n3, n2, n1 and discharging atoms green(n2, n3), green(n1, n3), green(n1, n2), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (51) ~ green(n1, n3) % 12.33/3.58 | (52) red(n1, n3) % 12.33/3.58 | % 12.33/3.58 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.58 |-Branch one: % 12.33/3.58 | (53) green(n3, n6) % 12.33/3.58 | % 12.33/3.58 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.58 |-Branch one: % 12.33/3.58 | (54) green(n2, n6) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (2) with n6, n3, n2 and discharging atoms green(n3, n6), green(n2, n6), green(n2, n3), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (56) ~ green(n2, n6) % 12.33/3.58 | (57) red(n2, n6) % 12.33/3.58 | % 12.33/3.58 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.58 |-Branch one: % 12.33/3.58 | (77) green(n2, n5) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (2) with n5, n3, n2 and discharging atoms green(n3, n5), green(n2, n5), green(n2, n3), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (79) ~ green(n2, n5) % 12.33/3.58 | (80) red(n2, n5) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (10) with n6, n5, n2 and discharging atoms red(n5, n6), red(n2, n6), red(n2, n5), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (59) ~ green(n3, n6) % 12.33/3.58 | (60) red(n3, n6) % 12.33/3.58 | % 12.33/3.58 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.58 |-Branch one: % 12.33/3.58 | (54) green(n2, n6) % 12.33/3.58 | % 12.33/3.58 +-Applying beta-rule and splitting (35), into two cases. % 12.33/3.58 |-Branch one: % 12.33/3.58 | (62) green(n1, n6) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (2) with n6, n2, n1 and discharging atoms green(n2, n6), green(n1, n6), green(n1, n2), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (64) ~ green(n1, n6) % 12.33/3.58 | (65) red(n1, n6) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (10) with n6, n3, n1 and discharging atoms red(n3, n6), red(n1, n6), red(n1, n3), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (56) ~ green(n2, n6) % 12.33/3.58 | (57) red(n2, n6) % 12.33/3.58 | % 12.33/3.58 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.58 |-Branch one: % 12.33/3.58 | (77) green(n2, n5) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (2) with n5, n3, n2 and discharging atoms green(n3, n5), green(n2, n5), green(n2, n3), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (79) ~ green(n2, n5) % 12.33/3.58 | (80) red(n2, n5) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (10) with n6, n5, n2 and discharging atoms red(n5, n6), red(n2, n6), red(n2, n5), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (82) ~ green(n3, n5) % 12.33/3.58 | (83) red(n3, n5) % 12.33/3.58 | % 12.33/3.58 +-Applying beta-rule and splitting (28), into two cases. % 12.33/3.58 |-Branch one: % 12.33/3.58 | (49) green(n1, n3) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (2) with n3, n2, n1 and discharging atoms green(n2, n3), green(n1, n3), green(n1, n2), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (51) ~ green(n1, n3) % 12.33/3.58 | (52) red(n1, n3) % 12.33/3.58 | % 12.33/3.58 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.58 |-Branch one: % 12.33/3.58 | (53) green(n3, n6) % 12.33/3.58 | % 12.33/3.58 +-Applying beta-rule and splitting (30), into two cases. % 12.33/3.58 |-Branch one: % 12.33/3.58 | (54) green(n2, n6) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (2) with n6, n3, n2 and discharging atoms green(n3, n6), green(n2, n6), green(n2, n3), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (56) ~ green(n2, n6) % 12.33/3.58 | (57) red(n2, n6) % 12.33/3.58 | % 12.33/3.58 +-Applying beta-rule and splitting (32), into two cases. % 12.33/3.58 |-Branch one: % 12.33/3.58 | (88) green(n1, n5) % 12.33/3.58 | % 12.33/3.58 +-Applying beta-rule and splitting (31), into two cases. % 12.33/3.58 |-Branch one: % 12.33/3.58 | (77) green(n2, n5) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (2) with n5, n2, n1 and discharging atoms green(n2, n5), green(n1, n5), green(n1, n2), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (79) ~ green(n2, n5) % 12.33/3.58 | (80) red(n2, n5) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (10) with n6, n5, n2 and discharging atoms red(n5, n6), red(n2, n6), red(n2, n5), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (94) ~ green(n1, n5) % 12.33/3.58 | (95) red(n1, n5) % 12.33/3.58 | % 12.33/3.58 | Instantiating formula (10) with n5, n3, n1 and discharging atoms red(n3, n5), red(n1, n5), red(n1, n3), yields: % 12.33/3.58 | (42) $false % 12.33/3.58 | % 12.33/3.58 |-The branch is then unsatisfiable % 12.33/3.58 |-Branch two: % 12.33/3.58 | (59) ~ green(n3, n6) % 12.33/3.59 | (60) red(n3, n6) % 12.33/3.59 | % 12.33/3.59 | Instantiating formula (10) with n6, n5, n3 and discharging atoms red(n5, n6), red(n3, n6), red(n3, n5), yields: % 12.33/3.59 | (42) $false % 12.33/3.59 | % 12.33/3.59 |-The branch is then unsatisfiable % 12.33/3.59 |-Branch two: % 12.33/3.59 | (148) ~ green(n2, n3) % 12.33/3.59 | (149) red(n2, n3) % 12.33/3.59 | % 12.33/3.59 +-Applying beta-rule and splitting (11), into two cases. % 12.33/3.59 |-Branch one: % 12.33/3.59 | (39) green(n5, n6) % 12.33/3.59 | % 12.33/3.59 +-Applying beta-rule and splitting (13), into two cases. % 12.33/3.59 |-Branch one: % 12.33/3.59 | (40) green(n4, n5) % 12.33/3.59 | % 12.33/3.59 +-Applying beta-rule and splitting (25), into two cases. % 12.33/3.59 |-Branch one: % 12.33/3.59 | (41) green(n2, n4) % 12.33/3.59 | % 12.33/3.59 +-Applying beta-rule and splitting (22), into two cases. % 12.33/3.59 |-Branch one: % 12.33/3.59 | (76) green(n3, n5) % 12.33/3.59 | % 12.33/3.59 +-Applying beta-rule and splitting (20), into two cases. % 12.33/3.59 |-Branch one: % 12.33/3.59 | (45) green(n4, n6) % 12.33/3.59 | % 12.33/3.59 | Instantiating formula (2) with n6, n5, n4 and discharging atoms green(n5, n6), green(n4, n6), green(n4, n5), yields: % 12.33/3.59 | (42) $false % 12.33/3.59 | % 12.33/3.59 |-The branch is then unsatisfiable % 12.33/3.59 |-Branch two: % 12.33/3.59 | (47) ~ green(n4, n6) % 12.33/3.59 | (48) red(n4, n6) % 12.33/3.59 | % 12.33/3.59 +-Applying beta-rule and splitting (29), into two cases. % 12.33/3.59 |-Branch one: % 12.33/3.59 | (53) green(n3, n6) % 12.33/3.59 | % 12.33/3.59 | Instantiating formula (2) with n6, n5, n3 and discharging atoms green(n5, n6), green(n3, n6), green(n3, n5), yields: % 12.33/3.59 | (42) $false % 12.80/3.59 | % 12.80/3.59 |-The branch is then unsatisfiable % 12.80/3.59 |-Branch two: % 12.80/3.59 | (59) ~ green(n3, n6) % 12.80/3.59 | (60) red(n3, n6) % 12.80/3.59 | % 12.80/3.59 | Instantiating formula (10) with n6, n4, n3 and discharging atoms red(n4, n6), red(n3, n6), red(n3, n4), yields: % 12.80/3.59 | (42) $false % 12.80/3.59 | % 12.80/3.59 |-The branch is then unsatisfiable % 12.80/3.59 |-Branch two: % 12.80/3.59 | (82) ~ green(n3, n5) % 12.80/3.59 | (83) red(n3, n5) % 12.80/3.59 | % 12.80/3.59 +-Applying beta-rule and splitting (31), into two cases. % 12.80/3.59 |-Branch one: % 12.80/3.59 | (77) green(n2, n5) % 12.80/3.59 | % 12.80/3.59 | Instantiating formula (2) with n5, n4, n2 and discharging atoms green(n4, n5), green(n2, n5), green(n2, n4), yields: % 12.80/3.59 | (42) $false % 12.80/3.59 | % 12.80/3.59 |-The branch is then unsatisfiable % 12.80/3.59 |-Branch two: % 12.80/3.59 | (79) ~ green(n2, n5) % 12.80/3.59 | (80) red(n2, n5) % 12.80/3.59 | % 12.80/3.59 | Instantiating formula (10) with n5, n3, n2 and discharging atoms red(n3, n5), red(n2, n5), red(n2, n3), yields: % 12.80/3.59 | (42) $false % 12.80/3.59 | % 12.80/3.59 |-The branch is then unsatisfiable % 12.80/3.59 |-Branch two: % 12.80/3.59 | (43) ~ green(n2, n4) % 12.80/3.59 | (44) red(n2, n4) % 12.80/3.59 | % 12.80/3.59 | Instantiating formula (10) with n4, n3, n2 and discharging atoms red(n3, n4), red(n2, n4), red(n2, n3), yields: % 12.80/3.59 | (42) $false % 12.80/3.59 | % 12.80/3.59 |-The branch is then unsatisfiable % 12.80/3.59 |-Branch two: % 12.80/3.59 | (70) ~ green(n4, n5) % 12.80/3.59 | (71) red(n4, n5) % 12.80/3.59 | % 12.80/3.59 +-Applying beta-rule and splitting (25), into two cases. % 12.80/3.59 |-Branch one: % 12.80/3.59 | (41) green(n2, n4) % 12.80/3.59 | % 12.80/3.59 +-Applying beta-rule and splitting (22), into two cases. % 12.80/3.59 |-Branch one: % 12.80/3.59 | (76) green(n3, n5) % 12.80/3.59 | % 12.80/3.59 +-Applying beta-rule and splitting (20), into two cases. % 12.80/3.59 |-Branch one: % 12.80/3.59 | (45) green(n4, n6) % 12.80/3.59 | % 12.80/3.59 +-Applying beta-rule and splitting (29), into two cases. % 12.80/3.59 |-Branch one: % 12.80/3.59 | (53) green(n3, n6) % 12.80/3.59 | % 12.80/3.59 | Instantiating formula (2) with n6, n5, n3 and discharging atoms green(n5, n6), green(n3, n6), green(n3, n5), yields: % 12.80/3.59 | (42) $false % 12.80/3.59 | % 12.80/3.59 |-The branch is then unsatisfiable % 12.80/3.59 |-Branch two: % 12.80/3.59 | (59) ~ green(n3, n6) % 12.80/3.59 | (60) red(n3, n6) % 12.80/3.59 | % 12.80/3.59 +-Applying beta-rule and splitting (30), into two cases. % 12.80/3.59 |-Branch one: % 12.80/3.59 | (54) green(n2, n6) % 12.80/3.59 | % 12.80/3.59 | Instantiating formula (2) with n6, n4, n2 and discharging atoms green(n4, n6), green(n2, n6), green(n2, n4), yields: % 12.80/3.59 | (42) $false % 12.80/3.59 | % 12.80/3.59 |-The branch is then unsatisfiable % 12.80/3.59 |-Branch two: % 12.80/3.59 | (56) ~ green(n2, n6) % 12.80/3.59 | (57) red(n2, n6) % 12.80/3.59 | % 12.80/3.59 | Instantiating formula (10) with n6, n3, n2 and discharging atoms red(n3, n6), red(n2, n6), red(n2, n3), yields: % 12.80/3.59 | (42) $false % 12.80/3.59 | % 12.80/3.59 |-The branch is then unsatisfiable % 12.80/3.59 |-Branch two: % 12.80/3.59 | (47) ~ green(n4, n6) % 12.80/3.59 | (48) red(n4, n6) % 12.80/3.59 | % 12.80/3.59 +-Applying beta-rule and splitting (29), into two cases. % 12.80/3.59 |-Branch one: % 12.80/3.59 | (53) green(n3, n6) % 12.80/3.59 | % 12.80/3.59 | Instantiating formula (2) with n6, n5, n3 and discharging atoms green(n5, n6), green(n3, n6), green(n3, n5), yields: % 12.80/3.59 | (42) $false % 12.80/3.59 | % 12.80/3.59 |-The branch is then unsatisfiable % 12.80/3.59 |-Branch two: % 12.80/3.59 | (59) ~ green(n3, n6) % 12.80/3.59 | (60) red(n3, n6) % 12.80/3.59 | % 12.80/3.59 | Instantiating formula (10) with n6, n4, n3 and discharging atoms red(n4, n6), red(n3, n6), red(n3, n4), yields: % 12.80/3.59 | (42) $false % 12.80/3.59 | % 12.80/3.59 |-The branch is then unsatisfiable % 12.80/3.59 |-Branch two: % 12.80/3.59 | (82) ~ green(n3, n5) % 12.80/3.59 | (83) red(n3, n5) % 12.80/3.59 | % 12.80/3.59 | Instantiating formula (10) with n5, n4, n3 and discharging atoms red(n4, n5), red(n3, n5), red(n3, n4), yields: % 12.80/3.59 | (42) $false % 12.80/3.59 | % 12.80/3.59 |-The branch is then unsatisfiable % 12.80/3.59 |-Branch two: % 12.80/3.59 | (43) ~ green(n2, n4) % 12.80/3.59 | (44) red(n2, n4) % 12.80/3.59 | % 12.80/3.59 | Instantiating formula (10) with n4, n3, n2 and discharging atoms red(n3, n4), red(n2, n4), red(n2, n3), yields: % 12.80/3.59 | (42) $false % 12.80/3.59 | % 12.80/3.59 |-The branch is then unsatisfiable % 12.80/3.59 |-Branch two: % 12.80/3.59 | (97) ~ green(n5, n6) % 12.80/3.59 | (98) red(n5, n6) % 12.80/3.59 | % 12.80/3.59 +-Applying beta-rule and splitting (13), into two cases. % 12.80/3.59 |-Branch one: % 12.80/3.59 | (40) green(n4, n5) % 12.80/3.59 | % 12.80/3.59 +-Applying beta-rule and splitting (25), into two cases. % 12.80/3.59 |-Branch one: % 12.80/3.59 | (41) green(n2, n4) % 12.80/3.59 | % 12.80/3.59 +-Applying beta-rule and splitting (20), into two cases. % 12.80/3.59 |-Branch one: % 12.80/3.59 | (45) green(n4, n6) % 12.80/3.59 | % 12.80/3.59 +-Applying beta-rule and splitting (30), into two cases. % 12.80/3.59 |-Branch one: % 12.80/3.59 | (54) green(n2, n6) % 12.80/3.59 | % 12.80/3.59 | Instantiating formula (2) with n6, n4, n2 and discharging atoms green(n4, n6), green(n2, n6), green(n2, n4), yields: % 12.80/3.59 | (42) $false % 12.80/3.59 | % 12.80/3.59 |-The branch is then unsatisfiable % 12.80/3.59 |-Branch two: % 12.80/3.59 | (56) ~ green(n2, n6) % 12.80/3.59 | (57) red(n2, n6) % 12.80/3.59 | % 12.80/3.59 +-Applying beta-rule and splitting (31), into two cases. % 12.80/3.59 |-Branch one: % 12.80/3.59 | (77) green(n2, n5) % 12.80/3.59 | % 12.80/3.59 | Instantiating formula (2) with n5, n4, n2 and discharging atoms green(n4, n5), green(n2, n5), green(n2, n4), yields: % 12.80/3.59 | (42) $false % 12.80/3.59 | % 12.80/3.59 |-The branch is then unsatisfiable % 12.80/3.59 |-Branch two: % 12.80/3.59 | (79) ~ green(n2, n5) % 12.80/3.59 | (80) red(n2, n5) % 12.80/3.59 | % 12.80/3.59 | Instantiating formula (10) with n6, n5, n2 and discharging atoms red(n5, n6), red(n2, n6), red(n2, n5), yields: % 12.80/3.59 | (42) $false % 12.80/3.59 | % 12.80/3.59 |-The branch is then unsatisfiable % 12.80/3.59 |-Branch two: % 12.80/3.59 | (47) ~ green(n4, n6) % 12.80/3.59 | (48) red(n4, n6) % 12.80/3.59 | % 12.80/3.59 +-Applying beta-rule and splitting (30), into two cases. % 12.80/3.59 |-Branch one: % 12.80/3.59 | (54) green(n2, n6) % 12.80/3.59 | % 12.80/3.59 +-Applying beta-rule and splitting (34), into two cases. % 12.80/3.59 |-Branch one: % 12.80/3.59 | (190) green(n1, n4) % 12.80/3.59 | % 12.80/3.59 | Instantiating formula (2) with n4, n2, n1 and discharging atoms green(n2, n4), green(n1, n4), green(n1, n2), yields: % 12.80/3.59 | (42) $false % 12.80/3.59 | % 12.80/3.59 |-The branch is then unsatisfiable % 12.80/3.59 |-Branch two: % 12.80/3.59 | (192) ~ green(n1, n4) % 12.80/3.59 | (193) red(n1, n4) % 12.80/3.59 | % 12.80/3.59 +-Applying beta-rule and splitting (35), into two cases. % 12.80/3.59 |-Branch one: % 12.80/3.59 | (62) green(n1, n6) % 12.80/3.59 | % 12.80/3.59 | Instantiating formula (2) with n6, n2, n1 and discharging atoms green(n2, n6), green(n1, n6), green(n1, n2), yields: % 12.80/3.60 | (42) $false % 12.80/3.60 | % 12.80/3.60 |-The branch is then unsatisfiable % 12.80/3.60 |-Branch two: % 12.80/3.60 | (64) ~ green(n1, n6) % 12.80/3.60 | (65) red(n1, n6) % 12.80/3.60 | % 12.80/3.60 | Instantiating formula (10) with n6, n4, n1 and discharging atoms red(n4, n6), red(n1, n6), red(n1, n4), yields: % 12.80/3.60 | (42) $false % 12.80/3.60 | % 12.80/3.60 |-The branch is then unsatisfiable % 12.80/3.60 |-Branch two: % 12.80/3.60 | (56) ~ green(n2, n6) % 12.80/3.60 | (57) red(n2, n6) % 12.80/3.60 | % 12.80/3.60 +-Applying beta-rule and splitting (31), into two cases. % 12.80/3.60 |-Branch one: % 12.80/3.60 | (77) green(n2, n5) % 12.80/3.60 | % 12.80/3.60 | Instantiating formula (2) with n5, n4, n2 and discharging atoms green(n4, n5), green(n2, n5), green(n2, n4), yields: % 12.80/3.60 | (42) $false % 12.80/3.60 | % 12.80/3.60 |-The branch is then unsatisfiable % 12.80/3.60 |-Branch two: % 12.80/3.60 | (79) ~ green(n2, n5) % 12.80/3.60 | (80) red(n2, n5) % 12.80/3.60 | % 12.80/3.60 | Instantiating formula (10) with n6, n5, n2 and discharging atoms red(n5, n6), red(n2, n6), red(n2, n5), yields: % 12.80/3.60 | (42) $false % 12.80/3.60 | % 12.80/3.60 |-The branch is then unsatisfiable % 12.80/3.60 |-Branch two: % 12.80/3.60 | (43) ~ green(n2, n4) % 12.80/3.60 | (44) red(n2, n4) % 12.80/3.60 | % 12.80/3.60 | Instantiating formula (10) with n4, n3, n2 and discharging atoms red(n3, n4), red(n2, n4), red(n2, n3), yields: % 12.80/3.60 | (42) $false % 12.80/3.60 | % 12.80/3.60 |-The branch is then unsatisfiable % 12.80/3.60 |-Branch two: % 12.80/3.60 | (70) ~ green(n4, n5) % 12.80/3.60 | (71) red(n4, n5) % 12.80/3.60 | % 12.80/3.60 +-Applying beta-rule and splitting (25), into two cases. % 12.80/3.60 |-Branch one: % 12.80/3.60 | (41) green(n2, n4) % 12.80/3.60 | % 12.80/3.60 +-Applying beta-rule and splitting (22), into two cases. % 12.80/3.60 |-Branch one: % 12.80/3.60 | (76) green(n3, n5) % 12.80/3.60 | % 12.80/3.60 +-Applying beta-rule and splitting (28), into two cases. % 12.80/3.60 |-Branch one: % 12.80/3.60 | (49) green(n1, n3) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (32), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (88) green(n1, n5) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (2) with n5, n3, n1 and discharging atoms green(n3, n5), green(n1, n5), green(n1, n3), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (94) ~ green(n1, n5) % 12.85/3.60 | (95) red(n1, n5) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (34), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (190) green(n1, n4) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (2) with n4, n2, n1 and discharging atoms green(n2, n4), green(n1, n4), green(n1, n2), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (192) ~ green(n1, n4) % 12.85/3.60 | (193) red(n1, n4) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (10) with n5, n4, n1 and discharging atoms red(n4, n5), red(n1, n5), red(n1, n4), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (51) ~ green(n1, n3) % 12.85/3.60 | (52) red(n1, n3) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (34), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (190) green(n1, n4) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (2) with n4, n2, n1 and discharging atoms green(n2, n4), green(n1, n4), green(n1, n2), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (192) ~ green(n1, n4) % 12.85/3.60 | (193) red(n1, n4) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (10) with n4, n3, n1 and discharging atoms red(n3, n4), red(n1, n4), red(n1, n3), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (82) ~ green(n3, n5) % 12.85/3.60 | (83) red(n3, n5) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (10) with n5, n4, n3 and discharging atoms red(n4, n5), red(n3, n5), red(n3, n4), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (43) ~ green(n2, n4) % 12.85/3.60 | (44) red(n2, n4) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (10) with n4, n3, n2 and discharging atoms red(n3, n4), red(n2, n4), red(n2, n3), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (363) ~ green(n1, n2) % 12.85/3.60 | (364) red(n1, n2) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (17), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (38) green(n2, n3) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (11), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (39) green(n5, n6) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (13), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (40) green(n4, n5) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (22), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (76) green(n3, n5) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (20), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (45) green(n4, n6) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (2) with n6, n5, n4 and discharging atoms green(n5, n6), green(n4, n6), green(n4, n5), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (47) ~ green(n4, n6) % 12.85/3.60 | (48) red(n4, n6) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (29), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (53) green(n3, n6) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (2) with n6, n5, n3 and discharging atoms green(n5, n6), green(n3, n6), green(n3, n5), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (59) ~ green(n3, n6) % 12.85/3.60 | (60) red(n3, n6) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (10) with n6, n4, n3 and discharging atoms red(n4, n6), red(n3, n6), red(n3, n4), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (82) ~ green(n3, n5) % 12.85/3.60 | (83) red(n3, n5) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (20), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (45) green(n4, n6) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (2) with n6, n5, n4 and discharging atoms green(n5, n6), green(n4, n6), green(n4, n5), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (47) ~ green(n4, n6) % 12.85/3.60 | (48) red(n4, n6) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (28), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (49) green(n1, n3) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (29), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (53) green(n3, n6) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (30), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (54) green(n2, n6) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (2) with n6, n3, n2 and discharging atoms green(n3, n6), green(n2, n6), green(n2, n3), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (56) ~ green(n2, n6) % 12.85/3.60 | (57) red(n2, n6) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (35), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (62) green(n1, n6) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (2) with n6, n3, n1 and discharging atoms green(n3, n6), green(n1, n6), green(n1, n3), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (64) ~ green(n1, n6) % 12.85/3.60 | (65) red(n1, n6) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (10) with n6, n2, n1 and discharging atoms red(n2, n6), red(n1, n6), red(n1, n2), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (59) ~ green(n3, n6) % 12.85/3.60 | (60) red(n3, n6) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (10) with n6, n4, n3 and discharging atoms red(n4, n6), red(n3, n6), red(n3, n4), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (51) ~ green(n1, n3) % 12.85/3.60 | (52) red(n1, n3) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (32), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (88) green(n1, n5) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (34), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (190) green(n1, n4) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (2) with n5, n4, n1 and discharging atoms green(n4, n5), green(n1, n5), green(n1, n4), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (192) ~ green(n1, n4) % 12.85/3.60 | (193) red(n1, n4) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (10) with n4, n3, n1 and discharging atoms red(n3, n4), red(n1, n4), red(n1, n3), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (94) ~ green(n1, n5) % 12.85/3.60 | (95) red(n1, n5) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (10) with n5, n3, n1 and discharging atoms red(n3, n5), red(n1, n5), red(n1, n3), yields: % 12.85/3.60 | (42) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (70) ~ green(n4, n5) % 12.85/3.60 | (71) red(n4, n5) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (25), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (41) green(n2, n4) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (22), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (76) green(n3, n5) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (20), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (45) green(n4, n6) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (28), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (49) green(n1, n3) % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (32), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (88) green(n1, n5) % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (2) with n5, n3, n1 and discharging atoms green(n3, n5), green(n1, n5), green(n1, n3), yields: % 12.85/3.61 | (42) $false % 12.85/3.61 | % 12.85/3.61 |-The branch is then unsatisfiable % 12.85/3.61 |-Branch two: % 12.85/3.61 | (94) ~ green(n1, n5) % 12.85/3.61 | (95) red(n1, n5) % 12.85/3.61 | % 12.85/3.61 +-Applying beta-rule and splitting (31), into two cases. % 12.85/3.61 |-Branch one: % 12.85/3.61 | (77) green(n2, n5) % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (2) with n5, n3, n2 and discharging atoms green(n3, n5), green(n2, n5), green(n2, n3), yields: % 12.85/3.61 | (42) $false % 12.85/3.61 | % 12.85/3.61 |-The branch is then unsatisfiable % 12.85/3.61 |-Branch two: % 12.85/3.61 | (79) ~ green(n2, n5) % 12.85/3.61 | (80) red(n2, n5) % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (10) with n5, n2, n1 and discharging atoms red(n2, n5), red(n1, n5), red(n1, n2), yields: % 12.85/3.61 | (42) $false % 12.85/3.61 | % 12.85/3.61 |-The branch is then unsatisfiable % 12.85/3.61 |-Branch two: % 12.85/3.61 | (51) ~ green(n1, n3) % 12.85/3.61 | (52) red(n1, n3) % 12.85/3.61 | % 12.85/3.61 +-Applying beta-rule and splitting (30), into two cases. % 12.85/3.61 |-Branch one: % 12.85/3.61 | (54) green(n2, n6) % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (2) with n6, n4, n2 and discharging atoms green(n4, n6), green(n2, n6), green(n2, n4), yields: % 12.85/3.61 | (42) $false % 12.85/3.61 | % 12.85/3.61 |-The branch is then unsatisfiable % 12.85/3.61 |-Branch two: % 12.85/3.61 | (56) ~ green(n2, n6) % 12.85/3.61 | (57) red(n2, n6) % 12.85/3.61 | % 12.85/3.61 +-Applying beta-rule and splitting (34), into two cases. % 12.85/3.61 |-Branch one: % 12.85/3.61 | (190) green(n1, n4) % 12.85/3.61 | % 12.85/3.61 +-Applying beta-rule and splitting (35), into two cases. % 12.85/3.61 |-Branch one: % 12.85/3.61 | (62) green(n1, n6) % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (2) with n6, n4, n1 and discharging atoms green(n4, n6), green(n1, n6), green(n1, n4), yields: % 12.85/3.61 | (42) $false % 12.85/3.61 | % 12.85/3.61 |-The branch is then unsatisfiable % 12.85/3.61 |-Branch two: % 12.85/3.61 | (64) ~ green(n1, n6) % 12.85/3.61 | (65) red(n1, n6) % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (10) with n6, n2, n1 and discharging atoms red(n2, n6), red(n1, n6), red(n1, n2), yields: % 12.85/3.61 | (42) $false % 12.85/3.61 | % 12.85/3.61 |-The branch is then unsatisfiable % 12.85/3.61 |-Branch two: % 12.85/3.61 | (192) ~ green(n1, n4) % 12.85/3.61 | (193) red(n1, n4) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (10) with n4, n3, n1 and discharging atoms red(n3, n4), red(n1, n4), red(n1, n3), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (47) ~ green(n4, n6) % 12.89/3.61 | (48) red(n4, n6) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (29), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (53) green(n3, n6) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (2) with n6, n5, n3 and discharging atoms green(n5, n6), green(n3, n6), green(n3, n5), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (59) ~ green(n3, n6) % 12.89/3.61 | (60) red(n3, n6) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (10) with n6, n4, n3 and discharging atoms red(n4, n6), red(n3, n6), red(n3, n4), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (82) ~ green(n3, n5) % 12.89/3.61 | (83) red(n3, n5) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (10) with n5, n4, n3 and discharging atoms red(n4, n5), red(n3, n5), red(n3, n4), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (43) ~ green(n2, n4) % 12.89/3.61 | (44) red(n2, n4) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (22), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (76) green(n3, n5) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (31), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (77) green(n2, n5) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (2) with n5, n3, n2 and discharging atoms green(n3, n5), green(n2, n5), green(n2, n3), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (79) ~ green(n2, n5) % 12.89/3.61 | (80) red(n2, n5) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (10) with n5, n4, n2 and discharging atoms red(n4, n5), red(n2, n5), red(n2, n4), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (82) ~ green(n3, n5) % 12.89/3.61 | (83) red(n3, n5) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (10) with n5, n4, n3 and discharging atoms red(n4, n5), red(n3, n5), red(n3, n4), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (97) ~ green(n5, n6) % 12.89/3.61 | (98) red(n5, n6) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (13), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (40) green(n4, n5) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (25), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (41) green(n2, n4) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (22), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (76) green(n3, n5) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (20), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (45) green(n4, n6) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (30), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (54) green(n2, n6) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (2) with n6, n4, n2 and discharging atoms green(n4, n6), green(n2, n6), green(n2, n4), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (56) ~ green(n2, n6) % 12.89/3.61 | (57) red(n2, n6) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (31), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (77) green(n2, n5) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (2) with n5, n3, n2 and discharging atoms green(n3, n5), green(n2, n5), green(n2, n3), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (79) ~ green(n2, n5) % 12.89/3.61 | (80) red(n2, n5) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (10) with n6, n5, n2 and discharging atoms red(n5, n6), red(n2, n6), red(n2, n5), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (47) ~ green(n4, n6) % 12.89/3.61 | (48) red(n4, n6) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (29), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (53) green(n3, n6) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (30), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (54) green(n2, n6) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (2) with n6, n3, n2 and discharging atoms green(n3, n6), green(n2, n6), green(n2, n3), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (56) ~ green(n2, n6) % 12.89/3.61 | (57) red(n2, n6) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (31), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (77) green(n2, n5) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (2) with n5, n3, n2 and discharging atoms green(n3, n5), green(n2, n5), green(n2, n3), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (79) ~ green(n2, n5) % 12.89/3.61 | (80) red(n2, n5) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (10) with n6, n5, n2 and discharging atoms red(n5, n6), red(n2, n6), red(n2, n5), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (59) ~ green(n3, n6) % 12.89/3.61 | (60) red(n3, n6) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (10) with n6, n4, n3 and discharging atoms red(n4, n6), red(n3, n6), red(n3, n4), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (82) ~ green(n3, n5) % 12.89/3.61 | (83) red(n3, n5) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (29), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (53) green(n3, n6) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (30), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (54) green(n2, n6) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (2) with n6, n3, n2 and discharging atoms green(n3, n6), green(n2, n6), green(n2, n3), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (56) ~ green(n2, n6) % 12.89/3.61 | (57) red(n2, n6) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (31), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (77) green(n2, n5) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (2) with n5, n4, n2 and discharging atoms green(n4, n5), green(n2, n5), green(n2, n4), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (79) ~ green(n2, n5) % 12.89/3.61 | (80) red(n2, n5) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (10) with n6, n5, n2 and discharging atoms red(n5, n6), red(n2, n6), red(n2, n5), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (59) ~ green(n3, n6) % 12.89/3.61 | (60) red(n3, n6) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (10) with n6, n5, n3 and discharging atoms red(n5, n6), red(n3, n6), red(n3, n5), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (43) ~ green(n2, n4) % 12.89/3.61 | (44) red(n2, n4) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (22), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (76) green(n3, n5) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (32), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (88) green(n1, n5) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (34), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (190) green(n1, n4) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (2) with n5, n4, n1 and discharging atoms green(n4, n5), green(n1, n5), green(n1, n4), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (192) ~ green(n1, n4) % 12.89/3.61 | (193) red(n1, n4) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (10) with n4, n2, n1 and discharging atoms red(n2, n4), red(n1, n4), red(n1, n2), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (94) ~ green(n1, n5) % 12.89/3.61 | (95) red(n1, n5) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (31), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (77) green(n2, n5) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (2) with n5, n3, n2 and discharging atoms green(n3, n5), green(n2, n5), green(n2, n3), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (79) ~ green(n2, n5) % 12.89/3.61 | (80) red(n2, n5) % 12.89/3.61 | % 12.89/3.61 | Instantiating formula (10) with n5, n2, n1 and discharging atoms red(n2, n5), red(n1, n5), red(n1, n2), yields: % 12.89/3.61 | (42) $false % 12.89/3.61 | % 12.89/3.61 |-The branch is then unsatisfiable % 12.89/3.61 |-Branch two: % 12.89/3.61 | (82) ~ green(n3, n5) % 12.89/3.61 | (83) red(n3, n5) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (28), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (49) green(n1, n3) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (29), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (53) green(n3, n6) % 12.89/3.61 | % 12.89/3.61 +-Applying beta-rule and splitting (30), into two cases. % 12.89/3.61 |-Branch one: % 12.89/3.61 | (54) green(n2, n6) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (2) with n6, n3, n2 and discharging atoms green(n3, n6), green(n2, n6), green(n2, n3), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (56) ~ green(n2, n6) % 12.89/3.62 | (57) red(n2, n6) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (35), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (62) green(n1, n6) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (2) with n6, n3, n1 and discharging atoms green(n3, n6), green(n1, n6), green(n1, n3), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (64) ~ green(n1, n6) % 12.89/3.62 | (65) red(n1, n6) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n6, n2, n1 and discharging atoms red(n2, n6), red(n1, n6), red(n1, n2), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (59) ~ green(n3, n6) % 12.89/3.62 | (60) red(n3, n6) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n6, n5, n3 and discharging atoms red(n5, n6), red(n3, n6), red(n3, n5), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (51) ~ green(n1, n3) % 12.89/3.62 | (52) red(n1, n3) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (32), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (88) green(n1, n5) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (34), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (190) green(n1, n4) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (2) with n5, n4, n1 and discharging atoms green(n4, n5), green(n1, n5), green(n1, n4), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (192) ~ green(n1, n4) % 12.89/3.62 | (193) red(n1, n4) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n4, n2, n1 and discharging atoms red(n2, n4), red(n1, n4), red(n1, n2), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (94) ~ green(n1, n5) % 12.89/3.62 | (95) red(n1, n5) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n5, n3, n1 and discharging atoms red(n3, n5), red(n1, n5), red(n1, n3), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (70) ~ green(n4, n5) % 12.89/3.62 | (71) red(n4, n5) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (25), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (41) green(n2, n4) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (22), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (76) green(n3, n5) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (20), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (45) green(n4, n6) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (30), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (54) green(n2, n6) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (2) with n6, n4, n2 and discharging atoms green(n4, n6), green(n2, n6), green(n2, n4), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (56) ~ green(n2, n6) % 12.89/3.62 | (57) red(n2, n6) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (31), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (77) green(n2, n5) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (2) with n5, n3, n2 and discharging atoms green(n3, n5), green(n2, n5), green(n2, n3), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (79) ~ green(n2, n5) % 12.89/3.62 | (80) red(n2, n5) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n6, n5, n2 and discharging atoms red(n5, n6), red(n2, n6), red(n2, n5), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (47) ~ green(n4, n6) % 12.89/3.62 | (48) red(n4, n6) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n6, n5, n4 and discharging atoms red(n5, n6), red(n4, n6), red(n4, n5), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (82) ~ green(n3, n5) % 12.89/3.62 | (83) red(n3, n5) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n5, n4, n3 and discharging atoms red(n4, n5), red(n3, n5), red(n3, n4), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (43) ~ green(n2, n4) % 12.89/3.62 | (44) red(n2, n4) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (22), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (76) green(n3, n5) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (31), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (77) green(n2, n5) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (2) with n5, n3, n2 and discharging atoms green(n3, n5), green(n2, n5), green(n2, n3), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (79) ~ green(n2, n5) % 12.89/3.62 | (80) red(n2, n5) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n5, n4, n2 and discharging atoms red(n4, n5), red(n2, n5), red(n2, n4), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (82) ~ green(n3, n5) % 12.89/3.62 | (83) red(n3, n5) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n5, n4, n3 and discharging atoms red(n4, n5), red(n3, n5), red(n3, n4), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (148) ~ green(n2, n3) % 12.89/3.62 | (149) red(n2, n3) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (11), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (39) green(n5, n6) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (13), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (40) green(n4, n5) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (25), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (41) green(n2, n4) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (22), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (76) green(n3, n5) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (20), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (45) green(n4, n6) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (2) with n6, n5, n4 and discharging atoms green(n5, n6), green(n4, n6), green(n4, n5), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (47) ~ green(n4, n6) % 12.89/3.62 | (48) red(n4, n6) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (29), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (53) green(n3, n6) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (2) with n6, n5, n3 and discharging atoms green(n5, n6), green(n3, n6), green(n3, n5), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (59) ~ green(n3, n6) % 12.89/3.62 | (60) red(n3, n6) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n6, n4, n3 and discharging atoms red(n4, n6), red(n3, n6), red(n3, n4), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (82) ~ green(n3, n5) % 12.89/3.62 | (83) red(n3, n5) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (31), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (77) green(n2, n5) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (2) with n5, n4, n2 and discharging atoms green(n4, n5), green(n2, n5), green(n2, n4), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (79) ~ green(n2, n5) % 12.89/3.62 | (80) red(n2, n5) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n5, n3, n2 and discharging atoms red(n3, n5), red(n2, n5), red(n2, n3), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (43) ~ green(n2, n4) % 12.89/3.62 | (44) red(n2, n4) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n4, n3, n2 and discharging atoms red(n3, n4), red(n2, n4), red(n2, n3), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (70) ~ green(n4, n5) % 12.89/3.62 | (71) red(n4, n5) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (25), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (41) green(n2, n4) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (22), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (76) green(n3, n5) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (20), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (45) green(n4, n6) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (29), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (53) green(n3, n6) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (2) with n6, n5, n3 and discharging atoms green(n5, n6), green(n3, n6), green(n3, n5), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (59) ~ green(n3, n6) % 12.89/3.62 | (60) red(n3, n6) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (30), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (54) green(n2, n6) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (2) with n6, n4, n2 and discharging atoms green(n4, n6), green(n2, n6), green(n2, n4), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (56) ~ green(n2, n6) % 12.89/3.62 | (57) red(n2, n6) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n6, n3, n2 and discharging atoms red(n3, n6), red(n2, n6), red(n2, n3), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (47) ~ green(n4, n6) % 12.89/3.62 | (48) red(n4, n6) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (29), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (53) green(n3, n6) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (2) with n6, n5, n3 and discharging atoms green(n5, n6), green(n3, n6), green(n3, n5), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (59) ~ green(n3, n6) % 12.89/3.62 | (60) red(n3, n6) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n6, n4, n3 and discharging atoms red(n4, n6), red(n3, n6), red(n3, n4), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (82) ~ green(n3, n5) % 12.89/3.62 | (83) red(n3, n5) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n5, n4, n3 and discharging atoms red(n4, n5), red(n3, n5), red(n3, n4), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (43) ~ green(n2, n4) % 12.89/3.62 | (44) red(n2, n4) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n4, n3, n2 and discharging atoms red(n3, n4), red(n2, n4), red(n2, n3), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (97) ~ green(n5, n6) % 12.89/3.62 | (98) red(n5, n6) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (13), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (40) green(n4, n5) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (25), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (41) green(n2, n4) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (22), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (76) green(n3, n5) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (28), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (49) green(n1, n3) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (32), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (88) green(n1, n5) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (2) with n5, n3, n1 and discharging atoms green(n3, n5), green(n1, n5), green(n1, n3), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (94) ~ green(n1, n5) % 12.89/3.62 | (95) red(n1, n5) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (31), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (77) green(n2, n5) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (2) with n5, n4, n2 and discharging atoms green(n4, n5), green(n2, n5), green(n2, n4), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (79) ~ green(n2, n5) % 12.89/3.62 | (80) red(n2, n5) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n5, n2, n1 and discharging atoms red(n2, n5), red(n1, n5), red(n1, n2), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (51) ~ green(n1, n3) % 12.89/3.62 | (52) red(n1, n3) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n3, n2, n1 and discharging atoms red(n2, n3), red(n1, n3), red(n1, n2), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (82) ~ green(n3, n5) % 12.89/3.62 | (83) red(n3, n5) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (31), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (77) green(n2, n5) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (2) with n5, n4, n2 and discharging atoms green(n4, n5), green(n2, n5), green(n2, n4), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (79) ~ green(n2, n5) % 12.89/3.62 | (80) red(n2, n5) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n5, n3, n2 and discharging atoms red(n3, n5), red(n2, n5), red(n2, n3), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (43) ~ green(n2, n4) % 12.89/3.62 | (44) red(n2, n4) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (10) with n4, n3, n2 and discharging atoms red(n3, n4), red(n2, n4), red(n2, n3), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (70) ~ green(n4, n5) % 12.89/3.62 | (71) red(n4, n5) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (25), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (41) green(n2, n4) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (20), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (45) green(n4, n6) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (28), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (49) green(n1, n3) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (29), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (53) green(n3, n6) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (30), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.62 | (54) green(n2, n6) % 12.89/3.62 | % 12.89/3.62 | Instantiating formula (2) with n6, n4, n2 and discharging atoms green(n4, n6), green(n2, n6), green(n2, n4), yields: % 12.89/3.62 | (42) $false % 12.89/3.62 | % 12.89/3.62 |-The branch is then unsatisfiable % 12.89/3.62 |-Branch two: % 12.89/3.62 | (56) ~ green(n2, n6) % 12.89/3.62 | (57) red(n2, n6) % 12.89/3.62 | % 12.89/3.62 +-Applying beta-rule and splitting (35), into two cases. % 12.89/3.62 |-Branch one: % 12.89/3.63 | (62) green(n1, n6) % 12.89/3.63 | % 12.89/3.63 | Instantiating formula (2) with n6, n3, n1 and discharging atoms green(n3, n6), green(n1, n6), green(n1, n3), yields: % 12.89/3.63 | (42) $false % 12.89/3.63 | % 12.89/3.63 |-The branch is then unsatisfiable % 12.89/3.63 |-Branch two: % 12.89/3.63 | (64) ~ green(n1, n6) % 12.89/3.63 | (65) red(n1, n6) % 12.89/3.63 | % 12.89/3.63 | Instantiating formula (10) with n6, n2, n1 and discharging atoms red(n2, n6), red(n1, n6), red(n1, n2), yields: % 12.89/3.63 | (42) $false % 12.89/3.63 | % 12.89/3.63 |-The branch is then unsatisfiable % 12.89/3.63 |-Branch two: % 12.89/3.63 | (59) ~ green(n3, n6) % 12.89/3.63 | (60) red(n3, n6) % 12.89/3.63 | % 12.89/3.63 +-Applying beta-rule and splitting (30), into two cases. % 12.89/3.63 |-Branch one: % 12.89/3.63 | (54) green(n2, n6) % 12.89/3.63 | % 12.89/3.63 | Instantiating formula (2) with n6, n4, n2 and discharging atoms green(n4, n6), green(n2, n6), green(n2, n4), yields: % 12.89/3.63 | (42) $false % 12.89/3.63 | % 12.89/3.63 |-The branch is then unsatisfiable % 12.89/3.63 |-Branch two: % 12.89/3.63 | (56) ~ green(n2, n6) % 12.89/3.63 | (57) red(n2, n6) % 12.89/3.63 | % 12.89/3.63 | Instantiating formula (10) with n6, n3, n2 and discharging atoms red(n3, n6), red(n2, n6), red(n2, n3), yields: % 12.89/3.63 | (42) $false % 12.89/3.63 | % 12.89/3.63 |-The branch is then unsatisfiable % 12.89/3.63 |-Branch two: % 12.89/3.63 | (51) ~ green(n1, n3) % 12.89/3.63 | (52) red(n1, n3) % 12.89/3.63 | % 12.89/3.63 | Instantiating formula (10) with n3, n2, n1 and discharging atoms red(n2, n3), red(n1, n3), red(n1, n2), yields: % 12.89/3.63 | (42) $false % 12.89/3.63 | % 12.89/3.63 |-The branch is then unsatisfiable % 12.89/3.63 |-Branch two: % 12.89/3.63 | (47) ~ green(n4, n6) % 12.89/3.63 | (48) red(n4, n6) % 12.89/3.63 | % 12.89/3.63 | Instantiating formula (10) with n6, n5, n4 and discharging atoms red(n5, n6), red(n4, n6), red(n4, n5), yields: % 12.89/3.63 | (42) $false % 12.89/3.63 | % 12.89/3.63 |-The branch is then unsatisfiable % 12.89/3.63 |-Branch two: % 12.89/3.63 | (43) ~ green(n2, n4) % 12.89/3.63 | (44) red(n2, n4) % 12.89/3.63 | % 12.89/3.63 | Instantiating formula (10) with n4, n3, n2 and discharging atoms red(n3, n4), red(n2, n4), red(n2, n3), yields: % 12.89/3.63 | (42) $false % 12.89/3.63 | % 12.89/3.63 |-The branch is then unsatisfiable % 12.89/3.63 % SZS output end Proof for theBenchmark % 12.89/3.63 % 12.89/3.63 3022ms %------------------------------------------------------------------------------