%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : MED001+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Sun Jul 17 21:53:05 EDT 2022
% Result : Theorem 29.25s 29.27s
% Output : Proof 29.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : MED001+1 : TPTP v8.1.0. Released v3.2.0.
% 0.10/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n009.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Tue Jul 5 01:37:52 EDT 2022
% 0.12/0.33 % CPUTime :
% 29.25/29.27 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.32/29.27 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.32/29.28
% 29.32/29.28 %-----------------------------------------------------
% 29.32/29.28 fof(sn_cure_1, axiom, ! [_30795] : (! [_30803] : (~ gt(_30795, _30803) => bsecretioni(_30803)) & bcapacitysn(_30795) & qilt27(_30795) & ! [_30803] : (gt(_30795, _30803) => conditionhyper(_30803)) => ! [_30803] : (~ gt(_30795, _30803) => conditionnormo(_30803))), file('/export/starexec/sandbox/benchmark/Axioms/MED001+0.ax', sn_cure_1)).
% 29.32/29.28 fof(sulfonylurea_effect, axiom, ! [_31200] : (! [_31208] : (~ gt(_31200, _31208) => drugsu(_31208)) & ~ bcapacityex(_31200) => ! [_31208] : (~ gt(_31200, _31208) => bsecretioni(_31208))), file('/export/starexec/sandbox/benchmark/Axioms/MED001+0.ax', sulfonylurea_effect)).
% 29.32/29.28 fof(treatmentsn2, conjecture, ! [_31494] : (~ gt(n0, _31494) => drugsu(_31494)) & ! [_31494] : (gt(n0, _31494) => conditionhyper(_31494)) & bcapacitysn(n0) & qilt27(n0) => ! [_31494] : (~ gt(n0, _31494) => conditionnormo(_31494)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', treatmentsn2)).
% 29.32/29.28 fof(xorcapacity4, axiom, ! [_31899] : (~ bcapacityex(_31899) | ~ bcapacitysn(_31899)), file('/export/starexec/sandbox/benchmark/Axioms/MED001+0.ax', xorcapacity4)).
% 29.32/29.28
% 29.32/29.28 cnf(1, plain, [-(11 ^ [_13459]), conditionhyper(10 ^ [_13459])], clausify(sn_cure_1)).
% 29.32/29.28 cnf(2, plain, [-(11 ^ [_13459]), -(gt(_13459, 10 ^ [_13459]))], clausify(sn_cure_1)).
% 29.32/29.28 cnf(3, plain, [-(9 ^ [_13459]), bsecretioni(8 ^ [_13459])], clausify(sn_cure_1)).
% 29.32/29.28 cnf(4, plain, [-(9 ^ [_13459]), gt(_13459, 8 ^ [_13459])], clausify(sn_cure_1)).
% 29.32/29.28 cnf(5, plain, [-(5 ^ [_12323]), drugsu(4 ^ [_12323])], clausify(sulfonylurea_effect)).
% 29.32/29.28 cnf(6, plain, [-(5 ^ [_12323]), gt(_12323, 4 ^ [_12323])], clausify(sulfonylurea_effect)).
% 29.32/29.28 cnf(7, plain, [gt(n0, 29 ^ [])], clausify(treatmentsn2)).
% 29.32/29.28 cnf(8, plain, [conditionnormo(29 ^ [])], clausify(treatmentsn2)).
% 29.32/29.28 cnf(9, plain, [-(gt(n0, _17674)), -(drugsu(_17674))], clausify(treatmentsn2)).
% 29.32/29.28 cnf(10, plain, [-(bcapacitysn(n0))], clausify(treatmentsn2)).
% 29.32/29.28 cnf(11, plain, [-(qilt27(n0))], clausify(treatmentsn2)).
% 29.32/29.28 cnf(12, plain, [gt(n0, _17850), -(conditionhyper(_17850))], clausify(treatmentsn2)).
% 29.32/29.28 cnf(13, plain, [bcapacityex(_10098), bcapacitysn(_10098)], clausify(xorcapacity4)).
% 29.32/29.28 cnf(14, plain, [-(bcapacityex(_12323)), 5 ^ [_12323], -(gt(_12323, _12643)), -(bsecretioni(_12643))], clausify(sulfonylurea_effect)).
% 29.32/29.28 cnf(15, plain, [-(conditionnormo(_14012)), -(gt(_13459, _14012)), 9 ^ [_13459], bcapacitysn(_13459), qilt27(_13459), 11 ^ [_13459]], clausify(sn_cure_1)).
% 29.32/29.28
% 29.32/29.28 cnf('1',plain,[gt(n0, 29 ^ [])],start(7)).
% 29.32/29.28 cnf('1.1',plain,[-(gt(n0, 29 ^ [])), -(conditionnormo(29 ^ [])), 9 ^ [n0], bcapacitysn(n0), qilt27(n0), 11 ^ [n0]],extension(15,bind([[_14012, _13459], [29 ^ [], n0]]))).
% 29.32/29.28 cnf('1.1.1',plain,[conditionnormo(29 ^ [])],extension(8)).
% 29.32/29.28 cnf('1.1.2',plain,[-(9 ^ [n0]), bsecretioni(8 ^ [n0])],extension(3,bind([[_13459], [n0]]))).
% 29.32/29.28 cnf('1.1.2.1',plain,[-(bsecretioni(8 ^ [n0])), -(bcapacityex(n0)), 5 ^ [n0], -(gt(n0, 8 ^ [n0]))],extension(14,bind([[_12323, _12643], [n0, 8 ^ [n0]]]))).
% 29.32/29.28 cnf('1.1.2.1.1',plain,[bcapacityex(n0), bcapacitysn(n0)],extension(13,bind([[_10098], [n0]]))).
% 29.32/29.28 cnf('1.1.2.1.1.1',plain,[-(bcapacitysn(n0))],extension(10)).
% 29.32/29.28 cnf('1.1.2.1.2',plain,[-(5 ^ [n0]), drugsu(4 ^ [n0])],extension(5,bind([[_12323], [n0]]))).
% 29.32/29.28 cnf('1.1.2.1.2.1',plain,[-(drugsu(4 ^ [n0])), -(gt(n0, 4 ^ [n0]))],extension(9,bind([[_17674], [4 ^ [n0]]]))).
% 29.32/29.28 cnf('1.1.2.1.2.1.1',plain,[gt(n0, 4 ^ [n0]), -(5 ^ [n0])],extension(6,bind([[_12323], [n0]]))).
% 29.32/29.28 cnf('1.1.2.1.2.1.1.1',plain,[5 ^ [n0]],reduction('1.1.2.1')).
% 29.32/29.28 cnf('1.1.2.1.3',plain,[gt(n0, 8 ^ [n0]), -(9 ^ [n0])],extension(4,bind([[_13459], [n0]]))).
% 29.32/29.28 cnf('1.1.2.1.3.1',plain,[9 ^ [n0]],reduction('1.1')).
% 29.32/29.28 cnf('1.1.3',plain,[-(bcapacitysn(n0))],extension(10)).
% 29.32/29.28 cnf('1.1.4',plain,[-(qilt27(n0))],extension(11)).
% 29.32/29.28 cnf('1.1.5',plain,[-(11 ^ [n0]), conditionhyper(10 ^ [n0])],extension(1,bind([[_13459], [n0]]))).
% 29.32/29.28 cnf('1.1.5.1',plain,[-(conditionhyper(10 ^ [n0])), gt(n0, 10 ^ [n0])],extension(12,bind([[_17850], [10 ^ [n0]]]))).
% 29.32/29.28 cnf('1.1.5.1.1',plain,[-(gt(n0, 10 ^ [n0])), -(11 ^ [n0])],extension(2,bind([[_13459], [n0]]))).
% 29.32/29.28 cnf('1.1.5.1.1.1',plain,[11 ^ [n0]],reduction('1.1')).
% 29.32/29.28 %-----------------------------------------------------
% 29.33/29.28
% 29.33/29.28 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------