%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWX048+1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n027.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 : Tue Apr 1 02:15:30 AM UTC 2025 % Result : Theorem 100.90s 13.87s % Output : Proof 101.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SWX048+1 : TPTP v9.1.0. Released v9.1.0. % 0.03/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n027.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Mon Mar 31 14:58:51 EDT 2025 % 0.13/0.35 % CPUTime : % 0.67/0.65 ________ _____ % 0.67/0.65 ___ __ \_________(_)________________________________ % 0.67/0.65 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.67/0.65 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.67/0.65 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.67/0.65 % 0.67/0.65 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.67/0.65 (2023-06-19) % 0.67/0.65 % 0.67/0.65 (c) Philipp Rümmer, 2009-2023 % 0.67/0.65 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.67/0.65 Amanda Stjerna. % 0.67/0.65 Free software under BSD-3-Clause. % 0.67/0.65 % 0.67/0.65 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.67/0.65 % 0.67/0.65 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.73/0.67 Running up to 7 provers in parallel. % 0.73/0.69 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.73/0.69 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.73/0.69 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.73/0.69 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.73/0.69 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.73/0.69 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.73/0.69 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 7.81/1.81 Prover 1: Preprocessing ... % 8.08/1.82 Prover 4: Preprocessing ... % 8.24/1.86 Prover 5: Preprocessing ... % 8.24/1.86 Prover 2: Preprocessing ... % 8.24/1.86 Prover 0: Preprocessing ... % 8.24/1.86 Prover 3: Preprocessing ... % 8.24/1.86 Prover 6: Preprocessing ... % 20.64/3.48 Prover 5: Proving ... % 20.64/3.51 Prover 1: Warning: ignoring some quantifiers % 21.22/3.56 Prover 3: Warning: ignoring some quantifiers % 21.22/3.60 Prover 6: Proving ... % 21.22/3.60 Prover 2: Proving ... % 21.68/3.62 Prover 3: Constructing countermodel ... % 21.68/3.63 Prover 1: Constructing countermodel ... % 21.68/3.64 Prover 4: Warning: ignoring some quantifiers % 21.99/3.68 Prover 4: Constructing countermodel ... % 24.26/3.98 Prover 0: Proving ... % 73.24/10.35 Prover 2: stopped % 73.78/10.37 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 75.58/10.62 Prover 7: Preprocessing ... % 80.13/11.20 Prover 7: Warning: ignoring some quantifiers % 80.53/11.24 Prover 7: Constructing countermodel ... % 100.90/13.86 Prover 7: Found proof (size 16) % 100.90/13.86 Prover 7: proved (3492ms) % 100.90/13.86 Prover 5: stopped % 100.90/13.86 Prover 3: stopped % 100.90/13.86 Prover 0: stopped % 100.90/13.86 Prover 4: stopped % 100.90/13.87 Prover 6: stopped % 100.90/13.87 Prover 1: stopped % 100.90/13.87 % 100.90/13.87 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 100.90/13.87 % 100.90/13.87 % SZS output start Proof for theBenchmark % 101.14/13.88 Assumptions after simplification: % 101.14/13.88 --------------------------------- % 101.14/13.88 % 101.14/13.88 (id49) % 101.14/13.92 $i(0) & $i(nil) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 101.14/13.92 [v4: $i] : (v3 = v0 | ~ (cons(v3, v4) = v1) | ~ $i(v4) | ~ $i(v3) | ~ % 101.14/13.92 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ occ_succeeds(v0, v4, v2) | % 101.14/13.92 occ_succeeds(v0, v1, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 101.14/13.92 [v3: $i] : ! [v4: $i] : ( ~ (cons(v0, v3) = v1) | ~ (s(v4) = v2) | ~ $i(v4) % 101.14/13.92 | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ occ_succeeds(v0, v3, % 101.14/13.92 v4) | occ_succeeds(v0, v1, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 101.14/13.92 : (v2 = 0 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ occ_succeeds(v0, v1, v2) | % 101.14/13.92 ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: % 101.14/13.92 $i] : ? [v9: $i] : ($i(v8) & $i(v7) & $i(v4) & $i(v3) & ((v9 = v1 & ~ % 101.14/13.92 (v7 = v0) & cons(v7, v8) = v1 & occ_succeeds(v0, v8, v2)) | (v6 = v2 & % 101.14/13.92 v5 = v1 & cons(v0, v3) = v1 & s(v4) = v2 & occ_succeeds(v0, v3, % 101.14/13.92 v4))))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = nil | ~ % 101.14/13.92 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ occ_succeeds(v0, v1, v2) | ? [v3: $i] : % 101.14/13.92 ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? % 101.14/13.92 [v9: $i] : ($i(v8) & $i(v7) & $i(v4) & $i(v3) & ((v9 = v1 & ~ (v7 = v0) & % 101.14/13.92 cons(v7, v8) = v1 & occ_succeeds(v0, v8, v2)) | (v6 = v2 & v5 = v1 & % 101.14/13.92 cons(v0, v3) = v1 & s(v4) = v2 & occ_succeeds(v0, v3, v4))))) & ? % 101.14/13.92 [v0: $i] : ( ~ $i(v0) | occ_succeeds(v0, nil, 0)) % 101.14/13.92 % 101.14/13.92 (id73) % 101.14/13.92 $i(nil) & list_succeeds(nil) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 101.14/13.92 (cons(v1, v2) = v0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 101.14/13.92 list_succeeds(v2) | list_succeeds(v0)) & ! [v0: $i] : (v0 = nil | ~ $i(v0) % 101.14/13.92 | ~ list_succeeds(v0) | ? [v1: $i] : ? [v2: $i] : (cons(v1, v2) = v0 & % 101.14/13.92 $i(v2) & $i(v1) & list_succeeds(v2))) % 101.14/13.92 % 101.14/13.92 (lemma-(occ:cons:diff)) % 101.14/13.93 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 101.14/13.93 $i] : ( ~ (v5 = v4) & ~ (v1 = v0) & occ(v0, v3) = v4 & occ(v0, v2) = v5 & % 101.14/13.93 cons(v1, v2) = v3 & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & % 101.14/13.93 list_succeeds(v2)) % 101.14/13.93 % 101.14/13.93 (occ/2) % 101.14/13.93 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v2 | ~ (occ(v0, % 101.14/13.93 v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ list_succeeds(v1) | % 101.14/13.93 ~ occ_succeeds(v0, v1, v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 101.14/13.93 (occ(v0, v1) = v2) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 101.14/13.93 list_succeeds(v1) | occ_succeeds(v0, v1, v2)) % 101.14/13.93 % 101.14/13.93 Further assumptions not needed in the proof: % 101.14/13.93 -------------------------------------------- % 101.14/13.93 (**)/2, (@*)/2, (@+)/2, axiom-(app:associative), axiom-(app:cons), % 101.14/13.93 axiom-(app:ground:1), axiom-(app:ground:2), axiom-(app:lh), % 101.14/13.93 axiom-(app:lh:leq:first), axiom-(app:lh:leq:second), axiom-(app:member:1), % 101.14/13.93 axiom-(app:member:2), axiom-(app:member:3), axiom-(app:nil), % 101.14/13.93 axiom-(app:nil)_015, axiom-(app:types:1), axiom-(app:types:2), % 101.14/13.93 axiom-(app:uniqueness:1), axiom-(append:cons:different), % 101.14/13.93 axiom-(append:equal:nil), axiom-(append:existence), axiom-(append:ground:1), % 101.14/13.93 axiom-(append:ground:2), axiom-(append:lh), axiom-(append:lh:leq:first), % 101.14/13.93 axiom-(append:lh:leq:second), axiom-(append:member), axiom-(append:member:1), % 101.14/13.93 axiom-(append:member:2), axiom-(append:member:3), axiom-(append:termination:1), % 101.14/13.93 axiom-(append:termination:2), axiom-(append:types:1), axiom-(append:types:2), % 101.14/13.93 axiom-(append:types:3), axiom-(append:types:4), axiom-(append:uniqueness), % 101.14/13.93 axiom-(append:uniqueness:1), axiom-(append:uniqueness:2), axiom-(delete:app:1), % 101.14/13.93 axiom-(delete:app:2), axiom-(delete:ground), axiom-(delete:length), % 101.14/13.93 axiom-(delete:member:1), axiom-(delete:member:2), axiom-(delete:member:3), % 101.14/13.93 axiom-(delete:member:different), axiom-(delete:member:existence), % 101.14/13.93 axiom-(delete:nat_list), axiom-(delete:termination:1), % 101.14/13.93 axiom-(delete:termination:2), axiom-(delete:types:1), axiom-(delete:types:2), % 101.14/13.93 axiom-(length:existence), axiom-(length:ground), axiom-(length:termination), % 101.14/13.93 axiom-(length:types), axiom-(length:uniqueness), axiom-(leq:antisymmetric), % 101.14/13.93 axiom-(leq:failure), axiom-(leq:less), axiom-(leq:less:transitive), % 101.14/13.93 axiom-(leq:one:failure), axiom-(leq:one:success), axiom-(leq:plus), % 101.14/13.93 axiom-(leq:plus)_007, axiom-(leq:plus:first), axiom-(leq:plus:first)_011, % 101.14/13.93 axiom-(leq:plus:inverse), axiom-(leq:plus:second), axiom-(leq:plus:second)_012, % 101.14/13.93 axiom-(leq:reflexive), axiom-(leq:termination:1), axiom-(leq:times:inverse), % 101.14/13.93 axiom-(leq:totality), axiom-(leq:transitive), axiom-(leq:types), % 101.14/13.93 axiom-(less:axiom:successor), axiom-(less:different:zero), axiom-(less:failure), % 101.14/13.93 axiom-(less:leq), axiom-(less:leq:total), axiom-(less:leq:transitive), % 101.14/13.93 axiom-(less:one), axiom-(less:plus), axiom-(less:plus)_008, % 101.14/13.93 axiom-(less:plus:first), axiom-(less:plus:first)_010, axiom-(less:plus:inverse), % 101.14/13.93 axiom-(less:plus:inverse)_013, axiom-(less:plus:second), % 101.14/13.93 axiom-(less:plus:second)_009, axiom-(less:strictness), axiom-(less:successor), % 101.14/13.93 axiom-(less:termination:1), axiom-(less:termination:2), axiom-(less:totality), % 101.14/13.93 axiom-(less:transitive), axiom-(less:transitive:successor), axiom-(less:types), % 101.14/13.93 axiom-(less:weakening), axiom-(lh:cons), axiom-(lh:cons:first), % 101.14/13.93 axiom-(lh:cons:leq), axiom-(lh:cons:second), axiom-(lh:nil), % 101.14/13.93 axiom-(lh:successor), axiom-(lh:types), axiom-(lh:zero), axiom-(list:1), % 101.14/13.93 axiom-(list:2), axiom-(list:3), axiom-(list:cons), axiom-(list:termination), % 101.14/13.93 axiom-(member:append), axiom-(member:cons), axiom-(member:ground), % 101.14/13.93 axiom-(member:termination), axiom-(member:termination)_014, axiom-(nat:ground), % 101.14/13.93 axiom-(nat:termination), axiom-(nat_list:ground), axiom-(nat_list:list), % 101.14/13.93 axiom-(nat_list:termination), axiom-(plus:associative), % 101.14/13.93 axiom-(plus:commutative), axiom-(plus:existence), axiom-(plus:ground:1), % 101.14/13.93 axiom-(plus:ground:2), axiom-(plus:ground:3), axiom-(plus:injective:first), % 101.14/13.93 axiom-(plus:injective:second), axiom-(plus:leq:leq), axiom-(plus:leq:less), % 101.14/13.93 axiom-(plus:less:leq), axiom-(plus:less:less), axiom-(plus:successor), % 101.14/13.93 axiom-(plus:successor)_002, axiom-(plus:termination:1), % 101.14/13.93 axiom-(plus:termination:2), axiom-(plus:termination:3), % 101.14/13.93 axiom-(plus:times:distributive), axiom-(plus:times:distributive)_006, % 101.14/13.93 axiom-(plus:types), axiom-(plus:types:1), axiom-(plus:types:2), % 101.14/13.93 axiom-(plus:types:3), axiom-(plus:uniqueness), axiom-(plus:zero), % 101.14/13.93 axiom-(plus:zero)_001, axiom-(sub:app:1), axiom-(sub:app:2), axiom-(sub:cons), % 101.14/13.93 axiom-(sub:cons:both), axiom-(sub:member), axiom-(sub:nil), % 101.14/13.93 axiom-(sub:reflexive), axiom-(sub:transitive), axiom-(times:associative), % 101.14/13.93 axiom-(times:commutative), axiom-(times:existence), axiom-(times:ground:1), % 101.14/13.93 axiom-(times:ground:2), axiom-(times:leq:first), axiom-(times:leq:second), % 101.14/13.93 axiom-(times:less:second), axiom-(times:one), axiom-(times:one)_005, % 101.14/13.93 axiom-(times:successor), axiom-(times:successor)_004, axiom-(times:termination), % 101.14/13.93 axiom-(times:types), axiom-(times:types:1), axiom-(times:types:2), % 101.14/13.93 axiom-(times:uniqueness), axiom-(times:zero), axiom-(times:zero)_003, id1, id10, % 101.14/13.93 id11, id12, id13, id14, id15, id16, id17, id18, id19, id2, id20, id21, id22, % 101.14/13.93 id23, id24, id25, id26, id27, id28, id29, id3, id30, id31, id32, id33, id34, % 101.14/13.93 id35, id36, id37, id38, id39, id4, id40, id41, id42, id43, id44, id45, id46, % 101.14/13.93 id47, id48, id5, id50, id51, id52, id53, id54, id55, id56, id57, id58, id59, % 101.14/13.93 id6, id60, id61, id62, id63, id64, id65, id66, id67, id68, id69, id7, id70, % 101.14/13.93 id71, id72, id74, id75, id76, id77, id78, id79, id8, id80, id81, id82, id83, % 101.14/13.93 id84, id85, id86, id87, id88, id89, id9, id90, id91, id92, id93, induction, % 101.14/13.93 lemma-(member2:ground), lemma-(member2:termination), % 101.14/13.93 lemma-(not_same_occ:termination), lemma-(occ:existence), lemma-(occ:ground), % 101.14/13.93 lemma-(occ:nil), lemma-(occ:termination), lemma-(occ:types), % 101.14/13.93 lemma-(occ:uniqueness), lemma-(permutation:termination), % 101.14/13.93 lemma-(permutation:types), lh/1, sub/2, theorem-(permutation:termination), % 101.14/13.93 theorem-(same_occ:termination) % 101.14/13.93 % 101.14/13.93 Those formulas are unsatisfiable: % 101.14/13.93 --------------------------------- % 101.14/13.93 % 101.14/13.93 Begin of proof % 101.14/13.93 | % 101.14/13.93 | ALPHA: (id49) implies: % 101.14/13.93 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 101.14/13.93 | (v3 = v0 | ~ (cons(v3, v4) = v1) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | % 101.14/13.93 | ~ $i(v1) | ~ $i(v0) | ~ occ_succeeds(v0, v4, v2) | % 101.14/13.93 | occ_succeeds(v0, v1, v2)) % 101.14/13.93 | % 101.14/13.93 | ALPHA: (id73) implies: % 101.14/13.93 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (cons(v1, v2) = v0) | ~ % 101.14/13.93 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ list_succeeds(v2) | % 101.14/13.93 | list_succeeds(v0)) % 101.14/13.93 | % 101.14/13.93 | ALPHA: (occ/2) implies: % 101.40/13.94 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (occ(v0, v1) = v2) | ~ % 101.40/13.94 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ list_succeeds(v1) | % 101.40/13.94 | occ_succeeds(v0, v1, v2)) % 101.40/13.94 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v2 | ~ % 101.40/13.94 | (occ(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 101.40/13.94 | list_succeeds(v1) | ~ occ_succeeds(v0, v1, v2)) % 101.40/13.94 | % 101.40/13.94 | DELTA: instantiating (lemma-(occ:cons:diff)) with fresh symbols all_367_0, % 101.40/13.94 | all_367_1, all_367_2, all_367_3, all_367_4, all_367_5 gives: % 101.40/13.94 | (5) ~ (all_367_0 = all_367_1) & ~ (all_367_4 = all_367_5) & % 101.40/13.94 | occ(all_367_5, all_367_2) = all_367_1 & occ(all_367_5, all_367_3) = % 101.40/13.94 | all_367_0 & cons(all_367_4, all_367_3) = all_367_2 & $i(all_367_0) & % 101.40/13.94 | $i(all_367_1) & $i(all_367_2) & $i(all_367_3) & $i(all_367_4) & % 101.40/13.94 | $i(all_367_5) & list_succeeds(all_367_3) % 101.40/13.94 | % 101.40/13.94 | ALPHA: (5) implies: % 101.40/13.94 | (6) ~ (all_367_4 = all_367_5) % 101.40/13.94 | (7) ~ (all_367_0 = all_367_1) % 101.40/13.94 | (8) list_succeeds(all_367_3) % 101.40/13.94 | (9) $i(all_367_5) % 101.40/13.94 | (10) $i(all_367_4) % 101.40/13.94 | (11) $i(all_367_3) % 101.40/13.94 | (12) $i(all_367_2) % 101.40/13.94 | (13) $i(all_367_0) % 101.40/13.94 | (14) cons(all_367_4, all_367_3) = all_367_2 % 101.40/13.94 | (15) occ(all_367_5, all_367_3) = all_367_0 % 101.40/13.94 | (16) occ(all_367_5, all_367_2) = all_367_1 % 101.40/13.94 | % 101.40/13.94 | GROUND_INST: instantiating (2) with all_367_2, all_367_4, all_367_3, % 101.40/13.94 | simplifying with (8), (10), (11), (12), (14) gives: % 101.40/13.94 | (17) list_succeeds(all_367_2) % 101.40/13.94 | % 101.40/13.94 | GROUND_INST: instantiating (3) with all_367_5, all_367_3, all_367_0, % 101.40/13.94 | simplifying with (8), (9), (11), (13), (15) gives: % 101.40/13.94 | (18) occ_succeeds(all_367_5, all_367_3, all_367_0) % 101.40/13.94 | % 101.40/13.94 | GROUND_INST: instantiating (1) with all_367_5, all_367_2, all_367_0, % 101.40/13.94 | all_367_4, all_367_3, simplifying with (9), (10), (11), (12), % 101.40/13.94 | (13), (14), (18) gives: % 101.40/13.94 | (19) all_367_4 = all_367_5 | occ_succeeds(all_367_5, all_367_2, all_367_0) % 101.40/13.94 | % 101.40/13.94 | BETA: splitting (19) gives: % 101.40/13.94 | % 101.40/13.94 | Case 1: % 101.40/13.94 | | % 101.40/13.94 | | (20) occ_succeeds(all_367_5, all_367_2, all_367_0) % 101.40/13.94 | | % 101.40/13.94 | | GROUND_INST: instantiating (4) with all_367_5, all_367_2, all_367_0, % 101.40/13.94 | | all_367_1, simplifying with (9), (12), (13), (16), (17), (20) % 101.40/13.94 | | gives: % 101.40/13.94 | | (21) all_367_0 = all_367_1 % 101.40/13.94 | | % 101.40/13.94 | | REDUCE: (7), (21) imply: % 101.40/13.94 | | (22) $false % 101.40/13.94 | | % 101.40/13.94 | | CLOSE: (22) is inconsistent. % 101.40/13.94 | | % 101.40/13.94 | Case 2: % 101.40/13.95 | | % 101.40/13.95 | | (23) all_367_4 = all_367_5 % 101.40/13.95 | | % 101.40/13.95 | | REDUCE: (6), (23) imply: % 101.40/13.95 | | (24) $false % 101.40/13.95 | | % 101.40/13.95 | | CLOSE: (24) is inconsistent. % 101.40/13.95 | | % 101.40/13.95 | End of split % 101.40/13.95 | % 101.40/13.95 End of proof % 101.40/13.95 % SZS output end Proof for theBenchmark % 101.40/13.95 % 101.40/13.95 13295ms %------------------------------------------------------------------------------