%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KRS180+1 : TPTP v8.1.0. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n021.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 03:13:55 EDT 2022
% Result : Theorem 0.34s 1.40s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : KRS180+1 : TPTP v8.1.0. Bugfixed v5.4.0.
% 0.11/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n021.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 Jun 7 11:13:51 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.34/1.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.34/1.40 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.34/1.41
% 0.34/1.41 %-----------------------------------------------------
% 0.34/1.41 fof(isa_exclusive, conjecture, ! [_27770, _27773] : ? [_27781, _27784] : (status(_27781, _27784, _27770) => ~ (isa(_27770, _27773) & (nota(_27770, _27773) | nevera(_27770, _27773) | xora(_27770, _27773)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', isa_exclusive)).
% 0.34/1.41 fof(mighta, axiom, ! [_28077, _28080] : (? [_28088, _28091] : (status(_28088, _28091, _28077) & status(_28088, _28091, _28080)) <=> mighta(_28077, _28080)), file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax', mighta)).
% 0.34/1.41 fof(isa, axiom, ! [_28321, _28324] : (! [_28332, _28335] : (status(_28332, _28335, _28321) => status(_28332, _28335, _28324)) <=> isa(_28321, _28324)), file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax', isa)).
% 0.34/1.41 fof(nota, axiom, ! [_28550, _28553] : (? [_28561, _28564] : (status(_28561, _28564, _28550) & ~ status(_28561, _28564, _28553)) <=> nota(_28550, _28553)), file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax', nota)).
% 0.34/1.41 fof(nevera, axiom, ! [_28801, _28804] : (! [_28812, _28815] : (status(_28812, _28815, _28801) => ~ status(_28812, _28815, _28804)) <=> nevera(_28801, _28804)), file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax', nevera)).
% 0.34/1.41 fof(xora, axiom, ! [_29039, _29042] : (! [_29050, _29053] : (status(_29050, _29053, _29039) <~> status(_29050, _29053, _29042)) <=> xora(_29039, _29042)), file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax', xora)).
% 0.34/1.41
% 0.34/1.41 cnf(1, plain, [-(status(_18318, _18323, 29 ^ []))], clausify(isa_exclusive)).
% 0.34/1.41 cnf(2, plain, [-(isa(29 ^ [], 30 ^ []))], clausify(isa_exclusive)).
% 0.34/1.41 cnf(3, plain, [-(nota(29 ^ [], 30 ^ [])), -(nevera(29 ^ [], 30 ^ [])), -(xora(29 ^ [], 30 ^ []))], clausify(isa_exclusive)).
% 0.34/1.41 cnf(4, plain, [-(status(1 ^ [_6941, _6878], 2 ^ [_6941, _6878], _6878)), mighta(_6878, _6941)], clausify(mighta)).
% 0.34/1.41 cnf(5, plain, [-(mighta(_6878, _6941)), status(_7014, _7070, _6878), status(_7014, _7070, _6941)], clausify(mighta)).
% 0.34/1.41 cnf(6, plain, [isa(_7503, _7566), status(_7638, _7693, _7503), -(status(_7638, _7693, _7566))], clausify(isa)).
% 0.34/1.41 cnf(7, plain, [-(status(5 ^ [_8191, _8126], 6 ^ [_8191, _8126], _8126)), nota(_8126, _8191)], clausify(nota)).
% 0.34/1.41 cnf(8, plain, [status(5 ^ [_8191, _8126], 6 ^ [_8191, _8126], _8191), nota(_8126, _8191)], clausify(nota)).
% 0.34/1.41 cnf(9, plain, [nevera(_8775, _8840), status(_8914, _8971, _8775), status(_8914, _8971, _8840)], clausify(nevera)).
% 0.34/1.41 cnf(10, plain, [xora(_9422, _9487), status(_9561, _9618, _9422), status(_9561, _9618, _9487)], clausify(xora)).
% 0.34/1.41
% 0.34/1.41 cnf('1',plain,[nevera(29 ^ [], 30 ^ []), status(1 ^ [29 ^ [], 30 ^ []], 2 ^ [29 ^ [], 30 ^ []], 29 ^ []), status(1 ^ [29 ^ [], 30 ^ []], 2 ^ [29 ^ [], 30 ^ []], 30 ^ [])],start(9,bind([[_8775, _8914, _8971, _8840], [29 ^ [], 1 ^ [29 ^ [], 30 ^ []], 2 ^ [29 ^ [], 30 ^ []], 30 ^ []]]))).
% 0.34/1.41 cnf('1.1',plain,[-(nevera(29 ^ [], 30 ^ [])), -(nota(29 ^ [], 30 ^ [])), -(xora(29 ^ [], 30 ^ []))],extension(3)).
% 0.34/1.41 cnf('1.1.1',plain,[nota(29 ^ [], 30 ^ []), -(status(5 ^ [30 ^ [], 29 ^ []], 6 ^ [30 ^ [], 29 ^ []], 29 ^ []))],extension(7,bind([[_8191, _8126], [30 ^ [], 29 ^ []]]))).
% 0.34/1.41 cnf('1.1.1.1',plain,[status(5 ^ [30 ^ [], 29 ^ []], 6 ^ [30 ^ [], 29 ^ []], 29 ^ []), isa(29 ^ [], 30 ^ []), -(status(5 ^ [30 ^ [], 29 ^ []], 6 ^ [30 ^ [], 29 ^ []], 30 ^ []))],extension(6,bind([[_7503, _7638, _7693, _7566], [29 ^ [], 5 ^ [30 ^ [], 29 ^ []], 6 ^ [30 ^ [], 29 ^ []], 30 ^ []]]))).
% 0.34/1.41 cnf('1.1.1.1.1',plain,[-(isa(29 ^ [], 30 ^ []))],extension(2)).
% 0.34/1.41 cnf('1.1.1.1.2',plain,[status(5 ^ [30 ^ [], 29 ^ []], 6 ^ [30 ^ [], 29 ^ []], 30 ^ []), nota(29 ^ [], 30 ^ [])],extension(8,bind([[_8126, _8191], [29 ^ [], 30 ^ []]]))).
% 0.34/1.41 cnf('1.1.1.1.2.1',plain,[-(nota(29 ^ [], 30 ^ []))],reduction('1.1')).
% 0.34/1.41 cnf('1.1.2',plain,[xora(29 ^ [], 30 ^ []), status(_20863, _20864, 29 ^ []), status(_20863, _20864, 30 ^ [])],extension(10,bind([[_9422, _9561, _9618, _9487], [29 ^ [], _20863, _20864, 30 ^ []]]))).
% 0.34/1.41 cnf('1.1.2.1',plain,[-(status(_20863, _20864, 29 ^ []))],extension(1,bind([[_18318, _18323], [_20863, _20864]]))).
% 0.34/1.41 cnf('1.1.2.2',plain,[-(status(_20863, _20864, 30 ^ [])), isa(29 ^ [], 30 ^ []), status(_20863, _20864, 29 ^ [])],extension(6,bind([[_7566, _7638, _7693, _7503], [30 ^ [], _20863, _20864, 29 ^ []]]))).
% 0.34/1.41 cnf('1.1.2.2.1',plain,[-(isa(29 ^ [], 30 ^ []))],extension(2)).
% 0.34/1.41 cnf('1.1.2.2.2',plain,[-(status(_20863, _20864, 29 ^ []))],extension(1,bind([[_18318, _18323], [_20863, _20864]]))).
% 0.34/1.41 cnf('1.2',plain,[-(status(1 ^ [29 ^ [], 30 ^ []], 2 ^ [29 ^ [], 30 ^ []], 29 ^ []))],extension(1,bind([[_18318, _18323], [1 ^ [29 ^ [], 30 ^ []], 2 ^ [29 ^ [], 30 ^ []]]]))).
% 0.34/1.41 cnf('1.3',plain,[-(status(1 ^ [29 ^ [], 30 ^ []], 2 ^ [29 ^ [], 30 ^ []], 30 ^ [])), mighta(30 ^ [], 29 ^ [])],extension(4,bind([[_6878, _6941], [30 ^ [], 29 ^ []]]))).
% 0.34/1.41 cnf('1.3.1',plain,[-(mighta(30 ^ [], 29 ^ [])), status(_21030, _21031, 30 ^ []), status(_21030, _21031, 29 ^ [])],extension(5,bind([[_6878, _7014, _7070, _6941], [30 ^ [], _21030, _21031, 29 ^ []]]))).
% 0.34/1.41 cnf('1.3.1.1',plain,[-(status(_21030, _21031, 30 ^ [])), isa(29 ^ [], 30 ^ []), status(_21030, _21031, 29 ^ [])],extension(6,bind([[_7566, _7638, _7693, _7503], [30 ^ [], _21030, _21031, 29 ^ []]]))).
% 0.34/1.41 cnf('1.3.1.1.1',plain,[-(isa(29 ^ [], 30 ^ []))],extension(2)).
% 0.34/1.41 cnf('1.3.1.1.2',plain,[-(status(_21030, _21031, 29 ^ []))],extension(1,bind([[_18318, _18323], [_21030, _21031]]))).
% 0.34/1.41 cnf('1.3.1.2',plain,[-(status(_21030, _21031, 29 ^ []))],extension(1,bind([[_18318, _18323], [_21030, _21031]]))).
% 0.34/1.41 %-----------------------------------------------------
% 0.34/1.41
% 0.34/1.42 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------