%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : NLP265^17 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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 : Wed Oct 7 10:32:43 AM UTC 2026
% Result : Theorem 1.31s 0.53s
% Output : CNFRefutation 1.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP265^17 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.18 % Computer : n002.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Oct 6 13:01:42 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.31/0.53
% 1.31/0.53 No.of.Axioms: 12
% 1.31/0.53
% 1.31/0.53 Length.of.Defs: 1296
% 1.31/0.53
% 1.31/0.53 Contains.Choice.Funs: false
% 1.31/0.53 .......eprover: <stdin>:1:(Column 88):(just read ''#i_alice''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 1.31/0.53 .eprover: <stdin>:1:(Column 88):(just read ''#i_alice''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 1.31/0.53 .eprover: <stdin>:1:(Column 88):(just read ''#i_alice''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 1.31/0.53 ..eprover: <stdin>:1:(Column 88):(just read ''#i_alice''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 1.31/0.53 .eprover: <stdin>:1:(Column 88):(just read ''#i_alice''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 1.31/0.53 ..eprover: <stdin>:1:(Column 88):(just read ''#i_alice''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 1.31/0.53 ..
% 1.31/0.53
% 1.31/0.53 ********************************
% 1.31/0.53 * All subproblems solved! *
% 1.31/0.53 ********************************
% 1.31/0.53 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:13,ps:3,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:583,loop_count:28,foatp_calls:6,translation:fof_full)
% 1.31/0.53
% 1.31/0.53 %**** Beginning of derivation protocol ****
% 1.31/0.53 % SZS output start CNFRefutation
% 1.31/0.53 thf(tp_mindex,type,(mindex: $tType)).
% 1.31/0.53 thf(tp_mworld,type,(mworld: $tType)).
% 1.31/0.53 thf(tp_'#b_alice',type,('#b_alice': mindex)).
% 1.31/0.53 thf(tp_'#b_bob',type,('#b_bob': mindex)).
% 1.31/0.53 thf(tp_'#i_alice',type,('#i_alice': mindex)).
% 1.31/0.53 thf(tp_'#i_bob',type,('#i_bob': mindex)).
% 1.31/0.53 thf(tp_bigcity,type,(bigcity: ($i>(mworld>$o)))).
% 1.31/0.53 thf(tp_mactual,type,(mactual: mworld)).
% 1.31/0.53 thf(tp_mand,type,(mand: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 1.31/0.53 thf(tp_mbox,type,(mbox: (mindex>((mworld>$o)>(mworld>$o))))).
% 1.31/0.53 thf(tp_mdia,type,(mdia: (mindex>((mworld>$o)>(mworld>$o))))).
% 1.31/0.53 thf(tp_mequiv,type,(mequiv: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 1.31/0.53 thf(tp_mimplies,type,(mimplies: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 1.31/0.53 thf(tp_mlocal,type,(mlocal: ((mworld>$o)>$o))).
% 1.31/0.53 thf(tp_mnot,type,(mnot: ((mworld>$o)>(mworld>$o)))).
% 1.31/0.53 thf(tp_mor,type,(mor: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 1.31/0.53 thf(tp_mrel,type,(mrel: (mindex>(mworld>(mworld>$o))))).
% 1.31/0.53 thf(tp_portland,type,(portland: $i)).
% 1.31/0.53 thf(tp_sK1_SY11,type,(sK1_SY11: mworld)).
% 1.31/0.53 thf(tp_sK2_SX0,type,(sK2_SX0: mworld)).
% 1.31/0.53 thf(tp_sK3_SY172,type,(sK3_SY172: (mworld>mworld))).
% 1.31/0.53 thf(tp_sK4_SY180,type,(sK4_SY180: (mworld>mworld))).
% 1.31/0.53 thf(tp_sK5_SY188,type,(sK5_SY188: (mworld>mworld))).
% 1.31/0.53 thf(tp_sK6_SY189,type,(sK6_SY189: (mworld>mworld))).
% 1.31/0.53 thf(mand,definition,(mand = (^[A:(mworld>$o),B:(mworld>$o),W:mworld]: ((A@W) & (B@W)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mand_def)).
% 1.31/0.53 thf(mbox,definition,(mbox = (^[R:mindex,Phi:(mworld>$o),W:mworld]: (![V:mworld]: ((((mrel@R)@W)@V) => (Phi@V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mbox_def)).
% 1.31/0.53 thf(mdia,definition,(mdia = (^[R:mindex,Phi:(mworld>$o),W:mworld]: (?[V:mworld]: ((((mrel@R)@W)@V) & (Phi@V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mdia_def)).
% 1.31/0.53 thf(mequiv,definition,(mequiv = (^[A:(mworld>$o),B:(mworld>$o),W:mworld]: ((A@W) <=> (B@W)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mequiv_def)).
% 1.31/0.53 thf(mimplies,definition,(mimplies = (^[A:(mworld>$o),B:(mworld>$o),W:mworld]: ((A@W) => (B@W)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mimplies_def)).
% 1.31/0.53 thf(mlocal,definition,(mlocal = (^[Phi:(mworld>$o)]: (Phi@mactual))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mlocal_def)).
% 1.31/0.53 thf(mnot,definition,(mnot = (^[A:(mworld>$o),W:mworld]: (~ (A@W)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mnot_def)).
% 1.31/0.53 thf(mor,definition,(mor = (^[A:(mworld>$o),B:(mworld>$o),W:mworld]: ((A@W) | (B@W)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mor_def)).
% 1.31/0.53 thf(1,axiom,(mlocal@((mbox@'#b_alice')@((mbox@'#b_bob')@(mnot@(bigcity@portland))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3)).
% 1.31/0.53 thf(2,axiom,(mlocal@((mbox@'#b_alice')@(bigcity@portland))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2)).
% 1.31/0.53 thf(6,axiom,(![W:mworld]: (((mrel@'#b_bob')@W)@W)),file('/export/starexec/sandbox/benchmark/theBenchmark.p','mrel_#b_bob_reflexive')).
% 1.31/0.53 thf(8,axiom,(![W:mworld]: (((mrel@'#b_alice')@W)@W)),file('/export/starexec/sandbox/benchmark/theBenchmark.p','mrel_#b_alice_reflexive')).
% 1.31/0.53 thf(16,plain,(((![SY27:mworld]: ((((mrel@'#b_alice')@mactual)@SY27) => (![SY26:mworld]: ((((mrel@'#b_bob')@SY27)@SY26) => (~ ((bigcity@portland)@SY26))))))=$true)),inference(unfold_def,[status(thm)],[1,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 1.31/0.53 thf(17,plain,(((![SY36:mworld]: ((((mrel@'#b_alice')@mactual)@SY36) => ((bigcity@portland)@SY36)))=$true)),inference(unfold_def,[status(thm)],[2,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 1.31/0.53 thf(21,plain,(((![W:mworld]: (((mrel@'#b_bob')@W)@W))=$true)),inference(unfold_def,[status(thm)],[6,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 1.31/0.53 thf(23,plain,(((![W:mworld]: (((mrel@'#b_alice')@W)@W))=$true)),inference(unfold_def,[status(thm)],[8,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 1.31/0.53 thf(36,plain,(((![W:mworld]: (((mrel@'#b_alice')@W)@W))=$true)),inference(copy,[status(thm)],[23])).
% 1.31/0.53 thf(38,plain,(((![W:mworld]: (((mrel@'#b_bob')@W)@W))=$true)),inference(copy,[status(thm)],[21])).
% 1.31/0.53 thf(42,plain,(((![SY36:mworld]: ((((mrel@'#b_alice')@mactual)@SY36) => ((bigcity@portland)@SY36)))=$true)),inference(copy,[status(thm)],[17])).
% 1.31/0.53 thf(43,plain,(((![SY27:mworld]: ((((mrel@'#b_alice')@mactual)@SY27) => (![SY26:mworld]: ((((mrel@'#b_bob')@SY27)@SY26) => (~ ((bigcity@portland)@SY26))))))=$true)),inference(copy,[status(thm)],[16])).
% 1.31/0.53 thf(46,plain,(((![SX0:mworld]: ((~ (((mrel@'#b_alice')@mactual)@SX0)) | (![SX1:mworld]: ((~ (((mrel@'#b_bob')@SX0)@SX1)) | (~ ((bigcity@portland)@SX1))))))=$true)),inference(unfold_def,[status(thm)],[43,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 1.31/0.53 thf(49,plain,(((![SX0:mworld]: ((~ (((mrel@'#b_alice')@mactual)@SX0)) | ((bigcity@portland)@SX0)))=$true)),inference(unfold_def,[status(thm)],[42,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 1.31/0.53 thf(57,plain,(![SV3:mworld]: (((((mrel@'#b_alice')@SV3)@SV3)=$true))),inference(extcnf_forall_pos,[status(thm)],[36])).
% 1.31/0.53 thf(58,plain,(![SV4:mworld]: (((((mrel@'#b_bob')@SV4)@SV4)=$true))),inference(extcnf_forall_pos,[status(thm)],[38])).
% 1.31/0.53 thf(59,plain,(![SV5:mworld]: ((((~ (((mrel@'#b_alice')@mactual)@SV5)) | (![SY167:mworld]: ((~ (((mrel@'#b_bob')@SV5)@SY167)) | (~ ((bigcity@portland)@SY167)))))=$true))),inference(extcnf_forall_pos,[status(thm)],[46])).
% 1.31/0.53 thf(62,plain,(![SV8:mworld]: ((((~ (((mrel@'#b_alice')@mactual)@SV8)) | ((bigcity@portland)@SV8))=$true))),inference(extcnf_forall_pos,[status(thm)],[49])).
% 1.31/0.53 thf(68,plain,(![SV5:mworld]: (((~ (((mrel@'#b_alice')@mactual)@SV5))=$true) | ((![SY167:mworld]: ((~ (((mrel@'#b_bob')@SV5)@SY167)) | (~ ((bigcity@portland)@SY167))))=$true))),inference(extcnf_or_pos,[status(thm)],[59])).
% 1.31/0.53 thf(71,plain,(![SV8:mworld]: (((~ (((mrel@'#b_alice')@mactual)@SV8))=$true) | (((bigcity@portland)@SV8)=$true))),inference(extcnf_or_pos,[status(thm)],[62])).
% 1.31/0.53 thf(77,plain,(![SV5:mworld]: (((((mrel@'#b_alice')@mactual)@SV5)=$false) | ((![SY167:mworld]: ((~ (((mrel@'#b_bob')@SV5)@SY167)) | (~ ((bigcity@portland)@SY167))))=$true))),inference(extcnf_not_pos,[status(thm)],[68])).
% 1.31/0.53 thf(80,plain,(![SV8:mworld]: (((((mrel@'#b_alice')@mactual)@SV8)=$false) | (((bigcity@portland)@SV8)=$true))),inference(extcnf_not_pos,[status(thm)],[71])).
% 1.31/0.53 thf(87,plain,(![SV21:mworld,SV5:mworld]: ((((~ (((mrel@'#b_bob')@SV5)@SV21)) | (~ ((bigcity@portland)@SV21)))=$true) | ((((mrel@'#b_alice')@mactual)@SV5)=$false))),inference(extcnf_forall_pos,[status(thm)],[77])).
% 1.31/0.53 thf(95,plain,(![SV21:mworld,SV5:mworld]: (((~ (((mrel@'#b_bob')@SV5)@SV21))=$true) | ((~ ((bigcity@portland)@SV21))=$true) | ((((mrel@'#b_alice')@mactual)@SV5)=$false))),inference(extcnf_or_pos,[status(thm)],[87])).
% 1.31/0.53 thf(102,plain,(![SV21:mworld,SV5:mworld]: (((((mrel@'#b_bob')@SV5)@SV21)=$false) | ((~ ((bigcity@portland)@SV21))=$true) | ((((mrel@'#b_alice')@mactual)@SV5)=$false))),inference(extcnf_not_pos,[status(thm)],[95])).
% 1.31/0.53 thf(109,plain,(![SV5:mworld,SV21:mworld]: ((((bigcity@portland)@SV21)=$false) | ((((mrel@'#b_bob')@SV5)@SV21)=$false) | ((((mrel@'#b_alice')@mactual)@SV5)=$false))),inference(extcnf_not_pos,[status(thm)],[102])).
% 1.31/0.53 thf(184,plain,(![SV36:mworld]: (((((mrel@'#b_alice')@SV36)@SV36)=$true))),inference(rename,[status(thm)],[57])).
% 1.31/0.53 thf(185,plain,(![SV37:mworld]: (((((mrel@'#b_bob')@SV37)@SV37)=$true))),inference(rename,[status(thm)],[58])).
% 1.31/0.53 thf(192,plain,(![SV38:mworld]: (((((mrel@'#b_alice')@mactual)@SV38)=$false) | (((bigcity@portland)@SV38)=$true))),inference(rename,[status(thm)],[80])).
% 1.31/0.53 thf(196,plain,(![SV38:mworld,SV36:mworld]: ((((((mrel@'#b_alice')@mactual)@SV38) = (((mrel@'#b_alice')@SV36)@SV36))=$false) | (((bigcity@portland)@SV38)=$true))),inference(res,[status(thm)],[192,184])).
% 1.31/0.53 thf(207,plain,((((bigcity@portland)@mactual)=$true)),inference(extuni,[status(esa)],[196:[bind(SV38,$thf(mactual)),bind(SV36,$thf(mactual))]])).
% 1.31/0.53 thf(222,plain,(![SV39:mworld,SV40:mworld]: ((((bigcity@portland)@SV40)=$false) | ((((mrel@'#b_bob')@SV39)@SV40)=$false) | ((((mrel@'#b_alice')@mactual)@SV39)=$false))),inference(rename,[status(thm)],[109])).
% 1.31/0.53 thf(229,plain,(![SV39:mworld,SV40:mworld,SV36:mworld]: ((((((mrel@'#b_alice')@mactual)@SV39) = (((mrel@'#b_alice')@SV36)@SV36))=$false) | (((bigcity@portland)@SV40)=$false) | ((((mrel@'#b_bob')@SV39)@SV40)=$false))),inference(res,[status(thm)],[222,184])).
% 1.31/0.53 thf(253,plain,(![SV40:mworld]: (((((mrel@'#b_bob')@mactual)@SV40)=$false) | (((bigcity@portland)@SV40)=$false))),inference(extuni,[status(esa)],[229:[bind(SV39,$thf(mactual)),bind(SV36,$thf(mactual))]])).
% 1.31/0.53 thf(531,plain,(![SV50:mworld]: (((((mrel@'#b_bob')@mactual)@SV50)=$false) | (((bigcity@portland)@SV50)=$false))),inference(rename,[status(thm)],[253])).
% 1.31/0.53 thf(545,plain,(![SV50:mworld,SV37:mworld]: ((((((mrel@'#b_bob')@mactual)@SV50) = (((mrel@'#b_bob')@SV37)@SV37))=$false) | (((bigcity@portland)@SV50)=$false))),inference(res,[status(thm)],[531,185])).
% 1.31/0.53 thf(562,plain,((((bigcity@portland)@mactual)=$false)),inference(extuni,[status(esa)],[545:[bind(SV50,$thf(mactual)),bind(SV37,$thf(mactual))]])).
% 1.31/0.53 thf(572,plain,(((((bigcity@portland)@mactual) = ((bigcity@portland)@mactual))=$false)),inference(res,[status(thm)],[562,207])).
% 1.31/0.53 thf(583,plain,((($false)=$true)),inference(extuni,[status(esa)],[572])).
% 1.31/0.53 thf(584,plain,($false),inference(solved_all_splits,[solved_all_splits(join,[])],[583])).
% 1.31/0.53 % SZS output end CNFRefutation
% 1.31/0.53
% 1.31/0.53 %**** End of derivation protocol ****
% 1.31/0.53 %**** no. of clauses in derivation: 40 ****
% 1.31/0.53 %**** clause counter: 583 ****
% 1.31/0.53
% 1.31/0.53 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:13,ps:3,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:583,loop_count:28,foatp_calls:6,translation:fof_full)
%------------------------------------------------------------------------------