%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : KRS090+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n032.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 19.06s 6.15s % Output : Proof 20.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.09 % Problem : KRS090+1 : TPTP v8.1.0. Released v3.1.0. % 0.06/0.10 % Command : ePrincess-casc -timeout=%d %s % 0.09/0.29 % Computer : n032.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 600 % 0.09/0.29 % DateTime : Tue Jun 7 07:48:35 EDT 2022 % 0.09/0.29 % CPUTime : % 0.14/0.49 ____ _ % 0.14/0.49 ___ / __ \_____(_)___ ________ __________ % 0.14/0.49 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.14/0.49 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.14/0.49 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.14/0.49 % 0.14/0.49 A Theorem Prover for First-Order Logic % 0.14/0.49 (ePrincess v.1.0) % 0.14/0.49 % 0.14/0.49 (c) Philipp Rümmer, 2009-2015 % 0.14/0.49 (c) Peter Backeman, 2014-2015 % 0.14/0.49 (contributions by Angelo Brillout, Peter Baumgartner) % 0.14/0.49 Free software under GNU Lesser General Public License (LGPL). % 0.14/0.49 Bug reports to peter@backeman.se % 0.14/0.49 % 0.14/0.49 For more information, visit http://user.uu.se/~petba168/breu/ % 0.14/0.49 % 0.14/0.50 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.60/0.54 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.23/0.80 Prover 0: Preprocessing ... % 1.60/0.96 Prover 0: Warning: ignoring some quantifiers % 1.60/0.98 Prover 0: Constructing countermodel ... % 17.85/5.83 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 18.06/5.88 Prover 1: Preprocessing ... % 19.06/6.10 Prover 1: Constructing countermodel ... % 19.06/6.14 Prover 1: proved (309ms) % 19.06/6.14 Prover 0: stopped % 19.06/6.15 % 19.06/6.15 No countermodel exists, formula is valid % 19.06/6.15 % SZS status Unsatisfiable for theBenchmark % 19.06/6.15 % 19.06/6.15 Generating proof ... found it (size 16) % 20.19/6.36 % 20.19/6.36 % SZS output start Proof for theBenchmark % 20.19/6.36 Assumed formulas after preprocessing and simplification: % 20.19/6.36 | (0) cTEST(i2003_11_14_17_19_57994) = 0 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (rR(v3, v2) = v1) | ~ (rR(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cTEST(v2) = v1) | ~ (cTEST(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC5(v2) = v1) | ~ (cC5(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC4(v2) = v1) | ~ (cC4(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC3(v2) = v1) | ~ (cC3(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC2(v2) = v1) | ~ (cC2(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB(v2) = v1) | ~ (cB(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA(v2) = v1) | ~ (cA(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB9(v2) = v1) | ~ (cB9(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC1(v2) = v1) | ~ (cC1(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB5(v2) = v1) | ~ (cB5(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA5(v2) = v1) | ~ (cA5(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB13(v2) = v1) | ~ (cB13(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA13(v2) = v1) | ~ (cA13(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA1(v2) = v1) | ~ (cA1(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB1(v2) = v1) | ~ (cB1(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA27(v2) = v1) | ~ (cA27(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB27(v2) = v1) | ~ (cB27(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA4(v2) = v1) | ~ (cA4(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB4(v2) = v1) | ~ (cB4(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB12(v2) = v1) | ~ (cB12(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA12(v2) = v1) | ~ (cA12(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB30(v2) = v1) | ~ (cB30(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA30(v2) = v1) | ~ (cA30(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA20(v2) = v1) | ~ (cA20(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB20(v2) = v1) | ~ (cB20(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB14(v2) = v1) | ~ (cB14(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA14(v2) = v1) | ~ (cA14(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB28(v2) = v1) | ~ (cB28(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA28(v2) = v1) | ~ (cA28(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA3(v2) = v1) | ~ (cA3(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB3(v2) = v1) | ~ (cB3(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB7(v2) = v1) | ~ (cB7(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA7(v2) = v1) | ~ (cA7(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB21(v2) = v1) | ~ (cB21(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA21(v2) = v1) | ~ (cA21(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB22(v2) = v1) | ~ (cB22(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA22(v2) = v1) | ~ (cA22(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB17(v2) = v1) | ~ (cB17(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA17(v2) = v1) | ~ (cA17(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB11(v2) = v1) | ~ (cB11(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA11(v2) = v1) | ~ (cA11(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB19(v2) = v1) | ~ (cB19(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA19(v2) = v1) | ~ (cA19(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA8(v2) = v1) | ~ (cA8(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB8(v2) = v1) | ~ (cB8(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA26(v2) = v1) | ~ (cA26(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB26(v2) = v1) | ~ (cB26(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA25(v2) = v1) | ~ (cA25(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB25(v2) = v1) | ~ (cB25(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA29(v2) = v1) | ~ (cA29(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB29(v2) = v1) | ~ (cB29(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB23(v2) = v1) | ~ (cB23(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA23(v2) = v1) | ~ (cA23(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB18(v2) = v1) | ~ (cB18(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA18(v2) = v1) | ~ (cA18(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB10(v2) = v1) | ~ (cB10(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA10(v2) = v1) | ~ (cA10(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB2(v2) = v1) | ~ (cB2(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA2(v2) = v1) | ~ (cA2(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA16(v2) = v1) | ~ (cA16(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB16(v2) = v1) | ~ (cB16(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB0(v2) = v1) | ~ (cB0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA0(v2) = v1) | ~ (cA0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB31(v2) = v1) | ~ (cB31(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA31(v2) = v1) | ~ (cA31(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA9(v2) = v1) | ~ (cA9(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB6(v2) = v1) | ~ (cB6(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA6(v2) = v1) | ~ (cA6(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB24(v2) = v1) | ~ (cB24(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA24(v2) = v1) | ~ (cA24(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB15(v2) = v1) | ~ (cB15(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA15(v2) = v1) | ~ (cA15(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (xsd_string(v2) = v1) | ~ (xsd_string(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (xsd_integer(v2) = v1) | ~ (xsd_integer(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cowlNothing(v2) = v1) | ~ (cowlNothing(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cowlThing(v2) = v1) | ~ (cowlThing(v2) = v0)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (xsd_string(v0) = v1) | xsd_integer(v0) = 0) & ! [v0] : ! [v1] : (v1 = 0 | ~ (cowlThing(v0) = v1)) & ! [v0] : ! [v1] : ( ~ (cC5(v0) = 0) | ~ (rR(v0, v1) = 0) | cC3(v1) = 0) & ! [v0] : ! [v1] : ( ~ (cB9(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ? [v19] : ? [v20] : ? [v21] : ? [v22] : ? [v23] : ? [v24] : ? [v25] : ? [v26] : ? [v27] : ? [v28] : ? [v29] : ? [v30] : ? [v31] : ? [v32] : ? [v33] : ? [v34] : ? [v35] : ? [v36] : ? [v37] : ? [v38] : ? [v39] : ? [v40] : ? [v41] : ? [v42] : ? [v43] : ? [v44] : ? [v45] : ? [v46] : ? [v47] : ? [v48] : ? [v49] : ? [v50] : ? [v51] : ? [v52] : ? [v53] : ? [v54] : ? [v55] : ? [v56] : ? [v57] : ? [v58] : ? [v59] : ? [v60] : ? [v61] : ? [v62] : ? [v63] : ? [v64] : ? [v65] : (cC1(v0) = v2 & cB5(v0) = v3 & cA5(v0) = v4 & cB13(v0) = v5 & cA13(v0) = v6 & cA1(v0) = v7 & cB1(v0) = v8 & cA27(v0) = v9 & cB27(v0) = v10 & cA4(v0) = v11 & cB4(v0) = v12 & cB12(v0) = v13 & cA12(v0) = v14 & cB30(v0) = v15 & cA30(v0) = v16 & cA20(v0) = v17 & cB20(v0) = v18 & cB14(v0) = v19 & cA14(v0) = v20 & cB28(v0) = v21 & cA28(v0) = v22 & cA3(v0) = v23 & cB3(v0) = v24 & cB7(v0) = v25 & cA7(v0) = v26 & cB21(v0) = v27 & cA21(v0) = v28 & cB22(v0) = v29 & cA22(v0) = v30 & cB17(v0) = v31 & cA17(v0) = v32 & cB11(v0) = v33 & cA11(v0) = v34 & cB19(v0) = v35 & cA19(v0) = v36 & cA8(v0) = v37 & cB8(v0) = v38 & cA26(v0) = v39 & cB26(v0) = v40 & cA25(v0) = v41 & cB25(v0) = v42 & cA29(v0) = v43 & cB29(v0) = v44 & cB23(v0) = v45 & cA23(v0) = v46 & cB18(v0) = v47 & cA18(v0) = v48 & cB10(v0) = v49 & cA10(v0) = v50 & cB2(v0) = v51 & cA2(v0) = v52 & cA16(v0) = v53 & cB16(v0) = v54 & cB0(v0) = v55 & cA0(v0) = v56 & cB31(v0) = v57 & cA31(v0) = v58 & cA9(v0) = v59 & cB6(v0) = v60 & cA6(v0) = v61 & cB24(v0) = v62 & cA24(v0) = v63 & cB15(v0) = v64 & cA15(v0) = v65 & ( ~ (v2 = 0) | ((v65 = 0 | v64 = 0) & (v63 = 0 | v62 = 0) & (v61 = 0 | v60 = 0) & (v59 = 0 | v1 = 0) & (v58 = 0 | v57 = 0) & (v56 = 0 | v55 = 0) & (v54 = 0 | v53 = 0) & (v52 = 0 | v51 = 0) & (v50 = 0 | v49 = 0) & (v48 = 0 | v47 = 0) & (v46 = 0 | v45 = 0) & (v44 = 0 | v43 = 0) & (v42 = 0 | v41 = 0) & (v40 = 0 | v39 = 0) & (v38 = 0 | v37 = 0) & (v36 = 0 | v35 = 0) & (v34 = 0 | v33 = 0) & (v32 = 0 | v31 = 0) & (v30 = 0 | v29 = 0) & (v28 = 0 | v27 = 0) & (v26 = 0 | v25 = 0) & (v24 = 0 | v23 = 0) & (v22 = 0 | v21 = 0) & (v20 = 0 | v19 = 0) & (v18 = 0 | v17 = 0) & (v16 = 0 | v15 = 0) & (v14 = 0 | v13 = 0) & (v12 = 0 | v11 = 0) & (v10 = 0 | v9 = 0) & (v8 = 0 | v7 = 0) & (v6 = 0 | v5 = 0) & (v4 = 0 | v3 = 0))))) & ! [v0] : ( ~ (cTEST(v0) = 0) | (cC5(v0) = 0 & cC4(v0) = 0 & cC1(v0) = 0)) & ! [v0] : ( ~ (cC4(v0) = 0) | ? [v1] : (rR(v0, v1) = 0 & cC2(v1) = 0)) & ! [v0] : ( ~ (cC3(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cB(v0) = v1 & cA(v0) = v2)) & ! [v0] : ( ~ (cC2(v0) = 0) | ? [v1] : (cB(v0) = v1 & cA(v0) = 0)) & ! [v0] : ( ~ (xsd_string(v0) = 0) | ? [v1] : ( ~ (v1 = 0) & xsd_integer(v0) = v1)) & ! [v0] : ~ (cowlNothing(v0) = 0) % 20.52/6.41 | Applying alpha-rule on (0) yields: % 20.52/6.41 | (1) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA27(v2) = v1) | ~ (cA27(v2) = v0)) % 20.52/6.41 | (2) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB9(v2) = v1) | ~ (cB9(v2) = v0)) % 20.52/6.41 | (3) ! [v0] : ~ (cowlNothing(v0) = 0) % 20.52/6.41 | (4) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA21(v2) = v1) | ~ (cA21(v2) = v0)) % 20.52/6.41 | (5) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA8(v2) = v1) | ~ (cA8(v2) = v0)) % 20.52/6.41 | (6) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB28(v2) = v1) | ~ (cB28(v2) = v0)) % 20.52/6.41 | (7) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA23(v2) = v1) | ~ (cA23(v2) = v0)) % 20.52/6.41 | (8) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA13(v2) = v1) | ~ (cA13(v2) = v0)) % 20.52/6.41 | (9) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA19(v2) = v1) | ~ (cA19(v2) = v0)) % 20.52/6.41 | (10) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cowlNothing(v2) = v1) | ~ (cowlNothing(v2) = v0)) % 20.52/6.41 | (11) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB17(v2) = v1) | ~ (cB17(v2) = v0)) % 20.52/6.41 | (12) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA1(v2) = v1) | ~ (cA1(v2) = v0)) % 20.52/6.41 | (13) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC5(v2) = v1) | ~ (cC5(v2) = v0)) % 20.52/6.41 | (14) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (rR(v3, v2) = v1) | ~ (rR(v3, v2) = v0)) % 20.52/6.41 | (15) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA17(v2) = v1) | ~ (cA17(v2) = v0)) % 20.52/6.41 | (16) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB25(v2) = v1) | ~ (cB25(v2) = v0)) % 20.52/6.41 | (17) ! [v0] : ( ~ (cC2(v0) = 0) | ? [v1] : (cB(v0) = v1 & cA(v0) = 0)) % 20.52/6.41 | (18) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB23(v2) = v1) | ~ (cB23(v2) = v0)) % 20.52/6.41 | (19) ! [v0] : ! [v1] : (v1 = 0 | ~ (xsd_string(v0) = v1) | xsd_integer(v0) = 0) % 20.52/6.41 | (20) ! [v0] : ( ~ (cC4(v0) = 0) | ? [v1] : (rR(v0, v1) = 0 & cC2(v1) = 0)) % 20.52/6.42 | (21) ! [v0] : ( ~ (cTEST(v0) = 0) | (cC5(v0) = 0 & cC4(v0) = 0 & cC1(v0) = 0)) % 20.52/6.42 | (22) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA15(v2) = v1) | ~ (cA15(v2) = v0)) % 20.52/6.42 | (23) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB15(v2) = v1) | ~ (cB15(v2) = v0)) % 20.52/6.42 | (24) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA20(v2) = v1) | ~ (cA20(v2) = v0)) % 20.52/6.42 | (25) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA10(v2) = v1) | ~ (cA10(v2) = v0)) % 20.52/6.42 | (26) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA14(v2) = v1) | ~ (cA14(v2) = v0)) % 20.52/6.42 | (27) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA11(v2) = v1) | ~ (cA11(v2) = v0)) % 20.52/6.42 | (28) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB13(v2) = v1) | ~ (cB13(v2) = v0)) % 20.52/6.42 | (29) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA7(v2) = v1) | ~ (cA7(v2) = v0)) % 20.52/6.42 | (30) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB21(v2) = v1) | ~ (cB21(v2) = v0)) % 20.52/6.42 | (31) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA5(v2) = v1) | ~ (cA5(v2) = v0)) % 20.52/6.42 | (32) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC3(v2) = v1) | ~ (cC3(v2) = v0)) % 20.52/6.42 | (33) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB14(v2) = v1) | ~ (cB14(v2) = v0)) % 20.52/6.42 | (34) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA24(v2) = v1) | ~ (cA24(v2) = v0)) % 20.52/6.42 | (35) ! [v0] : ! [v1] : ( ~ (cC5(v0) = 0) | ~ (rR(v0, v1) = 0) | cC3(v1) = 0) % 20.52/6.42 | (36) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cTEST(v2) = v1) | ~ (cTEST(v2) = v0)) % 20.52/6.42 | (37) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB2(v2) = v1) | ~ (cB2(v2) = v0)) % 20.52/6.42 | (38) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA29(v2) = v1) | ~ (cA29(v2) = v0)) % 20.52/6.42 | (39) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB8(v2) = v1) | ~ (cB8(v2) = v0)) % 20.52/6.42 | (40) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA31(v2) = v1) | ~ (cA31(v2) = v0)) % 20.52/6.42 | (41) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB30(v2) = v1) | ~ (cB30(v2) = v0)) % 20.52/6.42 | (42) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (xsd_integer(v2) = v1) | ~ (xsd_integer(v2) = v0)) % 20.52/6.42 | (43) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB24(v2) = v1) | ~ (cB24(v2) = v0)) % 20.52/6.42 | (44) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (xsd_string(v2) = v1) | ~ (xsd_string(v2) = v0)) % 20.52/6.42 | (45) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC2(v2) = v1) | ~ (cC2(v2) = v0)) % 20.52/6.42 | (46) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB31(v2) = v1) | ~ (cB31(v2) = v0)) % 20.52/6.42 | (47) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA18(v2) = v1) | ~ (cA18(v2) = v0)) % 20.52/6.42 | (48) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA30(v2) = v1) | ~ (cA30(v2) = v0)) % 20.52/6.42 | (49) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA26(v2) = v1) | ~ (cA26(v2) = v0)) % 20.52/6.42 | (50) cTEST(i2003_11_14_17_19_57994) = 0 % 20.52/6.42 | (51) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA12(v2) = v1) | ~ (cA12(v2) = v0)) % 20.52/6.42 | (52) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB26(v2) = v1) | ~ (cB26(v2) = v0)) % 20.52/6.42 | (53) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cowlThing(v2) = v1) | ~ (cowlThing(v2) = v0)) % 20.52/6.42 | (54) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC4(v2) = v1) | ~ (cC4(v2) = v0)) % 20.52/6.42 | (55) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB18(v2) = v1) | ~ (cB18(v2) = v0)) % 20.52/6.42 | (56) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB12(v2) = v1) | ~ (cB12(v2) = v0)) % 20.52/6.42 | (57) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA25(v2) = v1) | ~ (cA25(v2) = v0)) % 20.52/6.42 | (58) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB19(v2) = v1) | ~ (cB19(v2) = v0)) % 20.52/6.42 | (59) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB27(v2) = v1) | ~ (cB27(v2) = v0)) % 20.52/6.42 | (60) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB1(v2) = v1) | ~ (cB1(v2) = v0)) % 20.52/6.42 | (61) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB16(v2) = v1) | ~ (cB16(v2) = v0)) % 20.52/6.42 | (62) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB3(v2) = v1) | ~ (cB3(v2) = v0)) % 20.52/6.42 | (63) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA22(v2) = v1) | ~ (cA22(v2) = v0)) % 20.52/6.42 | (64) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA(v2) = v1) | ~ (cA(v2) = v0)) % 20.52/6.43 | (65) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cC1(v2) = v1) | ~ (cC1(v2) = v0)) % 20.52/6.43 | (66) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB4(v2) = v1) | ~ (cB4(v2) = v0)) % 20.52/6.43 | (67) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA28(v2) = v1) | ~ (cA28(v2) = v0)) % 20.52/6.43 | (68) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB22(v2) = v1) | ~ (cB22(v2) = v0)) % 20.52/6.43 | (69) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB7(v2) = v1) | ~ (cB7(v2) = v0)) % 20.52/6.43 | (70) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB(v2) = v1) | ~ (cB(v2) = v0)) % 20.52/6.43 | (71) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA9(v2) = v1) | ~ (cA9(v2) = v0)) % 20.52/6.43 | (72) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB6(v2) = v1) | ~ (cB6(v2) = v0)) % 20.52/6.43 | (73) ! [v0] : ! [v1] : ( ~ (cB9(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ? [v19] : ? [v20] : ? [v21] : ? [v22] : ? [v23] : ? [v24] : ? [v25] : ? [v26] : ? [v27] : ? [v28] : ? [v29] : ? [v30] : ? [v31] : ? [v32] : ? [v33] : ? [v34] : ? [v35] : ? [v36] : ? [v37] : ? [v38] : ? [v39] : ? [v40] : ? [v41] : ? [v42] : ? [v43] : ? [v44] : ? [v45] : ? [v46] : ? [v47] : ? [v48] : ? [v49] : ? [v50] : ? [v51] : ? [v52] : ? [v53] : ? [v54] : ? [v55] : ? [v56] : ? [v57] : ? [v58] : ? [v59] : ? [v60] : ? [v61] : ? [v62] : ? [v63] : ? [v64] : ? [v65] : (cC1(v0) = v2 & cB5(v0) = v3 & cA5(v0) = v4 & cB13(v0) = v5 & cA13(v0) = v6 & cA1(v0) = v7 & cB1(v0) = v8 & cA27(v0) = v9 & cB27(v0) = v10 & cA4(v0) = v11 & cB4(v0) = v12 & cB12(v0) = v13 & cA12(v0) = v14 & cB30(v0) = v15 & cA30(v0) = v16 & cA20(v0) = v17 & cB20(v0) = v18 & cB14(v0) = v19 & cA14(v0) = v20 & cB28(v0) = v21 & cA28(v0) = v22 & cA3(v0) = v23 & cB3(v0) = v24 & cB7(v0) = v25 & cA7(v0) = v26 & cB21(v0) = v27 & cA21(v0) = v28 & cB22(v0) = v29 & cA22(v0) = v30 & cB17(v0) = v31 & cA17(v0) = v32 & cB11(v0) = v33 & cA11(v0) = v34 & cB19(v0) = v35 & cA19(v0) = v36 & cA8(v0) = v37 & cB8(v0) = v38 & cA26(v0) = v39 & cB26(v0) = v40 & cA25(v0) = v41 & cB25(v0) = v42 & cA29(v0) = v43 & cB29(v0) = v44 & cB23(v0) = v45 & cA23(v0) = v46 & cB18(v0) = v47 & cA18(v0) = v48 & cB10(v0) = v49 & cA10(v0) = v50 & cB2(v0) = v51 & cA2(v0) = v52 & cA16(v0) = v53 & cB16(v0) = v54 & cB0(v0) = v55 & cA0(v0) = v56 & cB31(v0) = v57 & cA31(v0) = v58 & cA9(v0) = v59 & cB6(v0) = v60 & cA6(v0) = v61 & cB24(v0) = v62 & cA24(v0) = v63 & cB15(v0) = v64 & cA15(v0) = v65 & ( ~ (v2 = 0) | ((v65 = 0 | v64 = 0) & (v63 = 0 | v62 = 0) & (v61 = 0 | v60 = 0) & (v59 = 0 | v1 = 0) & (v58 = 0 | v57 = 0) & (v56 = 0 | v55 = 0) & (v54 = 0 | v53 = 0) & (v52 = 0 | v51 = 0) & (v50 = 0 | v49 = 0) & (v48 = 0 | v47 = 0) & (v46 = 0 | v45 = 0) & (v44 = 0 | v43 = 0) & (v42 = 0 | v41 = 0) & (v40 = 0 | v39 = 0) & (v38 = 0 | v37 = 0) & (v36 = 0 | v35 = 0) & (v34 = 0 | v33 = 0) & (v32 = 0 | v31 = 0) & (v30 = 0 | v29 = 0) & (v28 = 0 | v27 = 0) & (v26 = 0 | v25 = 0) & (v24 = 0 | v23 = 0) & (v22 = 0 | v21 = 0) & (v20 = 0 | v19 = 0) & (v18 = 0 | v17 = 0) & (v16 = 0 | v15 = 0) & (v14 = 0 | v13 = 0) & (v12 = 0 | v11 = 0) & (v10 = 0 | v9 = 0) & (v8 = 0 | v7 = 0) & (v6 = 0 | v5 = 0) & (v4 = 0 | v3 = 0))))) % 20.52/6.43 | (74) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB0(v2) = v1) | ~ (cB0(v2) = v0)) % 20.52/6.43 | (75) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA4(v2) = v1) | ~ (cA4(v2) = v0)) % 20.52/6.43 | (76) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA3(v2) = v1) | ~ (cA3(v2) = v0)) % 20.52/6.43 | (77) ! [v0] : ! [v1] : (v1 = 0 | ~ (cowlThing(v0) = v1)) % 20.52/6.43 | (78) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB11(v2) = v1) | ~ (cB11(v2) = v0)) % 20.52/6.43 | (79) ! [v0] : ( ~ (xsd_string(v0) = 0) | ? [v1] : ( ~ (v1 = 0) & xsd_integer(v0) = v1)) % 20.52/6.43 | (80) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB20(v2) = v1) | ~ (cB20(v2) = v0)) % 20.52/6.43 | (81) ! [v0] : ( ~ (cC3(v0) = 0) | ? [v1] : ? [v2] : ( ~ (v2 = 0) & cB(v0) = v1 & cA(v0) = v2)) % 20.52/6.43 | (82) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB5(v2) = v1) | ~ (cB5(v2) = v0)) % 20.52/6.43 | (83) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA2(v2) = v1) | ~ (cA2(v2) = v0)) % 20.52/6.43 | (84) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB29(v2) = v1) | ~ (cB29(v2) = v0)) % 20.52/6.43 | (85) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cB10(v2) = v1) | ~ (cB10(v2) = v0)) % 20.52/6.43 | (86) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA16(v2) = v1) | ~ (cA16(v2) = v0)) % 20.52/6.43 | (87) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA6(v2) = v1) | ~ (cA6(v2) = v0)) % 20.52/6.43 | (88) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (cA0(v2) = v1) | ~ (cA0(v2) = v0)) % 20.52/6.44 | % 20.52/6.44 | Instantiating formula (21) with i2003_11_14_17_19_57994 and discharging atoms cTEST(i2003_11_14_17_19_57994) = 0, yields: % 20.52/6.44 | (89) cC5(i2003_11_14_17_19_57994) = 0 & cC4(i2003_11_14_17_19_57994) = 0 & cC1(i2003_11_14_17_19_57994) = 0 % 20.52/6.44 | % 20.52/6.44 | Applying alpha-rule on (89) yields: % 20.52/6.44 | (90) cC5(i2003_11_14_17_19_57994) = 0 % 20.52/6.44 | (91) cC4(i2003_11_14_17_19_57994) = 0 % 20.52/6.44 | (92) cC1(i2003_11_14_17_19_57994) = 0 % 20.52/6.44 | % 20.52/6.44 | Instantiating formula (20) with i2003_11_14_17_19_57994 and discharging atoms cC4(i2003_11_14_17_19_57994) = 0, yields: % 20.52/6.44 | (93) ? [v0] : (rR(i2003_11_14_17_19_57994, v0) = 0 & cC2(v0) = 0) % 20.52/6.44 | % 20.52/6.44 | Instantiating (93) with all_13_0_0 yields: % 20.52/6.44 | (94) rR(i2003_11_14_17_19_57994, all_13_0_0) = 0 & cC2(all_13_0_0) = 0 % 20.52/6.44 | % 20.52/6.44 | Applying alpha-rule on (94) yields: % 20.52/6.44 | (95) rR(i2003_11_14_17_19_57994, all_13_0_0) = 0 % 20.52/6.44 | (96) cC2(all_13_0_0) = 0 % 20.52/6.44 | % 20.52/6.44 | Instantiating formula (35) with all_13_0_0, i2003_11_14_17_19_57994 and discharging atoms cC5(i2003_11_14_17_19_57994) = 0, rR(i2003_11_14_17_19_57994, all_13_0_0) = 0, yields: % 20.52/6.44 | (97) cC3(all_13_0_0) = 0 % 20.52/6.44 | % 20.52/6.44 | Instantiating formula (17) with all_13_0_0 and discharging atoms cC2(all_13_0_0) = 0, yields: % 20.52/6.44 | (98) ? [v0] : (cB(all_13_0_0) = v0 & cA(all_13_0_0) = 0) % 20.52/6.44 | % 20.52/6.44 | Instantiating (98) with all_21_0_1 yields: % 20.52/6.44 | (99) cB(all_13_0_0) = all_21_0_1 & cA(all_13_0_0) = 0 % 20.52/6.44 | % 20.52/6.44 | Applying alpha-rule on (99) yields: % 20.52/6.44 | (100) cB(all_13_0_0) = all_21_0_1 % 20.52/6.44 | (101) cA(all_13_0_0) = 0 % 20.52/6.44 | % 20.52/6.44 | Instantiating formula (81) with all_13_0_0 and discharging atoms cC3(all_13_0_0) = 0, yields: % 20.52/6.44 | (102) ? [v0] : ? [v1] : ( ~ (v1 = 0) & cB(all_13_0_0) = v0 & cA(all_13_0_0) = v1) % 20.52/6.44 | % 20.52/6.44 | Instantiating (102) with all_28_0_2, all_28_1_3 yields: % 20.52/6.44 | (103) ~ (all_28_0_2 = 0) & cB(all_13_0_0) = all_28_1_3 & cA(all_13_0_0) = all_28_0_2 % 20.52/6.44 | % 20.52/6.44 | Applying alpha-rule on (103) yields: % 20.52/6.44 | (104) ~ (all_28_0_2 = 0) % 20.52/6.44 | (105) cB(all_13_0_0) = all_28_1_3 % 20.52/6.44 | (106) cA(all_13_0_0) = all_28_0_2 % 20.52/6.44 | % 20.52/6.44 | Instantiating formula (64) with all_13_0_0, all_28_0_2, 0 and discharging atoms cA(all_13_0_0) = all_28_0_2, cA(all_13_0_0) = 0, yields: % 20.52/6.44 | (107) all_28_0_2 = 0 % 20.52/6.44 | % 20.52/6.44 | Equations (107) can reduce 104 to: % 20.52/6.44 | (108) $false % 20.52/6.44 | % 20.52/6.44 |-The branch is then unsatisfiable % 20.52/6.44 % SZS output end Proof for theBenchmark % 20.52/6.44 % 20.52/6.44 5937ms %------------------------------------------------------------------------------