%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL944_8 : TPTP v9.3.1. Released v8.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:08:42 PM UTC 2026
% Result : Theorem 7.79s 1.52s
% Output : CNFRefutation 7.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL944_8 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.02/0.31 % Computer : n012.cluster.edu
% 0.02/0.31 % Model : x86_64 x86_64
% 0.02/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.31 % Memory : 8046.5625MB
% 0.02/0.31 % OS : Linux 6.8.0-71-generic
% 0.02/0.31 % CPULimit : 300
% 0.02/0.31 % WCLimit : 300
% 0.02/0.31 % DateTime : Thu Sep 24 00:41:51 UTC 2026
% 0.02/0.31 % CPUTime :
% 0.02/0.31 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.06/0.33 Running first-order theorem proving
% 0.06/0.33 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.34
% 0.06/0.34 % ======== iProver multi-core TPTP/SMT =========
% 0.06/0.34
% 0.06/0.34 % Detected problem language: tptp
% 0.06/0.34 % Proving...
% 7.79/1.52 % SZS status Started for theBenchmark.p
% 7.79/1.52 % SZS status Theorem for theBenchmark.p
% 7.79/1.52
% 7.79/1.52 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 7.79/1.52
% 7.79/1.52 % ------ iProver source info
% 7.79/1.52
% 7.79/1.52 % git: date: 2026-07-19 20:42:38 +0200
% 7.79/1.52 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 7.79/1.52 % git: non_committed_changes: false
% 7.79/1.52
% 7.79/1.52 % ------ Parsing...
% 7.79/1.52 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 7.79/1.52
% 7.79/1.52 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e %
% 7.79/1.52
% 7.79/1.52 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 7.79/1.52 % ------ Proving...
% 7.79/1.52 % ------ Problem Properties
% 7.79/1.52
% 7.79/1.52 %
% 7.79/1.52 % clauses 286
% 7.79/1.52 % conjectures 2
% 7.79/1.52 % EPR 19
% 7.79/1.52 % Horn 96
% 7.79/1.52 % unary 4
% 7.79/1.52 % binary 21
% 7.79/1.52 % lits 1573
% 7.79/1.52 % lits eq 0
% 7.79/1.52 % fd_pure 0
% 7.79/1.52 % fd_pseudo 0
% 7.79/1.52 % fd_cond 0
% 7.79/1.52 % fd_pseudo_cond 0
% 7.79/1.52 % AC symbols 0
% 7.79/1.52
% 7.79/1.52 % ------ Input Options Time Limit: Unbounded
% 7.79/1.52
% 7.79/1.52
% 7.79/1.52 % ------
% 7.79/1.52 % Current options:
% 7.79/1.52 % ------
% 7.79/1.52
% 7.79/1.52
% 7.79/1.52 %
% 7.79/1.52
% 7.79/1.52 % ------ Proving...
% 7.79/1.52 %
% 7.79/1.52
% 7.79/1.52 % SZS status Theorem for theBenchmark.p
% 7.79/1.52
% 7.79/1.52 % SZS output start CNFRefutation for theBenchmark.p
% 7.79/1.52
% 7.79/1.52 tff(func_def_0, type, '$ki_local_world': '$ki_world').
% 7.79/1.52 tff(pred_def_1, type, '$ki_accessible': ('$ki_world' * '$ki_world') > $o).
% 7.79/1.52 tff(pred_def_2, type, r2: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_3, type, r3: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_4, type, r4: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_5, type, r5: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_6, type, equivalence_1: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_7, type, equivalence_2: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_8, type, cn2: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_9, type, cn1: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_10, type, cn3: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_11, type, kn2: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_12, type, kn1: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_13, type, kn3: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_14, type, equivalence_3: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_15, type, op_implies_or: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_16, type, op_and: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_17, type, and_2: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_18, type, and_3: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_19, type, and_1: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_20, type, implies_2: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_21, type, implies_3: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_22, type, op_implies_and: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_23, type, implies_1: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_24, type, substitution_of_equivalents: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_25, type, op_or: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_26, type, modus_tollens: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_27, type, or_1: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_28, type, or_2: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_29, type, or_3: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_30, type, op_equiv: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_31, type, modus_ponens: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_32, type, r1: '$ki_world' > $o).
% 7.79/1.52 tff(pred_def_33, type, qmltpeq: ('$ki_world' * $i * $i) > $o).
% 7.79/1.52 tff(pred_def_34, type, is_a_theorem: ('$ki_world' * $i) > $o).
% 7.79/1.52 tff(pred_def_35, type, '$ki_exists_in_world_$i': ('$ki_world' * $i) > $o).
% 7.79/1.52 tff(pred_def_36, type, sP0: '$ki_world' > $o).
% 7.79/1.52 tff(func_def_37, type, sK32: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_38, type, sK33: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_39, type, sK34: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_40, type, sK35: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_41, type, sK36: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_42, type, sK37: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_43, type, sK38: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_44, type, sK39: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_45, type, sK40: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_46, type, sK41: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_47, type, sK42: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_48, type, sK43: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_49, type, sK44: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_50, type, sK45: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_51, type, sK46: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_52, type, sK47: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_53, type, sK48: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_54, type, sK49: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_55, type, sK50: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_56, type, sK51: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_57, type, sK52: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_58, type, sK53: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_59, type, sK54: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_60, type, sK55: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_61, type, sK56: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_62, type, sK57: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_63, type, sK58: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_64, type, sK59: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_65, type, sK60: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_66, type, sK61: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_67, type, sK62: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_68, type, sK63: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_69, type, sK64: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_70, type, sK65: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_71, type, sK66: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_72, type, sK67: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_73, type, sK68: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_74, type, sK69: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_75, type, sK70: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_76, type, sK71: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_77, type, sK72: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_78, type, sK73: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_79, type, sK74: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_80, type, sK75: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_81, type, sK76: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_82, type, sK77: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_83, type, sK78: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_84, type, sK79: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_85, type, sK80: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_86, type, sK81: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_87, type, sK82: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_88, type, sK83: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_89, type, sK84: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_90, type, sK85: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_91, type, sK86: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_92, type, sK87: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_93, type, sK88: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_94, type, sK89: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_95, type, sK90: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_96, type, sK91: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_97, type, sK92: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_98, type, sK93: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_99, type, sK94: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_100, type, sK95: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_101, type, sK96: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_102, type, sK97: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_103, type, sK98: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_104, type, sK99: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_105, type, sK100: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_106, type, sK101: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_107, type, sK102: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_108, type, sK103: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_109, type, sK104: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_110, type, sK105: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_111, type, sK106: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_112, type, sK107: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_113, type, sK108: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_114, type, sK109: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_115, type, sK110: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_116, type, sK111: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_117, type, sK112: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_118, type, sK113: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_119, type, sK114: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_120, type, sK115: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_121, type, sK116: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_122, type, sK117: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_123, type, sK118: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_124, type, sK119: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_125, type, sK120: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_126, type, sK121: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_127, type, sK122: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_128, type, sK123: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_129, type, sK124: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_130, type, sK125: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_131, type, sK126: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_132, type, sK127: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_133, type, sK128: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_134, type, sK129: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_135, type, sK130: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_136, type, sK131: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_137, type, sK132: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_138, type, sK133: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_139, type, sK134: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_140, type, sK135: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_141, type, sK136: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_142, type, sK137: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_143, type, sK138: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_144, type, sK139: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_145, type, sK140: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_146, type, sK141: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_147, type, sK142: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_148, type, sK143: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_149, type, sK144: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_150, type, sK145: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_151, type, sK146: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_152, type, sK147: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_153, type, sK148: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_154, type, sK149: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_155, type, sK150: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_156, type, sK151: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_157, type, sK152: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_158, type, sK153: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_159, type, sK154: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_160, type, sK155: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_161, type, sK156: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_162, type, sK157: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_163, type, sK158: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_164, type, sK159: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_165, type, sK160: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_166, type, sK161: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_167, type, sK162: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_168, type, sK163: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_169, type, sK164: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_170, type, sK165: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_171, type, sK166: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_172, type, sK167: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_173, type, sK168: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_174, type, sK169: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_175, type, sK170: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_176, type, sK171: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_177, type, sK172: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_178, type, sK173: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_179, type, sK174: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_180, type, sK175: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_181, type, sK176: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_182, type, sK177: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_183, type, sK178: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_184, type, sK179: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_185, type, sK180: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_186, type, sK181: '$ki_world' > $i).
% 7.79/1.52 tff(func_def_187, type, sK182: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_188, type, sK183: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_189, type, sK184: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_190, type, sK185: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_191, type, sK186: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_192, type, sK187: '$ki_world' > '$ki_world').
% 7.79/1.52 tff(func_def_193, type, sK188: '$ki_world').
% 7.79/1.52 tff(f1,axiom,(
% 7.79/1.52 ! [X0 : '$ki_world'] : '$ki_accessible'(X0,X0)),
% 7.79/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mrel_reflexive)).
% 7.79/1.52
% 7.79/1.52 tff(f26,axiom,(
% 7.79/1.52 ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => (! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => or_2(X1)) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => ! [X2 : $i] : ('$ki_exists_in_world_$i'(X1,X2) => ! [X3 : '$ki_world'] : ('$ki_accessible'(X1,X3) => ! [X4 : $i] : ('$ki_exists_in_world_$i'(X3,X4) => ! [X5 : '$ki_world'] : ('$ki_accessible'(X3,X5) => is_a_theorem(X5,implies(X4,or(X2,X4)))))))))) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => (! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => ! [X2 : $i] : ('$ki_exists_in_world_$i'(X1,X2) => ! [X3 : '$ki_world'] : ('$ki_accessible'(X1,X3) => ! [X4 : $i] : ('$ki_exists_in_world_$i'(X3,X4) => ! [X5 : '$ki_world'] : ('$ki_accessible'(X3,X5) => is_a_theorem(X5,implies(X4,or(X2,X4)))))))) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => or_2(X1))))),
% 7.79/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_2_0)).
% 7.79/1.52
% 7.79/1.52 tff(f38,axiom,(
% 7.79/1.52 ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => (! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => r2(X1)) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => ! [X2 : $i] : ('$ki_exists_in_world_$i'(X1,X2) => ! [X3 : '$ki_world'] : ('$ki_accessible'(X1,X3) => ! [X4 : $i] : ('$ki_exists_in_world_$i'(X3,X4) => ! [X5 : '$ki_world'] : ('$ki_accessible'(X3,X5) => is_a_theorem(X5,implies(X4,or(X2,X4)))))))))) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => (! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => ! [X2 : $i] : ('$ki_exists_in_world_$i'(X1,X2) => ! [X3 : '$ki_world'] : ('$ki_accessible'(X1,X3) => ! [X4 : $i] : ('$ki_exists_in_world_$i'(X3,X4) => ! [X5 : '$ki_world'] : ('$ki_accessible'(X3,X5) => is_a_theorem(X5,implies(X4,or(X2,X4)))))))) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => r2(X1))))),
% 7.79/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',r2_0)).
% 7.79/1.52
% 7.79/1.52 tff(f59,axiom,(
% 7.79/1.52 ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => or_2(X0))),
% 7.79/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hilbert_or_2)).
% 7.79/1.52
% 7.79/1.52 tff(f68,conjecture,(
% 7.79/1.52 ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => r2(X0))),
% 7.79/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',verify)).
% 7.79/1.52
% 7.79/1.52 tff(f69,negated_conjecture,(
% 7.79/1.52 ~ ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => r2(X0))),
% 7.79/1.52 inference(negated_conjecture,[status(cth)],[f68])).
% 7.79/1.52
% 7.79/1.52 tff(f92,plain,(
% 7.79/1.52 ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => (! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => or_2(X1)) => ! [X2 : '$ki_world'] : ('$ki_accessible'(X0,X2) => ! [X3 : $i] : ('$ki_exists_in_world_$i'(X2,X3) => ! [X4 : '$ki_world'] : ('$ki_accessible'(X2,X4) => ! [X5 : $i] : ('$ki_exists_in_world_$i'(X4,X5) => ! [X6 : '$ki_world'] : ('$ki_accessible'(X4,X6) => is_a_theorem(X6,implies(X5,or(X3,X5)))))))))) & ! [X7 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X7) => (! [X8 : '$ki_world'] : ('$ki_accessible'(X7,X8) => ! [X9 : $i] : ('$ki_exists_in_world_$i'(X8,X9) => ! [X10 : '$ki_world'] : ('$ki_accessible'(X8,X10) => ! [X11 : $i] : ('$ki_exists_in_world_$i'(X10,X11) => ! [X12 : '$ki_world'] : ('$ki_accessible'(X10,X12) => is_a_theorem(X12,implies(X11,or(X9,X11)))))))) => ! [X13 : '$ki_world'] : ('$ki_accessible'(X7,X13) => or_2(X13))))),
% 7.79/1.52 inference(rectify,[],[f26])).
% 7.79/1.52
% 7.79/1.52 tff(f104,plain,(
% 7.79/1.52 ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => (! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => r2(X1)) => ! [X2 : '$ki_world'] : ('$ki_accessible'(X0,X2) => ! [X3 : $i] : ('$ki_exists_in_world_$i'(X2,X3) => ! [X4 : '$ki_world'] : ('$ki_accessible'(X2,X4) => ! [X5 : $i] : ('$ki_exists_in_world_$i'(X4,X5) => ! [X6 : '$ki_world'] : ('$ki_accessible'(X4,X6) => is_a_theorem(X6,implies(X5,or(X3,X5)))))))))) & ! [X7 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X7) => (! [X8 : '$ki_world'] : ('$ki_accessible'(X7,X8) => ! [X9 : $i] : ('$ki_exists_in_world_$i'(X8,X9) => ! [X10 : '$ki_world'] : ('$ki_accessible'(X8,X10) => ! [X11 : $i] : ('$ki_exists_in_world_$i'(X10,X11) => ! [X12 : '$ki_world'] : ('$ki_accessible'(X10,X12) => is_a_theorem(X12,implies(X11,or(X9,X11)))))))) => ! [X13 : '$ki_world'] : ('$ki_accessible'(X7,X13) => r2(X13))))),
% 7.79/1.52 inference(rectify,[],[f38])).
% 7.79/1.52
% 7.79/1.52 tff(f158,plain,(
% 7.79/1.52 ! [X0 : '$ki_world'] : ((! [X2 : '$ki_world'] : (! [X3 : $i] : (! [X4 : '$ki_world'] : (! [X5 : $i] : (! [X6 : '$ki_world'] : (is_a_theorem(X6,implies(X5,or(X3,X5))) | ~'$ki_accessible'(X4,X6)) | ~'$ki_exists_in_world_$i'(X4,X5)) | ~'$ki_accessible'(X2,X4)) | ~'$ki_exists_in_world_$i'(X2,X3)) | ~'$ki_accessible'(X0,X2)) | ? [X1 : '$ki_world'] : (~or_2(X1) & '$ki_accessible'(X0,X1))) | ~'$ki_accessible'('$ki_local_world',X0)) & ! [X7 : '$ki_world'] : ((! [X13 : '$ki_world'] : (or_2(X13) | ~'$ki_accessible'(X7,X13)) | ? [X8 : '$ki_world'] : (? [X9 : $i] : (? [X10 : '$ki_world'] : (? [X11 : $i] : (? [X12 : '$ki_world'] : (~is_a_theorem(X12,implies(X11,or(X9,X11))) & '$ki_accessible'(X10,X12)) & '$ki_exists_in_world_$i'(X10,X11)) & '$ki_accessible'(X8,X10)) & '$ki_exists_in_world_$i'(X8,X9)) & '$ki_accessible'(X7,X8))) | ~'$ki_accessible'('$ki_local_world',X7))),
% 7.79/1.52 inference(ennf_transformation,[],[f92])).
% 7.79/1.52
% 7.79/1.52 tff(f159,plain,(
% 7.79/1.52 ! [X0 : '$ki_world'] : (! [X2 : '$ki_world'] : (! [X3 : $i] : (! [X4 : '$ki_world'] : (! [X5 : $i] : (! [X6 : '$ki_world'] : (is_a_theorem(X6,implies(X5,or(X3,X5))) | ~'$ki_accessible'(X4,X6)) | ~'$ki_exists_in_world_$i'(X4,X5)) | ~'$ki_accessible'(X2,X4)) | ~'$ki_exists_in_world_$i'(X2,X3)) | ~'$ki_accessible'(X0,X2)) | ? [X1 : '$ki_world'] : (~or_2(X1) & '$ki_accessible'(X0,X1)) | ~'$ki_accessible'('$ki_local_world',X0)) & ! [X7 : '$ki_world'] : (! [X13 : '$ki_world'] : (or_2(X13) | ~'$ki_accessible'(X7,X13)) | ? [X8 : '$ki_world'] : (? [X9 : $i] : (? [X10 : '$ki_world'] : (? [X11 : $i] : (? [X12 : '$ki_world'] : (~is_a_theorem(X12,implies(X11,or(X9,X11))) & '$ki_accessible'(X10,X12)) & '$ki_exists_in_world_$i'(X10,X11)) & '$ki_accessible'(X8,X10)) & '$ki_exists_in_world_$i'(X8,X9)) & '$ki_accessible'(X7,X8)) | ~'$ki_accessible'('$ki_local_world',X7))),
% 7.79/1.52 inference(flattening,[],[f158])).
% 7.79/1.52
% 7.79/1.52 tff(f182,plain,(
% 7.79/1.52 ! [X0 : '$ki_world'] : ((! [X2 : '$ki_world'] : (! [X3 : $i] : (! [X4 : '$ki_world'] : (! [X5 : $i] : (! [X6 : '$ki_world'] : (is_a_theorem(X6,implies(X5,or(X3,X5))) | ~'$ki_accessible'(X4,X6)) | ~'$ki_exists_in_world_$i'(X4,X5)) | ~'$ki_accessible'(X2,X4)) | ~'$ki_exists_in_world_$i'(X2,X3)) | ~'$ki_accessible'(X0,X2)) | ? [X1 : '$ki_world'] : (~r2(X1) & '$ki_accessible'(X0,X1))) | ~'$ki_accessible'('$ki_local_world',X0)) & ! [X7 : '$ki_world'] : ((! [X13 : '$ki_world'] : (r2(X13) | ~'$ki_accessible'(X7,X13)) | ? [X8 : '$ki_world'] : (? [X9 : $i] : (? [X10 : '$ki_world'] : (? [X11 : $i] : (? [X12 : '$ki_world'] : (~is_a_theorem(X12,implies(X11,or(X9,X11))) & '$ki_accessible'(X10,X12)) & '$ki_exists_in_world_$i'(X10,X11)) & '$ki_accessible'(X8,X10)) & '$ki_exists_in_world_$i'(X8,X9)) & '$ki_accessible'(X7,X8))) | ~'$ki_accessible'('$ki_local_world',X7))),
% 7.79/1.52 inference(ennf_transformation,[],[f104])).
% 7.79/1.52
% 7.79/1.52 tff(f183,plain,(
% 7.79/1.52 ! [X0 : '$ki_world'] : (! [X2 : '$ki_world'] : (! [X3 : $i] : (! [X4 : '$ki_world'] : (! [X5 : $i] : (! [X6 : '$ki_world'] : (is_a_theorem(X6,implies(X5,or(X3,X5))) | ~'$ki_accessible'(X4,X6)) | ~'$ki_exists_in_world_$i'(X4,X5)) | ~'$ki_accessible'(X2,X4)) | ~'$ki_exists_in_world_$i'(X2,X3)) | ~'$ki_accessible'(X0,X2)) | ? [X1 : '$ki_world'] : (~r2(X1) & '$ki_accessible'(X0,X1)) | ~'$ki_accessible'('$ki_local_world',X0)) & ! [X7 : '$ki_world'] : (! [X13 : '$ki_world'] : (r2(X13) | ~'$ki_accessible'(X7,X13)) | ? [X8 : '$ki_world'] : (? [X9 : $i] : (? [X10 : '$ki_world'] : (? [X11 : $i] : (? [X12 : '$ki_world'] : (~is_a_theorem(X12,implies(X11,or(X9,X11))) & '$ki_accessible'(X10,X12)) & '$ki_exists_in_world_$i'(X10,X11)) & '$ki_accessible'(X8,X10)) & '$ki_exists_in_world_$i'(X8,X9)) & '$ki_accessible'(X7,X8)) | ~'$ki_accessible'('$ki_local_world',X7))),
% 7.79/1.52 inference(flattening,[],[f182])).
% 7.79/1.52
% 7.79/1.52 tff(f212,plain,(
% 7.79/1.52 ! [X0 : '$ki_world'] : (or_2(X0) | ~'$ki_accessible'('$ki_local_world',X0))),
% 7.79/1.52 inference(ennf_transformation,[],[f59])).
% 7.79/1.52
% 7.79/1.52 tff(f221,plain,(
% 7.79/1.52 ? [X0 : '$ki_world'] : (~r2(X0) & '$ki_accessible'('$ki_local_world',X0))),
% 7.79/1.52 inference(ennf_transformation,[],[f69])).
% 7.79/1.52
% 7.79/1.52 tff(f272,plain,(
% 7.79/1.52 ! [X0 : '$ki_world'] : (! [X1 : '$ki_world'] : (! [X2 : $i] : (! [X3 : '$ki_world'] : (! [X4 : $i] : (! [X5 : '$ki_world'] : (is_a_theorem(X5,implies(X4,or(X2,X4))) | ~'$ki_accessible'(X3,X5)) | ~'$ki_exists_in_world_$i'(X3,X4)) | ~'$ki_accessible'(X1,X3)) | ~'$ki_exists_in_world_$i'(X1,X2)) | ~'$ki_accessible'(X0,X1)) | ? [X6 : '$ki_world'] : (~or_2(X6) & '$ki_accessible'(X0,X6)) | ~'$ki_accessible'('$ki_local_world',X0)) & ! [X7 : '$ki_world'] : (! [X8 : '$ki_world'] : (or_2(X8) | ~'$ki_accessible'(X7,X8)) | ? [X9 : '$ki_world'] : (? [X10 : $i] : (? [X11 : '$ki_world'] : (? [X12 : $i] : (? [X13 : '$ki_world'] : (~is_a_theorem(X13,implies(X12,or(X10,X12))) & '$ki_accessible'(X11,X13)) & '$ki_exists_in_world_$i'(X11,X12)) & '$ki_accessible'(X9,X11)) & '$ki_exists_in_world_$i'(X9,X10)) & '$ki_accessible'(X7,X9)) | ~'$ki_accessible'('$ki_local_world',X7))),
% 7.79/1.52 inference(rectify,[],[f159])).
% 7.79/1.52
% 7.79/1.52 tff(f273,plain,(
% 7.79/1.52 ! [X0 : '$ki_world'] : (! [X1 : '$ki_world'] : (! [X2 : $i] : (! [X3 : '$ki_world'] : (! [X4 : $i] : (! [X5 : '$ki_world'] : (is_a_theorem(X5,implies(X4,or(X2,X4))) | ~'$ki_accessible'(X3,X5)) | ~'$ki_exists_in_world_$i'(X3,X4)) | ~'$ki_accessible'(X1,X3)) | ~'$ki_exists_in_world_$i'(X1,X2)) | ~'$ki_accessible'(X0,X1)) | (~or_2(sK83(X0)) & '$ki_accessible'(X0,sK83(X0))) | ~'$ki_accessible'('$ki_local_world',X0)) & ! [X7 : '$ki_world'] : (! [X8 : '$ki_world'] : (or_2(X8) | ~'$ki_accessible'(X7,X8)) | (((((~is_a_theorem(sK88(X7),implies(sK87(X7),or(sK85(X7),sK87(X7)))) & '$ki_accessible'(sK86(X7),sK88(X7))) & '$ki_exists_in_world_$i'(sK86(X7),sK87(X7))) & '$ki_accessible'(sK84(X7),sK86(X7))) & '$ki_exists_in_world_$i'(sK84(X7),sK85(X7))) & '$ki_accessible'(X7,sK84(X7))) | ~'$ki_accessible'('$ki_local_world',X7))),
% 7.79/1.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK83,sK84,sK85,sK86,sK87,sK88]),skolemize(X6,sK83(X0)),skolemize(X9,sK84(X7)),skolemize(X10,sK85(X7)),skolemize(X11,sK86(X7)),skolemize(X12,sK87(X7)),skolemize(X13,sK88(X7))],[f272])).
% 7.79/1.52
% 7.79/1.52 tff(f296,plain,(
% 7.79/1.52 ! [X0 : '$ki_world'] : (! [X1 : '$ki_world'] : (! [X2 : $i] : (! [X3 : '$ki_world'] : (! [X4 : $i] : (! [X5 : '$ki_world'] : (is_a_theorem(X5,implies(X4,or(X2,X4))) | ~'$ki_accessible'(X3,X5)) | ~'$ki_exists_in_world_$i'(X3,X4)) | ~'$ki_accessible'(X1,X3)) | ~'$ki_exists_in_world_$i'(X1,X2)) | ~'$ki_accessible'(X0,X1)) | ? [X6 : '$ki_world'] : (~r2(X6) & '$ki_accessible'(X0,X6)) | ~'$ki_accessible'('$ki_local_world',X0)) & ! [X7 : '$ki_world'] : (! [X8 : '$ki_world'] : (r2(X8) | ~'$ki_accessible'(X7,X8)) | ? [X9 : '$ki_world'] : (? [X10 : $i] : (? [X11 : '$ki_world'] : (? [X12 : $i] : (? [X13 : '$ki_world'] : (~is_a_theorem(X13,implies(X12,or(X10,X12))) & '$ki_accessible'(X11,X13)) & '$ki_exists_in_world_$i'(X11,X12)) & '$ki_accessible'(X9,X11)) & '$ki_exists_in_world_$i'(X9,X10)) & '$ki_accessible'(X7,X9)) | ~'$ki_accessible'('$ki_local_world',X7))),
% 7.79/1.52 inference(rectify,[],[f183])).
% 7.79/1.52
% 7.79/1.52 tff(f297,plain,(
% 7.79/1.52 ! [X0 : '$ki_world'] : (! [X1 : '$ki_world'] : (! [X2 : $i] : (! [X3 : '$ki_world'] : (! [X4 : $i] : (! [X5 : '$ki_world'] : (is_a_theorem(X5,implies(X4,or(X2,X4))) | ~'$ki_accessible'(X3,X5)) | ~'$ki_exists_in_world_$i'(X3,X4)) | ~'$ki_accessible'(X1,X3)) | ~'$ki_exists_in_world_$i'(X1,X2)) | ~'$ki_accessible'(X0,X1)) | (~r2(sK155(X0)) & '$ki_accessible'(X0,sK155(X0))) | ~'$ki_accessible'('$ki_local_world',X0)) & ! [X7 : '$ki_world'] : (! [X8 : '$ki_world'] : (r2(X8) | ~'$ki_accessible'(X7,X8)) | (((((~is_a_theorem(sK160(X7),implies(sK159(X7),or(sK157(X7),sK159(X7)))) & '$ki_accessible'(sK158(X7),sK160(X7))) & '$ki_exists_in_world_$i'(sK158(X7),sK159(X7))) & '$ki_accessible'(sK156(X7),sK158(X7))) & '$ki_exists_in_world_$i'(sK156(X7),sK157(X7))) & '$ki_accessible'(X7,sK156(X7))) | ~'$ki_accessible'('$ki_local_world',X7))),
% 7.79/1.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK155,sK156,sK157,sK158,sK159,sK160]),skolemize(X6,sK155(X0)),skolemize(X9,sK156(X7)),skolemize(X10,sK157(X7)),skolemize(X11,sK158(X7)),skolemize(X12,sK159(X7)),skolemize(X13,sK160(X7))],[f296])).
% 7.79/1.52
% 7.79/1.52 tff(f314,plain,(
% 7.79/1.52 ~r2(sK188) & '$ki_accessible'('$ki_local_world',sK188)),
% 7.79/1.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK188]),skolemize(X0,sK188)],[f221])).
% 7.79/1.52
% 7.79/1.52 tff(f315,plain,(
% 7.79/1.52 ( ! [X0 : '$ki_world'] : ('$ki_accessible'(X0,X0)) )),
% 7.79/1.52 inference(cnf_transformation,[],[f1])).
% 7.79/1.52
% 7.79/1.52 tff(f448,plain,(
% 7.79/1.52 ( ! [X2 : $i,X3 : '$ki_world',X0 : '$ki_world',X1 : '$ki_world',X4 : $i,X5 : '$ki_world'] : (is_a_theorem(X5,implies(X4,or(X2,X4))) | ~'$ki_accessible'(X3,X5) | ~'$ki_exists_in_world_$i'(X3,X4) | ~'$ki_accessible'(X1,X3) | ~'$ki_exists_in_world_$i'(X1,X2) | ~'$ki_accessible'(X0,X1) | '$ki_accessible'(X0,sK83(X0)) | ~'$ki_accessible'('$ki_local_world',X0)) )),
% 7.79/1.52 inference(cnf_transformation,[],[f273])).
% 7.79/1.52
% 7.79/1.52 tff(f449,plain,(
% 7.79/1.52 ( ! [X2 : $i,X3 : '$ki_world',X0 : '$ki_world',X1 : '$ki_world',X4 : $i,X5 : '$ki_world'] : (is_a_theorem(X5,implies(X4,or(X2,X4))) | ~'$ki_accessible'(X3,X5) | ~'$ki_exists_in_world_$i'(X3,X4) | ~'$ki_accessible'(X1,X3) | ~'$ki_exists_in_world_$i'(X1,X2) | ~'$ki_accessible'(X0,X1) | ~or_2(sK83(X0)) | ~'$ki_accessible'('$ki_local_world',X0)) )),
% 7.79/1.52 inference(cnf_transformation,[],[f273])).
% 7.79/1.52
% 7.79/1.52 tff(f538,plain,(
% 7.79/1.52 ( ! [X8 : '$ki_world',X7 : '$ki_world'] : (r2(X8) | ~'$ki_accessible'(X7,X8) | '$ki_accessible'(X7,sK156(X7)) | ~'$ki_accessible'('$ki_local_world',X7)) )),
% 7.79/1.52 inference(cnf_transformation,[],[f297])).
% 7.79/1.52
% 7.79/1.52 tff(f539,plain,(
% 7.79/1.52 ( ! [X8 : '$ki_world',X7 : '$ki_world'] : (r2(X8) | ~'$ki_accessible'(X7,X8) | '$ki_exists_in_world_$i'(sK156(X7),sK157(X7)) | ~'$ki_accessible'('$ki_local_world',X7)) )),
% 7.79/1.52 inference(cnf_transformation,[],[f297])).
% 7.79/1.52
% 7.79/1.52 tff(f540,plain,(
% 7.79/1.52 ( ! [X8 : '$ki_world',X7 : '$ki_world'] : (r2(X8) | ~'$ki_accessible'(X7,X8) | '$ki_accessible'(sK156(X7),sK158(X7)) | ~'$ki_accessible'('$ki_local_world',X7)) )),
% 7.79/1.52 inference(cnf_transformation,[],[f297])).
% 7.79/1.52
% 7.79/1.52 tff(f541,plain,(
% 7.79/1.52 ( ! [X8 : '$ki_world',X7 : '$ki_world'] : (r2(X8) | ~'$ki_accessible'(X7,X8) | '$ki_exists_in_world_$i'(sK158(X7),sK159(X7)) | ~'$ki_accessible'('$ki_local_world',X7)) )),
% 7.79/1.52 inference(cnf_transformation,[],[f297])).
% 7.79/1.52
% 7.79/1.52 tff(f542,plain,(
% 7.79/1.52 ( ! [X8 : '$ki_world',X7 : '$ki_world'] : (r2(X8) | ~'$ki_accessible'(X7,X8) | '$ki_accessible'(sK158(X7),sK160(X7)) | ~'$ki_accessible'('$ki_local_world',X7)) )),
% 7.79/1.52 inference(cnf_transformation,[],[f297])).
% 7.79/1.52
% 7.79/1.52 tff(f543,plain,(
% 7.79/1.52 ( ! [X8 : '$ki_world',X7 : '$ki_world'] : (r2(X8) | ~'$ki_accessible'(X7,X8) | ~is_a_theorem(sK160(X7),implies(sK159(X7),or(sK157(X7),sK159(X7)))) | ~'$ki_accessible'('$ki_local_world',X7)) )),
% 7.79/1.52 inference(cnf_transformation,[],[f297])).
% 7.79/1.52
% 7.79/1.52 tff(f596,plain,(
% 7.79/1.52 ( ! [X0 : '$ki_world'] : (or_2(X0) | ~'$ki_accessible'('$ki_local_world',X0)) )),
% 7.79/1.52 inference(cnf_transformation,[],[f212])).
% 7.79/1.52
% 7.79/1.52 tff(f605,plain,(
% 7.79/1.52 '$ki_accessible'('$ki_local_world',sK188)),
% 7.79/1.52 inference(cnf_transformation,[],[f314])).
% 7.79/1.52
% 7.79/1.52 tff(f606,plain,(
% 7.79/1.52 ~r2(sK188)),
% 7.79/1.52 inference(cnf_transformation,[],[f314])).
% 7.79/1.52
% 7.79/1.52 tcf(c_49,plain,![X0_'ki_world':'$ki_world']:
% 7.79/1.52 ('$ki_accessible'(X0_'ki_world',X0_'ki_world')),
% 7.79/1.52 inference(cnf_transformation,[],[f315])).
% 7.79/1.52
% 7.79/1.52 tcf(c_176,plain,![X0:$i,X0_'ki_world':'$ki_world',X1:$i,X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world',X3_'ki_world':'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'(X2_'ki_world',X3_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X3_'ki_world',X0_'ki_world')|~'$ki_exists_in_world(X0_'ki_world',X0)|
% 7.79/1.52 ~'$ki_exists_in_world(X3_'ki_world',X1)|~'$ki_accessible'('$ki_local_world',X2_'ki_world')|
% 7.79/1.52 ~or_2(sK83(X2_'ki_world'))|is_a_theorem(X1_'ki_world',implies(X0,or(X1,X0)))),
% 7.79/1.52 inference(cnf_transformation,[],[f449])).
% 7.79/1.52
% 7.79/1.52 tcf(c_177,plain,![X0:$i,X0_'ki_world':'$ki_world',X1:$i,X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world',X3_'ki_world':'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'(X2_'ki_world',X3_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X3_'ki_world',X0_'ki_world')|~'$ki_exists_in_world(X0_'ki_world',X0)|
% 7.79/1.52 ~'$ki_exists_in_world(X3_'ki_world',X1)|~'$ki_accessible'('$ki_local_world',X2_'ki_world')|
% 7.79/1.52 is_a_theorem(X1_'ki_world',implies(X0,or(X1,X0)))|'$ki_accessible'(X2_'ki_world',sK83(X2_'ki_world'))),
% 7.79/1.52 inference(cnf_transformation,[],[f448])).
% 7.79/1.52
% 7.79/1.52 tcf(c_274,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 7.79/1.52 (~is_a_theorem(sK160(X0_'ki_world'),implies(sK159(X0_'ki_world'),or(sK157(X0_'ki_world'),sK159(X0_'ki_world'))))|
% 7.79/1.52 ~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'('$ki_local_world',X0_'ki_world')|
% 7.79/1.52 r2(X1_'ki_world')),
% 7.79/1.52 inference(cnf_transformation,[],[f543])).
% 7.79/1.52
% 7.79/1.52 tcf(c_275,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'('$ki_local_world',X0_'ki_world')|
% 7.79/1.52 '$ki_accessible'(sK158(X0_'ki_world'),sK160(X0_'ki_world'))|r2(X1_'ki_world')),
% 7.79/1.52 inference(cnf_transformation,[],[f542])).
% 7.79/1.52
% 7.79/1.52 tcf(c_276,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'('$ki_local_world',X0_'ki_world')|
% 7.79/1.52 '$ki_exists_in_world(sK158(X0_'ki_world'),sK159(X0_'ki_world'))|r2(X1_'ki_world')),
% 7.79/1.52 inference(cnf_transformation,[],[f541])).
% 7.79/1.52
% 7.79/1.52 tcf(c_277,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'('$ki_local_world',X0_'ki_world')|
% 7.79/1.52 '$ki_accessible'(sK156(X0_'ki_world'),sK158(X0_'ki_world'))|r2(X1_'ki_world')),
% 7.79/1.52 inference(cnf_transformation,[],[f540])).
% 7.79/1.52
% 7.79/1.52 tcf(c_278,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'('$ki_local_world',X0_'ki_world')|
% 7.79/1.52 '$ki_exists_in_world(sK156(X0_'ki_world'),sK157(X0_'ki_world'))|r2(X1_'ki_world')),
% 7.79/1.52 inference(cnf_transformation,[],[f539])).
% 7.79/1.52
% 7.79/1.52 tcf(c_279,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'('$ki_local_world',X0_'ki_world')|
% 7.79/1.52 '$ki_accessible'(X0_'ki_world',sK156(X0_'ki_world'))|r2(X1_'ki_world')),
% 7.79/1.52 inference(cnf_transformation,[],[f538])).
% 7.79/1.52
% 7.79/1.52 tcf(c_330,plain,![X0_'ki_world':'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'('$ki_local_world',X0_'ki_world')|or_2(X0_'ki_world')),
% 7.79/1.52 inference(cnf_transformation,[],[f596])).
% 7.79/1.52
% 7.79/1.52 tcf(c_339,negated_conjecture,
% 7.79/1.52 (~r2(sK188)),
% 7.79/1.52 inference(cnf_transformation,[],[f606])).
% 7.79/1.52
% 7.79/1.52 tcf(c_340,negated_conjecture,
% 7.79/1.52 ('$ki_accessible'('$ki_local_world',sK188)),
% 7.79/1.52 inference(cnf_transformation,[],[f605])).
% 7.79/1.52
% 7.79/1.52 tcf(c_341,plain,
% 7.79/1.52 ('$ki_accessible'('$ki_local_world','$ki_local_world')),
% 7.79/1.52 inference(instantiation,[status(thm)],[c_49])).
% 7.79/1.52
% 7.79/1.52 tcf(c_8510,plain,![X0_'ki_world':'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_'ki_world',sK188)|~'$ki_accessible'('$ki_local_world',X0_'ki_world')|
% 7.79/1.52 '$ki_accessible'(X0_'ki_world',sK156(X0_'ki_world'))),
% 7.79/1.52 inference(resolution,[status(thm)],[c_279,c_339])).
% 7.79/1.52
% 7.79/1.52 tcf(c_8511,plain,
% 7.79/1.52 (~'$ki_accessible'('$ki_local_world','$ki_local_world')|~'$ki_accessible'('$ki_local_world',sK188)|
% 7.79/1.52 '$ki_accessible'('$ki_local_world',sK156('$ki_local_world'))),
% 7.79/1.52 inference(instantiation,[status(thm)],[c_8510])).
% 7.79/1.52
% 7.79/1.52 tcf(c_9876,negated_conjecture,
% 7.79/1.52 (~r2(sK188)),
% 7.79/1.52 inference(subtyping,[status(esa)],[c_339])).
% 7.79/1.52
% 7.79/1.52 tcf(c_9882,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 or_2(X0_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(subtyping,[status(esa)],[c_330])).
% 7.79/1.52
% 7.79/1.52 tcf(c_9925,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 '$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',sK156(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 r2(X1_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(subtyping,[status(esa)],[c_279])).
% 7.79/1.52
% 7.79/1.52 tcf(c_9926,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 '$ki_exists_in_world(sK156(X0_iProver_'ki_accessible'_2_'ki_world'),sK157(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 r2(X1_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(subtyping,[status(esa)],[c_278])).
% 7.79/1.52
% 7.79/1.52 tcf(c_9927,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 '$ki_accessible'(sK156(X0_iProver_'ki_accessible'_2_'ki_world'),sK158(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 r2(X1_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(subtyping,[status(esa)],[c_277])).
% 7.79/1.52
% 7.79/1.52 tcf(c_9928,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 '$ki_exists_in_world(sK158(X0_iProver_'ki_accessible'_2_'ki_world'),sK159(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 r2(X1_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(subtyping,[status(esa)],[c_276])).
% 7.79/1.52
% 7.79/1.52 tcf(c_9929,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 '$ki_accessible'(sK158(X0_iProver_'ki_accessible'_2_'ki_world'),sK160(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 r2(X1_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(subtyping,[status(esa)],[c_275])).
% 7.79/1.52
% 7.79/1.52 tcf(c_9930,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~is_a_theorem(sK160(X0_iProver_'ki_accessible'_2_'ki_world'),implies(sK159(X0_iProver_'ki_accessible'_2_'ki_world'),or(sK157(X0_iProver_'ki_accessible'_2_'ki_world'),sK159(X0_iProver_'ki_accessible'_2_'ki_world'))))|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 r2(X1_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(subtyping,[status(esa)],[c_274])).
% 7.79/1.52
% 7.79/1.52 tcf(c_10027,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X0_iProver_and_2:iProver_and_2,X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_and_2:iProver_and_2,X2_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X3_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X1_iProver_'ki_accessible'_2_'ki_world',X2_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X3_iProver_'ki_accessible'_2_'ki_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_exists_in_world(X0_iProver_'ki_accessible'_2_'ki_world',X0_iProver_and_2)|
% 7.79/1.52 ~'$ki_exists_in_world(X1_iProver_'ki_accessible'_2_'ki_world',X1_iProver_and_2)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X3_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 is_a_theorem(X2_iProver_'ki_accessible'_2_'ki_world',implies(X1_iProver_and_2,or(X0_iProver_and_2,X1_iProver_and_2)))|
% 7.79/1.52 '$ki_accessible'(X3_iProver_'ki_accessible'_2_'ki_world',sK83(X3_iProver_'ki_accessible'_2_'ki_world'))),
% 7.79/1.52 inference(subtyping,[status(esa)],[c_177])).
% 7.79/1.52
% 7.79/1.52 tcf(c_10028,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X0_iProver_and_2:iProver_and_2,X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_and_2:iProver_and_2,X2_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X3_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X1_iProver_'ki_accessible'_2_'ki_world',X2_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X3_iProver_'ki_accessible'_2_'ki_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_exists_in_world(X0_iProver_'ki_accessible'_2_'ki_world',X0_iProver_and_2)|
% 7.79/1.52 ~'$ki_exists_in_world(X1_iProver_'ki_accessible'_2_'ki_world',X1_iProver_and_2)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X3_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~or_2(sK83(X3_iProver_'ki_accessible'_2_'ki_world'))|is_a_theorem(X2_iProver_'ki_accessible'_2_'ki_world',implies(X1_iProver_and_2,or(X0_iProver_and_2,X1_iProver_and_2)))),
% 7.79/1.52 inference(subtyping,[status(esa)],[c_176])).
% 7.79/1.52
% 7.79/1.52 tcf(c_10155,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 ('$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X0_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(subtyping,[status(esa)],[c_49])).
% 7.79/1.52
% 7.79/1.52 tcf(c_10336,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~is_a_theorem(sK160(X0_iProver_'ki_accessible'_2_'ki_world'),implies(sK159(X0_iProver_'ki_accessible'_2_'ki_world'),or(sK157(X0_iProver_'ki_accessible'_2_'ki_world'),sK159(X0_iProver_'ki_accessible'_2_'ki_world'))))|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',sK188)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(resolution,[status(thm)],[c_9930,c_9876])).
% 7.79/1.52
% 7.79/1.52 tcf(c_11063,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X2_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X3_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',sK160(X1_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_exists_in_world(X0_iProver_'ki_accessible'_2_'ki_world',sK159(X1_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_exists_in_world(X2_iProver_'ki_accessible'_2_'ki_world',sK157(X1_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(X2_iProver_'ki_accessible'_2_'ki_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X3_iProver_'ki_accessible'_2_'ki_world',X2_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X1_iProver_'ki_accessible'_2_'ki_world',sK188)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X3_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~or_2(sK83(X3_iProver_'ki_accessible'_2_'ki_world'))),
% 7.79/1.52 inference(resolution,[status(thm)],[c_10028,c_10336])).
% 7.79/1.52
% 7.79/1.52 tcf(c_11311,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X2_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X3_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(sK156(X0_iProver_'ki_accessible'_2_'ki_world'),X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X1_iProver_'ki_accessible'_2_'ki_world',sK160(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(X2_iProver_'ki_accessible'_2_'ki_world',sK156(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_exists_in_world(X1_iProver_'ki_accessible'_2_'ki_world',sK159(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X3_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',sK188)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X2_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~or_2(sK83(X2_iProver_'ki_accessible'_2_'ki_world'))|r2(X3_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(resolution,[status(thm)],[c_11063,c_9926])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12148,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X2_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(sK156(X0_iProver_'ki_accessible'_2_'ki_world'),X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X1_iProver_'ki_accessible'_2_'ki_world',sK160(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(X2_iProver_'ki_accessible'_2_'ki_world',sK156(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_exists_in_world(X1_iProver_'ki_accessible'_2_'ki_world',sK159(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',sK188)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X2_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~or_2(sK83(X2_iProver_'ki_accessible'_2_'ki_world'))),
% 7.79/1.52 inference(resolution,[status(thm)],[c_11311,c_9876])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12158,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X2_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(sK156(X0_iProver_'ki_accessible'_2_'ki_world'),sK158(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(sK158(X0_iProver_'ki_accessible'_2_'ki_world'),sK160(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(X1_iProver_'ki_accessible'_2_'ki_world',sK156(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X2_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',sK188)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~or_2(sK83(X1_iProver_'ki_accessible'_2_'ki_world'))|r2(X2_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(resolution,[status(thm)],[c_12148,c_9928])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12169,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X2_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',sK156(X1_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(X1_iProver_'ki_accessible'_2_'ki_world',X2_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X1_iProver_'ki_accessible'_2_'ki_world',sK188)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~or_2(sK83(X0_iProver_'ki_accessible'_2_'ki_world'))|r2(X2_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(forward_subsumption_resolution,
% 7.79/1.52 [status(thm)],
% 7.79/1.52 [c_12158,c_9929,c_9927])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12185,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',sK156(X1_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(X1_iProver_'ki_accessible'_2_'ki_world',sK188)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~or_2(sK83(X0_iProver_'ki_accessible'_2_'ki_world'))),
% 7.79/1.52 inference(resolution,[status(thm)],[c_12169,c_9876])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12186,plain,
% 7.79/1.52 (~'$ki_accessible'('$ki_local_world',sK156('$ki_local_world'))|~'$ki_accessible'('$ki_local_world','$ki_local_world')|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',sK188)|~or_2(sK83('$ki_local_world'))),
% 7.79/1.52 inference(instantiation,[status(thm)],[c_12185])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12192,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',sK188)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~or_2(sK83(X0_iProver_'ki_accessible'_2_'ki_world'))|r2(X1_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(resolution,[status(thm)],[c_12185,c_9925])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12221,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',sK188)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~or_2(sK83(X0_iProver_'ki_accessible'_2_'ki_world'))),
% 7.79/1.52 inference(resolution,[status(thm)],[c_12192,c_9876])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12338,plain,
% 7.79/1.52 (~'$ki_accessible'('$ki_local_world',sK188)|~or_2(sK83('$ki_local_world'))),
% 7.79/1.52 inference(resolution,[status(thm)],[c_12221,c_10155])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12339,plain,
% 7.79/1.52 (~or_2(sK83('$ki_local_world'))),
% 7.79/1.52 inference(global_subsumption_just,
% 7.79/1.52 [status(thm)],
% 7.79/1.52 [c_12338,c_340,c_341,c_8511,c_12186])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12370,plain,
% 7.79/1.52 (~'$ki_accessible'('$ki_local_world',sK83('$ki_local_world'))),
% 7.79/1.52 inference(resolution,[status(thm)],[c_12339,c_9882])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12382,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X0_iProver_and_2:iProver_and_2,X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_and_2:iProver_and_2,X2_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X1_iProver_'ki_accessible'_2_'ki_world',X2_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_exists_in_world(X0_iProver_'ki_accessible'_2_'ki_world',X0_iProver_and_2)|
% 7.79/1.52 ~'$ki_exists_in_world(X1_iProver_'ki_accessible'_2_'ki_world',X1_iProver_and_2)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world','$ki_local_world')|is_a_theorem(X2_iProver_'ki_accessible'_2_'ki_world',implies(X1_iProver_and_2,or(X0_iProver_and_2,X1_iProver_and_2)))),
% 7.79/1.52 inference(resolution,[status(thm)],[c_12370,c_10027])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12384,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X0_iProver_and_2:iProver_and_2,X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_and_2:iProver_and_2,X2_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_exists_in_world(X1_iProver_'ki_accessible'_2_'ki_world',X1_iProver_and_2)|
% 7.79/1.52 ~'$ki_exists_in_world(X0_iProver_'ki_accessible'_2_'ki_world',X0_iProver_and_2)|
% 7.79/1.52 ~'$ki_accessible'(X1_iProver_'ki_accessible'_2_'ki_world',X2_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 is_a_theorem(X2_iProver_'ki_accessible'_2_'ki_world',implies(X1_iProver_and_2,or(X0_iProver_and_2,X1_iProver_and_2)))),
% 7.79/1.52 inference(global_subsumption_just,[status(thm)],[c_12382,c_341,c_12382])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12385,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X0_iProver_and_2:iProver_and_2,X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_and_2:iProver_and_2,X2_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X1_iProver_'ki_accessible'_2_'ki_world',X2_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_exists_in_world(X0_iProver_'ki_accessible'_2_'ki_world',X0_iProver_and_2)|
% 7.79/1.52 ~'$ki_exists_in_world(X1_iProver_'ki_accessible'_2_'ki_world',X1_iProver_and_2)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 is_a_theorem(X2_iProver_'ki_accessible'_2_'ki_world',implies(X1_iProver_and_2,or(X0_iProver_and_2,X1_iProver_and_2)))),
% 7.79/1.52 inference(renaming,[status(thm)],[c_12384])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12473,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X2_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',sK160(X1_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_exists_in_world(X0_iProver_'ki_accessible'_2_'ki_world',sK159(X1_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_exists_in_world(X2_iProver_'ki_accessible'_2_'ki_world',sK157(X1_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(X2_iProver_'ki_accessible'_2_'ki_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X1_iProver_'ki_accessible'_2_'ki_world',sK188)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X2_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(resolution,[status(thm)],[c_12385,c_10336])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12527,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X2_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(sK156(X0_iProver_'ki_accessible'_2_'ki_world'),X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X1_iProver_'ki_accessible'_2_'ki_world',sK160(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_exists_in_world(X1_iProver_'ki_accessible'_2_'ki_world',sK159(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',sK156(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X2_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',sK188)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 r2(X2_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(resolution,[status(thm)],[c_12473,c_9926])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12566,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(sK156(X0_iProver_'ki_accessible'_2_'ki_world'),X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X1_iProver_'ki_accessible'_2_'ki_world',sK160(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_exists_in_world(X1_iProver_'ki_accessible'_2_'ki_world',sK159(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',sK156(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',sK188)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(resolution,[status(thm)],[c_12527,c_9876])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12574,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'(sK156(X0_iProver_'ki_accessible'_2_'ki_world'),sK158(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(sK158(X0_iProver_'ki_accessible'_2_'ki_world'),sK160(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',sK156(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',sK188)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 r2(X1_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(resolution,[status(thm)],[c_12566,c_9928])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12576,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world',X1_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'('$ki_local_world',sK156(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',X1_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',sK188)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')|
% 7.79/1.52 r2(X1_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(global_subsumption_just,
% 7.79/1.52 [status(thm)],
% 7.79/1.52 [c_12574,c_9927,c_9929,c_12574])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12584,plain,![X0_iProver_'ki_accessible'_2_'ki_world':iProver_'$ki_accessible'_2_'$ki_world']:
% 7.79/1.52 (~'$ki_accessible'('$ki_local_world',sK156(X0_iProver_'ki_accessible'_2_'ki_world'))|
% 7.79/1.52 ~'$ki_accessible'(X0_iProver_'ki_accessible'_2_'ki_world',sK188)|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_2_'ki_world')),
% 7.79/1.52 inference(resolution,[status(thm)],[c_12576,c_9876])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12585,plain,
% 7.79/1.52 (~'$ki_accessible'('$ki_local_world',sK156('$ki_local_world'))|~'$ki_accessible'('$ki_local_world','$ki_local_world')|
% 7.79/1.52 ~'$ki_accessible'('$ki_local_world',sK188)),
% 7.79/1.52 inference(instantiation,[status(thm)],[c_12584])).
% 7.79/1.52
% 7.79/1.52 tcf(c_12586,plain,
% 7.79/1.52 ($false),
% 7.79/1.52 inference(prop_impl_just,[status(thm)],[c_12585,c_8511,c_341,c_340])).
% 7.79/1.52
% 7.79/1.52
% 7.79/1.52 % SZS output end CNFRefutation for theBenchmark.p
% 7.79/1.52
% 7.79/1.52
%------------------------------------------------------------------------------