%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL953_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 : n003.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:43 PM UTC 2026
% Result : Theorem 3.84s 1.45s
% Output : CNFRefutation 3.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL953_8 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.19/0.45 % Computer : n003.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Thu Sep 24 00:44:50 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.46 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.23/0.52 Running first-order theorem proving
% 0.23/0.52 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.23/0.54
% 0.23/0.54 % ======== iProver multi-core TPTP/SMT =========
% 0.23/0.54
% 0.23/0.54 % Detected problem language: tptp
% 0.23/0.56 % Proving...
% 3.84/1.45 % SZS status Started for theBenchmark.p
% 3.84/1.45 % SZS status Theorem for theBenchmark.p
% 3.84/1.45
% 3.84/1.45 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.84/1.45
% 3.84/1.45 % ------ iProver source info
% 3.84/1.45
% 3.84/1.45 % git: date: 2026-07-19 20:42:38 +0200
% 3.84/1.45 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.84/1.45 % git: non_committed_changes: false
% 3.84/1.45
% 3.84/1.45 % ------ Parsing...
% 3.84/1.45 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.84/1.45
% 3.84/1.45 % ------ Preprocessing... sf_s rm: 2 0s sf_e pe_s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 3.84/1.45
% 3.84/1.45 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 3.84/1.45 % ------ Proving...
% 3.84/1.45 % ------ Problem Properties
% 3.84/1.45
% 3.84/1.45 %
% 3.84/1.45 % clauses 22
% 3.84/1.45 % conjectures 9
% 3.84/1.45 % EPR 9
% 3.84/1.45 % Horn 18
% 3.84/1.45 % unary 11
% 3.84/1.45 % binary 3
% 3.84/1.45 % lits 82
% 3.84/1.45 % lits eq 0
% 3.84/1.45 % fd_pure 0
% 3.84/1.45 % fd_pseudo 0
% 3.84/1.45 % fd_cond 0
% 3.84/1.45 % fd_pseudo_cond 0
% 3.84/1.45 % AC symbols 0
% 3.84/1.45
% 3.84/1.45 % ------ Input Options Time Limit: Unbounded
% 3.84/1.45
% 3.84/1.45
% 3.84/1.45 % ------
% 3.84/1.45 % Current options:
% 3.84/1.45 % ------
% 3.84/1.45
% 3.84/1.45
% 3.84/1.45 %
% 3.84/1.45
% 3.84/1.45 % ------ Proving...
% 3.84/1.45 %
% 3.84/1.45
% 3.84/1.45 % SZS status Theorem for theBenchmark.p
% 3.84/1.45
% 3.84/1.45 % SZS output start CNFRefutation for theBenchmark.p
% 3.84/1.45
% 3.84/1.45 tff(func_def_0, type, '$ki_local_world': '$ki_world').
% 3.84/1.45 tff(pred_def_1, type, '$ki_accessible': ('$ki_world' * '$ki_world') > $o).
% 3.84/1.45 tff(pred_def_2, type, in: ('$ki_world' * $i * $i) > $o).
% 3.84/1.45 tff(pred_def_3, type, disjoint: ('$ki_world' * $i * $i) > $o).
% 3.84/1.45 tff(pred_def_4, type, empty: ('$ki_world' * $i) > $o).
% 3.84/1.45 tff(pred_def_5, type, '$ki_exists_in_world_$i': ('$ki_world' * $i) > $o).
% 3.84/1.45 tff(func_def_8, type, sK6: '$ki_world' > '$ki_world').
% 3.84/1.45 tff(func_def_9, type, sK7: ($i * $i * '$ki_world') > '$ki_world').
% 3.84/1.45 tff(func_def_10, type, sK8: '$ki_world').
% 3.84/1.45 tff(func_def_12, type, sK10: '$ki_world').
% 3.84/1.45 tff(func_def_14, type, sK12: '$ki_world').
% 3.84/1.45 tff(func_def_15, type, sK13: '$ki_world').
% 3.84/1.45 tff(func_def_16, type, sK14: '$ki_world' > '$ki_world').
% 3.84/1.45 tff(f7,axiom,(
% 3.84/1.45 ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : $i] : ('$ki_exists_in_world_$i'(X0,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 : '$ki_world'] : ('$ki_accessible'(X4,X5) => ~ ! [X6 : '$ki_world'] : ('$ki_accessible'(X5,X6) => in(X6,X1,X3))) => ! [X5 : '$ki_world'] : ('$ki_accessible'(X4,X5) => disjoint(X5,singleton(X1),X3))))))))),
% 3.84/1.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l28_zfmisc_1)).
% 3.84/1.45
% 3.84/1.45 tff(f8,conjecture,(
% 3.84/1.45 ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : $i] : ('$ki_exists_in_world_$i'(X0,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 : '$ki_world'] : ('$ki_accessible'(X4,X5) => ~ ! [X6 : '$ki_world'] : ('$ki_accessible'(X5,X6) => in(X6,X1,X3))) => ! [X5 : '$ki_world'] : ('$ki_accessible'(X4,X5) => disjoint(X5,singleton(X1),X3))))))))),
% 3.84/1.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',verify)).
% 3.84/1.45
% 3.84/1.45 tff(f9,negated_conjecture,(
% 3.84/1.45 ~ ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : $i] : ('$ki_exists_in_world_$i'(X0,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 : '$ki_world'] : ('$ki_accessible'(X4,X5) => ~ ! [X6 : '$ki_world'] : ('$ki_accessible'(X5,X6) => in(X6,X1,X3))) => ! [X5 : '$ki_world'] : ('$ki_accessible'(X4,X5) => disjoint(X5,singleton(X1),X3))))))))),
% 3.84/1.45 inference(negated_conjecture,[status(cth)],[f8])).
% 3.84/1.45
% 3.84/1.45 tff(f12,plain,(
% 3.84/1.45 ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : $i] : ('$ki_exists_in_world_$i'(X0,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 : '$ki_world'] : ('$ki_accessible'(X4,X5) => ~ ! [X6 : '$ki_world'] : ('$ki_accessible'(X5,X6) => in(X6,X1,X3))) => ! [X7 : '$ki_world'] : ('$ki_accessible'(X4,X7) => disjoint(X7,singleton(X1),X3))))))))),
% 3.84/1.45 inference(rectify,[],[f7])).
% 3.84/1.45
% 3.84/1.45 tff(f13,plain,(
% 3.84/1.45 ~ ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : $i] : ('$ki_exists_in_world_$i'(X0,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 : '$ki_world'] : ('$ki_accessible'(X4,X5) => ~ ! [X6 : '$ki_world'] : ('$ki_accessible'(X5,X6) => in(X6,X1,X3))) => ! [X7 : '$ki_world'] : ('$ki_accessible'(X4,X7) => disjoint(X7,singleton(X1),X3))))))))),
% 3.84/1.45 inference(rectify,[],[f9])).
% 3.84/1.45
% 3.84/1.45 tff(f20,plain,(
% 3.84/1.45 ! [X0 : '$ki_world'] : (! [X1 : $i] : (! [X2 : '$ki_world'] : (! [X3 : $i] : (! [X4 : '$ki_world'] : ((! [X7 : '$ki_world'] : (disjoint(X7,singleton(X1),X3) | ~'$ki_accessible'(X4,X7)) | ? [X5 : '$ki_world'] : (! [X6 : '$ki_world'] : (in(X6,X1,X3) | ~'$ki_accessible'(X5,X6)) & '$ki_accessible'(X4,X5))) | ~'$ki_accessible'(X2,X4)) | ~'$ki_exists_in_world_$i'(X2,X3)) | ~'$ki_accessible'(X0,X2)) | ~'$ki_exists_in_world_$i'(X0,X1)) | ~'$ki_accessible'('$ki_local_world',X0))),
% 3.84/1.45 inference(ennf_transformation,[],[f12])).
% 3.84/1.45
% 3.84/1.45 tff(f21,plain,(
% 3.84/1.45 ! [X0 : '$ki_world'] : (! [X1 : $i] : (! [X2 : '$ki_world'] : (! [X3 : $i] : (! [X4 : '$ki_world'] : (! [X7 : '$ki_world'] : (disjoint(X7,singleton(X1),X3) | ~'$ki_accessible'(X4,X7)) | ? [X5 : '$ki_world'] : (! [X6 : '$ki_world'] : (in(X6,X1,X3) | ~'$ki_accessible'(X5,X6)) & '$ki_accessible'(X4,X5)) | ~'$ki_accessible'(X2,X4)) | ~'$ki_exists_in_world_$i'(X2,X3)) | ~'$ki_accessible'(X0,X2)) | ~'$ki_exists_in_world_$i'(X0,X1)) | ~'$ki_accessible'('$ki_local_world',X0))),
% 3.84/1.45 inference(flattening,[],[f20])).
% 3.84/1.45
% 3.84/1.45 tff(f22,plain,(
% 3.84/1.45 ? [X0 : '$ki_world'] : (? [X1 : $i] : (? [X2 : '$ki_world'] : (? [X3 : $i] : (? [X4 : '$ki_world'] : ((? [X7 : '$ki_world'] : (~disjoint(X7,singleton(X1),X3) & '$ki_accessible'(X4,X7)) & ! [X5 : '$ki_world'] : (? [X6 : '$ki_world'] : (~in(X6,X1,X3) & '$ki_accessible'(X5,X6)) | ~'$ki_accessible'(X4,X5))) & '$ki_accessible'(X2,X4)) & '$ki_exists_in_world_$i'(X2,X3)) & '$ki_accessible'(X0,X2)) & '$ki_exists_in_world_$i'(X0,X1)) & '$ki_accessible'('$ki_local_world',X0))),
% 3.84/1.45 inference(ennf_transformation,[],[f13])).
% 3.84/1.45
% 3.84/1.45 tff(f23,plain,(
% 3.84/1.45 ? [X0 : '$ki_world'] : (? [X1 : $i] : (? [X2 : '$ki_world'] : (? [X3 : $i] : (? [X4 : '$ki_world'] : (? [X7 : '$ki_world'] : (~disjoint(X7,singleton(X1),X3) & '$ki_accessible'(X4,X7)) & ! [X5 : '$ki_world'] : (? [X6 : '$ki_world'] : (~in(X6,X1,X3) & '$ki_accessible'(X5,X6)) | ~'$ki_accessible'(X4,X5)) & '$ki_accessible'(X2,X4)) & '$ki_exists_in_world_$i'(X2,X3)) & '$ki_accessible'(X0,X2)) & '$ki_exists_in_world_$i'(X0,X1)) & '$ki_accessible'('$ki_local_world',X0))),
% 3.84/1.45 inference(flattening,[],[f22])).
% 3.84/1.45
% 3.84/1.45 tff(f31,plain,(
% 3.84/1.45 ! [X0 : '$ki_world'] : (! [X1 : $i] : (! [X2 : '$ki_world'] : (! [X3 : $i] : (! [X4 : '$ki_world'] : (! [X5 : '$ki_world'] : (disjoint(X5,singleton(X1),X3) | ~'$ki_accessible'(X4,X5)) | ? [X6 : '$ki_world'] : (! [X7 : '$ki_world'] : (in(X7,X1,X3) | ~'$ki_accessible'(X6,X7)) & '$ki_accessible'(X4,X6)) | ~'$ki_accessible'(X2,X4)) | ~'$ki_exists_in_world_$i'(X2,X3)) | ~'$ki_accessible'(X0,X2)) | ~'$ki_exists_in_world_$i'(X0,X1)) | ~'$ki_accessible'('$ki_local_world',X0))),
% 3.84/1.45 inference(rectify,[],[f21])).
% 3.84/1.45
% 3.84/1.45 tff(f32,plain,(
% 3.84/1.45 ! [X0 : '$ki_world'] : (! [X1 : $i] : (! [X2 : '$ki_world'] : (! [X3 : $i] : (! [X4 : '$ki_world'] : (! [X5 : '$ki_world'] : (disjoint(X5,singleton(X1),X3) | ~'$ki_accessible'(X4,X5)) | (! [X7 : '$ki_world'] : (in(X7,X1,X3) | ~'$ki_accessible'(sK7(X1,X3,X4),X7)) & '$ki_accessible'(X4,sK7(X1,X3,X4))) | ~'$ki_accessible'(X2,X4)) | ~'$ki_exists_in_world_$i'(X2,X3)) | ~'$ki_accessible'(X0,X2)) | ~'$ki_exists_in_world_$i'(X0,X1)) | ~'$ki_accessible'('$ki_local_world',X0))),
% 3.84/1.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X6,sK7(X1,X3,X4))],[f31])).
% 3.84/1.45
% 3.84/1.45 tff(f33,plain,(
% 3.84/1.45 ? [X0 : '$ki_world'] : (? [X1 : $i] : (? [X2 : '$ki_world'] : (? [X3 : $i] : (? [X4 : '$ki_world'] : (? [X5 : '$ki_world'] : (~disjoint(X5,singleton(X1),X3) & '$ki_accessible'(X4,X5)) & ! [X6 : '$ki_world'] : (? [X7 : '$ki_world'] : (~in(X7,X1,X3) & '$ki_accessible'(X6,X7)) | ~'$ki_accessible'(X4,X6)) & '$ki_accessible'(X2,X4)) & '$ki_exists_in_world_$i'(X2,X3)) & '$ki_accessible'(X0,X2)) & '$ki_exists_in_world_$i'(X0,X1)) & '$ki_accessible'('$ki_local_world',X0))),
% 3.84/1.45 inference(rectify,[],[f23])).
% 3.84/1.45
% 3.84/1.45 tff(f34,plain,(
% 3.84/1.45 (((((~disjoint(sK13,singleton(sK9),sK11) & '$ki_accessible'(sK12,sK13)) & ! [X6 : '$ki_world'] : ((~in(sK14(X6),sK9,sK11) & '$ki_accessible'(X6,sK14(X6))) | ~'$ki_accessible'(sK12,X6)) & '$ki_accessible'(sK10,sK12)) & '$ki_exists_in_world_$i'(sK10,sK11)) & '$ki_accessible'(sK8,sK10)) & '$ki_exists_in_world_$i'(sK8,sK9)) & '$ki_accessible'('$ki_local_world',sK8)),
% 3.84/1.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10,sK11,sK12,sK13,sK14]),skolemize(X0,sK8),skolemize(X1,sK9),skolemize(X2,sK10),skolemize(X3,sK11),skolemize(X4,sK12),skolemize(X5,sK13),skolemize(X7,sK14(X6))],[f33])).
% 3.84/1.45
% 3.84/1.45 tff(f48,plain,(
% 3.84/1.45 ( ! [X2 : '$ki_world',X3 : $i,X0 : '$ki_world',X1 : $i,X4 : '$ki_world',X5 : '$ki_world'] : (disjoint(X5,singleton(X1),X3) | ~'$ki_accessible'(X4,X5) | '$ki_accessible'(X4,sK7(X1,X3,X4)) | ~'$ki_accessible'(X2,X4) | ~'$ki_exists_in_world_$i'(X2,X3) | ~'$ki_accessible'(X0,X2) | ~'$ki_exists_in_world_$i'(X0,X1) | ~'$ki_accessible'('$ki_local_world',X0)) )),
% 3.84/1.45 inference(cnf_transformation,[],[f32])).
% 3.84/1.45
% 3.84/1.45 tff(f49,plain,(
% 3.84/1.45 ( ! [X2 : '$ki_world',X3 : $i,X0 : '$ki_world',X1 : $i,X7 : '$ki_world',X4 : '$ki_world',X5 : '$ki_world'] : (disjoint(X5,singleton(X1),X3) | ~'$ki_accessible'(X4,X5) | in(X7,X1,X3) | ~'$ki_accessible'(sK7(X1,X3,X4),X7) | ~'$ki_accessible'(X2,X4) | ~'$ki_exists_in_world_$i'(X2,X3) | ~'$ki_accessible'(X0,X2) | ~'$ki_exists_in_world_$i'(X0,X1) | ~'$ki_accessible'('$ki_local_world',X0)) )),
% 3.84/1.45 inference(cnf_transformation,[],[f32])).
% 3.84/1.45
% 3.84/1.45 tff(f50,plain,(
% 3.84/1.45 '$ki_accessible'('$ki_local_world',sK8)),
% 3.84/1.45 inference(cnf_transformation,[],[f34])).
% 3.84/1.45
% 3.84/1.45 tff(f51,plain,(
% 3.84/1.45 '$ki_exists_in_world_$i'(sK8,sK9)),
% 3.84/1.45 inference(cnf_transformation,[],[f34])).
% 3.84/1.45
% 3.84/1.45 tff(f52,plain,(
% 3.84/1.45 '$ki_accessible'(sK8,sK10)),
% 3.84/1.45 inference(cnf_transformation,[],[f34])).
% 3.84/1.45
% 3.84/1.45 tff(f53,plain,(
% 3.84/1.45 '$ki_exists_in_world_$i'(sK10,sK11)),
% 3.84/1.45 inference(cnf_transformation,[],[f34])).
% 3.84/1.45
% 3.84/1.45 tff(f54,plain,(
% 3.84/1.45 '$ki_accessible'(sK10,sK12)),
% 3.84/1.45 inference(cnf_transformation,[],[f34])).
% 3.84/1.45
% 3.84/1.45 tff(f55,plain,(
% 3.84/1.45 ( ! [X6 : '$ki_world'] : ('$ki_accessible'(X6,sK14(X6)) | ~'$ki_accessible'(sK12,X6)) )),
% 3.84/1.45 inference(cnf_transformation,[],[f34])).
% 3.84/1.45
% 3.84/1.45 tff(f56,plain,(
% 3.84/1.45 ( ! [X6 : '$ki_world'] : (~in(sK14(X6),sK9,sK11) | ~'$ki_accessible'(sK12,X6)) )),
% 3.84/1.45 inference(cnf_transformation,[],[f34])).
% 3.84/1.45
% 3.84/1.45 tff(f57,plain,(
% 3.84/1.45 '$ki_accessible'(sK12,sK13)),
% 3.84/1.45 inference(cnf_transformation,[],[f34])).
% 3.84/1.45
% 3.84/1.45 tff(f58,plain,(
% 3.84/1.45 ~disjoint(sK13,singleton(sK9),sK11)),
% 3.84/1.45 inference(cnf_transformation,[],[f34])).
% 3.84/1.45
% 3.84/1.45 tcf(c_62,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',X4_'ki_world':'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(sK7(X0,X1,X0_'ki_world'),X1_'ki_world')|~'$ki_accessible'(X0_'ki_world',X3_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X2_'ki_world',X0_'ki_world')|~'$ki_accessible'(X4_'ki_world',X2_'ki_world')|
% 3.84/1.45 ~'$ki_exists_in_world(X2_'ki_world',X1)|~'$ki_exists_in_world(X4_'ki_world',X0)|
% 3.84/1.45 ~'$ki_accessible'('$ki_local_world',X4_'ki_world')|disjoint(X3_'ki_world',singleton(X0),X1)|
% 3.84/1.45 in(X1_'ki_world',X0,X1)),
% 3.84/1.45 inference(cnf_transformation,[],[f49])).
% 3.84/1.45
% 3.84/1.45 tcf(c_63,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']:
% 3.84/1.45 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'(X1_'ki_world',X2_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X3_'ki_world',X0_'ki_world')|~'$ki_exists_in_world(X0_'ki_world',X0)|
% 3.84/1.45 ~'$ki_exists_in_world(X3_'ki_world',X1)|~'$ki_accessible'('$ki_local_world',X3_'ki_world')|
% 3.84/1.45 '$ki_accessible'(X1_'ki_world',sK7(X1,X0,X1_'ki_world'))|disjoint(X2_'ki_world',singleton(X1),X0)),
% 3.84/1.45 inference(cnf_transformation,[],[f48])).
% 3.84/1.45
% 3.84/1.45 tcf(c_64,negated_conjecture,
% 3.84/1.45 (~disjoint(sK13,singleton(sK9),sK11)),
% 3.84/1.45 inference(cnf_transformation,[],[f58])).
% 3.84/1.45
% 3.84/1.45 tcf(c_65,negated_conjecture,
% 3.84/1.45 ('$ki_accessible'(sK12,sK13)),
% 3.84/1.45 inference(cnf_transformation,[],[f57])).
% 3.84/1.45
% 3.84/1.45 tcf(c_66,negated_conjecture,![X0_'ki_world':'$ki_world']:
% 3.84/1.45 (~in(sK14(X0_'ki_world'),sK9,sK11)|~'$ki_accessible'(sK12,X0_'ki_world')),
% 3.84/1.45 inference(cnf_transformation,[],[f56])).
% 3.84/1.45
% 3.84/1.45 tcf(c_67,negated_conjecture,![X0_'ki_world':'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(sK12,X0_'ki_world')|'$ki_accessible'(X0_'ki_world',sK14(X0_'ki_world'))),
% 3.84/1.45 inference(cnf_transformation,[],[f55])).
% 3.84/1.45
% 3.84/1.45 tcf(c_68,negated_conjecture,
% 3.84/1.45 ('$ki_accessible'(sK10,sK12)),
% 3.84/1.45 inference(cnf_transformation,[],[f54])).
% 3.84/1.45
% 3.84/1.45 tcf(c_69,negated_conjecture,
% 3.84/1.45 ('$ki_exists_in_world(sK10,sK11)),
% 3.84/1.45 inference(cnf_transformation,[],[f53])).
% 3.84/1.45
% 3.84/1.45 tcf(c_70,negated_conjecture,
% 3.84/1.45 ('$ki_accessible'(sK8,sK10)),
% 3.84/1.45 inference(cnf_transformation,[],[f52])).
% 3.84/1.45
% 3.84/1.45 tcf(c_71,negated_conjecture,
% 3.84/1.45 ('$ki_exists_in_world(sK8,sK9)),
% 3.84/1.45 inference(cnf_transformation,[],[f51])).
% 3.84/1.45
% 3.84/1.45 tcf(c_72,negated_conjecture,
% 3.84/1.45 ('$ki_accessible'('$ki_local_world',sK8)),
% 3.84/1.45 inference(cnf_transformation,[],[f50])).
% 3.84/1.45
% 3.84/1.45 tcf(c_425,negated_conjecture,
% 3.84/1.45 ('$ki_exists_in_world(sK8,sK9)),
% 3.84/1.45 inference(subtyping,[status(esa)],[c_71])).
% 3.84/1.45
% 3.84/1.45 tcf(c_427,negated_conjecture,
% 3.84/1.45 ('$ki_exists_in_world(sK10,sK11)),
% 3.84/1.45 inference(subtyping,[status(esa)],[c_69])).
% 3.84/1.45
% 3.84/1.45 tcf(c_429,negated_conjecture,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(sK12,X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 '$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',sK14(X0_iProver_'ki_accessible'_1_'ki_world'))),
% 3.84/1.45 inference(subtyping,[status(esa)],[c_67])).
% 3.84/1.45
% 3.84/1.45 tcf(c_430,negated_conjecture,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~in(sK14(X0_iProver_'ki_accessible'_1_'ki_world'),sK9,sK11)|~'$ki_accessible'(sK12,X0_iProver_'ki_accessible'_1_'ki_world')),
% 3.84/1.45 inference(subtyping,[status(esa)],[c_66])).
% 3.84/1.45
% 3.84/1.45 tcf(c_432,negated_conjecture,
% 3.84/1.45 (~disjoint(sK13,singleton(sK9),sK11)),
% 3.84/1.45 inference(subtyping,[status(esa)],[c_64])).
% 3.84/1.45
% 3.84/1.45 tcf(c_433,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X0_iProver_disjoint_2:iProver_disjoint_2,X1_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X1_iProver_disjoint_2:iProver_disjoint_2,X2_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X3_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',X1_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X1_iProver_'ki_accessible'_1_'ki_world',X3_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X2_iProver_'ki_accessible'_1_'ki_world',X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_exists_in_world(X0_iProver_'ki_accessible'_1_'ki_world',X0_iProver_disjoint_2)|
% 3.84/1.45 ~'$ki_exists_in_world(X2_iProver_'ki_accessible'_1_'ki_world',X1_iProver_disjoint_2)|
% 3.84/1.45 ~'$ki_accessible'('$ki_local_world',X2_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 '$ki_accessible'(X1_iProver_'ki_accessible'_1_'ki_world',sK7(X1_iProver_disjoint_2,X0_iProver_disjoint_2,X1_iProver_'ki_accessible'_1_'ki_world'))|
% 3.84/1.45 disjoint(X3_iProver_'ki_accessible'_1_'ki_world',singleton(X1_iProver_disjoint_2),X0_iProver_disjoint_2)),
% 3.84/1.45 inference(subtyping,[status(esa)],[c_63])).
% 3.84/1.45
% 3.84/1.45 tcf(c_434,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X0_iProver_disjoint_2:iProver_disjoint_2,X1_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X1_iProver_disjoint_2:iProver_disjoint_2,X2_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X3_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X4_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(sK7(X0_iProver_disjoint_2,X1_iProver_disjoint_2,X0_iProver_'ki_accessible'_1_'ki_world'),X1_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',X4_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X2_iProver_'ki_accessible'_1_'ki_world',X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X3_iProver_'ki_accessible'_1_'ki_world',X2_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_exists_in_world(X2_iProver_'ki_accessible'_1_'ki_world',X1_iProver_disjoint_2)|
% 3.84/1.45 ~'$ki_exists_in_world(X3_iProver_'ki_accessible'_1_'ki_world',X0_iProver_disjoint_2)|
% 3.84/1.45 ~'$ki_accessible'('$ki_local_world',X3_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 disjoint(X4_iProver_'ki_accessible'_1_'ki_world',singleton(X0_iProver_disjoint_2),X1_iProver_disjoint_2)|
% 3.84/1.45 in(X1_iProver_'ki_accessible'_1_'ki_world',X0_iProver_disjoint_2,X1_iProver_disjoint_2)),
% 3.84/1.45 inference(subtyping,[status(esa)],[c_62])).
% 3.84/1.45
% 3.84/1.45 tcf(c_539,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X1_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X2_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X3_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(sK7(sK9,sK11,X0_iProver_'ki_accessible'_1_'ki_world'),X1_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X2_iProver_'ki_accessible'_1_'ki_world',X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X3_iProver_'ki_accessible'_1_'ki_world',X2_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',sK13)|~'$ki_accessible'('$ki_local_world',X3_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_exists_in_world(X2_iProver_'ki_accessible'_1_'ki_world',sK11)|
% 3.84/1.45 ~'$ki_exists_in_world(X3_iProver_'ki_accessible'_1_'ki_world',sK9)|
% 3.84/1.45 in(X1_iProver_'ki_accessible'_1_'ki_world',sK9,sK11)),
% 3.84/1.45 inference(resolution,[status(thm)],[c_434,c_432])).
% 3.84/1.45
% 3.84/1.45 tcf(c_549,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X1_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X2_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X3_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(sK7(sK9,sK11,X0_iProver_'ki_accessible'_1_'ki_world'),sK14(X1_iProver_'ki_accessible'_1_'ki_world'))|
% 3.84/1.45 ~'$ki_accessible'(X2_iProver_'ki_accessible'_1_'ki_world',X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X3_iProver_'ki_accessible'_1_'ki_world',X2_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',sK13)|~'$ki_accessible'('$ki_local_world',X3_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(sK12,X1_iProver_'ki_accessible'_1_'ki_world')|~'$ki_exists_in_world(X2_iProver_'ki_accessible'_1_'ki_world',sK11)|
% 3.84/1.45 ~'$ki_exists_in_world(X3_iProver_'ki_accessible'_1_'ki_world',sK9)),
% 3.84/1.45 inference(resolution,[status(thm)],[c_539,c_430])).
% 3.84/1.45
% 3.84/1.45 tcf(c_563,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X1_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X2_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(sK7(sK9,sK11,X0_iProver_'ki_accessible'_1_'ki_world'),sK14(X1_iProver_'ki_accessible'_1_'ki_world'))|
% 3.84/1.45 ~'$ki_accessible'(X2_iProver_'ki_accessible'_1_'ki_world',X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',sK13)|~'$ki_accessible'(sK8,X2_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(sK12,X1_iProver_'ki_accessible'_1_'ki_world')|~'$ki_exists_in_world(X2_iProver_'ki_accessible'_1_'ki_world',sK11)|
% 3.84/1.45 ~'$ki_accessible'('$ki_local_world',sK8)),
% 3.84/1.45 inference(resolution,[status(thm)],[c_549,c_425])).
% 3.84/1.45
% 3.84/1.45 tcf(c_565,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X1_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X2_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_exists_in_world(X2_iProver_'ki_accessible'_1_'ki_world',sK11)|
% 3.84/1.45 ~'$ki_accessible'(sK12,X1_iProver_'ki_accessible'_1_'ki_world')|~'$ki_accessible'(sK8,X2_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',sK13)|~'$ki_accessible'(X2_iProver_'ki_accessible'_1_'ki_world',X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(sK7(sK9,sK11,X0_iProver_'ki_accessible'_1_'ki_world'),sK14(X1_iProver_'ki_accessible'_1_'ki_world'))),
% 3.84/1.45 inference(global_subsumption_just,[status(thm)],[c_563,c_72,c_563])).
% 3.84/1.45
% 3.84/1.45 tcf(c_566,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X1_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X2_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(sK7(sK9,sK11,X0_iProver_'ki_accessible'_1_'ki_world'),sK14(X1_iProver_'ki_accessible'_1_'ki_world'))|
% 3.84/1.45 ~'$ki_accessible'(X2_iProver_'ki_accessible'_1_'ki_world',X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',sK13)|~'$ki_accessible'(sK8,X2_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(sK12,X1_iProver_'ki_accessible'_1_'ki_world')|~'$ki_exists_in_world(X2_iProver_'ki_accessible'_1_'ki_world',sK11)),
% 3.84/1.45 inference(renaming,[status(thm)],[c_565])).
% 3.84/1.45
% 3.84/1.45 tcf(c_576,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X1_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(sK7(sK9,sK11,X0_iProver_'ki_accessible'_1_'ki_world'),sK14(X1_iProver_'ki_accessible'_1_'ki_world'))|
% 3.84/1.45 ~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',sK13)|~'$ki_accessible'(sK10,X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(sK12,X1_iProver_'ki_accessible'_1_'ki_world')|~'$ki_accessible'(sK8,sK10)),
% 3.84/1.45 inference(resolution,[status(thm)],[c_566,c_427])).
% 3.84/1.45
% 3.84/1.45 tcf(c_578,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X1_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(sK12,X1_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(sK10,X0_iProver_'ki_accessible'_1_'ki_world')|~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',sK13)|
% 3.84/1.45 ~'$ki_accessible'(sK7(sK9,sK11,X0_iProver_'ki_accessible'_1_'ki_world'),sK14(X1_iProver_'ki_accessible'_1_'ki_world'))),
% 3.84/1.45 inference(global_subsumption_just,[status(thm)],[c_576,c_70,c_576])).
% 3.84/1.45
% 3.84/1.45 tcf(c_579,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X1_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(sK7(sK9,sK11,X0_iProver_'ki_accessible'_1_'ki_world'),sK14(X1_iProver_'ki_accessible'_1_'ki_world'))|
% 3.84/1.45 ~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',sK13)|~'$ki_accessible'(sK10,X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(sK12,X1_iProver_'ki_accessible'_1_'ki_world')),
% 3.84/1.45 inference(renaming,[status(thm)],[c_578])).
% 3.84/1.45
% 3.84/1.45 tcf(c_586,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(sK12,sK7(sK9,sK11,X0_iProver_'ki_accessible'_1_'ki_world'))|
% 3.84/1.45 ~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',sK13)|~'$ki_accessible'(sK10,X0_iProver_'ki_accessible'_1_'ki_world')),
% 3.84/1.45 inference(resolution,[status(thm)],[c_579,c_429])).
% 3.84/1.45
% 3.84/1.45 tcf(c_591,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X1_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X2_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',X1_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X1_iProver_'ki_accessible'_1_'ki_world',sK12)|~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(sK12,X2_iProver_'ki_accessible'_1_'ki_world')|~'$ki_exists_in_world(X0_iProver_'ki_accessible'_1_'ki_world',sK9)|
% 3.84/1.45 ~'$ki_exists_in_world(X1_iProver_'ki_accessible'_1_'ki_world',sK11)|
% 3.84/1.45 ~'$ki_accessible'(sK10,sK12)|~'$ki_accessible'(sK12,sK13)|disjoint(X2_iProver_'ki_accessible'_1_'ki_world',singleton(sK9),sK11)),
% 3.84/1.45 inference(resolution,[status(thm)],[c_586,c_433])).
% 3.84/1.45
% 3.84/1.45 tcf(c_593,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X1_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X2_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',X1_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X1_iProver_'ki_accessible'_1_'ki_world',sK12)|~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(sK12,X2_iProver_'ki_accessible'_1_'ki_world')|~'$ki_exists_in_world(X0_iProver_'ki_accessible'_1_'ki_world',sK9)|
% 3.84/1.45 ~'$ki_exists_in_world(X1_iProver_'ki_accessible'_1_'ki_world',sK11)|
% 3.84/1.45 disjoint(X2_iProver_'ki_accessible'_1_'ki_world',singleton(sK9),sK11)),
% 3.84/1.45 inference(global_subsumption_just,[status(thm)],[c_591,c_68,c_65,c_591])).
% 3.84/1.45
% 3.84/1.45 tcf(c_603,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X1_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',X1_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X1_iProver_'ki_accessible'_1_'ki_world',sK12)|~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_exists_in_world(X0_iProver_'ki_accessible'_1_'ki_world',sK9)|
% 3.84/1.45 ~'$ki_exists_in_world(X1_iProver_'ki_accessible'_1_'ki_world',sK11)|
% 3.84/1.45 ~'$ki_accessible'(sK12,sK13)),
% 3.84/1.45 inference(resolution,[status(thm)],[c_593,c_432])).
% 3.84/1.45
% 3.84/1.45 tcf(c_605,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X1_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_exists_in_world(X1_iProver_'ki_accessible'_1_'ki_world',sK11)|
% 3.84/1.45 ~'$ki_exists_in_world(X0_iProver_'ki_accessible'_1_'ki_world',sK9)|
% 3.84/1.45 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X1_iProver_'ki_accessible'_1_'ki_world',sK12)|~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',X1_iProver_'ki_accessible'_1_'ki_world')),
% 3.84/1.45 inference(global_subsumption_just,[status(thm)],[c_603,c_65,c_603])).
% 3.84/1.45
% 3.84/1.45 tcf(c_606,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world',X1_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',X1_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X1_iProver_'ki_accessible'_1_'ki_world',sK12)|~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_exists_in_world(X0_iProver_'ki_accessible'_1_'ki_world',sK9)|
% 3.84/1.45 ~'$ki_exists_in_world(X1_iProver_'ki_accessible'_1_'ki_world',sK11)),
% 3.84/1.45 inference(renaming,[status(thm)],[c_605])).
% 3.84/1.45
% 3.84/1.45 tcf(c_615,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',sK10)|
% 3.84/1.45 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_exists_in_world(X0_iProver_'ki_accessible'_1_'ki_world',sK9)|
% 3.84/1.45 ~'$ki_accessible'(sK10,sK12)),
% 3.84/1.45 inference(resolution,[status(thm)],[c_606,c_427])).
% 3.84/1.45
% 3.84/1.45 tcf(c_617,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_exists_in_world(X0_iProver_'ki_accessible'_1_'ki_world',sK9)|
% 3.84/1.45 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',sK10)),
% 3.84/1.45 inference(global_subsumption_just,[status(thm)],[c_615,c_68,c_615])).
% 3.84/1.45
% 3.84/1.45 tcf(c_618,plain,![X0_iProver_'ki_accessible'_1_'ki_world':iProver_'$ki_accessible'_1_'$ki_world']:
% 3.84/1.45 (~'$ki_accessible'(X0_iProver_'ki_accessible'_1_'ki_world',sK10)|
% 3.84/1.45 ~'$ki_accessible'('$ki_local_world',X0_iProver_'ki_accessible'_1_'ki_world')|
% 3.84/1.45 ~'$ki_exists_in_world(X0_iProver_'ki_accessible'_1_'ki_world',sK9)),
% 3.84/1.45 inference(renaming,[status(thm)],[c_617])).
% 3.84/1.45
% 3.84/1.45 tcf(c_628,plain,
% 3.84/1.45 (~'$ki_accessible'('$ki_local_world',sK8)|~'$ki_accessible'(sK8,sK10)),
% 3.84/1.45 inference(resolution,[status(thm)],[c_618,c_425])).
% 3.84/1.45
% 3.84/1.45 tcf(c_629,plain,
% 3.84/1.45 ($false),
% 3.84/1.45 inference(prop_impl_just,[status(thm)],[c_628,c_70,c_72])).
% 3.84/1.45
% 3.84/1.45
% 3.84/1.45 % SZS output end CNFRefutation for theBenchmark.p
% 3.84/1.45
%------------------------------------------------------------------------------