%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : ALG070+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n026.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:34:13 EDT 2022 % Result : Theorem 2.43s 1.21s % Output : Proof 4.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : ALG070+1 : TPTP v8.1.0. Released v2.7.0. % 0.07/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.32 % Computer : n026.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % 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 22:12:46 EDT 2022 % 0.12/0.33 % CPUTime : % 0.53/0.57 ____ _ % 0.53/0.57 ___ / __ \_____(_)___ ________ __________ % 0.53/0.57 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.53/0.57 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.53/0.57 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.53/0.57 % 0.53/0.57 A Theorem Prover for First-Order Logic % 0.53/0.57 (ePrincess v.1.0) % 0.53/0.57 % 0.53/0.57 (c) Philipp Rümmer, 2009-2015 % 0.53/0.57 (c) Peter Backeman, 2014-2015 % 0.53/0.57 (contributions by Angelo Brillout, Peter Baumgartner) % 0.53/0.57 Free software under GNU Lesser General Public License (LGPL). % 0.53/0.57 Bug reports to peter@backeman.se % 0.53/0.57 % 0.53/0.57 For more information, visit http://user.uu.se/~petba168/breu/ % 0.53/0.57 % 0.53/0.57 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.53/0.62 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.46/0.87 Prover 0: Preprocessing ... % 1.75/1.04 Prover 0: Constructing countermodel ... % 2.43/1.21 Prover 0: proved (592ms) % 2.43/1.21 % 2.43/1.21 No countermodel exists, formula is valid % 2.43/1.21 % SZS status Theorem for theBenchmark % 2.43/1.21 % 2.43/1.21 Generating proof ... found it (size 105) % 3.78/1.63 % 3.78/1.63 % SZS output start Proof for theBenchmark % 3.78/1.63 Assumed formulas after preprocessing and simplification: % 3.78/1.63 | (0) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = v0) & op2(v0, v1) = v2 & op2(v0, v0) = v1 & sorti2(v1) & sorti2(v0) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v4 = v3 | ~ (op2(v6, v5) = v4) | ~ (op2(v6, v5) = v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v4 = v3 | ~ (op1(v6, v5) = v4) | ~ (op1(v6, v5) = v3)) & ! [v3] : ! [v4] : ! [v5] : (v5 = v3 | ~ (op1(v3, v4) = v5) | ~ (op1(v3, v3) = v4) | ~ sorti1(v4) | ~ sorti1(v3)) & ! [v3] : ! [v4] : ! [v5] : (v4 = v3 | ~ (j(v5) = v4) | ~ (j(v5) = v3)) & ! [v3] : ! [v4] : ! [v5] : (v4 = v3 | ~ (h(v5) = v4) | ~ (h(v5) = v3)) & ! [v3] : ! [v4] : ! [v5] : ( ~ (op2(v3, v4) = v5) | ~ sorti2(v4) | ~ sorti2(v3) | sorti2(v5)) & ! [v3] : ! [v4] : ! [v5] : ( ~ (op1(v3, v4) = v5) | ~ sorti1(v4) | ~ sorti1(v3) | sorti1(v5)) & ! [v3] : ( ~ sorti2(v3) | ? [v4] : (j(v3) = v4 & h(v4) = v3)) & ! [v3] : ( ~ sorti2(v3) | ? [v4] : (j(v3) = v4 & sorti1(v4))) & ! [v3] : ( ~ sorti2(v3) | ? [v4] : (j(v3) = v4 & ! [v5] : ( ~ sorti2(v5) | ? [v6] : ? [v7] : ? [v8] : (j(v6) = v7 & j(v5) = v8 & op2(v3, v5) = v6 & op1(v4, v8) = v7)))) & ! [v3] : ( ~ sorti1(v3) | ? [v4] : (j(v4) = v3 & h(v3) = v4)) & ! [v3] : ( ~ sorti1(v3) | ? [v4] : (h(v3) = v4 & sorti2(v4))) & ! [v3] : ( ~ sorti1(v3) | ? [v4] : (h(v3) = v4 & ! [v5] : ( ~ sorti1(v5) | ? [v6] : ? [v7] : ? [v8] : (h(v6) = v7 & h(v5) = v8 & op2(v4, v8) = v7 & op1(v3, v5) = v6))))) % 4.03/1.66 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2 yields: % 4.03/1.66 | (1) ~ (all_0_0_0 = all_0_2_2) & op2(all_0_2_2, all_0_1_1) = all_0_0_0 & op2(all_0_2_2, all_0_2_2) = all_0_1_1 & sorti2(all_0_1_1) & sorti2(all_0_2_2) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op2(v3, v2) = v1) | ~ (op2(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op1(v3, v2) = v1) | ~ (op1(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v0 | ~ (op1(v0, v1) = v2) | ~ (op1(v0, v0) = v1) | ~ sorti1(v1) | ~ sorti1(v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (j(v2) = v1) | ~ (j(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h(v2) = v1) | ~ (h(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (op2(v0, v1) = v2) | ~ sorti2(v1) | ~ sorti2(v0) | sorti2(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (op1(v0, v1) = v2) | ~ sorti1(v1) | ~ sorti1(v0) | sorti1(v2)) & ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & h(v1) = v0)) & ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & sorti1(v1))) & ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & ! [v2] : ( ~ sorti2(v2) | ? [v3] : ? [v4] : ? [v5] : (j(v3) = v4 & j(v2) = v5 & op2(v0, v2) = v3 & op1(v1, v5) = v4)))) & ! [v0] : ( ~ sorti1(v0) | ? [v1] : (j(v1) = v0 & h(v0) = v1)) & ! [v0] : ( ~ sorti1(v0) | ? [v1] : (h(v0) = v1 & sorti2(v1))) & ! [v0] : ( ~ sorti1(v0) | ? [v1] : (h(v0) = v1 & ! [v2] : ( ~ sorti1(v2) | ? [v3] : ? [v4] : ? [v5] : (h(v3) = v4 & h(v2) = v5 & op2(v1, v5) = v4 & op1(v0, v2) = v3)))) % 4.03/1.67 | % 4.03/1.67 | Applying alpha-rule on (1) yields: % 4.03/1.67 | (2) ! [v0] : ! [v1] : ! [v2] : (v2 = v0 | ~ (op1(v0, v1) = v2) | ~ (op1(v0, v0) = v1) | ~ sorti1(v1) | ~ sorti1(v0)) % 4.03/1.67 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op2(v3, v2) = v1) | ~ (op2(v3, v2) = v0)) % 4.03/1.67 | (4) ! [v0] : ( ~ sorti1(v0) | ? [v1] : (j(v1) = v0 & h(v0) = v1)) % 4.03/1.67 | (5) op2(all_0_2_2, all_0_2_2) = all_0_1_1 % 4.03/1.67 | (6) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (j(v2) = v1) | ~ (j(v2) = v0)) % 4.03/1.67 | (7) ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & h(v1) = v0)) % 4.03/1.67 | (8) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h(v2) = v1) | ~ (h(v2) = v0)) % 4.03/1.67 | (9) ! [v0] : ( ~ sorti1(v0) | ? [v1] : (h(v0) = v1 & ! [v2] : ( ~ sorti1(v2) | ? [v3] : ? [v4] : ? [v5] : (h(v3) = v4 & h(v2) = v5 & op2(v1, v5) = v4 & op1(v0, v2) = v3)))) % 4.03/1.67 | (10) ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & ! [v2] : ( ~ sorti2(v2) | ? [v3] : ? [v4] : ? [v5] : (j(v3) = v4 & j(v2) = v5 & op2(v0, v2) = v3 & op1(v1, v5) = v4)))) % 4.03/1.67 | (11) ! [v0] : ! [v1] : ! [v2] : ( ~ (op1(v0, v1) = v2) | ~ sorti1(v1) | ~ sorti1(v0) | sorti1(v2)) % 4.03/1.67 | (12) ~ (all_0_0_0 = all_0_2_2) % 4.03/1.67 | (13) ! [v0] : ( ~ sorti1(v0) | ? [v1] : (h(v0) = v1 & sorti2(v1))) % 4.03/1.67 | (14) sorti2(all_0_1_1) % 4.03/1.67 | (15) sorti2(all_0_2_2) % 4.03/1.67 | (16) ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & sorti1(v1))) % 4.03/1.67 | (17) op2(all_0_2_2, all_0_1_1) = all_0_0_0 % 4.03/1.67 | (18) ! [v0] : ! [v1] : ! [v2] : ( ~ (op2(v0, v1) = v2) | ~ sorti2(v1) | ~ sorti2(v0) | sorti2(v2)) % 4.03/1.67 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op1(v3, v2) = v1) | ~ (op1(v3, v2) = v0)) % 4.03/1.67 | % 4.03/1.67 | Instantiating formula (7) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 4.03/1.67 | (20) ? [v0] : (j(all_0_1_1) = v0 & h(v0) = all_0_1_1) % 4.03/1.67 | % 4.03/1.67 | Instantiating formula (16) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 4.03/1.67 | (21) ? [v0] : (j(all_0_1_1) = v0 & sorti1(v0)) % 4.03/1.68 | % 4.03/1.68 | Instantiating formula (10) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 4.03/1.68 | (22) ? [v0] : (j(all_0_1_1) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_0_1_1, v1) = v2 & op1(v0, v4) = v3))) % 4.03/1.68 | % 4.03/1.68 | Instantiating formula (7) with all_0_2_2 and discharging atoms sorti2(all_0_2_2), yields: % 4.03/1.68 | (23) ? [v0] : (j(all_0_2_2) = v0 & h(v0) = all_0_2_2) % 4.03/1.68 | % 4.03/1.68 | Instantiating formula (16) with all_0_2_2 and discharging atoms sorti2(all_0_2_2), yields: % 4.03/1.68 | (24) ? [v0] : (j(all_0_2_2) = v0 & sorti1(v0)) % 4.03/1.68 | % 4.03/1.68 | Instantiating formula (10) with all_0_2_2 and discharging atoms sorti2(all_0_2_2), yields: % 4.03/1.68 | (25) ? [v0] : (j(all_0_2_2) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_0_2_2, v1) = v2 & op1(v0, v4) = v3))) % 4.03/1.68 | % 4.03/1.68 | Instantiating (25) with all_9_0_3 yields: % 4.03/1.68 | (26) j(all_0_2_2) = all_9_0_3 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_0_2_2, v0) = v1 & op1(all_9_0_3, v3) = v2)) % 4.03/1.68 | % 4.03/1.68 | Applying alpha-rule on (26) yields: % 4.03/1.68 | (27) j(all_0_2_2) = all_9_0_3 % 4.03/1.68 | (28) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_0_2_2, v0) = v1 & op1(all_9_0_3, v3) = v2)) % 4.03/1.68 | % 4.03/1.68 | Instantiating formula (28) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 4.16/1.68 | (29) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_1_1) = v2 & op2(all_0_2_2, all_0_1_1) = v0 & op1(all_9_0_3, v2) = v1) % 4.16/1.68 | % 4.16/1.68 | Instantiating formula (28) with all_0_2_2 and discharging atoms sorti2(all_0_2_2), yields: % 4.16/1.68 | (30) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_2_2) = v2 & op2(all_0_2_2, all_0_2_2) = v0 & op1(all_9_0_3, v2) = v1) % 4.16/1.68 | % 4.16/1.68 | Instantiating (24) with all_12_0_4 yields: % 4.16/1.68 | (31) j(all_0_2_2) = all_12_0_4 & sorti1(all_12_0_4) % 4.16/1.68 | % 4.16/1.68 | Applying alpha-rule on (31) yields: % 4.16/1.68 | (32) j(all_0_2_2) = all_12_0_4 % 4.16/1.68 | (33) sorti1(all_12_0_4) % 4.16/1.68 | % 4.16/1.68 | Instantiating (21) with all_14_0_5 yields: % 4.16/1.68 | (34) j(all_0_1_1) = all_14_0_5 & sorti1(all_14_0_5) % 4.16/1.68 | % 4.16/1.68 | Applying alpha-rule on (34) yields: % 4.16/1.68 | (35) j(all_0_1_1) = all_14_0_5 % 4.16/1.68 | (36) sorti1(all_14_0_5) % 4.16/1.68 | % 4.16/1.68 | Instantiating (20) with all_16_0_6 yields: % 4.16/1.68 | (37) j(all_0_1_1) = all_16_0_6 & h(all_16_0_6) = all_0_1_1 % 4.16/1.68 | % 4.16/1.68 | Applying alpha-rule on (37) yields: % 4.16/1.68 | (38) j(all_0_1_1) = all_16_0_6 % 4.16/1.68 | (39) h(all_16_0_6) = all_0_1_1 % 4.16/1.68 | % 4.16/1.68 | Instantiating (23) with all_18_0_7 yields: % 4.16/1.68 | (40) j(all_0_2_2) = all_18_0_7 & h(all_18_0_7) = all_0_2_2 % 4.16/1.68 | % 4.16/1.68 | Applying alpha-rule on (40) yields: % 4.16/1.68 | (41) j(all_0_2_2) = all_18_0_7 % 4.16/1.68 | (42) h(all_18_0_7) = all_0_2_2 % 4.16/1.68 | % 4.16/1.68 | Instantiating (22) with all_20_0_8 yields: % 4.16/1.68 | (43) j(all_0_1_1) = all_20_0_8 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_0_1_1, v0) = v1 & op1(all_20_0_8, v3) = v2)) % 4.16/1.68 | % 4.16/1.68 | Applying alpha-rule on (43) yields: % 4.16/1.68 | (44) j(all_0_1_1) = all_20_0_8 % 4.16/1.68 | (45) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_0_1_1, v0) = v1 & op1(all_20_0_8, v3) = v2)) % 4.16/1.68 | % 4.16/1.68 | Instantiating formula (45) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 4.16/1.68 | (46) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_1_1) = v2 & op2(all_0_1_1, all_0_1_1) = v0 & op1(all_20_0_8, v2) = v1) % 4.16/1.68 | % 4.16/1.68 | Instantiating formula (45) with all_0_2_2 and discharging atoms sorti2(all_0_2_2), yields: % 4.16/1.68 | (47) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_2_2) = v2 & op2(all_0_1_1, all_0_2_2) = v0 & op1(all_20_0_8, v2) = v1) % 4.16/1.69 | % 4.16/1.69 | Instantiating (30) with all_23_0_9, all_23_1_10, all_23_2_11 yields: % 4.16/1.69 | (48) j(all_23_2_11) = all_23_1_10 & j(all_0_2_2) = all_23_0_9 & op2(all_0_2_2, all_0_2_2) = all_23_2_11 & op1(all_9_0_3, all_23_0_9) = all_23_1_10 % 4.16/1.69 | % 4.16/1.69 | Applying alpha-rule on (48) yields: % 4.16/1.69 | (49) j(all_23_2_11) = all_23_1_10 % 4.16/1.69 | (50) j(all_0_2_2) = all_23_0_9 % 4.16/1.69 | (51) op2(all_0_2_2, all_0_2_2) = all_23_2_11 % 4.16/1.69 | (52) op1(all_9_0_3, all_23_0_9) = all_23_1_10 % 4.16/1.69 | % 4.16/1.69 | Instantiating (29) with all_25_0_12, all_25_1_13, all_25_2_14 yields: % 4.16/1.69 | (53) j(all_25_2_14) = all_25_1_13 & j(all_0_1_1) = all_25_0_12 & op2(all_0_2_2, all_0_1_1) = all_25_2_14 & op1(all_9_0_3, all_25_0_12) = all_25_1_13 % 4.16/1.69 | % 4.16/1.69 | Applying alpha-rule on (53) yields: % 4.16/1.69 | (54) j(all_25_2_14) = all_25_1_13 % 4.16/1.69 | (55) j(all_0_1_1) = all_25_0_12 % 4.16/1.69 | (56) op2(all_0_2_2, all_0_1_1) = all_25_2_14 % 4.16/1.69 | (57) op1(all_9_0_3, all_25_0_12) = all_25_1_13 % 4.16/1.69 | % 4.16/1.69 | Instantiating (47) with all_27_0_15, all_27_1_16, all_27_2_17 yields: % 4.16/1.69 | (58) j(all_27_2_17) = all_27_1_16 & j(all_0_2_2) = all_27_0_15 & op2(all_0_1_1, all_0_2_2) = all_27_2_17 & op1(all_20_0_8, all_27_0_15) = all_27_1_16 % 4.16/1.69 | % 4.16/1.69 | Applying alpha-rule on (58) yields: % 4.16/1.69 | (59) j(all_27_2_17) = all_27_1_16 % 4.16/1.69 | (60) j(all_0_2_2) = all_27_0_15 % 4.16/1.69 | (61) op2(all_0_1_1, all_0_2_2) = all_27_2_17 % 4.16/1.69 | (62) op1(all_20_0_8, all_27_0_15) = all_27_1_16 % 4.16/1.69 | % 4.16/1.69 | Instantiating (46) with all_29_0_18, all_29_1_19, all_29_2_20 yields: % 4.16/1.69 | (63) j(all_29_2_20) = all_29_1_19 & j(all_0_1_1) = all_29_0_18 & op2(all_0_1_1, all_0_1_1) = all_29_2_20 & op1(all_20_0_8, all_29_0_18) = all_29_1_19 % 4.16/1.69 | % 4.16/1.69 | Applying alpha-rule on (63) yields: % 4.16/1.69 | (64) j(all_29_2_20) = all_29_1_19 % 4.16/1.69 | (65) j(all_0_1_1) = all_29_0_18 % 4.16/1.69 | (66) op2(all_0_1_1, all_0_1_1) = all_29_2_20 % 4.16/1.69 | (67) op1(all_20_0_8, all_29_0_18) = all_29_1_19 % 4.16/1.69 | % 4.16/1.69 | Instantiating formula (6) with all_0_1_1, all_25_0_12, all_29_0_18 and discharging atoms j(all_0_1_1) = all_29_0_18, j(all_0_1_1) = all_25_0_12, yields: % 4.16/1.69 | (68) all_29_0_18 = all_25_0_12 % 4.16/1.69 | % 4.16/1.69 | Instantiating formula (6) with all_0_1_1, all_20_0_8, all_25_0_12 and discharging atoms j(all_0_1_1) = all_25_0_12, j(all_0_1_1) = all_20_0_8, yields: % 4.16/1.69 | (69) all_25_0_12 = all_20_0_8 % 4.16/1.69 | % 4.16/1.69 | Instantiating formula (6) with all_0_1_1, all_16_0_6, all_20_0_8 and discharging atoms j(all_0_1_1) = all_20_0_8, j(all_0_1_1) = all_16_0_6, yields: % 4.16/1.69 | (70) all_20_0_8 = all_16_0_6 % 4.16/1.69 | % 4.16/1.69 | Instantiating formula (6) with all_0_1_1, all_14_0_5, all_29_0_18 and discharging atoms j(all_0_1_1) = all_29_0_18, j(all_0_1_1) = all_14_0_5, yields: % 4.16/1.69 | (71) all_29_0_18 = all_14_0_5 % 4.16/1.69 | % 4.16/1.69 | Instantiating formula (6) with all_0_2_2, all_23_0_9, all_27_0_15 and discharging atoms j(all_0_2_2) = all_27_0_15, j(all_0_2_2) = all_23_0_9, yields: % 4.16/1.69 | (72) all_27_0_15 = all_23_0_9 % 4.16/1.69 | % 4.16/1.69 | Instantiating formula (6) with all_0_2_2, all_18_0_7, all_27_0_15 and discharging atoms j(all_0_2_2) = all_27_0_15, j(all_0_2_2) = all_18_0_7, yields: % 4.16/1.69 | (73) all_27_0_15 = all_18_0_7 % 4.16/1.69 | % 4.16/1.69 | Instantiating formula (6) with all_0_2_2, all_12_0_4, all_27_0_15 and discharging atoms j(all_0_2_2) = all_27_0_15, j(all_0_2_2) = all_12_0_4, yields: % 4.16/1.69 | (74) all_27_0_15 = all_12_0_4 % 4.16/1.69 | % 4.16/1.69 | Instantiating formula (6) with all_0_2_2, all_9_0_3, all_27_0_15 and discharging atoms j(all_0_2_2) = all_27_0_15, j(all_0_2_2) = all_9_0_3, yields: % 4.16/1.69 | (75) all_27_0_15 = all_9_0_3 % 4.16/1.69 | % 4.16/1.69 | Instantiating formula (3) with all_0_2_2, all_0_1_1, all_25_2_14, all_0_0_0 and discharging atoms op2(all_0_2_2, all_0_1_1) = all_25_2_14, op2(all_0_2_2, all_0_1_1) = all_0_0_0, yields: % 4.16/1.69 | (76) all_25_2_14 = all_0_0_0 % 4.16/1.69 | % 4.16/1.69 | Instantiating formula (3) with all_0_2_2, all_0_2_2, all_23_2_11, all_0_1_1 and discharging atoms op2(all_0_2_2, all_0_2_2) = all_23_2_11, op2(all_0_2_2, all_0_2_2) = all_0_1_1, yields: % 4.16/1.69 | (77) all_23_2_11 = all_0_1_1 % 4.16/1.69 | % 4.16/1.69 | Combining equations (68,71) yields a new equation: % 4.16/1.69 | (78) all_25_0_12 = all_14_0_5 % 4.16/1.70 | % 4.16/1.70 | Simplifying 78 yields: % 4.16/1.70 | (79) all_25_0_12 = all_14_0_5 % 4.16/1.70 | % 4.16/1.70 | Combining equations (74,72) yields a new equation: % 4.16/1.70 | (80) all_23_0_9 = all_12_0_4 % 4.16/1.70 | % 4.16/1.70 | Combining equations (73,72) yields a new equation: % 4.16/1.70 | (81) all_23_0_9 = all_18_0_7 % 4.16/1.70 | % 4.16/1.70 | Combining equations (75,72) yields a new equation: % 4.16/1.70 | (82) all_23_0_9 = all_9_0_3 % 4.16/1.70 | % 4.16/1.70 | Combining equations (69,79) yields a new equation: % 4.16/1.70 | (83) all_20_0_8 = all_14_0_5 % 4.16/1.70 | % 4.16/1.70 | Simplifying 83 yields: % 4.16/1.70 | (84) all_20_0_8 = all_14_0_5 % 4.16/1.70 | % 4.16/1.70 | Combining equations (82,81) yields a new equation: % 4.16/1.70 | (85) all_18_0_7 = all_9_0_3 % 4.16/1.70 | % 4.16/1.70 | Combining equations (80,81) yields a new equation: % 4.16/1.70 | (86) all_18_0_7 = all_12_0_4 % 4.16/1.70 | % 4.16/1.70 | Combining equations (70,84) yields a new equation: % 4.16/1.70 | (87) all_16_0_6 = all_14_0_5 % 4.16/1.70 | % 4.16/1.70 | Simplifying 87 yields: % 4.16/1.70 | (88) all_16_0_6 = all_14_0_5 % 4.16/1.70 | % 4.16/1.70 | Combining equations (86,85) yields a new equation: % 4.16/1.70 | (89) all_12_0_4 = all_9_0_3 % 4.16/1.70 | % 4.16/1.70 | Simplifying 89 yields: % 4.16/1.70 | (90) all_12_0_4 = all_9_0_3 % 4.16/1.70 | % 4.16/1.70 | Combining equations (85,81) yields a new equation: % 4.16/1.70 | (82) all_23_0_9 = all_9_0_3 % 4.16/1.70 | % 4.16/1.70 | From (77) and (49) follows: % 4.16/1.70 | (92) j(all_0_1_1) = all_23_1_10 % 4.16/1.70 | % 4.16/1.70 | From (88) and (38) follows: % 4.16/1.70 | (35) j(all_0_1_1) = all_14_0_5 % 4.16/1.70 | % 4.16/1.70 | From (85) and (42) follows: % 4.16/1.70 | (94) h(all_9_0_3) = all_0_2_2 % 4.16/1.70 | % 4.16/1.70 | From (88) and (39) follows: % 4.16/1.70 | (95) h(all_14_0_5) = all_0_1_1 % 4.16/1.70 | % 4.16/1.70 | From (76) and (56) follows: % 4.16/1.70 | (17) op2(all_0_2_2, all_0_1_1) = all_0_0_0 % 4.16/1.70 | % 4.16/1.70 | From (82) and (52) follows: % 4.16/1.70 | (97) op1(all_9_0_3, all_9_0_3) = all_23_1_10 % 4.16/1.70 | % 4.16/1.70 | From (90) and (33) follows: % 4.16/1.70 | (98) sorti1(all_9_0_3) % 4.16/1.70 | % 4.16/1.70 | Instantiating formula (6) with all_0_1_1, all_23_1_10, all_14_0_5 and discharging atoms j(all_0_1_1) = all_23_1_10, j(all_0_1_1) = all_14_0_5, yields: % 4.16/1.70 | (99) all_23_1_10 = all_14_0_5 % 4.16/1.70 | % 4.16/1.70 | From (99) and (97) follows: % 4.16/1.70 | (100) op1(all_9_0_3, all_9_0_3) = all_14_0_5 % 4.16/1.70 | % 4.16/1.70 | Instantiating formula (9) with all_14_0_5 and discharging atoms sorti1(all_14_0_5), yields: % 4.16/1.70 | (101) ? [v0] : (h(all_14_0_5) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_14_0_5, v1) = v2))) % 4.16/1.70 | % 4.16/1.70 | Instantiating formula (9) with all_9_0_3 and discharging atoms sorti1(all_9_0_3), yields: % 4.16/1.70 | (102) ? [v0] : (h(all_9_0_3) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_9_0_3, v1) = v2))) % 4.16/1.70 | % 4.16/1.70 | Instantiating (102) with all_58_0_29 yields: % 4.16/1.70 | (103) h(all_9_0_3) = all_58_0_29 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_58_0_29, v3) = v2 & op1(all_9_0_3, v0) = v1)) % 4.16/1.70 | % 4.16/1.70 | Applying alpha-rule on (103) yields: % 4.16/1.70 | (104) h(all_9_0_3) = all_58_0_29 % 4.16/1.70 | (105) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_58_0_29, v3) = v2 & op1(all_9_0_3, v0) = v1)) % 4.16/1.70 | % 4.16/1.70 | Instantiating formula (105) with all_14_0_5 and discharging atoms sorti1(all_14_0_5), yields: % 4.16/1.70 | (106) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_14_0_5) = v2 & op2(all_58_0_29, v2) = v1 & op1(all_9_0_3, all_14_0_5) = v0) % 4.16/1.70 | % 4.16/1.71 | Instantiating formula (105) with all_9_0_3 and discharging atoms sorti1(all_9_0_3), yields: % 4.16/1.71 | (107) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_9_0_3) = v2 & op2(all_58_0_29, v2) = v1 & op1(all_9_0_3, all_9_0_3) = v0) % 4.16/1.71 | % 4.16/1.71 | Instantiating (101) with all_61_0_30 yields: % 4.16/1.71 | (108) h(all_14_0_5) = all_61_0_30 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_61_0_30, v3) = v2 & op1(all_14_0_5, v0) = v1)) % 4.16/1.71 | % 4.16/1.71 | Applying alpha-rule on (108) yields: % 4.16/1.71 | (109) h(all_14_0_5) = all_61_0_30 % 4.16/1.71 | (110) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_61_0_30, v3) = v2 & op1(all_14_0_5, v0) = v1)) % 4.16/1.71 | % 4.16/1.71 | Instantiating formula (110) with all_14_0_5 and discharging atoms sorti1(all_14_0_5), yields: % 4.16/1.71 | (111) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_14_0_5) = v2 & op2(all_61_0_30, v2) = v1 & op1(all_14_0_5, all_14_0_5) = v0) % 4.16/1.71 | % 4.16/1.71 | Instantiating formula (110) with all_9_0_3 and discharging atoms sorti1(all_9_0_3), yields: % 4.16/1.71 | (112) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_9_0_3) = v2 & op2(all_61_0_30, v2) = v1 & op1(all_14_0_5, all_9_0_3) = v0) % 4.16/1.71 | % 4.16/1.71 | Instantiating (107) with all_70_0_40, all_70_1_41, all_70_2_42 yields: % 4.16/1.71 | (113) h(all_70_2_42) = all_70_1_41 & h(all_9_0_3) = all_70_0_40 & op2(all_58_0_29, all_70_0_40) = all_70_1_41 & op1(all_9_0_3, all_9_0_3) = all_70_2_42 % 4.16/1.71 | % 4.16/1.71 | Applying alpha-rule on (113) yields: % 4.16/1.71 | (114) h(all_70_2_42) = all_70_1_41 % 4.16/1.71 | (115) h(all_9_0_3) = all_70_0_40 % 4.16/1.71 | (116) op2(all_58_0_29, all_70_0_40) = all_70_1_41 % 4.16/1.71 | (117) op1(all_9_0_3, all_9_0_3) = all_70_2_42 % 4.16/1.71 | % 4.16/1.71 | Instantiating (106) with all_72_0_43, all_72_1_44, all_72_2_45 yields: % 4.16/1.71 | (118) h(all_72_2_45) = all_72_1_44 & h(all_14_0_5) = all_72_0_43 & op2(all_58_0_29, all_72_0_43) = all_72_1_44 & op1(all_9_0_3, all_14_0_5) = all_72_2_45 % 4.16/1.71 | % 4.16/1.71 | Applying alpha-rule on (118) yields: % 4.16/1.71 | (119) h(all_72_2_45) = all_72_1_44 % 4.16/1.71 | (120) h(all_14_0_5) = all_72_0_43 % 4.16/1.71 | (121) op2(all_58_0_29, all_72_0_43) = all_72_1_44 % 4.16/1.71 | (122) op1(all_9_0_3, all_14_0_5) = all_72_2_45 % 4.16/1.71 | % 4.16/1.71 | Instantiating (112) with all_74_0_46, all_74_1_47, all_74_2_48 yields: % 4.16/1.71 | (123) h(all_74_2_48) = all_74_1_47 & h(all_9_0_3) = all_74_0_46 & op2(all_61_0_30, all_74_0_46) = all_74_1_47 & op1(all_14_0_5, all_9_0_3) = all_74_2_48 % 4.16/1.71 | % 4.16/1.71 | Applying alpha-rule on (123) yields: % 4.16/1.71 | (124) h(all_74_2_48) = all_74_1_47 % 4.16/1.71 | (125) h(all_9_0_3) = all_74_0_46 % 4.16/1.71 | (126) op2(all_61_0_30, all_74_0_46) = all_74_1_47 % 4.16/1.71 | (127) op1(all_14_0_5, all_9_0_3) = all_74_2_48 % 4.16/1.71 | % 4.16/1.71 | Instantiating (111) with all_76_0_49, all_76_1_50, all_76_2_51 yields: % 4.16/1.71 | (128) h(all_76_2_51) = all_76_1_50 & h(all_14_0_5) = all_76_0_49 & op2(all_61_0_30, all_76_0_49) = all_76_1_50 & op1(all_14_0_5, all_14_0_5) = all_76_2_51 % 4.16/1.71 | % 4.16/1.71 | Applying alpha-rule on (128) yields: % 4.16/1.71 | (129) h(all_76_2_51) = all_76_1_50 % 4.16/1.71 | (130) h(all_14_0_5) = all_76_0_49 % 4.16/1.71 | (131) op2(all_61_0_30, all_76_0_49) = all_76_1_50 % 4.16/1.71 | (132) op1(all_14_0_5, all_14_0_5) = all_76_2_51 % 4.16/1.71 | % 4.16/1.71 | Instantiating formula (8) with all_14_0_5, all_72_0_43, all_0_1_1 and discharging atoms h(all_14_0_5) = all_72_0_43, h(all_14_0_5) = all_0_1_1, yields: % 4.16/1.71 | (133) all_72_0_43 = all_0_1_1 % 4.16/1.71 | % 4.16/1.71 | Instantiating formula (8) with all_14_0_5, all_72_0_43, all_76_0_49 and discharging atoms h(all_14_0_5) = all_76_0_49, h(all_14_0_5) = all_72_0_43, yields: % 4.16/1.71 | (134) all_76_0_49 = all_72_0_43 % 4.16/1.71 | % 4.16/1.71 | Instantiating formula (8) with all_14_0_5, all_61_0_30, all_76_0_49 and discharging atoms h(all_14_0_5) = all_76_0_49, h(all_14_0_5) = all_61_0_30, yields: % 4.16/1.72 | (135) all_76_0_49 = all_61_0_30 % 4.16/1.72 | % 4.16/1.72 | Instantiating formula (8) with all_9_0_3, all_74_0_46, all_0_2_2 and discharging atoms h(all_9_0_3) = all_74_0_46, h(all_9_0_3) = all_0_2_2, yields: % 4.16/1.72 | (136) all_74_0_46 = all_0_2_2 % 4.16/1.72 | % 4.16/1.72 | Instantiating formula (8) with all_9_0_3, all_70_0_40, all_74_0_46 and discharging atoms h(all_9_0_3) = all_74_0_46, h(all_9_0_3) = all_70_0_40, yields: % 4.16/1.72 | (137) all_74_0_46 = all_70_0_40 % 4.16/1.72 | % 4.16/1.72 | Instantiating formula (8) with all_9_0_3, all_58_0_29, all_70_0_40 and discharging atoms h(all_9_0_3) = all_70_0_40, h(all_9_0_3) = all_58_0_29, yields: % 4.16/1.72 | (138) all_70_0_40 = all_58_0_29 % 4.16/1.72 | % 4.16/1.72 | Instantiating formula (2) with all_72_2_45, all_14_0_5, all_9_0_3 and discharging atoms op1(all_9_0_3, all_14_0_5) = all_72_2_45, op1(all_9_0_3, all_9_0_3) = all_14_0_5, sorti1(all_14_0_5), sorti1(all_9_0_3), yields: % 4.16/1.72 | (139) all_72_2_45 = all_9_0_3 % 4.16/1.72 | % 4.16/1.72 | Combining equations (134,135) yields a new equation: % 4.16/1.72 | (140) all_72_0_43 = all_61_0_30 % 4.16/1.72 | % 4.16/1.72 | Simplifying 140 yields: % 4.16/1.72 | (141) all_72_0_43 = all_61_0_30 % 4.16/1.72 | % 4.16/1.72 | Combining equations (137,136) yields a new equation: % 4.16/1.72 | (142) all_70_0_40 = all_0_2_2 % 4.16/1.72 | % 4.16/1.72 | Simplifying 142 yields: % 4.16/1.72 | (143) all_70_0_40 = all_0_2_2 % 4.16/1.72 | % 4.16/1.72 | Combining equations (133,141) yields a new equation: % 4.16/1.72 | (144) all_61_0_30 = all_0_1_1 % 4.16/1.72 | % 4.16/1.72 | Combining equations (143,138) yields a new equation: % 4.16/1.72 | (145) all_58_0_29 = all_0_2_2 % 4.16/1.72 | % 4.16/1.72 | Combining equations (144,141) yields a new equation: % 4.16/1.72 | (133) all_72_0_43 = all_0_1_1 % 4.16/1.72 | % 4.16/1.72 | From (139) and (119) follows: % 4.16/1.72 | (147) h(all_9_0_3) = all_72_1_44 % 4.16/1.72 | % 4.16/1.72 | From (145) and (104) follows: % 4.16/1.72 | (94) h(all_9_0_3) = all_0_2_2 % 4.16/1.72 | % 4.16/1.72 | From (145)(133) and (121) follows: % 4.16/1.72 | (149) op2(all_0_2_2, all_0_1_1) = all_72_1_44 % 4.16/1.72 | % 4.16/1.72 | Instantiating formula (8) with all_9_0_3, all_72_1_44, all_0_2_2 and discharging atoms h(all_9_0_3) = all_72_1_44, h(all_9_0_3) = all_0_2_2, yields: % 4.16/1.72 | (150) all_72_1_44 = all_0_2_2 % 4.16/1.72 | % 4.16/1.72 | Instantiating formula (3) with all_0_2_2, all_0_1_1, all_72_1_44, all_0_0_0 and discharging atoms op2(all_0_2_2, all_0_1_1) = all_72_1_44, op2(all_0_2_2, all_0_1_1) = all_0_0_0, yields: % 4.16/1.72 | (151) all_72_1_44 = all_0_0_0 % 4.16/1.72 | % 4.16/1.72 | Combining equations (150,151) yields a new equation: % 4.16/1.72 | (152) all_0_0_0 = all_0_2_2 % 4.16/1.72 | % 4.16/1.72 | Equations (152) can reduce 12 to: % 4.16/1.72 | (153) $false % 4.16/1.72 | % 4.16/1.72 |-The branch is then unsatisfiable % 4.16/1.72 % SZS output end Proof for theBenchmark % 4.16/1.72 % 4.16/1.72 1143ms %------------------------------------------------------------------------------