%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : KRS081+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n029.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 : Sun Jul 17 02:56:30 EDT 2022 % Result : Unsatisfiable 61.32s 25.37s % Output : Proof 68.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : KRS081+1 : TPTP v8.1.0. Released v3.1.0. % 0.04/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.35 % Computer : n029.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Tue Jun 7 11:53:20 EDT 2022 % 0.13/0.35 % CPUTime : % 0.62/0.66 ____ _ % 0.62/0.66 ___ / __ \_____(_)___ ________ __________ % 0.62/0.66 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.62/0.66 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.62/0.66 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.62/0.66 % 0.62/0.66 A Theorem Prover for First-Order Logic % 0.62/0.66 (ePrincess v.1.0) % 0.62/0.66 % 0.62/0.66 (c) Philipp Rümmer, 2009-2015 % 0.62/0.66 (c) Peter Backeman, 2014-2015 % 0.62/0.66 (contributions by Angelo Brillout, Peter Baumgartner) % 0.62/0.66 Free software under GNU Lesser General Public License (LGPL). % 0.62/0.66 Bug reports to peter@backeman.se % 0.62/0.66 % 0.62/0.66 For more information, visit http://user.uu.se/~petba168/breu/ % 0.62/0.66 % 0.62/0.66 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.74/0.71 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.63/1.03 Prover 0: Preprocessing ... % 2.11/1.20 Prover 0: Warning: ignoring some quantifiers % 2.11/1.22 Prover 0: Constructing countermodel ... % 14.34/6.00 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 14.45/6.06 Prover 1: Preprocessing ... % 15.58/6.27 Prover 1: Constructing countermodel ... % 23.66/8.60 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 23.66/8.64 Prover 2: Preprocessing ... % 36.51/13.18 Prover 2: Warning: ignoring some quantifiers % 37.83/13.49 Prover 2: Constructing countermodel ... % 56.54/22.39 Prover 0: stopped % 56.74/22.59 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 56.79/22.62 Prover 3: Preprocessing ... % 56.79/22.64 Prover 3: Warning: ignoring some quantifiers % 56.79/22.65 Prover 3: Constructing countermodel ... % 61.32/25.36 Prover 3: proved (2775ms) % 61.32/25.37 Prover 1: stopped % 61.32/25.37 Prover 2: stopped % 61.32/25.37 % 61.32/25.37 No countermodel exists, formula is valid % 61.32/25.37 % SZS status Unsatisfiable for theBenchmark % 61.32/25.37 % 61.32/25.37 Generating proof ... Warning: ignoring some quantifiers % 68.08/29.19 found it (size 280) % 68.08/29.19 % 68.08/29.19 % SZS output start Proof for theBenchmark % 68.08/29.19 Assumed formulas after preprocessing and simplification: % 68.08/29.19 | (0) cUnsatisfiable(i2003_11_14_17_19_24236) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ rr(v0, v9) | ~ rr(v0, v8) | ~ rr(v0, v7) | ~ rr(v0, v6) | ~ rr(v0, v5) | ~ rr(v0, v4) | ~ rr(v0, v3) | ~ rr(v0, v2) | ~ rr(v0, v1) | ~ cp5(v5) | ~ cp4(v8) | ~ cp4(v7) | ~ cp3(v9) | ~ cp3(v4) | ~ cp2(v6) | ~ cp2(v1) | ~ cp1(v3) | ~ cp1(v2) | ~ cp(v8) | ~ cp(v6) | ~ cp(v4) | ~ cp(v2) | cUnsatisfiable(v0) | ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ( ~ (v14 = v13) & ~ (v14 = v12) & ~ (v14 = v11) & ~ (v14 = v10) & ~ (v13 = v12) & ~ (v13 = v11) & ~ (v13 = v10) & ~ (v12 = v11) & ~ (v12 = v10) & ~ (v11 = v10) & rr(v0, v14) & rr(v0, v13) & rr(v0, v12) & rr(v0, v11) & rr(v0, v10))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = v4 | v5 = v3 | v5 = v2 | v5 = v1 | v4 = v3 | v4 = v2 | v4 = v1 | v3 = v2 | v3 = v1 | v2 = v1 | ~ rr(v0, v5) | ~ rr(v0, v4) | ~ rr(v0, v3) | ~ rr(v0, v2) | ~ rr(v0, v1) | ~ cUnsatisfiable(v0)) & ! [v0] : ( ~ xsd_string(v0) | ~ xsd_integer(v0)) & ! [v0] : ( ~ cp5(v0) | ~ cp4(v0)) & ! [v0] : ( ~ cp5(v0) | ~ cp3(v0)) & ! [v0] : ( ~ cp5(v0) | ~ cp2(v0)) & ! [v0] : ( ~ cp5(v0) | ~ cp1(v0)) & ! [v0] : ( ~ cp4(v0) | ~ cp3(v0)) & ! [v0] : ( ~ cp4(v0) | ~ cp2(v0)) & ! [v0] : ( ~ cp4(v0) | ~ cp1(v0)) & ! [v0] : ( ~ cp3(v0) | ~ cp2(v0)) & ! [v0] : ( ~ cp3(v0) | ~ cp1(v0)) & ! [v0] : ( ~ cp2(v0) | ~ cp1(v0)) & ! [v0] : ~ cowlNothing(v0) & ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp5(v1))) & ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp4(v1) & cp(v1))) & ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp4(v1))) & ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp3(v1) & cp(v1))) & ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp3(v1))) & ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp2(v1) & cp(v1))) & ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp2(v1))) & ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp1(v1) & cp(v1))) & ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp1(v1))) & ? [v0] : (xsd_string(v0) | xsd_integer(v0)) & ? [v0] : cowlThing(v0) % 68.08/29.20 | Applying alpha-rule on (0) yields: % 68.08/29.20 | (1) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp1(v1) & cp(v1))) % 68.08/29.20 | (2) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp5(v1))) % 68.08/29.20 | (3) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp3(v1))) % 68.08/29.20 | (4) ! [v0] : ( ~ cp4(v0) | ~ cp3(v0)) % 68.08/29.20 | (5) ! [v0] : ( ~ cp3(v0) | ~ cp1(v0)) % 68.08/29.20 | (6) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp4(v1) & cp(v1))) % 68.08/29.20 | (7) ! [v0] : ( ~ cp5(v0) | ~ cp3(v0)) % 68.08/29.20 | (8) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp2(v1))) % 68.08/29.20 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ rr(v0, v9) | ~ rr(v0, v8) | ~ rr(v0, v7) | ~ rr(v0, v6) | ~ rr(v0, v5) | ~ rr(v0, v4) | ~ rr(v0, v3) | ~ rr(v0, v2) | ~ rr(v0, v1) | ~ cp5(v5) | ~ cp4(v8) | ~ cp4(v7) | ~ cp3(v9) | ~ cp3(v4) | ~ cp2(v6) | ~ cp2(v1) | ~ cp1(v3) | ~ cp1(v2) | ~ cp(v8) | ~ cp(v6) | ~ cp(v4) | ~ cp(v2) | cUnsatisfiable(v0) | ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ( ~ (v14 = v13) & ~ (v14 = v12) & ~ (v14 = v11) & ~ (v14 = v10) & ~ (v13 = v12) & ~ (v13 = v11) & ~ (v13 = v10) & ~ (v12 = v11) & ~ (v12 = v10) & ~ (v11 = v10) & rr(v0, v14) & rr(v0, v13) & rr(v0, v12) & rr(v0, v11) & rr(v0, v10))) % 68.08/29.21 | (10) ! [v0] : ( ~ cp2(v0) | ~ cp1(v0)) % 68.08/29.21 | (11) ? [v0] : cowlThing(v0) % 68.08/29.21 | (12) ! [v0] : ( ~ cp5(v0) | ~ cp1(v0)) % 68.08/29.21 | (13) ! [v0] : ( ~ cp3(v0) | ~ cp2(v0)) % 68.08/29.21 | (14) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp2(v1) & cp(v1))) % 68.08/29.21 | (15) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp4(v1))) % 68.08/29.21 | (16) ! [v0] : ( ~ cp5(v0) | ~ cp4(v0)) % 68.08/29.21 | (17) ! [v0] : ~ cowlNothing(v0) % 68.08/29.21 | (18) ! [v0] : ( ~ cp5(v0) | ~ cp2(v0)) % 68.08/29.21 | (19) cUnsatisfiable(i2003_11_14_17_19_24236) % 68.08/29.21 | (20) ! [v0] : ( ~ xsd_string(v0) | ~ xsd_integer(v0)) % 68.08/29.21 | (21) ! [v0] : ( ~ cp4(v0) | ~ cp2(v0)) % 68.08/29.21 | (22) ! [v0] : ( ~ cp4(v0) | ~ cp1(v0)) % 68.08/29.21 | (23) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = v4 | v5 = v3 | v5 = v2 | v5 = v1 | v4 = v3 | v4 = v2 | v4 = v1 | v3 = v2 | v3 = v1 | v2 = v1 | ~ rr(v0, v5) | ~ rr(v0, v4) | ~ rr(v0, v3) | ~ rr(v0, v2) | ~ rr(v0, v1) | ~ cUnsatisfiable(v0)) % 68.08/29.21 | (24) ? [v0] : (xsd_string(v0) | xsd_integer(v0)) % 68.08/29.21 | (25) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp1(v1))) % 68.08/29.21 | (26) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp3(v1) & cp(v1))) % 68.08/29.21 | % 68.08/29.21 | Instantiating formula (2) with i2003_11_14_17_19_24236 and discharging atoms cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.21 | (27) ? [v0] : (rr(i2003_11_14_17_19_24236, v0) & cp5(v0)) % 68.08/29.21 | % 68.08/29.21 | Instantiating formula (6) with i2003_11_14_17_19_24236 and discharging atoms cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.21 | (28) ? [v0] : (rr(i2003_11_14_17_19_24236, v0) & cp4(v0) & cp(v0)) % 68.08/29.21 | % 68.08/29.21 | Instantiating formula (15) with i2003_11_14_17_19_24236 and discharging atoms cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.21 | (29) ? [v0] : (rr(i2003_11_14_17_19_24236, v0) & cp4(v0)) % 68.08/29.21 | % 68.08/29.21 | Instantiating formula (26) with i2003_11_14_17_19_24236 and discharging atoms cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.21 | (30) ? [v0] : (rr(i2003_11_14_17_19_24236, v0) & cp3(v0) & cp(v0)) % 68.08/29.21 | % 68.08/29.21 | Instantiating formula (3) with i2003_11_14_17_19_24236 and discharging atoms cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.21 | (31) ? [v0] : (rr(i2003_11_14_17_19_24236, v0) & cp3(v0)) % 68.08/29.21 | % 68.08/29.21 | Instantiating formula (14) with i2003_11_14_17_19_24236 and discharging atoms cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.21 | (32) ? [v0] : (rr(i2003_11_14_17_19_24236, v0) & cp2(v0) & cp(v0)) % 68.08/29.21 | % 68.08/29.21 | Instantiating formula (8) with i2003_11_14_17_19_24236 and discharging atoms cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.21 | (33) ? [v0] : (rr(i2003_11_14_17_19_24236, v0) & cp2(v0)) % 68.08/29.21 | % 68.08/29.21 | Instantiating formula (1) with i2003_11_14_17_19_24236 and discharging atoms cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.21 | (34) ? [v0] : (rr(i2003_11_14_17_19_24236, v0) & cp1(v0) & cp(v0)) % 68.08/29.21 | % 68.08/29.21 | Instantiating formula (25) with i2003_11_14_17_19_24236 and discharging atoms cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.21 | (35) ? [v0] : (rr(i2003_11_14_17_19_24236, v0) & cp1(v0)) % 68.08/29.21 | % 68.08/29.21 | Instantiating (35) with all_10_0_2 yields: % 68.08/29.21 | (36) rr(i2003_11_14_17_19_24236, all_10_0_2) & cp1(all_10_0_2) % 68.08/29.21 | % 68.08/29.21 | Applying alpha-rule on (36) yields: % 68.08/29.21 | (37) rr(i2003_11_14_17_19_24236, all_10_0_2) % 68.08/29.21 | (38) cp1(all_10_0_2) % 68.08/29.21 | % 68.08/29.21 | Instantiating (33) with all_12_0_3 yields: % 68.08/29.21 | (39) rr(i2003_11_14_17_19_24236, all_12_0_3) & cp2(all_12_0_3) % 68.08/29.21 | % 68.08/29.21 | Applying alpha-rule on (39) yields: % 68.08/29.21 | (40) rr(i2003_11_14_17_19_24236, all_12_0_3) % 68.08/29.21 | (41) cp2(all_12_0_3) % 68.08/29.21 | % 68.08/29.21 | Instantiating (32) with all_14_0_4 yields: % 68.08/29.21 | (42) rr(i2003_11_14_17_19_24236, all_14_0_4) & cp2(all_14_0_4) & cp(all_14_0_4) % 68.08/29.21 | % 68.08/29.21 | Applying alpha-rule on (42) yields: % 68.08/29.21 | (43) rr(i2003_11_14_17_19_24236, all_14_0_4) % 68.08/29.22 | (44) cp2(all_14_0_4) % 68.08/29.22 | (45) cp(all_14_0_4) % 68.08/29.22 | % 68.08/29.22 | Instantiating (31) with all_16_0_5 yields: % 68.08/29.22 | (46) rr(i2003_11_14_17_19_24236, all_16_0_5) & cp3(all_16_0_5) % 68.08/29.22 | % 68.08/29.22 | Applying alpha-rule on (46) yields: % 68.08/29.22 | (47) rr(i2003_11_14_17_19_24236, all_16_0_5) % 68.08/29.22 | (48) cp3(all_16_0_5) % 68.08/29.22 | % 68.08/29.22 | Instantiating (34) with all_18_0_6 yields: % 68.08/29.22 | (49) rr(i2003_11_14_17_19_24236, all_18_0_6) & cp1(all_18_0_6) & cp(all_18_0_6) % 68.08/29.22 | % 68.08/29.22 | Applying alpha-rule on (49) yields: % 68.08/29.22 | (50) rr(i2003_11_14_17_19_24236, all_18_0_6) % 68.08/29.22 | (51) cp1(all_18_0_6) % 68.08/29.22 | (52) cp(all_18_0_6) % 68.08/29.22 | % 68.08/29.22 | Instantiating (29) with all_20_0_7 yields: % 68.08/29.22 | (53) rr(i2003_11_14_17_19_24236, all_20_0_7) & cp4(all_20_0_7) % 68.08/29.22 | % 68.08/29.22 | Applying alpha-rule on (53) yields: % 68.08/29.22 | (54) rr(i2003_11_14_17_19_24236, all_20_0_7) % 68.08/29.22 | (55) cp4(all_20_0_7) % 68.08/29.22 | % 68.08/29.22 | Instantiating (28) with all_22_0_8 yields: % 68.08/29.22 | (56) rr(i2003_11_14_17_19_24236, all_22_0_8) & cp4(all_22_0_8) & cp(all_22_0_8) % 68.08/29.22 | % 68.08/29.22 | Applying alpha-rule on (56) yields: % 68.08/29.22 | (57) rr(i2003_11_14_17_19_24236, all_22_0_8) % 68.08/29.22 | (58) cp4(all_22_0_8) % 68.08/29.22 | (59) cp(all_22_0_8) % 68.08/29.22 | % 68.08/29.22 | Instantiating (27) with all_24_0_9 yields: % 68.08/29.22 | (60) rr(i2003_11_14_17_19_24236, all_24_0_9) & cp5(all_24_0_9) % 68.08/29.22 | % 68.08/29.22 | Applying alpha-rule on (60) yields: % 68.08/29.22 | (61) rr(i2003_11_14_17_19_24236, all_24_0_9) % 68.08/29.22 | (62) cp5(all_24_0_9) % 68.08/29.22 | % 68.08/29.22 | Instantiating (30) with all_26_0_10 yields: % 68.08/29.22 | (63) rr(i2003_11_14_17_19_24236, all_26_0_10) & cp3(all_26_0_10) & cp(all_26_0_10) % 68.08/29.22 | % 68.08/29.22 | Applying alpha-rule on (63) yields: % 68.08/29.22 | (64) rr(i2003_11_14_17_19_24236, all_26_0_10) % 68.08/29.22 | (65) cp3(all_26_0_10) % 68.08/29.22 | (66) cp(all_26_0_10) % 68.08/29.22 | % 68.08/29.22 | Instantiating formula (23) with all_12_0_3, all_26_0_10, all_22_0_8, all_20_0_7, all_18_0_6, i2003_11_14_17_19_24236 and discharging atoms rr(i2003_11_14_17_19_24236, all_26_0_10), rr(i2003_11_14_17_19_24236, all_22_0_8), rr(i2003_11_14_17_19_24236, all_20_0_7), rr(i2003_11_14_17_19_24236, all_18_0_6), rr(i2003_11_14_17_19_24236, all_12_0_3), cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.22 | (67) all_26_0_10 = all_22_0_8 | all_26_0_10 = all_20_0_7 | all_26_0_10 = all_18_0_6 | all_26_0_10 = all_12_0_3 | all_22_0_8 = all_20_0_7 | all_22_0_8 = all_18_0_6 | all_22_0_8 = all_12_0_3 | all_20_0_7 = all_18_0_6 | all_20_0_7 = all_12_0_3 | all_18_0_6 = all_12_0_3 % 68.08/29.22 | % 68.08/29.22 | Instantiating formula (23) with all_12_0_3, all_26_0_10, all_22_0_8, all_18_0_6, all_16_0_5, i2003_11_14_17_19_24236 and discharging atoms rr(i2003_11_14_17_19_24236, all_26_0_10), rr(i2003_11_14_17_19_24236, all_22_0_8), rr(i2003_11_14_17_19_24236, all_18_0_6), rr(i2003_11_14_17_19_24236, all_16_0_5), rr(i2003_11_14_17_19_24236, all_12_0_3), cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.22 | (68) all_26_0_10 = all_22_0_8 | all_26_0_10 = all_18_0_6 | all_26_0_10 = all_16_0_5 | all_26_0_10 = all_12_0_3 | all_22_0_8 = all_18_0_6 | all_22_0_8 = all_16_0_5 | all_22_0_8 = all_12_0_3 | all_18_0_6 = all_16_0_5 | all_18_0_6 = all_12_0_3 | all_16_0_5 = all_12_0_3 % 68.08/29.22 | % 68.08/29.22 | Instantiating formula (23) with all_12_0_3, all_26_0_10, all_20_0_7, all_18_0_6, all_16_0_5, i2003_11_14_17_19_24236 and discharging atoms rr(i2003_11_14_17_19_24236, all_26_0_10), rr(i2003_11_14_17_19_24236, all_20_0_7), rr(i2003_11_14_17_19_24236, all_18_0_6), rr(i2003_11_14_17_19_24236, all_16_0_5), rr(i2003_11_14_17_19_24236, all_12_0_3), cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.22 | (69) all_26_0_10 = all_20_0_7 | all_26_0_10 = all_18_0_6 | all_26_0_10 = all_16_0_5 | all_26_0_10 = all_12_0_3 | all_20_0_7 = all_18_0_6 | all_20_0_7 = all_16_0_5 | all_20_0_7 = all_12_0_3 | all_18_0_6 = all_16_0_5 | all_18_0_6 = all_12_0_3 | all_16_0_5 = all_12_0_3 % 68.08/29.22 | % 68.08/29.22 | Instantiating formula (23) with all_12_0_3, all_20_0_7, all_18_0_6, all_16_0_5, all_14_0_4, i2003_11_14_17_19_24236 and discharging atoms rr(i2003_11_14_17_19_24236, all_20_0_7), rr(i2003_11_14_17_19_24236, all_18_0_6), rr(i2003_11_14_17_19_24236, all_16_0_5), rr(i2003_11_14_17_19_24236, all_14_0_4), rr(i2003_11_14_17_19_24236, all_12_0_3), cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.22 | (70) all_20_0_7 = all_18_0_6 | all_20_0_7 = all_16_0_5 | all_20_0_7 = all_14_0_4 | all_20_0_7 = all_12_0_3 | all_18_0_6 = all_16_0_5 | all_18_0_6 = all_14_0_4 | all_18_0_6 = all_12_0_3 | all_16_0_5 = all_14_0_4 | all_16_0_5 = all_12_0_3 | all_14_0_4 = all_12_0_3 % 68.08/29.22 | % 68.08/29.22 | Instantiating formula (23) with all_10_0_2, all_26_0_10, all_24_0_9, all_20_0_7, all_16_0_5, i2003_11_14_17_19_24236 and discharging atoms rr(i2003_11_14_17_19_24236, all_26_0_10), rr(i2003_11_14_17_19_24236, all_24_0_9), rr(i2003_11_14_17_19_24236, all_20_0_7), rr(i2003_11_14_17_19_24236, all_16_0_5), rr(i2003_11_14_17_19_24236, all_10_0_2), cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.22 | (71) all_26_0_10 = all_24_0_9 | all_26_0_10 = all_20_0_7 | all_26_0_10 = all_16_0_5 | all_26_0_10 = all_10_0_2 | all_24_0_9 = all_20_0_7 | all_24_0_9 = all_16_0_5 | all_24_0_9 = all_10_0_2 | all_20_0_7 = all_16_0_5 | all_20_0_7 = all_10_0_2 | all_16_0_5 = all_10_0_2 % 68.08/29.22 | % 68.08/29.22 | Instantiating formula (23) with all_10_0_2, all_26_0_10, all_24_0_9, all_20_0_7, all_14_0_4, i2003_11_14_17_19_24236 and discharging atoms rr(i2003_11_14_17_19_24236, all_26_0_10), rr(i2003_11_14_17_19_24236, all_24_0_9), rr(i2003_11_14_17_19_24236, all_20_0_7), rr(i2003_11_14_17_19_24236, all_14_0_4), rr(i2003_11_14_17_19_24236, all_10_0_2), cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.22 | (72) all_26_0_10 = all_24_0_9 | all_26_0_10 = all_20_0_7 | all_26_0_10 = all_14_0_4 | all_26_0_10 = all_10_0_2 | all_24_0_9 = all_20_0_7 | all_24_0_9 = all_14_0_4 | all_24_0_9 = all_10_0_2 | all_20_0_7 = all_14_0_4 | all_20_0_7 = all_10_0_2 | all_14_0_4 = all_10_0_2 % 68.08/29.22 | % 68.08/29.22 | Instantiating formula (23) with all_10_0_2, all_26_0_10, all_24_0_9, all_20_0_7, all_12_0_3, i2003_11_14_17_19_24236 and discharging atoms rr(i2003_11_14_17_19_24236, all_26_0_10), rr(i2003_11_14_17_19_24236, all_24_0_9), rr(i2003_11_14_17_19_24236, all_20_0_7), rr(i2003_11_14_17_19_24236, all_12_0_3), rr(i2003_11_14_17_19_24236, all_10_0_2), cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.22 | (73) all_26_0_10 = all_24_0_9 | all_26_0_10 = all_20_0_7 | all_26_0_10 = all_12_0_3 | all_26_0_10 = all_10_0_2 | all_24_0_9 = all_20_0_7 | all_24_0_9 = all_12_0_3 | all_24_0_9 = all_10_0_2 | all_20_0_7 = all_12_0_3 | all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.08/29.22 | % 68.08/29.22 | Instantiating formula (23) with all_10_0_2, all_26_0_10, all_22_0_8, all_20_0_7, all_16_0_5, i2003_11_14_17_19_24236 and discharging atoms rr(i2003_11_14_17_19_24236, all_26_0_10), rr(i2003_11_14_17_19_24236, all_22_0_8), rr(i2003_11_14_17_19_24236, all_20_0_7), rr(i2003_11_14_17_19_24236, all_16_0_5), rr(i2003_11_14_17_19_24236, all_10_0_2), cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.22 | (74) all_26_0_10 = all_22_0_8 | all_26_0_10 = all_20_0_7 | all_26_0_10 = all_16_0_5 | all_26_0_10 = all_10_0_2 | all_22_0_8 = all_20_0_7 | all_22_0_8 = all_16_0_5 | all_22_0_8 = all_10_0_2 | all_20_0_7 = all_16_0_5 | all_20_0_7 = all_10_0_2 | all_16_0_5 = all_10_0_2 % 68.08/29.22 | % 68.08/29.22 | Instantiating formula (23) with all_10_0_2, all_26_0_10, all_22_0_8, all_20_0_7, all_12_0_3, i2003_11_14_17_19_24236 and discharging atoms rr(i2003_11_14_17_19_24236, all_26_0_10), rr(i2003_11_14_17_19_24236, all_22_0_8), rr(i2003_11_14_17_19_24236, all_20_0_7), rr(i2003_11_14_17_19_24236, all_12_0_3), rr(i2003_11_14_17_19_24236, all_10_0_2), cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.22 | (75) all_26_0_10 = all_22_0_8 | all_26_0_10 = all_20_0_7 | all_26_0_10 = all_12_0_3 | all_26_0_10 = all_10_0_2 | all_22_0_8 = all_20_0_7 | all_22_0_8 = all_12_0_3 | all_22_0_8 = all_10_0_2 | all_20_0_7 = all_12_0_3 | all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.08/29.22 | % 68.08/29.22 | Instantiating formula (23) with all_10_0_2, all_26_0_10, all_22_0_8, all_18_0_6, all_16_0_5, i2003_11_14_17_19_24236 and discharging atoms rr(i2003_11_14_17_19_24236, all_26_0_10), rr(i2003_11_14_17_19_24236, all_22_0_8), rr(i2003_11_14_17_19_24236, all_18_0_6), rr(i2003_11_14_17_19_24236, all_16_0_5), rr(i2003_11_14_17_19_24236, all_10_0_2), cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.22 | (76) all_26_0_10 = all_22_0_8 | all_26_0_10 = all_18_0_6 | all_26_0_10 = all_16_0_5 | all_26_0_10 = all_10_0_2 | all_22_0_8 = all_18_0_6 | all_22_0_8 = all_16_0_5 | all_22_0_8 = all_10_0_2 | all_18_0_6 = all_16_0_5 | all_18_0_6 = all_10_0_2 | all_16_0_5 = all_10_0_2 % 68.08/29.22 | % 68.08/29.22 | Instantiating formula (23) with all_10_0_2, all_26_0_10, all_22_0_8, all_16_0_5, all_14_0_4, i2003_11_14_17_19_24236 and discharging atoms rr(i2003_11_14_17_19_24236, all_26_0_10), rr(i2003_11_14_17_19_24236, all_22_0_8), rr(i2003_11_14_17_19_24236, all_16_0_5), rr(i2003_11_14_17_19_24236, all_14_0_4), rr(i2003_11_14_17_19_24236, all_10_0_2), cUnsatisfiable(i2003_11_14_17_19_24236), yields: % 68.08/29.22 | (77) all_26_0_10 = all_22_0_8 | all_26_0_10 = all_16_0_5 | all_26_0_10 = all_14_0_4 | all_26_0_10 = all_10_0_2 | all_22_0_8 = all_16_0_5 | all_22_0_8 = all_14_0_4 | all_22_0_8 = all_10_0_2 | all_16_0_5 = all_14_0_4 | all_16_0_5 = all_10_0_2 | all_14_0_4 = all_10_0_2 % 68.08/29.22 | % 68.08/29.22 | Instantiating formula (16) with all_20_0_7 and discharging atoms cp4(all_20_0_7), yields: % 68.08/29.22 | (78) ~ cp5(all_20_0_7) % 68.08/29.22 | % 68.08/29.22 | Instantiating formula (7) with all_24_0_9 and discharging atoms cp5(all_24_0_9), yields: % 68.08/29.22 | (79) ~ cp3(all_24_0_9) % 68.08/29.22 | % 68.08/29.23 | Instantiating formula (4) with all_22_0_8 and discharging atoms cp4(all_22_0_8), yields: % 68.08/29.23 | (80) ~ cp3(all_22_0_8) % 68.08/29.23 | % 68.08/29.23 | Instantiating formula (4) with all_20_0_7 and discharging atoms cp4(all_20_0_7), yields: % 68.08/29.23 | (81) ~ cp3(all_20_0_7) % 68.08/29.23 | % 68.08/29.23 | Instantiating formula (4) with all_16_0_5 and discharging atoms cp3(all_16_0_5), yields: % 68.08/29.23 | (82) ~ cp4(all_16_0_5) % 68.08/29.23 | % 68.08/29.23 | Instantiating formula (18) with all_14_0_4 and discharging atoms cp2(all_14_0_4), yields: % 68.08/29.23 | (83) ~ cp5(all_14_0_4) % 68.08/29.23 | % 68.08/29.23 | Instantiating formula (21) with all_14_0_4 and discharging atoms cp2(all_14_0_4), yields: % 68.08/29.23 | (84) ~ cp4(all_14_0_4) % 68.08/29.23 | % 68.08/29.23 | Instantiating formula (13) with all_14_0_4 and discharging atoms cp2(all_14_0_4), yields: % 68.08/29.23 | (85) ~ cp3(all_14_0_4) % 68.08/29.23 | % 68.08/29.23 | Instantiating formula (21) with all_12_0_3 and discharging atoms cp2(all_12_0_3), yields: % 68.08/29.23 | (86) ~ cp4(all_12_0_3) % 68.08/29.23 | % 68.08/29.23 | Instantiating formula (13) with all_12_0_3 and discharging atoms cp2(all_12_0_3), yields: % 68.08/29.23 | (87) ~ cp3(all_12_0_3) % 68.08/29.23 | % 68.08/29.23 | Instantiating formula (22) with all_18_0_6 and discharging atoms cp1(all_18_0_6), yields: % 68.08/29.23 | (88) ~ cp4(all_18_0_6) % 68.08/29.23 | % 68.08/29.23 | Instantiating formula (5) with all_18_0_6 and discharging atoms cp1(all_18_0_6), yields: % 68.08/29.23 | (89) ~ cp3(all_18_0_6) % 68.08/29.23 | % 68.08/29.23 | Instantiating formula (10) with all_14_0_4 and discharging atoms cp2(all_14_0_4), yields: % 68.08/29.23 | (90) ~ cp1(all_14_0_4) % 68.08/29.23 | % 68.08/29.23 | Instantiating formula (10) with all_12_0_3 and discharging atoms cp2(all_12_0_3), yields: % 68.08/29.23 | (91) ~ cp1(all_12_0_3) % 68.08/29.23 | % 68.08/29.23 | Instantiating formula (12) with all_10_0_2 and discharging atoms cp1(all_10_0_2), yields: % 68.08/29.23 | (92) ~ cp5(all_10_0_2) % 68.08/29.23 | % 68.08/29.23 | Instantiating formula (22) with all_10_0_2 and discharging atoms cp1(all_10_0_2), yields: % 68.08/29.23 | (93) ~ cp4(all_10_0_2) % 68.08/29.23 | % 68.08/29.23 | Instantiating formula (5) with all_10_0_2 and discharging atoms cp1(all_10_0_2), yields: % 68.08/29.23 | (94) ~ cp3(all_10_0_2) % 68.08/29.23 | % 68.08/29.23 | Instantiating formula (10) with all_10_0_2 and discharging atoms cp1(all_10_0_2), yields: % 68.08/29.23 | (95) ~ cp2(all_10_0_2) % 68.08/29.23 | % 68.08/29.23 | Using (62) and (78) yields: % 68.08/29.23 | (96) ~ (all_24_0_9 = all_20_0_7) % 68.08/29.23 | % 68.08/29.23 | Using (62) and (83) yields: % 68.08/29.23 | (97) ~ (all_24_0_9 = all_14_0_4) % 68.08/29.23 | % 68.08/29.23 | Using (62) and (92) yields: % 68.08/29.23 | (98) ~ (all_24_0_9 = all_10_0_2) % 68.08/29.23 | % 68.08/29.23 | Using (58) and (88) yields: % 68.08/29.23 | (99) ~ (all_22_0_8 = all_18_0_6) % 68.08/29.23 | % 68.08/29.23 | Using (55) and (88) yields: % 68.08/29.23 | (100) ~ (all_20_0_7 = all_18_0_6) % 68.08/29.23 | % 68.08/29.23 | Using (58) and (82) yields: % 68.08/29.23 | (101) ~ (all_22_0_8 = all_16_0_5) % 68.08/29.23 | % 68.08/29.23 | Using (55) and (82) yields: % 68.08/29.23 | (102) ~ (all_20_0_7 = all_16_0_5) % 68.08/29.23 | % 68.08/29.23 | Using (58) and (84) yields: % 68.08/29.23 | (103) ~ (all_22_0_8 = all_14_0_4) % 68.08/29.23 | % 68.08/29.23 | Using (55) and (84) yields: % 68.08/29.23 | (104) ~ (all_20_0_7 = all_14_0_4) % 68.08/29.23 | % 68.08/29.23 | Using (55) and (86) yields: % 68.08/29.23 | (105) ~ (all_20_0_7 = all_12_0_3) % 68.08/29.23 | % 68.08/29.23 | Using (58) and (93) yields: % 68.08/29.23 | (106) ~ (all_22_0_8 = all_10_0_2) % 68.08/29.23 | % 68.08/29.23 | Using (55) and (93) yields: % 68.08/29.23 | (107) ~ (all_20_0_7 = all_10_0_2) % 68.08/29.23 | % 68.08/29.23 | Using (65) and (79) yields: % 68.08/29.23 | (108) ~ (all_26_0_10 = all_24_0_9) % 68.08/29.23 | % 68.08/29.23 | Using (65) and (80) yields: % 68.08/29.23 | (109) ~ (all_26_0_10 = all_22_0_8) % 68.08/29.23 | % 68.08/29.23 | Using (65) and (81) yields: % 68.08/29.23 | (110) ~ (all_26_0_10 = all_20_0_7) % 68.08/29.23 | % 68.08/29.23 | Using (65) and (89) yields: % 68.08/29.23 | (111) ~ (all_26_0_10 = all_18_0_6) % 68.08/29.23 | % 68.08/29.23 | Using (48) and (89) yields: % 68.08/29.23 | (112) ~ (all_18_0_6 = all_16_0_5) % 68.08/29.23 | % 68.08/29.23 | Using (65) and (85) yields: % 68.08/29.23 | (113) ~ (all_26_0_10 = all_14_0_4) % 68.08/29.23 | % 68.08/29.23 | Using (48) and (85) yields: % 68.08/29.23 | (114) ~ (all_16_0_5 = all_14_0_4) % 68.08/29.23 | % 68.08/29.23 | Using (48) and (87) yields: % 68.08/29.23 | (115) ~ (all_16_0_5 = all_12_0_3) % 68.08/29.23 | % 68.08/29.23 | Using (65) and (94) yields: % 68.08/29.23 | (116) ~ (all_26_0_10 = all_10_0_2) % 68.08/29.23 | % 68.08/29.23 | Using (48) and (94) yields: % 68.08/29.23 | (117) ~ (all_16_0_5 = all_10_0_2) % 68.08/29.23 | % 68.08/29.23 | Using (44) and (95) yields: % 68.08/29.23 | (118) ~ (all_14_0_4 = all_10_0_2) % 68.08/29.23 | % 68.08/29.23 | Using (51) and (90) yields: % 68.08/29.23 | (119) ~ (all_18_0_6 = all_14_0_4) % 68.08/29.23 | % 68.08/29.23 | Using (51) and (91) yields: % 68.08/29.23 | (120) ~ (all_18_0_6 = all_12_0_3) % 68.08/29.23 | % 68.08/29.23 +-Applying beta-rule and splitting (71), into two cases. % 68.08/29.23 |-Branch one: % 68.08/29.23 | (121) all_26_0_10 = all_24_0_9 % 68.08/29.23 | % 68.08/29.23 | Equations (121) can reduce 108 to: % 68.08/29.23 | (122) $false % 68.08/29.23 | % 68.08/29.23 |-The branch is then unsatisfiable % 68.08/29.23 |-Branch two: % 68.08/29.23 | (108) ~ (all_26_0_10 = all_24_0_9) % 68.08/29.23 | (124) all_26_0_10 = all_20_0_7 | all_26_0_10 = all_16_0_5 | all_26_0_10 = all_10_0_2 | all_24_0_9 = all_20_0_7 | all_24_0_9 = all_16_0_5 | all_24_0_9 = all_10_0_2 | all_20_0_7 = all_16_0_5 | all_20_0_7 = all_10_0_2 | all_16_0_5 = all_10_0_2 % 68.08/29.23 | % 68.08/29.23 +-Applying beta-rule and splitting (67), into two cases. % 68.08/29.23 |-Branch one: % 68.08/29.23 | (125) all_26_0_10 = all_22_0_8 % 68.08/29.23 | % 68.08/29.23 | Equations (125) can reduce 109 to: % 68.08/29.23 | (122) $false % 68.08/29.23 | % 68.08/29.23 |-The branch is then unsatisfiable % 68.08/29.23 |-Branch two: % 68.08/29.23 | (109) ~ (all_26_0_10 = all_22_0_8) % 68.08/29.23 | (128) all_26_0_10 = all_20_0_7 | all_26_0_10 = all_18_0_6 | all_26_0_10 = all_12_0_3 | all_22_0_8 = all_20_0_7 | all_22_0_8 = all_18_0_6 | all_22_0_8 = all_12_0_3 | all_20_0_7 = all_18_0_6 | all_20_0_7 = all_12_0_3 | all_18_0_6 = all_12_0_3 % 68.08/29.23 | % 68.08/29.23 +-Applying beta-rule and splitting (68), into two cases. % 68.08/29.23 |-Branch one: % 68.08/29.23 | (125) all_26_0_10 = all_22_0_8 % 68.08/29.23 | % 68.08/29.23 | Equations (125) can reduce 109 to: % 68.08/29.23 | (122) $false % 68.08/29.23 | % 68.08/29.23 |-The branch is then unsatisfiable % 68.08/29.23 |-Branch two: % 68.08/29.23 | (109) ~ (all_26_0_10 = all_22_0_8) % 68.08/29.23 | (132) all_26_0_10 = all_18_0_6 | all_26_0_10 = all_16_0_5 | all_26_0_10 = all_12_0_3 | all_22_0_8 = all_18_0_6 | all_22_0_8 = all_16_0_5 | all_22_0_8 = all_12_0_3 | all_18_0_6 = all_16_0_5 | all_18_0_6 = all_12_0_3 | all_16_0_5 = all_12_0_3 % 68.08/29.23 | % 68.08/29.23 +-Applying beta-rule and splitting (69), into two cases. % 68.08/29.23 |-Branch one: % 68.08/29.23 | (133) all_26_0_10 = all_20_0_7 % 68.08/29.23 | % 68.08/29.23 | Equations (133) can reduce 110 to: % 68.08/29.23 | (122) $false % 68.08/29.23 | % 68.08/29.23 |-The branch is then unsatisfiable % 68.08/29.23 |-Branch two: % 68.08/29.23 | (110) ~ (all_26_0_10 = all_20_0_7) % 68.08/29.23 | (136) all_26_0_10 = all_18_0_6 | all_26_0_10 = all_16_0_5 | all_26_0_10 = all_12_0_3 | all_20_0_7 = all_18_0_6 | all_20_0_7 = all_16_0_5 | all_20_0_7 = all_12_0_3 | all_18_0_6 = all_16_0_5 | all_18_0_6 = all_12_0_3 | all_16_0_5 = all_12_0_3 % 68.08/29.23 | % 68.08/29.23 +-Applying beta-rule and splitting (132), into two cases. % 68.08/29.23 |-Branch one: % 68.08/29.23 | (137) all_26_0_10 = all_18_0_6 % 68.08/29.23 | % 68.08/29.23 | Equations (137) can reduce 111 to: % 68.08/29.23 | (122) $false % 68.08/29.23 | % 68.08/29.23 |-The branch is then unsatisfiable % 68.08/29.23 |-Branch two: % 68.08/29.23 | (111) ~ (all_26_0_10 = all_18_0_6) % 68.08/29.24 | (140) all_26_0_10 = all_16_0_5 | all_26_0_10 = all_12_0_3 | all_22_0_8 = all_18_0_6 | all_22_0_8 = all_16_0_5 | all_22_0_8 = all_12_0_3 | all_18_0_6 = all_16_0_5 | all_18_0_6 = all_12_0_3 | all_16_0_5 = all_12_0_3 % 68.08/29.24 | % 68.08/29.24 +-Applying beta-rule and splitting (72), into two cases. % 68.08/29.24 |-Branch one: % 68.08/29.24 | (121) all_26_0_10 = all_24_0_9 % 68.08/29.24 | % 68.08/29.24 | Equations (121) can reduce 108 to: % 68.08/29.24 | (122) $false % 68.08/29.24 | % 68.08/29.24 |-The branch is then unsatisfiable % 68.08/29.24 |-Branch two: % 68.08/29.24 | (108) ~ (all_26_0_10 = all_24_0_9) % 68.08/29.24 | (144) all_26_0_10 = all_20_0_7 | all_26_0_10 = all_14_0_4 | all_26_0_10 = all_10_0_2 | all_24_0_9 = all_20_0_7 | all_24_0_9 = all_14_0_4 | all_24_0_9 = all_10_0_2 | all_20_0_7 = all_14_0_4 | all_20_0_7 = all_10_0_2 | all_14_0_4 = all_10_0_2 % 68.08/29.24 | % 68.08/29.24 +-Applying beta-rule and splitting (70), into two cases. % 68.08/29.24 |-Branch one: % 68.08/29.24 | (145) all_20_0_7 = all_18_0_6 % 68.08/29.24 | % 68.08/29.24 | Equations (145) can reduce 100 to: % 68.08/29.24 | (122) $false % 68.08/29.24 | % 68.08/29.24 |-The branch is then unsatisfiable % 68.08/29.24 |-Branch two: % 68.08/29.24 | (100) ~ (all_20_0_7 = all_18_0_6) % 68.08/29.24 | (148) all_20_0_7 = all_16_0_5 | all_20_0_7 = all_14_0_4 | all_20_0_7 = all_12_0_3 | all_18_0_6 = all_16_0_5 | all_18_0_6 = all_14_0_4 | all_18_0_6 = all_12_0_3 | all_16_0_5 = all_14_0_4 | all_16_0_5 = all_12_0_3 | all_14_0_4 = all_12_0_3 % 68.08/29.24 | % 68.08/29.24 +-Applying beta-rule and splitting (148), into two cases. % 68.08/29.24 |-Branch one: % 68.08/29.24 | (149) all_20_0_7 = all_16_0_5 % 68.08/29.24 | % 68.08/29.24 | Equations (149) can reduce 102 to: % 68.08/29.24 | (122) $false % 68.08/29.24 | % 68.08/29.24 |-The branch is then unsatisfiable % 68.08/29.24 |-Branch two: % 68.08/29.24 | (102) ~ (all_20_0_7 = all_16_0_5) % 68.08/29.24 | (152) all_20_0_7 = all_14_0_4 | all_20_0_7 = all_12_0_3 | all_18_0_6 = all_16_0_5 | all_18_0_6 = all_14_0_4 | all_18_0_6 = all_12_0_3 | all_16_0_5 = all_14_0_4 | all_16_0_5 = all_12_0_3 | all_14_0_4 = all_12_0_3 % 68.08/29.24 | % 68.08/29.24 +-Applying beta-rule and splitting (152), into two cases. % 68.08/29.24 |-Branch one: % 68.08/29.24 | (153) all_20_0_7 = all_14_0_4 % 68.08/29.24 | % 68.08/29.24 | Equations (153) can reduce 104 to: % 68.08/29.24 | (122) $false % 68.08/29.24 | % 68.08/29.24 |-The branch is then unsatisfiable % 68.08/29.24 |-Branch two: % 68.08/29.24 | (104) ~ (all_20_0_7 = all_14_0_4) % 68.08/29.24 | (156) all_20_0_7 = all_12_0_3 | all_18_0_6 = all_16_0_5 | all_18_0_6 = all_14_0_4 | all_18_0_6 = all_12_0_3 | all_16_0_5 = all_14_0_4 | all_16_0_5 = all_12_0_3 | all_14_0_4 = all_12_0_3 % 68.08/29.24 | % 68.08/29.24 +-Applying beta-rule and splitting (156), into two cases. % 68.08/29.24 |-Branch one: % 68.08/29.24 | (157) all_20_0_7 = all_12_0_3 % 68.08/29.24 | % 68.08/29.24 | Equations (157) can reduce 105 to: % 68.08/29.24 | (122) $false % 68.08/29.24 | % 68.08/29.24 |-The branch is then unsatisfiable % 68.08/29.24 |-Branch two: % 68.08/29.24 | (105) ~ (all_20_0_7 = all_12_0_3) % 68.08/29.24 | (160) all_18_0_6 = all_16_0_5 | all_18_0_6 = all_14_0_4 | all_18_0_6 = all_12_0_3 | all_16_0_5 = all_14_0_4 | all_16_0_5 = all_12_0_3 | all_14_0_4 = all_12_0_3 % 68.08/29.24 | % 68.08/29.24 +-Applying beta-rule and splitting (160), into two cases. % 68.08/29.24 |-Branch one: % 68.08/29.24 | (161) all_18_0_6 = all_16_0_5 % 68.08/29.24 | % 68.08/29.24 | Equations (161) can reduce 112 to: % 68.08/29.24 | (122) $false % 68.08/29.24 | % 68.08/29.24 |-The branch is then unsatisfiable % 68.08/29.24 |-Branch two: % 68.08/29.24 | (112) ~ (all_18_0_6 = all_16_0_5) % 68.08/29.24 | (164) all_18_0_6 = all_14_0_4 | all_18_0_6 = all_12_0_3 | all_16_0_5 = all_14_0_4 | all_16_0_5 = all_12_0_3 | all_14_0_4 = all_12_0_3 % 68.08/29.24 | % 68.08/29.24 +-Applying beta-rule and splitting (164), into two cases. % 68.08/29.24 |-Branch one: % 68.08/29.24 | (165) all_18_0_6 = all_14_0_4 % 68.08/29.24 | % 68.08/29.24 | Equations (165) can reduce 119 to: % 68.08/29.24 | (122) $false % 68.08/29.24 | % 68.08/29.24 |-The branch is then unsatisfiable % 68.08/29.24 |-Branch two: % 68.08/29.24 | (119) ~ (all_18_0_6 = all_14_0_4) % 68.08/29.24 | (168) all_18_0_6 = all_12_0_3 | all_16_0_5 = all_14_0_4 | all_16_0_5 = all_12_0_3 | all_14_0_4 = all_12_0_3 % 68.08/29.24 | % 68.08/29.24 +-Applying beta-rule and splitting (168), into two cases. % 68.08/29.24 |-Branch one: % 68.08/29.24 | (169) all_18_0_6 = all_12_0_3 % 68.08/29.24 | % 68.08/29.24 | Equations (169) can reduce 120 to: % 68.08/29.24 | (122) $false % 68.08/29.24 | % 68.08/29.24 |-The branch is then unsatisfiable % 68.08/29.24 |-Branch two: % 68.08/29.24 | (120) ~ (all_18_0_6 = all_12_0_3) % 68.08/29.24 | (172) all_16_0_5 = all_14_0_4 | all_16_0_5 = all_12_0_3 | all_14_0_4 = all_12_0_3 % 68.08/29.24 | % 68.08/29.24 +-Applying beta-rule and splitting (172), into two cases. % 68.08/29.24 |-Branch one: % 68.08/29.24 | (173) all_16_0_5 = all_14_0_4 % 68.08/29.24 | % 68.08/29.24 | Equations (173) can reduce 114 to: % 68.08/29.24 | (122) $false % 68.08/29.24 | % 68.08/29.24 |-The branch is then unsatisfiable % 68.08/29.24 |-Branch two: % 68.08/29.24 | (114) ~ (all_16_0_5 = all_14_0_4) % 68.08/29.24 | (176) all_16_0_5 = all_12_0_3 | all_14_0_4 = all_12_0_3 % 68.08/29.24 | % 68.08/29.24 +-Applying beta-rule and splitting (176), into two cases. % 68.08/29.24 |-Branch one: % 68.08/29.24 | (177) all_16_0_5 = all_12_0_3 % 68.08/29.24 | % 68.08/29.24 | Equations (177) can reduce 115 to: % 68.08/29.24 | (122) $false % 68.08/29.24 | % 68.08/29.24 |-The branch is then unsatisfiable % 68.08/29.24 |-Branch two: % 68.08/29.24 | (115) ~ (all_16_0_5 = all_12_0_3) % 68.08/29.24 | (180) all_14_0_4 = all_12_0_3 % 68.08/29.24 | % 68.08/29.24 | Equations (180) can reduce 113 to: % 68.08/29.24 | (181) ~ (all_26_0_10 = all_12_0_3) % 68.08/29.24 | % 68.08/29.24 | Equations (180) can reduce 97 to: % 68.08/29.24 | (182) ~ (all_24_0_9 = all_12_0_3) % 68.08/29.24 | % 68.08/29.24 | Equations (180) can reduce 103 to: % 68.08/29.24 | (183) ~ (all_22_0_8 = all_12_0_3) % 68.08/29.24 | % 68.08/29.24 | Equations (180) can reduce 104 to: % 68.08/29.24 | (105) ~ (all_20_0_7 = all_12_0_3) % 68.08/29.24 | % 68.08/29.24 | Equations (180) can reduce 119 to: % 68.08/29.24 | (120) ~ (all_18_0_6 = all_12_0_3) % 68.08/29.24 | % 68.08/29.24 | Equations (180) can reduce 114 to: % 68.08/29.24 | (115) ~ (all_16_0_5 = all_12_0_3) % 68.08/29.24 | % 68.08/29.24 | Equations (180) can reduce 118 to: % 68.08/29.24 | (187) ~ (all_12_0_3 = all_10_0_2) % 68.08/29.24 | % 68.08/29.24 +-Applying beta-rule and splitting (73), into two cases. % 68.08/29.24 |-Branch one: % 68.08/29.24 | (121) all_26_0_10 = all_24_0_9 % 68.08/29.24 | % 68.08/29.24 | Equations (121) can reduce 108 to: % 68.08/29.24 | (122) $false % 68.08/29.24 | % 68.08/29.24 |-The branch is then unsatisfiable % 68.08/29.24 |-Branch two: % 68.08/29.24 | (108) ~ (all_26_0_10 = all_24_0_9) % 68.08/29.24 | (191) all_26_0_10 = all_20_0_7 | all_26_0_10 = all_12_0_3 | all_26_0_10 = all_10_0_2 | all_24_0_9 = all_20_0_7 | all_24_0_9 = all_12_0_3 | all_24_0_9 = all_10_0_2 | all_20_0_7 = all_12_0_3 | all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.08/29.24 | % 68.08/29.24 +-Applying beta-rule and splitting (124), into two cases. % 68.08/29.24 |-Branch one: % 68.08/29.24 | (133) all_26_0_10 = all_20_0_7 % 68.08/29.24 | % 68.08/29.24 | Equations (133) can reduce 110 to: % 68.08/29.24 | (122) $false % 68.08/29.24 | % 68.08/29.24 |-The branch is then unsatisfiable % 68.08/29.24 |-Branch two: % 68.08/29.24 | (110) ~ (all_26_0_10 = all_20_0_7) % 68.08/29.24 | (195) all_26_0_10 = all_16_0_5 | all_26_0_10 = all_10_0_2 | all_24_0_9 = all_20_0_7 | all_24_0_9 = all_16_0_5 | all_24_0_9 = all_10_0_2 | all_20_0_7 = all_16_0_5 | all_20_0_7 = all_10_0_2 | all_16_0_5 = all_10_0_2 % 68.08/29.24 | % 68.08/29.24 +-Applying beta-rule and splitting (195), into two cases. % 68.08/29.24 |-Branch one: % 68.08/29.24 | (196) all_26_0_10 = all_16_0_5 % 68.08/29.24 | % 68.08/29.24 | Equations (196) can reduce 110 to: % 68.08/29.24 | (197) ~ (all_20_0_7 = all_16_0_5) % 68.08/29.24 | % 68.08/29.24 | Simplifying 197 yields: % 68.08/29.24 | (102) ~ (all_20_0_7 = all_16_0_5) % 68.08/29.24 | % 68.08/29.24 | Equations (196) can reduce 181 to: % 68.08/29.24 | (115) ~ (all_16_0_5 = all_12_0_3) % 68.08/29.24 | % 68.08/29.24 | Equations (196) can reduce 116 to: % 68.08/29.24 | (117) ~ (all_16_0_5 = all_10_0_2) % 68.08/29.24 | % 68.08/29.24 +-Applying beta-rule and splitting (191), into two cases. % 68.08/29.24 |-Branch one: % 68.08/29.24 | (133) all_26_0_10 = all_20_0_7 % 68.08/29.24 | % 68.08/29.25 | Combining equations (133,196) yields a new equation: % 68.08/29.25 | (202) all_20_0_7 = all_16_0_5 % 68.08/29.25 | % 68.08/29.25 | Simplifying 202 yields: % 68.08/29.25 | (149) all_20_0_7 = all_16_0_5 % 68.08/29.25 | % 68.08/29.25 | Equations (149) can reduce 102 to: % 68.08/29.25 | (122) $false % 68.08/29.25 | % 68.08/29.25 |-The branch is then unsatisfiable % 68.08/29.25 |-Branch two: % 68.08/29.25 | (110) ~ (all_26_0_10 = all_20_0_7) % 68.08/29.25 | (206) all_26_0_10 = all_12_0_3 | all_26_0_10 = all_10_0_2 | all_24_0_9 = all_20_0_7 | all_24_0_9 = all_12_0_3 | all_24_0_9 = all_10_0_2 | all_20_0_7 = all_12_0_3 | all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.08/29.25 | % 68.08/29.25 +-Applying beta-rule and splitting (206), into two cases. % 68.08/29.25 |-Branch one: % 68.08/29.25 | (207) all_26_0_10 = all_12_0_3 % 68.08/29.25 | % 68.08/29.25 | Combining equations (207,196) yields a new equation: % 68.08/29.25 | (177) all_16_0_5 = all_12_0_3 % 68.08/29.25 | % 68.08/29.25 | Equations (177) can reduce 115 to: % 68.08/29.25 | (122) $false % 68.08/29.25 | % 68.08/29.25 |-The branch is then unsatisfiable % 68.08/29.25 |-Branch two: % 68.08/29.25 | (181) ~ (all_26_0_10 = all_12_0_3) % 68.08/29.25 | (211) all_26_0_10 = all_10_0_2 | all_24_0_9 = all_20_0_7 | all_24_0_9 = all_12_0_3 | all_24_0_9 = all_10_0_2 | all_20_0_7 = all_12_0_3 | all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.08/29.25 | % 68.08/29.25 +-Applying beta-rule and splitting (211), into two cases. % 68.08/29.25 |-Branch one: % 68.08/29.25 | (212) all_26_0_10 = all_10_0_2 % 68.08/29.25 | % 68.08/29.25 | Combining equations (212,196) yields a new equation: % 68.08/29.25 | (213) all_16_0_5 = all_10_0_2 % 68.08/29.25 | % 68.08/29.25 | Equations (213) can reduce 117 to: % 68.08/29.25 | (122) $false % 68.08/29.25 | % 68.08/29.25 |-The branch is then unsatisfiable % 68.08/29.25 |-Branch two: % 68.08/29.25 | (116) ~ (all_26_0_10 = all_10_0_2) % 68.08/29.25 | (216) all_24_0_9 = all_20_0_7 | all_24_0_9 = all_12_0_3 | all_24_0_9 = all_10_0_2 | all_20_0_7 = all_12_0_3 | all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.08/29.25 | % 68.08/29.25 +-Applying beta-rule and splitting (216), into two cases. % 68.08/29.25 |-Branch one: % 68.08/29.25 | (217) all_24_0_9 = all_20_0_7 % 68.08/29.25 | % 68.08/29.25 | Equations (217) can reduce 96 to: % 68.08/29.25 | (122) $false % 68.08/29.25 | % 68.08/29.25 |-The branch is then unsatisfiable % 68.08/29.25 |-Branch two: % 68.08/29.25 | (96) ~ (all_24_0_9 = all_20_0_7) % 68.08/29.25 | (220) all_24_0_9 = all_12_0_3 | all_24_0_9 = all_10_0_2 | all_20_0_7 = all_12_0_3 | all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.08/29.25 | % 68.08/29.25 +-Applying beta-rule and splitting (220), into two cases. % 68.08/29.25 |-Branch one: % 68.08/29.25 | (221) all_24_0_9 = all_12_0_3 % 68.08/29.25 | % 68.08/29.25 | Equations (221) can reduce 182 to: % 68.08/29.25 | (122) $false % 68.08/29.25 | % 68.08/29.25 |-The branch is then unsatisfiable % 68.08/29.25 |-Branch two: % 68.08/29.25 | (182) ~ (all_24_0_9 = all_12_0_3) % 68.08/29.25 | (224) all_24_0_9 = all_10_0_2 | all_20_0_7 = all_12_0_3 | all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.57/29.25 | % 68.57/29.25 +-Applying beta-rule and splitting (224), into two cases. % 68.57/29.25 |-Branch one: % 68.57/29.25 | (225) all_24_0_9 = all_10_0_2 % 68.57/29.25 | % 68.57/29.25 | Equations (225) can reduce 98 to: % 68.57/29.25 | (122) $false % 68.57/29.25 | % 68.57/29.25 |-The branch is then unsatisfiable % 68.57/29.25 |-Branch two: % 68.57/29.25 | (98) ~ (all_24_0_9 = all_10_0_2) % 68.57/29.25 | (228) all_20_0_7 = all_12_0_3 | all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.57/29.25 | % 68.57/29.25 +-Applying beta-rule and splitting (228), into two cases. % 68.57/29.25 |-Branch one: % 68.57/29.25 | (157) all_20_0_7 = all_12_0_3 % 68.57/29.25 | % 68.57/29.25 | Equations (157) can reduce 105 to: % 68.57/29.25 | (122) $false % 68.57/29.25 | % 68.57/29.25 |-The branch is then unsatisfiable % 68.57/29.25 |-Branch two: % 68.57/29.25 | (105) ~ (all_20_0_7 = all_12_0_3) % 68.57/29.25 | (232) all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.57/29.25 | % 68.57/29.25 +-Applying beta-rule and splitting (232), into two cases. % 68.57/29.25 |-Branch one: % 68.57/29.25 | (233) all_20_0_7 = all_10_0_2 % 68.57/29.25 | % 68.57/29.25 | Equations (233) can reduce 107 to: % 68.57/29.25 | (122) $false % 68.57/29.25 | % 68.57/29.25 |-The branch is then unsatisfiable % 68.57/29.25 |-Branch two: % 68.57/29.25 | (107) ~ (all_20_0_7 = all_10_0_2) % 68.57/29.25 | (236) all_12_0_3 = all_10_0_2 % 68.57/29.25 | % 68.57/29.25 | Equations (236) can reduce 187 to: % 68.57/29.25 | (122) $false % 68.57/29.25 | % 68.57/29.25 |-The branch is then unsatisfiable % 68.57/29.25 |-Branch two: % 68.57/29.25 | (238) ~ (all_26_0_10 = all_16_0_5) % 68.57/29.25 | (239) all_26_0_10 = all_10_0_2 | all_24_0_9 = all_20_0_7 | all_24_0_9 = all_16_0_5 | all_24_0_9 = all_10_0_2 | all_20_0_7 = all_16_0_5 | all_20_0_7 = all_10_0_2 | all_16_0_5 = all_10_0_2 % 68.57/29.25 | % 68.57/29.25 +-Applying beta-rule and splitting (75), into two cases. % 68.57/29.25 |-Branch one: % 68.57/29.25 | (125) all_26_0_10 = all_22_0_8 % 68.57/29.25 | % 68.57/29.25 | Equations (125) can reduce 109 to: % 68.57/29.25 | (122) $false % 68.57/29.25 | % 68.57/29.25 |-The branch is then unsatisfiable % 68.57/29.25 |-Branch two: % 68.57/29.25 | (109) ~ (all_26_0_10 = all_22_0_8) % 68.57/29.25 | (243) all_26_0_10 = all_20_0_7 | all_26_0_10 = all_12_0_3 | all_26_0_10 = all_10_0_2 | all_22_0_8 = all_20_0_7 | all_22_0_8 = all_12_0_3 | all_22_0_8 = all_10_0_2 | all_20_0_7 = all_12_0_3 | all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.57/29.25 | % 68.57/29.25 +-Applying beta-rule and splitting (76), into two cases. % 68.57/29.25 |-Branch one: % 68.57/29.25 | (125) all_26_0_10 = all_22_0_8 % 68.57/29.25 | % 68.57/29.25 | Equations (125) can reduce 109 to: % 68.57/29.25 | (122) $false % 68.57/29.25 | % 68.57/29.25 |-The branch is then unsatisfiable % 68.57/29.25 |-Branch two: % 68.57/29.25 | (109) ~ (all_26_0_10 = all_22_0_8) % 68.57/29.25 | (247) all_26_0_10 = all_18_0_6 | all_26_0_10 = all_16_0_5 | all_26_0_10 = all_10_0_2 | all_22_0_8 = all_18_0_6 | all_22_0_8 = all_16_0_5 | all_22_0_8 = all_10_0_2 | all_18_0_6 = all_16_0_5 | all_18_0_6 = all_10_0_2 | all_16_0_5 = all_10_0_2 % 68.57/29.25 | % 68.57/29.25 +-Applying beta-rule and splitting (243), into two cases. % 68.57/29.25 |-Branch one: % 68.57/29.25 | (133) all_26_0_10 = all_20_0_7 % 68.57/29.25 | % 68.57/29.25 | Equations (133) can reduce 110 to: % 68.57/29.25 | (122) $false % 68.57/29.25 | % 68.57/29.25 |-The branch is then unsatisfiable % 68.57/29.25 |-Branch two: % 68.57/29.25 | (110) ~ (all_26_0_10 = all_20_0_7) % 68.57/29.25 | (251) all_26_0_10 = all_12_0_3 | all_26_0_10 = all_10_0_2 | all_22_0_8 = all_20_0_7 | all_22_0_8 = all_12_0_3 | all_22_0_8 = all_10_0_2 | all_20_0_7 = all_12_0_3 | all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.57/29.25 | % 68.57/29.25 +-Applying beta-rule and splitting (247), into two cases. % 68.57/29.25 |-Branch one: % 68.57/29.25 | (137) all_26_0_10 = all_18_0_6 % 68.57/29.25 | % 68.57/29.25 | Equations (137) can reduce 111 to: % 68.57/29.25 | (122) $false % 68.57/29.25 | % 68.57/29.25 |-The branch is then unsatisfiable % 68.57/29.25 |-Branch two: % 68.57/29.25 | (111) ~ (all_26_0_10 = all_18_0_6) % 68.57/29.25 | (255) all_26_0_10 = all_16_0_5 | all_26_0_10 = all_10_0_2 | all_22_0_8 = all_18_0_6 | all_22_0_8 = all_16_0_5 | all_22_0_8 = all_10_0_2 | all_18_0_6 = all_16_0_5 | all_18_0_6 = all_10_0_2 | all_16_0_5 = all_10_0_2 % 68.57/29.25 | % 68.57/29.25 +-Applying beta-rule and splitting (255), into two cases. % 68.57/29.25 |-Branch one: % 68.57/29.25 | (196) all_26_0_10 = all_16_0_5 % 68.57/29.25 | % 68.57/29.25 | Equations (196) can reduce 238 to: % 68.57/29.25 | (122) $false % 68.57/29.25 | % 68.57/29.25 |-The branch is then unsatisfiable % 68.57/29.25 |-Branch two: % 68.57/29.25 | (238) ~ (all_26_0_10 = all_16_0_5) % 68.57/29.26 | (259) all_26_0_10 = all_10_0_2 | all_22_0_8 = all_18_0_6 | all_22_0_8 = all_16_0_5 | all_22_0_8 = all_10_0_2 | all_18_0_6 = all_16_0_5 | all_18_0_6 = all_10_0_2 | all_16_0_5 = all_10_0_2 % 68.57/29.26 | % 68.57/29.26 +-Applying beta-rule and splitting (259), into two cases. % 68.57/29.26 |-Branch one: % 68.57/29.26 | (212) all_26_0_10 = all_10_0_2 % 68.57/29.26 | % 68.57/29.26 | Equations (212) can reduce 116 to: % 68.57/29.26 | (122) $false % 68.57/29.26 | % 68.57/29.26 |-The branch is then unsatisfiable % 68.57/29.26 |-Branch two: % 68.57/29.26 | (116) ~ (all_26_0_10 = all_10_0_2) % 68.57/29.26 | (263) all_22_0_8 = all_18_0_6 | all_22_0_8 = all_16_0_5 | all_22_0_8 = all_10_0_2 | all_18_0_6 = all_16_0_5 | all_18_0_6 = all_10_0_2 | all_16_0_5 = all_10_0_2 % 68.57/29.26 | % 68.57/29.26 +-Applying beta-rule and splitting (263), into two cases. % 68.57/29.26 |-Branch one: % 68.57/29.26 | (264) all_22_0_8 = all_18_0_6 % 68.57/29.26 | % 68.57/29.26 | Equations (264) can reduce 99 to: % 68.57/29.26 | (122) $false % 68.57/29.26 | % 68.57/29.26 |-The branch is then unsatisfiable % 68.57/29.26 |-Branch two: % 68.57/29.26 | (99) ~ (all_22_0_8 = all_18_0_6) % 68.57/29.26 | (267) all_22_0_8 = all_16_0_5 | all_22_0_8 = all_10_0_2 | all_18_0_6 = all_16_0_5 | all_18_0_6 = all_10_0_2 | all_16_0_5 = all_10_0_2 % 68.57/29.26 | % 68.57/29.26 +-Applying beta-rule and splitting (267), into two cases. % 68.57/29.26 |-Branch one: % 68.57/29.26 | (268) all_22_0_8 = all_16_0_5 % 68.57/29.26 | % 68.57/29.26 | Equations (268) can reduce 101 to: % 68.57/29.26 | (122) $false % 68.57/29.26 | % 68.57/29.26 |-The branch is then unsatisfiable % 68.57/29.26 |-Branch two: % 68.57/29.26 | (101) ~ (all_22_0_8 = all_16_0_5) % 68.57/29.26 | (271) all_22_0_8 = all_10_0_2 | all_18_0_6 = all_16_0_5 | all_18_0_6 = all_10_0_2 | all_16_0_5 = all_10_0_2 % 68.57/29.26 | % 68.57/29.26 +-Applying beta-rule and splitting (271), into two cases. % 68.57/29.26 |-Branch one: % 68.57/29.26 | (272) all_22_0_8 = all_10_0_2 % 68.57/29.26 | % 68.57/29.26 | Equations (272) can reduce 106 to: % 68.57/29.26 | (122) $false % 68.57/29.26 | % 68.57/29.26 |-The branch is then unsatisfiable % 68.57/29.26 |-Branch two: % 68.57/29.26 | (106) ~ (all_22_0_8 = all_10_0_2) % 68.57/29.26 | (275) all_18_0_6 = all_16_0_5 | all_18_0_6 = all_10_0_2 | all_16_0_5 = all_10_0_2 % 68.57/29.26 | % 68.57/29.26 +-Applying beta-rule and splitting (275), into two cases. % 68.57/29.26 |-Branch one: % 68.57/29.26 | (161) all_18_0_6 = all_16_0_5 % 68.57/29.26 | % 68.57/29.26 | Equations (161) can reduce 112 to: % 68.57/29.26 | (122) $false % 68.57/29.26 | % 68.57/29.26 |-The branch is then unsatisfiable % 68.57/29.26 |-Branch two: % 68.57/29.26 | (112) ~ (all_18_0_6 = all_16_0_5) % 68.57/29.26 | (279) all_18_0_6 = all_10_0_2 | all_16_0_5 = all_10_0_2 % 68.57/29.26 | % 68.57/29.26 +-Applying beta-rule and splitting (279), into two cases. % 68.57/29.26 |-Branch one: % 68.57/29.26 | (280) all_18_0_6 = all_10_0_2 % 68.57/29.26 | % 68.57/29.26 | Equations (280) can reduce 111 to: % 68.57/29.26 | (116) ~ (all_26_0_10 = all_10_0_2) % 68.57/29.26 | % 68.57/29.26 | Equations (280) can reduce 99 to: % 68.57/29.26 | (106) ~ (all_22_0_8 = all_10_0_2) % 68.57/29.26 | % 68.57/29.26 | Equations (280) can reduce 100 to: % 68.57/29.26 | (107) ~ (all_20_0_7 = all_10_0_2) % 68.57/29.26 | % 68.57/29.26 | Equations (280) can reduce 112 to: % 68.57/29.26 | (284) ~ (all_16_0_5 = all_10_0_2) % 68.57/29.26 | % 68.57/29.26 | Simplifying 284 yields: % 68.57/29.26 | (117) ~ (all_16_0_5 = all_10_0_2) % 68.57/29.26 | % 68.57/29.26 | Equations (280) can reduce 120 to: % 68.57/29.26 | (286) ~ (all_12_0_3 = all_10_0_2) % 68.57/29.26 | % 68.57/29.26 | Simplifying 286 yields: % 68.57/29.26 | (187) ~ (all_12_0_3 = all_10_0_2) % 68.57/29.26 | % 68.57/29.26 +-Applying beta-rule and splitting (74), into two cases. % 68.57/29.26 |-Branch one: % 68.57/29.26 | (125) all_26_0_10 = all_22_0_8 % 68.57/29.26 | % 68.57/29.26 | Equations (125) can reduce 109 to: % 68.57/29.26 | (122) $false % 68.57/29.26 | % 68.57/29.26 |-The branch is then unsatisfiable % 68.57/29.26 |-Branch two: % 68.57/29.26 | (109) ~ (all_26_0_10 = all_22_0_8) % 68.57/29.26 | (291) all_26_0_10 = all_20_0_7 | all_26_0_10 = all_16_0_5 | all_26_0_10 = all_10_0_2 | all_22_0_8 = all_20_0_7 | all_22_0_8 = all_16_0_5 | all_22_0_8 = all_10_0_2 | all_20_0_7 = all_16_0_5 | all_20_0_7 = all_10_0_2 | all_16_0_5 = all_10_0_2 % 68.57/29.26 | % 68.57/29.26 +-Applying beta-rule and splitting (251), into two cases. % 68.57/29.26 |-Branch one: % 68.57/29.26 | (207) all_26_0_10 = all_12_0_3 % 68.57/29.26 | % 68.57/29.26 | Equations (207) can reduce 181 to: % 68.57/29.26 | (122) $false % 68.57/29.26 | % 68.57/29.26 |-The branch is then unsatisfiable % 68.57/29.26 |-Branch two: % 68.57/29.26 | (181) ~ (all_26_0_10 = all_12_0_3) % 68.57/29.26 | (295) all_26_0_10 = all_10_0_2 | all_22_0_8 = all_20_0_7 | all_22_0_8 = all_12_0_3 | all_22_0_8 = all_10_0_2 | all_20_0_7 = all_12_0_3 | all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.57/29.26 | % 68.57/29.26 +-Applying beta-rule and splitting (295), into two cases. % 68.57/29.26 |-Branch one: % 68.57/29.26 | (212) all_26_0_10 = all_10_0_2 % 68.57/29.26 | % 68.57/29.26 | Equations (212) can reduce 116 to: % 68.57/29.26 | (122) $false % 68.57/29.26 | % 68.57/29.26 |-The branch is then unsatisfiable % 68.57/29.26 |-Branch two: % 68.57/29.26 | (116) ~ (all_26_0_10 = all_10_0_2) % 68.57/29.26 | (299) all_22_0_8 = all_20_0_7 | all_22_0_8 = all_12_0_3 | all_22_0_8 = all_10_0_2 | all_20_0_7 = all_12_0_3 | all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.57/29.26 | % 68.57/29.26 +-Applying beta-rule and splitting (299), into two cases. % 68.57/29.26 |-Branch one: % 68.57/29.26 | (300) all_22_0_8 = all_20_0_7 % 68.57/29.26 | % 68.57/29.26 | Equations (300) can reduce 109 to: % 68.57/29.26 | (110) ~ (all_26_0_10 = all_20_0_7) % 68.57/29.26 | % 68.57/29.26 | Equations (300) can reduce 101 to: % 68.57/29.26 | (102) ~ (all_20_0_7 = all_16_0_5) % 68.57/29.26 | % 68.57/29.26 | Equations (300) can reduce 183 to: % 68.57/29.26 | (105) ~ (all_20_0_7 = all_12_0_3) % 68.57/29.26 | % 68.57/29.26 | Equations (300) can reduce 106 to: % 68.57/29.26 | (107) ~ (all_20_0_7 = all_10_0_2) % 68.57/29.26 | % 68.57/29.26 +-Applying beta-rule and splitting (77), into two cases. % 68.57/29.26 |-Branch one: % 68.57/29.26 | (125) all_26_0_10 = all_22_0_8 % 68.57/29.26 | % 68.57/29.26 | Combining equations (300,125) yields a new equation: % 68.57/29.26 | (133) all_26_0_10 = all_20_0_7 % 68.57/29.26 | % 68.57/29.26 | Equations (133) can reduce 110 to: % 68.57/29.26 | (122) $false % 68.57/29.26 | % 68.57/29.26 |-The branch is then unsatisfiable % 68.57/29.26 |-Branch two: % 68.57/29.26 | (109) ~ (all_26_0_10 = all_22_0_8) % 68.57/29.26 | (309) all_26_0_10 = all_16_0_5 | all_26_0_10 = all_14_0_4 | all_26_0_10 = all_10_0_2 | all_22_0_8 = all_16_0_5 | all_22_0_8 = all_14_0_4 | all_22_0_8 = all_10_0_2 | all_16_0_5 = all_14_0_4 | all_16_0_5 = all_10_0_2 | all_14_0_4 = all_10_0_2 % 68.57/29.26 | % 68.57/29.26 +-Applying beta-rule and splitting (309), into two cases. % 68.57/29.26 |-Branch one: % 68.57/29.26 | (196) all_26_0_10 = all_16_0_5 % 68.57/29.26 | % 68.57/29.26 | Equations (196) can reduce 238 to: % 68.57/29.26 | (122) $false % 68.57/29.26 | % 68.57/29.26 |-The branch is then unsatisfiable % 68.57/29.26 |-Branch two: % 68.57/29.26 | (238) ~ (all_26_0_10 = all_16_0_5) % 68.57/29.26 | (313) all_26_0_10 = all_14_0_4 | all_26_0_10 = all_10_0_2 | all_22_0_8 = all_16_0_5 | all_22_0_8 = all_14_0_4 | all_22_0_8 = all_10_0_2 | all_16_0_5 = all_14_0_4 | all_16_0_5 = all_10_0_2 | all_14_0_4 = all_10_0_2 % 68.57/29.26 | % 68.57/29.26 +-Applying beta-rule and splitting (313), into two cases. % 68.57/29.26 |-Branch one: % 68.57/29.26 | (314) all_26_0_10 = all_14_0_4 % 68.57/29.26 | % 68.57/29.26 | Combining equations (180,314) yields a new equation: % 68.57/29.26 | (207) all_26_0_10 = all_12_0_3 % 68.57/29.26 | % 68.57/29.26 | Equations (207) can reduce 181 to: % 68.57/29.26 | (122) $false % 68.57/29.26 | % 68.57/29.26 |-The branch is then unsatisfiable % 68.57/29.26 |-Branch two: % 68.57/29.26 | (113) ~ (all_26_0_10 = all_14_0_4) % 68.57/29.26 | (318) all_26_0_10 = all_10_0_2 | all_22_0_8 = all_16_0_5 | all_22_0_8 = all_14_0_4 | all_22_0_8 = all_10_0_2 | all_16_0_5 = all_14_0_4 | all_16_0_5 = all_10_0_2 | all_14_0_4 = all_10_0_2 % 68.57/29.26 | % 68.57/29.26 +-Applying beta-rule and splitting (318), into two cases. % 68.57/29.26 |-Branch one: % 68.57/29.26 | (212) all_26_0_10 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 | Equations (212) can reduce 116 to: % 68.57/29.27 | (122) $false % 68.57/29.27 | % 68.57/29.27 |-The branch is then unsatisfiable % 68.57/29.27 |-Branch two: % 68.57/29.27 | (116) ~ (all_26_0_10 = all_10_0_2) % 68.57/29.27 | (322) all_22_0_8 = all_16_0_5 | all_22_0_8 = all_14_0_4 | all_22_0_8 = all_10_0_2 | all_16_0_5 = all_14_0_4 | all_16_0_5 = all_10_0_2 | all_14_0_4 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 +-Applying beta-rule and splitting (322), into two cases. % 68.57/29.27 |-Branch one: % 68.57/29.27 | (268) all_22_0_8 = all_16_0_5 % 68.57/29.27 | % 68.57/29.27 | Combining equations (268,300) yields a new equation: % 68.57/29.27 | (149) all_20_0_7 = all_16_0_5 % 68.57/29.27 | % 68.57/29.27 | Equations (149) can reduce 102 to: % 68.57/29.27 | (122) $false % 68.57/29.27 | % 68.57/29.27 |-The branch is then unsatisfiable % 68.57/29.27 |-Branch two: % 68.57/29.27 | (101) ~ (all_22_0_8 = all_16_0_5) % 68.57/29.27 | (327) all_22_0_8 = all_14_0_4 | all_22_0_8 = all_10_0_2 | all_16_0_5 = all_14_0_4 | all_16_0_5 = all_10_0_2 | all_14_0_4 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 +-Applying beta-rule and splitting (327), into two cases. % 68.57/29.27 |-Branch one: % 68.57/29.27 | (328) all_22_0_8 = all_14_0_4 % 68.57/29.27 | % 68.57/29.27 | Combining equations (328,300) yields a new equation: % 68.57/29.27 | (153) all_20_0_7 = all_14_0_4 % 68.57/29.27 | % 68.57/29.27 | Combining equations (180,153) yields a new equation: % 68.57/29.27 | (157) all_20_0_7 = all_12_0_3 % 68.57/29.27 | % 68.57/29.27 | Equations (157) can reduce 105 to: % 68.57/29.27 | (122) $false % 68.57/29.27 | % 68.57/29.27 |-The branch is then unsatisfiable % 68.57/29.27 |-Branch two: % 68.57/29.27 | (103) ~ (all_22_0_8 = all_14_0_4) % 68.57/29.27 | (333) all_22_0_8 = all_10_0_2 | all_16_0_5 = all_14_0_4 | all_16_0_5 = all_10_0_2 | all_14_0_4 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 +-Applying beta-rule and splitting (333), into two cases. % 68.57/29.27 |-Branch one: % 68.57/29.27 | (272) all_22_0_8 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 | Combining equations (272,300) yields a new equation: % 68.57/29.27 | (233) all_20_0_7 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 | Equations (233) can reduce 107 to: % 68.57/29.27 | (122) $false % 68.57/29.27 | % 68.57/29.27 |-The branch is then unsatisfiable % 68.57/29.27 |-Branch two: % 68.57/29.27 | (106) ~ (all_22_0_8 = all_10_0_2) % 68.57/29.27 | (338) all_16_0_5 = all_14_0_4 | all_16_0_5 = all_10_0_2 | all_14_0_4 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 +-Applying beta-rule and splitting (338), into two cases. % 68.57/29.27 |-Branch one: % 68.57/29.27 | (173) all_16_0_5 = all_14_0_4 % 68.57/29.27 | % 68.57/29.27 | Combining equations (180,173) yields a new equation: % 68.57/29.27 | (177) all_16_0_5 = all_12_0_3 % 68.57/29.27 | % 68.57/29.27 | Equations (177) can reduce 115 to: % 68.57/29.27 | (122) $false % 68.57/29.27 | % 68.57/29.27 |-The branch is then unsatisfiable % 68.57/29.27 |-Branch two: % 68.57/29.27 | (114) ~ (all_16_0_5 = all_14_0_4) % 68.57/29.27 | (343) all_16_0_5 = all_10_0_2 | all_14_0_4 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 +-Applying beta-rule and splitting (343), into two cases. % 68.57/29.27 |-Branch one: % 68.57/29.27 | (213) all_16_0_5 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 | Equations (213) can reduce 117 to: % 68.57/29.27 | (122) $false % 68.57/29.27 | % 68.57/29.27 |-The branch is then unsatisfiable % 68.57/29.27 |-Branch two: % 68.57/29.27 | (117) ~ (all_16_0_5 = all_10_0_2) % 68.57/29.27 | (347) all_14_0_4 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 | Combining equations (347,180) yields a new equation: % 68.57/29.27 | (236) all_12_0_3 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 | Equations (236) can reduce 187 to: % 68.57/29.27 | (122) $false % 68.57/29.27 | % 68.57/29.27 |-The branch is then unsatisfiable % 68.57/29.27 |-Branch two: % 68.57/29.27 | (350) ~ (all_22_0_8 = all_20_0_7) % 68.57/29.27 | (351) all_22_0_8 = all_12_0_3 | all_22_0_8 = all_10_0_2 | all_20_0_7 = all_12_0_3 | all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 +-Applying beta-rule and splitting (351), into two cases. % 68.57/29.27 |-Branch one: % 68.57/29.27 | (352) all_22_0_8 = all_12_0_3 % 68.57/29.27 | % 68.57/29.27 | Equations (352) can reduce 183 to: % 68.57/29.27 | (122) $false % 68.57/29.27 | % 68.57/29.27 |-The branch is then unsatisfiable % 68.57/29.27 |-Branch two: % 68.57/29.27 | (183) ~ (all_22_0_8 = all_12_0_3) % 68.57/29.27 | (355) all_22_0_8 = all_10_0_2 | all_20_0_7 = all_12_0_3 | all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 +-Applying beta-rule and splitting (355), into two cases. % 68.57/29.27 |-Branch one: % 68.57/29.27 | (272) all_22_0_8 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 | Equations (272) can reduce 106 to: % 68.57/29.27 | (122) $false % 68.57/29.27 | % 68.57/29.27 |-The branch is then unsatisfiable % 68.57/29.27 |-Branch two: % 68.57/29.27 | (106) ~ (all_22_0_8 = all_10_0_2) % 68.57/29.27 | (228) all_20_0_7 = all_12_0_3 | all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 +-Applying beta-rule and splitting (228), into two cases. % 68.57/29.27 |-Branch one: % 68.57/29.27 | (157) all_20_0_7 = all_12_0_3 % 68.57/29.27 | % 68.57/29.27 | Equations (157) can reduce 105 to: % 68.57/29.27 | (122) $false % 68.57/29.27 | % 68.57/29.27 |-The branch is then unsatisfiable % 68.57/29.27 |-Branch two: % 68.57/29.27 | (105) ~ (all_20_0_7 = all_12_0_3) % 68.57/29.27 | (232) all_20_0_7 = all_10_0_2 | all_12_0_3 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 +-Applying beta-rule and splitting (232), into two cases. % 68.57/29.27 |-Branch one: % 68.57/29.27 | (233) all_20_0_7 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 | Equations (233) can reduce 107 to: % 68.57/29.27 | (122) $false % 68.57/29.27 | % 68.57/29.27 |-The branch is then unsatisfiable % 68.57/29.27 |-Branch two: % 68.57/29.27 | (107) ~ (all_20_0_7 = all_10_0_2) % 68.57/29.27 | (236) all_12_0_3 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 | Equations (236) can reduce 187 to: % 68.57/29.27 | (122) $false % 68.57/29.27 | % 68.57/29.27 |-The branch is then unsatisfiable % 68.57/29.27 |-Branch two: % 68.57/29.27 | (369) ~ (all_18_0_6 = all_10_0_2) % 68.57/29.27 | (213) all_16_0_5 = all_10_0_2 % 68.57/29.27 | % 68.57/29.27 | Equations (213) can reduce 117 to: % 68.57/29.27 | (122) $false % 68.57/29.27 | % 68.57/29.27 |-The branch is then unsatisfiable % 68.57/29.27 % SZS output end Proof for theBenchmark % 68.57/29.27 % 68.57/29.27 28601ms %------------------------------------------------------------------------------