%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : ALG138+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n023.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 : Thu Jul 14 15:36:15 EDT 2022 % Result : Unsatisfiable 3.74s 1.47s % Output : Proof 6.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : ALG138+1 : TPTP v8.1.0. Released v2.7.0. % 0.07/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n023.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.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Wed Jun 8 11:40:38 EDT 2022 % 0.12/0.34 % CPUTime : % 0.50/0.58 ____ _ % 0.50/0.58 ___ / __ \_____(_)___ ________ __________ % 0.50/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.50/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.50/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.50/0.58 % 0.50/0.58 A Theorem Prover for First-Order Logic % 0.50/0.58 (ePrincess v.1.0) % 0.50/0.58 % 0.50/0.58 (c) Philipp Rümmer, 2009-2015 % 0.50/0.58 (c) Peter Backeman, 2014-2015 % 0.50/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.50/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.50/0.58 Bug reports to peter@backeman.se % 0.50/0.58 % 0.50/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.50/0.58 % 0.50/0.58 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.72/0.63 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.13/1.07 Prover 0: Preprocessing ... % 3.25/1.34 Prover 0: Constructing countermodel ... % 3.74/1.46 Prover 0: proved (834ms) % 3.74/1.47 % 3.74/1.47 No countermodel exists, formula is valid % 3.74/1.47 % SZS status Unsatisfiable for theBenchmark % 3.74/1.47 % 3.74/1.47 Generating proof ... found it (size 47) % 5.53/1.90 % 5.53/1.90 % SZS output start Proof for theBenchmark % 5.53/1.90 Assumed formulas after preprocessing and simplification: % 5.53/1.90 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ? [v19] : ? [v20] : ? [v21] : ? [v22] : ? [v23] : ( ~ (v11 = v10) & ~ (v11 = v9) & ~ (v11 = v4) & ~ (v11 = v1) & ~ (v11 = e3) & ~ (v11 = e2) & ~ (v10 = v9) & ~ (v10 = v7) & ~ (v10 = v0) & ~ (v10 = e3) & ~ (v10 = e1) & ~ (v9 = v6) & ~ (v9 = v3) & ~ (v9 = e3) & ~ (v9 = e0) & ~ (v8 = v7) & ~ (v8 = v6) & ~ (v8 = v5) & ~ (v8 = v2) & ~ (v8 = e3) & ~ (v8 = e2) & ~ (v7 = v6) & ~ (v7 = v0) & ~ (v7 = e2) & ~ (v7 = e1) & ~ (v6 = v3) & ~ (v6 = e2) & ~ (v6 = e0) & ~ (v5 = v4) & ~ (v5 = v3) & ~ (v5 = v2) & ~ (v5 = e3) & ~ (v5 = e1) & ~ (v4 = v3) & ~ (v4 = v1) & ~ (v4 = e2) & ~ (v4 = e1) & ~ (v3 = e1) & ~ (v3 = e0) & ~ (v2 = v1) & ~ (v2 = v0) & ~ (v2 = e3) & ~ (v2 = e0) & ~ (v1 = v0) & ~ (v1 = e2) & ~ (v1 = e0) & ~ (v0 = e1) & ~ (v0 = e0) & ~ (e3 = e2) & ~ (e3 = e1) & ~ (e3 = e0) & ~ (e2 = e1) & ~ (e2 = e0) & ~ (e1 = e0) & op(v11, e2) = v13 & op(v10, e1) = v15 & op(v9, e0) = v19 & op(v8, e3) = v12 & op(v7, e1) = v17 & op(v6, e0) = v21 & op(v5, e3) = v14 & op(v4, e2) = v16 & op(v3, e0) = v23 & op(v2, e3) = v18 & op(v1, e2) = v20 & op(v0, e1) = v22 & op(e3, e3) = e3 & op(e3, e2) = v11 & op(e3, e1) = v10 & op(e3, e0) = v9 & op(e2, e3) = v8 & op(e2, e2) = e2 & op(e2, e1) = v7 & op(e2, e0) = v6 & op(e1, e3) = v5 & op(e1, e2) = v4 & op(e1, e1) = e1 & op(e1, e0) = v3 & op(e0, e3) = v2 & op(e0, e2) = v1 & op(e0, e1) = v0 & op(e0, e0) = e0 & ! [v24] : ! [v25] : ! [v26] : ! [v27] : (v25 = v24 | ~ (op(v27, v26) = v25) | ~ (op(v27, v26) = v24)) & ( ~ (v23 = e3) | ~ (v3 = e2)) & ( ~ (v23 = e2) | ~ (v3 = e3)) & ( ~ (v22 = e3) | ~ (v0 = e2)) & ( ~ (v22 = e2) | ~ (v0 = e3)) & ( ~ (v21 = e3) | ~ (v6 = e1)) & ( ~ (v21 = e1) | ~ (v6 = e3)) & ( ~ (v20 = e3) | ~ (v1 = e1)) & ( ~ (v20 = e1) | ~ (v1 = e3)) & ( ~ (v19 = e2) | ~ (v9 = e1)) & ( ~ (v19 = e1) | ~ (v9 = e2)) & ( ~ (v18 = e2) | ~ (v2 = e1)) & ( ~ (v18 = e1) | ~ (v2 = e2)) & ( ~ (v17 = e3) | ~ (v7 = e0)) & ( ~ (v17 = e0) | ~ (v7 = e3)) & ( ~ (v16 = e3) | ~ (v4 = e0)) & ( ~ (v16 = e0) | ~ (v4 = e3)) & ( ~ (v15 = e2) | ~ (v10 = e0)) & ( ~ (v15 = e0) | ~ (v10 = e2)) & ( ~ (v14 = e2) | ~ (v5 = e0)) & ( ~ (v14 = e0) | ~ (v5 = e2)) & ( ~ (v13 = e1) | ~ (v11 = e0)) & ( ~ (v13 = e0) | ~ (v11 = e1)) & ( ~ (v12 = e1) | ~ (v8 = e0)) & ( ~ (v12 = e0) | ~ (v8 = e1)) & (v11 = e1 | v11 = e0) & (v11 = e1 | v9 = e1) & (v11 = e1 | v1 = e1) & (v11 = e0 | v10 = e0) & (v11 = e0 | v4 = e0) & (v10 = e2 | v10 = e0) & (v10 = e2 | v9 = e2) & (v10 = e2 | v0 = e2) & (v10 = e0 | v7 = e0) & (v9 = e2 | v9 = e1) & (v9 = e2 | v3 = e2) & (v9 = e1 | v6 = e1) & (v8 = e1 | v8 = e0) & (v8 = e1 | v6 = e1) & (v8 = e1 | v2 = e1) & (v8 = e0 | v7 = e0) & (v8 = e0 | v5 = e0) & (v7 = e3 | v7 = e0) & (v7 = e3 | v6 = e3) & (v7 = e3 | v0 = e3) & (v6 = e3 | v6 = e1) & (v6 = e3 | v3 = e3) & (v5 = e2 | v5 = e0) & (v5 = e2 | v3 = e2) & (v5 = e2 | v2 = e2) & (v5 = e0 | v4 = e0) & (v4 = e3 | v4 = e0) & (v4 = e3 | v3 = e3) & (v4 = e3 | v1 = e3) & (v3 = e3 | v3 = e2) & (v2 = e2 | v2 = e1) & (v2 = e2 | v0 = e2) & (v2 = e1 | v1 = e1) & (v1 = e3 | v1 = e1) & (v1 = e3 | v0 = e3) & (v0 = e3 | v0 = e2)) % 5.89/1.94 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12, all_0_13_13, all_0_14_14, all_0_15_15, all_0_16_16, all_0_17_17, all_0_18_18, all_0_19_19, all_0_20_20, all_0_21_21, all_0_22_22, all_0_23_23 yields: % 5.89/1.94 | (1) ~ (all_0_12_12 = all_0_13_13) & ~ (all_0_12_12 = all_0_14_14) & ~ (all_0_12_12 = all_0_19_19) & ~ (all_0_12_12 = all_0_22_22) & ~ (all_0_12_12 = e3) & ~ (all_0_12_12 = e2) & ~ (all_0_13_13 = all_0_14_14) & ~ (all_0_13_13 = all_0_16_16) & ~ (all_0_13_13 = all_0_23_23) & ~ (all_0_13_13 = e3) & ~ (all_0_13_13 = e1) & ~ (all_0_14_14 = all_0_17_17) & ~ (all_0_14_14 = all_0_20_20) & ~ (all_0_14_14 = e3) & ~ (all_0_14_14 = e0) & ~ (all_0_15_15 = all_0_16_16) & ~ (all_0_15_15 = all_0_17_17) & ~ (all_0_15_15 = all_0_18_18) & ~ (all_0_15_15 = all_0_21_21) & ~ (all_0_15_15 = e3) & ~ (all_0_15_15 = e2) & ~ (all_0_16_16 = all_0_17_17) & ~ (all_0_16_16 = all_0_23_23) & ~ (all_0_16_16 = e2) & ~ (all_0_16_16 = e1) & ~ (all_0_17_17 = all_0_20_20) & ~ (all_0_17_17 = e2) & ~ (all_0_17_17 = e0) & ~ (all_0_18_18 = all_0_19_19) & ~ (all_0_18_18 = all_0_20_20) & ~ (all_0_18_18 = all_0_21_21) & ~ (all_0_18_18 = e3) & ~ (all_0_18_18 = e1) & ~ (all_0_19_19 = all_0_20_20) & ~ (all_0_19_19 = all_0_22_22) & ~ (all_0_19_19 = e2) & ~ (all_0_19_19 = e1) & ~ (all_0_20_20 = e1) & ~ (all_0_20_20 = e0) & ~ (all_0_21_21 = all_0_22_22) & ~ (all_0_21_21 = all_0_23_23) & ~ (all_0_21_21 = e3) & ~ (all_0_21_21 = e0) & ~ (all_0_22_22 = all_0_23_23) & ~ (all_0_22_22 = e2) & ~ (all_0_22_22 = e0) & ~ (all_0_23_23 = e1) & ~ (all_0_23_23 = e0) & ~ (e3 = e2) & ~ (e3 = e1) & ~ (e3 = e0) & ~ (e2 = e1) & ~ (e2 = e0) & ~ (e1 = e0) & op(all_0_12_12, e2) = all_0_10_10 & op(all_0_13_13, e1) = all_0_8_8 & op(all_0_14_14, e0) = all_0_4_4 & op(all_0_15_15, e3) = all_0_11_11 & op(all_0_16_16, e1) = all_0_6_6 & op(all_0_17_17, e0) = all_0_2_2 & op(all_0_18_18, e3) = all_0_9_9 & op(all_0_19_19, e2) = all_0_7_7 & op(all_0_20_20, e0) = all_0_0_0 & op(all_0_21_21, e3) = all_0_5_5 & op(all_0_22_22, e2) = all_0_3_3 & op(all_0_23_23, e1) = all_0_1_1 & op(e3, e3) = e3 & op(e3, e2) = all_0_12_12 & op(e3, e1) = all_0_13_13 & op(e3, e0) = all_0_14_14 & op(e2, e3) = all_0_15_15 & op(e2, e2) = e2 & op(e2, e1) = all_0_16_16 & op(e2, e0) = all_0_17_17 & op(e1, e3) = all_0_18_18 & op(e1, e2) = all_0_19_19 & op(e1, e1) = e1 & op(e1, e0) = all_0_20_20 & op(e0, e3) = all_0_21_21 & op(e0, e2) = all_0_22_22 & op(e0, e1) = all_0_23_23 & op(e0, e0) = e0 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op(v3, v2) = v1) | ~ (op(v3, v2) = v0)) & ( ~ (all_0_0_0 = e3) | ~ (all_0_20_20 = e2)) & ( ~ (all_0_0_0 = e2) | ~ (all_0_20_20 = e3)) & ( ~ (all_0_1_1 = e3) | ~ (all_0_23_23 = e2)) & ( ~ (all_0_1_1 = e2) | ~ (all_0_23_23 = e3)) & ( ~ (all_0_2_2 = e3) | ~ (all_0_17_17 = e1)) & ( ~ (all_0_2_2 = e1) | ~ (all_0_17_17 = e3)) & ( ~ (all_0_3_3 = e3) | ~ (all_0_22_22 = e1)) & ( ~ (all_0_3_3 = e1) | ~ (all_0_22_22 = e3)) & ( ~ (all_0_4_4 = e2) | ~ (all_0_14_14 = e1)) & ( ~ (all_0_4_4 = e1) | ~ (all_0_14_14 = e2)) & ( ~ (all_0_5_5 = e2) | ~ (all_0_21_21 = e1)) & ( ~ (all_0_5_5 = e1) | ~ (all_0_21_21 = e2)) & ( ~ (all_0_6_6 = e3) | ~ (all_0_16_16 = e0)) & ( ~ (all_0_6_6 = e0) | ~ (all_0_16_16 = e3)) & ( ~ (all_0_7_7 = e3) | ~ (all_0_19_19 = e0)) & ( ~ (all_0_7_7 = e0) | ~ (all_0_19_19 = e3)) & ( ~ (all_0_8_8 = e2) | ~ (all_0_13_13 = e0)) & ( ~ (all_0_8_8 = e0) | ~ (all_0_13_13 = e2)) & ( ~ (all_0_9_9 = e2) | ~ (all_0_18_18 = e0)) & ( ~ (all_0_9_9 = e0) | ~ (all_0_18_18 = e2)) & ( ~ (all_0_10_10 = e1) | ~ (all_0_12_12 = e0)) & ( ~ (all_0_10_10 = e0) | ~ (all_0_12_12 = e1)) & ( ~ (all_0_11_11 = e1) | ~ (all_0_15_15 = e0)) & ( ~ (all_0_11_11 = e0) | ~ (all_0_15_15 = e1)) & (all_0_12_12 = e1 | all_0_12_12 = e0) & (all_0_12_12 = e1 | all_0_14_14 = e1) & (all_0_12_12 = e1 | all_0_22_22 = e1) & (all_0_12_12 = e0 | all_0_13_13 = e0) & (all_0_12_12 = e0 | all_0_19_19 = e0) & (all_0_13_13 = e2 | all_0_13_13 = e0) & (all_0_13_13 = e2 | all_0_14_14 = e2) & (all_0_13_13 = e2 | all_0_23_23 = e2) & (all_0_13_13 = e0 | all_0_16_16 = e0) & (all_0_14_14 = e2 | all_0_14_14 = e1) & (all_0_14_14 = e2 | all_0_20_20 = e2) & (all_0_14_14 = e1 | all_0_17_17 = e1) & (all_0_15_15 = e1 | all_0_15_15 = e0) & (all_0_15_15 = e1 | all_0_17_17 = e1) & (all_0_15_15 = e1 | all_0_21_21 = e1) & (all_0_15_15 = e0 | all_0_16_16 = e0) & (all_0_15_15 = e0 | all_0_18_18 = e0) & (all_0_16_16 = e3 | all_0_16_16 = e0) & (all_0_16_16 = e3 | all_0_17_17 = e3) & (all_0_16_16 = e3 | all_0_23_23 = e3) & (all_0_17_17 = e3 | all_0_17_17 = e1) & (all_0_17_17 = e3 | all_0_20_20 = e3) & (all_0_18_18 = e2 | all_0_18_18 = e0) & (all_0_18_18 = e2 | all_0_20_20 = e2) & (all_0_18_18 = e2 | all_0_21_21 = e2) & (all_0_18_18 = e0 | all_0_19_19 = e0) & (all_0_19_19 = e3 | all_0_19_19 = e0) & (all_0_19_19 = e3 | all_0_20_20 = e3) & (all_0_19_19 = e3 | all_0_22_22 = e3) & (all_0_20_20 = e3 | all_0_20_20 = e2) & (all_0_21_21 = e2 | all_0_21_21 = e1) & (all_0_21_21 = e2 | all_0_23_23 = e2) & (all_0_21_21 = e1 | all_0_22_22 = e1) & (all_0_22_22 = e3 | all_0_22_22 = e1) & (all_0_22_22 = e3 | all_0_23_23 = e3) & (all_0_23_23 = e3 | all_0_23_23 = e2) % 5.89/1.95 | % 5.89/1.95 | Applying alpha-rule on (1) yields: % 5.89/1.95 | (2) ~ (all_0_10_10 = e1) | ~ (all_0_12_12 = e0) % 5.89/1.95 | (3) ~ (all_0_15_15 = all_0_17_17) % 5.89/1.95 | (4) ~ (all_0_4_4 = e1) | ~ (all_0_14_14 = e2) % 5.89/1.95 | (5) op(e2, e0) = all_0_17_17 % 5.89/1.95 | (6) ~ (e2 = e1) % 5.89/1.95 | (7) ~ (all_0_18_18 = e1) % 5.89/1.95 | (8) ~ (all_0_9_9 = e2) | ~ (all_0_18_18 = e0) % 5.89/1.95 | (9) ~ (all_0_0_0 = e2) | ~ (all_0_20_20 = e3) % 5.89/1.95 | (10) all_0_21_21 = e1 | all_0_22_22 = e1 % 5.89/1.95 | (11) all_0_19_19 = e3 | all_0_22_22 = e3 % 5.89/1.95 | (12) op(e2, e2) = e2 % 5.89/1.95 | (13) ~ (all_0_15_15 = e2) % 5.89/1.95 | (14) all_0_16_16 = e3 | all_0_17_17 = e3 % 5.89/1.95 | (15) ~ (all_0_1_1 = e3) | ~ (all_0_23_23 = e2) % 5.89/1.95 | (16) all_0_20_20 = e3 | all_0_20_20 = e2 % 5.89/1.95 | (17) ~ (all_0_16_16 = all_0_23_23) % 5.89/1.95 | (18) all_0_18_18 = e2 | all_0_18_18 = e0 % 5.89/1.95 | (19) ~ (all_0_11_11 = e0) | ~ (all_0_15_15 = e1) % 5.89/1.95 | (20) ~ (all_0_5_5 = e2) | ~ (all_0_21_21 = e1) % 5.89/1.95 | (21) all_0_12_12 = e1 | all_0_14_14 = e1 % 5.89/1.95 | (22) all_0_14_14 = e2 | all_0_20_20 = e2 % 5.89/1.95 | (23) op(all_0_19_19, e2) = all_0_7_7 % 5.89/1.95 | (24) all_0_14_14 = e2 | all_0_14_14 = e1 % 5.89/1.95 | (25) all_0_13_13 = e2 | all_0_14_14 = e2 % 5.89/1.95 | (26) all_0_12_12 = e1 | all_0_22_22 = e1 % 5.89/1.95 | (27) ~ (all_0_21_21 = all_0_23_23) % 5.89/1.95 | (28) op(all_0_18_18, e3) = all_0_9_9 % 5.89/1.95 | (29) all_0_15_15 = e1 | all_0_21_21 = e1 % 5.89/1.95 | (30) ~ (all_0_14_14 = e0) % 5.89/1.95 | (31) ~ (all_0_12_12 = all_0_22_22) % 5.89/1.95 | (32) ~ (all_0_7_7 = e0) | ~ (all_0_19_19 = e3) % 5.89/1.95 | (33) ~ (all_0_13_13 = all_0_14_14) % 5.89/1.95 | (34) ~ (all_0_16_16 = e1) % 5.89/1.95 | (35) all_0_22_22 = e3 | all_0_23_23 = e3 % 5.89/1.95 | (36) op(all_0_15_15, e3) = all_0_11_11 % 5.89/1.95 | (37) ~ (all_0_6_6 = e0) | ~ (all_0_16_16 = e3) % 5.89/1.95 | (38) all_0_21_21 = e2 | all_0_21_21 = e1 % 5.89/1.95 | (39) op(e2, e1) = all_0_16_16 % 5.89/1.95 | (40) op(all_0_13_13, e1) = all_0_8_8 % 5.89/1.96 | (41) ~ (all_0_3_3 = e3) | ~ (all_0_22_22 = e1) % 5.89/1.96 | (42) op(e0, e0) = e0 % 5.89/1.96 | (43) all_0_22_22 = e3 | all_0_22_22 = e1 % 5.89/1.96 | (44) op(e0, e2) = all_0_22_22 % 5.89/1.96 | (45) ~ (all_0_8_8 = e0) | ~ (all_0_13_13 = e2) % 5.89/1.96 | (46) ~ (all_0_13_13 = e3) % 5.89/1.96 | (47) ~ (all_0_18_18 = all_0_20_20) % 5.89/1.96 | (48) op(all_0_17_17, e0) = all_0_2_2 % 5.89/1.96 | (49) ~ (all_0_23_23 = e0) % 5.89/1.96 | (50) all_0_15_15 = e1 | all_0_17_17 = e1 % 5.89/1.96 | (51) ~ (all_0_9_9 = e0) | ~ (all_0_18_18 = e2) % 5.89/1.96 | (52) ~ (all_0_20_20 = e0) % 5.89/1.96 | (53) ~ (all_0_11_11 = e1) | ~ (all_0_15_15 = e0) % 5.89/1.96 | (54) op(e0, e1) = all_0_23_23 % 5.89/1.96 | (55) op(e1, e3) = all_0_18_18 % 5.89/1.96 | (56) all_0_17_17 = e3 | all_0_20_20 = e3 % 5.89/1.96 | (57) all_0_12_12 = e0 | all_0_13_13 = e0 % 5.89/1.96 | (58) all_0_16_16 = e3 | all_0_16_16 = e0 % 5.89/1.96 | (59) ~ (all_0_18_18 = all_0_19_19) % 5.89/1.96 | (60) ~ (all_0_12_12 = all_0_19_19) % 5.89/1.96 | (61) all_0_18_18 = e2 | all_0_21_21 = e2 % 5.89/1.96 | (62) all_0_18_18 = e0 | all_0_19_19 = e0 % 5.89/1.96 | (63) all_0_14_14 = e1 | all_0_17_17 = e1 % 5.89/1.96 | (64) all_0_16_16 = e3 | all_0_23_23 = e3 % 5.89/1.96 | (65) ~ (all_0_3_3 = e1) | ~ (all_0_22_22 = e3) % 5.89/1.96 | (66) ~ (all_0_12_12 = all_0_14_14) % 5.89/1.96 | (67) all_0_23_23 = e3 | all_0_23_23 = e2 % 5.89/1.96 | (68) ~ (e3 = e0) % 5.89/1.96 | (69) ~ (all_0_19_19 = e1) % 5.89/1.96 | (70) all_0_13_13 = e2 | all_0_13_13 = e0 % 5.89/1.96 | (71) all_0_15_15 = e0 | all_0_16_16 = e0 % 5.89/1.96 | (72) ~ (all_0_7_7 = e3) | ~ (all_0_19_19 = e0) % 5.89/1.96 | (73) all_0_15_15 = e0 | all_0_18_18 = e0 % 5.89/1.96 | (74) ~ (all_0_4_4 = e2) | ~ (all_0_14_14 = e1) % 5.89/1.96 | (75) ~ (all_0_10_10 = e0) | ~ (all_0_12_12 = e1) % 5.89/1.96 | (76) ~ (all_0_17_17 = e0) % 5.89/1.96 | (77) op(e3, e1) = all_0_13_13 % 5.89/1.96 | (78) ~ (e1 = e0) % 5.89/1.96 | (79) op(e3, e3) = e3 % 5.89/1.96 | (80) all_0_17_17 = e3 | all_0_17_17 = e1 % 5.89/1.96 | (81) all_0_15_15 = e1 | all_0_15_15 = e0 % 5.89/1.96 | (82) ~ (all_0_15_15 = all_0_21_21) % 5.89/1.96 | (83) ~ (all_0_13_13 = all_0_16_16) % 5.89/1.96 | (84) ~ (all_0_2_2 = e3) | ~ (all_0_17_17 = e1) % 5.89/1.96 | (85) all_0_13_13 = e2 | all_0_23_23 = e2 % 5.89/1.96 | (86) all_0_19_19 = e3 | all_0_20_20 = e3 % 5.89/1.96 | (87) ~ (all_0_16_16 = e2) % 5.89/1.96 | (88) ~ (e3 = e2) % 5.89/1.96 | (89) op(e3, e2) = all_0_12_12 % 5.89/1.96 | (90) ~ (all_0_21_21 = all_0_22_22) % 5.89/1.96 | (91) all_0_18_18 = e2 | all_0_20_20 = e2 % 5.89/1.96 | (92) ~ (all_0_8_8 = e2) | ~ (all_0_13_13 = e0) % 5.89/1.96 | (93) all_0_19_19 = e3 | all_0_19_19 = e0 % 5.89/1.96 | (94) all_0_21_21 = e2 | all_0_23_23 = e2 % 5.89/1.96 | (95) ~ (all_0_2_2 = e1) | ~ (all_0_17_17 = e3) % 5.89/1.96 | (96) ~ (all_0_23_23 = e1) % 5.89/1.96 | (97) op(e2, e3) = all_0_15_15 % 5.89/1.96 | (98) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op(v3, v2) = v1) | ~ (op(v3, v2) = v0)) % 5.89/1.96 | (99) ~ (all_0_21_21 = e0) % 5.89/1.96 | (100) ~ (all_0_17_17 = all_0_20_20) % 5.89/1.96 | (101) all_0_13_13 = e0 | all_0_16_16 = e0 % 5.89/1.96 | (102) ~ (all_0_14_14 = e3) % 5.89/1.96 | (103) op(e3, e0) = all_0_14_14 % 5.89/1.96 | (104) ~ (all_0_15_15 = all_0_18_18) % 5.89/1.96 | (105) ~ (all_0_21_21 = e3) % 5.89/1.96 | (106) ~ (all_0_22_22 = all_0_23_23) % 5.89/1.96 | (107) ~ (all_0_15_15 = e3) % 5.89/1.96 | (108) ~ (all_0_13_13 = e1) % 5.89/1.96 | (109) ~ (all_0_15_15 = all_0_16_16) % 5.89/1.97 | (110) ~ (all_0_1_1 = e2) | ~ (all_0_23_23 = e3) % 5.89/1.97 | (111) all_0_12_12 = e1 | all_0_12_12 = e0 % 5.89/1.97 | (112) ~ (all_0_0_0 = e3) | ~ (all_0_20_20 = e2) % 5.89/1.97 | (113) op(e1, e1) = e1 % 5.89/1.97 | (114) ~ (all_0_20_20 = e1) % 5.89/1.97 | (115) ~ (all_0_14_14 = all_0_20_20) % 5.89/1.97 | (116) ~ (all_0_5_5 = e1) | ~ (all_0_21_21 = e2) % 5.89/1.97 | (117) all_0_12_12 = e0 | all_0_19_19 = e0 % 5.89/1.97 | (118) op(all_0_16_16, e1) = all_0_6_6 % 5.89/1.97 | (119) op(all_0_23_23, e1) = all_0_1_1 % 5.89/1.97 | (120) ~ (all_0_16_16 = all_0_17_17) % 5.89/1.97 | (121) op(all_0_21_21, e3) = all_0_5_5 % 5.89/1.97 | (122) ~ (all_0_19_19 = all_0_22_22) % 5.89/1.97 | (123) ~ (e3 = e1) % 5.89/1.97 | (124) ~ (all_0_22_22 = e2) % 5.89/1.97 | (125) op(e0, e3) = all_0_21_21 % 5.89/1.97 | (126) ~ (all_0_12_12 = all_0_13_13) % 5.89/1.97 | (127) op(all_0_14_14, e0) = all_0_4_4 % 5.89/1.97 | (128) ~ (all_0_19_19 = all_0_20_20) % 5.89/1.97 | (129) op(all_0_12_12, e2) = all_0_10_10 % 5.89/1.97 | (130) ~ (e2 = e0) % 5.89/1.97 | (131) ~ (all_0_14_14 = all_0_17_17) % 5.89/1.97 | (132) ~ (all_0_6_6 = e3) | ~ (all_0_16_16 = e0) % 5.89/1.97 | (133) ~ (all_0_18_18 = all_0_21_21) % 5.89/1.97 | (134) ~ (all_0_22_22 = e0) % 5.89/1.97 | (135) op(e1, e0) = all_0_20_20 % 5.89/1.97 | (136) op(all_0_22_22, e2) = all_0_3_3 % 5.89/1.97 | (137) ~ (all_0_18_18 = e3) % 5.89/1.97 | (138) op(e1, e2) = all_0_19_19 % 5.89/1.97 | (139) ~ (all_0_13_13 = all_0_23_23) % 5.89/1.97 | (140) ~ (all_0_17_17 = e2) % 5.89/1.97 | (141) ~ (all_0_12_12 = e3) % 5.89/1.97 | (142) ~ (all_0_12_12 = e2) % 5.89/1.97 | (143) ~ (all_0_19_19 = e2) % 5.89/1.97 | (144) op(all_0_20_20, e0) = all_0_0_0 % 5.89/1.97 | % 5.89/1.97 +-Applying beta-rule and splitting (18), into two cases. % 5.89/1.97 |-Branch one: % 5.89/1.97 | (145) all_0_18_18 = e2 % 5.89/1.97 | % 5.89/1.97 +-Applying beta-rule and splitting (73), into two cases. % 5.89/1.97 |-Branch one: % 5.89/1.97 | (146) all_0_15_15 = e0 % 5.89/1.97 | % 5.89/1.97 | Equations (146) can reduce 3 to: % 5.89/1.97 | (147) ~ (all_0_17_17 = e0) % 5.89/1.97 | % 5.89/1.97 | Simplifying 147 yields: % 5.89/1.97 | (76) ~ (all_0_17_17 = e0) % 5.89/1.97 | % 5.89/1.97 | From (146) and (36) follows: % 5.89/1.97 | (149) op(e0, e3) = all_0_11_11 % 5.89/1.97 | % 5.89/1.97 +-Applying beta-rule and splitting (50), into two cases. % 5.89/1.97 |-Branch one: % 5.89/1.97 | (150) all_0_15_15 = e1 % 5.89/1.97 | % 5.89/1.97 | Combining equations (150,146) yields a new equation: % 5.89/1.97 | (151) e1 = e0 % 5.89/1.97 | % 5.89/1.97 | Simplifying 151 yields: % 5.89/1.97 | (152) e1 = e0 % 5.89/1.97 | % 5.89/1.97 | Equations (152) can reduce 78 to: % 5.89/1.97 | (153) $false % 5.89/1.97 | % 5.89/1.97 |-The branch is then unsatisfiable % 5.89/1.97 |-Branch two: % 5.89/1.98 | (154) ~ (all_0_15_15 = e1) % 5.89/1.98 | (155) all_0_17_17 = e1 % 5.89/1.98 | % 5.89/1.98 | Equations (155) can reduce 76 to: % 5.89/1.98 | (78) ~ (e1 = e0) % 5.89/1.98 | % 5.89/1.98 +-Applying beta-rule and splitting (29), into two cases. % 5.89/1.98 |-Branch one: % 5.89/1.98 | (150) all_0_15_15 = e1 % 5.89/1.98 | % 5.89/1.98 | Combining equations (150,146) yields a new equation: % 5.89/1.98 | (151) e1 = e0 % 5.89/1.98 | % 5.89/1.98 | Simplifying 151 yields: % 5.89/1.98 | (152) e1 = e0 % 5.89/1.98 | % 5.89/1.98 | Equations (152) can reduce 78 to: % 5.89/1.98 | (153) $false % 5.89/1.98 | % 5.89/1.98 |-The branch is then unsatisfiable % 5.89/1.98 |-Branch two: % 5.89/1.98 | (154) ~ (all_0_15_15 = e1) % 5.89/1.98 | (162) all_0_21_21 = e1 % 5.89/1.98 | % 5.89/1.98 | From (162) and (125) follows: % 5.89/1.98 | (163) op(e0, e3) = e1 % 5.89/1.98 | % 5.89/1.98 +-Applying beta-rule and splitting (53), into two cases. % 5.89/1.98 |-Branch one: % 5.89/1.98 | (164) ~ (all_0_11_11 = e1) % 5.89/1.98 | % 5.89/1.98 | Instantiating formula (98) with e0, e3, e1, all_0_11_11 and discharging atoms op(e0, e3) = all_0_11_11, op(e0, e3) = e1, yields: % 5.89/1.98 | (165) all_0_11_11 = e1 % 5.89/1.98 | % 5.89/1.98 | Equations (165) can reduce 164 to: % 5.89/1.98 | (153) $false % 5.89/1.98 | % 5.89/1.98 |-The branch is then unsatisfiable % 5.89/1.98 |-Branch two: % 5.89/1.98 | (165) all_0_11_11 = e1 % 5.89/1.98 | (168) ~ (all_0_15_15 = e0) % 5.89/1.98 | % 5.89/1.98 | Equations (146) can reduce 168 to: % 5.89/1.98 | (153) $false % 5.89/1.98 | % 5.89/1.98 |-The branch is then unsatisfiable % 5.89/1.98 |-Branch two: % 5.89/1.98 | (168) ~ (all_0_15_15 = e0) % 6.09/1.98 | (171) all_0_18_18 = e0 % 6.09/1.98 | % 6.09/1.98 | Combining equations (171,145) yields a new equation: % 6.09/1.98 | (172) e2 = e0 % 6.09/1.98 | % 6.09/1.98 | Equations (172) can reduce 130 to: % 6.09/1.98 | (153) $false % 6.09/1.98 | % 6.09/1.98 |-The branch is then unsatisfiable % 6.09/1.98 |-Branch two: % 6.09/1.98 | (174) ~ (all_0_18_18 = e2) % 6.09/1.98 | (171) all_0_18_18 = e0 % 6.09/1.98 | % 6.09/1.98 | Equations (171) can reduce 174 to: % 6.09/1.98 | (176) ~ (e2 = e0) % 6.09/1.98 | % 6.09/1.98 | Simplifying 176 yields: % 6.09/1.98 | (130) ~ (e2 = e0) % 6.09/1.98 | % 6.09/1.98 | From (171) and (55) follows: % 6.09/1.98 | (178) op(e1, e3) = e0 % 6.09/1.98 | % 6.09/1.98 +-Applying beta-rule and splitting (61), into two cases. % 6.09/1.98 |-Branch one: % 6.09/1.98 | (145) all_0_18_18 = e2 % 6.09/1.98 | % 6.09/1.98 | Combining equations (145,171) yields a new equation: % 6.09/1.98 | (180) e2 = e0 % 6.09/1.98 | % 6.09/1.98 | Simplifying 180 yields: % 6.09/1.98 | (172) e2 = e0 % 6.09/1.98 | % 6.09/1.98 | Equations (172) can reduce 130 to: % 6.09/1.98 | (153) $false % 6.09/1.98 | % 6.09/1.98 |-The branch is then unsatisfiable % 6.09/1.98 |-Branch two: % 6.09/1.98 | (174) ~ (all_0_18_18 = e2) % 6.09/1.98 | (184) all_0_21_21 = e2 % 6.09/1.98 | % 6.09/1.98 +-Applying beta-rule and splitting (29), into two cases. % 6.09/1.98 |-Branch one: % 6.09/1.98 | (150) all_0_15_15 = e1 % 6.09/1.98 | % 6.09/1.98 | From (150) and (36) follows: % 6.09/1.99 | (186) op(e1, e3) = all_0_11_11 % 6.09/1.99 | % 6.09/1.99 +-Applying beta-rule and splitting (19), into two cases. % 6.09/1.99 |-Branch one: % 6.09/1.99 | (187) ~ (all_0_11_11 = e0) % 6.09/1.99 | % 6.09/1.99 | Instantiating formula (98) with e1, e3, e0, all_0_11_11 and discharging atoms op(e1, e3) = all_0_11_11, op(e1, e3) = e0, yields: % 6.09/1.99 | (188) all_0_11_11 = e0 % 6.09/1.99 | % 6.09/1.99 | Equations (188) can reduce 187 to: % 6.09/1.99 | (153) $false % 6.09/1.99 | % 6.09/1.99 |-The branch is then unsatisfiable % 6.09/1.99 |-Branch two: % 6.09/1.99 | (188) all_0_11_11 = e0 % 6.09/1.99 | (154) ~ (all_0_15_15 = e1) % 6.09/1.99 | % 6.09/1.99 | Equations (150) can reduce 154 to: % 6.09/1.99 | (153) $false % 6.09/1.99 | % 6.09/1.99 |-The branch is then unsatisfiable % 6.09/1.99 |-Branch two: % 6.09/1.99 | (154) ~ (all_0_15_15 = e1) % 6.09/1.99 | (162) all_0_21_21 = e1 % 6.09/1.99 | % 6.09/1.99 | Combining equations (162,184) yields a new equation: % 6.09/1.99 | (195) e2 = e1 % 6.09/1.99 | % 6.09/1.99 | Equations (195) can reduce 6 to: % 6.09/1.99 | (153) $false % 6.09/1.99 | % 6.09/1.99 |-The branch is then unsatisfiable % 6.09/1.99 % SZS output end Proof for theBenchmark % 6.09/1.99 % 6.09/1.99 1397ms %------------------------------------------------------------------------------