%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NLP079+1 : TPTP v8.1.2. Released v2.4.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n006.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 : 300s % DateTime : Thu Aug 31 10:03:46 EDT 2023 % Result : Theorem 7.20s 1.69s % Output : Proof 11.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.13 % Problem : NLP079+1 : TPTP v8.1.2. Released v2.4.0. % 0.13/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.35 % Computer : n006.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Thu Aug 24 12:47:53 EDT 2023 % 0.14/0.35 % CPUTime : % 0.20/0.62 ________ _____ % 0.20/0.62 ___ __ \_________(_)________________________________ % 0.20/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.62 % 0.20/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.62 (2023-06-19) % 0.20/0.62 % 0.20/0.62 (c) Philipp Rümmer, 2009-2023 % 0.20/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.62 Amanda Stjerna. % 0.20/0.62 Free software under BSD-3-Clause. % 0.20/0.62 % 0.20/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.62 % 0.20/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.20/0.63 Running up to 7 provers in parallel. % 0.20/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.97/1.11 Prover 1: Preprocessing ... % 2.97/1.11 Prover 4: Preprocessing ... % 2.97/1.15 Prover 5: Preprocessing ... % 2.97/1.15 Prover 3: Preprocessing ... % 2.97/1.15 Prover 6: Preprocessing ... % 2.97/1.15 Prover 0: Preprocessing ... % 2.97/1.15 Prover 2: Preprocessing ... % 4.24/1.38 Prover 5: Constructing countermodel ... % 4.24/1.39 Prover 2: Constructing countermodel ... % 6.47/1.60 Prover 6: Proving ... % 6.47/1.62 Prover 1: Constructing countermodel ... % 6.47/1.65 Prover 3: Constructing countermodel ... % 7.20/1.69 Prover 2: proved (1053ms) % 7.20/1.69 % 7.20/1.69 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.20/1.69 % 7.20/1.69 Prover 3: stopped % 7.20/1.70 Prover 6: stopped % 7.20/1.70 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 7.20/1.70 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 7.20/1.70 Prover 5: stopped % 7.20/1.70 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 7.20/1.70 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 7.67/1.79 Prover 10: Preprocessing ... % 7.67/1.79 Prover 8: Preprocessing ... % 7.67/1.79 Prover 7: Preprocessing ... % 7.67/1.80 Prover 11: Preprocessing ... % 8.20/1.84 Prover 10: Constructing countermodel ... % 8.20/1.84 Prover 7: Constructing countermodel ... % 8.61/1.87 Prover 0: stopped % 8.61/1.88 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 8.61/1.92 Prover 13: Preprocessing ... % 9.22/1.96 Prover 13: Constructing countermodel ... % 9.22/1.97 Prover 8: Warning: ignoring some quantifiers % 9.22/1.98 Prover 8: Constructing countermodel ... % 9.22/2.00 Prover 10: Found proof (size 31) % 9.22/2.00 Prover 10: proved (296ms) % 9.22/2.00 Prover 1: stopped % 9.22/2.00 Prover 7: stopped % 9.22/2.00 Prover 8: stopped % 9.22/2.00 Prover 13: stopped % 9.22/2.07 Prover 11: stopped % 10.48/2.29 Prover 4: stopped % 10.48/2.29 % 10.48/2.29 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.48/2.29 % 10.48/2.29 % SZS output start Proof for theBenchmark % 10.48/2.30 Assumptions after simplification: % 10.48/2.30 --------------------------------- % 10.48/2.30 % 10.48/2.30 (co1) % 10.48/2.34 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 10.48/2.34 $i] : ? [v6: $i] : ? [v7: $i] : ($i(v7) & $i(v6) & $i(v5) & $i(v4) & % 10.48/2.34 $i(v3) & $i(v2) & $i(v1) & $i(v0) & ((scream(v0, v7) & cry(v0, v6) & % 10.48/2.34 revenge(v0, v5) & group(v0, v4) & six(v0, v4) & nonreflexive(v0, v7) & % 10.48/2.34 present(v0, v7) & patient(v0, v7, v6) & agent(v0, v7, v1) & event(v0, % 10.48/2.34 v7) & cannon(v0, v3) & of(v0, v7, v5) & of(v0, v3, v2) & man(v0, v2) & % 10.48/2.34 male(v0, v2) & male(v0, v1) & actual_world(v0) & ! [v8: $i] : ! [v9: % 10.48/2.34 $i] : ! [v10: $i] : ! [v11: $i] : ! [v12: $i] : ! [v13: $i] : ! % 10.48/2.34 [v14: $i] : ! [v15: $i] : ( ~ $i(v15) | ~ $i(v14) | ~ $i(v13) | ~ % 10.48/2.34 $i(v12) | ~ $i(v11) | ~ $i(v10) | ~ $i(v9) | ~ $i(v8) | ~ % 10.48/2.34 scream(v8, v15) | ~ cry(v8, v13) | ~ revenge(v8, v14) | ~ group(v8, % 10.48/2.34 v12) | ~ six(v8, v12) | ~ nonreflexive(v8, v15) | ~ present(v8, % 10.48/2.34 v15) | ~ patient(v8, v15, v13) | ~ agent(v8, v15, v9) | ~ % 10.48/2.34 event(v8, v15) | ~ cannon(v8, v11) | ~ of(v8, v15, v14) | ~ of(v8, % 10.48/2.34 v11, v10) | ~ man(v8, v10) | ~ male(v8, v10) | ~ male(v8, v9) | % 10.48/2.34 ~ actual_world(v8) | ? [v16: $i] : ($i(v16) & ((member(v8, v16, v12) % 10.48/2.34 & ~ shot(v8, v16)) | (member(v8, v16, v12) & ! [v17: $i] : ( ~ % 10.48/2.34 $i(v17) | ~ from_loc(v8, v17, v11) | ~ fire(v8, v17) | ~ % 10.48/2.34 nonreflexive(v8, v17) | ~ present(v8, v17) | ~ patient(v8, % 10.48/2.34 v17, v16) | ~ agent(v8, v17, v10) | ~ event(v8, v17)))))) % 10.48/2.34 & ! [v8: $i] : ( ~ $i(v8) | ~ member(v0, v8, v4) | shot(v0, v8)) & ! % 10.48/2.34 [v8: $i] : ( ~ $i(v8) | ~ member(v0, v8, v4) | ? [v9: $i] : ($i(v9) & % 10.48/2.34 from_loc(v0, v9, v3) & fire(v0, v9) & nonreflexive(v0, v9) & % 10.48/2.34 present(v0, v9) & patient(v0, v9, v8) & agent(v0, v9, v2) & % 10.48/2.34 event(v0, v9)))) | (scream(v0, v7) & cry(v0, v5) & revenge(v0, v6) & % 10.48/2.34 group(v0, v4) & six(v0, v4) & nonreflexive(v0, v7) & present(v0, v7) & % 10.48/2.34 patient(v0, v7, v5) & agent(v0, v7, v1) & event(v0, v7) & cannon(v0, v3) % 10.48/2.34 & of(v0, v7, v6) & of(v0, v3, v2) & man(v0, v2) & male(v0, v2) & % 10.48/2.34 male(v0, v1) & actual_world(v0) & ! [v8: $i] : ! [v9: $i] : ! [v10: % 10.48/2.34 $i] : ! [v11: $i] : ! [v12: $i] : ! [v13: $i] : ! [v14: $i] : ! % 10.48/2.34 [v15: $i] : ( ~ $i(v15) | ~ $i(v14) | ~ $i(v13) | ~ $i(v12) | ~ % 10.48/2.34 $i(v11) | ~ $i(v10) | ~ $i(v9) | ~ $i(v8) | ~ scream(v8, v15) | ~ % 10.48/2.34 cry(v8, v14) | ~ revenge(v8, v13) | ~ group(v8, v12) | ~ six(v8, % 10.48/2.34 v12) | ~ nonreflexive(v8, v15) | ~ present(v8, v15) | ~ % 10.48/2.34 patient(v8, v15, v14) | ~ agent(v8, v15, v9) | ~ event(v8, v15) | ~ % 10.48/2.34 cannon(v8, v11) | ~ of(v8, v15, v13) | ~ of(v8, v11, v10) | ~ % 10.48/2.34 man(v8, v10) | ~ male(v8, v10) | ~ male(v8, v9) | ~ % 10.48/2.34 actual_world(v8) | ? [v16: $i] : ($i(v16) & ((member(v8, v16, v12) & % 10.48/2.34 ~ shot(v8, v16)) | (member(v8, v16, v12) & ! [v17: $i] : ( ~ % 10.48/2.34 $i(v17) | ~ from_loc(v8, v17, v11) | ~ fire(v8, v17) | ~ % 10.48/2.34 nonreflexive(v8, v17) | ~ present(v8, v17) | ~ patient(v8, % 10.48/2.34 v17, v16) | ~ agent(v8, v17, v10) | ~ event(v8, v17)))))) % 10.48/2.34 & ! [v8: $i] : ( ~ $i(v8) | ~ member(v0, v8, v4) | shot(v0, v8)) & ! % 10.48/2.34 [v8: $i] : ( ~ $i(v8) | ~ member(v0, v8, v4) | ? [v9: $i] : ($i(v9) & % 10.48/2.34 from_loc(v0, v9, v3) & fire(v0, v9) & nonreflexive(v0, v9) & % 10.48/2.34 present(v0, v9) & patient(v0, v9, v8) & agent(v0, v9, v2) & % 10.48/2.34 event(v0, v9)))))) % 10.48/2.34 % 10.48/2.34 Those formulas are unsatisfiable: % 10.48/2.34 --------------------------------- % 10.48/2.34 % 10.48/2.34 Begin of proof % 10.48/2.35 | % 10.48/2.35 | DELTA: instantiating (co1) with fresh symbols all_2_0, all_2_1, all_2_2, % 10.48/2.35 | all_2_3, all_2_4, all_2_5, all_2_6, all_2_7 gives: % 10.79/2.37 | (1) $i(all_2_0) & $i(all_2_1) & $i(all_2_2) & $i(all_2_3) & $i(all_2_4) & % 10.79/2.37 | $i(all_2_5) & $i(all_2_6) & $i(all_2_7) & ((scream(all_2_7, all_2_0) & % 10.79/2.37 | cry(all_2_7, all_2_1) & revenge(all_2_7, all_2_2) & group(all_2_7, % 10.79/2.37 | all_2_3) & six(all_2_7, all_2_3) & nonreflexive(all_2_7, all_2_0) % 10.79/2.37 | & present(all_2_7, all_2_0) & patient(all_2_7, all_2_0, all_2_1) & % 10.79/2.37 | agent(all_2_7, all_2_0, all_2_6) & event(all_2_7, all_2_0) & % 10.79/2.37 | cannon(all_2_7, all_2_4) & of(all_2_7, all_2_0, all_2_2) & % 10.79/2.37 | of(all_2_7, all_2_4, all_2_5) & man(all_2_7, all_2_5) & % 10.79/2.37 | male(all_2_7, all_2_5) & male(all_2_7, all_2_6) & % 10.79/2.37 | actual_world(all_2_7) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 10.79/2.37 | ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] % 10.79/2.37 | : ( ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 10.79/2.37 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ scream(v0, v7) | ~ cry(v0, % 10.79/2.37 | v5) | ~ revenge(v0, v6) | ~ group(v0, v4) | ~ six(v0, v4) | % 10.79/2.37 | ~ nonreflexive(v0, v7) | ~ present(v0, v7) | ~ patient(v0, v7, % 10.79/2.37 | v5) | ~ agent(v0, v7, v1) | ~ event(v0, v7) | ~ cannon(v0, % 10.79/2.37 | v3) | ~ of(v0, v7, v6) | ~ of(v0, v3, v2) | ~ man(v0, v2) | % 10.79/2.37 | ~ male(v0, v2) | ~ male(v0, v1) | ~ actual_world(v0) | ? [v8: % 10.79/2.37 | $i] : ($i(v8) & ((member(v0, v8, v4) & ~ shot(v0, v8)) | % 10.79/2.37 | (member(v0, v8, v4) & ! [v9: $i] : ( ~ $i(v9) | ~ % 10.79/2.37 | from_loc(v0, v9, v3) | ~ fire(v0, v9) | ~ % 10.79/2.37 | nonreflexive(v0, v9) | ~ present(v0, v9) | ~ % 10.79/2.37 | patient(v0, v9, v8) | ~ agent(v0, v9, v2) | ~ event(v0, % 10.79/2.37 | v9)))))) & ! [v0: $i] : ( ~ $i(v0) | ~ % 10.79/2.37 | member(all_2_7, v0, all_2_3) | shot(all_2_7, v0)) & ! [v0: $i] : % 10.79/2.37 | ( ~ $i(v0) | ~ member(all_2_7, v0, all_2_3) | ? [v1: $i] : % 10.79/2.37 | ($i(v1) & from_loc(all_2_7, v1, all_2_4) & fire(all_2_7, v1) & % 10.79/2.37 | nonreflexive(all_2_7, v1) & present(all_2_7, v1) & % 10.79/2.37 | patient(all_2_7, v1, v0) & agent(all_2_7, v1, all_2_5) & % 10.79/2.37 | event(all_2_7, v1)))) | (scream(all_2_7, all_2_0) & % 10.79/2.37 | cry(all_2_7, all_2_2) & revenge(all_2_7, all_2_1) & group(all_2_7, % 10.79/2.37 | all_2_3) & six(all_2_7, all_2_3) & nonreflexive(all_2_7, all_2_0) % 10.79/2.37 | & present(all_2_7, all_2_0) & patient(all_2_7, all_2_0, all_2_2) & % 10.79/2.37 | agent(all_2_7, all_2_0, all_2_6) & event(all_2_7, all_2_0) & % 10.79/2.37 | cannon(all_2_7, all_2_4) & of(all_2_7, all_2_0, all_2_1) & % 10.79/2.37 | of(all_2_7, all_2_4, all_2_5) & man(all_2_7, all_2_5) & % 10.79/2.37 | male(all_2_7, all_2_5) & male(all_2_7, all_2_6) & % 10.79/2.37 | actual_world(all_2_7) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 10.79/2.37 | ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] % 10.79/2.37 | : ( ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 10.79/2.37 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ scream(v0, v7) | ~ cry(v0, % 10.79/2.37 | v6) | ~ revenge(v0, v5) | ~ group(v0, v4) | ~ six(v0, v4) | % 10.79/2.37 | ~ nonreflexive(v0, v7) | ~ present(v0, v7) | ~ patient(v0, v7, % 10.79/2.37 | v6) | ~ agent(v0, v7, v1) | ~ event(v0, v7) | ~ cannon(v0, % 10.79/2.37 | v3) | ~ of(v0, v7, v5) | ~ of(v0, v3, v2) | ~ man(v0, v2) | % 10.79/2.37 | ~ male(v0, v2) | ~ male(v0, v1) | ~ actual_world(v0) | ? [v8: % 10.79/2.37 | $i] : ($i(v8) & ((member(v0, v8, v4) & ~ shot(v0, v8)) | % 10.79/2.37 | (member(v0, v8, v4) & ! [v9: $i] : ( ~ $i(v9) | ~ % 10.79/2.37 | from_loc(v0, v9, v3) | ~ fire(v0, v9) | ~ % 10.79/2.37 | nonreflexive(v0, v9) | ~ present(v0, v9) | ~ % 10.79/2.37 | patient(v0, v9, v8) | ~ agent(v0, v9, v2) | ~ event(v0, % 10.79/2.37 | v9)))))) & ! [v0: $i] : ( ~ $i(v0) | ~ % 10.79/2.37 | member(all_2_7, v0, all_2_3) | shot(all_2_7, v0)) & ! [v0: $i] : % 10.79/2.37 | ( ~ $i(v0) | ~ member(all_2_7, v0, all_2_3) | ? [v1: $i] : % 10.79/2.37 | ($i(v1) & from_loc(all_2_7, v1, all_2_4) & fire(all_2_7, v1) & % 10.79/2.37 | nonreflexive(all_2_7, v1) & present(all_2_7, v1) & % 10.79/2.37 | patient(all_2_7, v1, v0) & agent(all_2_7, v1, all_2_5) & % 10.79/2.37 | event(all_2_7, v1))))) % 10.79/2.37 | % 10.79/2.37 | ALPHA: (1) implies: % 10.79/2.37 | (2) $i(all_2_7) % 10.79/2.37 | (3) $i(all_2_6) % 10.79/2.37 | (4) $i(all_2_5) % 10.79/2.37 | (5) $i(all_2_4) % 10.79/2.37 | (6) $i(all_2_3) % 10.79/2.37 | (7) $i(all_2_2) % 10.79/2.37 | (8) $i(all_2_1) % 10.79/2.37 | (9) $i(all_2_0) % 10.89/2.38 | (10) (scream(all_2_7, all_2_0) & cry(all_2_7, all_2_1) & revenge(all_2_7, % 10.89/2.38 | all_2_2) & group(all_2_7, all_2_3) & six(all_2_7, all_2_3) & % 10.89/2.38 | nonreflexive(all_2_7, all_2_0) & present(all_2_7, all_2_0) & % 10.89/2.38 | patient(all_2_7, all_2_0, all_2_1) & agent(all_2_7, all_2_0, % 10.89/2.38 | all_2_6) & event(all_2_7, all_2_0) & cannon(all_2_7, all_2_4) & % 10.89/2.38 | of(all_2_7, all_2_0, all_2_2) & of(all_2_7, all_2_4, all_2_5) & % 10.89/2.38 | man(all_2_7, all_2_5) & male(all_2_7, all_2_5) & male(all_2_7, % 10.89/2.38 | all_2_6) & actual_world(all_2_7) & ! [v0: $i] : ! [v1: $i] : ! % 10.89/2.38 | [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : % 10.89/2.38 | ! [v7: $i] : ( ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ % 10.89/2.38 | $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ scream(v0, v7) | % 10.89/2.38 | ~ cry(v0, v5) | ~ revenge(v0, v6) | ~ group(v0, v4) | ~ six(v0, % 10.89/2.38 | v4) | ~ nonreflexive(v0, v7) | ~ present(v0, v7) | ~ % 10.89/2.38 | patient(v0, v7, v5) | ~ agent(v0, v7, v1) | ~ event(v0, v7) | ~ % 10.89/2.38 | cannon(v0, v3) | ~ of(v0, v7, v6) | ~ of(v0, v3, v2) | ~ % 10.89/2.38 | man(v0, v2) | ~ male(v0, v2) | ~ male(v0, v1) | ~ % 10.89/2.38 | actual_world(v0) | ? [v8: $i] : ($i(v8) & ((member(v0, v8, v4) & % 10.89/2.38 | ~ shot(v0, v8)) | (member(v0, v8, v4) & ! [v9: $i] : ( ~ % 10.89/2.38 | $i(v9) | ~ from_loc(v0, v9, v3) | ~ fire(v0, v9) | ~ % 10.89/2.38 | nonreflexive(v0, v9) | ~ present(v0, v9) | ~ patient(v0, % 10.89/2.38 | v9, v8) | ~ agent(v0, v9, v2) | ~ event(v0, v9)))))) & % 10.89/2.38 | ! [v0: $i] : ( ~ $i(v0) | ~ member(all_2_7, v0, all_2_3) | % 10.89/2.38 | shot(all_2_7, v0)) & ! [v0: $i] : ( ~ $i(v0) | ~ member(all_2_7, % 10.89/2.38 | v0, all_2_3) | ? [v1: $i] : ($i(v1) & from_loc(all_2_7, v1, % 10.89/2.38 | all_2_4) & fire(all_2_7, v1) & nonreflexive(all_2_7, v1) & % 10.89/2.38 | present(all_2_7, v1) & patient(all_2_7, v1, v0) & agent(all_2_7, % 10.89/2.38 | v1, all_2_5) & event(all_2_7, v1)))) | (scream(all_2_7, % 10.89/2.38 | all_2_0) & cry(all_2_7, all_2_2) & revenge(all_2_7, all_2_1) & % 10.89/2.38 | group(all_2_7, all_2_3) & six(all_2_7, all_2_3) & % 10.89/2.38 | nonreflexive(all_2_7, all_2_0) & present(all_2_7, all_2_0) & % 10.89/2.38 | patient(all_2_7, all_2_0, all_2_2) & agent(all_2_7, all_2_0, % 10.89/2.38 | all_2_6) & event(all_2_7, all_2_0) & cannon(all_2_7, all_2_4) & % 10.89/2.38 | of(all_2_7, all_2_0, all_2_1) & of(all_2_7, all_2_4, all_2_5) & % 10.89/2.38 | man(all_2_7, all_2_5) & male(all_2_7, all_2_5) & male(all_2_7, % 10.89/2.38 | all_2_6) & actual_world(all_2_7) & ! [v0: $i] : ! [v1: $i] : ! % 10.89/2.38 | [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : % 10.89/2.38 | ! [v7: $i] : ( ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ % 10.89/2.38 | $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ scream(v0, v7) | % 10.89/2.38 | ~ cry(v0, v6) | ~ revenge(v0, v5) | ~ group(v0, v4) | ~ six(v0, % 10.89/2.38 | v4) | ~ nonreflexive(v0, v7) | ~ present(v0, v7) | ~ % 10.89/2.38 | patient(v0, v7, v6) | ~ agent(v0, v7, v1) | ~ event(v0, v7) | ~ % 10.89/2.38 | cannon(v0, v3) | ~ of(v0, v7, v5) | ~ of(v0, v3, v2) | ~ % 10.89/2.38 | man(v0, v2) | ~ male(v0, v2) | ~ male(v0, v1) | ~ % 10.89/2.38 | actual_world(v0) | ? [v8: $i] : ($i(v8) & ((member(v0, v8, v4) & % 10.89/2.38 | ~ shot(v0, v8)) | (member(v0, v8, v4) & ! [v9: $i] : ( ~ % 10.89/2.38 | $i(v9) | ~ from_loc(v0, v9, v3) | ~ fire(v0, v9) | ~ % 10.89/2.38 | nonreflexive(v0, v9) | ~ present(v0, v9) | ~ patient(v0, % 10.89/2.38 | v9, v8) | ~ agent(v0, v9, v2) | ~ event(v0, v9)))))) & % 10.89/2.38 | ! [v0: $i] : ( ~ $i(v0) | ~ member(all_2_7, v0, all_2_3) | % 10.89/2.38 | shot(all_2_7, v0)) & ! [v0: $i] : ( ~ $i(v0) | ~ member(all_2_7, % 10.89/2.38 | v0, all_2_3) | ? [v1: $i] : ($i(v1) & from_loc(all_2_7, v1, % 10.89/2.38 | all_2_4) & fire(all_2_7, v1) & nonreflexive(all_2_7, v1) & % 10.89/2.38 | present(all_2_7, v1) & patient(all_2_7, v1, v0) & agent(all_2_7, % 10.89/2.38 | v1, all_2_5) & event(all_2_7, v1)))) % 10.89/2.38 | % 10.89/2.38 | BETA: splitting (10) gives: % 10.89/2.38 | % 10.89/2.38 | Case 1: % 10.89/2.38 | | % 10.89/2.39 | | (11) scream(all_2_7, all_2_0) & cry(all_2_7, all_2_1) & revenge(all_2_7, % 10.89/2.39 | | all_2_2) & group(all_2_7, all_2_3) & six(all_2_7, all_2_3) & % 10.89/2.39 | | nonreflexive(all_2_7, all_2_0) & present(all_2_7, all_2_0) & % 10.89/2.39 | | patient(all_2_7, all_2_0, all_2_1) & agent(all_2_7, all_2_0, % 10.89/2.39 | | all_2_6) & event(all_2_7, all_2_0) & cannon(all_2_7, all_2_4) & % 10.89/2.39 | | of(all_2_7, all_2_0, all_2_2) & of(all_2_7, all_2_4, all_2_5) & % 10.89/2.39 | | man(all_2_7, all_2_5) & male(all_2_7, all_2_5) & male(all_2_7, % 10.89/2.39 | | all_2_6) & actual_world(all_2_7) & ! [v0: $i] : ! [v1: $i] : ! % 10.89/2.39 | | [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : % 10.89/2.39 | | ! [v7: $i] : ( ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ % 10.89/2.39 | | $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ scream(v0, v7) | % 10.89/2.39 | | ~ cry(v0, v5) | ~ revenge(v0, v6) | ~ group(v0, v4) | ~ six(v0, % 10.89/2.39 | | v4) | ~ nonreflexive(v0, v7) | ~ present(v0, v7) | ~ % 10.89/2.39 | | patient(v0, v7, v5) | ~ agent(v0, v7, v1) | ~ event(v0, v7) | ~ % 10.89/2.39 | | cannon(v0, v3) | ~ of(v0, v7, v6) | ~ of(v0, v3, v2) | ~ % 10.89/2.39 | | man(v0, v2) | ~ male(v0, v2) | ~ male(v0, v1) | ~ % 10.89/2.39 | | actual_world(v0) | ? [v8: $i] : ($i(v8) & ((member(v0, v8, v4) & % 10.89/2.39 | | ~ shot(v0, v8)) | (member(v0, v8, v4) & ! [v9: $i] : ( ~ % 10.89/2.39 | | $i(v9) | ~ from_loc(v0, v9, v3) | ~ fire(v0, v9) | ~ % 10.89/2.39 | | nonreflexive(v0, v9) | ~ present(v0, v9) | ~ patient(v0, % 10.89/2.39 | | v9, v8) | ~ agent(v0, v9, v2) | ~ event(v0, v9)))))) & % 10.89/2.39 | | ! [v0: $i] : ( ~ $i(v0) | ~ member(all_2_7, v0, all_2_3) | % 10.89/2.39 | | shot(all_2_7, v0)) & ! [v0: $i] : ( ~ $i(v0) | ~ member(all_2_7, % 10.89/2.39 | | v0, all_2_3) | ? [v1: $i] : ($i(v1) & from_loc(all_2_7, v1, % 10.89/2.39 | | all_2_4) & fire(all_2_7, v1) & nonreflexive(all_2_7, v1) & % 10.89/2.39 | | present(all_2_7, v1) & patient(all_2_7, v1, v0) & agent(all_2_7, % 10.89/2.39 | | v1, all_2_5) & event(all_2_7, v1))) % 10.89/2.39 | | % 10.89/2.39 | | ALPHA: (11) implies: % 10.89/2.39 | | (12) actual_world(all_2_7) % 10.89/2.39 | | (13) male(all_2_7, all_2_6) % 10.89/2.39 | | (14) male(all_2_7, all_2_5) % 10.89/2.39 | | (15) man(all_2_7, all_2_5) % 10.89/2.39 | | (16) of(all_2_7, all_2_4, all_2_5) % 10.89/2.39 | | (17) of(all_2_7, all_2_0, all_2_2) % 10.89/2.39 | | (18) cannon(all_2_7, all_2_4) % 10.89/2.39 | | (19) event(all_2_7, all_2_0) % 10.89/2.39 | | (20) agent(all_2_7, all_2_0, all_2_6) % 10.89/2.39 | | (21) patient(all_2_7, all_2_0, all_2_1) % 10.89/2.39 | | (22) present(all_2_7, all_2_0) % 10.89/2.39 | | (23) nonreflexive(all_2_7, all_2_0) % 10.89/2.39 | | (24) six(all_2_7, all_2_3) % 10.89/2.39 | | (25) group(all_2_7, all_2_3) % 10.89/2.39 | | (26) revenge(all_2_7, all_2_2) % 10.89/2.39 | | (27) cry(all_2_7, all_2_1) % 10.89/2.39 | | (28) scream(all_2_7, all_2_0) % 10.89/2.39 | | (29) ! [v0: $i] : ( ~ $i(v0) | ~ member(all_2_7, v0, all_2_3) | ? [v1: % 10.89/2.39 | | $i] : ($i(v1) & from_loc(all_2_7, v1, all_2_4) & fire(all_2_7, % 10.89/2.39 | | v1) & nonreflexive(all_2_7, v1) & present(all_2_7, v1) & % 10.89/2.39 | | patient(all_2_7, v1, v0) & agent(all_2_7, v1, all_2_5) & % 10.89/2.39 | | event(all_2_7, v1))) % 10.89/2.39 | | (30) ! [v0: $i] : ( ~ $i(v0) | ~ member(all_2_7, v0, all_2_3) | % 10.89/2.39 | | shot(all_2_7, v0)) % 10.89/2.40 | | (31) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 10.89/2.40 | | : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ( ~ $i(v7) | ~ $i(v6) | % 10.89/2.40 | | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 10.89/2.40 | | $i(v0) | ~ scream(v0, v7) | ~ cry(v0, v5) | ~ revenge(v0, v6) | % 10.89/2.40 | | ~ group(v0, v4) | ~ six(v0, v4) | ~ nonreflexive(v0, v7) | ~ % 10.89/2.40 | | present(v0, v7) | ~ patient(v0, v7, v5) | ~ agent(v0, v7, v1) | % 10.89/2.40 | | ~ event(v0, v7) | ~ cannon(v0, v3) | ~ of(v0, v7, v6) | ~ % 10.89/2.40 | | of(v0, v3, v2) | ~ man(v0, v2) | ~ male(v0, v2) | ~ male(v0, % 10.89/2.40 | | v1) | ~ actual_world(v0) | ? [v8: $i] : ($i(v8) & ((member(v0, % 10.89/2.40 | | v8, v4) & ~ shot(v0, v8)) | (member(v0, v8, v4) & ! [v9: % 10.89/2.40 | | $i] : ( ~ $i(v9) | ~ from_loc(v0, v9, v3) | ~ fire(v0, % 10.89/2.40 | | v9) | ~ nonreflexive(v0, v9) | ~ present(v0, v9) | ~ % 10.89/2.40 | | patient(v0, v9, v8) | ~ agent(v0, v9, v2) | ~ event(v0, % 10.89/2.40 | | v9)))))) % 10.89/2.40 | | % 10.89/2.40 | | GROUND_INST: instantiating (31) with all_2_7, all_2_6, all_2_5, all_2_4, % 10.89/2.40 | | all_2_3, all_2_1, all_2_2, all_2_0, simplifying with (2), (3), % 10.89/2.40 | | (4), (5), (6), (7), (8), (9), (12), (13), (14), (15), (16), % 10.89/2.40 | | (17), (18), (19), (20), (21), (22), (23), (24), (25), (26), % 10.89/2.40 | | (27), (28) gives: % 10.89/2.40 | | (32) ? [v0: $i] : ($i(v0) & ((member(all_2_7, v0, all_2_3) & ~ % 10.89/2.40 | | shot(all_2_7, v0)) | (member(all_2_7, v0, all_2_3) & ! [v1: % 10.89/2.40 | | $i] : ( ~ $i(v1) | ~ from_loc(all_2_7, v1, all_2_4) | ~ % 10.89/2.40 | | fire(all_2_7, v1) | ~ nonreflexive(all_2_7, v1) | ~ % 10.89/2.40 | | present(all_2_7, v1) | ~ patient(all_2_7, v1, v0) | ~ % 10.89/2.40 | | agent(all_2_7, v1, all_2_5) | ~ event(all_2_7, v1))))) % 10.89/2.40 | | % 10.89/2.40 | | DELTA: instantiating (32) with fresh symbol all_17_0 gives: % 10.89/2.40 | | (33) $i(all_17_0) & ((member(all_2_7, all_17_0, all_2_3) & ~ % 10.89/2.40 | | shot(all_2_7, all_17_0)) | (member(all_2_7, all_17_0, all_2_3) & % 10.89/2.40 | | ! [v0: $i] : ( ~ $i(v0) | ~ from_loc(all_2_7, v0, all_2_4) | % 10.89/2.40 | | ~ fire(all_2_7, v0) | ~ nonreflexive(all_2_7, v0) | ~ % 10.89/2.40 | | present(all_2_7, v0) | ~ patient(all_2_7, v0, all_17_0) | ~ % 10.89/2.40 | | agent(all_2_7, v0, all_2_5) | ~ event(all_2_7, v0)))) % 10.89/2.40 | | % 10.89/2.40 | | ALPHA: (33) implies: % 10.89/2.40 | | (34) $i(all_17_0) % 10.89/2.40 | | (35) (member(all_2_7, all_17_0, all_2_3) & ~ shot(all_2_7, all_17_0)) | % 10.89/2.40 | | (member(all_2_7, all_17_0, all_2_3) & ! [v0: $i] : ( ~ $i(v0) | ~ % 10.89/2.40 | | from_loc(all_2_7, v0, all_2_4) | ~ fire(all_2_7, v0) | ~ % 10.89/2.40 | | nonreflexive(all_2_7, v0) | ~ present(all_2_7, v0) | ~ % 10.89/2.40 | | patient(all_2_7, v0, all_17_0) | ~ agent(all_2_7, v0, all_2_5) % 10.89/2.40 | | | ~ event(all_2_7, v0))) % 10.89/2.40 | | % 10.89/2.40 | | BETA: splitting (35) gives: % 10.89/2.40 | | % 10.89/2.40 | | Case 1: % 10.89/2.40 | | | % 10.89/2.40 | | | (36) member(all_2_7, all_17_0, all_2_3) & ~ shot(all_2_7, all_17_0) % 10.89/2.40 | | | % 10.89/2.40 | | | ALPHA: (36) implies: % 10.89/2.40 | | | (37) ~ shot(all_2_7, all_17_0) % 10.89/2.40 | | | (38) member(all_2_7, all_17_0, all_2_3) % 10.89/2.40 | | | % 10.89/2.41 | | | GROUND_INST: instantiating (30) with all_17_0, simplifying with (34), % 10.89/2.41 | | | (37), (38) gives: % 10.89/2.41 | | | (39) $false % 10.89/2.41 | | | % 10.89/2.41 | | | CLOSE: (39) is inconsistent. % 10.89/2.41 | | | % 10.89/2.41 | | Case 2: % 10.89/2.41 | | | % 10.89/2.41 | | | (40) member(all_2_7, all_17_0, all_2_3) & ! [v0: $i] : ( ~ $i(v0) | ~ % 10.89/2.41 | | | from_loc(all_2_7, v0, all_2_4) | ~ fire(all_2_7, v0) | ~ % 10.89/2.41 | | | nonreflexive(all_2_7, v0) | ~ present(all_2_7, v0) | ~ % 10.89/2.41 | | | patient(all_2_7, v0, all_17_0) | ~ agent(all_2_7, v0, all_2_5) % 10.89/2.41 | | | | ~ event(all_2_7, v0)) % 10.89/2.41 | | | % 10.89/2.41 | | | ALPHA: (40) implies: % 10.89/2.41 | | | (41) member(all_2_7, all_17_0, all_2_3) % 10.89/2.41 | | | (42) ! [v0: $i] : ( ~ $i(v0) | ~ from_loc(all_2_7, v0, all_2_4) | ~ % 10.89/2.41 | | | fire(all_2_7, v0) | ~ nonreflexive(all_2_7, v0) | ~ % 10.89/2.41 | | | present(all_2_7, v0) | ~ patient(all_2_7, v0, all_17_0) | ~ % 10.89/2.41 | | | agent(all_2_7, v0, all_2_5) | ~ event(all_2_7, v0)) % 10.89/2.41 | | | % 10.89/2.41 | | | GROUND_INST: instantiating (29) with all_17_0, simplifying with (34), (41) % 10.89/2.41 | | | gives: % 10.89/2.41 | | | (43) ? [v0: $i] : ($i(v0) & from_loc(all_2_7, v0, all_2_4) & % 10.89/2.41 | | | fire(all_2_7, v0) & nonreflexive(all_2_7, v0) & present(all_2_7, % 10.89/2.41 | | | v0) & patient(all_2_7, v0, all_17_0) & agent(all_2_7, v0, % 10.89/2.41 | | | all_2_5) & event(all_2_7, v0)) % 10.89/2.41 | | | % 10.89/2.41 | | | DELTA: instantiating (43) with fresh symbol all_33_0 gives: % 10.89/2.41 | | | (44) $i(all_33_0) & from_loc(all_2_7, all_33_0, all_2_4) & % 10.89/2.41 | | | fire(all_2_7, all_33_0) & nonreflexive(all_2_7, all_33_0) & % 10.89/2.41 | | | present(all_2_7, all_33_0) & patient(all_2_7, all_33_0, all_17_0) % 10.89/2.41 | | | & agent(all_2_7, all_33_0, all_2_5) & event(all_2_7, all_33_0) % 10.89/2.41 | | | % 10.89/2.41 | | | ALPHA: (44) implies: % 10.89/2.41 | | | (45) event(all_2_7, all_33_0) % 10.89/2.41 | | | (46) agent(all_2_7, all_33_0, all_2_5) % 10.89/2.41 | | | (47) patient(all_2_7, all_33_0, all_17_0) % 10.89/2.41 | | | (48) present(all_2_7, all_33_0) % 10.89/2.41 | | | (49) nonreflexive(all_2_7, all_33_0) % 10.89/2.41 | | | (50) fire(all_2_7, all_33_0) % 10.89/2.41 | | | (51) from_loc(all_2_7, all_33_0, all_2_4) % 10.89/2.41 | | | (52) $i(all_33_0) % 10.89/2.41 | | | % 10.89/2.41 | | | GROUND_INST: instantiating (42) with all_33_0, simplifying with (45), % 10.89/2.41 | | | (46), (47), (48), (49), (50), (51), (52) gives: % 10.89/2.41 | | | (53) $false % 10.89/2.41 | | | % 10.89/2.41 | | | CLOSE: (53) is inconsistent. % 10.89/2.41 | | | % 10.89/2.41 | | End of split % 10.89/2.41 | | % 10.89/2.41 | Case 2: % 10.89/2.41 | | % 10.89/2.42 | | (54) scream(all_2_7, all_2_0) & cry(all_2_7, all_2_2) & revenge(all_2_7, % 10.89/2.42 | | all_2_1) & group(all_2_7, all_2_3) & six(all_2_7, all_2_3) & % 10.89/2.42 | | nonreflexive(all_2_7, all_2_0) & present(all_2_7, all_2_0) & % 10.89/2.42 | | patient(all_2_7, all_2_0, all_2_2) & agent(all_2_7, all_2_0, % 10.89/2.42 | | all_2_6) & event(all_2_7, all_2_0) & cannon(all_2_7, all_2_4) & % 10.89/2.42 | | of(all_2_7, all_2_0, all_2_1) & of(all_2_7, all_2_4, all_2_5) & % 10.89/2.42 | | man(all_2_7, all_2_5) & male(all_2_7, all_2_5) & male(all_2_7, % 10.89/2.42 | | all_2_6) & actual_world(all_2_7) & ! [v0: $i] : ! [v1: $i] : ! % 10.89/2.42 | | [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : % 10.89/2.42 | | ! [v7: $i] : ( ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ % 10.89/2.42 | | $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ scream(v0, v7) | % 10.89/2.42 | | ~ cry(v0, v6) | ~ revenge(v0, v5) | ~ group(v0, v4) | ~ six(v0, % 10.89/2.42 | | v4) | ~ nonreflexive(v0, v7) | ~ present(v0, v7) | ~ % 10.89/2.42 | | patient(v0, v7, v6) | ~ agent(v0, v7, v1) | ~ event(v0, v7) | ~ % 10.89/2.42 | | cannon(v0, v3) | ~ of(v0, v7, v5) | ~ of(v0, v3, v2) | ~ % 10.89/2.42 | | man(v0, v2) | ~ male(v0, v2) | ~ male(v0, v1) | ~ % 10.89/2.42 | | actual_world(v0) | ? [v8: $i] : ($i(v8) & ((member(v0, v8, v4) & % 10.89/2.42 | | ~ shot(v0, v8)) | (member(v0, v8, v4) & ! [v9: $i] : ( ~ % 10.89/2.42 | | $i(v9) | ~ from_loc(v0, v9, v3) | ~ fire(v0, v9) | ~ % 10.89/2.42 | | nonreflexive(v0, v9) | ~ present(v0, v9) | ~ patient(v0, % 10.89/2.42 | | v9, v8) | ~ agent(v0, v9, v2) | ~ event(v0, v9)))))) & % 10.89/2.42 | | ! [v0: $i] : ( ~ $i(v0) | ~ member(all_2_7, v0, all_2_3) | % 10.89/2.42 | | shot(all_2_7, v0)) & ! [v0: $i] : ( ~ $i(v0) | ~ member(all_2_7, % 10.89/2.42 | | v0, all_2_3) | ? [v1: $i] : ($i(v1) & from_loc(all_2_7, v1, % 10.89/2.42 | | all_2_4) & fire(all_2_7, v1) & nonreflexive(all_2_7, v1) & % 10.89/2.42 | | present(all_2_7, v1) & patient(all_2_7, v1, v0) & agent(all_2_7, % 10.89/2.42 | | v1, all_2_5) & event(all_2_7, v1))) % 10.89/2.42 | | % 10.89/2.42 | | ALPHA: (54) implies: % 11.09/2.42 | | (55) actual_world(all_2_7) % 11.09/2.42 | | (56) male(all_2_7, all_2_6) % 11.09/2.42 | | (57) male(all_2_7, all_2_5) % 11.09/2.42 | | (58) man(all_2_7, all_2_5) % 11.09/2.42 | | (59) of(all_2_7, all_2_4, all_2_5) % 11.09/2.42 | | (60) of(all_2_7, all_2_0, all_2_1) % 11.09/2.42 | | (61) cannon(all_2_7, all_2_4) % 11.09/2.42 | | (62) event(all_2_7, all_2_0) % 11.09/2.42 | | (63) agent(all_2_7, all_2_0, all_2_6) % 11.09/2.42 | | (64) patient(all_2_7, all_2_0, all_2_2) % 11.09/2.42 | | (65) present(all_2_7, all_2_0) % 11.09/2.42 | | (66) nonreflexive(all_2_7, all_2_0) % 11.09/2.42 | | (67) six(all_2_7, all_2_3) % 11.09/2.42 | | (68) group(all_2_7, all_2_3) % 11.09/2.42 | | (69) revenge(all_2_7, all_2_1) % 11.09/2.42 | | (70) cry(all_2_7, all_2_2) % 11.09/2.42 | | (71) scream(all_2_7, all_2_0) % 11.09/2.42 | | (72) ! [v0: $i] : ( ~ $i(v0) | ~ member(all_2_7, v0, all_2_3) | ? [v1: % 11.09/2.42 | | $i] : ($i(v1) & from_loc(all_2_7, v1, all_2_4) & fire(all_2_7, % 11.09/2.42 | | v1) & nonreflexive(all_2_7, v1) & present(all_2_7, v1) & % 11.09/2.42 | | patient(all_2_7, v1, v0) & agent(all_2_7, v1, all_2_5) & % 11.09/2.42 | | event(all_2_7, v1))) % 11.09/2.42 | | (73) ! [v0: $i] : ( ~ $i(v0) | ~ member(all_2_7, v0, all_2_3) | % 11.09/2.42 | | shot(all_2_7, v0)) % 11.09/2.43 | | (74) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 11.09/2.43 | | : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ( ~ $i(v7) | ~ $i(v6) | % 11.09/2.43 | | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 11.09/2.43 | | $i(v0) | ~ scream(v0, v7) | ~ cry(v0, v6) | ~ revenge(v0, v5) | % 11.09/2.43 | | ~ group(v0, v4) | ~ six(v0, v4) | ~ nonreflexive(v0, v7) | ~ % 11.09/2.43 | | present(v0, v7) | ~ patient(v0, v7, v6) | ~ agent(v0, v7, v1) | % 11.09/2.43 | | ~ event(v0, v7) | ~ cannon(v0, v3) | ~ of(v0, v7, v5) | ~ % 11.09/2.43 | | of(v0, v3, v2) | ~ man(v0, v2) | ~ male(v0, v2) | ~ male(v0, % 11.09/2.43 | | v1) | ~ actual_world(v0) | ? [v8: $i] : ($i(v8) & ((member(v0, % 11.09/2.43 | | v8, v4) & ~ shot(v0, v8)) | (member(v0, v8, v4) & ! [v9: % 11.09/2.43 | | $i] : ( ~ $i(v9) | ~ from_loc(v0, v9, v3) | ~ fire(v0, % 11.09/2.43 | | v9) | ~ nonreflexive(v0, v9) | ~ present(v0, v9) | ~ % 11.09/2.43 | | patient(v0, v9, v8) | ~ agent(v0, v9, v2) | ~ event(v0, % 11.09/2.43 | | v9)))))) % 11.09/2.43 | | % 11.09/2.43 | | GROUND_INST: instantiating (74) with all_2_7, all_2_6, all_2_5, all_2_4, % 11.09/2.43 | | all_2_3, all_2_1, all_2_2, all_2_0, simplifying with (2), (3), % 11.09/2.43 | | (4), (5), (6), (7), (8), (9), (55), (56), (57), (58), (59), % 11.09/2.43 | | (60), (61), (62), (63), (64), (65), (66), (67), (68), (69), % 11.09/2.43 | | (70), (71) gives: % 11.09/2.43 | | (75) ? [v0: $i] : ($i(v0) & ((member(all_2_7, v0, all_2_3) & ~ % 11.09/2.43 | | shot(all_2_7, v0)) | (member(all_2_7, v0, all_2_3) & ! [v1: % 11.09/2.43 | | $i] : ( ~ $i(v1) | ~ from_loc(all_2_7, v1, all_2_4) | ~ % 11.09/2.43 | | fire(all_2_7, v1) | ~ nonreflexive(all_2_7, v1) | ~ % 11.09/2.43 | | present(all_2_7, v1) | ~ patient(all_2_7, v1, v0) | ~ % 11.09/2.43 | | agent(all_2_7, v1, all_2_5) | ~ event(all_2_7, v1))))) % 11.09/2.43 | | % 11.09/2.43 | | DELTA: instantiating (75) with fresh symbol all_17_0 gives: % 11.09/2.43 | | (76) $i(all_17_0) & ((member(all_2_7, all_17_0, all_2_3) & ~ % 11.09/2.43 | | shot(all_2_7, all_17_0)) | (member(all_2_7, all_17_0, all_2_3) & % 11.09/2.43 | | ! [v0: $i] : ( ~ $i(v0) | ~ from_loc(all_2_7, v0, all_2_4) | % 11.09/2.43 | | ~ fire(all_2_7, v0) | ~ nonreflexive(all_2_7, v0) | ~ % 11.09/2.43 | | present(all_2_7, v0) | ~ patient(all_2_7, v0, all_17_0) | ~ % 11.09/2.43 | | agent(all_2_7, v0, all_2_5) | ~ event(all_2_7, v0)))) % 11.09/2.43 | | % 11.09/2.43 | | ALPHA: (76) implies: % 11.09/2.43 | | (77) $i(all_17_0) % 11.09/2.43 | | (78) (member(all_2_7, all_17_0, all_2_3) & ~ shot(all_2_7, all_17_0)) | % 11.09/2.43 | | (member(all_2_7, all_17_0, all_2_3) & ! [v0: $i] : ( ~ $i(v0) | ~ % 11.09/2.43 | | from_loc(all_2_7, v0, all_2_4) | ~ fire(all_2_7, v0) | ~ % 11.09/2.43 | | nonreflexive(all_2_7, v0) | ~ present(all_2_7, v0) | ~ % 11.09/2.43 | | patient(all_2_7, v0, all_17_0) | ~ agent(all_2_7, v0, all_2_5) % 11.09/2.43 | | | ~ event(all_2_7, v0))) % 11.09/2.43 | | % 11.09/2.43 | | BETA: splitting (78) gives: % 11.09/2.43 | | % 11.09/2.43 | | Case 1: % 11.09/2.43 | | | % 11.09/2.43 | | | (79) member(all_2_7, all_17_0, all_2_3) & ~ shot(all_2_7, all_17_0) % 11.09/2.43 | | | % 11.09/2.43 | | | ALPHA: (79) implies: % 11.09/2.43 | | | (80) ~ shot(all_2_7, all_17_0) % 11.09/2.43 | | | (81) member(all_2_7, all_17_0, all_2_3) % 11.09/2.43 | | | % 11.09/2.43 | | | GROUND_INST: instantiating (73) with all_17_0, simplifying with (77), % 11.09/2.43 | | | (80), (81) gives: % 11.09/2.43 | | | (82) $false % 11.09/2.43 | | | % 11.09/2.43 | | | CLOSE: (82) is inconsistent. % 11.09/2.43 | | | % 11.09/2.44 | | Case 2: % 11.09/2.44 | | | % 11.09/2.44 | | | (83) member(all_2_7, all_17_0, all_2_3) & ! [v0: $i] : ( ~ $i(v0) | ~ % 11.09/2.44 | | | from_loc(all_2_7, v0, all_2_4) | ~ fire(all_2_7, v0) | ~ % 11.09/2.44 | | | nonreflexive(all_2_7, v0) | ~ present(all_2_7, v0) | ~ % 11.09/2.44 | | | patient(all_2_7, v0, all_17_0) | ~ agent(all_2_7, v0, all_2_5) % 11.09/2.44 | | | | ~ event(all_2_7, v0)) % 11.09/2.44 | | | % 11.09/2.44 | | | ALPHA: (83) implies: % 11.09/2.44 | | | (84) member(all_2_7, all_17_0, all_2_3) % 11.09/2.44 | | | (85) ! [v0: $i] : ( ~ $i(v0) | ~ from_loc(all_2_7, v0, all_2_4) | ~ % 11.09/2.44 | | | fire(all_2_7, v0) | ~ nonreflexive(all_2_7, v0) | ~ % 11.09/2.44 | | | present(all_2_7, v0) | ~ patient(all_2_7, v0, all_17_0) | ~ % 11.09/2.44 | | | agent(all_2_7, v0, all_2_5) | ~ event(all_2_7, v0)) % 11.09/2.44 | | | % 11.09/2.44 | | | GROUND_INST: instantiating (72) with all_17_0, simplifying with (77), (84) % 11.09/2.44 | | | gives: % 11.09/2.44 | | | (86) ? [v0: $i] : ($i(v0) & from_loc(all_2_7, v0, all_2_4) & % 11.09/2.44 | | | fire(all_2_7, v0) & nonreflexive(all_2_7, v0) & present(all_2_7, % 11.09/2.44 | | | v0) & patient(all_2_7, v0, all_17_0) & agent(all_2_7, v0, % 11.09/2.44 | | | all_2_5) & event(all_2_7, v0)) % 11.09/2.44 | | | % 11.09/2.44 | | | DELTA: instantiating (86) with fresh symbol all_33_0 gives: % 11.09/2.44 | | | (87) $i(all_33_0) & from_loc(all_2_7, all_33_0, all_2_4) & % 11.09/2.44 | | | fire(all_2_7, all_33_0) & nonreflexive(all_2_7, all_33_0) & % 11.09/2.44 | | | present(all_2_7, all_33_0) & patient(all_2_7, all_33_0, all_17_0) % 11.09/2.44 | | | & agent(all_2_7, all_33_0, all_2_5) & event(all_2_7, all_33_0) % 11.09/2.44 | | | % 11.09/2.44 | | | ALPHA: (87) implies: % 11.09/2.44 | | | (88) event(all_2_7, all_33_0) % 11.09/2.44 | | | (89) agent(all_2_7, all_33_0, all_2_5) % 11.09/2.44 | | | (90) patient(all_2_7, all_33_0, all_17_0) % 11.09/2.44 | | | (91) present(all_2_7, all_33_0) % 11.09/2.44 | | | (92) nonreflexive(all_2_7, all_33_0) % 11.09/2.44 | | | (93) fire(all_2_7, all_33_0) % 11.09/2.44 | | | (94) from_loc(all_2_7, all_33_0, all_2_4) % 11.09/2.44 | | | (95) $i(all_33_0) % 11.09/2.44 | | | % 11.09/2.44 | | | GROUND_INST: instantiating (85) with all_33_0, simplifying with (88), % 11.09/2.44 | | | (89), (90), (91), (92), (93), (94), (95) gives: % 11.09/2.44 | | | (96) $false % 11.21/2.44 | | | % 11.21/2.44 | | | CLOSE: (96) is inconsistent. % 11.21/2.44 | | | % 11.21/2.44 | | End of split % 11.21/2.44 | | % 11.21/2.44 | End of split % 11.21/2.44 | % 11.21/2.44 End of proof % 11.21/2.44 % SZS output end Proof for theBenchmark % 11.21/2.44 % 11.21/2.44 1824ms %------------------------------------------------------------------------------