%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : NLP267^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/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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.52s 0.27s
% Output : CNFRefutation 0.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP267^18 : 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/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.17 % Computer : n010.cluster.edu
% 0.07/0.17 % Model : x86_64 x86_64
% 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.17 % Memory : 8046.5625MB
% 0.07/0.17 % OS : Linux 6.8.0-71-generic
% 0.07/0.17 % CPULimit : 300
% 0.07/0.17 % WCLimit : 300
% 0.07/0.17 % DateTime : Tue Oct 6 13:00:30 UTC 2026
% 0.07/0.17 % CPUTime :
% 0.07/0.17 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.52/0.27
% 0.52/0.27 No.of.Axioms: 9
% 0.52/0.27
% 0.52/0.27 Length.of.Defs: 1304
% 0.52/0.27
% 0.52/0.27 Contains.Choice.Funs: false
% 0.52/0.27 ...eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 0.52/0.27 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 0.52/0.27 eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 0.52/0.27 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 0.52/0.27 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 0.52/0.27 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 0.52/0.27 .eprover: <stdin>:1:(Column 88):(just read ''#b_s''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 0.52/0.27 .
% 0.52/0.27
% 0.52/0.27 ********************************
% 0.52/0.27 * All subproblems solved! *
% 0.52/0.27 ********************************
% 0.52/0.27 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:0,axioms:10,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:312,loop_count:34,foatp_calls:7,translation:fof_full)
% 0.52/0.27
% 0.52/0.27 %**** Beginning of derivation protocol ****
% 0.52/0.27 % SZS output start CNFRefutation
% 0.52/0.27 thf(tp_mindex,type,(mindex: $tType)).
% 0.52/0.27 thf(tp_mworld,type,(mworld: $tType)).
% 0.52/0.27 thf(tp_'#b_s',type,('#b_s': mindex)).
% 0.52/0.27 thf(tp_'#b_u',type,('#b_u': mindex)).
% 0.52/0.27 thf(tp_class,type,(class: ($i>(mworld>$o)))).
% 0.52/0.27 thf(tp_dest,type,(dest: ($i>(mworld>$o)))).
% 0.52/0.27 thf(tp_first,type,(first: $i)).
% 0.52/0.27 thf(tp_mactual,type,(mactual: mworld)).
% 0.52/0.27 thf(tp_mand,type,(mand: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 0.52/0.27 thf(tp_mbox,type,(mbox: (mindex>((mworld>$o)>(mworld>$o))))).
% 0.52/0.27 thf(tp_mdia,type,(mdia: (mindex>((mworld>$o)>(mworld>$o))))).
% 0.52/0.27 thf(tp_mequiv,type,(mequiv: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 0.52/0.27 thf(tp_mimplies,type,(mimplies: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 0.52/0.27 thf(tp_mlocal,type,(mlocal: ((mworld>$o)>$o))).
% 0.52/0.27 thf(tp_mnot,type,(mnot: ((mworld>$o)>(mworld>$o)))).
% 0.52/0.27 thf(tp_mor,type,(mor: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 0.52/0.27 thf(tp_mrel,type,(mrel: (mindex>(mworld>(mworld>$o))))).
% 0.52/0.27 thf(tp_ninetyfive,type,(ninetyfive: $i)).
% 0.52/0.27 thf(tp_paris,type,(paris: $i)).
% 0.52/0.27 thf(tp_price,type,(price: ($i>(mworld>$o)))).
% 0.52/0.27 thf(tp_sK1_SY5,type,(sK1_SY5: mworld)).
% 0.52/0.27 thf(tp_second,type,(second: $i)).
% 0.52/0.27 thf(tp_seventy,type,(seventy: $i)).
% 0.52/0.27 thf(mand,definition,(mand = (^[A:(mworld>$o),B:(mworld>$o),W:mworld]: ((A@W) & (B@W)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mand_def)).
% 0.52/0.27 thf(mbox,definition,(mbox = (^[R:mindex,Phi:(mworld>$o),W:mworld]: (![V:mworld]: ((((mrel@R)@W)@V) => (Phi@V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mbox_def)).
% 0.52/0.27 thf(mdia,definition,(mdia = (^[R:mindex,Phi:(mworld>$o),W:mworld]: (?[V:mworld]: ((((mrel@R)@W)@V) & (Phi@V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mdia_def)).
% 0.52/0.27 thf(mequiv,definition,(mequiv = (^[A:(mworld>$o),B:(mworld>$o),W:mworld]: ((A@W) <=> (B@W)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mequiv_def)).
% 0.52/0.27 thf(mimplies,definition,(mimplies = (^[A:(mworld>$o),B:(mworld>$o),W:mworld]: ((A@W) => (B@W)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mimplies_def)).
% 0.52/0.27 thf(mlocal,definition,(mlocal = (^[Phi:(mworld>$o)]: (Phi@mactual))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mlocal_def)).
% 0.52/0.27 thf(mnot,definition,(mnot = (^[A:(mworld>$o),W:mworld]: (~ (A@W)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mnot_def)).
% 0.52/0.27 thf(mor,definition,(mor = (^[A:(mworld>$o),B:(mworld>$o),W:mworld]: ((A@W) | (B@W)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mor_def)).
% 0.52/0.27 thf(1,axiom,(mlocal@((mbox@'#b_s')@((mand@(dest@paris))@(class@second)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5)).
% 0.52/0.27 thf(6,axiom,(mlocal@((mbox@'#b_s')@((mimplies@((mand@(dest@paris))@(class@second)))@(price@seventy)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2)).
% 0.52/0.27 thf(8,axiom,(![W:mworld,V:mworld]: (((mrel@'#b_s')@W)@V)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mrel_#b_s_universal')).
% 0.52/0.27 thf(10,conjecture,(mlocal@((mbox@'#b_s')@(price@seventy))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',con)).
% 0.52/0.27 thf(11,negated_conjecture,(((mlocal@((mbox@'#b_s')@(price@seventy)))=$false)),inference(negate_conjecture,[status(cth)],[10])).
% 0.52/0.27 thf(12,plain,(((![SY5:mworld]: ((((mrel@'#b_s')@mactual)@SY5) => ((price@seventy)@SY5)))=$false)),inference(unfold_def,[status(thm)],[11,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 0.52/0.27 thf(13,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])).
% 0.52/0.27 thf(18,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])).
% 0.52/0.27 thf(20,plain,(((![W:mworld,V:mworld]: (((mrel@'#b_s')@W)@V))=$true)),inference(unfold_def,[status(thm)],[8,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 0.52/0.27 thf(22,plain,((((((mrel@'#b_s')@mactual)@sK1_SY5) => ((price@seventy)@sK1_SY5))=$false)),inference(extcnf_forall_neg,[status(esa)],[12])).
% 0.52/0.27 thf(24,plain,((((price@seventy)@sK1_SY5)=$false)),inference(standard_cnf,[status(thm)],[22])).
% 0.52/0.27 thf(25,plain,(((~ ((price@seventy)@sK1_SY5))=$true)),inference(polarity_switch,[status(thm)],[24])).
% 0.52/0.27 thf(27,plain,(((![W:mworld,V:mworld]: (((mrel@'#b_s')@W)@V))=$true)),inference(copy,[status(thm)],[20])).
% 0.52/0.27 thf(29,plain,(((![SY72:mworld]: ((((mrel@'#b_s')@mactual)@SY72) => ((((dest@paris)@SY72) & ((class@second)@SY72)) => ((price@seventy)@SY72))))=$true)),inference(copy,[status(thm)],[18])).
% 0.52/0.27 thf(34,plain,(((![SY15:mworld]: ((((mrel@'#b_s')@mactual)@SY15) => (((dest@paris)@SY15) & ((class@second)@SY15))))=$true)),inference(copy,[status(thm)],[13])).
% 0.52/0.27 thf(36,plain,(((~ ((price@seventy)@sK1_SY5))=$true)),inference(copy,[status(thm)],[25])).
% 0.52/0.27 thf(37,plain,(((![SX0:mworld]: ((~ (((mrel@'#b_s')@mactual)@SX0)) | ((~ (~ ((~ ((dest@paris)@SX0)) | (~ ((class@second)@SX0))))) | ((price@seventy)@SX0))))=$true)),inference(unfold_def,[status(thm)],[29,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 0.52/0.27 thf(40,plain,(((![SX0:mworld]: ((~ (((mrel@'#b_s')@mactual)@SX0)) | (~ ((~ ((dest@paris)@SX0)) | (~ ((class@second)@SX0))))))=$true)),inference(unfold_def,[status(thm)],[34,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 0.52/0.27 thf(45,plain,(![SV2:mworld]: (((![SY92:mworld]: (((mrel@'#b_s')@SV2)@SY92))=$true))),inference(extcnf_forall_pos,[status(thm)],[27])).
% 0.52/0.27 thf(46,plain,((((price@seventy)@sK1_SY5)=$false)),inference(extcnf_not_pos,[status(thm)],[36])).
% 0.52/0.27 thf(47,plain,(![SV3:mworld]: ((((~ (((mrel@'#b_s')@mactual)@SV3)) | ((~ (~ ((~ ((dest@paris)@SV3)) | (~ ((class@second)@SV3))))) | ((price@seventy)@SV3)))=$true))),inference(extcnf_forall_pos,[status(thm)],[37])).
% 0.52/0.27 thf(50,plain,(![SV6:mworld]: ((((~ (((mrel@'#b_s')@mactual)@SV6)) | (~ ((~ ((dest@paris)@SV6)) | (~ ((class@second)@SV6)))))=$true))),inference(extcnf_forall_pos,[status(thm)],[40])).
% 0.52/0.27 thf(55,plain,(![SV11:mworld,SV2:mworld]: (((((mrel@'#b_s')@SV2)@SV11)=$true))),inference(extcnf_forall_pos,[status(thm)],[45])).
% 0.52/0.27 thf(56,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)],[47])).
% 0.52/0.27 thf(59,plain,(![SV6:mworld]: (((~ (((mrel@'#b_s')@mactual)@SV6))=$true) | ((~ ((~ ((dest@paris)@SV6)) | (~ ((class@second)@SV6))))=$true))),inference(extcnf_or_pos,[status(thm)],[50])).
% 0.52/0.27 thf(63,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)],[56])).
% 0.52/0.27 thf(66,plain,(![SV6:mworld]: (((((mrel@'#b_s')@mactual)@SV6)=$false) | ((~ ((~ ((dest@paris)@SV6)) | (~ ((class@second)@SV6))))=$true))),inference(extcnf_not_pos,[status(thm)],[59])).
% 0.52/0.27 thf(70,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)],[63])).
% 0.52/0.27 thf(73,plain,(![SV6:mworld]: ((((~ ((dest@paris)@SV6)) | (~ ((class@second)@SV6)))=$false) | ((((mrel@'#b_s')@mactual)@SV6)=$false))),inference(extcnf_not_pos,[status(thm)],[66])).
% 0.52/0.27 thf(77,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)],[70])).
% 0.52/0.27 thf(80,plain,(![SV6:mworld]: (((~ ((dest@paris)@SV6))=$false) | ((((mrel@'#b_s')@mactual)@SV6)=$false))),inference(extcnf_or_neg,[status(thm)],[73])).
% 0.52/0.27 thf(81,plain,(![SV6:mworld]: (((~ ((class@second)@SV6))=$false) | ((((mrel@'#b_s')@mactual)@SV6)=$false))),inference(extcnf_or_neg,[status(thm)],[73])).
% 0.52/0.27 thf(85,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)],[77])).
% 0.52/0.27 thf(88,plain,(![SV6:mworld]: ((((dest@paris)@SV6)=$true) | ((((mrel@'#b_s')@mactual)@SV6)=$false))),inference(extcnf_not_neg,[status(thm)],[80])).
% 0.52/0.27 thf(89,plain,(![SV6:mworld]: ((((class@second)@SV6)=$true) | ((((mrel@'#b_s')@mactual)@SV6)=$false))),inference(extcnf_not_neg,[status(thm)],[81])).
% 0.52/0.27 thf(93,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)],[85])).
% 0.52/0.27 thf(99,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)],[93])).
% 0.52/0.27 thf(105,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)],[99])).
% 0.52/0.27 thf(110,plain,(![SV14:mworld,SV15:mworld]: (((((mrel@'#b_s')@SV15)@SV14)=$true))),inference(rename,[status(thm)],[55])).
% 0.52/0.27 thf(112,plain,(![SV16:mworld]: ((((dest@paris)@SV16)=$true) | ((((mrel@'#b_s')@mactual)@SV16)=$false))),inference(rename,[status(thm)],[88])).
% 0.52/0.27 thf(115,plain,(![SV16:mworld,SV14:mworld,SV15:mworld]: ((((((mrel@'#b_s')@mactual)@SV16) = (((mrel@'#b_s')@SV15)@SV14))=$false) | (((dest@paris)@SV16)=$true))),inference(res,[status(thm)],[112,110])).
% 0.52/0.27 thf(119,plain,(![SV14:mworld]: ((((dest@paris)@SV14)=$true))),inference(extuni,[status(esa)],[115:[bind(SV16,$thf(SV14)),bind(SV15,$thf(mactual))]])).
% 0.52/0.27 thf(120,plain,(![SV17:mworld]: ((((dest@paris)@SV17)=$true))),inference(rename,[status(thm)],[119])).
% 0.52/0.27 thf(122,plain,(![SV18:mworld]: ((((class@second)@SV18)=$true) | ((((mrel@'#b_s')@mactual)@SV18)=$false))),inference(rename,[status(thm)],[89])).
% 0.52/0.27 thf(126,plain,(![SV18:mworld,SV14:mworld,SV15:mworld]: ((((((mrel@'#b_s')@mactual)@SV18) = (((mrel@'#b_s')@SV15)@SV14))=$false) | (((class@second)@SV18)=$true))),inference(res,[status(thm)],[122,110])).
% 0.52/0.27 thf(130,plain,(![SV14:mworld]: ((((class@second)@SV14)=$true))),inference(extuni,[status(esa)],[126:[bind(SV18,$thf(SV14)),bind(SV15,$thf(mactual))]])).
% 0.52/0.27 thf(131,plain,(![SV19:mworld]: ((((class@second)@SV19)=$true))),inference(rename,[status(thm)],[130])).
% 0.52/0.27 thf(234,plain,(![SV35:mworld]: ((((class@second)@SV35)=$false) | (((dest@paris)@SV35)=$false) | (((price@seventy)@SV35)=$true) | ((((mrel@'#b_s')@mactual)@SV35)=$false))),inference(rename,[status(thm)],[105])).
% 0.52/0.27 thf(259,plain,(![SV35:mworld]: (((((price@seventy)@SV35) = ((price@seventy)@sK1_SY5))=$false) | (((class@second)@SV35)=$false) | (((dest@paris)@SV35)=$false) | ((((mrel@'#b_s')@mactual)@SV35)=$false))),inference(res,[status(thm)],[234,46])).
% 0.52/0.27 thf(260,plain,(((((mrel@'#b_s')@mactual)@sK1_SY5)=$false) | (((dest@paris)@sK1_SY5)=$false) | (((class@second)@sK1_SY5)=$false)),inference(extuni,[status(esa)],[259:[bind(SV35,$thf(sK1_SY5))]])).
% 0.52/0.27 thf(286,plain,(![SV14:mworld,SV15:mworld]: ((((((mrel@'#b_s')@mactual)@sK1_SY5) = (((mrel@'#b_s')@SV15)@SV14))=$false) | (((dest@paris)@sK1_SY5)=$false) | (((class@second)@sK1_SY5)=$false))),inference(res,[status(thm)],[260,110])).
% 0.52/0.27 thf(291,plain,((((class@second)@sK1_SY5)=$false) | (((dest@paris)@sK1_SY5)=$false)),inference(extuni,[status(esa)],[286:[bind(SV14,$thf(sK1_SY5)),bind(SV15,$thf(mactual))]])).
% 0.52/0.27 thf(298,plain,(![SV17:mworld]: (((((dest@paris)@sK1_SY5) = ((dest@paris)@SV17))=$false) | (((class@second)@sK1_SY5)=$false))),inference(res,[status(thm)],[291,120])).
% 0.52/0.27 thf(305,plain,((((class@second)@sK1_SY5)=$false)),inference(extuni,[status(esa)],[298:[bind(SV17,$thf(sK1_SY5))]])).
% 0.52/0.27 thf(308,plain,(![SV19:mworld]: (((((class@second)@sK1_SY5) = ((class@second)@SV19))=$false))),inference(res,[status(thm)],[305,131])).
% 0.52/0.27 thf(312,plain,((($false)=$true)),inference(extuni,[status(esa)],[308:[bind(SV19,$thf(sK1_SY5))]])).
% 0.52/0.27 thf(313,plain,($false),inference(solved_all_splits,[solved_all_splits(join,[])],[312])).
% 0.52/0.27 % SZS output end CNFRefutation
% 0.52/0.27
% 0.52/0.27 %**** End of derivation protocol ****
% 0.52/0.27 %**** no. of clauses in derivation: 57 ****
% 0.52/0.27 %**** clause counter: 312 ****
% 0.52/0.27
% 0.52/0.27 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:0,axioms:10,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:312,loop_count:34,foatp_calls:7,translation:fof_full)
%------------------------------------------------------------------------------