%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : NLP265^18 : 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 : n014.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:44 AM UTC 2026
% Result : Theorem 0.05s 0.24s
% Output : CNFRefutation 0.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP265^18 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.03 % 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.05/0.17 % Computer : n014.cluster.edu
% 0.05/0.17 % Model : x86_64 x86_64
% 0.05/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.17 % Memory : 8046.5625MB
% 0.05/0.17 % OS : Linux 6.8.0-71-generic
% 0.05/0.17 % CPULimit : 300
% 0.05/0.17 % WCLimit : 300
% 0.05/0.17 % DateTime : Tue Oct 6 12:58:41 UTC 2026
% 0.05/0.17 % CPUTime :
% 0.05/0.17 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.05/0.24
% 0.05/0.24 No.of.Axioms: 8
% 0.05/0.24
% 0.05/0.24 Length.of.Defs: 1296
% 0.05/0.24
% 0.05/0.24 Contains.Choice.Funs: false
% 0.05/0.24 .....eprover: <stdin>:1:(Column 88):(just read ''#i_alice''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 0.05/0.24 .eprover: <stdin>:1:(Column 88):(just read ''#i_alice''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 0.05/0.24 .
% 0.05/0.24
% 0.05/0.24 ********************************
% 0.05/0.24 * All subproblems solved! *
% 0.05/0.24 ********************************
% 0.05/0.24 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:9,ps:3,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:true,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:166,loop_count:9,foatp_calls:2,translation:fof_full)
% 0.05/0.24
% 0.05/0.24 %**** Beginning of derivation protocol ****
% 0.05/0.24 % SZS output start CNFRefutation
% 0.05/0.24 thf(tp_mindex,type,(mindex: $tType)).
% 0.05/0.24 thf(tp_mworld,type,(mworld: $tType)).
% 0.05/0.24 thf(tp_'#b_alice',type,('#b_alice': mindex)).
% 0.05/0.24 thf(tp_'#b_bob',type,('#b_bob': mindex)).
% 0.05/0.24 thf(tp_'#i_alice',type,('#i_alice': mindex)).
% 0.05/0.24 thf(tp_'#i_bob',type,('#i_bob': mindex)).
% 0.05/0.24 thf(tp_bigcity,type,(bigcity: ($i>(mworld>$o)))).
% 0.05/0.24 thf(tp_mactual,type,(mactual: mworld)).
% 0.05/0.24 thf(tp_mand,type,(mand: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 0.05/0.24 thf(tp_mbox,type,(mbox: (mindex>((mworld>$o)>(mworld>$o))))).
% 0.05/0.24 thf(tp_mdia,type,(mdia: (mindex>((mworld>$o)>(mworld>$o))))).
% 0.05/0.24 thf(tp_mequiv,type,(mequiv: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 0.05/0.24 thf(tp_mimplies,type,(mimplies: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 0.05/0.24 thf(tp_mlocal,type,(mlocal: ((mworld>$o)>$o))).
% 0.05/0.24 thf(tp_mnot,type,(mnot: ((mworld>$o)>(mworld>$o)))).
% 0.05/0.24 thf(tp_mor,type,(mor: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 0.05/0.24 thf(tp_mrel,type,(mrel: (mindex>(mworld>(mworld>$o))))).
% 0.05/0.24 thf(tp_portland,type,(portland: $i)).
% 0.05/0.24 thf(tp_sK1_SY11,type,(sK1_SY11: mworld)).
% 0.05/0.24 thf(tp_sK2_SY158,type,(sK2_SY158: mworld)).
% 0.05/0.24 thf(tp_sK3_SY80,type,(sK3_SY80: (mworld>mworld))).
% 0.05/0.24 thf(tp_sK4_SY159,type,(sK4_SY159: (mworld>mworld))).
% 0.05/0.24 thf(tp_sK5_SY136,type,(sK5_SY136: (mworld>mworld))).
% 0.05/0.24 thf(tp_sK6_SY160,type,(sK6_SY160: (mworld>mworld))).
% 0.05/0.24 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)).
% 0.05/0.24 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)).
% 0.05/0.24 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)).
% 0.05/0.24 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)).
% 0.05/0.24 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)).
% 0.05/0.24 thf(mlocal,definition,(mlocal = (^[Phi:(mworld>$o)]: (Phi@mactual))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mlocal_def)).
% 0.05/0.24 thf(mnot,definition,(mnot = (^[A:(mworld>$o),W:mworld]: (~ (A@W)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mnot_def)).
% 0.05/0.24 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)).
% 0.05/0.24 thf(2,axiom,(mlocal@((mbox@'#b_alice')@(bigcity@portland))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2)).
% 0.05/0.24 thf(6,axiom,(![W:mworld,V:mworld]: (((mrel@'#b_alice')@W)@V)),file('/export/starexec/sandbox/benchmark/theBenchmark.p','mrel_#b_alice_universal')).
% 0.05/0.24 thf(9,conjecture,(mlocal@((mbox@'#i_alice')@((mbox@'#b_bob')@(bigcity@portland)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 0.05/0.24 thf(10,negated_conjecture,(((mlocal@((mbox@'#i_alice')@((mbox@'#b_bob')@(bigcity@portland))))=$false)),inference(negate_conjecture,[status(cth)],[9])).
% 0.05/0.24 thf(11,plain,(((![SY11:mworld]: ((((mrel@'#i_alice')@mactual)@SY11) => (![SY10:mworld]: ((((mrel@'#b_bob')@SY11)@SY10) => ((bigcity@portland)@SY10)))))=$false)),inference(unfold_def,[status(thm)],[10,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 0.05/0.24 thf(13,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])).
% 0.05/0.24 thf(17,plain,(((![W:mworld,V:mworld]: (((mrel@'#b_alice')@W)@V))=$true)),inference(unfold_def,[status(thm)],[6,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 0.05/0.24 thf(20,plain,((((((mrel@'#i_alice')@mactual)@sK1_SY11) => (![SY158:mworld]: ((((mrel@'#b_bob')@sK1_SY11)@SY158) => ((bigcity@portland)@SY158))))=$false)),inference(extcnf_forall_neg,[status(esa)],[11])).
% 0.05/0.24 thf(22,plain,(((![SY158:mworld]: ((((mrel@'#b_bob')@sK1_SY11)@SY158) => ((bigcity@portland)@SY158)))=$false)),inference(standard_cnf,[status(thm)],[20])).
% 0.05/0.24 thf(23,plain,(((~ (![SY158:mworld]: ((((mrel@'#b_bob')@sK1_SY11)@SY158) => ((bigcity@portland)@SY158))))=$true)),inference(polarity_switch,[status(thm)],[22])).
% 0.05/0.24 thf(24,plain,((((((mrel@'#b_bob')@sK1_SY11)@sK2_SY158) & (~ ((bigcity@portland)@sK2_SY158)))=$true)),inference(extcnf_combined,[status(esa)],[23])).
% 0.05/0.24 thf(26,plain,(((![SY36:mworld]: ((~ (((mrel@'#b_alice')@mactual)@SY36)) | ((bigcity@portland)@SY36)))=$true)),inference(extcnf_combined,[status(esa)],[13])).
% 0.05/0.24 thf(31,plain,(((![W:mworld,V:mworld]: (((mrel@'#b_alice')@W)@V))=$true)),inference(copy,[status(thm)],[17])).
% 0.05/0.24 thf(35,plain,(((![SY36:mworld]: ((~ (((mrel@'#b_alice')@mactual)@SY36)) | ((bigcity@portland)@SY36)))=$true)),inference(copy,[status(thm)],[26])).
% 0.05/0.24 thf(38,plain,((((((mrel@'#b_bob')@sK1_SY11)@sK2_SY158) & (~ ((bigcity@portland)@sK2_SY158)))=$true)),inference(copy,[status(thm)],[24])).
% 0.05/0.24 thf(41,plain,(((~ ((~ (((mrel@'#b_bob')@sK1_SY11)@sK2_SY158)) | (~ (~ ((bigcity@portland)@sK2_SY158)))))=$true)),inference(unfold_def,[status(thm)],[38,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 0.05/0.24 thf(44,plain,(![SV3:mworld]: (((![SY163:mworld]: (((mrel@'#b_alice')@SV3)@SY163))=$true))),inference(extcnf_forall_pos,[status(thm)],[31])).
% 0.05/0.24 thf(46,plain,(![SV5:mworld]: ((((~ (((mrel@'#b_alice')@mactual)@SV5)) | ((bigcity@portland)@SV5))=$true))),inference(extcnf_forall_pos,[status(thm)],[35])).
% 0.05/0.24 thf(50,plain,((((~ (((mrel@'#b_bob')@sK1_SY11)@sK2_SY158)) | (~ (~ ((bigcity@portland)@sK2_SY158))))=$false)),inference(extcnf_not_pos,[status(thm)],[41])).
% 0.05/0.24 thf(53,plain,(![SV11:mworld,SV3:mworld]: (((((mrel@'#b_alice')@SV3)@SV11)=$true))),inference(extcnf_forall_pos,[status(thm)],[44])).
% 0.05/0.24 thf(55,plain,(![SV5:mworld]: (((~ (((mrel@'#b_alice')@mactual)@SV5))=$true) | (((bigcity@portland)@SV5)=$true))),inference(extcnf_or_pos,[status(thm)],[46])).
% 0.05/0.24 thf(60,plain,(((~ (~ ((bigcity@portland)@sK2_SY158)))=$false)),inference(extcnf_or_neg,[status(thm)],[50])).
% 0.05/0.24 thf(61,plain,(![SV5:mworld]: (((((mrel@'#b_alice')@mactual)@SV5)=$false) | (((bigcity@portland)@SV5)=$true))),inference(extcnf_not_pos,[status(thm)],[55])).
% 0.05/0.24 thf(66,plain,(((~ ((bigcity@portland)@sK2_SY158))=$true)),inference(extcnf_not_neg,[status(thm)],[60])).
% 0.05/0.24 thf(70,plain,((((bigcity@portland)@sK2_SY158)=$false)),inference(extcnf_not_pos,[status(thm)],[66])).
% 0.05/0.24 thf(140,plain,(![SV30:mworld,SV31:mworld]: (((((mrel@'#b_alice')@SV31)@SV30)=$true))),inference(rename,[status(thm)],[53])).
% 0.05/0.24 thf(146,plain,(![SV34:mworld]: (((((mrel@'#b_alice')@mactual)@SV34)=$false) | (((bigcity@portland)@SV34)=$true))),inference(rename,[status(thm)],[61])).
% 0.05/0.24 thf(153,plain,(![SV34:mworld]: (((((bigcity@portland)@SV34) = ((bigcity@portland)@sK2_SY158))=$false) | ((((mrel@'#b_alice')@mactual)@SV34)=$false))),inference(res,[status(thm)],[146,70])).
% 0.05/0.24 thf(154,plain,(((((mrel@'#b_alice')@mactual)@sK2_SY158)=$false)),inference(extuni,[status(esa)],[153:[bind(SV34,$thf(sK2_SY158))]])).
% 0.05/0.24 thf(161,plain,(![SV30:mworld,SV31:mworld]: ((((((mrel@'#b_alice')@mactual)@sK2_SY158) = (((mrel@'#b_alice')@SV31)@SV30))=$false))),inference(res,[status(thm)],[154,140])).
% 0.05/0.24 thf(166,plain,((($false)=$true)),inference(extuni,[status(esa)],[161:[bind(SV30,$thf(sK2_SY158)),bind(SV31,$thf(mactual))]])).
% 0.05/0.24 thf(167,plain,($false),inference(solved_all_splits,[solved_all_splits(join,[])],[166])).
% 0.05/0.24 % SZS output end CNFRefutation
% 0.05/0.24
% 0.05/0.24 %**** End of derivation protocol ****
% 0.05/0.24 %**** no. of clauses in derivation: 32 ****
% 0.05/0.24 %**** clause counter: 166 ****
% 0.05/0.24
% 0.05/0.24 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:9,ps:3,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:true,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:166,loop_count:9,foatp_calls:2,translation:fof_full)
%------------------------------------------------------------------------------