%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET809+4 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n015.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:06 EDT 2022
% Result : Theorem 0.38s 1.40s
% Output : Proof 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET809+4 : TPTP v8.1.0. Released v3.2.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n015.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Sun Jul 10 22:45:23 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.38/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/1.40 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/1.41
% 0.38/1.41 %-----------------------------------------------------
% 0.38/1.41 fof(thV2, conjecture, ! [_54999] : (member(_54999, on) => ~ member(_54999, _54999)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', thV2)).
% 0.38/1.41 fof(ordinal_number, axiom, ! [_55203] : (member(_55203, on) <=> set(_55203) & strict_well_order(member_predicate, _55203) & ! [_55238] : (member(_55238, _55203) => subset(_55238, _55203))), file('/export/starexec/sandbox/benchmark/Axioms/SET006+4.ax', ordinal_number)).
% 0.38/1.41 fof(strict_well_order, axiom, ! [_55451, _55454] : (strict_well_order(_55451, _55454) <=> strict_order(_55451, _55454) & ! [_55482] : (subset(_55482, _55454) & ? [_55500] : member(_55500, _55482) => ? [_55518] : least(_55518, _55451, _55482))), file('/export/starexec/sandbox/benchmark/Axioms/SET006+4.ax', strict_well_order)).
% 0.38/1.41 fof(rel_member, axiom, ! [_55785, _55788] : (apply(member_predicate, _55785, _55788) <=> member(_55785, _55788)), file('/export/starexec/sandbox/benchmark/Axioms/SET006+4.ax', rel_member)).
% 0.38/1.41 fof(strict_order, axiom, ! [_55968, _55971] : (strict_order(_55968, _55971) <=> ! [_55989, _55992] : (member(_55989, _55971) & member(_55992, _55971) => ~ (apply(_55968, _55989, _55992) & apply(_55968, _55992, _55989))) & ! [_55989, _55992, _56052] : (member(_55989, _55971) & member(_55992, _55971) & member(_56052, _55971) => apply(_55968, _55989, _55992) & apply(_55968, _55992, _56052) => apply(_55968, _55989, _56052))), file('/export/starexec/sandbox/benchmark/Axioms/SET006+4.ax', strict_order)).
% 0.38/1.41
% 0.38/1.41 cnf(1, plain, [-(member(14 ^ [], on))], clausify(thV2)).
% 0.38/1.41 cnf(2, plain, [-(member(14 ^ [], 14 ^ []))], clausify(thV2)).
% 0.38/1.41 cnf(3, plain, [member(_29891, on), -(strict_well_order(member_predicate, _29891))], clausify(ordinal_number)).
% 0.38/1.41 cnf(4, plain, [strict_well_order(_30419, _30498), -(strict_order(_30419, _30498))], clausify(strict_well_order)).
% 0.38/1.41 cnf(5, plain, [-(apply(member_predicate, _32058, _32104)), member(_32058, _32104)], clausify(rel_member)).
% 0.38/1.41 cnf(6, plain, [strict_order(_32410, _32541), member(_32809, _32541), member(_32740, _32541), apply(_32410, _32740, _32809), apply(_32410, _32809, _32740)], clausify(strict_order)).
% 0.38/1.41
% 0.38/1.41 cnf('1',plain,[strict_order(member_predicate, 14 ^ []), member(14 ^ [], 14 ^ []), member(14 ^ [], 14 ^ []), apply(member_predicate, 14 ^ [], 14 ^ []), apply(member_predicate, 14 ^ [], 14 ^ [])],start(6,bind([[_32541, _32410, _32809, _32740], [14 ^ [], member_predicate, 14 ^ [], 14 ^ []]]))).
% 0.38/1.41 cnf('1.1',plain,[-(strict_order(member_predicate, 14 ^ [])), strict_well_order(member_predicate, 14 ^ [])],extension(4,bind([[_30419, _30498], [member_predicate, 14 ^ []]]))).
% 0.38/1.41 cnf('1.1.1',plain,[-(strict_well_order(member_predicate, 14 ^ [])), member(14 ^ [], on)],extension(3,bind([[_29891], [14 ^ []]]))).
% 0.38/1.41 cnf('1.1.1.1',plain,[-(member(14 ^ [], on))],extension(1)).
% 0.38/1.41 cnf('1.2',plain,[-(member(14 ^ [], 14 ^ []))],extension(2)).
% 0.38/1.41 cnf('1.3',plain,[-(member(14 ^ [], 14 ^ []))],extension(2)).
% 0.38/1.41 cnf('1.4',plain,[-(apply(member_predicate, 14 ^ [], 14 ^ [])), member(14 ^ [], 14 ^ [])],extension(5,bind([[_32058, _32104], [14 ^ [], 14 ^ []]]))).
% 0.38/1.41 cnf('1.4.1',plain,[-(member(14 ^ [], 14 ^ []))],extension(2)).
% 0.38/1.41 cnf('1.5',plain,[-(apply(member_predicate, 14 ^ [], 14 ^ []))],lemmata('1')).
% 0.38/1.41 %-----------------------------------------------------
% 0.38/1.41
% 0.38/1.41 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------