%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET800+4 : 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 : Tue Jul 19 02:56:03 EDT 2022
% Result : Theorem 29.79s 29.36s
% Output : Proof 29.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SET800+4 : TPTP v8.1.0. Released v3.2.0.
% 0.00/0.12 % Command : leancop_casc.sh %s %d
% 0.11/0.32 % Computer : n009.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 600
% 0.11/0.32 % DateTime : Sat Jul 9 23:20:52 EDT 2022
% 0.11/0.33 % CPUTime :
% 29.79/29.36 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.79/29.36 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.79/29.37
% 29.79/29.37 %-----------------------------------------------------
% 29.79/29.37 fof(greatest_lower_bound, axiom, ! [_75915, _75918, _75921, _75924] : (greatest_lower_bound(_75915, _75918, _75921, _75924) <=> member(_75915, _75918) & lower_bound(_75915, _75921, _75918) & ! [_75971] : (member(_75971, _75924) & lower_bound(_75971, _75921, _75918) => apply(_75921, _75971, _75915))), file('/export/starexec/sandbox2/benchmark/Axioms/SET006+3.ax', greatest_lower_bound)).
% 29.79/29.37 fof(thIV12, conjecture, ! [_76340, _76343] : (order(_76340, _76343) => ! [_76361, _76364] : (subset(_76361, _76343) & subset(_76364, _76343) & subset(_76361, _76364) => ! [_76402, _76405] : (greatest_lower_bound(_76402, _76361, _76340, _76343) & greatest_lower_bound(_76405, _76364, _76340, _76343) => apply(_76340, _76405, _76402)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thIV12)).
% 29.79/29.37 fof(subset, axiom, ! [_76805, _76808] : (subset(_76805, _76808) <=> ! [_76826] : (member(_76826, _76805) => member(_76826, _76808))), file('/export/starexec/sandbox2/benchmark/Axioms/SET006+0.ax', subset)).
% 29.79/29.37 fof(lower_bound, axiom, ! [_77035, _77038, _77041] : (lower_bound(_77041, _77035, _77038) <=> ! [_77062] : (member(_77062, _77038) => apply(_77035, _77041, _77062))), file('/export/starexec/sandbox2/benchmark/Axioms/SET006+3.ax', lower_bound)).
% 29.79/29.37
% 29.79/29.37 cnf(1, plain, [-(45 ^ [_48954, _48867, _48779, _48690]), -(lower_bound(_48690, _48867, _48779))], clausify(greatest_lower_bound)).
% 29.79/29.37 cnf(2, plain, [-(45 ^ [_48954, _48867, _48779, _48690]), -(member(_48690, _48779))], clausify(greatest_lower_bound)).
% 29.79/29.37 cnf(3, plain, [-(subset(50 ^ [], 51 ^ []))], clausify(thIV12)).
% 29.79/29.37 cnf(4, plain, [-(greatest_lower_bound(52 ^ [], 50 ^ [], 48 ^ [], 49 ^ []))], clausify(thIV12)).
% 29.79/29.37 cnf(5, plain, [-(greatest_lower_bound(53 ^ [], 51 ^ [], 48 ^ [], 49 ^ []))], clausify(thIV12)).
% 29.79/29.37 cnf(6, plain, [apply(48 ^ [], 53 ^ [], 52 ^ [])], clausify(thIV12)).
% 29.79/29.37 cnf(7, plain, [subset(_35283, _35339), member(_35453, _35283), -(member(_35453, _35339))], clausify(subset)).
% 29.79/29.37 cnf(8, plain, [lower_bound(_43969, _43844, _43907), member(_44129, _43907), -(apply(_43844, _43969, _44129))], clausify(lower_bound)).
% 29.79/29.37 cnf(9, plain, [greatest_lower_bound(_48690, _48779, _48867, _48954), 45 ^ [_48954, _48867, _48779, _48690]], clausify(greatest_lower_bound)).
% 29.79/29.37
% 29.79/29.37 cnf('1',plain,[-(subset(50 ^ [], 51 ^ []))],start(3)).
% 29.79/29.37 cnf('1.1',plain,[subset(50 ^ [], 51 ^ []), member(52 ^ [], 50 ^ []), -(member(52 ^ [], 51 ^ []))],extension(7,bind([[_35283, _35453, _35339], [50 ^ [], 52 ^ [], 51 ^ []]]))).
% 29.79/29.37 cnf('1.1.1',plain,[-(member(52 ^ [], 50 ^ [])), -(45 ^ [49 ^ [], 48 ^ [], 50 ^ [], 52 ^ []])],extension(2,bind([[_48954, _48867, _48779, _48690], [49 ^ [], 48 ^ [], 50 ^ [], 52 ^ []]]))).
% 29.79/29.37 cnf('1.1.1.1',plain,[45 ^ [49 ^ [], 48 ^ [], 50 ^ [], 52 ^ []], greatest_lower_bound(52 ^ [], 50 ^ [], 48 ^ [], 49 ^ [])],extension(9,bind([[_48690, _48779, _48867, _48954], [52 ^ [], 50 ^ [], 48 ^ [], 49 ^ []]]))).
% 29.79/29.37 cnf('1.1.1.1.1',plain,[-(greatest_lower_bound(52 ^ [], 50 ^ [], 48 ^ [], 49 ^ []))],extension(4)).
% 29.79/29.37 cnf('1.1.2',plain,[member(52 ^ [], 51 ^ []), lower_bound(53 ^ [], 48 ^ [], 51 ^ []), -(apply(48 ^ [], 53 ^ [], 52 ^ []))],extension(8,bind([[_43907, _43844, _43969, _44129], [51 ^ [], 48 ^ [], 53 ^ [], 52 ^ []]]))).
% 29.79/29.37 cnf('1.1.2.1',plain,[-(lower_bound(53 ^ [], 48 ^ [], 51 ^ [])), -(45 ^ [49 ^ [], 48 ^ [], 51 ^ [], 53 ^ []])],extension(1,bind([[_48954, _48867, _48779, _48690], [49 ^ [], 48 ^ [], 51 ^ [], 53 ^ []]]))).
% 29.79/29.37 cnf('1.1.2.1.1',plain,[45 ^ [49 ^ [], 48 ^ [], 51 ^ [], 53 ^ []], greatest_lower_bound(53 ^ [], 51 ^ [], 48 ^ [], 49 ^ [])],extension(9,bind([[_48690, _48779, _48867, _48954], [53 ^ [], 51 ^ [], 48 ^ [], 49 ^ []]]))).
% 29.79/29.37 cnf('1.1.2.1.1.1',plain,[-(greatest_lower_bound(53 ^ [], 51 ^ [], 48 ^ [], 49 ^ []))],extension(5)).
% 29.79/29.37 cnf('1.1.2.2',plain,[apply(48 ^ [], 53 ^ [], 52 ^ [])],extension(6)).
% 29.79/29.37 %-----------------------------------------------------
% 29.79/29.38
% 29.79/29.38 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------