%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SEU368+1 : TPTP v8.1.2. Released v3.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%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 : 300s % DateTime : Thu Aug 31 17:44:20 EDT 2023 % Result : Theorem 13.43s 2.51s % Output : Proof 16.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SEU368+1 : TPTP v8.1.2. Released v3.3.0. % 0.00/0.11 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.11/0.31 % Computer : n032.cluster.edu % 0.11/0.31 % Model : x86_64 x86_64 % 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.31 % Memory : 8042.1875MB % 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.31 % CPULimit : 300 % 0.11/0.31 % WCLimit : 300 % 0.11/0.31 % DateTime : Wed Aug 23 18:21:11 EDT 2023 % 0.11/0.31 % CPUTime : % 0.16/0.52 ________ _____ % 0.16/0.52 ___ __ \_________(_)________________________________ % 0.16/0.52 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.16/0.52 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.16/0.52 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.16/0.52 % 0.16/0.52 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.16/0.52 (2023-06-19) % 0.16/0.52 % 0.16/0.52 (c) Philipp Rümmer, 2009-2023 % 0.16/0.52 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.16/0.52 Amanda Stjerna. % 0.16/0.52 Free software under BSD-3-Clause. % 0.16/0.52 % 0.16/0.52 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.16/0.52 % 0.16/0.52 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.16/0.53 Running up to 7 provers in parallel. % 0.16/0.55 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.16/0.55 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.16/0.55 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.16/0.55 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.16/0.55 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.16/0.55 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.16/0.55 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.54/0.98 Prover 4: Preprocessing ... % 2.54/0.98 Prover 1: Preprocessing ... % 2.82/1.02 Prover 0: Preprocessing ... % 2.82/1.02 Prover 6: Preprocessing ... % 2.82/1.02 Prover 2: Preprocessing ... % 2.82/1.02 Prover 3: Preprocessing ... % 2.82/1.02 Prover 5: Preprocessing ... % 6.00/1.52 Prover 1: Warning: ignoring some quantifiers % 6.64/1.56 Prover 5: Proving ... % 6.83/1.58 Prover 1: Constructing countermodel ... % 6.83/1.61 Prover 6: Proving ... % 7.26/1.67 Prover 2: Proving ... % 7.26/1.70 Prover 3: Warning: ignoring some quantifiers % 7.26/1.71 Prover 4: Warning: ignoring some quantifiers % 7.82/1.74 Prover 3: Constructing countermodel ... % 8.22/1.80 Prover 4: Constructing countermodel ... % 8.22/1.84 Prover 0: Proving ... % 10.02/2.15 Prover 3: gave up % 10.02/2.15 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 11.12/2.21 Prover 7: Preprocessing ... % 11.63/2.29 Prover 1: gave up % 11.63/2.30 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 12.05/2.35 Prover 8: Preprocessing ... % 12.38/2.36 Prover 7: Warning: ignoring some quantifiers % 12.38/2.38 Prover 7: Constructing countermodel ... % 13.43/2.51 Prover 2: proved (1970ms) % 13.43/2.51 % 13.43/2.51 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.43/2.51 % 13.43/2.51 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 13.43/2.52 Prover 6: stopped % 13.43/2.52 Prover 5: stopped % 13.43/2.52 Prover 0: stopped % 13.43/2.52 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 13.43/2.52 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 13.43/2.52 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 13.43/2.52 Prover 8: Warning: ignoring some quantifiers % 13.85/2.55 Prover 8: Constructing countermodel ... % 13.93/2.57 Prover 10: Preprocessing ... % 13.93/2.57 Prover 13: Preprocessing ... % 13.93/2.58 Prover 11: Preprocessing ... % 13.93/2.60 Prover 16: Preprocessing ... % 14.30/2.66 Prover 10: Warning: ignoring some quantifiers % 14.30/2.70 Prover 13: Warning: ignoring some quantifiers % 14.30/2.71 Prover 10: Constructing countermodel ... % 14.30/2.72 Prover 16: Warning: ignoring some quantifiers % 14.30/2.73 Prover 13: Constructing countermodel ... % 14.30/2.73 Prover 16: Constructing countermodel ... % 14.30/2.79 Prover 7: Found proof (size 69) % 14.30/2.79 Prover 7: proved (646ms) % 14.30/2.79 Prover 13: stopped % 14.30/2.79 Prover 16: stopped % 14.30/2.79 Prover 8: stopped % 14.30/2.79 Prover 4: stopped % 14.30/2.79 Prover 10: stopped % 15.13/2.84 Prover 11: Warning: ignoring some quantifiers % 15.13/2.86 Prover 11: Constructing countermodel ... % 15.13/2.88 Prover 11: stopped % 15.13/2.88 % 15.13/2.88 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 15.13/2.88 % 16.05/2.89 % SZS output start Proof for theBenchmark % 16.05/2.90 Assumptions after simplification: % 16.05/2.90 --------------------------------- % 16.05/2.90 % 16.05/2.90 (abstractness_v1_orders_2) % 16.05/2.93 ! [v0: $i] : ! [v1: $i] : ( ~ (the_InternalRel(v0) = v1) | ~ $i(v0) | ~ % 16.05/2.93 strict_rel_str(v0) | ~ rel_str(v0) | ? [v2: $i] : (rel_str_of(v2, v1) = v0 % 16.05/2.93 & the_carrier(v0) = v2 & $i(v2))) & ! [v0: $i] : ! [v1: $i] : ( ~ % 16.05/2.93 (the_carrier(v0) = v1) | ~ $i(v0) | ~ strict_rel_str(v0) | ~ rel_str(v0) % 16.05/2.93 | ? [v2: $i] : (the_InternalRel(v0) = v2 & rel_str_of(v1, v2) = v0 & % 16.05/2.93 $i(v2))) % 16.05/2.93 % 16.05/2.93 (d1_yellow_1) % 16.05/2.94 ! [v0: $i] : ! [v1: $i] : ( ~ (inclusion_order(v0) = v1) | ~ $i(v0) | ? % 16.05/2.94 [v2: $i] : (rel_str_of(v0, v1) = v2 & incl_POSet(v0) = v2 & $i(v2))) & ! % 16.05/2.94 [v0: $i] : ! [v1: $i] : ( ~ (incl_POSet(v0) = v1) | ~ $i(v0) | ? [v2: $i] : % 16.05/2.94 (inclusion_order(v0) = v2 & rel_str_of(v0, v2) = v1 & $i(v2) & $i(v1))) % 16.05/2.94 % 16.05/2.94 (dt_k1_yellow_1) % 16.27/2.94 ! [v0: $i] : ! [v1: $i] : ( ~ (inclusion_order(v0) = v1) | ~ $i(v0) | % 16.27/2.94 relation_of2_as_subset(v1, v0, v0)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 16.27/2.94 (inclusion_order(v0) = v1) | ~ $i(v0) | v1_partfun1(v1, v0, v0)) & ! [v0: % 16.27/2.94 $i] : ! [v1: $i] : ( ~ (inclusion_order(v0) = v1) | ~ $i(v0) | % 16.27/2.94 transitive(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ (inclusion_order(v0) = v1) % 16.27/2.94 | ~ $i(v0) | antisymmetric(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 16.27/2.94 (inclusion_order(v0) = v1) | ~ $i(v0) | reflexive(v1)) % 16.27/2.94 % 16.27/2.94 (dt_k2_yellow_1) % 16.27/2.94 ! [v0: $i] : ! [v1: $i] : ( ~ (incl_POSet(v0) = v1) | ~ $i(v0) | % 16.27/2.94 strict_rel_str(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ (incl_POSet(v0) = v1) % 16.27/2.94 | ~ $i(v0) | rel_str(v1)) % 16.27/2.94 % 16.27/2.94 (dt_u1_orders_2) % 16.30/2.95 ! [v0: $i] : ! [v1: $i] : ( ~ (the_InternalRel(v0) = v1) | ~ $i(v0) | ~ % 16.30/2.95 rel_str(v0) | ? [v2: $i] : (the_carrier(v0) = v2 & $i(v2) & % 16.30/2.95 relation_of2_as_subset(v1, v2, v2))) & ! [v0: $i] : ! [v1: $i] : ( ~ % 16.30/2.95 (the_carrier(v0) = v1) | ~ $i(v0) | ~ rel_str(v0) | ? [v2: $i] : % 16.30/2.95 (the_InternalRel(v0) = v2 & $i(v2) & relation_of2_as_subset(v2, v1, v1))) % 16.30/2.95 % 16.30/2.95 (fc2_orders_2) % 16.30/2.95 ! [v0: $i] : ! [v1: $i] : ( ~ (the_InternalRel(v0) = v1) | ~ $i(v0) | ~ % 16.30/2.95 antisymmetric_relstr(v0) | ~ transitive_relstr(v0) | ~ % 16.30/2.95 reflexive_relstr(v0) | ~ rel_str(v0) | relation(v1)) & ! [v0: $i] : ! % 16.30/2.95 [v1: $i] : ( ~ (the_InternalRel(v0) = v1) | ~ $i(v0) | ~ % 16.30/2.95 antisymmetric_relstr(v0) | ~ transitive_relstr(v0) | ~ % 16.30/2.95 reflexive_relstr(v0) | ~ rel_str(v0) | transitive(v1)) & ! [v0: $i] : ! % 16.30/2.95 [v1: $i] : ( ~ (the_InternalRel(v0) = v1) | ~ $i(v0) | ~ % 16.30/2.95 antisymmetric_relstr(v0) | ~ transitive_relstr(v0) | ~ % 16.30/2.95 reflexive_relstr(v0) | ~ rel_str(v0) | antisymmetric(v1)) & ! [v0: $i] : % 16.30/2.95 ! [v1: $i] : ( ~ (the_InternalRel(v0) = v1) | ~ $i(v0) | ~ % 16.30/2.95 antisymmetric_relstr(v0) | ~ transitive_relstr(v0) | ~ % 16.30/2.95 reflexive_relstr(v0) | ~ rel_str(v0) | reflexive(v1)) & ! [v0: $i] : ! % 16.30/2.95 [v1: $i] : ( ~ (the_InternalRel(v0) = v1) | ~ $i(v0) | ~ % 16.30/2.95 antisymmetric_relstr(v0) | ~ transitive_relstr(v0) | ~ % 16.30/2.95 reflexive_relstr(v0) | ~ rel_str(v0) | ? [v2: $i] : (the_carrier(v0) = v2 % 16.30/2.95 & $i(v2) & v1_partfun1(v1, v2, v2))) & ! [v0: $i] : ! [v1: $i] : ( ~ % 16.30/2.95 (the_carrier(v0) = v1) | ~ $i(v0) | ~ antisymmetric_relstr(v0) | ~ % 16.30/2.95 transitive_relstr(v0) | ~ reflexive_relstr(v0) | ~ rel_str(v0) | ? [v2: % 16.30/2.95 $i] : (the_InternalRel(v0) = v2 & $i(v2) & relation(v2) & v1_partfun1(v2, % 16.30/2.95 v1, v1) & transitive(v2) & antisymmetric(v2) & reflexive(v2))) % 16.30/2.95 % 16.30/2.95 (fc5_yellow_1) % 16.30/2.95 ! [v0: $i] : ! [v1: $i] : ( ~ (incl_POSet(v0) = v1) | ~ $i(v0) | % 16.30/2.95 antisymmetric_relstr(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ (incl_POSet(v0) % 16.30/2.95 = v1) | ~ $i(v0) | transitive_relstr(v1)) & ! [v0: $i] : ! [v1: $i] : ( % 16.30/2.95 ~ (incl_POSet(v0) = v1) | ~ $i(v0) | reflexive_relstr(v1)) & ! [v0: $i] : % 16.30/2.95 ! [v1: $i] : ( ~ (incl_POSet(v0) = v1) | ~ $i(v0) | strict_rel_str(v1)) % 16.30/2.95 % 16.30/2.95 (free_g1_orders_2) % 16.30/2.96 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v4 = v1 % 16.30/2.96 | ~ (rel_str_of(v3, v4) = v2) | ~ (rel_str_of(v0, v1) = v2) | ~ $i(v4) | % 16.30/2.96 ~ $i(v3) | ~ $i(v1) | ~ $i(v0) | ~ relation_of2(v1, v0, v0)) & ! [v0: % 16.30/2.96 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v3 = v0 | ~ % 16.30/2.96 (rel_str_of(v3, v4) = v2) | ~ (rel_str_of(v0, v1) = v2) | ~ $i(v4) | ~ % 16.30/2.96 $i(v3) | ~ $i(v1) | ~ $i(v0) | ~ relation_of2(v1, v0, v0)) % 16.30/2.96 % 16.30/2.96 (redefinition_k1_yellow_1) % 16.30/2.96 ! [v0: $i] : ! [v1: $i] : ( ~ (inclusion_order(v0) = v1) | ~ $i(v0) | % 16.30/2.96 (inclusion_relation(v0) = v1 & $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ % 16.30/2.96 (inclusion_relation(v0) = v1) | ~ $i(v0) | (inclusion_order(v0) = v1 & % 16.30/2.96 $i(v1))) % 16.30/2.96 % 16.30/2.96 (redefinition_m2_relset_1) % 16.30/2.96 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 16.30/2.96 ~ relation_of2_as_subset(v2, v0, v1) | relation_of2(v2, v0, v1)) & ! [v0: % 16.30/2.96 $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 16.30/2.96 relation_of2(v2, v0, v1) | relation_of2_as_subset(v2, v0, v1)) % 16.30/2.96 % 16.30/2.96 (t1_yellow_1) % 16.30/2.96 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 16.30/2.96 (incl_POSet(v0) = v1 & $i(v1) & $i(v0) & (( ~ (v4 = v3) & inclusion_order(v0) % 16.30/2.96 = v4 & the_InternalRel(v1) = v3 & $i(v4) & $i(v3)) | ( ~ (v2 = v0) & % 16.30/2.96 the_carrier(v1) = v2 & $i(v2)))) % 16.30/2.96 % 16.30/2.96 (function-axioms) % 16.30/2.96 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 16.30/2.96 (cartesian_product2(v3, v2) = v1) | ~ (cartesian_product2(v3, v2) = v0)) & % 16.30/2.96 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 16.30/2.96 (rel_str_of(v3, v2) = v1) | ~ (rel_str_of(v3, v2) = v0)) & ! [v0: $i] : ! % 16.30/2.96 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (inclusion_order(v2) = v1) | ~ % 16.30/2.96 (inclusion_order(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 % 16.30/2.96 = v0 | ~ (inclusion_relation(v2) = v1) | ~ (inclusion_relation(v2) = v0)) % 16.30/2.96 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (the_InternalRel(v2) % 16.30/2.96 = v1) | ~ (the_InternalRel(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 16.30/2.96 [v2: $i] : (v1 = v0 | ~ (incl_POSet(v2) = v1) | ~ (incl_POSet(v2) = v0)) & % 16.30/2.96 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (powerset(v2) = v1) | % 16.30/2.96 ~ (powerset(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 16.30/2.96 | ~ (the_carrier(v2) = v1) | ~ (the_carrier(v2) = v0)) % 16.30/2.96 % 16.30/2.96 Further assumptions not needed in the proof: % 16.30/2.96 -------------------------------------------- % 16.30/2.96 antisymmetry_r2_hidden, cc1_relset_1, dt_g1_orders_2, dt_k1_wellord2, % 16.30/2.96 dt_k1_xboole_0, dt_k1_zfmisc_1, dt_k2_zfmisc_1, dt_l1_orders_2, dt_l1_struct_0, % 16.30/2.96 dt_m1_relset_1, dt_m1_subset_1, dt_m2_relset_1, dt_u1_struct_0, % 16.30/2.96 existence_l1_orders_2, existence_l1_struct_0, existence_m1_relset_1, % 16.30/2.96 existence_m1_subset_1, existence_m2_relset_1, fc1_orders_2, fc1_struct_0, % 16.30/2.96 fc1_subset_1, fc1_xboole_0, fc3_orders_2, fc4_subset_1, fc6_yellow_1, % 16.30/2.96 rc1_orders_2, rc1_subset_1, rc1_xboole_0, rc2_orders_2, rc2_subset_1, % 16.30/2.96 rc2_xboole_0, rc3_struct_0, rc5_struct_0, reflexivity_r1_tarski, t1_subset, % 16.30/2.96 t2_subset, t3_subset, t4_subset, t5_subset, t6_boole, t7_boole, t8_boole % 16.30/2.96 % 16.30/2.96 Those formulas are unsatisfiable: % 16.30/2.96 --------------------------------- % 16.30/2.96 % 16.30/2.96 Begin of proof % 16.30/2.97 | % 16.30/2.97 | ALPHA: (free_g1_orders_2) implies: % 16.30/2.97 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 16.30/2.97 | (v3 = v0 | ~ (rel_str_of(v3, v4) = v2) | ~ (rel_str_of(v0, v1) = v2) % 16.30/2.97 | | ~ $i(v4) | ~ $i(v3) | ~ $i(v1) | ~ $i(v0) | ~ relation_of2(v1, % 16.30/2.97 | v0, v0)) % 16.30/2.97 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 16.30/2.97 | (v4 = v1 | ~ (rel_str_of(v3, v4) = v2) | ~ (rel_str_of(v0, v1) = v2) % 16.30/2.97 | | ~ $i(v4) | ~ $i(v3) | ~ $i(v1) | ~ $i(v0) | ~ relation_of2(v1, % 16.30/2.97 | v0, v0)) % 16.30/2.97 | % 16.30/2.97 | ALPHA: (abstractness_v1_orders_2) implies: % 16.30/2.97 | (3) ! [v0: $i] : ! [v1: $i] : ( ~ (the_carrier(v0) = v1) | ~ $i(v0) | ~ % 16.30/2.97 | strict_rel_str(v0) | ~ rel_str(v0) | ? [v2: $i] : % 16.30/2.97 | (the_InternalRel(v0) = v2 & rel_str_of(v1, v2) = v0 & $i(v2))) % 16.30/2.97 | (4) ! [v0: $i] : ! [v1: $i] : ( ~ (the_InternalRel(v0) = v1) | ~ $i(v0) % 16.30/2.97 | | ~ strict_rel_str(v0) | ~ rel_str(v0) | ? [v2: $i] : % 16.30/2.97 | (rel_str_of(v2, v1) = v0 & the_carrier(v0) = v2 & $i(v2))) % 16.30/2.97 | % 16.30/2.97 | ALPHA: (redefinition_m2_relset_1) implies: % 16.30/2.97 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 16.30/2.97 | $i(v0) | ~ relation_of2_as_subset(v2, v0, v1) | relation_of2(v2, v0, % 16.30/2.97 | v1)) % 16.30/2.97 | % 16.30/2.97 | ALPHA: (fc2_orders_2) implies: % 16.30/2.97 | (6) ! [v0: $i] : ! [v1: $i] : ( ~ (the_carrier(v0) = v1) | ~ $i(v0) | ~ % 16.30/2.97 | antisymmetric_relstr(v0) | ~ transitive_relstr(v0) | ~ % 16.30/2.97 | reflexive_relstr(v0) | ~ rel_str(v0) | ? [v2: $i] : % 16.30/2.97 | (the_InternalRel(v0) = v2 & $i(v2) & relation(v2) & v1_partfun1(v2, % 16.30/2.97 | v1, v1) & transitive(v2) & antisymmetric(v2) & reflexive(v2))) % 16.30/2.97 | (7) ! [v0: $i] : ! [v1: $i] : ( ~ (the_InternalRel(v0) = v1) | ~ $i(v0) % 16.30/2.97 | | ~ antisymmetric_relstr(v0) | ~ transitive_relstr(v0) | ~ % 16.30/2.97 | reflexive_relstr(v0) | ~ rel_str(v0) | ? [v2: $i] : % 16.30/2.97 | (the_carrier(v0) = v2 & $i(v2) & v1_partfun1(v1, v2, v2))) % 16.30/2.97 | % 16.30/2.97 | ALPHA: (redefinition_k1_yellow_1) implies: % 16.30/2.98 | (8) ! [v0: $i] : ! [v1: $i] : ( ~ (inclusion_order(v0) = v1) | ~ $i(v0) % 16.30/2.98 | | (inclusion_relation(v0) = v1 & $i(v1))) % 16.30/2.98 | % 16.30/2.98 | ALPHA: (dt_k1_yellow_1) implies: % 16.30/2.98 | (9) ! [v0: $i] : ! [v1: $i] : ( ~ (inclusion_order(v0) = v1) | ~ $i(v0) % 16.30/2.98 | | relation_of2_as_subset(v1, v0, v0)) % 16.30/2.98 | % 16.30/2.98 | ALPHA: (dt_k2_yellow_1) implies: % 16.30/2.98 | (10) ! [v0: $i] : ! [v1: $i] : ( ~ (incl_POSet(v0) = v1) | ~ $i(v0) | % 16.30/2.98 | rel_str(v1)) % 16.30/2.98 | % 16.30/2.98 | ALPHA: (dt_u1_orders_2) implies: % 16.30/2.98 | (11) ! [v0: $i] : ! [v1: $i] : ( ~ (the_carrier(v0) = v1) | ~ $i(v0) | % 16.30/2.98 | ~ rel_str(v0) | ? [v2: $i] : (the_InternalRel(v0) = v2 & $i(v2) & % 16.30/2.98 | relation_of2_as_subset(v2, v1, v1))) % 16.30/2.98 | (12) ! [v0: $i] : ! [v1: $i] : ( ~ (the_InternalRel(v0) = v1) | ~ $i(v0) % 16.30/2.98 | | ~ rel_str(v0) | ? [v2: $i] : (the_carrier(v0) = v2 & $i(v2) & % 16.30/2.98 | relation_of2_as_subset(v1, v2, v2))) % 16.30/2.98 | % 16.30/2.98 | ALPHA: (fc5_yellow_1) implies: % 16.30/2.98 | (13) ! [v0: $i] : ! [v1: $i] : ( ~ (incl_POSet(v0) = v1) | ~ $i(v0) | % 16.30/2.98 | strict_rel_str(v1)) % 16.30/2.98 | (14) ! [v0: $i] : ! [v1: $i] : ( ~ (incl_POSet(v0) = v1) | ~ $i(v0) | % 16.30/2.98 | reflexive_relstr(v1)) % 16.30/2.98 | (15) ! [v0: $i] : ! [v1: $i] : ( ~ (incl_POSet(v0) = v1) | ~ $i(v0) | % 16.30/2.98 | transitive_relstr(v1)) % 16.30/2.98 | (16) ! [v0: $i] : ! [v1: $i] : ( ~ (incl_POSet(v0) = v1) | ~ $i(v0) | % 16.30/2.98 | antisymmetric_relstr(v1)) % 16.30/2.98 | % 16.30/2.98 | ALPHA: (d1_yellow_1) implies: % 16.30/2.98 | (17) ! [v0: $i] : ! [v1: $i] : ( ~ (incl_POSet(v0) = v1) | ~ $i(v0) | ? % 16.30/2.98 | [v2: $i] : (inclusion_order(v0) = v2 & rel_str_of(v0, v2) = v1 & % 16.30/2.98 | $i(v2) & $i(v1))) % 16.30/2.98 | % 16.30/2.98 | ALPHA: (function-axioms) implies: % 16.30/2.98 | (18) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 16.30/2.98 | (the_carrier(v2) = v1) | ~ (the_carrier(v2) = v0)) % 16.30/2.98 | (19) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 16.30/2.98 | (the_InternalRel(v2) = v1) | ~ (the_InternalRel(v2) = v0)) % 16.30/2.98 | (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 16.30/2.98 | (inclusion_order(v2) = v1) | ~ (inclusion_order(v2) = v0)) % 16.30/2.98 | % 16.30/2.98 | DELTA: instantiating (t1_yellow_1) with fresh symbols all_55_0, all_55_1, % 16.30/2.98 | all_55_2, all_55_3, all_55_4 gives: % 16.30/2.99 | (21) incl_POSet(all_55_4) = all_55_3 & $i(all_55_3) & $i(all_55_4) & (( ~ % 16.30/2.99 | (all_55_0 = all_55_1) & inclusion_order(all_55_4) = all_55_0 & % 16.30/2.99 | the_InternalRel(all_55_3) = all_55_1 & $i(all_55_0) & % 16.30/2.99 | $i(all_55_1)) | ( ~ (all_55_2 = all_55_4) & the_carrier(all_55_3) % 16.30/2.99 | = all_55_2 & $i(all_55_2))) % 16.30/2.99 | % 16.30/2.99 | ALPHA: (21) implies: % 16.30/2.99 | (22) $i(all_55_4) % 16.30/2.99 | (23) incl_POSet(all_55_4) = all_55_3 % 16.30/2.99 | (24) ( ~ (all_55_0 = all_55_1) & inclusion_order(all_55_4) = all_55_0 & % 16.30/2.99 | the_InternalRel(all_55_3) = all_55_1 & $i(all_55_0) & $i(all_55_1)) % 16.30/2.99 | | ( ~ (all_55_2 = all_55_4) & the_carrier(all_55_3) = all_55_2 & % 16.30/2.99 | $i(all_55_2)) % 16.30/2.99 | % 16.30/2.99 | GROUND_INST: instantiating (16) with all_55_4, all_55_3, simplifying with % 16.30/2.99 | (22), (23) gives: % 16.30/2.99 | (25) antisymmetric_relstr(all_55_3) % 16.30/2.99 | % 16.30/2.99 | GROUND_INST: instantiating (15) with all_55_4, all_55_3, simplifying with % 16.30/2.99 | (22), (23) gives: % 16.30/2.99 | (26) transitive_relstr(all_55_3) % 16.30/2.99 | % 16.30/2.99 | GROUND_INST: instantiating (14) with all_55_4, all_55_3, simplifying with % 16.30/2.99 | (22), (23) gives: % 16.30/2.99 | (27) reflexive_relstr(all_55_3) % 16.30/2.99 | % 16.30/2.99 | GROUND_INST: instantiating (13) with all_55_4, all_55_3, simplifying with % 16.30/2.99 | (22), (23) gives: % 16.30/2.99 | (28) strict_rel_str(all_55_3) % 16.30/2.99 | % 16.30/2.99 | GROUND_INST: instantiating (10) with all_55_4, all_55_3, simplifying with % 16.30/2.99 | (22), (23) gives: % 16.30/2.99 | (29) rel_str(all_55_3) % 16.30/2.99 | % 16.30/2.99 | GROUND_INST: instantiating (17) with all_55_4, all_55_3, simplifying with % 16.30/2.99 | (22), (23) gives: % 16.30/2.99 | (30) ? [v0: $i] : (inclusion_order(all_55_4) = v0 & rel_str_of(all_55_4, % 16.30/2.99 | v0) = all_55_3 & $i(v0) & $i(all_55_3)) % 16.30/2.99 | % 16.30/2.99 | DELTA: instantiating (30) with fresh symbol all_67_0 gives: % 16.30/2.99 | (31) inclusion_order(all_55_4) = all_67_0 & rel_str_of(all_55_4, all_67_0) % 16.30/2.99 | = all_55_3 & $i(all_67_0) & $i(all_55_3) % 16.30/2.99 | % 16.30/2.99 | ALPHA: (31) implies: % 16.30/2.99 | (32) $i(all_55_3) % 16.30/2.99 | (33) rel_str_of(all_55_4, all_67_0) = all_55_3 % 16.30/2.99 | (34) inclusion_order(all_55_4) = all_67_0 % 16.30/2.99 | % 16.30/2.99 | GROUND_INST: instantiating (9) with all_55_4, all_67_0, simplifying with (22), % 16.30/2.99 | (34) gives: % 16.30/2.99 | (35) relation_of2_as_subset(all_67_0, all_55_4, all_55_4) % 16.30/2.99 | % 16.30/2.99 | GROUND_INST: instantiating (8) with all_55_4, all_67_0, simplifying with (22), % 16.30/2.99 | (34) gives: % 16.30/2.99 | (36) inclusion_relation(all_55_4) = all_67_0 & $i(all_67_0) % 16.30/2.99 | % 16.30/2.99 | ALPHA: (36) implies: % 16.30/2.99 | (37) $i(all_67_0) % 16.30/2.99 | % 16.30/2.99 | GROUND_INST: instantiating (5) with all_55_4, all_55_4, all_67_0, simplifying % 16.30/2.99 | with (22), (35), (37) gives: % 16.30/2.99 | (38) relation_of2(all_67_0, all_55_4, all_55_4) % 16.30/2.99 | % 16.30/2.99 | BETA: splitting (24) gives: % 16.30/2.99 | % 16.30/2.99 | Case 1: % 16.30/2.99 | | % 16.30/2.99 | | (39) ~ (all_55_0 = all_55_1) & inclusion_order(all_55_4) = all_55_0 & % 16.30/2.99 | | the_InternalRel(all_55_3) = all_55_1 & $i(all_55_0) & $i(all_55_1) % 16.30/2.99 | | % 16.30/2.99 | | ALPHA: (39) implies: % 16.30/3.00 | | (40) ~ (all_55_0 = all_55_1) % 16.30/3.00 | | (41) $i(all_55_1) % 16.30/3.00 | | (42) the_InternalRel(all_55_3) = all_55_1 % 16.30/3.00 | | (43) inclusion_order(all_55_4) = all_55_0 % 16.30/3.00 | | % 16.30/3.00 | | GROUND_INST: instantiating (20) with all_67_0, all_55_0, all_55_4, % 16.30/3.00 | | simplifying with (34), (43) gives: % 16.30/3.00 | | (44) all_67_0 = all_55_0 % 16.30/3.00 | | % 16.30/3.00 | | REDUCE: (33), (44) imply: % 16.30/3.00 | | (45) rel_str_of(all_55_4, all_55_0) = all_55_3 % 16.30/3.00 | | % 16.30/3.00 | | REDUCE: (37), (44) imply: % 16.30/3.00 | | (46) $i(all_55_0) % 16.30/3.00 | | % 16.30/3.00 | | REDUCE: (38), (44) imply: % 16.30/3.00 | | (47) relation_of2(all_55_0, all_55_4, all_55_4) % 16.30/3.00 | | % 16.30/3.00 | | GROUND_INST: instantiating (7) with all_55_3, all_55_1, simplifying with % 16.30/3.00 | | (25), (26), (27), (29), (32), (42) gives: % 16.30/3.00 | | (48) ? [v0: $i] : (the_carrier(all_55_3) = v0 & $i(v0) & % 16.30/3.00 | | v1_partfun1(all_55_1, v0, v0)) % 16.30/3.00 | | % 16.30/3.00 | | GROUND_INST: instantiating (4) with all_55_3, all_55_1, simplifying with % 16.30/3.00 | | (28), (29), (32), (42) gives: % 16.30/3.00 | | (49) ? [v0: $i] : (rel_str_of(v0, all_55_1) = all_55_3 & % 16.30/3.00 | | the_carrier(all_55_3) = v0 & $i(v0)) % 16.30/3.00 | | % 16.30/3.00 | | GROUND_INST: instantiating (12) with all_55_3, all_55_1, simplifying with % 16.30/3.00 | | (29), (32), (42) gives: % 16.30/3.00 | | (50) ? [v0: $i] : (the_carrier(all_55_3) = v0 & $i(v0) & % 16.30/3.00 | | relation_of2_as_subset(all_55_1, v0, v0)) % 16.30/3.00 | | % 16.30/3.00 | | DELTA: instantiating (50) with fresh symbol all_142_0 gives: % 16.30/3.00 | | (51) the_carrier(all_55_3) = all_142_0 & $i(all_142_0) & % 16.30/3.00 | | relation_of2_as_subset(all_55_1, all_142_0, all_142_0) % 16.30/3.00 | | % 16.30/3.00 | | ALPHA: (51) implies: % 16.30/3.00 | | (52) the_carrier(all_55_3) = all_142_0 % 16.30/3.00 | | % 16.30/3.00 | | DELTA: instantiating (49) with fresh symbol all_144_0 gives: % 16.30/3.00 | | (53) rel_str_of(all_144_0, all_55_1) = all_55_3 & the_carrier(all_55_3) = % 16.30/3.00 | | all_144_0 & $i(all_144_0) % 16.30/3.00 | | % 16.30/3.00 | | ALPHA: (53) implies: % 16.30/3.00 | | (54) $i(all_144_0) % 16.30/3.00 | | (55) the_carrier(all_55_3) = all_144_0 % 16.30/3.00 | | (56) rel_str_of(all_144_0, all_55_1) = all_55_3 % 16.30/3.00 | | % 16.30/3.00 | | DELTA: instantiating (48) with fresh symbol all_146_0 gives: % 16.30/3.00 | | (57) the_carrier(all_55_3) = all_146_0 & $i(all_146_0) & % 16.30/3.00 | | v1_partfun1(all_55_1, all_146_0, all_146_0) % 16.30/3.00 | | % 16.30/3.00 | | ALPHA: (57) implies: % 16.30/3.00 | | (58) the_carrier(all_55_3) = all_146_0 % 16.30/3.00 | | % 16.30/3.00 | | GROUND_INST: instantiating (18) with all_144_0, all_146_0, all_55_3, % 16.30/3.00 | | simplifying with (55), (58) gives: % 16.30/3.00 | | (59) all_146_0 = all_144_0 % 16.30/3.00 | | % 16.30/3.00 | | GROUND_INST: instantiating (18) with all_142_0, all_146_0, all_55_3, % 16.30/3.00 | | simplifying with (52), (58) gives: % 16.30/3.00 | | (60) all_146_0 = all_142_0 % 16.30/3.00 | | % 16.30/3.00 | | COMBINE_EQS: (59), (60) imply: % 16.30/3.00 | | (61) all_144_0 = all_142_0 % 16.30/3.00 | | % 16.30/3.00 | | SIMP: (61) implies: % 16.30/3.00 | | (62) all_144_0 = all_142_0 % 16.30/3.00 | | % 16.30/3.00 | | REDUCE: (56), (62) imply: % 16.30/3.00 | | (63) rel_str_of(all_142_0, all_55_1) = all_55_3 % 16.30/3.00 | | % 16.30/3.00 | | REDUCE: (54), (62) imply: % 16.30/3.00 | | (64) $i(all_142_0) % 16.30/3.00 | | % 16.30/3.00 | | GROUND_INST: instantiating (2) with all_55_4, all_55_0, all_55_3, all_142_0, % 16.30/3.00 | | all_55_1, simplifying with (22), (41), (45), (46), (47), (63), % 16.59/3.00 | | (64) gives: % 16.59/3.00 | | (65) all_55_0 = all_55_1 % 16.59/3.00 | | % 16.59/3.00 | | REDUCE: (40), (65) imply: % 16.59/3.00 | | (66) $false % 16.59/3.00 | | % 16.59/3.00 | | CLOSE: (66) is inconsistent. % 16.59/3.00 | | % 16.59/3.01 | Case 2: % 16.59/3.01 | | % 16.59/3.01 | | (67) ~ (all_55_2 = all_55_4) & the_carrier(all_55_3) = all_55_2 & % 16.59/3.01 | | $i(all_55_2) % 16.59/3.01 | | % 16.59/3.01 | | ALPHA: (67) implies: % 16.59/3.01 | | (68) ~ (all_55_2 = all_55_4) % 16.59/3.01 | | (69) $i(all_55_2) % 16.59/3.01 | | (70) the_carrier(all_55_3) = all_55_2 % 16.59/3.01 | | % 16.59/3.01 | | GROUND_INST: instantiating (6) with all_55_3, all_55_2, simplifying with % 16.59/3.01 | | (25), (26), (27), (29), (32), (70) gives: % 16.59/3.01 | | (71) ? [v0: $i] : (the_InternalRel(all_55_3) = v0 & $i(v0) & % 16.59/3.01 | | relation(v0) & v1_partfun1(v0, all_55_2, all_55_2) & % 16.59/3.01 | | transitive(v0) & antisymmetric(v0) & reflexive(v0)) % 16.59/3.01 | | % 16.59/3.01 | | GROUND_INST: instantiating (3) with all_55_3, all_55_2, simplifying with % 16.59/3.01 | | (28), (29), (32), (70) gives: % 16.59/3.01 | | (72) ? [v0: $i] : (the_InternalRel(all_55_3) = v0 & rel_str_of(all_55_2, % 16.59/3.01 | | v0) = all_55_3 & $i(v0)) % 16.59/3.01 | | % 16.59/3.01 | | GROUND_INST: instantiating (11) with all_55_3, all_55_2, simplifying with % 16.59/3.01 | | (29), (32), (70) gives: % 16.59/3.01 | | (73) ? [v0: $i] : (the_InternalRel(all_55_3) = v0 & $i(v0) & % 16.59/3.01 | | relation_of2_as_subset(v0, all_55_2, all_55_2)) % 16.59/3.01 | | % 16.59/3.01 | | DELTA: instantiating (73) with fresh symbol all_141_0 gives: % 16.59/3.01 | | (74) the_InternalRel(all_55_3) = all_141_0 & $i(all_141_0) & % 16.59/3.01 | | relation_of2_as_subset(all_141_0, all_55_2, all_55_2) % 16.59/3.01 | | % 16.59/3.01 | | ALPHA: (74) implies: % 16.59/3.01 | | (75) the_InternalRel(all_55_3) = all_141_0 % 16.59/3.01 | | % 16.59/3.01 | | DELTA: instantiating (72) with fresh symbol all_143_0 gives: % 16.59/3.01 | | (76) the_InternalRel(all_55_3) = all_143_0 & rel_str_of(all_55_2, % 16.59/3.01 | | all_143_0) = all_55_3 & $i(all_143_0) % 16.59/3.01 | | % 16.59/3.01 | | ALPHA: (76) implies: % 16.59/3.01 | | (77) $i(all_143_0) % 16.59/3.01 | | (78) rel_str_of(all_55_2, all_143_0) = all_55_3 % 16.59/3.01 | | (79) the_InternalRel(all_55_3) = all_143_0 % 16.59/3.01 | | % 16.59/3.01 | | DELTA: instantiating (71) with fresh symbol all_145_0 gives: % 16.59/3.01 | | (80) the_InternalRel(all_55_3) = all_145_0 & $i(all_145_0) & % 16.59/3.01 | | relation(all_145_0) & v1_partfun1(all_145_0, all_55_2, all_55_2) & % 16.59/3.01 | | transitive(all_145_0) & antisymmetric(all_145_0) & % 16.59/3.01 | | reflexive(all_145_0) % 16.59/3.01 | | % 16.59/3.01 | | ALPHA: (80) implies: % 16.59/3.01 | | (81) the_InternalRel(all_55_3) = all_145_0 % 16.59/3.01 | | % 16.59/3.01 | | GROUND_INST: instantiating (19) with all_143_0, all_145_0, all_55_3, % 16.59/3.01 | | simplifying with (79), (81) gives: % 16.59/3.01 | | (82) all_145_0 = all_143_0 % 16.59/3.01 | | % 16.59/3.01 | | GROUND_INST: instantiating (19) with all_141_0, all_145_0, all_55_3, % 16.59/3.01 | | simplifying with (75), (81) gives: % 16.59/3.01 | | (83) all_145_0 = all_141_0 % 16.59/3.01 | | % 16.59/3.01 | | COMBINE_EQS: (82), (83) imply: % 16.59/3.01 | | (84) all_143_0 = all_141_0 % 16.59/3.01 | | % 16.59/3.01 | | SIMP: (84) implies: % 16.59/3.01 | | (85) all_143_0 = all_141_0 % 16.59/3.01 | | % 16.59/3.01 | | REDUCE: (78), (85) imply: % 16.59/3.01 | | (86) rel_str_of(all_55_2, all_141_0) = all_55_3 % 16.59/3.01 | | % 16.59/3.01 | | REDUCE: (77), (85) imply: % 16.59/3.01 | | (87) $i(all_141_0) % 16.59/3.01 | | % 16.59/3.01 | | GROUND_INST: instantiating (1) with all_55_4, all_67_0, all_55_3, all_55_2, % 16.59/3.01 | | all_141_0, simplifying with (22), (33), (37), (38), (69), (86), % 16.59/3.01 | | (87) gives: % 16.59/3.01 | | (88) all_55_2 = all_55_4 % 16.59/3.01 | | % 16.59/3.01 | | REDUCE: (68), (88) imply: % 16.59/3.01 | | (89) $false % 16.59/3.01 | | % 16.59/3.01 | | CLOSE: (89) is inconsistent. % 16.59/3.01 | | % 16.59/3.01 | End of split % 16.59/3.01 | % 16.59/3.01 End of proof % 16.59/3.01 % SZS output end Proof for theBenchmark % 16.59/3.01 % 16.59/3.01 2492ms %------------------------------------------------------------------------------