%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : KRS080+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n017.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 21.37s 8.59s % Output : Proof 23.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : KRS080+1 : TPTP v8.1.0. Released v3.1.0. % 0.06/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.11/0.33 % Computer : n017.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Tue Jun 7 19:34:17 EDT 2022 % 0.11/0.33 % CPUTime : % 0.50/0.57 ____ _ % 0.50/0.57 ___ / __ \_____(_)___ ________ __________ % 0.50/0.57 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.50/0.57 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.50/0.57 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.50/0.57 % 0.50/0.57 A Theorem Prover for First-Order Logic % 0.50/0.57 (ePrincess v.1.0) % 0.50/0.57 % 0.50/0.57 (c) Philipp Rümmer, 2009-2015 % 0.50/0.57 (c) Peter Backeman, 2014-2015 % 0.50/0.57 (contributions by Angelo Brillout, Peter Baumgartner) % 0.50/0.57 Free software under GNU Lesser General Public License (LGPL). % 0.50/0.57 Bug reports to peter@backeman.se % 0.50/0.57 % 0.50/0.57 For more information, visit http://user.uu.se/~petba168/breu/ % 0.50/0.57 % 0.50/0.57 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.50/0.62 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.51/0.90 Prover 0: Preprocessing ... % 2.02/1.06 Prover 0: Warning: ignoring some quantifiers % 2.02/1.08 Prover 0: Constructing countermodel ... % 10.04/5.91 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 10.24/5.96 Prover 1: Preprocessing ... % 11.15/6.15 Prover 1: Constructing countermodel ... % 13.03/6.62 Prover 1: gave up % 13.03/6.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 13.03/6.64 Prover 2: Preprocessing ... % 18.41/7.90 Prover 2: Warning: ignoring some quantifiers % 18.80/7.97 Prover 2: Constructing countermodel ... % 20.45/8.35 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 20.50/8.38 Prover 3: Preprocessing ... % 20.50/8.40 Prover 3: Warning: ignoring some quantifiers % 20.50/8.40 Prover 3: Constructing countermodel ... % 21.37/8.58 Prover 3: proved (238ms) % 21.37/8.59 Prover 2: stopped % 21.37/8.59 Prover 0: stopped % 21.37/8.59 % 21.37/8.59 No countermodel exists, formula is valid % 21.37/8.59 % SZS status Unsatisfiable for theBenchmark % 21.37/8.59 % 21.37/8.59 Generating proof ... Warning: ignoring some quantifiers % 23.09/8.98 found it (size 53) % 23.09/8.98 % 23.09/8.98 % SZS output start Proof for theBenchmark % 23.09/8.98 Assumed formulas after preprocessing and simplification: % 23.09/8.98 | (0) cUnsatisfiable(i2003_11_14_17_19_21224) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ rr(v0, v7) | ~ rr(v0, v6) | ~ rr(v0, v5) | ~ rr(v0, v4) | ~ rr(v0, v3) | ~ rr(v0, v2) | ~ rr(v0, v1) | ~ cp4(v5) | ~ cp3(v3) | ~ cp3(v2) | ~ cp2(v4) | ~ cp2(v1) | ~ cp1(v7) | ~ cp1(v6) | ~ cp(v7) | ~ cp(v2) | ~ cp(v1) | cUnsatisfiable(v0) | ? [v8] : ? [v9] : ? [v10] : ? [v11] : ( ~ (v11 = v10) & ~ (v11 = v9) & ~ (v11 = v8) & ~ (v10 = v9) & ~ (v10 = v8) & ~ (v9 = v8) & rr(v0, v11) & rr(v0, v10) & rr(v0, v9) & rr(v0, v8))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v3 | v4 = v2 | v4 = v1 | v3 = v2 | v3 = v1 | v2 = v1 | ~ 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) & 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) % 23.09/8.99 | Applying alpha-rule on (0) yields: % 23.09/8.99 | (1) ! [v0] : ( ~ cp2(v0) | ~ cp1(v0)) % 23.09/8.99 | (2) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp2(v1) & cp(v1))) % 23.09/8.99 | (3) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp1(v1))) % 23.09/8.99 | (4) ! [v0] : ( ~ cp3(v0) | ~ cp2(v0)) % 23.09/8.99 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v3 | v4 = v2 | v4 = v1 | v3 = v2 | v3 = v1 | v2 = v1 | ~ rr(v0, v4) | ~ rr(v0, v3) | ~ rr(v0, v2) | ~ rr(v0, v1) | ~ cUnsatisfiable(v0)) % 23.09/8.99 | (6) ! [v0] : ( ~ cp4(v0) | ~ cp2(v0)) % 23.09/8.99 | (7) ! [v0] : ( ~ cp5(v0) | ~ cp1(v0)) % 23.09/8.99 | (8) ! [v0] : ( ~ cp5(v0) | ~ cp3(v0)) % 23.09/8.99 | (9) cUnsatisfiable(i2003_11_14_17_19_21224) % 23.09/8.99 | (10) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp1(v1) & cp(v1))) % 23.09/8.99 | (11) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp3(v1))) % 23.09/8.99 | (12) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp3(v1) & cp(v1))) % 23.09/9.00 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ rr(v0, v7) | ~ rr(v0, v6) | ~ rr(v0, v5) | ~ rr(v0, v4) | ~ rr(v0, v3) | ~ rr(v0, v2) | ~ rr(v0, v1) | ~ cp4(v5) | ~ cp3(v3) | ~ cp3(v2) | ~ cp2(v4) | ~ cp2(v1) | ~ cp1(v7) | ~ cp1(v6) | ~ cp(v7) | ~ cp(v2) | ~ cp(v1) | cUnsatisfiable(v0) | ? [v8] : ? [v9] : ? [v10] : ? [v11] : ( ~ (v11 = v10) & ~ (v11 = v9) & ~ (v11 = v8) & ~ (v10 = v9) & ~ (v10 = v8) & ~ (v9 = v8) & rr(v0, v11) & rr(v0, v10) & rr(v0, v9) & rr(v0, v8))) % 23.09/9.00 | (14) ! [v0] : ( ~ cp4(v0) | ~ cp1(v0)) % 23.09/9.00 | (15) ! [v0] : ( ~ xsd_string(v0) | ~ xsd_integer(v0)) % 23.09/9.00 | (16) ! [v0] : ( ~ cp4(v0) | ~ cp3(v0)) % 23.09/9.00 | (17) ! [v0] : ( ~ cp3(v0) | ~ cp1(v0)) % 23.09/9.00 | (18) ! [v0] : ( ~ cp5(v0) | ~ cp2(v0)) % 23.09/9.00 | (19) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp4(v1))) % 23.09/9.00 | (20) ? [v0] : (xsd_string(v0) | xsd_integer(v0)) % 23.09/9.00 | (21) ! [v0] : ( ~ cp5(v0) | ~ cp4(v0)) % 23.09/9.00 | (22) ? [v0] : cowlThing(v0) % 23.09/9.00 | (23) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : (rr(v0, v1) & cp2(v1))) % 23.09/9.00 | (24) ! [v0] : ~ cowlNothing(v0) % 23.09/9.00 | % 23.09/9.00 | Instantiating formula (19) with i2003_11_14_17_19_21224 and discharging atoms cUnsatisfiable(i2003_11_14_17_19_21224), yields: % 23.09/9.00 | (25) ? [v0] : (rr(i2003_11_14_17_19_21224, v0) & cp4(v0)) % 23.09/9.00 | % 23.09/9.00 | Instantiating formula (12) with i2003_11_14_17_19_21224 and discharging atoms cUnsatisfiable(i2003_11_14_17_19_21224), yields: % 23.09/9.00 | (26) ? [v0] : (rr(i2003_11_14_17_19_21224, v0) & cp3(v0) & cp(v0)) % 23.09/9.00 | % 23.09/9.00 | Instantiating formula (2) with i2003_11_14_17_19_21224 and discharging atoms cUnsatisfiable(i2003_11_14_17_19_21224), yields: % 23.09/9.00 | (27) ? [v0] : (rr(i2003_11_14_17_19_21224, v0) & cp2(v0) & cp(v0)) % 23.09/9.00 | % 23.09/9.00 | Instantiating formula (23) with i2003_11_14_17_19_21224 and discharging atoms cUnsatisfiable(i2003_11_14_17_19_21224), yields: % 23.09/9.00 | (28) ? [v0] : (rr(i2003_11_14_17_19_21224, v0) & cp2(v0)) % 23.09/9.00 | % 23.09/9.00 | Instantiating formula (10) with i2003_11_14_17_19_21224 and discharging atoms cUnsatisfiable(i2003_11_14_17_19_21224), yields: % 23.09/9.00 | (29) ? [v0] : (rr(i2003_11_14_17_19_21224, v0) & cp1(v0) & cp(v0)) % 23.09/9.00 | % 23.09/9.00 | Instantiating (29) with all_12_0_3 yields: % 23.09/9.00 | (30) rr(i2003_11_14_17_19_21224, all_12_0_3) & cp1(all_12_0_3) & cp(all_12_0_3) % 23.09/9.00 | % 23.09/9.00 | Applying alpha-rule on (30) yields: % 23.09/9.00 | (31) rr(i2003_11_14_17_19_21224, all_12_0_3) % 23.09/9.00 | (32) cp1(all_12_0_3) % 23.09/9.00 | (33) cp(all_12_0_3) % 23.09/9.00 | % 23.09/9.00 | Instantiating (28) with all_14_0_4 yields: % 23.09/9.00 | (34) rr(i2003_11_14_17_19_21224, all_14_0_4) & cp2(all_14_0_4) % 23.09/9.00 | % 23.09/9.00 | Applying alpha-rule on (34) yields: % 23.09/9.00 | (35) rr(i2003_11_14_17_19_21224, all_14_0_4) % 23.09/9.00 | (36) cp2(all_14_0_4) % 23.38/9.00 | % 23.38/9.00 | Instantiating (27) with all_16_0_5 yields: % 23.38/9.00 | (37) rr(i2003_11_14_17_19_21224, all_16_0_5) & cp2(all_16_0_5) & cp(all_16_0_5) % 23.38/9.00 | % 23.38/9.00 | Applying alpha-rule on (37) yields: % 23.38/9.00 | (38) rr(i2003_11_14_17_19_21224, all_16_0_5) % 23.38/9.01 | (39) cp2(all_16_0_5) % 23.38/9.01 | (40) cp(all_16_0_5) % 23.38/9.01 | % 23.38/9.01 | Instantiating (26) with all_20_0_7 yields: % 23.38/9.01 | (41) rr(i2003_11_14_17_19_21224, all_20_0_7) & cp3(all_20_0_7) & cp(all_20_0_7) % 23.38/9.01 | % 23.38/9.01 | Applying alpha-rule on (41) yields: % 23.38/9.01 | (42) rr(i2003_11_14_17_19_21224, all_20_0_7) % 23.38/9.01 | (43) cp3(all_20_0_7) % 23.38/9.01 | (44) cp(all_20_0_7) % 23.38/9.01 | % 23.38/9.01 | Instantiating (25) with all_22_0_8 yields: % 23.38/9.01 | (45) rr(i2003_11_14_17_19_21224, all_22_0_8) & cp4(all_22_0_8) % 23.38/9.01 | % 23.38/9.01 | Applying alpha-rule on (45) yields: % 23.38/9.01 | (46) rr(i2003_11_14_17_19_21224, all_22_0_8) % 23.38/9.01 | (47) cp4(all_22_0_8) % 23.38/9.01 | % 23.38/9.01 | Instantiating formula (5) with all_14_0_4, all_22_0_8, all_20_0_7, all_16_0_5, i2003_11_14_17_19_21224 and discharging atoms rr(i2003_11_14_17_19_21224, all_22_0_8), rr(i2003_11_14_17_19_21224, all_20_0_7), rr(i2003_11_14_17_19_21224, all_16_0_5), rr(i2003_11_14_17_19_21224, all_14_0_4), cUnsatisfiable(i2003_11_14_17_19_21224), yields: % 23.38/9.01 | (48) all_22_0_8 = all_20_0_7 | all_22_0_8 = all_16_0_5 | all_22_0_8 = all_14_0_4 | all_20_0_7 = all_16_0_5 | all_20_0_7 = all_14_0_4 | all_16_0_5 = all_14_0_4 % 23.38/9.01 | % 23.38/9.01 | Instantiating formula (5) with all_12_0_3, all_22_0_8, all_20_0_7, all_16_0_5, i2003_11_14_17_19_21224 and discharging atoms rr(i2003_11_14_17_19_21224, all_22_0_8), rr(i2003_11_14_17_19_21224, all_20_0_7), rr(i2003_11_14_17_19_21224, all_16_0_5), rr(i2003_11_14_17_19_21224, all_12_0_3), cUnsatisfiable(i2003_11_14_17_19_21224), yields: % 23.38/9.01 | (49) all_22_0_8 = all_20_0_7 | all_22_0_8 = all_16_0_5 | all_22_0_8 = all_12_0_3 | all_20_0_7 = all_16_0_5 | all_20_0_7 = all_12_0_3 | all_16_0_5 = all_12_0_3 % 23.38/9.01 | % 23.38/9.01 | Instantiating formula (16) with all_20_0_7 and discharging atoms cp3(all_20_0_7), yields: % 23.38/9.01 | (50) ~ cp4(all_20_0_7) % 23.38/9.01 | % 23.38/9.01 | Instantiating formula (6) with all_16_0_5 and discharging atoms cp2(all_16_0_5), yields: % 23.38/9.01 | (51) ~ cp4(all_16_0_5) % 23.38/9.01 | % 23.38/9.01 | Instantiating formula (4) with all_16_0_5 and discharging atoms cp2(all_16_0_5), yields: % 23.38/9.01 | (52) ~ cp3(all_16_0_5) % 23.38/9.01 | % 23.38/9.01 | Instantiating formula (14) with all_12_0_3 and discharging atoms cp1(all_12_0_3), yields: % 23.38/9.01 | (53) ~ cp4(all_12_0_3) % 23.38/9.01 | % 23.38/9.01 | Instantiating formula (17) with all_12_0_3 and discharging atoms cp1(all_12_0_3), yields: % 23.38/9.01 | (54) ~ cp3(all_12_0_3) % 23.38/9.01 | % 23.38/9.01 | Instantiating formula (1) with all_12_0_3 and discharging atoms cp1(all_12_0_3), yields: % 23.38/9.01 | (55) ~ cp2(all_12_0_3) % 23.38/9.01 | % 23.38/9.01 | Using (47) and (50) yields: % 23.38/9.01 | (56) ~ (all_22_0_8 = all_20_0_7) % 23.38/9.01 | % 23.38/9.01 | Using (47) and (51) yields: % 23.38/9.01 | (57) ~ (all_22_0_8 = all_16_0_5) % 23.38/9.01 | % 23.38/9.01 | Using (47) and (53) yields: % 23.38/9.01 | (58) ~ (all_22_0_8 = all_12_0_3) % 23.38/9.01 | % 23.38/9.01 | Using (43) and (52) yields: % 23.38/9.01 | (59) ~ (all_20_0_7 = all_16_0_5) % 23.38/9.01 | % 23.38/9.01 | Using (43) and (54) yields: % 23.38/9.01 | (60) ~ (all_20_0_7 = all_12_0_3) % 23.38/9.01 | % 23.38/9.01 | Using (39) and (55) yields: % 23.38/9.01 | (61) ~ (all_16_0_5 = all_12_0_3) % 23.38/9.01 | % 23.38/9.01 +-Applying beta-rule and splitting (49), into two cases. % 23.38/9.01 |-Branch one: % 23.38/9.01 | (62) all_22_0_8 = all_20_0_7 % 23.38/9.01 | % 23.38/9.01 | Equations (62) can reduce 56 to: % 23.38/9.01 | (63) $false % 23.38/9.01 | % 23.38/9.01 |-The branch is then unsatisfiable % 23.38/9.01 |-Branch two: % 23.38/9.01 | (56) ~ (all_22_0_8 = all_20_0_7) % 23.38/9.01 | (65) all_22_0_8 = all_16_0_5 | all_22_0_8 = all_12_0_3 | all_20_0_7 = all_16_0_5 | all_20_0_7 = all_12_0_3 | all_16_0_5 = all_12_0_3 % 23.38/9.01 | % 23.38/9.01 +-Applying beta-rule and splitting (48), into two cases. % 23.38/9.01 |-Branch one: % 23.38/9.01 | (62) all_22_0_8 = all_20_0_7 % 23.38/9.01 | % 23.38/9.01 | Equations (62) can reduce 56 to: % 23.38/9.01 | (63) $false % 23.38/9.01 | % 23.38/9.01 |-The branch is then unsatisfiable % 23.38/9.01 |-Branch two: % 23.38/9.01 | (56) ~ (all_22_0_8 = all_20_0_7) % 23.38/9.01 | (69) all_22_0_8 = all_16_0_5 | all_22_0_8 = all_14_0_4 | all_20_0_7 = all_16_0_5 | all_20_0_7 = all_14_0_4 | all_16_0_5 = all_14_0_4 % 23.38/9.01 | % 23.38/9.01 +-Applying beta-rule and splitting (69), into two cases. % 23.38/9.01 |-Branch one: % 23.38/9.01 | (70) all_22_0_8 = all_16_0_5 % 23.38/9.01 | % 23.38/9.01 | Equations (70) can reduce 57 to: % 23.38/9.01 | (63) $false % 23.38/9.01 | % 23.38/9.01 |-The branch is then unsatisfiable % 23.38/9.01 |-Branch two: % 23.38/9.01 | (57) ~ (all_22_0_8 = all_16_0_5) % 23.38/9.01 | (73) all_22_0_8 = all_14_0_4 | all_20_0_7 = all_16_0_5 | all_20_0_7 = all_14_0_4 | all_16_0_5 = all_14_0_4 % 23.38/9.01 | % 23.38/9.01 +-Applying beta-rule and splitting (65), into two cases. % 23.38/9.01 |-Branch one: % 23.38/9.01 | (70) all_22_0_8 = all_16_0_5 % 23.38/9.01 | % 23.38/9.01 | Equations (70) can reduce 57 to: % 23.38/9.01 | (63) $false % 23.38/9.01 | % 23.38/9.01 |-The branch is then unsatisfiable % 23.38/9.01 |-Branch two: % 23.38/9.01 | (57) ~ (all_22_0_8 = all_16_0_5) % 23.38/9.01 | (77) all_22_0_8 = all_12_0_3 | all_20_0_7 = all_16_0_5 | all_20_0_7 = all_12_0_3 | all_16_0_5 = all_12_0_3 % 23.38/9.01 | % 23.38/9.01 +-Applying beta-rule and splitting (77), into two cases. % 23.38/9.01 |-Branch one: % 23.38/9.01 | (78) all_22_0_8 = all_12_0_3 % 23.38/9.01 | % 23.38/9.01 | Equations (78) can reduce 58 to: % 23.38/9.01 | (63) $false % 23.38/9.01 | % 23.38/9.01 |-The branch is then unsatisfiable % 23.38/9.01 |-Branch two: % 23.38/9.01 | (58) ~ (all_22_0_8 = all_12_0_3) % 23.38/9.01 | (81) all_20_0_7 = all_16_0_5 | all_20_0_7 = all_12_0_3 | all_16_0_5 = all_12_0_3 % 23.38/9.01 | % 23.38/9.01 +-Applying beta-rule and splitting (81), into two cases. % 23.38/9.01 |-Branch one: % 23.38/9.01 | (82) all_20_0_7 = all_16_0_5 % 23.38/9.01 | % 23.38/9.01 | Equations (82) can reduce 59 to: % 23.38/9.01 | (63) $false % 23.38/9.01 | % 23.38/9.01 |-The branch is then unsatisfiable % 23.38/9.01 |-Branch two: % 23.38/9.01 | (59) ~ (all_20_0_7 = all_16_0_5) % 23.38/9.01 | (85) all_20_0_7 = all_12_0_3 | all_16_0_5 = all_12_0_3 % 23.38/9.01 | % 23.38/9.01 +-Applying beta-rule and splitting (85), into two cases. % 23.38/9.01 |-Branch one: % 23.38/9.01 | (86) all_20_0_7 = all_12_0_3 % 23.38/9.01 | % 23.38/9.01 | Equations (86) can reduce 60 to: % 23.38/9.01 | (63) $false % 23.38/9.02 | % 23.38/9.02 |-The branch is then unsatisfiable % 23.38/9.02 |-Branch two: % 23.38/9.02 | (60) ~ (all_20_0_7 = all_12_0_3) % 23.38/9.02 | (89) all_16_0_5 = all_12_0_3 % 23.38/9.02 | % 23.38/9.02 | Equations (89) can reduce 61 to: % 23.38/9.02 | (63) $false % 23.38/9.02 | % 23.38/9.02 |-The branch is then unsatisfiable % 23.38/9.02 % SZS output end Proof for theBenchmark % 23.38/9.02 % 23.38/9.02 8436ms %------------------------------------------------------------------------------