%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : NLP267^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 : n015.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 69.12s 11.88s
% Output : CNFRefutation 69.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP267^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 : n015.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:02:28 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 69.12/11.88
% 69.12/11.88 No.of.Axioms: 11
% 69.12/11.88
% 69.12/11.88 Length.of.Defs: 1296
% 69.12/11.88
% 69.12/11.88 Contains.Choice.Funs: false
% 69.12/11.88 ....eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ...eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ..eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ..eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ..eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ....eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ..eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ..eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ..eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ..eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ..eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ....eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ...eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ...eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ......eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .....eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ...eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ...eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ...eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ......eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ...eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ......eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .....eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ...eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .....eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ....eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ...eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ....eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .....eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ...eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ...eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ....eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .....eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .....eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ....eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ........eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 ........eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 69.12/11.88 .......
% 69.12/11.88
% 69.12/11.88 ********************************
% 69.12/11.88 * All subproblems solved! *
% 69.12/11.88 ********************************
% 69.12/11.88 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:12,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:7743,loop_count:264,foatp_calls:53,translation:fof_full)
% 69.12/11.88
% 69.12/11.88 %**** Beginning of derivation protocol ****
% 69.12/11.88 % SZS output start CNFRefutation
% 69.12/11.88 thf(tp_mindex,type,(mindex: $tType)).
% 69.12/11.88 thf(tp_mworld,type,(mworld: $tType)).
% 69.12/11.88 thf(tp_'#b_s',type,('#b_s': mindex)).
% 69.12/11.88 thf(tp_'#b_u',type,('#b_u': mindex)).
% 69.12/11.88 thf(tp_class,type,(class: ($i>(mworld>$o)))).
% 69.12/11.88 thf(tp_dest,type,(dest: ($i>(mworld>$o)))).
% 69.12/11.88 thf(tp_first,type,(first: $i)).
% 69.12/11.88 thf(tp_mactual,type,(mactual: mworld)).
% 69.12/11.88 thf(tp_mand,type,(mand: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 69.12/11.88 thf(tp_mbox,type,(mbox: (mindex>((mworld>$o)>(mworld>$o))))).
% 69.12/11.88 thf(tp_mdia,type,(mdia: (mindex>((mworld>$o)>(mworld>$o))))).
% 69.12/11.88 thf(tp_mequiv,type,(mequiv: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 69.12/11.88 thf(tp_mimplies,type,(mimplies: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 69.12/11.88 thf(tp_mlocal,type,(mlocal: ((mworld>$o)>$o))).
% 69.12/11.88 thf(tp_mnot,type,(mnot: ((mworld>$o)>(mworld>$o)))).
% 69.12/11.88 thf(tp_mor,type,(mor: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 69.12/11.88 thf(tp_mrel,type,(mrel: (mindex>(mworld>(mworld>$o))))).
% 69.12/11.88 thf(tp_ninetyfive,type,(ninetyfive: $i)).
% 69.12/11.88 thf(tp_paris,type,(paris: $i)).
% 69.12/11.88 thf(tp_price,type,(price: ($i>(mworld>$o)))).
% 69.12/11.88 thf(tp_sK1_SY5,type,(sK1_SY5: mworld)).
% 69.12/11.88 thf(tp_second,type,(second: $i)).
% 69.12/11.88 thf(tp_seventy,type,(seventy: $i)).
% 69.12/11.88 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)).
% 69.12/11.88 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)).
% 69.12/11.88 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)).
% 69.12/11.88 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)).
% 69.12/11.88 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)).
% 69.12/11.88 thf(mlocal,definition,(mlocal = (^[Phi:(mworld>$o)]: (Phi@mactual))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mlocal_def)).
% 69.12/11.88 thf(mnot,definition,(mnot = (^[A:(mworld>$o),W:mworld]: (~ (A@W)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mnot_def)).
% 69.12/11.88 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)).
% 69.12/11.88 thf(1,axiom,(mlocal@((mbox@'#b_s')@((mand@(dest@paris))@(class@second)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_5)).
% 69.12/11.88 thf(6,axiom,(mlocal@((mbox@'#b_s')@((mimplies@((mand@(dest@paris))@(class@second)))@(price@seventy)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2)).
% 69.12/11.88 thf(12,conjecture,(mlocal@((mbox@'#b_s')@(price@seventy))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 69.12/11.88 thf(13,negated_conjecture,(((mlocal@((mbox@'#b_s')@(price@seventy)))=$false)),inference(negate_conjecture,[status(cth)],[12])).
% 69.12/11.88 thf(14,plain,(((![SY5:mworld]: ((((mrel@'#b_s')@mactual)@SY5) => ((price@seventy)@SY5)))=$false)),inference(unfold_def,[status(thm)],[13,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 69.12/11.88 thf(15,plain,(((![SY15:mworld]: ((((mrel@'#b_s')@mactual)@SY15) => (((dest@paris)@SY15) & ((class@second)@SY15))))=$true)),inference(unfold_def,[status(thm)],[1,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 69.12/11.88 thf(20,plain,(((![SY72:mworld]: ((((mrel@'#b_s')@mactual)@SY72) => ((((dest@paris)@SY72) & ((class@second)@SY72)) => ((price@seventy)@SY72))))=$true)),inference(unfold_def,[status(thm)],[6,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 69.12/11.88 thf(26,plain,((((((mrel@'#b_s')@mactual)@sK1_SY5) => ((price@seventy)@sK1_SY5))=$false)),inference(extcnf_forall_neg,[status(esa)],[14])).
% 69.12/11.88 thf(27,plain,(((((mrel@'#b_s')@mactual)@sK1_SY5)=$true)),inference(standard_cnf,[status(thm)],[26])).
% 69.12/11.88 thf(28,plain,((((price@seventy)@sK1_SY5)=$false)),inference(standard_cnf,[status(thm)],[26])).
% 69.12/11.88 thf(29,plain,(((~ ((price@seventy)@sK1_SY5))=$true)),inference(polarity_switch,[status(thm)],[28])).
% 69.12/11.88 thf(35,plain,(((![SY72:mworld]: ((((mrel@'#b_s')@mactual)@SY72) => ((((dest@paris)@SY72) & ((class@second)@SY72)) => ((price@seventy)@SY72))))=$true)),inference(copy,[status(thm)],[20])).
% 69.12/11.88 thf(40,plain,(((![SY15:mworld]: ((((mrel@'#b_s')@mactual)@SY15) => (((dest@paris)@SY15) & ((class@second)@SY15))))=$true)),inference(copy,[status(thm)],[15])).
% 69.12/11.88 thf(41,plain,(((((mrel@'#b_s')@mactual)@sK1_SY5)=$true)),inference(copy,[status(thm)],[27])).
% 69.12/11.88 thf(42,plain,(((~ ((price@seventy)@sK1_SY5))=$true)),inference(copy,[status(thm)],[29])).
% 69.12/11.88 thf(43,plain,(((![SX0:mworld]: ((~ (((mrel@'#b_s')@mactual)@SX0)) | ((~ (~ ((~ ((dest@paris)@SX0)) | (~ ((class@second)@SX0))))) | ((price@seventy)@SX0))))=$true)),inference(unfold_def,[status(thm)],[35,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 69.12/11.88 thf(51,plain,(((![SX0:mworld]: ((~ (((mrel@'#b_s')@mactual)@SX0)) | (~ ((~ ((dest@paris)@SX0)) | (~ ((class@second)@SX0))))))=$true)),inference(unfold_def,[status(thm)],[40,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 69.12/11.88 thf(54,plain,((((price@seventy)@sK1_SY5)=$false)),inference(extcnf_not_pos,[status(thm)],[42])).
% 69.12/11.88 thf(55,plain,(![SV3:mworld]: ((((~ (((mrel@'#b_s')@mactual)@SV3)) | ((~ (~ ((~ ((dest@paris)@SV3)) | (~ ((class@second)@SV3))))) | ((price@seventy)@SV3)))=$true))),inference(extcnf_forall_pos,[status(thm)],[43])).
% 69.12/11.88 thf(63,plain,(![SV11:mworld]: ((((~ (((mrel@'#b_s')@mactual)@SV11)) | (~ ((~ ((dest@paris)@SV11)) | (~ ((class@second)@SV11)))))=$true))),inference(extcnf_forall_pos,[status(thm)],[51])).
% 69.12/11.88 thf(64,plain,(![SV3:mworld]: (((~ (((mrel@'#b_s')@mactual)@SV3))=$true) | (((~ (~ ((~ ((dest@paris)@SV3)) | (~ ((class@second)@SV3))))) | ((price@seventy)@SV3))=$true))),inference(extcnf_or_pos,[status(thm)],[55])).
% 69.12/11.88 thf(72,plain,(![SV11:mworld]: (((~ (((mrel@'#b_s')@mactual)@SV11))=$true) | ((~ ((~ ((dest@paris)@SV11)) | (~ ((class@second)@SV11))))=$true))),inference(extcnf_or_pos,[status(thm)],[63])).
% 69.12/11.88 thf(73,plain,(![SV3:mworld]: (((((mrel@'#b_s')@mactual)@SV3)=$false) | (((~ (~ ((~ ((dest@paris)@SV3)) | (~ ((class@second)@SV3))))) | ((price@seventy)@SV3))=$true))),inference(extcnf_not_pos,[status(thm)],[64])).
% 69.12/11.88 thf(81,plain,(![SV11:mworld]: (((((mrel@'#b_s')@mactual)@SV11)=$false) | ((~ ((~ ((dest@paris)@SV11)) | (~ ((class@second)@SV11))))=$true))),inference(extcnf_not_pos,[status(thm)],[72])).
% 69.12/11.88 thf(82,plain,(![SV3:mworld]: (((~ (~ ((~ ((dest@paris)@SV3)) | (~ ((class@second)@SV3)))))=$true) | (((price@seventy)@SV3)=$true) | ((((mrel@'#b_s')@mactual)@SV3)=$false))),inference(extcnf_or_pos,[status(thm)],[73])).
% 69.12/11.88 thf(90,plain,(![SV11:mworld]: ((((~ ((dest@paris)@SV11)) | (~ ((class@second)@SV11)))=$false) | ((((mrel@'#b_s')@mactual)@SV11)=$false))),inference(extcnf_not_pos,[status(thm)],[81])).
% 69.12/11.88 thf(91,plain,(![SV3:mworld]: (((~ ((~ ((dest@paris)@SV3)) | (~ ((class@second)@SV3))))=$false) | (((price@seventy)@SV3)=$true) | ((((mrel@'#b_s')@mactual)@SV3)=$false))),inference(extcnf_not_pos,[status(thm)],[82])).
% 69.12/11.88 thf(99,plain,(![SV11:mworld]: (((~ ((dest@paris)@SV11))=$false) | ((((mrel@'#b_s')@mactual)@SV11)=$false))),inference(extcnf_or_neg,[status(thm)],[90])).
% 69.12/11.88 thf(100,plain,(![SV11:mworld]: (((~ ((class@second)@SV11))=$false) | ((((mrel@'#b_s')@mactual)@SV11)=$false))),inference(extcnf_or_neg,[status(thm)],[90])).
% 69.12/11.88 thf(101,plain,(![SV3:mworld]: ((((~ ((dest@paris)@SV3)) | (~ ((class@second)@SV3)))=$true) | (((price@seventy)@SV3)=$true) | ((((mrel@'#b_s')@mactual)@SV3)=$false))),inference(extcnf_not_neg,[status(thm)],[91])).
% 69.12/11.88 thf(109,plain,(![SV11:mworld]: ((((dest@paris)@SV11)=$true) | ((((mrel@'#b_s')@mactual)@SV11)=$false))),inference(extcnf_not_neg,[status(thm)],[99])).
% 69.12/11.88 thf(110,plain,(![SV11:mworld]: ((((class@second)@SV11)=$true) | ((((mrel@'#b_s')@mactual)@SV11)=$false))),inference(extcnf_not_neg,[status(thm)],[100])).
% 69.12/11.88 thf(111,plain,(![SV3:mworld]: (((~ ((dest@paris)@SV3))=$true) | ((~ ((class@second)@SV3))=$true) | (((price@seventy)@SV3)=$true) | ((((mrel@'#b_s')@mactual)@SV3)=$false))),inference(extcnf_or_pos,[status(thm)],[101])).
% 69.12/11.88 thf(119,plain,(![SV3:mworld]: ((((dest@paris)@SV3)=$false) | ((~ ((class@second)@SV3))=$true) | (((price@seventy)@SV3)=$true) | ((((mrel@'#b_s')@mactual)@SV3)=$false))),inference(extcnf_not_pos,[status(thm)],[111])).
% 69.12/11.88 thf(127,plain,(![SV3:mworld]: ((((class@second)@SV3)=$false) | (((dest@paris)@SV3)=$false) | (((price@seventy)@SV3)=$true) | ((((mrel@'#b_s')@mactual)@SV3)=$false))),inference(extcnf_not_pos,[status(thm)],[119])).
% 69.12/11.88 thf(136,plain,(![SV18:mworld]: ((((dest@paris)@SV18)=$true) | ((((mrel@'#b_s')@mactual)@SV18)=$false))),inference(rename,[status(thm)],[109])).
% 69.12/11.88 thf(142,plain,(![SV18:mworld]: ((((((mrel@'#b_s')@mactual)@SV18) = (((mrel@'#b_s')@mactual)@sK1_SY5))=$false) | (((dest@paris)@SV18)=$true))),inference(res,[status(thm)],[136,41])).
% 69.12/11.88 thf(143,plain,((((dest@paris)@sK1_SY5)=$true)),inference(extuni,[status(esa)],[142:[bind(SV18,$thf(sK1_SY5))]])).
% 69.12/11.88 thf(150,plain,(![SV19:mworld]: ((((class@second)@SV19)=$true) | ((((mrel@'#b_s')@mactual)@SV19)=$false))),inference(rename,[status(thm)],[110])).
% 69.12/11.88 thf(160,plain,(![SV19:mworld]: ((((((mrel@'#b_s')@mactual)@SV19) = (((mrel@'#b_s')@mactual)@sK1_SY5))=$false) | (((class@second)@SV19)=$true))),inference(res,[status(thm)],[150,41])).
% 69.12/11.88 thf(161,plain,((((class@second)@sK1_SY5)=$true)),inference(extuni,[status(esa)],[160:[bind(SV19,$thf(sK1_SY5))]])).
% 69.12/11.88 thf(459,plain,(![SV25:mworld]: ((((class@second)@SV25)=$false) | (((dest@paris)@SV25)=$false) | (((price@seventy)@SV25)=$true) | ((((mrel@'#b_s')@mactual)@SV25)=$false))),inference(rename,[status(thm)],[127])).
% 69.12/11.88 thf(511,plain,(![SV25:mworld]: ((((((mrel@'#b_s')@mactual)@SV25) = (((mrel@'#b_s')@mactual)@sK1_SY5))=$false) | (((class@second)@SV25)=$false) | (((dest@paris)@SV25)=$false) | (((price@seventy)@SV25)=$true))),inference(res,[status(thm)],[459,41])).
% 69.12/11.88 thf(514,plain,((((price@seventy)@sK1_SY5)=$true) | (((dest@paris)@sK1_SY5)=$false) | (((class@second)@sK1_SY5)=$false)),inference(extuni,[status(esa)],[511:[bind(SV25,$thf(sK1_SY5))]])).
% 69.12/11.88 thf(1984,plain,(((((price@seventy)@sK1_SY5) = ((price@seventy)@sK1_SY5))=$false) | (((dest@paris)@sK1_SY5)=$false) | (((class@second)@sK1_SY5)=$false)),inference(res,[status(thm)],[514,54])).
% 69.12/11.88 thf(1987,plain,((((class@second)@sK1_SY5)=$false) | (((dest@paris)@sK1_SY5)=$false)),inference(extuni,[status(esa)],[1984])).
% 69.12/11.88 thf(7680,plain,(((((dest@paris)@sK1_SY5) = ((dest@paris)@sK1_SY5))=$false) | (((class@second)@sK1_SY5)=$false)),inference(res,[status(thm)],[1987,143])).
% 69.12/11.88 thf(7692,plain,((((class@second)@sK1_SY5)=$false)),inference(extuni,[status(esa)],[7680])).
% 69.12/11.88 thf(7734,plain,(((((class@second)@sK1_SY5) = ((class@second)@sK1_SY5))=$false)),inference(res,[status(thm)],[7692,161])).
% 69.12/11.88 thf(7743,plain,((($false)=$true)),inference(extuni,[status(esa)],[7734])).
% 69.12/11.88 thf(7744,plain,($false),inference(solved_all_splits,[solved_all_splits(join,[])],[7743])).
% 69.12/11.88 % SZS output end CNFRefutation
% 69.12/11.88
% 69.12/11.88 %**** End of derivation protocol ****
% 69.12/11.88 %**** no. of clauses in derivation: 51 ****
% 69.12/11.88 %**** clause counter: 7743 ****
% 69.12/11.88
% 69.12/11.88 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:12,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:7743,loop_count:264,foatp_calls:53,translation:fof_full)
%------------------------------------------------------------------------------