%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET792+4 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n007.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 : Tue Jul 19 02:56:01 EDT 2022
% Result : Theorem 0.33s 1.40s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SET792+4 : TPTP v8.1.0. Released v3.2.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n007.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 : Sun Jul 10 05:11:01 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.33/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.40 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.41
% 0.33/1.41 %-----------------------------------------------------
% 0.33/1.41 fof(thIV4, conjecture, ! [_66564, _66567, _66570] : (order(_66564, _66567) & least(_66570, _66564, _66567) => min(_66570, _66564, _66567)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', thIV4)).
% 0.33/1.41 fof(order, axiom, ! [_66883, _66886] : (order(_66883, _66886) <=> ! [_66904] : (member(_66904, _66886) => apply(_66883, _66904, _66904)) & ! [_66904, _66937] : (member(_66904, _66886) & member(_66937, _66886) => apply(_66883, _66904, _66937) & apply(_66883, _66937, _66904) => _66904 = _66937) & ! [_66904, _66937, _67001] : (member(_66904, _66886) & member(_66937, _66886) & member(_67001, _66886) => apply(_66883, _66904, _66937) & apply(_66883, _66937, _67001) => apply(_66883, _66904, _67001))), file('/export/starexec/sandbox/benchmark/Axioms/SET006+3.ax', order)).
% 0.33/1.41 fof(least, axiom, ! [_67540, _67543, _67546] : (least(_67546, _67540, _67543) <=> member(_67546, _67543) & ! [_67577] : (member(_67577, _67543) => apply(_67540, _67546, _67577))), file('/export/starexec/sandbox/benchmark/Axioms/SET006+3.ax', least)).
% 0.33/1.41 fof(min, axiom, ! [_67816, _67819, _67822] : (min(_67822, _67816, _67819) <=> member(_67822, _67819) & ! [_67853] : (member(_67853, _67819) & apply(_67816, _67853, _67822) => _67822 = _67853)), file('/export/starexec/sandbox/benchmark/Axioms/SET006+3.ax', min)).
% 0.33/1.41
% 0.33/1.41 cnf(1, plain, [-(order(17 ^ [], 18 ^ []))], clausify(thIV4)).
% 0.33/1.41 cnf(2, plain, [-(least(19 ^ [], 17 ^ [], 18 ^ []))], clausify(thIV4)).
% 0.33/1.41 cnf(3, plain, [min(19 ^ [], 17 ^ [], 18 ^ [])], clausify(thIV4)).
% 0.33/1.41 cnf(4, plain, [-(_11512 = _11512)], theory(equality)).
% 0.33/1.41 cnf(5, plain, [-(member(_20600, _20731)), member(_20533, _20666), _20533 = _20600, _20666 = _20731], theory(equality)).
% 0.33/1.41 cnf(6, plain, [order(_24646, _24799), member(_25322, _24799), member(_25249, _24799), -(_25249 = _25322), apply(_24646, _25249, _25322), apply(_24646, _25322, _25249)], clausify(order)).
% 0.33/1.41 cnf(7, plain, [least(_29806, _29669, _29738), -(member(_29806, _29738))], clausify(least)).
% 0.33/1.41 cnf(8, plain, [least(_29806, _29669, _29738), member(_30031, _29738), -(apply(_29669, _29806, _30031))], clausify(least)).
% 0.33/1.41 cnf(9, plain, [-(min(_31356, _31207, _31282)), member(_31356, _31282), -(member(14 ^ [_31356, _31282, _31207], _31282))], clausify(min)).
% 0.33/1.41 cnf(10, plain, [-(min(_31356, _31207, _31282)), member(_31356, _31282), -(apply(_31207, 14 ^ [_31356, _31282, _31207], _31356))], clausify(min)).
% 0.33/1.41 cnf(11, plain, [-(min(_31356, _31207, _31282)), member(_31356, _31282), _31356 = 14 ^ [_31356, _31282, _31207]], clausify(min)).
% 0.33/1.41
% 0.33/1.41 cnf('1',plain,[min(19 ^ [], 17 ^ [], 18 ^ [])],start(3)).
% 0.33/1.41 cnf('1.1',plain,[-(min(19 ^ [], 17 ^ [], 18 ^ [])), member(19 ^ [], 18 ^ []), -(apply(17 ^ [], 14 ^ [19 ^ [], 18 ^ [], 17 ^ []], 19 ^ []))],extension(10,bind([[_31282, _31207, _31356], [18 ^ [], 17 ^ [], 19 ^ []]]))).
% 0.33/1.41 cnf('1.1.1',plain,[-(member(19 ^ [], 18 ^ [])), member(19 ^ [], 18 ^ []), 19 ^ [] = 19 ^ [], 18 ^ [] = 18 ^ []],extension(5,bind([[_20533, _20600, _20666, _20731], [19 ^ [], 19 ^ [], 18 ^ [], 18 ^ []]]))).
% 0.33/1.41 cnf('1.1.1.1',plain,[-(member(19 ^ [], 18 ^ [])), least(19 ^ [], 17 ^ [], 18 ^ [])],extension(7,bind([[_29806, _29669, _29738], [19 ^ [], 17 ^ [], 18 ^ []]]))).
% 0.33/1.41 cnf('1.1.1.1.1',plain,[-(least(19 ^ [], 17 ^ [], 18 ^ []))],extension(2)).
% 0.33/1.41 cnf('1.1.1.2',plain,[-(19 ^ [] = 19 ^ [])],extension(4,bind([[_11512], [19 ^ []]]))).
% 0.33/1.41 cnf('1.1.1.3',plain,[-(18 ^ [] = 18 ^ [])],extension(4,bind([[_11512], [18 ^ []]]))).
% 0.33/1.41 cnf('1.1.2',plain,[apply(17 ^ [], 14 ^ [19 ^ [], 18 ^ [], 17 ^ []], 19 ^ []), order(17 ^ [], 18 ^ []), member(14 ^ [19 ^ [], 18 ^ [], 17 ^ []], 18 ^ []), member(19 ^ [], 18 ^ []), -(19 ^ [] = 14 ^ [19 ^ [], 18 ^ [], 17 ^ []]), apply(17 ^ [], 19 ^ [], 14 ^ [19 ^ [], 18 ^ [], 17 ^ []])],extension(6,bind([[_24799, _24646, _25249, _25322], [18 ^ [], 17 ^ [], 19 ^ [], 14 ^ [19 ^ [], 18 ^ [], 17 ^ []]]]))).
% 0.33/1.41 cnf('1.1.2.1',plain,[-(order(17 ^ [], 18 ^ []))],extension(1)).
% 0.33/1.41 cnf('1.1.2.2',plain,[-(member(14 ^ [19 ^ [], 18 ^ [], 17 ^ []], 18 ^ [])), -(min(19 ^ [], 17 ^ [], 18 ^ [])), member(19 ^ [], 18 ^ [])],extension(9,bind([[_31207, _31356, _31282], [17 ^ [], 19 ^ [], 18 ^ []]]))).
% 0.33/1.41 cnf('1.1.2.2.1',plain,[min(19 ^ [], 17 ^ [], 18 ^ [])],extension(3)).
% 0.33/1.41 cnf('1.1.2.2.2',plain,[-(member(19 ^ [], 18 ^ []))],lemmata('1.1')).
% 0.33/1.41 cnf('1.1.2.3',plain,[-(member(19 ^ [], 18 ^ []))],lemmata('1.1')).
% 0.33/1.41 cnf('1.1.2.4',plain,[19 ^ [] = 14 ^ [19 ^ [], 18 ^ [], 17 ^ []], -(min(19 ^ [], 17 ^ [], 18 ^ [])), member(19 ^ [], 18 ^ [])],extension(11,bind([[_31207, _31356, _31282], [17 ^ [], 19 ^ [], 18 ^ []]]))).
% 0.33/1.41 cnf('1.1.2.4.1',plain,[min(19 ^ [], 17 ^ [], 18 ^ [])],extension(3)).
% 0.33/1.41 cnf('1.1.2.4.2',plain,[-(member(19 ^ [], 18 ^ []))],lemmata('1.1.2')).
% 0.33/1.41 cnf('1.1.2.5',plain,[-(apply(17 ^ [], 19 ^ [], 14 ^ [19 ^ [], 18 ^ [], 17 ^ []])), least(19 ^ [], 17 ^ [], 18 ^ []), member(14 ^ [19 ^ [], 18 ^ [], 17 ^ []], 18 ^ [])],extension(8,bind([[_29806, _29669, _30031, _29738], [19 ^ [], 17 ^ [], 14 ^ [19 ^ [], 18 ^ [], 17 ^ []], 18 ^ []]]))).
% 0.33/1.41 cnf('1.1.2.5.1',plain,[-(least(19 ^ [], 17 ^ [], 18 ^ []))],extension(2)).
% 0.33/1.41 cnf('1.1.2.5.2',plain,[-(member(14 ^ [19 ^ [], 18 ^ [], 17 ^ []], 18 ^ []))],lemmata('1.1.2')).
% 0.33/1.41 %-----------------------------------------------------
% 0.33/1.41
% 0.33/1.41 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------