%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : LCL941_5 : TPTP v9.3.1. Released v8.2.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n009.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 : Mon Sep 7 03:01:12 PM UTC 2026
% Result : Theorem 0.57s 0.89s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL941_5 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.03 % Command : run_E %s %d THM
% 0.12/0.36 % Computer : n009.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Sun Sep 6 00:47:08 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.57/0.89 % SZS status Theorem
% 0.57/0.89 % SZS output start Proof
% 0.57/0.89 tff(tptp_fun___ki_accessible__type, type, (
% 0.57/0.89 tptp_fun___ki_accessible_: ( |'$ki_world'| * |'$ki_world'| ) > $o)).
% 0.57/0.89 tff(tptp_fun_W_82_type, type, (
% 0.57/0.89 tptp_fun_W_82: |'$ki_world'|)).
% 0.57/0.89 tff(tptp_fun_W_92_type, type, (
% 0.57/0.89 tptp_fun_W_92: |'$ki_world'|)).
% 0.57/0.89 tff(qmltpeq_type, type, (
% 0.57/0.89 qmltpeq: ( |'$ki_world'| * $i * $i ) > $o)).
% 0.57/0.89 tff(e1_type, type, (
% 0.57/0.89 e1: $i)).
% 0.57/0.89 tff(op_type, type, (
% 0.57/0.89 op: ( $i * $i ) > $i)).
% 0.57/0.89 tff(e2_type, type, (
% 0.57/0.89 e2: $i)).
% 0.57/0.89 tff(e3_type, type, (
% 0.57/0.89 e3: $i)).
% 0.57/0.89 tff(e0_type, type, (
% 0.57/0.89 e0: $i)).
% 0.57/0.89 tff(tptp_fun_W_79_type, type, (
% 0.57/0.89 tptp_fun_W_79: |'$ki_world'|)).
% 0.57/0.89 tff(tptp_fun___ki_local_world__type, type, (
% 0.57/0.89 tptp_fun___ki_local_world_: |'$ki_world'|)).
% 0.57/0.89 tff(tptp_fun_W_78_type, type, (
% 0.57/0.89 tptp_fun_W_78: |'$ki_world'|)).
% 0.57/0.89 tff(tptp_fun_W_77_type, type, (
% 0.57/0.89 tptp_fun_W_77: |'$ki_world'|)).
% 0.57/0.89 tff(tptp_fun_W_76_type, type, (
% 0.57/0.89 tptp_fun_W_76: |'$ki_world'|)).
% 0.57/0.89 tff(tptp_fun_W_88_type, type, (
% 0.57/0.89 tptp_fun_W_88: |'$ki_world'|)).
% 0.57/0.89 tff(tptp_fun_W_91_type, type, (
% 0.57/0.89 tptp_fun_W_91: |'$ki_world'|)).
% 0.57/0.89 tff(tptp_fun_W_90_type, type, (
% 0.57/0.89 tptp_fun_W_90: |'$ki_world'|)).
% 0.57/0.89 tff(tptp_fun_W_89_type, type, (
% 0.57/0.89 tptp_fun_W_89: |'$ki_world'|)).
% 0.57/0.89 tff(tptp_fun_W_87_type, type, (
% 0.57/0.89 tptp_fun_W_87: |'$ki_world'|)).
% 0.57/0.89 tff(tptp_fun_W_86_type, type, (
% 0.57/0.89 tptp_fun_W_86: |'$ki_world'|)).
% 0.57/0.89 tff(tptp_fun_W_84_type, type, (
% 0.57/0.89 tptp_fun_W_84: |'$ki_world'|)).
% 0.57/0.89 tff(tptp_fun_W_85_type, type, (
% 0.57/0.89 tptp_fun_W_85: |'$ki_world'|)).
% 0.57/0.89 tff(tptp_fun_W_81_type, type, (
% 0.57/0.89 tptp_fun_W_81: |'$ki_world'|)).
% 0.57/0.89 tff(tptp_fun_W_80_type, type, (
% 0.57/0.89 tptp_fun_W_80: |'$ki_world'|)).
% 0.57/0.89 tff(tptp_fun_W_83_type, type, (
% 0.57/0.89 tptp_fun_W_83: |'$ki_world'|)).
% 0.57/0.89 tff(1,assumption,(~((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e0, e0), e0))) | (~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e1, e1), e0))) | (~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e2, e2), e0))) | (~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e3, e3), e0))))), introduced(assumption)).
% 0.57/0.89 tff(2,plain,
% 0.57/0.89 (((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e0, e0), e0))) | (~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e1, e1), e0))) | (~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e2, e2), e0))) | (~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e3, e3), e0)))) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e3, e3), e0))),
% 0.57/0.89 inference(tautology,[status(thm)],[])).
% 0.57/0.89 tff(3,plain,
% 0.57/0.89 (![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e3, e3), e0))),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[2, 1])).
% 0.57/0.89 tff(4,assumption,(~tptp_fun___ki_accessible_(W!92, W!79)), introduced(assumption)).
% 0.57/0.89 tff(5,plain,
% 0.57/0.89 (^[W: |'$ki_world'|, V: |'$ki_world'|] : refl(tptp_fun___ki_accessible_(W, V) <=> tptp_fun___ki_accessible_(W, V))),
% 0.57/0.89 inference(bind,[status(th)],[])).
% 0.57/0.89 tff(6,plain,
% 0.57/0.89 (![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V) <=> ![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)),
% 0.57/0.89 inference(quant_intro,[status(thm)],[5])).
% 0.57/0.89 tff(7,plain,
% 0.57/0.89 (![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V) <=> ![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)),
% 0.57/0.89 inference(rewrite,[status(thm)],[])).
% 0.57/0.89 tff(8,axiom,(![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mrel_universal')).
% 0.57/0.89 tff(9,plain,
% 0.57/0.89 (![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)),
% 0.57/0.89 inference(modus_ponens,[status(thm)],[8, 7])).
% 0.57/0.89 tff(10,plain,(
% 0.57/0.89 ![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)),
% 0.57/0.89 inference(skolemize,[status(sab)],[9])).
% 0.57/0.89 tff(11,plain,
% 0.57/0.89 (![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)),
% 0.57/0.89 inference(modus_ponens,[status(thm)],[10, 6])).
% 0.57/0.89 tff(12,plain,
% 0.57/0.89 ((~![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)) | tptp_fun___ki_accessible_(W!92, W!79)),
% 0.57/0.89 inference(quant_inst,[status(thm)],[])).
% 0.57/0.89 tff(13,plain,
% 0.57/0.89 ($false),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[12, 11, 4])).
% 0.57/0.89 tff(14,plain,(tptp_fun___ki_accessible_(W!92, W!79)), inference(lemma,lemma(discharge,[]))).
% 0.57/0.89 tff(15,assumption,(![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e3, e3), e0))), introduced(assumption)).
% 0.57/0.89 tff(16,assumption,(~qmltpeq(W!79, op(e3, e3), e0)), introduced(assumption)).
% 0.57/0.89 tff(17,plain,
% 0.57/0.89 (((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e3, e3), e0))) | ((~tptp_fun___ki_accessible_(W!92, W!79)) | qmltpeq(W!79, op(e3, e3), e0))) <=> ((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e3, e3), e0))) | (~tptp_fun___ki_accessible_(W!92, W!79)) | qmltpeq(W!79, op(e3, e3), e0))),
% 0.57/0.89 inference(rewrite,[status(thm)],[])).
% 0.57/0.89 tff(18,plain,
% 0.57/0.89 ((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e3, e3), e0))) | ((~tptp_fun___ki_accessible_(W!92, W!79)) | qmltpeq(W!79, op(e3, e3), e0))),
% 0.57/0.89 inference(quant_inst,[status(thm)],[])).
% 0.57/0.89 tff(19,plain,
% 0.57/0.89 ((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e3, e3), e0))) | (~tptp_fun___ki_accessible_(W!92, W!79)) | qmltpeq(W!79, op(e3, e3), e0)),
% 0.57/0.89 inference(modus_ponens,[status(thm)],[18, 17])).
% 0.57/0.89 tff(20,plain,
% 0.57/0.89 ($false),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[19, 16, 15, 14])).
% 0.57/0.89 tff(21,plain,((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e3, e3), e0))) | qmltpeq(W!79, op(e3, e3), e0)), inference(lemma,lemma(discharge,[]))).
% 0.57/0.89 tff(22,plain,
% 0.57/0.89 (qmltpeq(W!79, op(e3, e3), e0)),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[21, 3])).
% 0.57/0.89 tff(23,plain,
% 0.57/0.89 (((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W!79)) | qmltpeq(W!79, op(e3, e3), e0)) | (~qmltpeq(W!79, op(e3, e3), e0))),
% 0.57/0.89 inference(tautology,[status(thm)],[])).
% 0.57/0.89 tff(24,plain,
% 0.57/0.89 ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W!79)) | qmltpeq(W!79, op(e3, e3), e0)),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[23, 22])).
% 0.57/0.89 tff(25,assumption,(~tptp_fun___ki_accessible_(W!92, W!78)), introduced(assumption)).
% 0.57/0.89 tff(26,plain,
% 0.57/0.89 ((~![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)) | tptp_fun___ki_accessible_(W!92, W!78)),
% 0.57/0.89 inference(quant_inst,[status(thm)],[])).
% 0.57/0.89 tff(27,plain,
% 0.57/0.89 ($false),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[26, 11, 25])).
% 0.57/0.89 tff(28,plain,(tptp_fun___ki_accessible_(W!92, W!78)), inference(lemma,lemma(discharge,[]))).
% 0.57/0.89 tff(29,plain,
% 0.57/0.89 (((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e0, e0), e0))) | (~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e1, e1), e0))) | (~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e2, e2), e0))) | (~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e3, e3), e0)))) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e2, e2), e0))),
% 0.57/0.89 inference(tautology,[status(thm)],[])).
% 0.57/0.89 tff(30,plain,
% 0.57/0.89 (![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e2, e2), e0))),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[29, 1])).
% 0.57/0.89 tff(31,plain,
% 0.57/0.89 (((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e2, e2), e0))) | ((~tptp_fun___ki_accessible_(W!92, W!78)) | qmltpeq(W!78, op(e2, e2), e0))) <=> ((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e2, e2), e0))) | (~tptp_fun___ki_accessible_(W!92, W!78)) | qmltpeq(W!78, op(e2, e2), e0))),
% 0.57/0.89 inference(rewrite,[status(thm)],[])).
% 0.57/0.89 tff(32,plain,
% 0.57/0.89 ((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e2, e2), e0))) | ((~tptp_fun___ki_accessible_(W!92, W!78)) | qmltpeq(W!78, op(e2, e2), e0))),
% 0.57/0.89 inference(quant_inst,[status(thm)],[])).
% 0.57/0.89 tff(33,plain,
% 0.57/0.89 ((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e2, e2), e0))) | (~tptp_fun___ki_accessible_(W!92, W!78)) | qmltpeq(W!78, op(e2, e2), e0)),
% 0.57/0.89 inference(modus_ponens,[status(thm)],[32, 31])).
% 0.57/0.89 tff(34,plain,
% 0.57/0.89 (qmltpeq(W!78, op(e2, e2), e0)),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[33, 30, 28])).
% 0.57/0.89 tff(35,plain,
% 0.57/0.89 (((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W!78)) | qmltpeq(W!78, op(e2, e2), e0)) | (~qmltpeq(W!78, op(e2, e2), e0))),
% 0.57/0.89 inference(tautology,[status(thm)],[])).
% 0.57/0.89 tff(36,plain,
% 0.57/0.89 ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W!78)) | qmltpeq(W!78, op(e2, e2), e0)),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[35, 34])).
% 0.57/0.89 tff(37,assumption,(~tptp_fun___ki_accessible_(W!92, W!77)), introduced(assumption)).
% 0.57/0.89 tff(38,plain,
% 0.57/0.89 ((~![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)) | tptp_fun___ki_accessible_(W!92, W!77)),
% 0.57/0.89 inference(quant_inst,[status(thm)],[])).
% 0.57/0.89 tff(39,plain,
% 0.57/0.89 ($false),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[38, 11, 37])).
% 0.57/0.89 tff(40,plain,(tptp_fun___ki_accessible_(W!92, W!77)), inference(lemma,lemma(discharge,[]))).
% 0.57/0.89 tff(41,plain,
% 0.57/0.89 (((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e0, e0), e0))) | (~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e1, e1), e0))) | (~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e2, e2), e0))) | (~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e3, e3), e0)))) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e1, e1), e0))),
% 0.57/0.89 inference(tautology,[status(thm)],[])).
% 0.57/0.89 tff(42,plain,
% 0.57/0.89 (![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e1, e1), e0))),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[41, 1])).
% 0.57/0.89 tff(43,plain,
% 0.57/0.89 (((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e1, e1), e0))) | ((~tptp_fun___ki_accessible_(W!92, W!77)) | qmltpeq(W!77, op(e1, e1), e0))) <=> ((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e1, e1), e0))) | (~tptp_fun___ki_accessible_(W!92, W!77)) | qmltpeq(W!77, op(e1, e1), e0))),
% 0.57/0.89 inference(rewrite,[status(thm)],[])).
% 0.57/0.89 tff(44,plain,
% 0.57/0.89 ((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e1, e1), e0))) | ((~tptp_fun___ki_accessible_(W!92, W!77)) | qmltpeq(W!77, op(e1, e1), e0))),
% 0.57/0.89 inference(quant_inst,[status(thm)],[])).
% 0.57/0.89 tff(45,plain,
% 0.57/0.89 ((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e1, e1), e0))) | (~tptp_fun___ki_accessible_(W!92, W!77)) | qmltpeq(W!77, op(e1, e1), e0)),
% 0.57/0.89 inference(modus_ponens,[status(thm)],[44, 43])).
% 0.57/0.89 tff(46,plain,
% 0.57/0.89 (qmltpeq(W!77, op(e1, e1), e0)),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[45, 42, 40])).
% 0.57/0.89 tff(47,plain,
% 0.57/0.89 (((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W!77)) | qmltpeq(W!77, op(e1, e1), e0)) | (~qmltpeq(W!77, op(e1, e1), e0))),
% 0.57/0.89 inference(tautology,[status(thm)],[])).
% 0.57/0.89 tff(48,plain,
% 0.57/0.89 ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W!77)) | qmltpeq(W!77, op(e1, e1), e0)),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[47, 46])).
% 0.57/0.89 tff(49,assumption,(~tptp_fun___ki_accessible_(W!92, W!76)), introduced(assumption)).
% 0.57/0.89 tff(50,plain,
% 0.57/0.89 ((~![W: |'$ki_world'|, V: |'$ki_world'|] : tptp_fun___ki_accessible_(W, V)) | tptp_fun___ki_accessible_(W!92, W!76)),
% 0.57/0.89 inference(quant_inst,[status(thm)],[])).
% 0.57/0.89 tff(51,plain,
% 0.57/0.89 ($false),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[50, 11, 49])).
% 0.57/0.89 tff(52,plain,(tptp_fun___ki_accessible_(W!92, W!76)), inference(lemma,lemma(discharge,[]))).
% 0.57/0.89 tff(53,plain,
% 0.57/0.89 (((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e0, e0), e0))) | (~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e1, e1), e0))) | (~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e2, e2), e0))) | (~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e3, e3), e0)))) | ![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e0, e0), e0))),
% 0.57/0.89 inference(tautology,[status(thm)],[])).
% 0.57/0.89 tff(54,plain,
% 0.57/0.89 (![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e0, e0), e0))),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[53, 1])).
% 0.57/0.89 tff(55,plain,
% 0.57/0.89 (((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e0, e0), e0))) | ((~tptp_fun___ki_accessible_(W!92, W!76)) | qmltpeq(W!76, op(e0, e0), e0))) <=> ((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e0, e0), e0))) | (~tptp_fun___ki_accessible_(W!92, W!76)) | qmltpeq(W!76, op(e0, e0), e0))),
% 0.57/0.89 inference(rewrite,[status(thm)],[])).
% 0.57/0.89 tff(56,plain,
% 0.57/0.89 ((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e0, e0), e0))) | ((~tptp_fun___ki_accessible_(W!92, W!76)) | qmltpeq(W!76, op(e0, e0), e0))),
% 0.57/0.89 inference(quant_inst,[status(thm)],[])).
% 0.57/0.89 tff(57,plain,
% 0.57/0.89 ((~![W0: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(W!92, W0)) | qmltpeq(W0, op(e0, e0), e0))) | (~tptp_fun___ki_accessible_(W!92, W!76)) | qmltpeq(W!76, op(e0, e0), e0)),
% 0.57/0.89 inference(modus_ponens,[status(thm)],[56, 55])).
% 0.57/0.89 tff(58,plain,
% 0.57/0.89 (qmltpeq(W!76, op(e0, e0), e0)),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[57, 54, 52])).
% 0.57/0.89 tff(59,plain,
% 0.57/0.89 (((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W!76)) | qmltpeq(W!76, op(e0, e0), e0)) | (~qmltpeq(W!76, op(e0, e0), e0))),
% 0.57/0.89 inference(tautology,[status(thm)],[])).
% 0.57/0.89 tff(60,plain,
% 0.57/0.89 ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W!76)) | qmltpeq(W!76, op(e0, e0), e0)),
% 0.57/0.89 inference(unit_resolution,[status(thm)],[59, 58])).
% 0.57/0.89 tff(61,plain,
% 0.57/0.89 ((~(![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e0, e0), e0)) & ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e1, e1), e0)) & ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e2, e2), e0)) & ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e3, e3), e0)))) <=> (~(![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e0, e0), e0)) & ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e1, e1), e0)) & ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e2, e2), e0)) & ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e3, e3), e0))))),
% 0.57/0.89 inference(rewrite,[status(thm)],[])).
% 0.57/0.89 tff(62,plain,
% 0.57/0.89 ((~(((![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e0, e0), e0)) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e1, e1), e0))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e2, e2), e0))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e3, e3), e0)))) <=> (~(![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e0, e0), e0)) & ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e1, e1), e0)) & ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e2, e2), e0)) & ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e3, e3), e0))))),
% 0.57/0.89 inference(rewrite,[status(thm)],[])).
% 0.57/0.89 tff(63,axiom,(~(((((((![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e0, e0), e0)) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e1, e1), e0))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e2, e2), e0))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e3, e3), e0))) | (((![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e0, e0), e1)) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e1, e1), e1))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e2, e2), e1))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e3, e3), e1)))) | (((![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e0, e0), e2)) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e1, e1), e2))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e2, e2), e2))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e3, e3), e2)))) | (((![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e0, e0), e3)) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e1, e1), e3))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e2, e2), e3))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e3, e3), e3)))) | ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => (~((((((![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => qmltpeq(W0, op(e0, e0), e0)) & ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => qmltpeq(W0, op(e1, e1), e0))) & ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => qmltpeq(W0, op(e2, e2), e0))) & ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => qmltpeq(W0, op(e3, e3), e0))) | (((![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => qmltpeq(W0, op(e0, e0), e1)) & ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => qmltpeq(W0, op(e1, e1), e1))) & ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => qmltpeq(W0, op(e2, e2), e1))) & ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => qmltpeq(W0, op(e3, e3), e1)))) | (((![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => qmltpeq(W0, op(e0, e0), e2)) & ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => qmltpeq(W0, op(e1, e1), e2))) & ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => qmltpeq(W0, op(e2, e2), e2))) & ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => qmltpeq(W0, op(e3, e3), e2)))) | (((![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => qmltpeq(W0, op(e0, e0), e3)) & ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => qmltpeq(W0, op(e1, e1), e3))) & ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => qmltpeq(W0, op(e2, e2), e3))) & ![W0: |'$ki_world'|] : (tptp_fun___ki_accessible_(W, W0) => qmltpeq(W0, op(e3, e3), e3)))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','verify')).
% 0.66/0.90 tff(64,plain,
% 0.66/0.90 (~((((((![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e0, e0), e0)) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e1, e1), e0))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e2, e2), e0))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e3, e3), e0))) | (((![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e0, e0), e1)) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e1, e1), e1))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e2, e2), e1))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e3, e3), e1)))) | (((![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e0, e0), e2)) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e1, e1), e2))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e2, e2), e2))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e3, e3), e2)))) | (((![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e0, e0), e3)) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e1, e1), e3))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e2, e2), e3))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e3, e3), e3))))),
% 0.66/0.90 inference(or_elim,[status(thm)],[63])).
% 0.66/0.90 tff(65,plain,
% 0.66/0.90 (~(((((![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e0, e0), e0)) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e1, e1), e0))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e2, e2), e0))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e3, e3), e0))) | (((![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e0, e0), e1)) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e1, e1), e1))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e2, e2), e1))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e3, e3), e1)))) | (((![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e0, e0), e2)) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e1, e1), e2))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e2, e2), e2))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e3, e3), e2))))),
% 0.66/0.90 inference(or_elim,[status(thm)],[64])).
% 0.66/0.90 tff(66,plain,
% 0.66/0.90 (~((((![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e0, e0), e0)) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e1, e1), e0))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e2, e2), e0))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e3, e3), e0))) | (((![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e0, e0), e1)) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e1, e1), e1))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e2, e2), e1))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e3, e3), e1))))),
% 0.66/0.90 inference(or_elim,[status(thm)],[65])).
% 0.66/0.90 tff(67,plain,
% 0.66/0.90 (~(((![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e0, e0), e0)) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e1, e1), e0))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e2, e2), e0))) & ![W: |'$ki_world'|] : (tptp_fun___ki_accessible_(|'$ki_local_world'|, W) => qmltpeq(W, op(e3, e3), e0)))),
% 0.66/0.90 inference(or_elim,[status(thm)],[66])).
% 0.66/0.90 tff(68,plain,
% 0.66/0.90 (~(![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e0, e0), e0)) & ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e1, e1), e0)) & ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e2, e2), e0)) & ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e3, e3), e0)))),
% 0.66/0.90 inference(modus_ponens,[status(thm)],[67, 62])).
% 0.66/0.90 tff(69,plain,
% 0.66/0.90 (~(![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e0, e0), e0)) & ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e1, e1), e0)) & ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e2, e2), e0)) & ![W: |'$ki_world'|] : ((~tptp_fun___ki_accessible_(|'$ki_local_world'|, W)) | qmltpeq(W, op(e3, e3), e0)))),
% 0.66/0.90 inference(modus_ponens,[status(thm)],[68, 61])).
% 0.66/0.90 unexpected number of arguments: (let ((a!1 (forall ((W |'$ki_world'|))
% 0.66/0.90 (or (not (|'$ki_accessible'| |'$ki_local_world'| W))
% 0.66/0.90 (qmltpeq W (op e0 e0) e0))))
% 0.66/0.90 (a!2 (not (or (not (|'$ki_accessible'| |'$ki_local_world'| W!76))
% 0.66/0.90 (qmltpeq W!76 (op e0 e0) e0))))
% 0.66/0.90 (a!3 (forall ((W |'$ki_world'|))
% 0.66/0.90 (or (not (|'$ki_accessible'| |'$ki_local_world'| W))
% 0.66/0.90 (qmltpeq W (op e1 e1) e0))))
% 0.66/0.90 (a!4 (not (or (not (|'$ki_accessible'| |'$ki_local_world'| W!77))
% 0.66/0.90 (qmltpeq W!77 (op e1 e1) e0))))
% 0.66/0.90 (a!5 (forall ((W |'$ki_world'|))
% 0.66/0.90 (or (not (|'$ki_accessible'| |'$ki_local_world'| W))
% 0.66/0.90 (qmltpeq W (op e2 e2) e0))))
% 0.66/0.90 (a!6 (not (or (not (|'$ki_accessible'| |'$ki_local_world'| W!78))
% 0.66/0.90 (qmltpeq W!78 (op e2 e2) e0))))
% 0.66/0.90 (a!7 (forall ((W |'$ki_world'|))
% 0.66/0.90 (or (not (|'$ki_accessible'| |'$ki_local_world'| W))
% 0.66/0.90 (qmltpeq W (op e3 e3) e0))))
% 0.66/0.90 (a!8 (not (or (not (|'$ki_accessible'| |'$ki_local_world'| W!79))
% 0.66/0.90 (qmltpeq W!79 (op e3 e3) e0)))))
% 0.66/0.90 (nnf-neg (sk (~ (not a!1) a!2))
% 0.66/0.90 (sk (~ (not a!3) a!4))
% 0.66/0.90 (sk (~ (not a!5) a!6))
% 0.66/0.90 (sk (~ (not a!7) a!8))
% 0.66/0.90 (~ (not (and a!1 a!3 a!5 a!7)) (or a!2 a!4 a!6 a!8))))
% 0.66/0.90 Proof display could not be completed: unexpected number of arguments
% 0.66/0.93 % E exiting
%------------------------------------------------------------------------------