%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL941_5 : 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 : n001.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 3.18s 1.07s
% Output : CNFRefutation 3.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL941_5 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.35 % Computer : n001.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Thu Sep 24 00:47:36 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.39 Running first-order theorem proving
% 0.13/0.39 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.13/0.40
% 0.13/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.40
% 0.13/0.40 % Detected problem language: tptp
% 0.13/0.41 % Proving...
% 3.18/1.07 % SZS status Started for theBenchmark.p
% 3.18/1.07 % SZS status Theorem for theBenchmark.p
% 3.18/1.07
% 3.18/1.07 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.18/1.07
% 3.18/1.07 % ------ iProver source info
% 3.18/1.07
% 3.18/1.07 % git: date: 2026-07-19 20:42:38 +0200
% 3.18/1.07 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.18/1.07 % git: non_committed_changes: false
% 3.18/1.07
% 3.18/1.07 % ------ Parsing...
% 3.18/1.07 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 3.18/1.07 % ------ Proving...
% 3.18/1.07 % ------ Problem Properties
% 3.18/1.07
% 3.18/1.07 %
% 3.18/1.07 % clauses 332
% 3.18/1.07 % conjectures 37
% 3.18/1.07 % EPR 14
% 3.18/1.07 % Horn 256
% 3.18/1.07 % unary 4
% 3.18/1.07 % binary 214
% 3.18/1.07 % lits 1032
% 3.18/1.07 % lits eq 0
% 3.18/1.07 % fd_pure 0
% 3.18/1.07 % fd_pseudo 0
% 3.18/1.07 % fd_cond 0
% 3.18/1.07 % fd_pseudo_cond 0
% 3.18/1.07 % AC symbols 0
% 3.18/1.07
% 3.18/1.07 % ------ Input Options Time Limit: Unbounded
% 3.18/1.07
% 3.18/1.07
% 3.18/1.07 % ------
% 3.18/1.07 % Current options:
% 3.18/1.07 % ------
% 3.18/1.07
% 3.18/1.07
% 3.18/1.07 %
% 3.18/1.07
% 3.18/1.07 % ------ Proving...
% 3.18/1.07 %
% 3.18/1.07
% 3.18/1.07 % SZS status Theorem for theBenchmark.p
% 3.18/1.07
% 3.18/1.07 % SZS output start CNFRefutation for theBenchmark.p
% 3.18/1.07
% 3.18/1.07 tff(func_def_0, type, '$ki_local_world': '$ki_world').
% 3.18/1.07 tff(pred_def_1, type, '$ki_accessible': ('$ki_world' * '$ki_world') > $o).
% 3.18/1.07 tff(pred_def_2, type, qmltpeq: ('$ki_world' * $i * $i) > $o).
% 3.18/1.07 tff(pred_def_3, type, '$ki_exists_in_world_$i': ('$ki_world' * $i) > $o).
% 3.18/1.07 tff(pred_def_4, type, sP0: '$ki_world' > $o).
% 3.18/1.07 tff(pred_def_5, type, sP1: '$ki_world' > $o).
% 3.18/1.07 tff(pred_def_6, type, sP2: '$ki_world' > $o).
% 3.18/1.07 tff(func_def_8, type, sK7: '$ki_world' > $i).
% 3.18/1.07 tff(func_def_9, type, sK8: ($i * $i * '$ki_world') > '$ki_world').
% 3.18/1.07 tff(func_def_10, type, sK9: ($i * $i * '$ki_world') > '$ki_world').
% 3.18/1.07 tff(func_def_11, type, sK10: ($i * $i * '$ki_world') > '$ki_world').
% 3.18/1.07 tff(func_def_12, type, sK11: ($i * $i * '$ki_world') > '$ki_world').
% 3.18/1.07 tff(func_def_13, type, sK12: ($i * $i * '$ki_world') > '$ki_world').
% 3.18/1.07 tff(func_def_14, type, sK13: ($i * $i * '$ki_world') > '$ki_world').
% 3.18/1.07 tff(func_def_15, type, sK14: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_16, type, sK15: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_17, type, sK16: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_18, type, sK17: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_19, type, sK18: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_20, type, sK19: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_21, type, sK20: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_22, type, sK21: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_23, type, sK22: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_24, type, sK23: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_25, type, sK24: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_26, type, sK25: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_27, type, sK26: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_28, type, sK27: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_29, type, sK28: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_30, type, sK29: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_31, type, sK30: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_32, type, sK31: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_33, type, sK32: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_34, type, sK33: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_35, type, sK34: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_36, type, sK35: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_37, type, sK36: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_38, type, sK37: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_39, type, sK38: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_40, type, sK39: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_41, type, sK40: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_42, type, sK41: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_43, type, sK42: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_44, type, sK43: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_45, type, sK44: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_46, type, sK45: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_47, type, sK46: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_48, type, sK47: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_49, type, sK48: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_50, type, sK49: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_51, type, sK50: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_52, type, sK51: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_53, type, sK52: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_54, type, sK53: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_55, type, sK54: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_56, type, sK55: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_57, type, sK56: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_58, type, sK57: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_59, type, sK58: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_60, type, sK59: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_61, type, sK60: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_62, type, sK61: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_63, type, sK62: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_64, type, sK63: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_65, type, sK64: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_66, type, sK65: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_67, type, sK66: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_68, type, sK67: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_69, type, sK68: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_70, type, sK69: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_71, type, sK70: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_72, type, sK71: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_73, type, sK72: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_74, type, sK73: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_75, type, sK74: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_76, type, sK75: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_77, type, sK76: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_78, type, sK77: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_79, type, sK78: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_80, type, sK79: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_81, type, sK80: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_82, type, sK81: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_83, type, sK82: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_84, type, sK83: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_85, type, sK84: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_86, type, sK85: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_87, type, sK86: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_88, type, sK87: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_89, type, sK88: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_90, type, sK89: '$ki_world' > '$ki_world').
% 3.18/1.07 tff(func_def_91, type, sK90: '$ki_world').
% 3.18/1.07 tff(func_def_92, type, sK91: '$ki_world').
% 3.18/1.07 tff(func_def_93, type, sK92: '$ki_world').
% 3.18/1.07 tff(func_def_94, type, sK93: '$ki_world').
% 3.18/1.07 tff(func_def_95, type, sK94: '$ki_world').
% 3.18/1.07 tff(func_def_96, type, sK95: '$ki_world').
% 3.18/1.07 tff(func_def_97, type, sK96: '$ki_world').
% 3.18/1.07 tff(func_def_98, type, sK97: '$ki_world').
% 3.18/1.07 tff(func_def_99, type, sK98: '$ki_world').
% 3.18/1.07 tff(func_def_100, type, sK99: '$ki_world').
% 3.18/1.07 tff(func_def_101, type, sK100: '$ki_world').
% 3.18/1.07 tff(func_def_102, type, sK101: '$ki_world').
% 3.18/1.07 tff(func_def_103, type, sK102: '$ki_world').
% 3.18/1.07 tff(func_def_104, type, sK103: '$ki_world').
% 3.18/1.07 tff(func_def_105, type, sK104: '$ki_world').
% 3.18/1.07 tff(func_def_106, type, sK105: '$ki_world').
% 3.18/1.07 tff(func_def_107, type, sK106: '$ki_world').
% 3.18/1.07 tff(f1,axiom,(
% 3.18/1.07 ! [X0 : '$ki_world',X1 : '$ki_world'] : '$ki_accessible'(X0,X1)),
% 3.18/1.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mrel_universal)).
% 3.18/1.07
% 3.18/1.07 tff(f10,axiom,(
% 3.18/1.07 (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e0),e0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e0),e1)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e0),e2)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e0),e3))) & (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e1),e0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e1),e1)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e1),e2)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e1),e3))) & (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e2),e0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e2),e1)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e2),e2)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e2),e3))) & (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e3),e0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e3),e1)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e3),e2)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e3),e3))) & (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e0),e0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e0),e1)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e0),e2)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e0),e3))) & (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e1),e0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e1),e1)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e1),e2)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e1),e3))) & (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e2),e0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e2),e1)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e2),e2)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e2),e3))) & (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e3),e0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e3),e1)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e3),e2)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e3),e3))) & (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e0),e0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e0),e1)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e0),e2)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e0),e3))) & (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e1),e0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e1),e1)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e1),e2)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e1),e3))) & (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e2),e0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e2),e1)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e2),e2)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e2),e3))) & (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e3),e0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e3),e1)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e3),e2)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e3),e3))) & (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e0),e0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e0),e1)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e0),e2)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e0),e3))) & (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e1),e0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e1),e1)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e1),e2)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e1),e3))) & (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e2),e0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e2),e1)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e2),e2)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e2),e3))) & (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e3),e0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e3),e1)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e3),e2)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e3),e3)))),
% 3.18/1.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1)).
% 3.18/1.07
% 3.18/1.07 tff(f21,conjecture,(
% 3.18/1.07 (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e0),e0)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e1),e0)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e2),e0)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e3),e0))) | (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e0),e1)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e1),e1)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e2),e1)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e3),e1))) | (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e0),e2)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e1),e2)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e2),e2)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e3),e2))) | (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e0),e3)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e1),e3)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e2),e3)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e3),e3))) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ~((! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e0,e0),e0)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e1,e1),e0)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e2,e2),e0)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e3,e3),e0))) | (! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e0,e0),e1)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e1,e1),e1)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e2,e2),e1)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e3,e3),e1))) | (! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e0,e0),e2)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e1,e1),e2)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e2,e2),e2)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e3,e3),e2))) | (! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e0,e0),e3)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e1,e1),e3)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e2,e2),e3)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e3,e3),e3)))))),
% 3.18/1.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',verify)).
% 3.18/1.07
% 3.18/1.07 tff(f22,negated_conjecture,(
% 3.18/1.07 ~((! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e0),e0)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e1),e0)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e2),e0)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e3),e0))) | (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e0),e1)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e1),e1)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e2),e1)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e3),e1))) | (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e0),e2)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e1),e2)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e2),e2)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e3),e2))) | (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e0),e3)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e1,e1),e3)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e2,e2),e3)) & ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e3,e3),e3))) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ~((! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e0,e0),e0)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e1,e1),e0)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e2,e2),e0)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e3,e3),e0))) | (! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e0,e0),e1)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e1,e1),e1)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e2,e2),e1)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e3,e3),e1))) | (! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e0,e0),e2)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e1,e1),e2)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e2,e2),e2)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e3,e3),e2))) | (! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e0,e0),e3)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e1,e1),e3)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e2,e2),e3)) & ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => qmltpeq(X1,op(e3,e3),e3))))))),
% 3.18/1.07 inference(negated_conjecture,[status(cth)],[f21])).
% 3.18/1.07
% 3.18/1.07 tff(f28,plain,(
% 3.18/1.07 (! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e0),e0)) | ! [X1 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X1) => qmltpeq(X1,op(e0,e0),e1)) | ! [X2 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X2) => qmltpeq(X2,op(e0,e0),e2)) | ! [X3 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X3) => qmltpeq(X3,op(e0,e0),e3))) & (! [X4 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X4) => qmltpeq(X4,op(e0,e1),e0)) | ! [X5 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X5) => qmltpeq(X5,op(e0,e1),e1)) | ! [X6 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X6) => qmltpeq(X6,op(e0,e1),e2)) | ! [X7 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X7) => qmltpeq(X7,op(e0,e1),e3))) & (! [X8 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X8) => qmltpeq(X8,op(e0,e2),e0)) | ! [X9 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X9) => qmltpeq(X9,op(e0,e2),e1)) | ! [X10 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X10) => qmltpeq(X10,op(e0,e2),e2)) | ! [X11 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X11) => qmltpeq(X11,op(e0,e2),e3))) & (! [X12 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X12) => qmltpeq(X12,op(e0,e3),e0)) | ! [X13 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X13) => qmltpeq(X13,op(e0,e3),e1)) | ! [X14 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X14) => qmltpeq(X14,op(e0,e3),e2)) | ! [X15 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X15) => qmltpeq(X15,op(e0,e3),e3))) & (! [X16 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X16) => qmltpeq(X16,op(e1,e0),e0)) | ! [X17 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X17) => qmltpeq(X17,op(e1,e0),e1)) | ! [X18 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X18) => qmltpeq(X18,op(e1,e0),e2)) | ! [X19 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X19) => qmltpeq(X19,op(e1,e0),e3))) & (! [X20 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X20) => qmltpeq(X20,op(e1,e1),e0)) | ! [X21 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X21) => qmltpeq(X21,op(e1,e1),e1)) | ! [X22 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X22) => qmltpeq(X22,op(e1,e1),e2)) | ! [X23 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X23) => qmltpeq(X23,op(e1,e1),e3))) & (! [X24 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X24) => qmltpeq(X24,op(e1,e2),e0)) | ! [X25 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X25) => qmltpeq(X25,op(e1,e2),e1)) | ! [X26 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X26) => qmltpeq(X26,op(e1,e2),e2)) | ! [X27 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X27) => qmltpeq(X27,op(e1,e2),e3))) & (! [X28 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X28) => qmltpeq(X28,op(e1,e3),e0)) | ! [X29 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X29) => qmltpeq(X29,op(e1,e3),e1)) | ! [X30 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X30) => qmltpeq(X30,op(e1,e3),e2)) | ! [X31 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X31) => qmltpeq(X31,op(e1,e3),e3))) & (! [X32 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X32) => qmltpeq(X32,op(e2,e0),e0)) | ! [X33 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X33) => qmltpeq(X33,op(e2,e0),e1)) | ! [X34 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X34) => qmltpeq(X34,op(e2,e0),e2)) | ! [X35 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X35) => qmltpeq(X35,op(e2,e0),e3))) & (! [X36 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X36) => qmltpeq(X36,op(e2,e1),e0)) | ! [X37 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X37) => qmltpeq(X37,op(e2,e1),e1)) | ! [X38 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X38) => qmltpeq(X38,op(e2,e1),e2)) | ! [X39 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X39) => qmltpeq(X39,op(e2,e1),e3))) & (! [X40 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X40) => qmltpeq(X40,op(e2,e2),e0)) | ! [X41 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X41) => qmltpeq(X41,op(e2,e2),e1)) | ! [X42 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X42) => qmltpeq(X42,op(e2,e2),e2)) | ! [X43 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X43) => qmltpeq(X43,op(e2,e2),e3))) & (! [X44 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X44) => qmltpeq(X44,op(e2,e3),e0)) | ! [X45 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X45) => qmltpeq(X45,op(e2,e3),e1)) | ! [X46 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X46) => qmltpeq(X46,op(e2,e3),e2)) | ! [X47 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X47) => qmltpeq(X47,op(e2,e3),e3))) & (! [X48 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X48) => qmltpeq(X48,op(e3,e0),e0)) | ! [X49 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X49) => qmltpeq(X49,op(e3,e0),e1)) | ! [X50 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X50) => qmltpeq(X50,op(e3,e0),e2)) | ! [X51 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X51) => qmltpeq(X51,op(e3,e0),e3))) & (! [X52 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X52) => qmltpeq(X52,op(e3,e1),e0)) | ! [X53 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X53) => qmltpeq(X53,op(e3,e1),e1)) | ! [X54 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X54) => qmltpeq(X54,op(e3,e1),e2)) | ! [X55 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X55) => qmltpeq(X55,op(e3,e1),e3))) & (! [X56 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X56) => qmltpeq(X56,op(e3,e2),e0)) | ! [X57 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X57) => qmltpeq(X57,op(e3,e2),e1)) | ! [X58 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X58) => qmltpeq(X58,op(e3,e2),e2)) | ! [X59 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X59) => qmltpeq(X59,op(e3,e2),e3))) & (! [X60 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X60) => qmltpeq(X60,op(e3,e3),e0)) | ! [X61 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X61) => qmltpeq(X61,op(e3,e3),e1)) | ! [X62 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X62) => qmltpeq(X62,op(e3,e3),e2)) | ! [X63 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X63) => qmltpeq(X63,op(e3,e3),e3)))),
% 3.18/1.07 inference(rectify,[],[f10])).
% 3.18/1.07
% 3.18/1.07 tff(f37,plain,(
% 3.18/1.07 ~((! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => qmltpeq(X0,op(e0,e0),e0)) & ! [X1 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X1) => qmltpeq(X1,op(e1,e1),e0)) & ! [X2 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X2) => qmltpeq(X2,op(e2,e2),e0)) & ! [X3 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X3) => qmltpeq(X3,op(e3,e3),e0))) | (! [X4 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X4) => qmltpeq(X4,op(e0,e0),e1)) & ! [X5 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X5) => qmltpeq(X5,op(e1,e1),e1)) & ! [X6 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X6) => qmltpeq(X6,op(e2,e2),e1)) & ! [X7 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X7) => qmltpeq(X7,op(e3,e3),e1))) | (! [X8 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X8) => qmltpeq(X8,op(e0,e0),e2)) & ! [X9 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X9) => qmltpeq(X9,op(e1,e1),e2)) & ! [X10 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X10) => qmltpeq(X10,op(e2,e2),e2)) & ! [X11 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X11) => qmltpeq(X11,op(e3,e3),e2))) | (! [X12 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X12) => qmltpeq(X12,op(e0,e0),e3)) & ! [X13 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X13) => qmltpeq(X13,op(e1,e1),e3)) & ! [X14 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X14) => qmltpeq(X14,op(e2,e2),e3)) & ! [X15 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X15) => qmltpeq(X15,op(e3,e3),e3))) | ! [X16 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X16) => ~((! [X17 : '$ki_world'] : ('$ki_accessible'(X16,X17) => qmltpeq(X17,op(e0,e0),e0)) & ! [X18 : '$ki_world'] : ('$ki_accessible'(X16,X18) => qmltpeq(X18,op(e1,e1),e0)) & ! [X19 : '$ki_world'] : ('$ki_accessible'(X16,X19) => qmltpeq(X19,op(e2,e2),e0)) & ! [X20 : '$ki_world'] : ('$ki_accessible'(X16,X20) => qmltpeq(X20,op(e3,e3),e0))) | (! [X21 : '$ki_world'] : ('$ki_accessible'(X16,X21) => qmltpeq(X21,op(e0,e0),e1)) & ! [X22 : '$ki_world'] : ('$ki_accessible'(X16,X22) => qmltpeq(X22,op(e1,e1),e1)) & ! [X23 : '$ki_world'] : ('$ki_accessible'(X16,X23) => qmltpeq(X23,op(e2,e2),e1)) & ! [X24 : '$ki_world'] : ('$ki_accessible'(X16,X24) => qmltpeq(X24,op(e3,e3),e1))) | (! [X25 : '$ki_world'] : ('$ki_accessible'(X16,X25) => qmltpeq(X25,op(e0,e0),e2)) & ! [X26 : '$ki_world'] : ('$ki_accessible'(X16,X26) => qmltpeq(X26,op(e1,e1),e2)) & ! [X27 : '$ki_world'] : ('$ki_accessible'(X16,X27) => qmltpeq(X27,op(e2,e2),e2)) & ! [X28 : '$ki_world'] : ('$ki_accessible'(X16,X28) => qmltpeq(X28,op(e3,e3),e2))) | (! [X29 : '$ki_world'] : ('$ki_accessible'(X16,X29) => qmltpeq(X29,op(e0,e0),e3)) & ! [X30 : '$ki_world'] : ('$ki_accessible'(X16,X30) => qmltpeq(X30,op(e1,e1),e3)) & ! [X31 : '$ki_world'] : ('$ki_accessible'(X16,X31) => qmltpeq(X31,op(e2,e2),e3)) & ! [X32 : '$ki_world'] : ('$ki_accessible'(X16,X32) => qmltpeq(X32,op(e3,e3),e3))))))),
% 3.18/1.07 inference(rectify,[],[f22])).
% 3.18/1.07
% 3.18/1.07 tff(f49,plain,(
% 3.18/1.07 (! [X0 : '$ki_world'] : (qmltpeq(X0,op(e0,e0),e0) | ~'$ki_accessible'('$ki_local_world',X0)) | ! [X1 : '$ki_world'] : (qmltpeq(X1,op(e0,e0),e1) | ~'$ki_accessible'('$ki_local_world',X1)) | ! [X2 : '$ki_world'] : (qmltpeq(X2,op(e0,e0),e2) | ~'$ki_accessible'('$ki_local_world',X2)) | ! [X3 : '$ki_world'] : (qmltpeq(X3,op(e0,e0),e3) | ~'$ki_accessible'('$ki_local_world',X3))) & (! [X4 : '$ki_world'] : (qmltpeq(X4,op(e0,e1),e0) | ~'$ki_accessible'('$ki_local_world',X4)) | ! [X5 : '$ki_world'] : (qmltpeq(X5,op(e0,e1),e1) | ~'$ki_accessible'('$ki_local_world',X5)) | ! [X6 : '$ki_world'] : (qmltpeq(X6,op(e0,e1),e2) | ~'$ki_accessible'('$ki_local_world',X6)) | ! [X7 : '$ki_world'] : (qmltpeq(X7,op(e0,e1),e3) | ~'$ki_accessible'('$ki_local_world',X7))) & (! [X8 : '$ki_world'] : (qmltpeq(X8,op(e0,e2),e0) | ~'$ki_accessible'('$ki_local_world',X8)) | ! [X9 : '$ki_world'] : (qmltpeq(X9,op(e0,e2),e1) | ~'$ki_accessible'('$ki_local_world',X9)) | ! [X10 : '$ki_world'] : (qmltpeq(X10,op(e0,e2),e2) | ~'$ki_accessible'('$ki_local_world',X10)) | ! [X11 : '$ki_world'] : (qmltpeq(X11,op(e0,e2),e3) | ~'$ki_accessible'('$ki_local_world',X11))) & (! [X12 : '$ki_world'] : (qmltpeq(X12,op(e0,e3),e0) | ~'$ki_accessible'('$ki_local_world',X12)) | ! [X13 : '$ki_world'] : (qmltpeq(X13,op(e0,e3),e1) | ~'$ki_accessible'('$ki_local_world',X13)) | ! [X14 : '$ki_world'] : (qmltpeq(X14,op(e0,e3),e2) | ~'$ki_accessible'('$ki_local_world',X14)) | ! [X15 : '$ki_world'] : (qmltpeq(X15,op(e0,e3),e3) | ~'$ki_accessible'('$ki_local_world',X15))) & (! [X16 : '$ki_world'] : (qmltpeq(X16,op(e1,e0),e0) | ~'$ki_accessible'('$ki_local_world',X16)) | ! [X17 : '$ki_world'] : (qmltpeq(X17,op(e1,e0),e1) | ~'$ki_accessible'('$ki_local_world',X17)) | ! [X18 : '$ki_world'] : (qmltpeq(X18,op(e1,e0),e2) | ~'$ki_accessible'('$ki_local_world',X18)) | ! [X19 : '$ki_world'] : (qmltpeq(X19,op(e1,e0),e3) | ~'$ki_accessible'('$ki_local_world',X19))) & (! [X20 : '$ki_world'] : (qmltpeq(X20,op(e1,e1),e0) | ~'$ki_accessible'('$ki_local_world',X20)) | ! [X21 : '$ki_world'] : (qmltpeq(X21,op(e1,e1),e1) | ~'$ki_accessible'('$ki_local_world',X21)) | ! [X22 : '$ki_world'] : (qmltpeq(X22,op(e1,e1),e2) | ~'$ki_accessible'('$ki_local_world',X22)) | ! [X23 : '$ki_world'] : (qmltpeq(X23,op(e1,e1),e3) | ~'$ki_accessible'('$ki_local_world',X23))) & (! [X24 : '$ki_world'] : (qmltpeq(X24,op(e1,e2),e0) | ~'$ki_accessible'('$ki_local_world',X24)) | ! [X25 : '$ki_world'] : (qmltpeq(X25,op(e1,e2),e1) | ~'$ki_accessible'('$ki_local_world',X25)) | ! [X26 : '$ki_world'] : (qmltpeq(X26,op(e1,e2),e2) | ~'$ki_accessible'('$ki_local_world',X26)) | ! [X27 : '$ki_world'] : (qmltpeq(X27,op(e1,e2),e3) | ~'$ki_accessible'('$ki_local_world',X27))) & (! [X28 : '$ki_world'] : (qmltpeq(X28,op(e1,e3),e0) | ~'$ki_accessible'('$ki_local_world',X28)) | ! [X29 : '$ki_world'] : (qmltpeq(X29,op(e1,e3),e1) | ~'$ki_accessible'('$ki_local_world',X29)) | ! [X30 : '$ki_world'] : (qmltpeq(X30,op(e1,e3),e2) | ~'$ki_accessible'('$ki_local_world',X30)) | ! [X31 : '$ki_world'] : (qmltpeq(X31,op(e1,e3),e3) | ~'$ki_accessible'('$ki_local_world',X31))) & (! [X32 : '$ki_world'] : (qmltpeq(X32,op(e2,e0),e0) | ~'$ki_accessible'('$ki_local_world',X32)) | ! [X33 : '$ki_world'] : (qmltpeq(X33,op(e2,e0),e1) | ~'$ki_accessible'('$ki_local_world',X33)) | ! [X34 : '$ki_world'] : (qmltpeq(X34,op(e2,e0),e2) | ~'$ki_accessible'('$ki_local_world',X34)) | ! [X35 : '$ki_world'] : (qmltpeq(X35,op(e2,e0),e3) | ~'$ki_accessible'('$ki_local_world',X35))) & (! [X36 : '$ki_world'] : (qmltpeq(X36,op(e2,e1),e0) | ~'$ki_accessible'('$ki_local_world',X36)) | ! [X37 : '$ki_world'] : (qmltpeq(X37,op(e2,e1),e1) | ~'$ki_accessible'('$ki_local_world',X37)) | ! [X38 : '$ki_world'] : (qmltpeq(X38,op(e2,e1),e2) | ~'$ki_accessible'('$ki_local_world',X38)) | ! [X39 : '$ki_world'] : (qmltpeq(X39,op(e2,e1),e3) | ~'$ki_accessible'('$ki_local_world',X39))) & (! [X40 : '$ki_world'] : (qmltpeq(X40,op(e2,e2),e0) | ~'$ki_accessible'('$ki_local_world',X40)) | ! [X41 : '$ki_world'] : (qmltpeq(X41,op(e2,e2),e1) | ~'$ki_accessible'('$ki_local_world',X41)) | ! [X42 : '$ki_world'] : (qmltpeq(X42,op(e2,e2),e2) | ~'$ki_accessible'('$ki_local_world',X42)) | ! [X43 : '$ki_world'] : (qmltpeq(X43,op(e2,e2),e3) | ~'$ki_accessible'('$ki_local_world',X43))) & (! [X44 : '$ki_world'] : (qmltpeq(X44,op(e2,e3),e0) | ~'$ki_accessible'('$ki_local_world',X44)) | ! [X45 : '$ki_world'] : (qmltpeq(X45,op(e2,e3),e1) | ~'$ki_accessible'('$ki_local_world',X45)) | ! [X46 : '$ki_world'] : (qmltpeq(X46,op(e2,e3),e2) | ~'$ki_accessible'('$ki_local_world',X46)) | ! [X47 : '$ki_world'] : (qmltpeq(X47,op(e2,e3),e3) | ~'$ki_accessible'('$ki_local_world',X47))) & (! [X48 : '$ki_world'] : (qmltpeq(X48,op(e3,e0),e0) | ~'$ki_accessible'('$ki_local_world',X48)) | ! [X49 : '$ki_world'] : (qmltpeq(X49,op(e3,e0),e1) | ~'$ki_accessible'('$ki_local_world',X49)) | ! [X50 : '$ki_world'] : (qmltpeq(X50,op(e3,e0),e2) | ~'$ki_accessible'('$ki_local_world',X50)) | ! [X51 : '$ki_world'] : (qmltpeq(X51,op(e3,e0),e3) | ~'$ki_accessible'('$ki_local_world',X51))) & (! [X52 : '$ki_world'] : (qmltpeq(X52,op(e3,e1),e0) | ~'$ki_accessible'('$ki_local_world',X52)) | ! [X53 : '$ki_world'] : (qmltpeq(X53,op(e3,e1),e1) | ~'$ki_accessible'('$ki_local_world',X53)) | ! [X54 : '$ki_world'] : (qmltpeq(X54,op(e3,e1),e2) | ~'$ki_accessible'('$ki_local_world',X54)) | ! [X55 : '$ki_world'] : (qmltpeq(X55,op(e3,e1),e3) | ~'$ki_accessible'('$ki_local_world',X55))) & (! [X56 : '$ki_world'] : (qmltpeq(X56,op(e3,e2),e0) | ~'$ki_accessible'('$ki_local_world',X56)) | ! [X57 : '$ki_world'] : (qmltpeq(X57,op(e3,e2),e1) | ~'$ki_accessible'('$ki_local_world',X57)) | ! [X58 : '$ki_world'] : (qmltpeq(X58,op(e3,e2),e2) | ~'$ki_accessible'('$ki_local_world',X58)) | ! [X59 : '$ki_world'] : (qmltpeq(X59,op(e3,e2),e3) | ~'$ki_accessible'('$ki_local_world',X59))) & (! [X60 : '$ki_world'] : (qmltpeq(X60,op(e3,e3),e0) | ~'$ki_accessible'('$ki_local_world',X60)) | ! [X61 : '$ki_world'] : (qmltpeq(X61,op(e3,e3),e1) | ~'$ki_accessible'('$ki_local_world',X61)) | ! [X62 : '$ki_world'] : (qmltpeq(X62,op(e3,e3),e2) | ~'$ki_accessible'('$ki_local_world',X62)) | ! [X63 : '$ki_world'] : (qmltpeq(X63,op(e3,e3),e3) | ~'$ki_accessible'('$ki_local_world',X63)))),
% 3.18/1.07 inference(ennf_transformation,[],[f28])).
% 3.18/1.07
% 3.18/1.07 tff(f61,plain,(
% 3.18/1.07 (? [X0 : '$ki_world'] : (~qmltpeq(X0,op(e0,e0),e0) & '$ki_accessible'('$ki_local_world',X0)) | ? [X1 : '$ki_world'] : (~qmltpeq(X1,op(e1,e1),e0) & '$ki_accessible'('$ki_local_world',X1)) | ? [X2 : '$ki_world'] : (~qmltpeq(X2,op(e2,e2),e0) & '$ki_accessible'('$ki_local_world',X2)) | ? [X3 : '$ki_world'] : (~qmltpeq(X3,op(e3,e3),e0) & '$ki_accessible'('$ki_local_world',X3))) & (? [X4 : '$ki_world'] : (~qmltpeq(X4,op(e0,e0),e1) & '$ki_accessible'('$ki_local_world',X4)) | ? [X5 : '$ki_world'] : (~qmltpeq(X5,op(e1,e1),e1) & '$ki_accessible'('$ki_local_world',X5)) | ? [X6 : '$ki_world'] : (~qmltpeq(X6,op(e2,e2),e1) & '$ki_accessible'('$ki_local_world',X6)) | ? [X7 : '$ki_world'] : (~qmltpeq(X7,op(e3,e3),e1) & '$ki_accessible'('$ki_local_world',X7))) & (? [X8 : '$ki_world'] : (~qmltpeq(X8,op(e0,e0),e2) & '$ki_accessible'('$ki_local_world',X8)) | ? [X9 : '$ki_world'] : (~qmltpeq(X9,op(e1,e1),e2) & '$ki_accessible'('$ki_local_world',X9)) | ? [X10 : '$ki_world'] : (~qmltpeq(X10,op(e2,e2),e2) & '$ki_accessible'('$ki_local_world',X10)) | ? [X11 : '$ki_world'] : (~qmltpeq(X11,op(e3,e3),e2) & '$ki_accessible'('$ki_local_world',X11))) & (? [X12 : '$ki_world'] : (~qmltpeq(X12,op(e0,e0),e3) & '$ki_accessible'('$ki_local_world',X12)) | ? [X13 : '$ki_world'] : (~qmltpeq(X13,op(e1,e1),e3) & '$ki_accessible'('$ki_local_world',X13)) | ? [X14 : '$ki_world'] : (~qmltpeq(X14,op(e2,e2),e3) & '$ki_accessible'('$ki_local_world',X14)) | ? [X15 : '$ki_world'] : (~qmltpeq(X15,op(e3,e3),e3) & '$ki_accessible'('$ki_local_world',X15))) & ? [X16 : '$ki_world'] : (((! [X17 : '$ki_world'] : (qmltpeq(X17,op(e0,e0),e0) | ~'$ki_accessible'(X16,X17)) & ! [X18 : '$ki_world'] : (qmltpeq(X18,op(e1,e1),e0) | ~'$ki_accessible'(X16,X18)) & ! [X19 : '$ki_world'] : (qmltpeq(X19,op(e2,e2),e0) | ~'$ki_accessible'(X16,X19)) & ! [X20 : '$ki_world'] : (qmltpeq(X20,op(e3,e3),e0) | ~'$ki_accessible'(X16,X20))) | (! [X21 : '$ki_world'] : (qmltpeq(X21,op(e0,e0),e1) | ~'$ki_accessible'(X16,X21)) & ! [X22 : '$ki_world'] : (qmltpeq(X22,op(e1,e1),e1) | ~'$ki_accessible'(X16,X22)) & ! [X23 : '$ki_world'] : (qmltpeq(X23,op(e2,e2),e1) | ~'$ki_accessible'(X16,X23)) & ! [X24 : '$ki_world'] : (qmltpeq(X24,op(e3,e3),e1) | ~'$ki_accessible'(X16,X24))) | (! [X25 : '$ki_world'] : (qmltpeq(X25,op(e0,e0),e2) | ~'$ki_accessible'(X16,X25)) & ! [X26 : '$ki_world'] : (qmltpeq(X26,op(e1,e1),e2) | ~'$ki_accessible'(X16,X26)) & ! [X27 : '$ki_world'] : (qmltpeq(X27,op(e2,e2),e2) | ~'$ki_accessible'(X16,X27)) & ! [X28 : '$ki_world'] : (qmltpeq(X28,op(e3,e3),e2) | ~'$ki_accessible'(X16,X28))) | (! [X29 : '$ki_world'] : (qmltpeq(X29,op(e0,e0),e3) | ~'$ki_accessible'(X16,X29)) & ! [X30 : '$ki_world'] : (qmltpeq(X30,op(e1,e1),e3) | ~'$ki_accessible'(X16,X30)) & ! [X31 : '$ki_world'] : (qmltpeq(X31,op(e2,e2),e3) | ~'$ki_accessible'(X16,X31)) & ! [X32 : '$ki_world'] : (qmltpeq(X32,op(e3,e3),e3) | ~'$ki_accessible'(X16,X32)))) & '$ki_accessible'('$ki_local_world',X16))),
% 3.18/1.07 inference(ennf_transformation,[],[f37])).
% 3.18/1.07
% 3.18/1.07 tff(f86,plain,(
% 3.18/1.07 ? [X3 : '$ki_world'] : (~qmltpeq(X3,op(e3,e3),e0) & '$ki_accessible'('$ki_local_world',X3)) | ~sP6),
% 3.18/1.07 inference(nnf_transformation,[],[f68])).
% 3.18/1.07
% 3.18/1.07 tff(f87,plain,(
% 3.18/1.07 ? [X0 : '$ki_world'] : (~qmltpeq(X0,op(e3,e3),e0) & '$ki_accessible'('$ki_local_world',X0)) | ~sP6),
% 3.18/1.07 inference(rectify,[],[f86])).
% 3.18/1.07
% 3.18/1.07 tff(f88,plain,(
% 3.18/1.07 (~qmltpeq(sK90,op(e3,e3),e0) & '$ki_accessible'('$ki_local_world',sK90)) | ~sP6),
% 3.18/1.07 inference(skolemize,[status(esa),new_symbols(skolem,[sK90]),skolemize(X0,sK90)],[f87])).
% 3.18/1.07
% 3.18/1.07 tff(f89,plain,(
% 3.18/1.07 ? [X7 : '$ki_world'] : (~qmltpeq(X7,op(e3,e3),e1) & '$ki_accessible'('$ki_local_world',X7)) | ~sP5),
% 3.18/1.07 inference(nnf_transformation,[],[f67])).
% 3.18/1.07
% 3.18/1.07 tff(f90,plain,(
% 3.18/1.07 ? [X0 : '$ki_world'] : (~qmltpeq(X0,op(e3,e3),e1) & '$ki_accessible'('$ki_local_world',X0)) | ~sP5),
% 3.18/1.07 inference(rectify,[],[f89])).
% 3.18/1.07
% 3.18/1.07 tff(f91,plain,(
% 3.18/1.07 (~qmltpeq(sK91,op(e3,e3),e1) & '$ki_accessible'('$ki_local_world',sK91)) | ~sP5),
% 3.18/1.07 inference(skolemize,[status(esa),new_symbols(skolem,[sK91]),skolemize(X0,sK91)],[f90])).
% 3.18/1.07
% 3.18/1.07 tff(f92,plain,(
% 3.18/1.07 ? [X11 : '$ki_world'] : (~qmltpeq(X11,op(e3,e3),e2) & '$ki_accessible'('$ki_local_world',X11)) | ~sP4),
% 3.18/1.07 inference(nnf_transformation,[],[f66])).
% 3.18/1.07
% 3.18/1.07 tff(f93,plain,(
% 3.18/1.07 ? [X0 : '$ki_world'] : (~qmltpeq(X0,op(e3,e3),e2) & '$ki_accessible'('$ki_local_world',X0)) | ~sP4),
% 3.18/1.07 inference(rectify,[],[f92])).
% 3.18/1.07
% 3.18/1.07 tff(f94,plain,(
% 3.18/1.07 (~qmltpeq(sK92,op(e3,e3),e2) & '$ki_accessible'('$ki_local_world',sK92)) | ~sP4),
% 3.18/1.07 inference(skolemize,[status(esa),new_symbols(skolem,[sK92]),skolemize(X0,sK92)],[f93])).
% 3.18/1.07
% 3.18/1.07 tff(f95,plain,(
% 3.18/1.07 ? [X15 : '$ki_world'] : (~qmltpeq(X15,op(e3,e3),e3) & '$ki_accessible'('$ki_local_world',X15)) | ~sP3),
% 3.18/1.07 inference(nnf_transformation,[],[f65])).
% 3.18/1.07
% 3.18/1.07 tff(f96,plain,(
% 3.18/1.07 ? [X0 : '$ki_world'] : (~qmltpeq(X0,op(e3,e3),e3) & '$ki_accessible'('$ki_local_world',X0)) | ~sP3),
% 3.18/1.07 inference(rectify,[],[f95])).
% 3.18/1.07
% 3.18/1.07 tff(f97,plain,(
% 3.18/1.07 (~qmltpeq(sK93,op(e3,e3),e3) & '$ki_accessible'('$ki_local_world',sK93)) | ~sP3),
% 3.18/1.07 inference(skolemize,[status(esa),new_symbols(skolem,[sK93]),skolemize(X0,sK93)],[f96])).
% 3.18/1.07
% 3.18/1.07 tff(f98,plain,(
% 3.18/1.07 ! [X16 : '$ki_world'] : ((! [X21 : '$ki_world'] : (qmltpeq(X21,op(e0,e0),e1) | ~'$ki_accessible'(X16,X21)) & ! [X22 : '$ki_world'] : (qmltpeq(X22,op(e1,e1),e1) | ~'$ki_accessible'(X16,X22)) & ! [X23 : '$ki_world'] : (qmltpeq(X23,op(e2,e2),e1) | ~'$ki_accessible'(X16,X23)) & ! [X24 : '$ki_world'] : (qmltpeq(X24,op(e3,e3),e1) | ~'$ki_accessible'(X16,X24))) | ~sP2(X16))),
% 3.18/1.07 inference(nnf_transformation,[],[f64])).
% 3.18/1.07
% 3.18/1.07 tff(f99,plain,(
% 3.18/1.07 ! [X0 : '$ki_world'] : ((! [X1 : '$ki_world'] : (qmltpeq(X1,op(e0,e0),e1) | ~'$ki_accessible'(X0,X1)) & ! [X2 : '$ki_world'] : (qmltpeq(X2,op(e1,e1),e1) | ~'$ki_accessible'(X0,X2)) & ! [X3 : '$ki_world'] : (qmltpeq(X3,op(e2,e2),e1) | ~'$ki_accessible'(X0,X3)) & ! [X4 : '$ki_world'] : (qmltpeq(X4,op(e3,e3),e1) | ~'$ki_accessible'(X0,X4))) | ~sP2(X0))),
% 3.18/1.07 inference(rectify,[],[f98])).
% 3.18/1.07
% 3.18/1.07 tff(f100,plain,(
% 3.18/1.07 ! [X16 : '$ki_world'] : ((! [X25 : '$ki_world'] : (qmltpeq(X25,op(e0,e0),e2) | ~'$ki_accessible'(X16,X25)) & ! [X26 : '$ki_world'] : (qmltpeq(X26,op(e1,e1),e2) | ~'$ki_accessible'(X16,X26)) & ! [X27 : '$ki_world'] : (qmltpeq(X27,op(e2,e2),e2) | ~'$ki_accessible'(X16,X27)) & ! [X28 : '$ki_world'] : (qmltpeq(X28,op(e3,e3),e2) | ~'$ki_accessible'(X16,X28))) | ~sP1(X16))),
% 3.18/1.07 inference(nnf_transformation,[],[f63])).
% 3.18/1.07
% 3.18/1.07 tff(f101,plain,(
% 3.18/1.07 ! [X0 : '$ki_world'] : ((! [X1 : '$ki_world'] : (qmltpeq(X1,op(e0,e0),e2) | ~'$ki_accessible'(X0,X1)) & ! [X2 : '$ki_world'] : (qmltpeq(X2,op(e1,e1),e2) | ~'$ki_accessible'(X0,X2)) & ! [X3 : '$ki_world'] : (qmltpeq(X3,op(e2,e2),e2) | ~'$ki_accessible'(X0,X3)) & ! [X4 : '$ki_world'] : (qmltpeq(X4,op(e3,e3),e2) | ~'$ki_accessible'(X0,X4))) | ~sP1(X0))),
% 3.18/1.07 inference(rectify,[],[f100])).
% 3.18/1.07
% 3.18/1.07 tff(f104,plain,(
% 3.18/1.07 (? [X0 : '$ki_world'] : (~qmltpeq(X0,op(e0,e0),e0) & '$ki_accessible'('$ki_local_world',X0)) | ? [X1 : '$ki_world'] : (~qmltpeq(X1,op(e1,e1),e0) & '$ki_accessible'('$ki_local_world',X1)) | ? [X2 : '$ki_world'] : (~qmltpeq(X2,op(e2,e2),e0) & '$ki_accessible'('$ki_local_world',X2)) | sP6) & (? [X3 : '$ki_world'] : (~qmltpeq(X3,op(e0,e0),e1) & '$ki_accessible'('$ki_local_world',X3)) | ? [X4 : '$ki_world'] : (~qmltpeq(X4,op(e1,e1),e1) & '$ki_accessible'('$ki_local_world',X4)) | ? [X5 : '$ki_world'] : (~qmltpeq(X5,op(e2,e2),e1) & '$ki_accessible'('$ki_local_world',X5)) | sP5) & (? [X6 : '$ki_world'] : (~qmltpeq(X6,op(e0,e0),e2) & '$ki_accessible'('$ki_local_world',X6)) | ? [X7 : '$ki_world'] : (~qmltpeq(X7,op(e1,e1),e2) & '$ki_accessible'('$ki_local_world',X7)) | ? [X8 : '$ki_world'] : (~qmltpeq(X8,op(e2,e2),e2) & '$ki_accessible'('$ki_local_world',X8)) | sP4) & (? [X9 : '$ki_world'] : (~qmltpeq(X9,op(e0,e0),e3) & '$ki_accessible'('$ki_local_world',X9)) | ? [X10 : '$ki_world'] : (~qmltpeq(X10,op(e1,e1),e3) & '$ki_accessible'('$ki_local_world',X10)) | ? [X11 : '$ki_world'] : (~qmltpeq(X11,op(e2,e2),e3) & '$ki_accessible'('$ki_local_world',X11)) | sP3) & ? [X12 : '$ki_world'] : (((! [X13 : '$ki_world'] : (qmltpeq(X13,op(e0,e0),e0) | ~'$ki_accessible'(X12,X13)) & ! [X14 : '$ki_world'] : (qmltpeq(X14,op(e1,e1),e0) | ~'$ki_accessible'(X12,X14)) & ! [X15 : '$ki_world'] : (qmltpeq(X15,op(e2,e2),e0) | ~'$ki_accessible'(X12,X15)) & ! [X16 : '$ki_world'] : (qmltpeq(X16,op(e3,e3),e0) | ~'$ki_accessible'(X12,X16))) | sP2(X12) | sP1(X12) | sP0(X12)) & '$ki_accessible'('$ki_local_world',X12))),
% 3.18/1.07 inference(rectify,[],[f69])).
% 3.18/1.07
% 3.18/1.07 tff(f105,plain,(
% 3.18/1.07 ((~qmltpeq(sK94,op(e0,e0),e0) & '$ki_accessible'('$ki_local_world',sK94)) | (~qmltpeq(sK95,op(e1,e1),e0) & '$ki_accessible'('$ki_local_world',sK95)) | (~qmltpeq(sK96,op(e2,e2),e0) & '$ki_accessible'('$ki_local_world',sK96)) | sP6) & ((~qmltpeq(sK97,op(e0,e0),e1) & '$ki_accessible'('$ki_local_world',sK97)) | (~qmltpeq(sK98,op(e1,e1),e1) & '$ki_accessible'('$ki_local_world',sK98)) | (~qmltpeq(sK99,op(e2,e2),e1) & '$ki_accessible'('$ki_local_world',sK99)) | sP5) & ((~qmltpeq(sK100,op(e0,e0),e2) & '$ki_accessible'('$ki_local_world',sK100)) | (~qmltpeq(sK101,op(e1,e1),e2) & '$ki_accessible'('$ki_local_world',sK101)) | (~qmltpeq(sK102,op(e2,e2),e2) & '$ki_accessible'('$ki_local_world',sK102)) | sP4) & ((~qmltpeq(sK103,op(e0,e0),e3) & '$ki_accessible'('$ki_local_world',sK103)) | (~qmltpeq(sK104,op(e1,e1),e3) & '$ki_accessible'('$ki_local_world',sK104)) | (~qmltpeq(sK105,op(e2,e2),e3) & '$ki_accessible'('$ki_local_world',sK105)) | sP3) & (((! [X13 : '$ki_world'] : (qmltpeq(X13,op(e0,e0),e0) | ~'$ki_accessible'(sK106,X13)) & ! [X14 : '$ki_world'] : (qmltpeq(X14,op(e1,e1),e0) | ~'$ki_accessible'(sK106,X14)) & ! [X15 : '$ki_world'] : (qmltpeq(X15,op(e2,e2),e0) | ~'$ki_accessible'(sK106,X15)) & ! [X16 : '$ki_world'] : (qmltpeq(X16,op(e3,e3),e0) | ~'$ki_accessible'(sK106,X16))) | sP2(sK106) | sP1(sK106) | sP0(sK106)) & '$ki_accessible'('$ki_local_world',sK106))),
% 3.18/1.07 inference(skolemize,[status(esa),new_symbols(skolem,[sK94,sK95,sK96,sK97,sK98,sK99,sK100,sK101,sK102,sK103,sK104,sK105,sK106]),skolemize(X0,sK94),skolemize(X1,sK95),skolemize(X2,sK96),skolemize(X3,sK97),skolemize(X4,sK98),skolemize(X5,sK99),skolemize(X6,sK100),skolemize(X7,sK101),skolemize(X8,sK102),skolemize(X9,sK103),skolemize(X10,sK104),skolemize(X11,sK105),skolemize(X12,sK106)],[f104])).
% 3.18/1.07
% 3.18/1.07 tff(f106,plain,(
% 3.18/1.07 ( ! [X0 : '$ki_world',X1 : '$ki_world'] : ('$ki_accessible'(X0,X1)) )),
% 3.18/1.07 inference(cnf_transformation,[],[f1])).
% 3.18/1.07
% 3.18/1.07 tff(f127,plain,(
% 3.18/1.07 ( ! [X40 : '$ki_world',X41 : '$ki_world',X42 : '$ki_world',X43 : '$ki_world'] : (qmltpeq(X40,op(e2,e2),e0) | ~'$ki_accessible'('$ki_local_world',X40) | qmltpeq(X41,op(e2,e2),e1) | ~'$ki_accessible'('$ki_local_world',X41) | qmltpeq(X42,op(e2,e2),e2) | ~'$ki_accessible'('$ki_local_world',X42) | qmltpeq(X43,op(e2,e2),e3) | ~'$ki_accessible'('$ki_local_world',X43)) )),
% 3.18/1.07 inference(cnf_transformation,[],[f49])).
% 3.18/1.07
% 3.18/1.07 tff(f132,plain,(
% 3.18/1.07 ( ! [X21 : '$ki_world',X22 : '$ki_world',X23 : '$ki_world',X20 : '$ki_world'] : (qmltpeq(X20,op(e1,e1),e0) | ~'$ki_accessible'('$ki_local_world',X20) | qmltpeq(X21,op(e1,e1),e1) | ~'$ki_accessible'('$ki_local_world',X21) | qmltpeq(X22,op(e1,e1),e2) | ~'$ki_accessible'('$ki_local_world',X22) | qmltpeq(X23,op(e1,e1),e3) | ~'$ki_accessible'('$ki_local_world',X23)) )),
% 3.18/1.07 inference(cnf_transformation,[],[f49])).
% 3.18/1.07
% 3.18/1.07 tff(f137,plain,(
% 3.18/1.07 ( ! [X2 : '$ki_world',X3 : '$ki_world',X0 : '$ki_world',X1 : '$ki_world'] : (qmltpeq(X0,op(e0,e0),e0) | ~'$ki_accessible'('$ki_local_world',X0) | qmltpeq(X1,op(e0,e0),e1) | ~'$ki_accessible'('$ki_local_world',X1) | qmltpeq(X2,op(e0,e0),e2) | ~'$ki_accessible'('$ki_local_world',X2) | qmltpeq(X3,op(e0,e0),e3) | ~'$ki_accessible'('$ki_local_world',X3)) )),
% 3.18/1.07 inference(cnf_transformation,[],[f49])).
% 3.18/1.07
% 3.18/1.07 tff(f382,plain,(
% 3.18/1.07 ~qmltpeq(sK90,op(e3,e3),e0) | ~sP6),
% 3.18/1.07 inference(cnf_transformation,[],[f88])).
% 3.18/1.07
% 3.18/1.07 tff(f384,plain,(
% 3.18/1.07 ~qmltpeq(sK91,op(e3,e3),e1) | ~sP5),
% 3.18/1.07 inference(cnf_transformation,[],[f91])).
% 3.18/1.07
% 3.18/1.07 tff(f386,plain,(
% 3.18/1.07 ~qmltpeq(sK92,op(e3,e3),e2) | ~sP4),
% 3.18/1.07 inference(cnf_transformation,[],[f94])).
% 3.18/1.07
% 3.18/1.07 tff(f388,plain,(
% 3.18/1.07 ~qmltpeq(sK93,op(e3,e3),e3) | ~sP3),
% 3.18/1.07 inference(cnf_transformation,[],[f97])).
% 3.18/1.07
% 3.18/1.07 tff(f389,plain,(
% 3.18/1.07 ( ! [X0 : '$ki_world',X4 : '$ki_world'] : (qmltpeq(X4,op(e3,e3),e1) | ~'$ki_accessible'(X0,X4) | ~sP2(X0)) )),
% 3.18/1.07 inference(cnf_transformation,[],[f99])).
% 3.18/1.07
% 3.18/1.07 tff(f390,plain,(
% 3.18/1.07 ( ! [X3 : '$ki_world',X0 : '$ki_world'] : (qmltpeq(X3,op(e2,e2),e1) | ~'$ki_accessible'(X0,X3) | ~sP2(X0)) )),
% 3.18/1.07 inference(cnf_transformation,[],[f99])).
% 3.18/1.07
% 3.18/1.07 tff(f391,plain,(
% 3.18/1.07 ( ! [X2 : '$ki_world',X0 : '$ki_world'] : (qmltpeq(X2,op(e1,e1),e1) | ~'$ki_accessible'(X0,X2) | ~sP2(X0)) )),
% 3.18/1.07 inference(cnf_transformation,[],[f99])).
% 3.18/1.07
% 3.18/1.07 tff(f392,plain,(
% 3.18/1.07 ( ! [X0 : '$ki_world',X1 : '$ki_world'] : (qmltpeq(X1,op(e0,e0),e1) | ~'$ki_accessible'(X0,X1) | ~sP2(X0)) )),
% 3.18/1.07 inference(cnf_transformation,[],[f99])).
% 3.18/1.07
% 3.18/1.07 tff(f393,plain,(
% 3.18/1.07 ( ! [X0 : '$ki_world',X4 : '$ki_world'] : (qmltpeq(X4,op(e3,e3),e2) | ~'$ki_accessible'(X0,X4) | ~sP1(X0)) )),
% 3.18/1.07 inference(cnf_transformation,[],[f101])).
% 3.18/1.07
% 3.18/1.07 tff(f394,plain,(
% 3.18/1.07 ( ! [X3 : '$ki_world',X0 : '$ki_world'] : (qmltpeq(X3,op(e2,e2),e2) | ~'$ki_accessible'(X0,X3) | ~sP1(X0)) )),
% 3.18/1.07 inference(cnf_transformation,[],[f101])).
% 3.18/1.07
% 3.18/1.07 tff(f395,plain,(
% 3.18/1.07 ( ! [X2 : '$ki_world',X0 : '$ki_world'] : (qmltpeq(X2,op(e1,e1),e2) | ~'$ki_accessible'(X0,X2) | ~sP1(X0)) )),
% 3.18/1.07 inference(cnf_transformation,[],[f101])).
% 3.18/1.07
% 3.18/1.07 tff(f396,plain,(
% 3.18/1.07 ( ! [X0 : '$ki_world',X1 : '$ki_world'] : (qmltpeq(X1,op(e0,e0),e2) | ~'$ki_accessible'(X0,X1) | ~sP1(X0)) )),
% 3.18/1.07 inference(cnf_transformation,[],[f101])).
% 3.18/1.07
% 3.18/1.07 tff(f402,plain,(
% 3.18/1.07 ( ! [X16 : '$ki_world'] : (qmltpeq(X16,op(e3,e3),e0) | ~'$ki_accessible'(sK106,X16) | sP2(sK106) | sP1(sK106) | sP0(sK106)) )),
% 3.18/1.07 inference(cnf_transformation,[],[f105])).
% 3.18/1.07
% 3.18/1.07 tff(f403,plain,(
% 3.18/1.07 ( ! [X15 : '$ki_world'] : (qmltpeq(X15,op(e2,e2),e0) | ~'$ki_accessible'(sK106,X15) | sP2(sK106) | sP1(sK106) | sP0(sK106)) )),
% 3.18/1.07 inference(cnf_transformation,[],[f105])).
% 3.18/1.07
% 3.18/1.07 tff(f404,plain,(
% 3.18/1.07 ( ! [X14 : '$ki_world'] : (qmltpeq(X14,op(e1,e1),e0) | ~'$ki_accessible'(sK106,X14) | sP2(sK106) | sP1(sK106) | sP0(sK106)) )),
% 3.18/1.07 inference(cnf_transformation,[],[f105])).
% 3.18/1.07
% 3.18/1.07 tff(f405,plain,(
% 3.18/1.07 ( ! [X13 : '$ki_world'] : (qmltpeq(X13,op(e0,e0),e0) | ~'$ki_accessible'(sK106,X13) | sP2(sK106) | sP1(sK106) | sP0(sK106)) )),
% 3.18/1.07 inference(cnf_transformation,[],[f105])).
% 3.18/1.07
% 3.18/1.07 tff(f413,plain,(
% 3.18/1.07 ~qmltpeq(sK103,op(e0,e0),e3) | ~qmltpeq(sK104,op(e1,e1),e3) | ~qmltpeq(sK105,op(e2,e2),e3) | sP3),
% 3.18/1.07 inference(cnf_transformation,[],[f105])).
% 3.18/1.07
% 3.18/1.07 tff(f421,plain,(
% 3.18/1.07 ~qmltpeq(sK100,op(e0,e0),e2) | ~qmltpeq(sK101,op(e1,e1),e2) | ~qmltpeq(sK102,op(e2,e2),e2) | sP4),
% 3.18/1.07 inference(cnf_transformation,[],[f105])).
% 3.18/1.07
% 3.18/1.07 tff(f429,plain,(
% 3.18/1.07 ~qmltpeq(sK97,op(e0,e0),e1) | ~qmltpeq(sK98,op(e1,e1),e1) | ~qmltpeq(sK99,op(e2,e2),e1) | sP5),
% 3.18/1.07 inference(cnf_transformation,[],[f105])).
% 3.18/1.07
% 3.18/1.07 tff(f437,plain,(
% 3.18/1.07 ~qmltpeq(sK94,op(e0,e0),e0) | ~qmltpeq(sK95,op(e1,e1),e0) | ~qmltpeq(sK96,op(e2,e2),e0) | sP6),
% 3.18/1.07 inference(cnf_transformation,[],[f105])).
% 3.18/1.07
% 3.18/1.07 tcf(c_49,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 ('$ki_accessible'(X0_'ki_world',X1_'ki_world')),
% 3.18/1.07 inference(cnf_transformation,[],[f106])).
% 3.18/1.07
% 3.18/1.07 tcf(c_65,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world',X3_'ki_world':'$ki_world']:
% 3.18/1.07 (~'$ki_accessible'('$ki_local_world',X0_'ki_world')|~'$ki_accessible'('$ki_local_world',X1_'ki_world')|
% 3.18/1.07 ~'$ki_accessible'('$ki_local_world',X2_'ki_world')|~'$ki_accessible'('$ki_local_world',X3_'ki_world')|
% 3.18/1.07 qmltpeq(X0_'ki_world',op(e0,e0),e0)|qmltpeq(X1_'ki_world',op(e0,e0),e3)|
% 3.18/1.07 qmltpeq(X2_'ki_world',op(e0,e0),e2)|qmltpeq(X3_'ki_world',op(e0,e0),e1)),
% 3.18/1.07 inference(cnf_transformation,[],[f137])).
% 3.18/1.07
% 3.18/1.07 tcf(c_70,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world',X3_'ki_world':'$ki_world']:
% 3.18/1.07 (~'$ki_accessible'('$ki_local_world',X0_'ki_world')|~'$ki_accessible'('$ki_local_world',X1_'ki_world')|
% 3.18/1.07 ~'$ki_accessible'('$ki_local_world',X2_'ki_world')|~'$ki_accessible'('$ki_local_world',X3_'ki_world')|
% 3.18/1.07 qmltpeq(X0_'ki_world',op(e1,e1),e0)|qmltpeq(X1_'ki_world',op(e1,e1),e1)|
% 3.18/1.07 qmltpeq(X2_'ki_world',op(e1,e1),e3)|qmltpeq(X3_'ki_world',op(e1,e1),e2)),
% 3.18/1.07 inference(cnf_transformation,[],[f132])).
% 3.18/1.07
% 3.18/1.07 tcf(c_75,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world',X3_'ki_world':'$ki_world']:
% 3.18/1.07 (~'$ki_accessible'('$ki_local_world',X0_'ki_world')|~'$ki_accessible'('$ki_local_world',X1_'ki_world')|
% 3.18/1.07 ~'$ki_accessible'('$ki_local_world',X2_'ki_world')|~'$ki_accessible'('$ki_local_world',X3_'ki_world')|
% 3.18/1.07 qmltpeq(X0_'ki_world',op(e2,e2),e1)|qmltpeq(X1_'ki_world',op(e2,e2),e0)|
% 3.18/1.07 qmltpeq(X2_'ki_world',op(e2,e2),e2)|qmltpeq(X3_'ki_world',op(e2,e2),e3)),
% 3.18/1.07 inference(cnf_transformation,[],[f127])).
% 3.18/1.07
% 3.18/1.07 tcf(c_324,plain,
% 3.18/1.07 (~qmltpeq(sK90,op(e3,e3),e0)|~sP6),
% 3.18/1.07 inference(cnf_transformation,[],[f382])).
% 3.18/1.07
% 3.18/1.07 tcf(c_326,plain,
% 3.18/1.07 (~qmltpeq(sK91,op(e3,e3),e1)|~sP5),
% 3.18/1.07 inference(cnf_transformation,[],[f384])).
% 3.18/1.07
% 3.18/1.07 tcf(c_328,plain,
% 3.18/1.07 (~qmltpeq(sK92,op(e3,e3),e2)|~sP4),
% 3.18/1.07 inference(cnf_transformation,[],[f386])).
% 3.18/1.07
% 3.18/1.07 tcf(c_330,plain,
% 3.18/1.07 (~qmltpeq(sK93,op(e3,e3),e3)|~sP3),
% 3.18/1.07 inference(cnf_transformation,[],[f388])).
% 3.18/1.07
% 3.18/1.07 tcf(c_332,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~sP2(X0_'ki_world')|
% 3.18/1.07 qmltpeq(X1_'ki_world',op(e0,e0),e1)),
% 3.18/1.07 inference(cnf_transformation,[],[f392])).
% 3.18/1.07
% 3.18/1.07 tcf(c_333,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~sP2(X0_'ki_world')|
% 3.18/1.07 qmltpeq(X1_'ki_world',op(e1,e1),e1)),
% 3.18/1.07 inference(cnf_transformation,[],[f391])).
% 3.18/1.07
% 3.18/1.07 tcf(c_334,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~sP2(X0_'ki_world')|
% 3.18/1.07 qmltpeq(X1_'ki_world',op(e2,e2),e1)),
% 3.18/1.07 inference(cnf_transformation,[],[f390])).
% 3.18/1.07
% 3.18/1.07 tcf(c_335,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~sP2(X0_'ki_world')|
% 3.18/1.07 qmltpeq(X1_'ki_world',op(e3,e3),e1)),
% 3.18/1.07 inference(cnf_transformation,[],[f389])).
% 3.18/1.07
% 3.18/1.07 tcf(c_336,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~sP1(X0_'ki_world')|
% 3.18/1.07 qmltpeq(X1_'ki_world',op(e0,e0),e2)),
% 3.18/1.07 inference(cnf_transformation,[],[f396])).
% 3.18/1.07
% 3.18/1.07 tcf(c_337,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~sP1(X0_'ki_world')|
% 3.18/1.07 qmltpeq(X1_'ki_world',op(e1,e1),e2)),
% 3.18/1.07 inference(cnf_transformation,[],[f395])).
% 3.18/1.07
% 3.18/1.07 tcf(c_338,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~sP1(X0_'ki_world')|
% 3.18/1.07 qmltpeq(X1_'ki_world',op(e2,e2),e2)),
% 3.18/1.07 inference(cnf_transformation,[],[f394])).
% 3.18/1.07
% 3.18/1.07 tcf(c_339,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~sP1(X0_'ki_world')|
% 3.18/1.07 qmltpeq(X1_'ki_world',op(e3,e3),e2)),
% 3.18/1.07 inference(cnf_transformation,[],[f393])).
% 3.18/1.07
% 3.18/1.07 tcf(c_344,negated_conjecture,
% 3.18/1.07 (~qmltpeq(sK94,op(e0,e0),e0)|~qmltpeq(sK95,op(e1,e1),e0)|~qmltpeq(sK96,op(e2,e2),e0)|
% 3.18/1.07 sP6),
% 3.18/1.07 inference(cnf_transformation,[],[f437])).
% 3.18/1.07
% 3.18/1.07 tcf(c_352,negated_conjecture,
% 3.18/1.07 (~qmltpeq(sK97,op(e0,e0),e1)|~qmltpeq(sK98,op(e1,e1),e1)|~qmltpeq(sK99,op(e2,e2),e1)|
% 3.18/1.07 sP5),
% 3.18/1.07 inference(cnf_transformation,[],[f429])).
% 3.18/1.07
% 3.18/1.07 tcf(c_360,negated_conjecture,
% 3.18/1.07 (~qmltpeq(sK100,op(e0,e0),e2)|~qmltpeq(sK101,op(e1,e1),e2)|~qmltpeq(sK102,op(e2,e2),e2)|
% 3.18/1.07 sP4),
% 3.18/1.07 inference(cnf_transformation,[],[f421])).
% 3.18/1.07
% 3.18/1.07 tcf(c_368,negated_conjecture,
% 3.18/1.07 (~qmltpeq(sK103,op(e0,e0),e3)|~qmltpeq(sK104,op(e1,e1),e3)|~qmltpeq(sK105,op(e2,e2),e3)|
% 3.18/1.07 sP3),
% 3.18/1.07 inference(cnf_transformation,[],[f413])).
% 3.18/1.07
% 3.18/1.07 tcf(c_376,negated_conjecture,![X0_'ki_world':'$ki_world']:
% 3.18/1.07 (~'$ki_accessible'(sK106,X0_'ki_world')|qmltpeq(X0_'ki_world',op(e0,e0),e0)|
% 3.18/1.07 sP0(sK106)|sP1(sK106)|sP2(sK106)),
% 3.18/1.07 inference(cnf_transformation,[],[f405])).
% 3.18/1.07
% 3.18/1.07 tcf(c_377,negated_conjecture,![X0_'ki_world':'$ki_world']:
% 3.18/1.07 (~'$ki_accessible'(sK106,X0_'ki_world')|qmltpeq(X0_'ki_world',op(e1,e1),e0)|
% 3.18/1.07 sP0(sK106)|sP1(sK106)|sP2(sK106)),
% 3.18/1.07 inference(cnf_transformation,[],[f404])).
% 3.18/1.07
% 3.18/1.07 tcf(c_378,negated_conjecture,![X0_'ki_world':'$ki_world']:
% 3.18/1.07 (~'$ki_accessible'(sK106,X0_'ki_world')|qmltpeq(X0_'ki_world',op(e2,e2),e0)|
% 3.18/1.07 sP0(sK106)|sP1(sK106)|sP2(sK106)),
% 3.18/1.07 inference(cnf_transformation,[],[f403])).
% 3.18/1.07
% 3.18/1.07 tcf(c_379,negated_conjecture,![X0_'ki_world':'$ki_world']:
% 3.18/1.07 (~'$ki_accessible'(sK106,X0_'ki_world')|qmltpeq(X0_'ki_world',op(e3,e3),e0)|
% 3.18/1.07 sP0(sK106)|sP1(sK106)|sP2(sK106)),
% 3.18/1.07 inference(cnf_transformation,[],[f402])).
% 3.18/1.07
% 3.18/1.07 tcf(c_536,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 (~sP1(X0_'ki_world')|qmltpeq(X1_'ki_world',op(e3,e3),e2)),
% 3.18/1.07 inference(global_subsumption_just,[status(thm)],[c_339,c_49,c_339])).
% 3.18/1.07
% 3.18/1.07 tcf(c_543,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 (~sP1(X0_'ki_world')|qmltpeq(X1_'ki_world',op(e2,e2),e2)),
% 3.18/1.07 inference(global_subsumption_just,[status(thm)],[c_338,c_49,c_338])).
% 3.18/1.07
% 3.18/1.07 tcf(c_550,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 (~sP1(X0_'ki_world')|qmltpeq(X1_'ki_world',op(e1,e1),e2)),
% 3.18/1.07 inference(global_subsumption_just,[status(thm)],[c_337,c_49,c_337])).
% 3.18/1.07
% 3.18/1.07 tcf(c_557,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 (~sP1(X0_'ki_world')|qmltpeq(X1_'ki_world',op(e0,e0),e2)),
% 3.18/1.07 inference(global_subsumption_just,[status(thm)],[c_336,c_49,c_336])).
% 3.18/1.07
% 3.18/1.07 tcf(c_564,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 (~sP2(X0_'ki_world')|qmltpeq(X1_'ki_world',op(e3,e3),e1)),
% 3.18/1.07 inference(global_subsumption_just,[status(thm)],[c_335,c_49,c_335])).
% 3.18/1.07
% 3.18/1.07 tcf(c_571,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 (~sP2(X0_'ki_world')|qmltpeq(X1_'ki_world',op(e2,e2),e1)),
% 3.18/1.07 inference(global_subsumption_just,[status(thm)],[c_334,c_49,c_334])).
% 3.18/1.07
% 3.18/1.07 tcf(c_578,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 (~sP2(X0_'ki_world')|qmltpeq(X1_'ki_world',op(e1,e1),e1)),
% 3.18/1.07 inference(global_subsumption_just,[status(thm)],[c_333,c_49,c_333])).
% 3.18/1.07
% 3.18/1.07 tcf(c_585,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.07 (~sP2(X0_'ki_world')|qmltpeq(X1_'ki_world',op(e0,e0),e1)),
% 3.18/1.07 inference(global_subsumption_just,[status(thm)],[c_332,c_49,c_332])).
% 3.18/1.07
% 3.18/1.07 tcf(c_645,plain,![X0_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e3,e3),e0)|sP0(sK106)|sP1(sK106)|sP2(sK106)),
% 3.18/1.07 inference(forward_subsumption_resolution,[status(thm)],[c_379,c_49])).
% 3.18/1.07
% 3.18/1.07 tcf(c_654,plain,
% 3.18/1.07 (~sP6|sP0(sK106)|sP1(sK106)|sP2(sK106)),
% 3.18/1.07 inference(superposition,[status(thm)],[c_645,c_324])).
% 3.18/1.07
% 3.18/1.07 tcf(c_660,plain,![X0_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e2,e2),e0)|sP0(sK106)|sP1(sK106)|sP2(sK106)),
% 3.18/1.07 inference(forward_subsumption_resolution,[status(thm)],[c_378,c_49])).
% 3.18/1.07
% 3.18/1.07 tcf(c_674,plain,![X0_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e1,e1),e0)|sP0(sK106)|sP1(sK106)|sP2(sK106)),
% 3.18/1.07 inference(forward_subsumption_resolution,[status(thm)],[c_377,c_49])).
% 3.18/1.07
% 3.18/1.07 tcf(c_688,plain,![X0_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e0,e0),e0)|sP0(sK106)|sP1(sK106)|sP2(sK106)),
% 3.18/1.07 inference(forward_subsumption_resolution,[status(thm)],[c_376,c_49])).
% 3.18/1.07
% 3.18/1.07 tcf(c_969,plain,
% 3.18/1.07 (~qmltpeq(sK95,op(e1,e1),e0)|~qmltpeq(sK96,op(e2,e2),e0)|sP0(sK106)|
% 3.18/1.07 sP1(sK106)|sP2(sK106)|sP6),
% 3.18/1.07 inference(superposition,[status(thm)],[c_688,c_344])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1071,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world',X3_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e2,e2),e1)|qmltpeq(X1_'ki_world',op(e2,e2),e0)|
% 3.18/1.07 qmltpeq(X2_'ki_world',op(e2,e2),e2)|qmltpeq(X3_'ki_world',op(e2,e2),e3)),
% 3.18/1.07 inference(forward_subsumption_resolution,
% 3.18/1.07 [status(thm)],
% 3.18/1.07 [c_75,c_49,c_49,c_49,c_49])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1156,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world',X3_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e1,e1),e0)|qmltpeq(X1_'ki_world',op(e1,e1),e1)|
% 3.18/1.07 qmltpeq(X2_'ki_world',op(e1,e1),e3)|qmltpeq(X3_'ki_world',op(e1,e1),e2)),
% 3.18/1.07 inference(forward_subsumption_resolution,
% 3.18/1.07 [status(thm)],
% 3.18/1.07 [c_70,c_49,c_49,c_49,c_49])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1241,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world',X3_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e0,e0),e0)|qmltpeq(X1_'ki_world',op(e0,e0),e3)|
% 3.18/1.07 qmltpeq(X2_'ki_world',op(e0,e0),e2)|qmltpeq(X3_'ki_world',op(e0,e0),e1)),
% 3.18/1.07 inference(forward_subsumption_resolution,
% 3.18/1.07 [status(thm)],
% 3.18/1.07 [c_65,c_49,c_49,c_49,c_49])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1250,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world']:
% 3.18/1.07 (~qmltpeq(sK98,op(e1,e1),e1)|~qmltpeq(sK99,op(e2,e2),e1)|qmltpeq(X0_'ki_world',op(e0,e0),e0)|
% 3.18/1.07 qmltpeq(X1_'ki_world',op(e0,e0),e3)|qmltpeq(X2_'ki_world',op(e0,e0),e2)|
% 3.18/1.07 sP5),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1241,c_352])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1251,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world']:
% 3.18/1.07 (~qmltpeq(sK101,op(e1,e1),e2)|~qmltpeq(sK102,op(e2,e2),e2)|qmltpeq(X0_'ki_world',op(e0,e0),e0)|
% 3.18/1.07 qmltpeq(X1_'ki_world',op(e0,e0),e3)|qmltpeq(X2_'ki_world',op(e0,e0),e1)|
% 3.18/1.07 sP4),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1241,c_360])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1253,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world']:
% 3.18/1.07 (~qmltpeq(sK95,op(e1,e1),e0)|~qmltpeq(sK96,op(e2,e2),e0)|qmltpeq(X0_'ki_world',op(e0,e0),e3)|
% 3.18/1.07 qmltpeq(X1_'ki_world',op(e0,e0),e2)|qmltpeq(X2_'ki_world',op(e0,e0),e1)|
% 3.18/1.07 sP6),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1241,c_344])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1274,plain,
% 3.18/1.07 (sP2(sK106)|sP1(sK106)|sP0(sK106)|~qmltpeq(sK96,op(e2,e2),e0)|~qmltpeq(sK95,op(e1,e1),e0)),
% 3.18/1.07 inference(global_subsumption_just,[status(thm)],[c_969,c_654,c_969])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1275,plain,
% 3.18/1.07 (~qmltpeq(sK95,op(e1,e1),e0)|~qmltpeq(sK96,op(e2,e2),e0)|sP0(sK106)|
% 3.18/1.07 sP1(sK106)|sP2(sK106)),
% 3.18/1.07 inference(renaming,[status(thm)],[c_1274])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1281,plain,
% 3.18/1.07 (sP0(sK106)|sP1(sK106)|sP2(sK106)),
% 3.18/1.07 inference(forward_subsumption_resolution,
% 3.18/1.07 [status(thm)],
% 3.18/1.07 [c_1275,c_660,c_674])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1291,plain,![X0_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e0,e0),e1)|sP0(sK106)|sP1(sK106)),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1281,c_585])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1292,plain,![X0_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e1,e1),e1)|sP0(sK106)|sP1(sK106)),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1281,c_578])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1293,plain,![X0_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e2,e2),e1)|sP0(sK106)|sP1(sK106)),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1281,c_571])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1294,plain,![X0_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e3,e3),e1)|sP0(sK106)|sP1(sK106)),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1281,c_564])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1361,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world',X3_'ki_world':'$ki_world',X4_'ki_world':'$ki_world',X5_'ki_world':'$ki_world']:
% 3.18/1.07 (~qmltpeq(sK96,op(e2,e2),e0)|qmltpeq(X0_'ki_world',op(e1,e1),e1)|
% 3.18/1.07 qmltpeq(X1_'ki_world',op(e1,e1),e3)|qmltpeq(X2_'ki_world',op(e1,e1),e2)|
% 3.18/1.07 qmltpeq(X3_'ki_world',op(e0,e0),e3)|qmltpeq(X4_'ki_world',op(e0,e0),e2)|
% 3.18/1.07 qmltpeq(X5_'ki_world',op(e0,e0),e1)|sP6),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1156,c_1253])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1389,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world',X3_'ki_world':'$ki_world',X4_'ki_world':'$ki_world',X5_'ki_world':'$ki_world']:
% 3.18/1.07 (~qmltpeq(sK102,op(e2,e2),e2)|qmltpeq(X0_'ki_world',op(e1,e1),e0)|
% 3.18/1.07 qmltpeq(X1_'ki_world',op(e1,e1),e1)|qmltpeq(X2_'ki_world',op(e1,e1),e3)|
% 3.18/1.07 qmltpeq(X3_'ki_world',op(e0,e0),e0)|qmltpeq(X4_'ki_world',op(e0,e0),e3)|
% 3.18/1.07 qmltpeq(X5_'ki_world',op(e0,e0),e1)|sP4),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1156,c_1251])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1419,plain,
% 3.18/1.07 (~sP5|sP0(sK106)|sP1(sK106)),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1294,c_326])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1432,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world']:
% 3.18/1.07 (~qmltpeq(sK99,op(e2,e2),e1)|qmltpeq(X0_'ki_world',op(e0,e0),e0)|
% 3.18/1.07 qmltpeq(X1_'ki_world',op(e0,e0),e3)|qmltpeq(X2_'ki_world',op(e0,e0),e2)|
% 3.18/1.07 sP0(sK106)|sP1(sK106)|sP5),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1292,c_1250])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1440,plain,
% 3.18/1.07 (~qmltpeq(sK98,op(e1,e1),e1)|~qmltpeq(sK99,op(e2,e2),e1)|sP0(sK106)|
% 3.18/1.07 sP1(sK106)|sP5),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1291,c_352])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1521,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world',X3_'ki_world':'$ki_world',X4_'ki_world':'$ki_world',X5_'ki_world':'$ki_world',X6_'ki_world':'$ki_world',X7_'ki_world':'$ki_world',X8_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e2,e2),e1)|qmltpeq(X1_'ki_world',op(e2,e2),e2)|
% 3.18/1.07 qmltpeq(X2_'ki_world',op(e2,e2),e3)|qmltpeq(X3_'ki_world',op(e1,e1),e1)|
% 3.18/1.07 qmltpeq(X4_'ki_world',op(e1,e1),e3)|qmltpeq(X5_'ki_world',op(e1,e1),e2)|
% 3.18/1.07 qmltpeq(X6_'ki_world',op(e0,e0),e3)|qmltpeq(X7_'ki_world',op(e0,e0),e2)|
% 3.18/1.07 qmltpeq(X8_'ki_world',op(e0,e0),e1)|sP6),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1071,c_1361])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1593,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world']:
% 3.18/1.07 (sP1(sK106)|sP0(sK106)|qmltpeq(X2_'ki_world',op(e0,e0),e2)|qmltpeq(X1_'ki_world',op(e0,e0),e3)|
% 3.18/1.07 qmltpeq(X0_'ki_world',op(e0,e0),e0)|~qmltpeq(sK99,op(e2,e2),e1)),
% 3.18/1.07 inference(global_subsumption_just,[status(thm)],[c_1432,c_1419,c_1432])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1594,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world']:
% 3.18/1.07 (~qmltpeq(sK99,op(e2,e2),e1)|qmltpeq(X0_'ki_world',op(e0,e0),e0)|
% 3.18/1.07 qmltpeq(X1_'ki_world',op(e0,e0),e3)|qmltpeq(X2_'ki_world',op(e0,e0),e2)|
% 3.18/1.07 sP0(sK106)|sP1(sK106)),
% 3.18/1.07 inference(renaming,[status(thm)],[c_1593])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1618,plain,
% 3.18/1.07 (sP1(sK106)|sP0(sK106)|~qmltpeq(sK99,op(e2,e2),e1)|~qmltpeq(sK98,op(e1,e1),e1)),
% 3.18/1.07 inference(global_subsumption_just,[status(thm)],[c_1440,c_1419,c_1440])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1619,plain,
% 3.18/1.07 (~qmltpeq(sK98,op(e1,e1),e1)|~qmltpeq(sK99,op(e2,e2),e1)|sP0(sK106)|
% 3.18/1.07 sP1(sK106)),
% 3.18/1.07 inference(renaming,[status(thm)],[c_1618])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1624,plain,
% 3.18/1.07 (sP0(sK106)|sP1(sK106)),
% 3.18/1.07 inference(forward_subsumption_resolution,
% 3.18/1.07 [status(thm)],
% 3.18/1.07 [c_1619,c_1293,c_1292])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1631,plain,![X0_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e0,e0),e2)|sP0(sK106)),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1624,c_557])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1632,plain,![X0_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e1,e1),e2)|sP0(sK106)),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1624,c_550])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1633,plain,![X0_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e2,e2),e2)|sP0(sK106)),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1624,c_543])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1634,plain,![X0_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e3,e3),e2)|sP0(sK106)),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1624,c_536])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1699,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world',X3_'ki_world':'$ki_world',X4_'ki_world':'$ki_world',X5_'ki_world':'$ki_world',X6_'ki_world':'$ki_world',X7_'ki_world':'$ki_world',X8_'ki_world':'$ki_world',X9_'ki_world':'$ki_world',X10_'ki_world':'$ki_world',X11_'ki_world':'$ki_world',X12_'ki_world':'$ki_world',X13_'ki_world':'$ki_world']:
% 3.18/1.07 (qmltpeq(X0_'ki_world',op(e2,e2),e1)|qmltpeq(X1_'ki_world',op(e2,e2),e3)|
% 3.18/1.07 qmltpeq(X2_'ki_world',op(e1,e1),e1)|qmltpeq(X3_'ki_world',op(e1,e1),e3)|
% 3.18/1.07 qmltpeq(X4_'ki_world',op(e1,e1),e2)|qmltpeq(X5_'ki_world',op(e0,e0),e3)|
% 3.18/1.07 qmltpeq(X6_'ki_world',op(e0,e0),e2)|qmltpeq(X7_'ki_world',op(e0,e0),e1)|
% 3.18/1.07 qmltpeq(X8_'ki_world',op(e1,e1),e0)|qmltpeq(X9_'ki_world',op(e1,e1),e1)|
% 3.18/1.07 qmltpeq(X10_'ki_world',op(e1,e1),e3)|qmltpeq(X11_'ki_world',op(e0,e0),e0)|
% 3.18/1.07 qmltpeq(X12_'ki_world',op(e0,e0),e3)|qmltpeq(X13_'ki_world',op(e0,e0),e1)|
% 3.18/1.07 sP6|sP4),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1521,c_1389])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1855,plain,
% 3.18/1.07 (~sP4|sP0(sK106)),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1634,c_328])).
% 3.18/1.07
% 3.18/1.07 tcf(c_1870,plain,
% 3.18/1.07 (~qmltpeq(sK101,op(e1,e1),e2)|~qmltpeq(sK102,op(e2,e2),e2)|sP0(sK106)|
% 3.18/1.07 sP4),
% 3.18/1.07 inference(superposition,[status(thm)],[c_1631,c_360])).
% 3.18/1.07
% 3.18/1.07 tcf(c_2505,plain,
% 3.18/1.07 (sP0(sK106)|~qmltpeq(sK102,op(e2,e2),e2)|~qmltpeq(sK101,op(e1,e1),e2)),
% 3.18/1.07 inference(global_subsumption_just,[status(thm)],[c_1870,c_1855,c_1870])).
% 3.18/1.07
% 3.18/1.07 tcf(c_2506,plain,
% 3.18/1.07 (~qmltpeq(sK101,op(e1,e1),e2)|~qmltpeq(sK102,op(e2,e2),e2)|sP0(sK106)),
% 3.18/1.07 inference(renaming,[status(thm)],[c_2505])).
% 3.18/1.07
% 3.18/1.07 tcf(c_2510,plain,
% 3.18/1.07 (sP0(sK106)),
% 3.18/1.07 inference(forward_subsumption_resolution,
% 3.18/1.07 [status(thm)],
% 3.18/1.07 [c_2506,c_1633,c_1632])).
% 3.18/1.08
% 3.18/1.08 tff(f62,definition,(
% 3.18/1.08 ! [X16 : '$ki_world'] : ((! [X29 : '$ki_world'] : (qmltpeq(X29,op(e0,e0),e3) | ~'$ki_accessible'(X16,X29)) & ! [X30 : '$ki_world'] : (qmltpeq(X30,op(e1,e1),e3) | ~'$ki_accessible'(X16,X30)) & ! [X31 : '$ki_world'] : (qmltpeq(X31,op(e2,e2),e3) | ~'$ki_accessible'(X16,X31)) & ! [X32 : '$ki_world'] : (qmltpeq(X32,op(e3,e3),e3) | ~'$ki_accessible'(X16,X32))) | ~ sP0(X16))),
% 3.18/1.08 introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction])).
% 3.18/1.08 tff(f63,definition,(
% 3.18/1.08 ! [X16 : '$ki_world'] : ((! [X25 : '$ki_world'] : (qmltpeq(X25,op(e0,e0),e2) | ~'$ki_accessible'(X16,X25)) & ! [X26 : '$ki_world'] : (qmltpeq(X26,op(e1,e1),e2) | ~'$ki_accessible'(X16,X26)) & ! [X27 : '$ki_world'] : (qmltpeq(X27,op(e2,e2),e2) | ~'$ki_accessible'(X16,X27)) & ! [X28 : '$ki_world'] : (qmltpeq(X28,op(e3,e3),e2) | ~'$ki_accessible'(X16,X28))) | ~ sP1(X16))),
% 3.18/1.08 introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction])).
% 3.18/1.08 tff(f64,definition,(
% 3.18/1.08 ! [X16 : '$ki_world'] : ((! [X21 : '$ki_world'] : (qmltpeq(X21,op(e0,e0),e1) | ~'$ki_accessible'(X16,X21)) & ! [X22 : '$ki_world'] : (qmltpeq(X22,op(e1,e1),e1) | ~'$ki_accessible'(X16,X22)) & ! [X23 : '$ki_world'] : (qmltpeq(X23,op(e2,e2),e1) | ~'$ki_accessible'(X16,X23)) & ! [X24 : '$ki_world'] : (qmltpeq(X24,op(e3,e3),e1) | ~'$ki_accessible'(X16,X24))) | ~ sP2(X16))),
% 3.18/1.08 introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction])).
% 3.18/1.08 tff(f65,definition,(
% 3.18/1.08 ? [X15 : '$ki_world'] : (~qmltpeq(X15,op(e3,e3),e3) & '$ki_accessible'('$ki_local_world',X15)) | ~ sP3),
% 3.18/1.08 introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction])).
% 3.18/1.08 tff(f66,definition,(
% 3.18/1.08 ? [X11 : '$ki_world'] : (~qmltpeq(X11,op(e3,e3),e2) & '$ki_accessible'('$ki_local_world',X11)) | ~ sP4),
% 3.18/1.08 introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction])).
% 3.18/1.08 tff(f67,definition,(
% 3.18/1.08 ? [X7 : '$ki_world'] : (~qmltpeq(X7,op(e3,e3),e1) & '$ki_accessible'('$ki_local_world',X7)) | ~ sP5),
% 3.18/1.08 introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction])).
% 3.18/1.08 tff(f68,definition,(
% 3.18/1.08 ? [X3 : '$ki_world'] : (~qmltpeq(X3,op(e3,e3),e0) & '$ki_accessible'('$ki_local_world',X3)) | ~ sP6),
% 3.18/1.08 introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction])).
% 3.18/1.08 tff(f69,plain,(
% 3.18/1.08 (? [X0 : '$ki_world'] : (~qmltpeq(X0,op(e0,e0),e0) & '$ki_accessible'('$ki_local_world',X0)) | ? [X1 : '$ki_world'] : (~qmltpeq(X1,op(e1,e1),e0) & '$ki_accessible'('$ki_local_world',X1)) | ? [X2 : '$ki_world'] : (~qmltpeq(X2,op(e2,e2),e0) & '$ki_accessible'('$ki_local_world',X2)) | sP6) & (? [X4 : '$ki_world'] : (~qmltpeq(X4,op(e0,e0),e1) & '$ki_accessible'('$ki_local_world',X4)) | ? [X5 : '$ki_world'] : (~qmltpeq(X5,op(e1,e1),e1) & '$ki_accessible'('$ki_local_world',X5)) | ? [X6 : '$ki_world'] : (~qmltpeq(X6,op(e2,e2),e1) & '$ki_accessible'('$ki_local_world',X6)) | sP5) & (? [X8 : '$ki_world'] : (~qmltpeq(X8,op(e0,e0),e2) & '$ki_accessible'('$ki_local_world',X8)) | ? [X9 : '$ki_world'] : (~qmltpeq(X9,op(e1,e1),e2) & '$ki_accessible'('$ki_local_world',X9)) | ? [X10 : '$ki_world'] : (~qmltpeq(X10,op(e2,e2),e2) & '$ki_accessible'('$ki_local_world',X10)) | sP4) & (? [X12 : '$ki_world'] : (~qmltpeq(X12,op(e0,e0),e3) & '$ki_accessible'('$ki_local_world',X12)) | ? [X13 : '$ki_world'] : (~qmltpeq(X13,op(e1,e1),e3) & '$ki_accessible'('$ki_local_world',X13)) | ? [X14 : '$ki_world'] : (~qmltpeq(X14,op(e2,e2),e3) & '$ki_accessible'('$ki_local_world',X14)) | sP3) & ? [X16 : '$ki_world'] : (((! [X17 : '$ki_world'] : (qmltpeq(X17,op(e0,e0),e0) | ~'$ki_accessible'(X16,X17)) & ! [X18 : '$ki_world'] : (qmltpeq(X18,op(e1,e1),e0) | ~'$ki_accessible'(X16,X18)) & ! [X19 : '$ki_world'] : (qmltpeq(X19,op(e2,e2),e0) | ~'$ki_accessible'(X16,X19)) & ! [X20 : '$ki_world'] : (qmltpeq(X20,op(e3,e3),e0) | ~'$ki_accessible'(X16,X20))) | sP2(X16) | sP1(X16) | sP0(X16)) & '$ki_accessible'('$ki_local_world',X16))),
% 3.18/1.08 inference(definition_folding,[],[f61,f68,f67,f66,f65,f64,f63,f62])).
% 3.18/1.08
% 3.18/1.08 tff(f102,plain,(
% 3.18/1.08 ! [X16 : '$ki_world'] : ((! [X29 : '$ki_world'] : (qmltpeq(X29,op(e0,e0),e3) | ~'$ki_accessible'(X16,X29)) & ! [X30 : '$ki_world'] : (qmltpeq(X30,op(e1,e1),e3) | ~'$ki_accessible'(X16,X30)) & ! [X31 : '$ki_world'] : (qmltpeq(X31,op(e2,e2),e3) | ~'$ki_accessible'(X16,X31)) & ! [X32 : '$ki_world'] : (qmltpeq(X32,op(e3,e3),e3) | ~'$ki_accessible'(X16,X32))) | ~sP0(X16))),
% 3.18/1.08 inference(nnf_transformation,[],[f62])).
% 3.18/1.08
% 3.18/1.08 tff(f103,plain,(
% 3.18/1.08 ! [X0 : '$ki_world'] : ((! [X1 : '$ki_world'] : (qmltpeq(X1,op(e0,e0),e3) | ~'$ki_accessible'(X0,X1)) & ! [X2 : '$ki_world'] : (qmltpeq(X2,op(e1,e1),e3) | ~'$ki_accessible'(X0,X2)) & ! [X3 : '$ki_world'] : (qmltpeq(X3,op(e2,e2),e3) | ~'$ki_accessible'(X0,X3)) & ! [X4 : '$ki_world'] : (qmltpeq(X4,op(e3,e3),e3) | ~'$ki_accessible'(X0,X4))) | ~sP0(X0))),
% 3.18/1.08 inference(rectify,[],[f102])).
% 3.18/1.08
% 3.18/1.08 tff(f397,plain,(
% 3.18/1.08 ( ! [X0 : '$ki_world',X4 : '$ki_world'] : (qmltpeq(X4,op(e3,e3),e3) | ~'$ki_accessible'(X0,X4) | ~sP0(X0)) )),
% 3.18/1.08 inference(cnf_transformation,[],[f103])).
% 3.18/1.08
% 3.18/1.08 tff(f398,plain,(
% 3.18/1.08 ( ! [X3 : '$ki_world',X0 : '$ki_world'] : (qmltpeq(X3,op(e2,e2),e3) | ~'$ki_accessible'(X0,X3) | ~sP0(X0)) )),
% 3.18/1.08 inference(cnf_transformation,[],[f103])).
% 3.18/1.08
% 3.18/1.08 tff(f399,plain,(
% 3.18/1.08 ( ! [X2 : '$ki_world',X0 : '$ki_world'] : (qmltpeq(X2,op(e1,e1),e3) | ~'$ki_accessible'(X0,X2) | ~sP0(X0)) )),
% 3.18/1.08 inference(cnf_transformation,[],[f103])).
% 3.18/1.08
% 3.18/1.08 tff(f400,plain,(
% 3.18/1.08 ( ! [X0 : '$ki_world',X1 : '$ki_world'] : (qmltpeq(X1,op(e0,e0),e3) | ~'$ki_accessible'(X0,X1) | ~sP0(X0)) )),
% 3.18/1.08 inference(cnf_transformation,[],[f103])).
% 3.18/1.08
% 3.18/1.08 tcf(c_340,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.08 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~sP0(X0_'ki_world')|
% 3.18/1.08 qmltpeq(X1_'ki_world',op(e0,e0),e3)),
% 3.18/1.08 inference(cnf_transformation,[],[f400])).
% 3.18/1.08
% 3.18/1.08 tcf(c_341,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.08 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~sP0(X0_'ki_world')|
% 3.18/1.08 qmltpeq(X1_'ki_world',op(e1,e1),e3)),
% 3.18/1.08 inference(cnf_transformation,[],[f399])).
% 3.18/1.08
% 3.18/1.08 tcf(c_342,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.08 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~sP0(X0_'ki_world')|
% 3.18/1.08 qmltpeq(X1_'ki_world',op(e2,e2),e3)),
% 3.18/1.08 inference(cnf_transformation,[],[f398])).
% 3.18/1.08
% 3.18/1.08 tcf(c_343,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.08 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~sP0(X0_'ki_world')|
% 3.18/1.08 qmltpeq(X1_'ki_world',op(e3,e3),e3)),
% 3.18/1.08 inference(cnf_transformation,[],[f397])).
% 3.18/1.08
% 3.18/1.08 tcf(c_508,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.08 (~sP0(X0_'ki_world')|qmltpeq(X1_'ki_world',op(e3,e3),e3)),
% 3.18/1.08 inference(global_subsumption_just,[status(thm)],[c_343,c_49,c_343])).
% 3.18/1.08
% 3.18/1.08 tcf(c_515,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.08 (~sP0(X0_'ki_world')|qmltpeq(X1_'ki_world',op(e2,e2),e3)),
% 3.18/1.08 inference(global_subsumption_just,[status(thm)],[c_342,c_49,c_342])).
% 3.18/1.08
% 3.18/1.08 tcf(c_522,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.08 (~sP0(X0_'ki_world')|qmltpeq(X1_'ki_world',op(e1,e1),e3)),
% 3.18/1.08 inference(global_subsumption_just,[status(thm)],[c_341,c_49,c_341])).
% 3.18/1.08
% 3.18/1.08 tcf(c_529,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.08 (~sP0(X0_'ki_world')|qmltpeq(X1_'ki_world',op(e0,e0),e3)),
% 3.18/1.08 inference(global_subsumption_just,[status(thm)],[c_340,c_49,c_340])).
% 3.18/1.08
% 3.18/1.08 tcf(c_1602,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world']:
% 3.18/1.08 (qmltpeq(X0_'ki_world',op(e0,e0),e0)|qmltpeq(X1_'ki_world',op(e0,e0),e3)|
% 3.18/1.08 qmltpeq(X2_'ki_world',op(e0,e0),e2)),
% 3.18/1.08 inference(forward_subsumption_resolution,
% 3.18/1.08 [status(thm)],
% 3.18/1.08 [c_1594,c_557,c_529,c_1293])).
% 3.18/1.08
% 3.18/1.08 tcf(c_1989,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world']:
% 3.18/1.08 (qmltpeq(X0_'ki_world',op(e0,e0),e2)|qmltpeq(X1_'ki_world',op(e0,e0),e0)|
% 3.18/1.08 qmltpeq(X2_'ki_world',op(e0,e0),e3)),
% 3.18/1.08 inference(forward_subsumption_resolution,
% 3.18/1.08 [status(thm)],
% 3.18/1.08 [c_1699,c_1602,c_1602,c_1602,c_1602,c_1602,c_1602,c_1602,
% 3.18/1.08 c_1602,c_1602,c_1602,c_1602,c_1602,c_1602])).
% 3.18/1.08
% 3.18/1.08 tcf(c_1999,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 3.18/1.08 (~qmltpeq(sK104,op(e1,e1),e3)|~qmltpeq(sK105,op(e2,e2),e3)|qmltpeq(X0_'ki_world',op(e0,e0),e2)|
% 3.18/1.08 qmltpeq(X1_'ki_world',op(e0,e0),e0)|sP3),
% 3.18/1.08 inference(superposition,[status(thm)],[c_1989,c_368])).
% 3.18/1.08
% 3.18/1.08 tcf(c_2511,plain,![X0_'ki_world':'$ki_world']:
% 3.18/1.08 (qmltpeq(X0_'ki_world',op(e0,e0),e3)),
% 3.18/1.08 inference(superposition,[status(thm)],[c_2510,c_529])).
% 3.18/1.08
% 3.18/1.08 tcf(c_2512,plain,![X0_'ki_world':'$ki_world']:
% 3.18/1.08 (qmltpeq(X0_'ki_world',op(e1,e1),e3)),
% 3.18/1.08 inference(superposition,[status(thm)],[c_2510,c_522])).
% 3.18/1.08
% 3.18/1.08 tcf(c_2513,plain,![X0_'ki_world':'$ki_world']:
% 3.18/1.08 (qmltpeq(X0_'ki_world',op(e2,e2),e3)),
% 3.18/1.08 inference(superposition,[status(thm)],[c_2510,c_515])).
% 3.18/1.08
% 3.18/1.08 tcf(c_2514,plain,![X0_'ki_world':'$ki_world']:
% 3.18/1.08 (qmltpeq(X0_'ki_world',op(e3,e3),e3)),
% 3.18/1.08 inference(superposition,[status(thm)],[c_2510,c_508])).
% 3.18/1.08
% 3.18/1.08 tcf(c_2515,plain,
% 3.18/1.08 (~qmltpeq(sK104,op(e1,e1),e3)|~qmltpeq(sK105,op(e2,e2),e3)|sP3),
% 3.18/1.08 inference(backward_subsumption_resolution,[status(thm)],[c_368,c_2511])).
% 3.18/1.08
% 3.18/1.08 tcf(c_2517,plain,
% 3.18/1.08 (~sP3),
% 3.18/1.08 inference(backward_subsumption_resolution,[status(thm)],[c_330,c_2514])).
% 3.18/1.08
% 3.18/1.08 tcf(c_2914,plain,
% 3.18/1.08 (~qmltpeq(sK105,op(e2,e2),e3)|~qmltpeq(sK104,op(e1,e1),e3)),
% 3.18/1.08 inference(global_subsumption_just,[status(thm)],[c_1999,c_2517,c_2515])).
% 3.18/1.08
% 3.18/1.08 tcf(c_2915,plain,
% 3.18/1.08 (~qmltpeq(sK104,op(e1,e1),e3)|~qmltpeq(sK105,op(e2,e2),e3)),
% 3.18/1.08 inference(renaming,[status(thm)],[c_2914])).
% 3.18/1.08
% 3.18/1.08 tcf(c_3917,plain,
% 3.18/1.08 (~qmltpeq(sK105,op(e2,e2),e3)),
% 3.18/1.08 inference(superposition,[status(thm)],[c_2512,c_2915])).
% 3.18/1.08
% 3.18/1.08 tcf(c_6176,plain,
% 3.18/1.08 ($false),
% 3.18/1.08 inference(forward_subsumption_resolution,[status(thm)],[c_3917,c_2513])).
% 3.18/1.08
% 3.18/1.08
% 3.18/1.08 % SZS output end CNFRefutation for theBenchmark.p
% 3.18/1.08
% 3.18/1.08
%------------------------------------------------------------------------------