%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SYN393+1.003 : TPTP v8.1.0. Released v2.0.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 : Thu Jul 21 05:02:05 EDT 2022 % Result : Theorem 1.46s 0.98s % Output : Proof 2.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SYN393+1.003 : TPTP v8.1.0. Released v2.0.0. % 0.07/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.35 % Computer : n021.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 : Mon Jul 11 21:31:38 EDT 2022 % 0.13/0.35 % CPUTime : % 0.59/0.60 ____ _ % 0.59/0.60 ___ / __ \_____(_)___ ________ __________ % 0.59/0.60 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.59/0.60 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.59/0.60 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.59/0.60 % 0.59/0.60 A Theorem Prover for First-Order Logic % 0.59/0.60 (ePrincess v.1.0) % 0.59/0.60 % 0.59/0.60 (c) Philipp Rümmer, 2009-2015 % 0.59/0.60 (c) Peter Backeman, 2014-2015 % 0.59/0.60 (contributions by Angelo Brillout, Peter Baumgartner) % 0.59/0.60 Free software under GNU Lesser General Public License (LGPL). % 0.59/0.60 Bug reports to peter@backeman.se % 0.59/0.60 % 0.59/0.60 For more information, visit http://user.uu.se/~petba168/breu/ % 0.59/0.60 % 0.59/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.72/0.65 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.14/0.84 Prover 0: Preprocessing ... % 1.41/0.91 Prover 0: Constructing countermodel ... % 1.46/0.97 Prover 0: proved (326ms) % 1.46/0.98 % 1.46/0.98 No countermodel exists, formula is valid % 1.46/0.98 % SZS status Theorem for theBenchmark % 1.46/0.98 % 1.46/0.98 Generating proof ... found it (size 117) % 1.86/1.13 % 1.86/1.13 % SZS output start Proof for theBenchmark % 1.86/1.13 Assumed formulas after preprocessing and simplification: % 1.86/1.13 | (0) (((p3 & ((p2 & p1) | ( ~ p2 & ~ p1))) | ( ~ p3 & ((p2 & ~ p1) | (p1 & ~ p2)))) & ((p1 & ((p3 & ~ p2) | (p2 & ~ p3))) | ( ~ p1 & ((p3 & p2) | ( ~ p3 & ~ p2))))) | (((p3 & ((p2 & ~ p1) | (p1 & ~ p2))) | ( ~ p3 & ((p2 & p1) | ( ~ p2 & ~ p1)))) & ((p1 & ((p3 & p2) | ( ~ p3 & ~ p2))) | ( ~ p1 & ((p3 & ~ p2) | (p2 & ~ p3))))) % 1.86/1.14 +-Applying beta-rule and splitting (0), into two cases. % 1.86/1.14 |-Branch one: % 1.86/1.14 | (1) ((p3 & ((p2 & p1) | ( ~ p2 & ~ p1))) | ( ~ p3 & ((p2 & ~ p1) | (p1 & ~ p2)))) & ((p1 & ((p3 & ~ p2) | (p2 & ~ p3))) | ( ~ p1 & ((p3 & p2) | ( ~ p3 & ~ p2)))) % 1.86/1.14 | % 1.86/1.14 | Applying alpha-rule on (1) yields: % 1.86/1.14 | (2) (p3 & ((p2 & p1) | ( ~ p2 & ~ p1))) | ( ~ p3 & ((p2 & ~ p1) | (p1 & ~ p2))) % 1.86/1.14 | (3) (p1 & ((p3 & ~ p2) | (p2 & ~ p3))) | ( ~ p1 & ((p3 & p2) | ( ~ p3 & ~ p2))) % 1.86/1.15 | % 1.86/1.15 +-Applying beta-rule and splitting (3), into two cases. % 1.86/1.15 |-Branch one: % 1.86/1.15 | (4) p1 & ((p3 & ~ p2) | (p2 & ~ p3)) % 1.86/1.15 | % 1.86/1.15 | Applying alpha-rule on (4) yields: % 1.86/1.15 | (5) p1 % 1.86/1.15 | (6) (p3 & ~ p2) | (p2 & ~ p3) % 1.86/1.15 | % 1.86/1.15 +-Applying beta-rule and splitting (2), into two cases. % 1.86/1.15 |-Branch one: % 1.86/1.15 | (7) p3 & ((p2 & p1) | ( ~ p2 & ~ p1)) % 1.86/1.15 | % 1.86/1.15 | Applying alpha-rule on (7) yields: % 1.86/1.15 | (8) p3 % 1.86/1.15 | (9) (p2 & p1) | ( ~ p2 & ~ p1) % 1.86/1.15 | % 1.86/1.15 +-Applying beta-rule and splitting (6), into two cases. % 1.86/1.15 |-Branch one: % 1.86/1.15 | (10) p3 & ~ p2 % 1.86/1.15 | % 1.86/1.15 | Applying alpha-rule on (10) yields: % 1.86/1.15 | (8) p3 % 1.86/1.15 | (12) ~ p2 % 1.86/1.15 | % 1.86/1.15 +-Applying beta-rule and splitting (9), into two cases. % 1.86/1.15 |-Branch one: % 1.86/1.15 | (13) p2 & p1 % 1.86/1.15 | % 1.86/1.15 | Applying alpha-rule on (13) yields: % 1.86/1.15 | (14) p2 % 1.86/1.15 | (5) p1 % 1.86/1.15 | % 1.86/1.15 | Using (14) and (12) yields: % 1.86/1.15 | (16) $false % 1.86/1.15 | % 1.86/1.15 |-The branch is then unsatisfiable % 1.86/1.15 |-Branch two: % 1.86/1.15 | (17) ~ p2 & ~ p1 % 1.86/1.15 | % 1.86/1.15 | Applying alpha-rule on (17) yields: % 1.86/1.15 | (12) ~ p2 % 1.86/1.15 | (19) ~ p1 % 1.86/1.15 | % 1.86/1.15 | Using (5) and (19) yields: % 1.86/1.15 | (16) $false % 1.86/1.15 | % 1.86/1.15 |-The branch is then unsatisfiable % 1.86/1.15 |-Branch two: % 1.86/1.15 | (21) p2 & ~ p3 % 1.86/1.15 | % 1.86/1.15 | Applying alpha-rule on (21) yields: % 1.86/1.15 | (14) p2 % 1.86/1.15 | (23) ~ p3 % 1.86/1.15 | % 1.86/1.15 | Using (8) and (23) yields: % 1.86/1.15 | (16) $false % 1.86/1.15 | % 1.86/1.15 |-The branch is then unsatisfiable % 1.86/1.15 |-Branch two: % 1.86/1.15 | (25) ~ p3 & ((p2 & ~ p1) | (p1 & ~ p2)) % 1.86/1.15 | % 1.86/1.15 | Applying alpha-rule on (25) yields: % 1.86/1.15 | (23) ~ p3 % 1.86/1.15 | (27) (p2 & ~ p1) | (p1 & ~ p2) % 1.86/1.16 | % 1.86/1.16 +-Applying beta-rule and splitting (6), into two cases. % 1.86/1.16 |-Branch one: % 1.86/1.16 | (10) p3 & ~ p2 % 1.86/1.16 | % 1.86/1.16 | Applying alpha-rule on (10) yields: % 1.86/1.16 | (8) p3 % 1.86/1.16 | (12) ~ p2 % 1.86/1.16 | % 1.86/1.16 | Using (8) and (23) yields: % 1.86/1.16 | (16) $false % 1.86/1.16 | % 1.86/1.16 |-The branch is then unsatisfiable % 1.86/1.16 |-Branch two: % 1.86/1.16 | (21) p2 & ~ p3 % 1.86/1.16 | % 1.86/1.16 | Applying alpha-rule on (21) yields: % 1.86/1.16 | (14) p2 % 1.86/1.16 | (23) ~ p3 % 1.86/1.16 | % 1.86/1.16 +-Applying beta-rule and splitting (27), into two cases. % 1.86/1.16 |-Branch one: % 1.86/1.16 | (35) p2 & ~ p1 % 1.86/1.16 | % 1.86/1.16 | Applying alpha-rule on (35) yields: % 1.86/1.16 | (14) p2 % 1.86/1.16 | (19) ~ p1 % 1.86/1.16 | % 1.86/1.16 | Using (5) and (19) yields: % 1.86/1.16 | (16) $false % 1.86/1.16 | % 1.86/1.16 |-The branch is then unsatisfiable % 1.86/1.16 |-Branch two: % 1.86/1.16 | (39) p1 & ~ p2 % 1.86/1.16 | % 1.86/1.16 | Applying alpha-rule on (39) yields: % 1.86/1.16 | (5) p1 % 1.86/1.16 | (12) ~ p2 % 1.86/1.16 | % 1.86/1.16 | Using (14) and (12) yields: % 1.86/1.16 | (16) $false % 1.86/1.16 | % 1.86/1.16 |-The branch is then unsatisfiable % 1.86/1.16 |-Branch two: % 1.86/1.16 | (43) ~ p1 & ((p3 & p2) | ( ~ p3 & ~ p2)) % 1.86/1.16 | % 1.86/1.16 | Applying alpha-rule on (43) yields: % 1.86/1.16 | (19) ~ p1 % 1.86/1.16 | (45) (p3 & p2) | ( ~ p3 & ~ p2) % 1.86/1.16 | % 1.86/1.16 +-Applying beta-rule and splitting (2), into two cases. % 1.86/1.16 |-Branch one: % 1.86/1.16 | (7) p3 & ((p2 & p1) | ( ~ p2 & ~ p1)) % 1.86/1.16 | % 1.86/1.16 | Applying alpha-rule on (7) yields: % 1.86/1.16 | (8) p3 % 1.86/1.16 | (9) (p2 & p1) | ( ~ p2 & ~ p1) % 1.86/1.16 | % 1.86/1.16 +-Applying beta-rule and splitting (45), into two cases. % 1.86/1.16 |-Branch one: % 1.86/1.16 | (49) p3 & p2 % 1.86/1.16 | % 1.86/1.16 | Applying alpha-rule on (49) yields: % 1.86/1.16 | (8) p3 % 1.86/1.16 | (14) p2 % 1.86/1.16 | % 1.86/1.16 +-Applying beta-rule and splitting (9), into two cases. % 1.86/1.16 |-Branch one: % 1.86/1.16 | (13) p2 & p1 % 1.86/1.16 | % 1.86/1.16 | Applying alpha-rule on (13) yields: % 1.86/1.16 | (14) p2 % 1.86/1.16 | (5) p1 % 1.86/1.16 | % 1.86/1.16 | Using (5) and (19) yields: % 1.86/1.16 | (16) $false % 1.86/1.16 | % 1.86/1.16 |-The branch is then unsatisfiable % 1.86/1.16 |-Branch two: % 1.86/1.16 | (17) ~ p2 & ~ p1 % 1.86/1.16 | % 1.86/1.16 | Applying alpha-rule on (17) yields: % 1.86/1.16 | (12) ~ p2 % 1.86/1.16 | (19) ~ p1 % 1.86/1.16 | % 1.86/1.16 | Using (14) and (12) yields: % 1.86/1.16 | (16) $false % 1.86/1.16 | % 1.86/1.16 |-The branch is then unsatisfiable % 1.86/1.16 |-Branch two: % 1.86/1.16 | (60) ~ p3 & ~ p2 % 1.86/1.16 | % 1.86/1.16 | Applying alpha-rule on (60) yields: % 1.86/1.16 | (23) ~ p3 % 1.86/1.16 | (12) ~ p2 % 1.86/1.16 | % 1.86/1.16 | Using (8) and (23) yields: % 1.86/1.16 | (16) $false % 1.86/1.16 | % 1.86/1.16 |-The branch is then unsatisfiable % 1.86/1.16 |-Branch two: % 1.86/1.16 | (25) ~ p3 & ((p2 & ~ p1) | (p1 & ~ p2)) % 1.86/1.16 | % 1.86/1.16 | Applying alpha-rule on (25) yields: % 1.86/1.16 | (23) ~ p3 % 1.86/1.17 | (27) (p2 & ~ p1) | (p1 & ~ p2) % 1.86/1.17 | % 1.86/1.17 +-Applying beta-rule and splitting (45), into two cases. % 1.86/1.17 |-Branch one: % 1.86/1.17 | (49) p3 & p2 % 1.86/1.17 | % 1.86/1.17 | Applying alpha-rule on (49) yields: % 1.86/1.17 | (8) p3 % 1.86/1.17 | (14) p2 % 1.86/1.17 | % 1.86/1.17 | Using (8) and (23) yields: % 1.86/1.17 | (16) $false % 1.86/1.17 | % 1.86/1.17 |-The branch is then unsatisfiable % 1.86/1.17 |-Branch two: % 1.86/1.17 | (60) ~ p3 & ~ p2 % 1.86/1.17 | % 1.86/1.17 | Applying alpha-rule on (60) yields: % 1.86/1.17 | (23) ~ p3 % 1.86/1.17 | (12) ~ p2 % 1.86/1.17 | % 1.86/1.17 +-Applying beta-rule and splitting (27), into two cases. % 1.86/1.17 |-Branch one: % 1.86/1.17 | (35) p2 & ~ p1 % 1.86/1.17 | % 1.86/1.17 | Applying alpha-rule on (35) yields: % 1.86/1.17 | (14) p2 % 1.86/1.17 | (19) ~ p1 % 1.86/1.17 | % 1.86/1.17 | Using (14) and (12) yields: % 1.86/1.17 | (16) $false % 1.86/1.17 | % 1.86/1.17 |-The branch is then unsatisfiable % 1.86/1.17 |-Branch two: % 1.86/1.17 | (39) p1 & ~ p2 % 1.86/1.17 | % 1.86/1.17 | Applying alpha-rule on (39) yields: % 1.86/1.17 | (5) p1 % 1.86/1.17 | (12) ~ p2 % 1.86/1.17 | % 1.86/1.17 | Using (5) and (19) yields: % 1.86/1.17 | (16) $false % 1.86/1.17 | % 1.86/1.17 |-The branch is then unsatisfiable % 1.86/1.17 |-Branch two: % 1.86/1.17 | (82) ((p3 & ((p2 & ~ p1) | (p1 & ~ p2))) | ( ~ p3 & ((p2 & p1) | ( ~ p2 & ~ p1)))) & ((p1 & ((p3 & p2) | ( ~ p3 & ~ p2))) | ( ~ p1 & ((p3 & ~ p2) | (p2 & ~ p3)))) % 1.86/1.17 | % 1.86/1.17 | Applying alpha-rule on (82) yields: % 1.86/1.17 | (83) (p3 & ((p2 & ~ p1) | (p1 & ~ p2))) | ( ~ p3 & ((p2 & p1) | ( ~ p2 & ~ p1))) % 1.86/1.17 | (84) (p1 & ((p3 & p2) | ( ~ p3 & ~ p2))) | ( ~ p1 & ((p3 & ~ p2) | (p2 & ~ p3))) % 1.86/1.17 | % 1.86/1.17 +-Applying beta-rule and splitting (84), into two cases. % 1.86/1.17 |-Branch one: % 1.86/1.17 | (85) p1 & ((p3 & p2) | ( ~ p3 & ~ p2)) % 1.86/1.17 | % 1.86/1.17 | Applying alpha-rule on (85) yields: % 1.86/1.17 | (5) p1 % 1.86/1.17 | (45) (p3 & p2) | ( ~ p3 & ~ p2) % 1.86/1.17 | % 1.86/1.17 +-Applying beta-rule and splitting (83), into two cases. % 1.86/1.17 |-Branch one: % 1.86/1.17 | (88) p3 & ((p2 & ~ p1) | (p1 & ~ p2)) % 1.86/1.17 | % 1.86/1.17 | Applying alpha-rule on (88) yields: % 1.86/1.17 | (8) p3 % 1.86/1.17 | (27) (p2 & ~ p1) | (p1 & ~ p2) % 1.86/1.17 | % 1.86/1.17 +-Applying beta-rule and splitting (45), into two cases. % 1.86/1.17 |-Branch one: % 1.86/1.17 | (49) p3 & p2 % 1.86/1.17 | % 1.86/1.17 | Applying alpha-rule on (49) yields: % 1.86/1.17 | (8) p3 % 1.86/1.17 | (14) p2 % 1.86/1.17 | % 1.86/1.17 +-Applying beta-rule and splitting (27), into two cases. % 1.86/1.17 |-Branch one: % 1.86/1.17 | (35) p2 & ~ p1 % 1.86/1.17 | % 1.86/1.17 | Applying alpha-rule on (35) yields: % 1.86/1.17 | (14) p2 % 1.86/1.17 | (19) ~ p1 % 1.86/1.17 | % 1.86/1.17 | Using (5) and (19) yields: % 1.86/1.17 | (16) $false % 1.86/1.17 | % 1.86/1.17 |-The branch is then unsatisfiable % 1.86/1.17 |-Branch two: % 1.86/1.17 | (39) p1 & ~ p2 % 1.86/1.17 | % 1.86/1.17 | Applying alpha-rule on (39) yields: % 1.86/1.17 | (5) p1 % 1.86/1.17 | (12) ~ p2 % 1.86/1.17 | % 1.86/1.17 | Using (14) and (12) yields: % 1.86/1.17 | (16) $false % 1.86/1.17 | % 1.86/1.17 |-The branch is then unsatisfiable % 1.86/1.17 |-Branch two: % 1.86/1.17 | (60) ~ p3 & ~ p2 % 1.86/1.17 | % 1.86/1.17 | Applying alpha-rule on (60) yields: % 1.86/1.17 | (23) ~ p3 % 1.86/1.17 | (12) ~ p2 % 1.86/1.17 | % 1.86/1.17 | Using (8) and (23) yields: % 1.86/1.17 | (16) $false % 1.86/1.17 | % 1.86/1.17 |-The branch is then unsatisfiable % 1.86/1.17 |-Branch two: % 1.86/1.17 | (106) ~ p3 & ((p2 & p1) | ( ~ p2 & ~ p1)) % 1.86/1.17 | % 1.86/1.17 | Applying alpha-rule on (106) yields: % 1.86/1.17 | (23) ~ p3 % 1.86/1.17 | (9) (p2 & p1) | ( ~ p2 & ~ p1) % 1.86/1.17 | % 1.86/1.17 +-Applying beta-rule and splitting (45), into two cases. % 1.86/1.17 |-Branch one: % 1.86/1.17 | (49) p3 & p2 % 1.86/1.17 | % 1.86/1.17 | Applying alpha-rule on (49) yields: % 1.86/1.17 | (8) p3 % 1.86/1.17 | (14) p2 % 1.86/1.17 | % 1.86/1.17 | Using (8) and (23) yields: % 1.86/1.17 | (16) $false % 1.86/1.17 | % 1.86/1.17 |-The branch is then unsatisfiable % 1.86/1.17 |-Branch two: % 1.86/1.18 | (60) ~ p3 & ~ p2 % 1.86/1.18 | % 1.86/1.18 | Applying alpha-rule on (60) yields: % 1.86/1.18 | (23) ~ p3 % 1.86/1.18 | (12) ~ p2 % 1.86/1.18 | % 1.86/1.18 +-Applying beta-rule and splitting (9), into two cases. % 1.86/1.18 |-Branch one: % 1.86/1.18 | (13) p2 & p1 % 1.86/1.18 | % 1.86/1.18 | Applying alpha-rule on (13) yields: % 1.86/1.18 | (14) p2 % 1.86/1.18 | (5) p1 % 1.86/1.18 | % 1.86/1.18 | Using (14) and (12) yields: % 1.86/1.18 | (16) $false % 1.86/1.18 | % 1.86/1.18 |-The branch is then unsatisfiable % 1.86/1.18 |-Branch two: % 1.86/1.18 | (17) ~ p2 & ~ p1 % 1.86/1.18 | % 1.86/1.18 | Applying alpha-rule on (17) yields: % 1.86/1.18 | (12) ~ p2 % 1.86/1.18 | (19) ~ p1 % 1.86/1.18 | % 1.86/1.18 | Using (5) and (19) yields: % 1.86/1.18 | (16) $false % 1.86/1.18 | % 1.86/1.18 |-The branch is then unsatisfiable % 1.86/1.18 |-Branch two: % 1.86/1.18 | (124) ~ p1 & ((p3 & ~ p2) | (p2 & ~ p3)) % 1.86/1.18 | % 1.86/1.18 | Applying alpha-rule on (124) yields: % 1.86/1.18 | (19) ~ p1 % 1.86/1.18 | (6) (p3 & ~ p2) | (p2 & ~ p3) % 1.86/1.18 | % 1.86/1.18 +-Applying beta-rule and splitting (83), into two cases. % 1.86/1.18 |-Branch one: % 1.86/1.18 | (88) p3 & ((p2 & ~ p1) | (p1 & ~ p2)) % 1.86/1.18 | % 1.86/1.18 | Applying alpha-rule on (88) yields: % 1.86/1.18 | (8) p3 % 1.86/1.18 | (27) (p2 & ~ p1) | (p1 & ~ p2) % 1.86/1.18 | % 1.86/1.18 +-Applying beta-rule and splitting (6), into two cases. % 1.86/1.18 |-Branch one: % 1.86/1.18 | (10) p3 & ~ p2 % 1.86/1.18 | % 1.86/1.18 | Applying alpha-rule on (10) yields: % 1.86/1.18 | (8) p3 % 1.86/1.18 | (12) ~ p2 % 1.86/1.18 | % 2.12/1.18 +-Applying beta-rule and splitting (27), into two cases. % 2.12/1.18 |-Branch one: % 2.12/1.18 | (35) p2 & ~ p1 % 2.12/1.18 | % 2.12/1.18 | Applying alpha-rule on (35) yields: % 2.12/1.18 | (14) p2 % 2.12/1.18 | (19) ~ p1 % 2.12/1.18 | % 2.12/1.18 | Using (14) and (12) yields: % 2.12/1.18 | (16) $false % 2.12/1.18 | % 2.12/1.18 |-The branch is then unsatisfiable % 2.12/1.18 |-Branch two: % 2.12/1.18 | (39) p1 & ~ p2 % 2.12/1.18 | % 2.12/1.18 | Applying alpha-rule on (39) yields: % 2.12/1.18 | (5) p1 % 2.12/1.18 | (12) ~ p2 % 2.12/1.18 | % 2.12/1.18 | Using (5) and (19) yields: % 2.12/1.18 | (16) $false % 2.12/1.18 | % 2.12/1.18 |-The branch is then unsatisfiable % 2.12/1.18 |-Branch two: % 2.12/1.18 | (21) p2 & ~ p3 % 2.12/1.18 | % 2.12/1.18 | Applying alpha-rule on (21) yields: % 2.12/1.18 | (14) p2 % 2.12/1.18 | (23) ~ p3 % 2.12/1.18 | % 2.12/1.18 | Using (8) and (23) yields: % 2.12/1.18 | (16) $false % 2.12/1.18 | % 2.12/1.18 |-The branch is then unsatisfiable % 2.12/1.18 |-Branch two: % 2.12/1.18 | (106) ~ p3 & ((p2 & p1) | ( ~ p2 & ~ p1)) % 2.12/1.18 | % 2.12/1.18 | Applying alpha-rule on (106) yields: % 2.12/1.18 | (23) ~ p3 % 2.12/1.18 | (9) (p2 & p1) | ( ~ p2 & ~ p1) % 2.12/1.18 | % 2.12/1.18 +-Applying beta-rule and splitting (6), into two cases. % 2.12/1.18 |-Branch one: % 2.12/1.18 | (10) p3 & ~ p2 % 2.12/1.18 | % 2.12/1.18 | Applying alpha-rule on (10) yields: % 2.12/1.18 | (8) p3 % 2.12/1.18 | (12) ~ p2 % 2.12/1.18 | % 2.12/1.18 | Using (8) and (23) yields: % 2.12/1.18 | (16) $false % 2.12/1.18 | % 2.12/1.18 |-The branch is then unsatisfiable % 2.12/1.18 |-Branch two: % 2.12/1.18 | (21) p2 & ~ p3 % 2.12/1.18 | % 2.12/1.18 | Applying alpha-rule on (21) yields: % 2.12/1.18 | (14) p2 % 2.12/1.18 | (23) ~ p3 % 2.12/1.18 | % 2.12/1.18 +-Applying beta-rule and splitting (9), into two cases. % 2.12/1.18 |-Branch one: % 2.12/1.18 | (13) p2 & p1 % 2.12/1.18 | % 2.12/1.18 | Applying alpha-rule on (13) yields: % 2.12/1.18 | (14) p2 % 2.12/1.18 | (5) p1 % 2.12/1.18 | % 2.12/1.18 | Using (5) and (19) yields: % 2.12/1.18 | (16) $false % 2.12/1.18 | % 2.12/1.18 |-The branch is then unsatisfiable % 2.12/1.18 |-Branch two: % 2.12/1.18 | (17) ~ p2 & ~ p1 % 2.12/1.18 | % 2.12/1.18 | Applying alpha-rule on (17) yields: % 2.12/1.18 | (12) ~ p2 % 2.12/1.18 | (19) ~ p1 % 2.12/1.18 | % 2.12/1.18 | Using (14) and (12) yields: % 2.12/1.18 | (16) $false % 2.12/1.18 | % 2.12/1.18 |-The branch is then unsatisfiable % 2.12/1.18 % SZS output end Proof for theBenchmark % 2.12/1.18 % 2.12/1.18 573ms %------------------------------------------------------------------------------