%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET579+3 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n018.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:54:20 EDT 2022
% Result : Theorem 0.36s 1.40s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SET579+3 : TPTP v8.1.0. Released v2.2.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.13/0.33 % Computer : n018.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 : Mon Jul 11 04:39:43 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.36/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/1.40 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/1.41
% 0.36/1.41 %-----------------------------------------------------
% 0.36/1.41 fof(prove_th20, conjecture, ! [_19224, _19227, _19230] : (! [_19238] : (member(_19238, _19224) <=> member(_19238, _19227) & ~ member(_19238, _19230)) => _19224 = difference(_19227, _19230)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_th20)).
% 0.36/1.41 fof(difference_defn, axiom, ! [_19530, _19533, _19536] : (member(_19536, difference(_19530, _19533)) <=> member(_19536, _19530) & ~ member(_19536, _19533)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', difference_defn)).
% 0.36/1.41 fof(equal_defn, axiom, ! [_19764, _19767] : (_19764 = _19767 <=> subset(_19764, _19767) & subset(_19767, _19764)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', equal_defn)).
% 0.36/1.41 fof(subset_defn, axiom, ! [_19935, _19938] : (subset(_19935, _19938) <=> ! [_19956] : (member(_19956, _19935) => member(_19956, _19938))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', subset_defn)).
% 0.36/1.41
% 0.36/1.41 cnf(1, plain, [-(5 ^ [_11296]), member(_11296, 4 ^ [])], clausify(prove_th20)).
% 0.36/1.41 cnf(2, plain, [-(5 ^ [_11296]), -(member(_11296, 3 ^ []))], clausify(prove_th20)).
% 0.36/1.41 cnf(3, plain, [2 ^ [] = difference(3 ^ [], 4 ^ [])], clausify(prove_th20)).
% 0.36/1.41 cnf(4, plain, [member(_11296, 2 ^ []), 5 ^ [_11296]], clausify(prove_th20)).
% 0.36/1.41 cnf(5, plain, [-(member(_11296, 2 ^ [])), member(_11296, 3 ^ []), -(member(_11296, 4 ^ []))], clausify(prove_th20)).
% 0.36/1.41 cnf(6, plain, [member(_7689, difference(_7568, _7629)), -(member(_7689, _7568))], clausify(difference_defn)).
% 0.36/1.41 cnf(7, plain, [member(_7689, difference(_7568, _7629)), member(_7689, _7629)], clausify(difference_defn)).
% 0.36/1.41 cnf(8, plain, [-(member(_7689, difference(_7568, _7629))), member(_7689, _7568), -(member(_7689, _7629))], clausify(difference_defn)).
% 0.36/1.41 cnf(9, plain, [-(_8103 = _8154), subset(_8103, _8154), subset(_8154, _8103)], clausify(equal_defn)).
% 0.36/1.41 cnf(10, plain, [-(subset(_8499, _8555)), -(member(1 ^ [_8555, _8499], _8499))], clausify(subset_defn)).
% 0.36/1.41 cnf(11, plain, [-(subset(_8499, _8555)), member(1 ^ [_8555, _8499], _8555)], clausify(subset_defn)).
% 0.36/1.41
% 0.36/1.41 cnf('1',plain,[2 ^ [] = difference(3 ^ [], 4 ^ [])],start(3)).
% 0.36/1.41 cnf('1.1',plain,[-(2 ^ [] = difference(3 ^ [], 4 ^ [])), subset(2 ^ [], difference(3 ^ [], 4 ^ [])), subset(difference(3 ^ [], 4 ^ []), 2 ^ [])],extension(9,bind([[_8154, _8103], [difference(3 ^ [], 4 ^ []), 2 ^ []]]))).
% 0.36/1.41 cnf('1.1.1',plain,[-(subset(2 ^ [], difference(3 ^ [], 4 ^ []))), member(1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []], difference(3 ^ [], 4 ^ []))],extension(11,bind([[_8499, _8555], [2 ^ [], difference(3 ^ [], 4 ^ [])]]))).
% 0.36/1.41 cnf('1.1.1.1',plain,[-(member(1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []], difference(3 ^ [], 4 ^ []))), member(1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []], 3 ^ []), -(member(1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []], 4 ^ []))],extension(8,bind([[_7568, _7689, _7629], [3 ^ [], 1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []], 4 ^ []]]))).
% 0.36/1.41 cnf('1.1.1.1.1',plain,[-(member(1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []], 3 ^ [])), -(5 ^ [1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []]])],extension(2,bind([[_11296], [1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []]]]))).
% 0.36/1.41 cnf('1.1.1.1.1.1',plain,[5 ^ [1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []]], member(1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []], 2 ^ [])],extension(4,bind([[_11296], [1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []]]]))).
% 0.36/1.41 cnf('1.1.1.1.1.1.1',plain,[-(member(1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []], 2 ^ [])), -(subset(2 ^ [], difference(3 ^ [], 4 ^ [])))],extension(10,bind([[_8499, _8555], [2 ^ [], difference(3 ^ [], 4 ^ [])]]))).
% 0.36/1.41 cnf('1.1.1.1.1.1.1.1',plain,[subset(2 ^ [], difference(3 ^ [], 4 ^ []))],reduction('1.1')).
% 0.36/1.41 cnf('1.1.1.1.2',plain,[member(1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []], 4 ^ []), -(5 ^ [1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []]])],extension(1,bind([[_11296], [1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []]]]))).
% 0.36/1.41 cnf('1.1.1.1.2.1',plain,[5 ^ [1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []]], member(1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []], 2 ^ [])],extension(4,bind([[_11296], [1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []]]]))).
% 0.36/1.41 cnf('1.1.1.1.2.1.1',plain,[-(member(1 ^ [difference(3 ^ [], 4 ^ []), 2 ^ []], 2 ^ [])), -(subset(2 ^ [], difference(3 ^ [], 4 ^ [])))],extension(10,bind([[_8499, _8555], [2 ^ [], difference(3 ^ [], 4 ^ [])]]))).
% 0.36/1.41 cnf('1.1.1.1.2.1.1.1',plain,[subset(2 ^ [], difference(3 ^ [], 4 ^ []))],reduction('1.1')).
% 0.36/1.41 cnf('1.1.2',plain,[-(subset(difference(3 ^ [], 4 ^ []), 2 ^ [])), -(member(1 ^ [2 ^ [], difference(3 ^ [], 4 ^ [])], difference(3 ^ [], 4 ^ [])))],extension(10,bind([[_8555, _8499], [2 ^ [], difference(3 ^ [], 4 ^ [])]]))).
% 0.36/1.41 cnf('1.1.2.1',plain,[member(1 ^ [2 ^ [], difference(3 ^ [], 4 ^ [])], difference(3 ^ [], 4 ^ [])), -(member(1 ^ [2 ^ [], difference(3 ^ [], 4 ^ [])], 3 ^ []))],extension(6,bind([[_7629, _7689, _7568], [4 ^ [], 1 ^ [2 ^ [], difference(3 ^ [], 4 ^ [])], 3 ^ []]]))).
% 0.36/1.41 cnf('1.1.2.1.1',plain,[member(1 ^ [2 ^ [], difference(3 ^ [], 4 ^ [])], 3 ^ []), -(member(1 ^ [2 ^ [], difference(3 ^ [], 4 ^ [])], 2 ^ [])), -(member(1 ^ [2 ^ [], difference(3 ^ [], 4 ^ [])], 4 ^ []))],extension(5,bind([[_11296], [1 ^ [2 ^ [], difference(3 ^ [], 4 ^ [])]]]))).
% 0.36/1.41 cnf('1.1.2.1.1.1',plain,[member(1 ^ [2 ^ [], difference(3 ^ [], 4 ^ [])], 2 ^ []), -(subset(difference(3 ^ [], 4 ^ []), 2 ^ []))],extension(11,bind([[_8499, _8555], [difference(3 ^ [], 4 ^ []), 2 ^ []]]))).
% 0.36/1.41 cnf('1.1.2.1.1.1.1',plain,[subset(difference(3 ^ [], 4 ^ []), 2 ^ [])],reduction('1.1')).
% 0.36/1.41 cnf('1.1.2.1.1.2',plain,[member(1 ^ [2 ^ [], difference(3 ^ [], 4 ^ [])], 4 ^ []), member(1 ^ [2 ^ [], difference(3 ^ [], 4 ^ [])], difference(3 ^ [], 4 ^ []))],extension(7,bind([[_7689, _7568, _7629], [1 ^ [2 ^ [], difference(3 ^ [], 4 ^ [])], 3 ^ [], 4 ^ []]]))).
% 0.36/1.41 cnf('1.1.2.1.1.2.1',plain,[-(member(1 ^ [2 ^ [], difference(3 ^ [], 4 ^ [])], difference(3 ^ [], 4 ^ [])))],reduction('1.1.2')).
% 0.36/1.41 %-----------------------------------------------------
% 0.36/1.41
% 0.36/1.42 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------