%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : PUZ149^13 : 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 : n018.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:37:02 AM UTC 2026
% Result : Theorem 27.86s 5.48s
% Output : CNFRefutation 27.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ149^13 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % 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.09/0.19 % Computer : n018.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Oct 6 14:02:36 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.86/5.48
% 27.86/5.48 No.of.Axioms: 6
% 27.86/5.48
% 27.86/5.48 Length.of.Defs: 1296
% 27.86/5.48
% 27.86/5.48 Contains.Choice.Funs: false
% 27.86/5.48 ....eprover: <stdin>:1:(Column 167):(just read ''#pour_a''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 .eprover: <stdin>:1:(Column 167):(just read ''#pour_a''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 .eprover: <stdin>:1:(Column 167):(just read ''#pour_a''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 eprover: <stdin>:1:(Column 167):(just read ''#pour_a''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ..eprover: <stdin>:1:(Column 167):(just read ''#pour_a''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 .eprover: <stdin>:1:(Column 167):(just read ''#pour_a''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ..eprover: <stdin>:1:(Column 167):(just read ''#pour_a''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 .eprover: <stdin>:1:(Column 167):(just read ''#pour_a''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 .eprover: <stdin>:1:(Column 167):(just read ''#pour_a''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ...eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 .eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 .eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ...eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ...eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ..eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 .....eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ....eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ....eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ....eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ....eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 .....eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 .......eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 .....eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ..eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ...eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ...eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ..eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ...eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 .....eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ......eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ....eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 .....eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ......eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ......eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ......eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ......eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ......eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ......eprover: <stdin>:2:(Column 89):(just read ''#make_c''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 27.86/5.48 ..
% 27.86/5.48
% 27.86/5.48 ********************************
% 27.86/5.48 * All subproblems solved! *
% 27.86/5.48 ********************************
% 27.86/5.48 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:6,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:5510,loop_count:141,foatp_calls:30,translation:fof_full)
% 27.86/5.48
% 27.86/5.48 %**** Beginning of derivation protocol ****
% 27.86/5.48 % SZS output start CNFRefutation
% 27.86/5.48 thf(tp_mindex,type,(mindex: $tType)).
% 27.86/5.48 thf(tp_mworld,type,(mworld: $tType)).
% 27.86/5.48 thf(tp_'#make_c',type,('#make_c': mindex)).
% 27.86/5.48 thf(tp_'#pour_a',type,('#pour_a': mindex)).
% 27.86/5.48 thf(tp_'#pour_b',type,('#pour_b': mindex)).
% 27.86/5.48 thf(tp_acid,type,(acid: (mworld>$o))).
% 27.86/5.48 thf(tp_mactual,type,(mactual: mworld)).
% 27.86/5.48 thf(tp_mand,type,(mand: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 27.86/5.48 thf(tp_mbox,type,(mbox: (mindex>((mworld>$o)>(mworld>$o))))).
% 27.86/5.48 thf(tp_mdia,type,(mdia: (mindex>((mworld>$o)>(mworld>$o))))).
% 27.86/5.48 thf(tp_mequiv,type,(mequiv: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 27.86/5.48 thf(tp_mimplies,type,(mimplies: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 27.86/5.48 thf(tp_mlocal,type,(mlocal: ((mworld>$o)>$o))).
% 27.86/5.48 thf(tp_mnot,type,(mnot: ((mworld>$o)>(mworld>$o)))).
% 27.86/5.48 thf(tp_mor,type,(mor: ((mworld>$o)>((mworld>$o)>(mworld>$o))))).
% 27.86/5.48 thf(tp_mrel,type,(mrel: (mindex>(mworld>(mworld>$o))))).
% 27.86/5.48 thf(tp_sK10_REN,type,(sK10_REN: $o)).
% 27.86/5.48 thf(tp_sK11_SY163,type,(sK11_SY163: mworld)).
% 27.86/5.48 thf(tp_sK12_SY172,type,(sK12_SY172: mworld)).
% 27.86/5.48 thf(tp_sK13_REN,type,(sK13_REN: $o)).
% 27.86/5.48 thf(tp_sK1_SY35,type,(sK1_SY35: mworld)).
% 27.86/5.48 thf(tp_sK2_SY71,type,(sK2_SY71: mworld)).
% 27.86/5.48 thf(tp_sK3_SY169,type,(sK3_SY169: mworld)).
% 27.86/5.48 thf(tp_sK4_REN,type,(sK4_REN: $o)).
% 27.86/5.48 thf(tp_sK5_SY101,type,(sK5_SY101: mworld)).
% 27.86/5.48 thf(tp_sK6_SY170,type,(sK6_SY170: mworld)).
% 27.86/5.48 thf(tp_sK7_REN,type,(sK7_REN: $o)).
% 27.86/5.48 thf(tp_sK8_SY133,type,(sK8_SY133: mworld)).
% 27.86/5.48 thf(tp_sK9_SY171,type,(sK9_SY171: mworld)).
% 27.86/5.48 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)).
% 27.86/5.48 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)).
% 27.86/5.48 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)).
% 27.86/5.48 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)).
% 27.86/5.48 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)).
% 27.86/5.48 thf(mlocal,definition,(mlocal = (^[Phi:(mworld>$o)]: (Phi@mactual))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mlocal_def)).
% 27.86/5.48 thf(mnot,definition,(mnot = (^[A:(mworld>$o),W:mworld]: (~ (A@W)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mnot_def)).
% 27.86/5.48 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)).
% 27.86/5.48 thf(1,axiom,(mlocal@((mdia@'#make_c')@acid)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',make_c_acid)).
% 27.86/5.48 thf(2,axiom,(mlocal@((mbox@'#pour_a')@(mnot@acid))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',pour_a_acid)).
% 27.86/5.48 thf(5,axiom,(mlocal@((mimplies@((mbox@'#pour_a')@((mbox@'#pour_b')@(mnot@acid))))@((mbox@'#make_c')@(mnot@acid)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',pour_ab_make_axiom_2)).
% 27.86/5.48 thf(7,conjecture,(mlocal@((mand@((mdia@'#pour_a')@(mnot@acid)))@((mdia@'#pour_a')@((mdia@'#pour_b')@acid)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj)).
% 27.86/5.48 thf(8,negated_conjecture,(((mlocal@((mand@((mdia@'#pour_a')@(mnot@acid)))@((mdia@'#pour_a')@((mdia@'#pour_b')@acid))))=$false)),inference(negate_conjecture,[status(cth)],[7])).
% 27.86/5.48 thf(9,plain,((((?[SY24:mworld]: ((((mrel@'#pour_a')@mactual)@SY24) & (~ (acid@SY24)))) & (?[SY25:mworld]: ((((mrel@'#pour_a')@mactual)@SY25) & (?[SY19:mworld]: ((((mrel@'#pour_b')@SY25)@SY19) & (acid@SY19))))))=$false)),inference(unfold_def,[status(thm)],[8,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 27.86/5.48 thf(10,plain,(((?[SY35:mworld]: ((((mrel@'#make_c')@mactual)@SY35) & (acid@SY35)))=$true)),inference(unfold_def,[status(thm)],[1,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 27.86/5.48 thf(11,plain,(((![SY43:mworld]: ((((mrel@'#pour_a')@mactual)@SY43) => (~ (acid@SY43))))=$true)),inference(unfold_def,[status(thm)],[2,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 27.86/5.48 thf(14,plain,((((![SY133:mworld]: ((((mrel@'#pour_a')@mactual)@SY133) => (![SY118:mworld]: ((((mrel@'#pour_b')@SY133)@SY118) => (~ (acid@SY118)))))) => (![SY135:mworld]: ((((mrel@'#make_c')@mactual)@SY135) => (~ (acid@SY135)))))=$true)),inference(unfold_def,[status(thm)],[5,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 27.86/5.48 thf(16,plain,(((?[SY24:mworld]: ((((mrel@'#pour_a')@mactual)@SY24) & (~ (acid@SY24))))=$false)),inference(split_conjecture,[split_conjecture(split,[])],[9])).
% 27.86/5.48 thf(17,plain,(((?[SY25:mworld]: ((((mrel@'#pour_a')@mactual)@SY25) & (?[SY19:mworld]: ((((mrel@'#pour_b')@SY25)@SY19) & (acid@SY19)))))=$false)),inference(split_conjecture,[split_conjecture(split,[])],[9])).
% 27.86/5.48 thf(18,plain,(((~ (?[SY24:mworld]: ((((mrel@'#pour_a')@mactual)@SY24) & (~ (acid@SY24)))))=$true)),inference(polarity_switch,[status(thm)],[16])).
% 27.86/5.48 thf(19,plain,(((~ (?[SY25:mworld]: ((((mrel@'#pour_a')@mactual)@SY25) & (?[SY19:mworld]: ((((mrel@'#pour_b')@SY25)@SY19) & (acid@SY19))))))=$true)),inference(polarity_switch,[status(thm)],[17])).
% 27.86/5.48 thf(20,plain,(((![SY24:mworld]: ((~ (((mrel@'#pour_a')@mactual)@SY24)) | (acid@SY24)))=$true)),inference(extcnf_combined,[status(esa)],[18])).
% 27.86/5.48 thf(21,plain,(((![SY25:mworld]: ((![SY19:mworld]: ((~ (acid@SY19)) | (~ (((mrel@'#pour_b')@SY25)@SY19)))) | (~ (((mrel@'#pour_a')@mactual)@SY25))))=$true)),inference(extcnf_combined,[status(esa)],[19])).
% 27.86/5.48 thf(22,plain,((((acid@sK1_SY35) & (((mrel@'#make_c')@mactual)@sK1_SY35))=$true)),inference(extcnf_combined,[status(esa)],[10])).
% 27.86/5.48 thf(23,plain,(((![SY43:mworld]: ((~ (((mrel@'#pour_a')@mactual)@SY43)) | (~ (acid@SY43))))=$true)),inference(extcnf_combined,[status(esa)],[11])).
% 27.86/5.48 thf(26,plain,((((sK10_REN | (![SY135:mworld]: ((~ (((mrel@'#make_c')@mactual)@SY135)) | (~ (acid@SY135))))) & (sK10_REN => ((((mrel@'#pour_a')@mactual)@sK8_SY133) & ((((mrel@'#pour_b')@sK8_SY133)@sK9_SY171) & (acid@sK9_SY171)))))=$true)),inference(extcnf_combined,[status(esa)],[14])).
% 27.86/5.48 thf(29,plain,((((sK10_REN | (![SY135:mworld]: ((~ (((mrel@'#make_c')@mactual)@SY135)) | (~ (acid@SY135))))) & (sK10_REN => ((((mrel@'#pour_a')@mactual)@sK8_SY133) & ((((mrel@'#pour_b')@sK8_SY133)@sK9_SY171) & (acid@sK9_SY171)))))=$true)),inference(copy,[status(thm)],[26])).
% 27.86/5.48 thf(32,plain,(((![SY43:mworld]: ((~ (((mrel@'#pour_a')@mactual)@SY43)) | (~ (acid@SY43))))=$true)),inference(copy,[status(thm)],[23])).
% 27.86/5.48 thf(33,plain,((((acid@sK1_SY35) & (((mrel@'#make_c')@mactual)@sK1_SY35))=$true)),inference(copy,[status(thm)],[22])).
% 27.86/5.48 thf(34,plain,(((![SY24:mworld]: ((~ (((mrel@'#pour_a')@mactual)@SY24)) | (acid@SY24)))=$true)),inference(copy,[status(thm)],[20])).
% 27.86/5.48 thf(35,plain,(((~ ((~ (sK10_REN | (![SX0:mworld]: ((~ (((mrel@'#make_c')@mactual)@SX0)) | (~ (acid@SX0)))))) | (~ ((~ (sK10_REN)) | (~ ((~ (((mrel@'#pour_a')@mactual)@sK8_SY133)) | (~ (~ ((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171)))))))))))=$true)),inference(unfold_def,[status(thm)],[29,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 27.86/5.48 thf(36,plain,(((~ ((~ (acid@sK1_SY35)) | (~ (((mrel@'#make_c')@mactual)@sK1_SY35))))=$true)),inference(unfold_def,[status(thm)],[33,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 27.86/5.48 thf(40,plain,(![SV1:mworld]: ((((~ (((mrel@'#pour_a')@mactual)@SV1)) | (~ (acid@SV1)))=$true))),inference(extcnf_forall_pos,[status(thm)],[32])).
% 27.86/5.48 thf(41,plain,(![SV2:mworld]: ((((~ (((mrel@'#pour_a')@mactual)@SV2)) | (acid@SV2))=$true))),inference(extcnf_forall_pos,[status(thm)],[34])).
% 27.86/5.48 thf(42,plain,((((~ (sK10_REN | (![SX0:mworld]: ((~ (((mrel@'#make_c')@mactual)@SX0)) | (~ (acid@SX0)))))) | (~ ((~ (sK10_REN)) | (~ ((~ (((mrel@'#pour_a')@mactual)@sK8_SY133)) | (~ (~ ((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171))))))))))=$false)),inference(extcnf_not_pos,[status(thm)],[35])).
% 27.86/5.48 thf(43,plain,((((~ (acid@sK1_SY35)) | (~ (((mrel@'#make_c')@mactual)@sK1_SY35)))=$false)),inference(extcnf_not_pos,[status(thm)],[36])).
% 27.86/5.48 thf(47,plain,(![SV1:mworld]: (((~ (((mrel@'#pour_a')@mactual)@SV1))=$true) | ((~ (acid@SV1))=$true))),inference(extcnf_or_pos,[status(thm)],[40])).
% 27.86/5.48 thf(48,plain,(![SV2:mworld]: (((~ (((mrel@'#pour_a')@mactual)@SV2))=$true) | ((acid@SV2)=$true))),inference(extcnf_or_pos,[status(thm)],[41])).
% 27.86/5.48 thf(49,plain,(((~ (sK10_REN | (![SX0:mworld]: ((~ (((mrel@'#make_c')@mactual)@SX0)) | (~ (acid@SX0))))))=$false)),inference(extcnf_or_neg,[status(thm)],[42])).
% 27.86/5.48 thf(50,plain,(((~ ((~ (sK10_REN)) | (~ ((~ (((mrel@'#pour_a')@mactual)@sK8_SY133)) | (~ (~ ((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171)))))))))=$false)),inference(extcnf_or_neg,[status(thm)],[42])).
% 27.86/5.48 thf(51,plain,(((~ (acid@sK1_SY35))=$false)),inference(extcnf_or_neg,[status(thm)],[43])).
% 27.86/5.48 thf(52,plain,(((~ (((mrel@'#make_c')@mactual)@sK1_SY35))=$false)),inference(extcnf_or_neg,[status(thm)],[43])).
% 27.86/5.48 thf(59,plain,(![SV1:mworld]: (((((mrel@'#pour_a')@mactual)@SV1)=$false) | ((~ (acid@SV1))=$true))),inference(extcnf_not_pos,[status(thm)],[47])).
% 27.86/5.48 thf(60,plain,(![SV2:mworld]: (((((mrel@'#pour_a')@mactual)@SV2)=$false) | ((acid@SV2)=$true))),inference(extcnf_not_pos,[status(thm)],[48])).
% 27.86/5.48 thf(61,plain,(((sK10_REN | (![SX0:mworld]: ((~ (((mrel@'#make_c')@mactual)@SX0)) | (~ (acid@SX0)))))=$true)),inference(extcnf_not_neg,[status(thm)],[49])).
% 27.86/5.48 thf(62,plain,((((~ (sK10_REN)) | (~ ((~ (((mrel@'#pour_a')@mactual)@sK8_SY133)) | (~ (~ ((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171))))))))=$true)),inference(extcnf_not_neg,[status(thm)],[50])).
% 27.86/5.48 thf(63,plain,(((acid@sK1_SY35)=$true)),inference(extcnf_not_neg,[status(thm)],[51])).
% 27.86/5.48 thf(64,plain,(((((mrel@'#make_c')@mactual)@sK1_SY35)=$true)),inference(extcnf_not_neg,[status(thm)],[52])).
% 27.86/5.48 thf(71,plain,(![SV1:mworld]: (((acid@SV1)=$false) | ((((mrel@'#pour_a')@mactual)@SV1)=$false))),inference(extcnf_not_pos,[status(thm)],[59])).
% 27.86/5.48 thf(72,plain,(((sK10_REN)=$true) | ((![SX0:mworld]: ((~ (((mrel@'#make_c')@mactual)@SX0)) | (~ (acid@SX0))))=$true)),inference(extcnf_or_pos,[status(thm)],[61])).
% 27.86/5.48 thf(73,plain,(((~ (sK10_REN))=$true) | ((~ ((~ (((mrel@'#pour_a')@mactual)@sK8_SY133)) | (~ (~ ((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171)))))))=$true)),inference(extcnf_or_pos,[status(thm)],[62])).
% 27.86/5.48 thf(80,plain,(![SV3:mworld]: ((((~ (((mrel@'#make_c')@mactual)@SV3)) | (~ (acid@SV3)))=$true) | ((sK10_REN)=$true))),inference(extcnf_forall_pos,[status(thm)],[72])).
% 27.86/5.48 thf(81,plain,(((sK10_REN)=$false) | ((~ ((~ (((mrel@'#pour_a')@mactual)@sK8_SY133)) | (~ (~ ((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171)))))))=$true)),inference(extcnf_not_pos,[status(thm)],[73])).
% 27.86/5.48 thf(88,plain,(![SV3:mworld]: (((~ (((mrel@'#make_c')@mactual)@SV3))=$true) | ((~ (acid@SV3))=$true) | ((sK10_REN)=$true))),inference(extcnf_or_pos,[status(thm)],[80])).
% 27.86/5.48 thf(89,plain,((((~ (((mrel@'#pour_a')@mactual)@sK8_SY133)) | (~ (~ ((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171))))))=$false) | ((sK10_REN)=$false)),inference(extcnf_not_pos,[status(thm)],[81])).
% 27.86/5.48 thf(96,plain,(![SV3:mworld]: (((((mrel@'#make_c')@mactual)@SV3)=$false) | ((~ (acid@SV3))=$true) | ((sK10_REN)=$true))),inference(extcnf_not_pos,[status(thm)],[88])).
% 27.86/5.48 thf(97,plain,(((~ (((mrel@'#pour_a')@mactual)@sK8_SY133))=$false) | ((sK10_REN)=$false)),inference(extcnf_or_neg,[status(thm)],[89])).
% 27.86/5.48 thf(108,plain,(![SV3:mworld]: (((acid@SV3)=$false) | ((((mrel@'#make_c')@mactual)@SV3)=$false) | ((sK10_REN)=$true))),inference(extcnf_not_pos,[status(thm)],[96])).
% 27.86/5.48 thf(109,plain,(((((mrel@'#pour_a')@mactual)@sK8_SY133)=$true) | ((sK10_REN)=$false)),inference(extcnf_not_neg,[status(thm)],[97])).
% 27.86/5.48 thf(176,plain,(![SV7:mworld]: (((((mrel@'#pour_a')@mactual)@SV7)=$false) | ((acid@SV7)=$true))),inference(rename,[status(thm)],[60])).
% 27.86/5.48 thf(182,plain,(![SV8:mworld]: (((acid@SV8)=$false) | ((((mrel@'#pour_a')@mactual)@SV8)=$false))),inference(rename,[status(thm)],[71])).
% 27.86/5.48 thf(184,plain,(![SV8:mworld,SV7:mworld]: ((((acid@SV8) = (acid@SV7))=$false) | ((((mrel@'#pour_a')@mactual)@SV8)=$false) | ((((mrel@'#pour_a')@mactual)@SV7)=$false))),inference(res,[status(thm)],[182,176])).
% 27.86/5.48 thf(192,plain,(![SV7:mworld]: (((((mrel@'#pour_a')@mactual)@SV7)=$false) | ((((mrel@'#pour_a')@mactual)@SV7)=$false))),inference(extuni,[status(esa)],[184:[bind(SV8,$thf(SV7))]])).
% 27.86/5.48 thf(193,plain,(![SV7:mworld]: (((((mrel@'#pour_a')@mactual)@SV7)=$false))),inference(sim,[status(thm)],[192])).
% 27.86/5.48 thf(216,plain,(![SV10:mworld]: (((((mrel@'#pour_a')@mactual)@SV10)=$false))),inference(rename,[status(thm)],[193])).
% 27.86/5.48 thf(245,plain,(![SV10:mworld]: ((((((mrel@'#pour_a')@mactual)@sK8_SY133) = (((mrel@'#pour_a')@mactual)@SV10))=$false) | ((sK10_REN)=$false))),inference(res,[status(thm)],[109,216])).
% 27.86/5.48 thf(255,plain,(((sK10_REN)=$false)),inference(extuni,[status(esa)],[245:[bind(SV10,$thf(sK8_SY133))]])).
% 27.86/5.48 thf(287,plain,(![SV12:mworld]: (((acid@SV12)=$false) | ((((mrel@'#make_c')@mactual)@SV12)=$false) | ((sK10_REN)=$true))),inference(rename,[status(thm)],[108])).
% 27.86/5.48 thf(309,plain,(![SV12:mworld]: ((((acid@SV12) = (acid@sK1_SY35))=$false) | ((((mrel@'#make_c')@mactual)@SV12)=$false) | ((sK10_REN)=$true))),inference(res,[status(thm)],[287,63])).
% 27.86/5.48 thf(310,plain,(((sK10_REN)=$true) | ((((mrel@'#make_c')@mactual)@sK1_SY35)=$false)),inference(extuni,[status(esa)],[309:[bind(SV12,$thf(sK1_SY35))]])).
% 27.86/5.48 thf(594,plain,((((((mrel@'#make_c')@mactual)@sK1_SY35) = (((mrel@'#make_c')@mactual)@sK1_SY35))=$false) | ((sK10_REN)=$true)),inference(res,[status(thm)],[310,64])).
% 27.86/5.48 thf(596,plain,(((sK10_REN)=$true)),inference(extuni,[status(esa)],[594])).
% 27.86/5.48 thf(606,plain,(((sK10_REN = sK10_REN)=$false)),inference(res,[status(thm)],[596,255])).
% 27.86/5.48 thf(616,plain,((($false)=$true)),inference(extuni,[status(esa)],[606])).
% 27.86/5.48 thf(618,plain,((((sK10_REN | (![SY135:mworld]: ((~ (((mrel@'#make_c')@mactual)@SY135)) | (~ (acid@SY135))))) & (sK10_REN => ((((mrel@'#pour_a')@mactual)@sK8_SY133) & ((((mrel@'#pour_b')@sK8_SY133)@sK9_SY171) & (acid@sK9_SY171)))))=$true)),inference(copy,[status(thm)],[26])).
% 27.86/5.48 thf(622,plain,((((acid@sK1_SY35) & (((mrel@'#make_c')@mactual)@sK1_SY35))=$true)),inference(copy,[status(thm)],[22])).
% 27.86/5.48 thf(623,plain,(((![SY25:mworld]: ((![SY19:mworld]: ((~ (acid@SY19)) | (~ (((mrel@'#pour_b')@SY25)@SY19)))) | (~ (((mrel@'#pour_a')@mactual)@SY25))))=$true)),inference(copy,[status(thm)],[21])).
% 27.86/5.48 thf(625,plain,(((~ ((~ (sK10_REN | (![SX0:mworld]: ((~ (((mrel@'#make_c')@mactual)@SX0)) | (~ (acid@SX0)))))) | (~ ((~ (sK10_REN)) | (~ ((~ (((mrel@'#pour_a')@mactual)@sK8_SY133)) | (~ (~ ((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171)))))))))))=$true)),inference(unfold_def,[status(thm)],[618,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 27.86/5.48 thf(628,plain,(((~ ((~ (acid@sK1_SY35)) | (~ (((mrel@'#make_c')@mactual)@sK1_SY35))))=$true)),inference(unfold_def,[status(thm)],[622,mand,mbox,mdia,mequiv,mimplies,mlocal,mnot,mor])).
% 27.86/5.48 thf(630,plain,(![SV18:mworld]: ((((![SY173:mworld]: ((~ (acid@SY173)) | (~ (((mrel@'#pour_b')@SV18)@SY173)))) | (~ (((mrel@'#pour_a')@mactual)@SV18)))=$true))),inference(extcnf_forall_pos,[status(thm)],[623])).
% 27.86/5.48 thf(632,plain,((((~ (sK10_REN | (![SX0:mworld]: ((~ (((mrel@'#make_c')@mactual)@SX0)) | (~ (acid@SX0)))))) | (~ ((~ (sK10_REN)) | (~ ((~ (((mrel@'#pour_a')@mactual)@sK8_SY133)) | (~ (~ ((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171))))))))))=$false)),inference(extcnf_not_pos,[status(thm)],[625])).
% 27.86/5.48 thf(635,plain,((((~ (acid@sK1_SY35)) | (~ (((mrel@'#make_c')@mactual)@sK1_SY35)))=$false)),inference(extcnf_not_pos,[status(thm)],[628])).
% 27.86/5.48 thf(637,plain,(![SV18:mworld]: (((![SY173:mworld]: ((~ (acid@SY173)) | (~ (((mrel@'#pour_b')@SV18)@SY173))))=$true) | ((~ (((mrel@'#pour_a')@mactual)@SV18))=$true))),inference(extcnf_or_pos,[status(thm)],[630])).
% 27.86/5.48 thf(640,plain,(((~ (sK10_REN | (![SX0:mworld]: ((~ (((mrel@'#make_c')@mactual)@SX0)) | (~ (acid@SX0))))))=$false)),inference(extcnf_or_neg,[status(thm)],[632])).
% 27.86/5.48 thf(641,plain,(((~ ((~ (sK10_REN)) | (~ ((~ (((mrel@'#pour_a')@mactual)@sK8_SY133)) | (~ (~ ((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171)))))))))=$false)),inference(extcnf_or_neg,[status(thm)],[632])).
% 27.86/5.48 thf(646,plain,(((~ (acid@sK1_SY35))=$false)),inference(extcnf_or_neg,[status(thm)],[635])).
% 27.86/5.48 thf(647,plain,(((~ (((mrel@'#make_c')@mactual)@sK1_SY35))=$false)),inference(extcnf_or_neg,[status(thm)],[635])).
% 27.86/5.48 thf(649,plain,(![SV18:mworld,SV19:mworld]: ((((~ (acid@SV19)) | (~ (((mrel@'#pour_b')@SV18)@SV19)))=$true) | ((~ (((mrel@'#pour_a')@mactual)@SV18))=$true))),inference(extcnf_forall_pos,[status(thm)],[637])).
% 27.86/5.48 thf(652,plain,(((sK10_REN | (![SX0:mworld]: ((~ (((mrel@'#make_c')@mactual)@SX0)) | (~ (acid@SX0)))))=$true)),inference(extcnf_not_neg,[status(thm)],[640])).
% 27.86/5.48 thf(653,plain,((((~ (sK10_REN)) | (~ ((~ (((mrel@'#pour_a')@mactual)@sK8_SY133)) | (~ (~ ((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171))))))))=$true)),inference(extcnf_not_neg,[status(thm)],[641])).
% 27.86/5.48 thf(658,plain,(((acid@sK1_SY35)=$true)),inference(extcnf_not_neg,[status(thm)],[646])).
% 27.86/5.48 thf(659,plain,(((((mrel@'#make_c')@mactual)@sK1_SY35)=$true)),inference(extcnf_not_neg,[status(thm)],[647])).
% 27.86/5.48 thf(661,plain,(![SV18:mworld,SV19:mworld]: (((~ (acid@SV19))=$true) | ((~ (((mrel@'#pour_b')@SV18)@SV19))=$true) | ((~ (((mrel@'#pour_a')@mactual)@SV18))=$true))),inference(extcnf_or_pos,[status(thm)],[649])).
% 27.86/5.48 thf(664,plain,(((sK10_REN)=$true) | ((![SX0:mworld]: ((~ (((mrel@'#make_c')@mactual)@SX0)) | (~ (acid@SX0))))=$true)),inference(extcnf_or_pos,[status(thm)],[652])).
% 27.86/5.48 thf(665,plain,(((~ (sK10_REN))=$true) | ((~ ((~ (((mrel@'#pour_a')@mactual)@sK8_SY133)) | (~ (~ ((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171)))))))=$true)),inference(extcnf_or_pos,[status(thm)],[653])).
% 27.86/5.48 thf(670,plain,(![SV18:mworld,SV19:mworld]: (((acid@SV19)=$false) | ((~ (((mrel@'#pour_b')@SV18)@SV19))=$true) | ((~ (((mrel@'#pour_a')@mactual)@SV18))=$true))),inference(extcnf_not_pos,[status(thm)],[661])).
% 27.86/5.48 thf(673,plain,(![SV21:mworld]: ((((~ (((mrel@'#make_c')@mactual)@SV21)) | (~ (acid@SV21)))=$true) | ((sK10_REN)=$true))),inference(extcnf_forall_pos,[status(thm)],[664])).
% 27.86/5.48 thf(674,plain,(((sK10_REN)=$false) | ((~ ((~ (((mrel@'#pour_a')@mactual)@sK8_SY133)) | (~ (~ ((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171)))))))=$true)),inference(extcnf_not_pos,[status(thm)],[665])).
% 27.86/5.48 thf(679,plain,(![SV19:mworld,SV18:mworld]: (((((mrel@'#pour_b')@SV18)@SV19)=$false) | ((acid@SV19)=$false) | ((~ (((mrel@'#pour_a')@mactual)@SV18))=$true))),inference(extcnf_not_pos,[status(thm)],[670])).
% 27.86/5.48 thf(682,plain,(![SV21:mworld]: (((~ (((mrel@'#make_c')@mactual)@SV21))=$true) | ((~ (acid@SV21))=$true) | ((sK10_REN)=$true))),inference(extcnf_or_pos,[status(thm)],[673])).
% 27.86/5.48 thf(683,plain,((((~ (((mrel@'#pour_a')@mactual)@sK8_SY133)) | (~ (~ ((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171))))))=$false) | ((sK10_REN)=$false)),inference(extcnf_not_pos,[status(thm)],[674])).
% 27.86/5.48 thf(688,plain,(![SV19:mworld,SV18:mworld]: (((((mrel@'#pour_a')@mactual)@SV18)=$false) | ((acid@SV19)=$false) | ((((mrel@'#pour_b')@SV18)@SV19)=$false))),inference(extcnf_not_pos,[status(thm)],[679])).
% 27.86/5.48 thf(692,plain,(![SV21:mworld]: (((((mrel@'#make_c')@mactual)@SV21)=$false) | ((~ (acid@SV21))=$true) | ((sK10_REN)=$true))),inference(extcnf_not_pos,[status(thm)],[682])).
% 27.86/5.48 thf(693,plain,(((~ (((mrel@'#pour_a')@mactual)@sK8_SY133))=$false) | ((sK10_REN)=$false)),inference(extcnf_or_neg,[status(thm)],[683])).
% 27.86/5.48 thf(694,plain,(((~ (~ ((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171)))))=$false) | ((sK10_REN)=$false)),inference(extcnf_or_neg,[status(thm)],[683])).
% 27.86/5.48 thf(704,plain,(![SV21:mworld]: (((acid@SV21)=$false) | ((((mrel@'#make_c')@mactual)@SV21)=$false) | ((sK10_REN)=$true))),inference(extcnf_not_pos,[status(thm)],[692])).
% 27.86/5.48 thf(705,plain,(((((mrel@'#pour_a')@mactual)@sK8_SY133)=$true) | ((sK10_REN)=$false)),inference(extcnf_not_neg,[status(thm)],[693])).
% 27.86/5.48 thf(706,plain,(((~ ((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171))))=$true) | ((sK10_REN)=$false)),inference(extcnf_not_neg,[status(thm)],[694])).
% 27.86/5.48 thf(712,plain,((((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)) | (~ (acid@sK9_SY171)))=$false) | ((sK10_REN)=$false)),inference(extcnf_not_pos,[status(thm)],[706])).
% 27.86/5.48 thf(717,plain,(((~ (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171))=$false) | ((sK10_REN)=$false)),inference(extcnf_or_neg,[status(thm)],[712])).
% 27.86/5.48 thf(718,plain,(((~ (acid@sK9_SY171))=$false) | ((sK10_REN)=$false)),inference(extcnf_or_neg,[status(thm)],[712])).
% 27.86/5.48 thf(725,plain,(((((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)=$true) | ((sK10_REN)=$false)),inference(extcnf_not_neg,[status(thm)],[717])).
% 27.86/5.48 thf(726,plain,(((acid@sK9_SY171)=$true) | ((sK10_REN)=$false)),inference(extcnf_not_neg,[status(thm)],[718])).
% 27.86/5.48 thf(792,plain,(![SV25:mworld,SV26:mworld]: (((((mrel@'#pour_a')@mactual)@SV26)=$false) | ((acid@SV25)=$false) | ((((mrel@'#pour_b')@SV26)@SV25)=$false))),inference(rename,[status(thm)],[688])).
% 27.86/5.48 thf(1373,plain,(![SV32:mworld]: (((acid@SV32)=$false) | ((((mrel@'#make_c')@mactual)@SV32)=$false) | ((sK10_REN)=$true))),inference(rename,[status(thm)],[704])).
% 27.86/5.48 thf(1438,plain,(![SV32:mworld]: ((((acid@SV32) = (acid@sK1_SY35))=$false) | ((((mrel@'#make_c')@mactual)@SV32)=$false) | ((sK10_REN)=$true))),inference(res,[status(thm)],[1373,658])).
% 27.86/5.48 thf(1439,plain,(((sK10_REN)=$true) | ((((mrel@'#make_c')@mactual)@sK1_SY35)=$false)),inference(extuni,[status(esa)],[1438:[bind(SV32,$thf(sK1_SY35))]])).
% 27.86/5.48 thf(2642,plain,((((((mrel@'#make_c')@mactual)@sK1_SY35) = (((mrel@'#make_c')@mactual)@sK1_SY35))=$false) | ((sK10_REN)=$true)),inference(res,[status(thm)],[1439,659])).
% 27.86/5.48 thf(2644,plain,(((sK10_REN)=$true)),inference(extuni,[status(esa)],[2642])).
% 27.86/5.48 thf(2784,plain,(((sK10_REN = sK10_REN)=$false) | ((acid@sK9_SY171)=$true)),inference(res,[status(thm)],[2644,726])).
% 27.86/5.48 thf(2785,plain,(((sK10_REN = sK10_REN)=$false) | ((((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)=$true)),inference(res,[status(thm)],[2644,725])).
% 27.86/5.48 thf(2788,plain,(((sK10_REN = sK10_REN)=$false) | ((((mrel@'#pour_a')@mactual)@sK8_SY133)=$true)),inference(res,[status(thm)],[2644,705])).
% 27.86/5.48 thf(2789,plain,(((((mrel@'#pour_a')@mactual)@sK8_SY133)=$true)),inference(extuni,[status(esa)],[2788])).
% 27.86/5.48 thf(2790,plain,(((((mrel@'#pour_b')@sK8_SY133)@sK9_SY171)=$true)),inference(extuni,[status(esa)],[2785])).
% 27.86/5.48 thf(2791,plain,(((acid@sK9_SY171)=$true)),inference(extuni,[status(esa)],[2784])).
% 27.86/5.48 thf(2831,plain,(![SV25:mworld,SV26:mworld]: ((((((mrel@'#pour_a')@mactual)@sK8_SY133) = (((mrel@'#pour_a')@mactual)@SV26))=$false) | ((acid@SV25)=$false) | ((((mrel@'#pour_b')@SV26)@SV25)=$false))),inference(res,[status(thm)],[2789,792])).
% 27.86/5.48 thf(2854,plain,(![SV25:mworld]: (((((mrel@'#pour_b')@sK8_SY133)@SV25)=$false) | ((acid@SV25)=$false))),inference(extuni,[status(esa)],[2831:[bind(SV26,$thf(sK8_SY133))]])).
% 27.86/5.48 thf(5404,plain,(![SV41:mworld]: (((((mrel@'#pour_b')@sK8_SY133)@SV41)=$false) | ((acid@SV41)=$false))),inference(rename,[status(thm)],[2854])).
% 27.86/5.48 thf(5412,plain,(![SV41:mworld]: ((((((mrel@'#pour_b')@sK8_SY133)@SV41) = (((mrel@'#pour_b')@sK8_SY133)@sK9_SY171))=$false) | ((acid@SV41)=$false))),inference(res,[status(thm)],[5404,2790])).
% 27.86/5.48 thf(5473,plain,(((acid@sK9_SY171)=$false)),inference(extuni,[status(esa)],[5412:[bind(SV41,$thf(sK9_SY171))]])).
% 27.86/5.48 thf(5479,plain,((((acid@sK9_SY171) = (acid@sK9_SY171))=$false)),inference(res,[status(thm)],[5473,2791])).
% 27.86/5.48 thf(5510,plain,((($false)=$true)),inference(extuni,[status(esa)],[5479])).
% 27.86/5.48 thf(5511,plain,($false),inference(solved_all_splits,[solved_all_splits(join,[])],[5510,616])).
% 27.86/5.48 % SZS output end CNFRefutation
% 27.86/5.48
% 27.86/5.48 %**** End of derivation protocol ****
% 27.86/5.48 %**** no. of clauses in derivation: 125 ****
% 27.86/5.48 %**** clause counter: 5510 ****
% 27.86/5.48
% 27.86/5.48 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:6,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:5510,loop_count:141,foatp_calls:30,translation:fof_full)
%------------------------------------------------------------------------------