%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET805+4 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n027.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:05 EDT 2022
% Result : Theorem 31.98s 31.51s
% Output : Proof 31.98s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SET805+4 : TPTP v8.1.0. Released v3.2.0.
% 0.06/0.12 % Command : leancop_casc.sh %s %d
% 0.13/0.33 % Computer : n027.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Sat Jul 9 23:53:17 EDT 2022
% 0.13/0.34 % CPUTime :
% 31.98/31.51 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 31.98/31.52 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 31.98/31.52
% 31.98/31.52 %-----------------------------------------------------
% 31.98/31.52 fof(order, axiom, ! [_88437, _88440] : (order(_88437, _88440) <=> ! [_88458] : (member(_88458, _88440) => apply(_88437, _88458, _88458)) & ! [_88458, _88491] : (member(_88458, _88440) & member(_88491, _88440) => apply(_88437, _88458, _88491) & apply(_88437, _88491, _88458) => _88458 = _88491) & ! [_88458, _88491, _88555] : (member(_88458, _88440) & member(_88491, _88440) & member(_88555, _88440) => apply(_88437, _88458, _88491) & apply(_88437, _88491, _88555) => apply(_88437, _88458, _88555))), file('/export/starexec/sandbox2/benchmark/Axioms/SET006+3.ax', order)).
% 31.98/31.52 fof(thIV17, conjecture, ! [_89258, _89261] : (order(_89258, _89261) => ! [_89279] : (subset(_89279, _89261) => order(_89258, _89279))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thIV17)).
% 31.98/31.52 fof(subset, axiom, ! [_89512, _89515] : (subset(_89512, _89515) <=> ! [_89533] : (member(_89533, _89512) => member(_89533, _89515))), file('/export/starexec/sandbox2/benchmark/Axioms/SET006+0.ax', subset)).
% 31.98/31.52
% 31.98/31.52 cnf(1, plain, [-(21 ^ [_39842, _39689]), apply(_39689, 18 ^ [_39842, _39689], 20 ^ [_39842, _39689])], clausify(order)).
% 31.98/31.52 cnf(2, plain, [-(21 ^ [_39842, _39689]), -(apply(_39689, 19 ^ [_39842, _39689], 20 ^ [_39842, _39689]))], clausify(order)).
% 31.98/31.52 cnf(3, plain, [-(21 ^ [_39842, _39689]), -(apply(_39689, 18 ^ [_39842, _39689], 19 ^ [_39842, _39689]))], clausify(order)).
% 31.98/31.52 cnf(4, plain, [-(21 ^ [_39842, _39689]), -(member(20 ^ [_39842, _39689], _39842))], clausify(order)).
% 31.98/31.52 cnf(5, plain, [-(21 ^ [_39842, _39689]), -(member(19 ^ [_39842, _39689], _39842))], clausify(order)).
% 31.98/31.52 cnf(6, plain, [-(21 ^ [_39842, _39689]), -(member(18 ^ [_39842, _39689], _39842))], clausify(order)).
% 31.98/31.52 cnf(7, plain, [-(17 ^ [_39842, _39689]), 15 ^ [_39842, _39689] = 16 ^ [_39842, _39689]], clausify(order)).
% 31.98/31.52 cnf(8, plain, [-(17 ^ [_39842, _39689]), -(apply(_39689, 16 ^ [_39842, _39689], 15 ^ [_39842, _39689]))], clausify(order)).
% 31.98/31.52 cnf(9, plain, [-(17 ^ [_39842, _39689]), -(apply(_39689, 15 ^ [_39842, _39689], 16 ^ [_39842, _39689]))], clausify(order)).
% 31.98/31.52 cnf(10, plain, [-(17 ^ [_39842, _39689]), -(member(16 ^ [_39842, _39689], _39842))], clausify(order)).
% 31.98/31.52 cnf(11, plain, [-(17 ^ [_39842, _39689]), -(member(15 ^ [_39842, _39689], _39842))], clausify(order)).
% 31.98/31.52 cnf(12, plain, [-(14 ^ [_39842, _39689]), apply(_39689, 13 ^ [_39842, _39689], 13 ^ [_39842, _39689])], clausify(order)).
% 31.98/31.52 cnf(13, plain, [-(14 ^ [_39842, _39689]), -(member(13 ^ [_39842, _39689], _39842))], clausify(order)).
% 31.98/31.52 cnf(14, plain, [-(12 ^ [_39842, _39689]), member(_41045, _39842), member(_40961, _39842), member(_40876, _39842), -(apply(_39689, _40876, _41045)), apply(_39689, _40876, _40961), apply(_39689, _40961, _41045)], clausify(order)).
% 31.98/31.52 cnf(15, plain, [-(12 ^ [_39842, _39689]), member(_40365, _39842), member(_40292, _39842), -(_40292 = _40365), apply(_39689, _40292, _40365), apply(_39689, _40365, _40292)], clausify(order)).
% 31.98/31.52 cnf(16, plain, [-(12 ^ [_39842, _39689]), member(_40063, _39842), -(apply(_39689, _40063, _40063))], clausify(order)).
% 31.98/31.52 cnf(17, plain, [-(order(48 ^ [], 49 ^ []))], clausify(thIV17)).
% 31.98/31.52 cnf(18, plain, [-(subset(50 ^ [], 49 ^ []))], clausify(thIV17)).
% 31.98/31.52 cnf(19, plain, [order(48 ^ [], 50 ^ [])], clausify(thIV17)).
% 31.98/31.52 cnf(20, plain, [subset(_34803, _34859), member(_34973, _34803), -(member(_34973, _34859))], clausify(subset)).
% 31.98/31.52 cnf(21, plain, [-(order(_39689, _39842)), 14 ^ [_39842, _39689], 17 ^ [_39842, _39689], 21 ^ [_39842, _39689]], clausify(order)).
% 31.98/31.52 cnf(22, plain, [order(_39689, _39842), 12 ^ [_39842, _39689]], clausify(order)).
% 31.98/31.52
% 31.98/31.52 cnf('1',plain,[order(48 ^ [], 50 ^ [])],start(19)).
% 31.98/31.52 cnf('1.1',plain,[-(order(48 ^ [], 50 ^ [])), 14 ^ [50 ^ [], 48 ^ []], 17 ^ [50 ^ [], 48 ^ []], 21 ^ [50 ^ [], 48 ^ []]],extension(21,bind([[_39842, _39689], [50 ^ [], 48 ^ []]]))).
% 31.98/31.52 cnf('1.1.1',plain,[-(14 ^ [50 ^ [], 48 ^ []]), apply(48 ^ [], 13 ^ [50 ^ [], 48 ^ []], 13 ^ [50 ^ [], 48 ^ []])],extension(12,bind([[_39842, _39689], [50 ^ [], 48 ^ []]]))).
% 31.98/31.52 cnf('1.1.1.1',plain,[-(apply(48 ^ [], 13 ^ [50 ^ [], 48 ^ []], 13 ^ [50 ^ [], 48 ^ []])), -(12 ^ [49 ^ [], 48 ^ []]), member(13 ^ [50 ^ [], 48 ^ []], 49 ^ [])],extension(16,bind([[_39689, _40063, _39842], [48 ^ [], 13 ^ [50 ^ [], 48 ^ []], 49 ^ []]]))).
% 31.98/31.52 cnf('1.1.1.1.1',plain,[12 ^ [49 ^ [], 48 ^ []], order(48 ^ [], 49 ^ [])],extension(22,bind([[_39689, _39842], [48 ^ [], 49 ^ []]]))).
% 31.98/31.52 cnf('1.1.1.1.1.1',plain,[-(order(48 ^ [], 49 ^ []))],extension(17)).
% 31.98/31.52 cnf('1.1.1.1.2',plain,[-(member(13 ^ [50 ^ [], 48 ^ []], 49 ^ [])), subset(50 ^ [], 49 ^ []), member(13 ^ [50 ^ [], 48 ^ []], 50 ^ [])],extension(20,bind([[_34859, _34973, _34803], [49 ^ [], 13 ^ [50 ^ [], 48 ^ []], 50 ^ []]]))).
% 31.98/31.52 cnf('1.1.1.1.2.1',plain,[-(subset(50 ^ [], 49 ^ []))],extension(18)).
% 31.98/31.52 cnf('1.1.1.1.2.2',plain,[-(member(13 ^ [50 ^ [], 48 ^ []], 50 ^ [])), -(14 ^ [50 ^ [], 48 ^ []])],extension(13,bind([[_39842, _39689], [50 ^ [], 48 ^ []]]))).
% 31.98/31.52 cnf('1.1.1.1.2.2.1',plain,[14 ^ [50 ^ [], 48 ^ []]],reduction('1.1')).
% 31.98/31.52 cnf('1.1.2',plain,[-(17 ^ [50 ^ [], 48 ^ []]), 15 ^ [50 ^ [], 48 ^ []] = 16 ^ [50 ^ [], 48 ^ []]],extension(7,bind([[_39842, _39689], [50 ^ [], 48 ^ []]]))).
% 31.98/31.52 cnf('1.1.2.1',plain,[-(15 ^ [50 ^ [], 48 ^ []] = 16 ^ [50 ^ [], 48 ^ []]), -(12 ^ [49 ^ [], 48 ^ []]), member(16 ^ [50 ^ [], 48 ^ []], 49 ^ []), member(15 ^ [50 ^ [], 48 ^ []], 49 ^ []), apply(48 ^ [], 15 ^ [50 ^ [], 48 ^ []], 16 ^ [50 ^ [], 48 ^ []]), apply(48 ^ [], 16 ^ [50 ^ [], 48 ^ []], 15 ^ [50 ^ [], 48 ^ []])],extension(15,bind([[_39842, _39689, _40365, _40292], [49 ^ [], 48 ^ [], 16 ^ [50 ^ [], 48 ^ []], 15 ^ [50 ^ [], 48 ^ []]]]))).
% 31.98/31.52 cnf('1.1.2.1.1',plain,[12 ^ [49 ^ [], 48 ^ []], order(48 ^ [], 49 ^ [])],extension(22,bind([[_39689, _39842], [48 ^ [], 49 ^ []]]))).
% 31.98/31.52 cnf('1.1.2.1.1.1',plain,[-(order(48 ^ [], 49 ^ []))],extension(17)).
% 31.98/31.52 cnf('1.1.2.1.2',plain,[-(member(16 ^ [50 ^ [], 48 ^ []], 49 ^ [])), subset(50 ^ [], 49 ^ []), member(16 ^ [50 ^ [], 48 ^ []], 50 ^ [])],extension(20,bind([[_34859, _34973, _34803], [49 ^ [], 16 ^ [50 ^ [], 48 ^ []], 50 ^ []]]))).
% 31.98/31.52 cnf('1.1.2.1.2.1',plain,[-(subset(50 ^ [], 49 ^ []))],extension(18)).
% 31.98/31.52 cnf('1.1.2.1.2.2',plain,[-(member(16 ^ [50 ^ [], 48 ^ []], 50 ^ [])), -(17 ^ [50 ^ [], 48 ^ []])],extension(10,bind([[_39842, _39689], [50 ^ [], 48 ^ []]]))).
% 31.98/31.52 cnf('1.1.2.1.2.2.1',plain,[17 ^ [50 ^ [], 48 ^ []]],reduction('1.1')).
% 31.98/31.52 cnf('1.1.2.1.3',plain,[-(member(15 ^ [50 ^ [], 48 ^ []], 49 ^ [])), subset(50 ^ [], 49 ^ []), member(15 ^ [50 ^ [], 48 ^ []], 50 ^ [])],extension(20,bind([[_34859, _34973, _34803], [49 ^ [], 15 ^ [50 ^ [], 48 ^ []], 50 ^ []]]))).
% 31.98/31.52 cnf('1.1.2.1.3.1',plain,[-(subset(50 ^ [], 49 ^ []))],extension(18)).
% 31.98/31.52 cnf('1.1.2.1.3.2',plain,[-(member(15 ^ [50 ^ [], 48 ^ []], 50 ^ [])), -(17 ^ [50 ^ [], 48 ^ []])],extension(11,bind([[_39842, _39689], [50 ^ [], 48 ^ []]]))).
% 31.98/31.52 cnf('1.1.2.1.3.2.1',plain,[17 ^ [50 ^ [], 48 ^ []]],reduction('1.1')).
% 31.98/31.52 cnf('1.1.2.1.4',plain,[-(apply(48 ^ [], 15 ^ [50 ^ [], 48 ^ []], 16 ^ [50 ^ [], 48 ^ []])), -(17 ^ [50 ^ [], 48 ^ []])],extension(9,bind([[_39842, _39689], [50 ^ [], 48 ^ []]]))).
% 31.98/31.52 cnf('1.1.2.1.4.1',plain,[17 ^ [50 ^ [], 48 ^ []]],reduction('1.1')).
% 31.98/31.52 cnf('1.1.2.1.5',plain,[-(apply(48 ^ [], 16 ^ [50 ^ [], 48 ^ []], 15 ^ [50 ^ [], 48 ^ []])), -(17 ^ [50 ^ [], 48 ^ []])],extension(8,bind([[_39842, _39689], [50 ^ [], 48 ^ []]]))).
% 31.98/31.52 cnf('1.1.2.1.5.1',plain,[17 ^ [50 ^ [], 48 ^ []]],reduction('1.1')).
% 31.98/31.52 cnf('1.1.3',plain,[-(21 ^ [50 ^ [], 48 ^ []]), -(apply(48 ^ [], 18 ^ [50 ^ [], 48 ^ []], 19 ^ [50 ^ [], 48 ^ []]))],extension(3,bind([[_39842, _39689], [50 ^ [], 48 ^ []]]))).
% 31.98/31.52 cnf('1.1.3.1',plain,[apply(48 ^ [], 18 ^ [50 ^ [], 48 ^ []], 19 ^ [50 ^ [], 48 ^ []]), -(12 ^ [49 ^ [], 48 ^ []]), member(20 ^ [50 ^ [], 48 ^ []], 49 ^ []), member(19 ^ [50 ^ [], 48 ^ []], 49 ^ []), member(18 ^ [50 ^ [], 48 ^ []], 49 ^ []), -(apply(48 ^ [], 18 ^ [50 ^ [], 48 ^ []], 20 ^ [50 ^ [], 48 ^ []])), apply(48 ^ [], 19 ^ [50 ^ [], 48 ^ []], 20 ^ [50 ^ [], 48 ^ []])],extension(14,bind([[_39842, _40876, _39689, _40961, _41045], [49 ^ [], 18 ^ [50 ^ [], 48 ^ []], 48 ^ [], 19 ^ [50 ^ [], 48 ^ []], 20 ^ [50 ^ [], 48 ^ []]]]))).
% 31.98/31.52 cnf('1.1.3.1.1',plain,[12 ^ [49 ^ [], 48 ^ []], order(48 ^ [], 49 ^ [])],extension(22,bind([[_39689, _39842], [48 ^ [], 49 ^ []]]))).
% 31.98/31.52 cnf('1.1.3.1.1.1',plain,[-(order(48 ^ [], 49 ^ []))],extension(17)).
% 31.98/31.52 cnf('1.1.3.1.2',plain,[-(member(20 ^ [50 ^ [], 48 ^ []], 49 ^ [])), subset(50 ^ [], 49 ^ []), member(20 ^ [50 ^ [], 48 ^ []], 50 ^ [])],extension(20,bind([[_34859, _34973, _34803], [49 ^ [], 20 ^ [50 ^ [], 48 ^ []], 50 ^ []]]))).
% 31.98/31.52 cnf('1.1.3.1.2.1',plain,[-(subset(50 ^ [], 49 ^ []))],extension(18)).
% 31.98/31.52 cnf('1.1.3.1.2.2',plain,[-(member(20 ^ [50 ^ [], 48 ^ []], 50 ^ [])), -(21 ^ [50 ^ [], 48 ^ []])],extension(4,bind([[_39842, _39689], [50 ^ [], 48 ^ []]]))).
% 31.98/31.52 cnf('1.1.3.1.2.2.1',plain,[21 ^ [50 ^ [], 48 ^ []]],reduction('1.1')).
% 31.98/31.52 cnf('1.1.3.1.3',plain,[-(member(19 ^ [50 ^ [], 48 ^ []], 49 ^ [])), subset(50 ^ [], 49 ^ []), member(19 ^ [50 ^ [], 48 ^ []], 50 ^ [])],extension(20,bind([[_34859, _34973, _34803], [49 ^ [], 19 ^ [50 ^ [], 48 ^ []], 50 ^ []]]))).
% 31.98/31.52 cnf('1.1.3.1.3.1',plain,[-(subset(50 ^ [], 49 ^ []))],extension(18)).
% 31.98/31.52 cnf('1.1.3.1.3.2',plain,[-(member(19 ^ [50 ^ [], 48 ^ []], 50 ^ [])), -(21 ^ [50 ^ [], 48 ^ []])],extension(5,bind([[_39842, _39689], [50 ^ [], 48 ^ []]]))).
% 31.98/31.52 cnf('1.1.3.1.3.2.1',plain,[21 ^ [50 ^ [], 48 ^ []]],reduction('1.1')).
% 31.98/31.52 cnf('1.1.3.1.4',plain,[-(member(18 ^ [50 ^ [], 48 ^ []], 49 ^ [])), subset(50 ^ [], 49 ^ []), member(18 ^ [50 ^ [], 48 ^ []], 50 ^ [])],extension(20,bind([[_34859, _34973, _34803], [49 ^ [], 18 ^ [50 ^ [], 48 ^ []], 50 ^ []]]))).
% 31.98/31.52 cnf('1.1.3.1.4.1',plain,[-(subset(50 ^ [], 49 ^ []))],extension(18)).
% 31.98/31.52 cnf('1.1.3.1.4.2',plain,[-(member(18 ^ [50 ^ [], 48 ^ []], 50 ^ [])), -(21 ^ [50 ^ [], 48 ^ []])],extension(6,bind([[_39842, _39689], [50 ^ [], 48 ^ []]]))).
% 31.98/31.52 cnf('1.1.3.1.4.2.1',plain,[21 ^ [50 ^ [], 48 ^ []]],reduction('1.1')).
% 31.98/31.52 cnf('1.1.3.1.5',plain,[apply(48 ^ [], 18 ^ [50 ^ [], 48 ^ []], 20 ^ [50 ^ [], 48 ^ []]), -(21 ^ [50 ^ [], 48 ^ []])],extension(1,bind([[_39842, _39689], [50 ^ [], 48 ^ []]]))).
% 31.98/31.52 cnf('1.1.3.1.5.1',plain,[21 ^ [50 ^ [], 48 ^ []]],reduction('1.1')).
% 31.98/31.52 cnf('1.1.3.1.6',plain,[-(apply(48 ^ [], 19 ^ [50 ^ [], 48 ^ []], 20 ^ [50 ^ [], 48 ^ []])), -(21 ^ [50 ^ [], 48 ^ []])],extension(2,bind([[_39842, _39689], [50 ^ [], 48 ^ []]]))).
% 31.98/31.52 cnf('1.1.3.1.6.1',plain,[21 ^ [50 ^ [], 48 ^ []]],reduction('1.1')).
% 31.98/31.52 %-----------------------------------------------------
% 31.98/31.53
% 31.98/31.53 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------