%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : KRS089+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n021.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:32 EDT 2022 % Result : Unsatisfiable 17.41s 6.13s % Output : Proof 24.96s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS089+1 : TPTP v8.1.0. Released v3.1.0. % 0.03/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Tue Jun 7 20:03:51 EDT 2022 % 0.12/0.34 % CPUTime : % 0.56/0.59 ____ _ % 0.56/0.59 ___ / __ \_____(_)___ ________ __________ % 0.56/0.59 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.56/0.59 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.56/0.59 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.56/0.59 % 0.56/0.59 A Theorem Prover for First-Order Logic % 0.56/0.59 (ePrincess v.1.0) % 0.56/0.59 % 0.56/0.59 (c) Philipp Rümmer, 2009-2015 % 0.56/0.59 (c) Peter Backeman, 2014-2015 % 0.56/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.56/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.56/0.59 Bug reports to peter@backeman.se % 0.56/0.59 % 0.56/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.56/0.59 % 0.56/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.72/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.57/0.95 Prover 0: Preprocessing ... % 1.79/1.06 Prover 0: Warning: ignoring some quantifiers % 1.91/1.08 Prover 0: Constructing countermodel ... % 2.28/1.22 Prover 0: gave up % 2.28/1.22 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 2.46/1.25 Prover 1: Preprocessing ... % 2.89/1.37 Prover 1: Constructing countermodel ... % 3.29/1.47 Prover 1: gave up % 3.29/1.47 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 3.44/1.49 Prover 2: Preprocessing ... % 3.74/1.57 Prover 2: Warning: ignoring some quantifiers % 3.74/1.57 Prover 2: Constructing countermodel ... % 4.10/1.67 Prover 2: gave up % 4.10/1.67 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 4.32/1.69 Prover 3: Preprocessing ... % 4.32/1.70 Prover 3: Warning: ignoring some quantifiers % 4.32/1.70 Prover 3: Constructing countermodel ... % 4.32/1.73 Prover 3: gave up % 4.32/1.73 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 4.32/1.75 Prover 4: Preprocessing ... % 4.81/1.81 Prover 4: Warning: ignoring some quantifiers % 4.95/1.82 Prover 4: Constructing countermodel ... % 5.39/1.94 Prover 4: gave up % 5.39/1.94 Prover 5: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 5.39/1.96 Prover 5: Preprocessing ... % 5.72/1.99 Prover 5: Constructing countermodel ... % 5.72/2.03 Prover 5: gave up % 5.72/2.03 Prover 6: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 5.72/2.04 Prover 6: Preprocessing ... % 6.12/2.07 Prover 6: Warning: ignoring some quantifiers % 6.12/2.07 Prover 6: Constructing countermodel ... % 6.34/2.12 Prover 6: gave up % 6.34/2.12 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximalOutermost -resolutionMethod=normal -ignoreQuantifiers -generateTriggers=all % 6.34/2.14 Prover 7: Preprocessing ... % 6.47/2.15 Prover 7: Proving ... % 17.41/6.13 Prover 7: proved (4007ms) % 17.41/6.13 % 17.41/6.13 % SZS status Unsatisfiable for theBenchmark % 17.41/6.13 % 17.41/6.13 Generating proof ... found it (size 67) % 24.96/9.31 % 24.96/9.31 % SZS output start Proof for theBenchmark % 24.96/9.31 Assumed formulas after preprocessing and simplification: % 24.96/9.31 | (0) ? [v0] : ? [v1] : (cowlThing(v1) & cUnsatisfiable(v0) & ! [v2] : ! [v3] : ! [v4] : (v4 = v3 | v4 = v2 | v3 = v2 | ~ rinvP(v1, v4) | ~ rinvP(v1, v3) | ~ rinvP(v1, v2)) & ! [v2] : ! [v3] : ( ~ rp(v2, v3) | rinvP(v3, v2)) & ! [v2] : ! [v3] : ( ~ rinvP(v3, v2) | rp(v2, v3)) & ! [v2] : ( ~ xsd_string(v2) | ~ xsd_integer(v2)) & ! [v2] : ( ~ cowlThing(v2) | rp(v2, v1)) & ! [v2] : ~ cowlNothing(v2) & ! [v2] : ( ~ cUnsatisfiable(v2) | ? [v3] : ? [v4] : ? [v5] : ( ~ (v5 = v4) & ~ (v5 = v3) & ~ (v4 = v3) & rr(v2, v5) & rr(v2, v4) & rr(v2, v3))) & ! [v2] : (xsd_string(v2) | xsd_integer(v2)) & ! [v2] : cowlThing(v2)) % 24.96/9.31 | Instantiating (0) with all_0_0_0, all_0_1_1 yields: % 24.96/9.31 | (1) cowlThing(all_0_0_0) & cUnsatisfiable(all_0_1_1) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | v2 = v0 | v1 = v0 | ~ rinvP(all_0_0_0, v2) | ~ rinvP(all_0_0_0, v1) | ~ rinvP(all_0_0_0, v0)) & ! [v0] : ! [v1] : ( ~ rp(v0, v1) | rinvP(v1, v0)) & ! [v0] : ! [v1] : ( ~ rinvP(v1, v0) | rp(v0, v1)) & ! [v0] : ( ~ xsd_string(v0) | ~ xsd_integer(v0)) & ! [v0] : ( ~ cowlThing(v0) | rp(v0, all_0_0_0)) & ! [v0] : ~ cowlNothing(v0) & ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = v2) & ~ (v3 = v1) & ~ (v2 = v1) & rr(v0, v3) & rr(v0, v2) & rr(v0, v1))) & ! [v0] : (xsd_string(v0) | xsd_integer(v0)) & ! [v0] : cowlThing(v0) % 24.96/9.32 | % 24.96/9.32 | Applying alpha-rule on (1) yields: % 24.96/9.32 | (2) ! [v0] : ~ cowlNothing(v0) % 24.96/9.32 | (3) ! [v0] : ( ~ xsd_string(v0) | ~ xsd_integer(v0)) % 24.96/9.32 | (4) cUnsatisfiable(all_0_1_1) % 24.96/9.32 | (5) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | v2 = v0 | v1 = v0 | ~ rinvP(all_0_0_0, v2) | ~ rinvP(all_0_0_0, v1) | ~ rinvP(all_0_0_0, v0)) % 24.96/9.32 | (6) ! [v0] : cowlThing(v0) % 24.96/9.32 | (7) ! [v0] : (xsd_string(v0) | xsd_integer(v0)) % 24.96/9.32 | (8) ! [v0] : ( ~ cUnsatisfiable(v0) | ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = v2) & ~ (v3 = v1) & ~ (v2 = v1) & rr(v0, v3) & rr(v0, v2) & rr(v0, v1))) % 24.96/9.32 | (9) ! [v0] : ( ~ cowlThing(v0) | rp(v0, all_0_0_0)) % 24.96/9.32 | (10) cowlThing(all_0_0_0) % 24.96/9.32 | (11) ! [v0] : ! [v1] : ( ~ rinvP(v1, v0) | rp(v0, v1)) % 24.96/9.32 | (12) ! [v0] : ! [v1] : ( ~ rp(v0, v1) | rinvP(v1, v0)) % 24.96/9.32 | % 24.96/9.32 | Instantiating formula (9) with all_0_0_0 and discharging atoms cowlThing(all_0_0_0), yields: % 24.96/9.32 | (13) rp(all_0_0_0, all_0_0_0) % 24.96/9.32 | % 24.96/9.32 | Instantiating formula (8) with all_0_1_1 and discharging atoms cUnsatisfiable(all_0_1_1), yields: % 24.96/9.32 | (14) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = v1) & ~ (v2 = v0) & ~ (v1 = v0) & rr(all_0_1_1, v2) & rr(all_0_1_1, v1) & rr(all_0_1_1, v0)) % 24.96/9.32 | % 24.96/9.32 | Instantiating (14) with all_9_0_2, all_9_1_3, all_9_2_4 yields: % 24.96/9.32 | (15) ~ (all_9_0_2 = all_9_1_3) & ~ (all_9_0_2 = all_9_2_4) & ~ (all_9_1_3 = all_9_2_4) & rr(all_0_1_1, all_9_0_2) & rr(all_0_1_1, all_9_1_3) & rr(all_0_1_1, all_9_2_4) % 24.96/9.32 | % 24.96/9.32 | Applying alpha-rule on (15) yields: % 24.96/9.32 | (16) ~ (all_9_0_2 = all_9_2_4) % 24.96/9.32 | (17) rr(all_0_1_1, all_9_1_3) % 24.96/9.32 | (18) ~ (all_9_0_2 = all_9_1_3) % 24.96/9.32 | (19) ~ (all_9_1_3 = all_9_2_4) % 24.96/9.32 | (20) rr(all_0_1_1, all_9_2_4) % 24.96/9.32 | (21) rr(all_0_1_1, all_9_0_2) % 24.96/9.32 | % 24.96/9.32 | Instantiating formula (12) with all_0_0_0, all_0_0_0 and discharging atoms rp(all_0_0_0, all_0_0_0), yields: % 24.96/9.32 | (22) rinvP(all_0_0_0, all_0_0_0) % 24.96/9.32 | % 24.96/9.32 | Introducing new symbol ex_32_0_6 defined by: % 24.96/9.32 | (23) ex_32_0_6 = all_9_2_4 % 24.96/9.32 | % 24.96/9.32 | Instantiating formula (6) with ex_32_0_6 yields: % 24.96/9.32 | (24) cowlThing(ex_32_0_6) % 24.96/9.32 | % 24.96/9.32 | Instantiating formula (9) with ex_32_0_6 and discharging atoms cowlThing(ex_32_0_6), yields: % 24.96/9.32 | (25) rp(ex_32_0_6, all_0_0_0) % 24.96/9.32 | % 24.96/9.32 | Instantiating formula (12) with all_0_0_0, ex_32_0_6 and discharging atoms rp(ex_32_0_6, all_0_0_0), yields: % 24.96/9.32 | (26) rinvP(all_0_0_0, ex_32_0_6) % 24.96/9.32 | % 24.96/9.32 | Introducing new symbol ex_61_0_8 defined by: % 24.96/9.32 | (27) ex_61_0_8 = all_9_0_2 % 24.96/9.32 | % 24.96/9.32 | Instantiating formula (6) with ex_61_0_8 yields: % 24.96/9.32 | (28) cowlThing(ex_61_0_8) % 24.96/9.32 | % 24.96/9.32 | Instantiating formula (9) with ex_61_0_8 and discharging atoms cowlThing(ex_61_0_8), yields: % 24.96/9.32 | (29) rp(ex_61_0_8, all_0_0_0) % 24.96/9.32 | % 24.96/9.32 | Instantiating formula (12) with all_0_0_0, ex_61_0_8 and discharging atoms rp(ex_61_0_8, all_0_0_0), yields: % 24.96/9.32 | (30) rinvP(all_0_0_0, ex_61_0_8) % 24.96/9.32 | % 24.96/9.32 | Instantiating formula (5) with ex_61_0_8, ex_32_0_6, all_0_0_0 and discharging atoms rinvP(all_0_0_0, ex_61_0_8), rinvP(all_0_0_0, ex_32_0_6), rinvP(all_0_0_0, all_0_0_0), yields: % 24.96/9.32 | (31) ex_61_0_8 = ex_32_0_6 | ex_61_0_8 = all_0_0_0 | ex_32_0_6 = all_0_0_0 % 24.96/9.32 | % 24.96/9.32 +-Applying beta-rule and splitting (31), into two cases. % 24.96/9.32 |-Branch one: % 24.96/9.32 | (32) ex_61_0_8 = ex_32_0_6 % 24.96/9.32 | % 24.96/9.32 | Combining equations (27,32) yields a new equation: % 24.96/9.32 | (33) ex_32_0_6 = all_9_0_2 % 24.96/9.32 | % 24.96/9.32 | Combining equations (23,33) yields a new equation: % 24.96/9.32 | (34) all_9_0_2 = all_9_2_4 % 24.96/9.33 | % 24.96/9.33 | Equations (34) can reduce 16 to: % 24.96/9.33 | (35) $false % 24.96/9.33 | % 24.96/9.33 |-The branch is then unsatisfiable % 24.96/9.33 |-Branch two: % 24.96/9.33 | (36) ex_61_0_8 = all_0_0_0 | ex_32_0_6 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 +-Applying beta-rule and splitting (36), into two cases. % 24.96/9.33 |-Branch one: % 24.96/9.33 | (37) ex_61_0_8 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Introducing new symbol ex_98_0_10 defined by: % 24.96/9.33 | (38) ex_98_0_10 = all_9_1_3 % 24.96/9.33 | % 24.96/9.33 | Instantiating formula (6) with ex_98_0_10 yields: % 24.96/9.33 | (39) cowlThing(ex_98_0_10) % 24.96/9.33 | % 24.96/9.33 | Instantiating formula (9) with ex_98_0_10 and discharging atoms cowlThing(ex_98_0_10), yields: % 24.96/9.33 | (40) rp(ex_98_0_10, all_0_0_0) % 24.96/9.33 | % 24.96/9.33 | Instantiating formula (12) with all_0_0_0, ex_98_0_10 and discharging atoms rp(ex_98_0_10, all_0_0_0), yields: % 24.96/9.33 | (41) rinvP(all_0_0_0, ex_98_0_10) % 24.96/9.33 | % 24.96/9.33 | Instantiating formula (5) with ex_98_0_10, ex_32_0_6, all_0_0_0 and discharging atoms rinvP(all_0_0_0, ex_98_0_10), rinvP(all_0_0_0, ex_32_0_6), rinvP(all_0_0_0, all_0_0_0), yields: % 24.96/9.33 | (42) ex_98_0_10 = ex_32_0_6 | ex_98_0_10 = all_0_0_0 | ex_32_0_6 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 +-Applying beta-rule and splitting (42), into two cases. % 24.96/9.33 |-Branch one: % 24.96/9.33 | (43) ex_98_0_10 = ex_32_0_6 % 24.96/9.33 | % 24.96/9.33 | Combining equations (38,43) yields a new equation: % 24.96/9.33 | (44) ex_32_0_6 = all_9_1_3 % 24.96/9.33 | % 24.96/9.33 | Combining equations (23,44) yields a new equation: % 24.96/9.33 | (45) all_9_1_3 = all_9_2_4 % 24.96/9.33 | % 24.96/9.33 | Equations (45) can reduce 19 to: % 24.96/9.33 | (35) $false % 24.96/9.33 | % 24.96/9.33 |-The branch is then unsatisfiable % 24.96/9.33 |-Branch two: % 24.96/9.33 | (47) ex_98_0_10 = all_0_0_0 | ex_32_0_6 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 +-Applying beta-rule and splitting (47), into two cases. % 24.96/9.33 |-Branch one: % 24.96/9.33 | (48) ex_98_0_10 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Combining equations (38,48) yields a new equation: % 24.96/9.33 | (49) all_9_1_3 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Simplifying 49 yields: % 24.96/9.33 | (50) all_9_1_3 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Combining equations (27,37) yields a new equation: % 24.96/9.33 | (51) all_9_0_2 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Simplifying 51 yields: % 24.96/9.33 | (52) all_9_0_2 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Equations (52,50) can reduce 18 to: % 24.96/9.33 | (35) $false % 24.96/9.33 | % 24.96/9.33 |-The branch is then unsatisfiable % 24.96/9.33 |-Branch two: % 24.96/9.33 | (54) ex_32_0_6 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Combining equations (37,27) yields a new equation: % 24.96/9.33 | (52) all_9_0_2 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Combining equations (23,54) yields a new equation: % 24.96/9.33 | (56) all_9_2_4 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Simplifying 56 yields: % 24.96/9.33 | (57) all_9_2_4 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Equations (52,57) can reduce 16 to: % 24.96/9.33 | (35) $false % 24.96/9.33 | % 24.96/9.33 |-The branch is then unsatisfiable % 24.96/9.33 |-Branch two: % 24.96/9.33 | (54) ex_32_0_6 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Introducing new symbol ex_98_0_12 defined by: % 24.96/9.33 | (60) ex_98_0_12 = all_9_1_3 % 24.96/9.33 | % 24.96/9.33 | Instantiating formula (6) with ex_98_0_12 yields: % 24.96/9.33 | (61) cowlThing(ex_98_0_12) % 24.96/9.33 | % 24.96/9.33 | Instantiating formula (9) with ex_98_0_12 and discharging atoms cowlThing(ex_98_0_12), yields: % 24.96/9.33 | (62) rp(ex_98_0_12, all_0_0_0) % 24.96/9.33 | % 24.96/9.33 | Instantiating formula (12) with all_0_0_0, ex_98_0_12 and discharging atoms rp(ex_98_0_12, all_0_0_0), yields: % 24.96/9.33 | (63) rinvP(all_0_0_0, ex_98_0_12) % 24.96/9.33 | % 24.96/9.33 | Instantiating formula (5) with ex_98_0_12, ex_61_0_8, all_0_0_0 and discharging atoms rinvP(all_0_0_0, ex_98_0_12), rinvP(all_0_0_0, ex_61_0_8), rinvP(all_0_0_0, all_0_0_0), yields: % 24.96/9.33 | (64) ex_98_0_12 = ex_61_0_8 | ex_98_0_12 = all_0_0_0 | ex_61_0_8 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 +-Applying beta-rule and splitting (64), into two cases. % 24.96/9.33 |-Branch one: % 24.96/9.33 | (65) ex_98_0_12 = ex_61_0_8 % 24.96/9.33 | % 24.96/9.33 | Combining equations (60,65) yields a new equation: % 24.96/9.33 | (66) ex_61_0_8 = all_9_1_3 % 24.96/9.33 | % 24.96/9.33 | Combining equations (27,66) yields a new equation: % 24.96/9.33 | (67) all_9_0_2 = all_9_1_3 % 24.96/9.33 | % 24.96/9.33 | Simplifying 67 yields: % 24.96/9.33 | (68) all_9_0_2 = all_9_1_3 % 24.96/9.33 | % 24.96/9.33 | Equations (68) can reduce 18 to: % 24.96/9.33 | (35) $false % 24.96/9.33 | % 24.96/9.33 |-The branch is then unsatisfiable % 24.96/9.33 |-Branch two: % 24.96/9.33 | (70) ex_98_0_12 = all_0_0_0 | ex_61_0_8 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 +-Applying beta-rule and splitting (70), into two cases. % 24.96/9.33 |-Branch one: % 24.96/9.33 | (71) ex_98_0_12 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Combining equations (60,71) yields a new equation: % 24.96/9.33 | (49) all_9_1_3 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Simplifying 49 yields: % 24.96/9.33 | (50) all_9_1_3 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Combining equations (23,54) yields a new equation: % 24.96/9.33 | (56) all_9_2_4 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Simplifying 56 yields: % 24.96/9.33 | (57) all_9_2_4 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Equations (50,57) can reduce 19 to: % 24.96/9.33 | (35) $false % 24.96/9.33 | % 24.96/9.33 |-The branch is then unsatisfiable % 24.96/9.33 |-Branch two: % 24.96/9.33 | (37) ex_61_0_8 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Combining equations (37,27) yields a new equation: % 24.96/9.33 | (52) all_9_0_2 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Combining equations (23,54) yields a new equation: % 24.96/9.33 | (56) all_9_2_4 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Simplifying 56 yields: % 24.96/9.33 | (57) all_9_2_4 = all_0_0_0 % 24.96/9.33 | % 24.96/9.33 | Equations (52,57) can reduce 16 to: % 24.96/9.33 | (35) $false % 24.96/9.33 | % 24.96/9.33 |-The branch is then unsatisfiable % 24.96/9.33 % SZS output end Proof for theBenchmark % 24.96/9.33 % 24.96/9.33 8727ms %------------------------------------------------------------------------------