%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYO903_10 : TPTP v9.3.1. Released v8.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:52:18 PM UTC 2026
% Result : Theorem 0.17s 0.96s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYO903_10 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.04/0.31 % Computer : n012.cluster.edu
% 0.04/0.31 % Model : x86_64 x86_64
% 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.31 % Memory : 8046.5625MB
% 0.04/0.31 % OS : Linux 6.8.0-71-generic
% 0.04/0.31 % CPULimit : 300
% 0.04/0.31 % WCLimit : 300
% 0.04/0.31 % DateTime : Fri Sep 25 03:58:37 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.07/0.33 Running first-order theorem proving
% 0.07/0.33 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.33
% 0.07/0.33 % ======== iProver multi-core TPTP/SMT =========
% 0.07/0.33
% 0.07/0.34 % Detected problem language: tptp
% 0.07/0.34 % Proving...
% 0.17/0.96 % SZS status Started for theBenchmark.p
% 0.17/0.96 % SZS status Theorem for theBenchmark.p
% 0.17/0.96
% 0.17/0.96 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 0.17/0.96
% 0.17/0.96 % ------ iProver source info
% 0.17/0.96
% 0.17/0.96 % git: date: 2026-07-19 20:42:38 +0200
% 0.17/0.96 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 0.17/0.96 % git: non_committed_changes: false
% 0.17/0.96
% 0.17/0.96 % ------ Parsing...
% 0.17/0.96 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 0.17/0.96 %
% 0.17/0.96
% 0.17/0.96 % ------ Preprocessing...%
% 0.17/0.96
% 0.17/0.96 % SZS status Theorem for theBenchmark.p
% 0.17/0.96
% 0.17/0.96 % SZS output start CNFRefutation for theBenchmark.p
% 0.17/0.96
% 0.17/0.96 tff(func_def_0, type, '$ki_local_world': '$ki_world').
% 0.17/0.96 tff(pred_def_1, type, '$ki_accessible': ('$ki_world' * '$ki_world') > $o).
% 0.17/0.96 tff(pred_def_2, type, v1: '$ki_world' > $o).
% 0.17/0.96 tff(pred_def_3, type, v2: '$ki_world' > $o).
% 0.17/0.96 tff(pred_def_4, type, v3: '$ki_world' > $o).
% 0.17/0.96 tff(pred_def_5, type, v4: '$ki_world' > $o).
% 0.17/0.96 tff(f1,axiom,(
% 0.17/0.96 ! [X0 : '$ki_world'] : '$ki_accessible'(X0,X0)),
% 0.17/0.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mrel_reflexive)).
% 0.17/0.96
% 0.17/0.96 tff(f5,axiom,(
% 0.17/0.96 v1('$ki_local_world') | v2('$ki_local_world') | ~v3('$ki_local_world') | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => ~v4(X1)))),
% 0.17/0.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat3)).
% 0.17/0.96
% 0.17/0.96 tff(f7,axiom,(
% 0.17/0.96 v1('$ki_local_world') | v3('$ki_local_world') | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => v3(X1))) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => v4(X1)))),
% 0.17/0.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat5)).
% 0.17/0.96
% 0.17/0.96 tff(f9,axiom,(
% 0.17/0.96 v1('$ki_local_world') | ~v2('$ki_local_world') | ~v4('$ki_local_world') | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => ~v2(X1)))),
% 0.17/0.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat7)).
% 0.17/0.96
% 0.17/0.96 tff(f20,axiom,(
% 0.17/0.96 v2('$ki_local_world') | ~v3('$ki_local_world') | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ~v1(X0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => ~v1(X1)))),
% 0.17/0.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat18)).
% 0.17/0.96
% 0.17/0.96 tff(f28,axiom,(
% 0.17/0.96 v3('$ki_local_world') | ~v4('$ki_local_world') | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => v3(X1))) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => ~v4(X1)))),
% 0.17/0.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat26)).
% 0.17/0.96
% 0.17/0.96 tff(f31,axiom,(
% 0.17/0.96 v4('$ki_local_world') | ~v1('$ki_local_world') | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ~v1(X0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => v3(X1)))),
% 0.17/0.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat29)).
% 0.17/0.96
% 0.17/0.96 tff(f33,axiom,(
% 0.17/0.96 v4('$ki_local_world') | ~v3('$ki_local_world') | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => v1(X1))) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => v4(X1)))),
% 0.17/0.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat31)).
% 0.17/0.96
% 0.17/0.96 tff(f36,axiom,(
% 0.17/0.96 ~v1('$ki_local_world') | ~v2('$ki_local_world') | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ~v4(X0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => ~v1(X1)))),
% 0.17/0.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat34)).
% 0.17/0.96
% 0.17/0.96 tff(f37,axiom,(
% 0.17/0.96 ~v1('$ki_local_world') | ~v3('$ki_local_world') | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ~v3(X0)) | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => v4(X1)))),
% 0.17/0.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat35)).
% 0.17/0.96
% 0.17/0.96 tff(f57,plain,(
% 0.17/0.96 v1('$ki_local_world') | v3('$ki_local_world') | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => v3(X1))) | ! [X2 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X2) => ! [X3 : '$ki_world'] : ('$ki_accessible'(X2,X3) => v4(X3)))),
% 0.17/0.96 inference(rectify,[],[f7])).
% 0.17/0.96
% 0.17/0.96 tff(f67,plain,(
% 0.17/0.96 v2('$ki_local_world') | ~v3('$ki_local_world') | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ~v1(X0)) | ! [X1 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X1) => ! [X2 : '$ki_world'] : ('$ki_accessible'(X1,X2) => ~v1(X2)))),
% 0.17/0.96 inference(rectify,[],[f20])).
% 0.17/0.96
% 0.17/0.96 tff(f75,plain,(
% 0.17/0.96 v3('$ki_local_world') | ~v4('$ki_local_world') | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => v3(X1))) | ! [X2 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X2) => ! [X3 : '$ki_world'] : ('$ki_accessible'(X2,X3) => ~v4(X3)))),
% 0.17/0.96 inference(rectify,[],[f28])).
% 0.17/0.96
% 0.17/0.96 tff(f78,plain,(
% 0.17/0.96 v4('$ki_local_world') | ~v1('$ki_local_world') | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ~v1(X0)) | ! [X1 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X1) => ! [X2 : '$ki_world'] : ('$ki_accessible'(X1,X2) => v3(X2)))),
% 0.17/0.96 inference(rectify,[],[f31])).
% 0.17/0.96
% 0.17/0.96 tff(f80,plain,(
% 0.17/0.96 v4('$ki_local_world') | ~v3('$ki_local_world') | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ! [X1 : '$ki_world'] : ('$ki_accessible'(X0,X1) => v1(X1))) | ! [X2 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X2) => ! [X3 : '$ki_world'] : ('$ki_accessible'(X2,X3) => v4(X3)))),
% 0.17/0.96 inference(rectify,[],[f33])).
% 0.17/0.96
% 0.17/0.96 tff(f83,plain,(
% 0.17/0.96 ~v1('$ki_local_world') | ~v2('$ki_local_world') | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ~v4(X0)) | ! [X1 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X1) => ! [X2 : '$ki_world'] : ('$ki_accessible'(X1,X2) => ~v1(X2)))),
% 0.17/0.96 inference(rectify,[],[f36])).
% 0.17/0.96
% 0.17/0.96 tff(f84,plain,(
% 0.17/0.96 ~v1('$ki_local_world') | ~v3('$ki_local_world') | ! [X0 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X0) => ~v3(X0)) | ! [X1 : '$ki_world'] : ('$ki_accessible'('$ki_local_world',X1) => ! [X2 : '$ki_world'] : ('$ki_accessible'(X1,X2) => v4(X2)))),
% 0.17/0.96 inference(rectify,[],[f37])).
% 0.17/0.96
% 0.17/0.96 tff(f106,plain,(
% 0.17/0.96 v1('$ki_local_world') | v2('$ki_local_world') | ~v3('$ki_local_world') | ! [X0 : '$ki_world'] : (! [X1 : '$ki_world'] : (~v4(X1) | ~'$ki_accessible'(X0,X1)) | ~'$ki_accessible'('$ki_local_world',X0))),
% 0.17/0.96 inference(ennf_transformation,[],[f5])).
% 0.17/0.96
% 0.17/0.96 tff(f108,plain,(
% 0.17/0.96 v1('$ki_local_world') | v3('$ki_local_world') | ! [X0 : '$ki_world'] : (! [X1 : '$ki_world'] : (v3(X1) | ~'$ki_accessible'(X0,X1)) | ~'$ki_accessible'('$ki_local_world',X0)) | ! [X2 : '$ki_world'] : (! [X3 : '$ki_world'] : (v4(X3) | ~'$ki_accessible'(X2,X3)) | ~'$ki_accessible'('$ki_local_world',X2))),
% 0.17/0.96 inference(ennf_transformation,[],[f57])).
% 0.17/0.96
% 0.17/0.96 tff(f110,plain,(
% 0.17/0.96 v1('$ki_local_world') | ~v2('$ki_local_world') | ~v4('$ki_local_world') | ! [X0 : '$ki_world'] : (! [X1 : '$ki_world'] : (~v2(X1) | ~'$ki_accessible'(X0,X1)) | ~'$ki_accessible'('$ki_local_world',X0))),
% 0.17/0.96 inference(ennf_transformation,[],[f9])).
% 0.17/0.96
% 0.17/0.96 tff(f121,plain,(
% 0.17/0.96 v2('$ki_local_world') | ~v3('$ki_local_world') | ! [X0 : '$ki_world'] : (~v1(X0) | ~'$ki_accessible'('$ki_local_world',X0)) | ! [X1 : '$ki_world'] : (! [X2 : '$ki_world'] : (~v1(X2) | ~'$ki_accessible'(X1,X2)) | ~'$ki_accessible'('$ki_local_world',X1))),
% 0.17/0.96 inference(ennf_transformation,[],[f67])).
% 0.17/0.96
% 0.17/0.96 tff(f129,plain,(
% 0.17/0.96 v3('$ki_local_world') | ~v4('$ki_local_world') | ! [X0 : '$ki_world'] : (! [X1 : '$ki_world'] : (v3(X1) | ~'$ki_accessible'(X0,X1)) | ~'$ki_accessible'('$ki_local_world',X0)) | ! [X2 : '$ki_world'] : (! [X3 : '$ki_world'] : (~v4(X3) | ~'$ki_accessible'(X2,X3)) | ~'$ki_accessible'('$ki_local_world',X2))),
% 0.17/0.96 inference(ennf_transformation,[],[f75])).
% 0.17/0.96
% 0.17/0.96 tff(f132,plain,(
% 0.17/0.96 v4('$ki_local_world') | ~v1('$ki_local_world') | ! [X0 : '$ki_world'] : (~v1(X0) | ~'$ki_accessible'('$ki_local_world',X0)) | ! [X1 : '$ki_world'] : (! [X2 : '$ki_world'] : (v3(X2) | ~'$ki_accessible'(X1,X2)) | ~'$ki_accessible'('$ki_local_world',X1))),
% 0.17/0.96 inference(ennf_transformation,[],[f78])).
% 0.17/0.96
% 0.17/0.96 tff(f134,plain,(
% 0.17/0.96 v4('$ki_local_world') | ~v3('$ki_local_world') | ! [X0 : '$ki_world'] : (! [X1 : '$ki_world'] : (v1(X1) | ~'$ki_accessible'(X0,X1)) | ~'$ki_accessible'('$ki_local_world',X0)) | ! [X2 : '$ki_world'] : (! [X3 : '$ki_world'] : (v4(X3) | ~'$ki_accessible'(X2,X3)) | ~'$ki_accessible'('$ki_local_world',X2))),
% 0.17/0.96 inference(ennf_transformation,[],[f80])).
% 0.17/0.96
% 0.17/0.96 tff(f137,plain,(
% 0.17/0.96 ~v1('$ki_local_world') | ~v2('$ki_local_world') | ! [X0 : '$ki_world'] : (~v4(X0) | ~'$ki_accessible'('$ki_local_world',X0)) | ! [X1 : '$ki_world'] : (! [X2 : '$ki_world'] : (~v1(X2) | ~'$ki_accessible'(X1,X2)) | ~'$ki_accessible'('$ki_local_world',X1))),
% 0.17/0.96 inference(ennf_transformation,[],[f83])).
% 0.17/0.96
% 0.17/0.96 tff(f138,plain,(
% 0.17/0.96 ~v1('$ki_local_world') | ~v3('$ki_local_world') | ! [X0 : '$ki_world'] : (~v3(X0) | ~'$ki_accessible'('$ki_local_world',X0)) | ! [X1 : '$ki_world'] : (! [X2 : '$ki_world'] : (v4(X2) | ~'$ki_accessible'(X1,X2)) | ~'$ki_accessible'('$ki_local_world',X1))),
% 0.17/0.96 inference(ennf_transformation,[],[f84])).
% 0.17/0.96
% 0.17/0.96 tff(f155,plain,(
% 0.17/0.96 ( ! [X0 : '$ki_world'] : ('$ki_accessible'(X0,X0)) )),
% 0.17/0.96 inference(cnf_transformation,[],[f1])).
% 0.17/0.96
% 0.17/0.96 tff(f159,plain,(
% 0.17/0.96 ( ! [X0 : '$ki_world',X1 : '$ki_world'] : (v1('$ki_local_world') | v2('$ki_local_world') | ~v3('$ki_local_world') | ~v4(X1) | ~'$ki_accessible'(X0,X1) | ~'$ki_accessible'('$ki_local_world',X0)) )),
% 0.17/0.96 inference(cnf_transformation,[],[f106])).
% 0.17/0.96
% 0.17/0.96 tff(f161,plain,(
% 0.17/0.96 ( ! [X2 : '$ki_world',X3 : '$ki_world',X0 : '$ki_world',X1 : '$ki_world'] : (v1('$ki_local_world') | v3('$ki_local_world') | v3(X1) | ~'$ki_accessible'(X0,X1) | ~'$ki_accessible'('$ki_local_world',X0) | v4(X3) | ~'$ki_accessible'(X2,X3) | ~'$ki_accessible'('$ki_local_world',X2)) )),
% 0.17/0.96 inference(cnf_transformation,[],[f108])).
% 0.17/0.96
% 0.17/0.96 tff(f163,plain,(
% 0.17/0.96 ( ! [X0 : '$ki_world',X1 : '$ki_world'] : (v1('$ki_local_world') | ~v2('$ki_local_world') | ~v4('$ki_local_world') | ~v2(X1) | ~'$ki_accessible'(X0,X1) | ~'$ki_accessible'('$ki_local_world',X0)) )),
% 0.17/0.96 inference(cnf_transformation,[],[f110])).
% 0.17/0.96
% 0.17/0.96 tff(f174,plain,(
% 0.17/0.96 ( ! [X2 : '$ki_world',X0 : '$ki_world',X1 : '$ki_world'] : (v2('$ki_local_world') | ~v3('$ki_local_world') | ~v1(X0) | ~'$ki_accessible'('$ki_local_world',X0) | ~v1(X2) | ~'$ki_accessible'(X1,X2) | ~'$ki_accessible'('$ki_local_world',X1)) )),
% 0.17/0.96 inference(cnf_transformation,[],[f121])).
% 0.17/0.96
% 0.17/0.96 tff(f182,plain,(
% 0.17/0.96 ( ! [X2 : '$ki_world',X3 : '$ki_world',X0 : '$ki_world',X1 : '$ki_world'] : (v3('$ki_local_world') | ~v4('$ki_local_world') | v3(X1) | ~'$ki_accessible'(X0,X1) | ~'$ki_accessible'('$ki_local_world',X0) | ~v4(X3) | ~'$ki_accessible'(X2,X3) | ~'$ki_accessible'('$ki_local_world',X2)) )),
% 0.17/0.96 inference(cnf_transformation,[],[f129])).
% 0.17/0.96
% 0.17/0.96 tff(f185,plain,(
% 0.17/0.96 ( ! [X2 : '$ki_world',X0 : '$ki_world',X1 : '$ki_world'] : (v4('$ki_local_world') | ~v1('$ki_local_world') | ~v1(X0) | ~'$ki_accessible'('$ki_local_world',X0) | v3(X2) | ~'$ki_accessible'(X1,X2) | ~'$ki_accessible'('$ki_local_world',X1)) )),
% 0.17/0.96 inference(cnf_transformation,[],[f132])).
% 0.17/0.96
% 0.17/0.96 tff(f187,plain,(
% 0.17/0.96 ( ! [X2 : '$ki_world',X3 : '$ki_world',X0 : '$ki_world',X1 : '$ki_world'] : (v4('$ki_local_world') | ~v3('$ki_local_world') | v1(X1) | ~'$ki_accessible'(X0,X1) | ~'$ki_accessible'('$ki_local_world',X0) | v4(X3) | ~'$ki_accessible'(X2,X3) | ~'$ki_accessible'('$ki_local_world',X2)) )),
% 0.17/0.96 inference(cnf_transformation,[],[f134])).
% 0.17/0.96
% 0.17/0.96 tff(f190,plain,(
% 0.17/0.96 ( ! [X2 : '$ki_world',X0 : '$ki_world',X1 : '$ki_world'] : (~v1('$ki_local_world') | ~v2('$ki_local_world') | ~v4(X0) | ~'$ki_accessible'('$ki_local_world',X0) | ~v1(X2) | ~'$ki_accessible'(X1,X2) | ~'$ki_accessible'('$ki_local_world',X1)) )),
% 0.17/0.96 inference(cnf_transformation,[],[f137])).
% 0.17/0.96
% 0.17/0.96 tff(f191,plain,(
% 0.17/0.96 ( ! [X2 : '$ki_world',X0 : '$ki_world',X1 : '$ki_world'] : (~v1('$ki_local_world') | ~v3('$ki_local_world') | ~v3(X0) | ~'$ki_accessible'('$ki_local_world',X0) | v4(X2) | ~'$ki_accessible'(X1,X2) | ~'$ki_accessible'('$ki_local_world',X1)) )),
% 0.17/0.96 inference(cnf_transformation,[],[f138])).
% 0.17/0.96
% 0.17/0.96 tcf(c_49,plain,![X0_'ki_world':'$ki_world']:
% 0.17/0.96 ('$ki_accessible'(X0_'ki_world',X0_'ki_world')),
% 0.17/0.96 inference(cnf_transformation,[],[f155])).
% 0.17/0.96
% 0.17/0.96 tcf(c_53,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 0.17/0.96 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'('$ki_local_world',X0_'ki_world')|
% 0.17/0.96 ~v4(X1_'ki_world')|~v3('$ki_local_world')|v1('$ki_local_world')|v2('$ki_local_world')),
% 0.17/0.96 inference(cnf_transformation,[],[f159])).
% 0.17/0.96
% 0.17/0.96 tcf(c_55,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world',X3_'ki_world':'$ki_world']:
% 0.17/0.96 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'(X2_'ki_world',X3_'ki_world')|
% 0.17/0.96 ~'$ki_accessible'('$ki_local_world',X0_'ki_world')|~'$ki_accessible'('$ki_local_world',X2_'ki_world')|
% 0.17/0.96 v3(X1_'ki_world')|v4(X3_'ki_world')|v1('$ki_local_world')|v3('$ki_local_world')),
% 0.17/0.96 inference(cnf_transformation,[],[f161])).
% 0.17/0.96
% 0.17/0.96 tcf(c_57,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world']:
% 0.17/0.96 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'('$ki_local_world',X0_'ki_world')|
% 0.17/0.96 ~v2(X1_'ki_world')|~v2('$ki_local_world')|~v4('$ki_local_world')|
% 0.17/0.96 v1('$ki_local_world')),
% 0.17/0.96 inference(cnf_transformation,[],[f163])).
% 0.17/0.96
% 0.17/0.96 tcf(c_68,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world']:
% 0.17/0.96 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'('$ki_local_world',X0_'ki_world')|
% 0.17/0.96 ~'$ki_accessible'('$ki_local_world',X2_'ki_world')|~v1(X1_'ki_world')|
% 0.17/0.96 ~v1(X2_'ki_world')|~v3('$ki_local_world')|v2('$ki_local_world')),
% 0.17/0.96 inference(cnf_transformation,[],[f174])).
% 0.17/0.96
% 0.17/0.96 tcf(c_76,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world',X3_'ki_world':'$ki_world']:
% 0.17/0.96 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'(X2_'ki_world',X3_'ki_world')|
% 0.17/0.96 ~'$ki_accessible'('$ki_local_world',X0_'ki_world')|~'$ki_accessible'('$ki_local_world',X2_'ki_world')|
% 0.17/0.96 ~v4(X3_'ki_world')|~v4('$ki_local_world')|v3(X1_'ki_world')|v3('$ki_local_world')),
% 0.17/0.96 inference(cnf_transformation,[],[f182])).
% 0.17/0.96
% 0.17/0.96 tcf(c_79,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world']:
% 0.17/0.96 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'('$ki_local_world',X0_'ki_world')|
% 0.17/0.96 ~'$ki_accessible'('$ki_local_world',X2_'ki_world')|~v1(X2_'ki_world')|
% 0.17/0.96 ~v1('$ki_local_world')|v3(X1_'ki_world')|v4('$ki_local_world')),
% 0.17/0.96 inference(cnf_transformation,[],[f185])).
% 0.17/0.96
% 0.17/0.96 tcf(c_81,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world',X3_'ki_world':'$ki_world']:
% 0.17/0.96 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'(X2_'ki_world',X3_'ki_world')|
% 0.17/0.96 ~'$ki_accessible'('$ki_local_world',X0_'ki_world')|~'$ki_accessible'('$ki_local_world',X2_'ki_world')|
% 0.17/0.96 ~v3('$ki_local_world')|v1(X1_'ki_world')|v4(X3_'ki_world')|v4('$ki_local_world')),
% 0.17/0.96 inference(cnf_transformation,[],[f187])).
% 0.17/0.96
% 0.17/0.96 tcf(c_84,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world']:
% 0.17/0.96 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'('$ki_local_world',X0_'ki_world')|
% 0.17/0.96 ~'$ki_accessible'('$ki_local_world',X2_'ki_world')|~v1(X1_'ki_world')|
% 0.17/0.96 ~v4(X2_'ki_world')|~v1('$ki_local_world')|~v2('$ki_local_world')),
% 0.17/0.96 inference(cnf_transformation,[],[f190])).
% 0.17/0.96
% 0.17/0.96 tcf(c_85,plain,![X0_'ki_world':'$ki_world',X1_'ki_world':'$ki_world',X2_'ki_world':'$ki_world']:
% 0.17/0.96 (~'$ki_accessible'(X0_'ki_world',X1_'ki_world')|~'$ki_accessible'('$ki_local_world',X0_'ki_world')|
% 0.17/0.96 ~'$ki_accessible'('$ki_local_world',X2_'ki_world')|~v3(X2_'ki_world')|
% 0.17/0.96 ~v1('$ki_local_world')|~v3('$ki_local_world')|v4(X1_'ki_world')),
% 0.17/0.96 inference(cnf_transformation,[],[f191])).
% 0.17/0.96
% 0.17/0.96 tcf(c_103,plain,
% 0.17/0.96 ('$ki_accessible'('$ki_local_world','$ki_local_world')),
% 0.17/0.96 inference(instantiation,[status(thm)],[c_49])).
% 0.17/0.96
% 0.17/0.96 tcf(c_104,plain,
% 0.17/0.96 (~'$ki_accessible'('$ki_local_world','$ki_local_world')|~v3('$ki_local_world')|
% 0.17/0.96 ~v4('$ki_local_world')|v1('$ki_local_world')|v2('$ki_local_world')),
% 0.17/0.96 inference(instantiation,[status(thm)],[c_53])).
% 0.17/0.96
% 0.17/0.96 tcf(c_106,plain,
% 0.17/0.96 (~'$ki_accessible'('$ki_local_world','$ki_local_world')|~v2('$ki_local_world')|
% 0.17/0.96 ~v4('$ki_local_world')|v1('$ki_local_world')),
% 0.17/0.96 inference(instantiation,[status(thm)],[c_57])).
% 0.17/0.96
% 0.17/0.96 tcf(c_109,plain,
% 0.17/0.96 (~'$ki_accessible'('$ki_local_world','$ki_local_world')|~v1('$ki_local_world')|
% 0.17/0.96 v3('$ki_local_world')|v4('$ki_local_world')),
% 0.17/0.96 inference(instantiation,[status(thm)],[c_79])).
% 0.17/0.96
% 0.17/0.96 tcf(c_111,plain,
% 0.17/0.96 (~'$ki_accessible'('$ki_local_world','$ki_local_world')|~v1('$ki_local_world')|
% 0.17/0.96 ~v3('$ki_local_world')|v4('$ki_local_world')),
% 0.17/0.96 inference(instantiation,[status(thm)],[c_85])).
% 0.17/0.96
% 0.17/0.96 tcf(c_113,plain,
% 0.17/0.96 (~'$ki_accessible'('$ki_local_world','$ki_local_world')|~v1('$ki_local_world')|
% 0.17/0.96 ~v3('$ki_local_world')|v2('$ki_local_world')),
% 0.17/0.96 inference(instantiation,[status(thm)],[c_68])).
% 0.17/0.96
% 0.17/0.96 tcf(c_114,plain,
% 0.17/0.96 (~'$ki_accessible'('$ki_local_world','$ki_local_world')|~v1('$ki_local_world')|
% 0.17/0.96 ~v2('$ki_local_world')|~v4('$ki_local_world')),
% 0.17/0.96 inference(instantiation,[status(thm)],[c_84])).
% 0.17/0.96
% 0.17/0.96 tcf(c_116,plain,
% 0.17/0.96 (~'$ki_accessible'('$ki_local_world','$ki_local_world')|v1('$ki_local_world')|
% 0.17/0.96 v3('$ki_local_world')|v4('$ki_local_world')),
% 0.17/0.96 inference(instantiation,[status(thm)],[c_55])).
% 0.17/0.96
% 0.17/0.96 tcf(c_117,plain,
% 0.17/0.96 (~'$ki_accessible'('$ki_local_world','$ki_local_world')|~v3('$ki_local_world')|
% 0.17/0.96 v1('$ki_local_world')|v4('$ki_local_world')),
% 0.17/0.96 inference(instantiation,[status(thm)],[c_81])).
% 0.17/0.96
% 0.17/0.96 tcf(c_119,plain,
% 0.17/0.96 (~'$ki_accessible'('$ki_local_world','$ki_local_world')|~v4('$ki_local_world')|
% 0.17/0.96 v3('$ki_local_world')),
% 0.17/0.96 inference(instantiation,[status(thm)],[c_76])).
% 0.17/0.96
% 0.17/0.96 tcf(c_126,plain,
% 0.17/0.96 ($false),
% 0.17/0.96 inference(prop_impl_just,
% 0.17/0.96 [status(thm)],
% 0.17/0.96 [c_119,c_117,c_116,c_114,c_113,c_111,c_109,c_106,c_104,c_103])).
% 0.17/0.96
% 0.17/0.96
% 0.17/0.96 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/0.96
% 0.17/0.96
%------------------------------------------------------------------------------