%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET610+3 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n010.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:43 EDT 2022
% Result : Theorem 0.57s 1.41s
% Output : Proof 0.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SET610+3 : TPTP v8.1.0. Released v2.2.0.
% 0.10/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n010.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Sun Jul 10 15:50:15 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.57/1.41 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.57/1.41 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.57/1.42
% 0.57/1.42 %-----------------------------------------------------
% 0.57/1.42 fof(prove_th83, conjecture, ! [_24546, _24549] : difference(union(_24546, _24549), _24549) = difference(_24546, _24549), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_th83)).
% 0.57/1.42 fof(member_equal, axiom, ! [_24715, _24718] : (! [_24726] : (member(_24726, _24715) <=> member(_24726, _24718)) => _24715 = _24718), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', member_equal)).
% 0.57/1.42 fof(union_defn, axiom, ! [_24927, _24930, _24933] : (member(_24933, union(_24927, _24930)) <=> member(_24933, _24927) | member(_24933, _24930)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', union_defn)).
% 0.57/1.42 fof(difference_defn, axiom, ! [_25141, _25144, _25147] : (member(_25147, difference(_25141, _25144)) <=> member(_25147, _25141) & ~ member(_25147, _25144)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', difference_defn)).
% 0.57/1.42
% 0.57/1.42 cnf(1, plain, [difference(union(4 ^ [], 5 ^ []), 5 ^ []) = difference(4 ^ [], 5 ^ [])], clausify(prove_th83)).
% 0.57/1.42 cnf(2, plain, [-(_9503 = _9559), member(1 ^ [_9559, _9503], _9503), member(1 ^ [_9559, _9503], _9559)], clausify(member_equal)).
% 0.57/1.42 cnf(3, plain, [-(_9503 = _9559), -(member(1 ^ [_9559, _9503], _9503)), -(member(1 ^ [_9559, _9503], _9559))], clausify(member_equal)).
% 0.57/1.42 cnf(4, plain, [-(member(_10081, union(_9964, _10023))), member(_10081, _9964)], clausify(union_defn)).
% 0.57/1.42 cnf(5, plain, [member(_10081, union(_9964, _10023)), -(member(_10081, _9964)), -(member(_10081, _10023))], clausify(union_defn)).
% 0.57/1.42 cnf(6, plain, [member(_10598, difference(_10477, _10538)), -(member(_10598, _10477))], clausify(difference_defn)).
% 0.57/1.42 cnf(7, plain, [member(_10598, difference(_10477, _10538)), member(_10598, _10538)], clausify(difference_defn)).
% 0.57/1.42 cnf(8, plain, [-(member(_10598, difference(_10477, _10538))), member(_10598, _10477), -(member(_10598, _10538))], clausify(difference_defn)).
% 0.57/1.42
% 0.57/1.42 cnf('1',plain,[difference(union(4 ^ [], 5 ^ []), 5 ^ []) = difference(4 ^ [], 5 ^ [])],start(1)).
% 0.57/1.42 cnf('1.1',plain,[-(difference(union(4 ^ [], 5 ^ []), 5 ^ []) = difference(4 ^ [], 5 ^ [])), -(member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(union(4 ^ [], 5 ^ []), 5 ^ []))), -(member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(4 ^ [], 5 ^ [])))],extension(3,bind([[_9503, _9559], [difference(union(4 ^ [], 5 ^ []), 5 ^ []), difference(4 ^ [], 5 ^ [])]]))).
% 0.57/1.42 cnf('1.1.1',plain,[member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(union(4 ^ [], 5 ^ []), 5 ^ [])), -(member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], union(4 ^ [], 5 ^ [])))],extension(6,bind([[_10538, _10598, _10477], [5 ^ [], 1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], union(4 ^ [], 5 ^ [])]]))).
% 0.57/1.42 cnf('1.1.1.1',plain,[member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], union(4 ^ [], 5 ^ [])), -(member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], 4 ^ [])), -(member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], 5 ^ []))],extension(5,bind([[_9964, _10081, _10023], [4 ^ [], 1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], 5 ^ []]]))).
% 0.57/1.42 cnf('1.1.1.1.1',plain,[member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], 4 ^ []), -(member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(4 ^ [], 5 ^ []))), -(member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], 5 ^ []))],extension(8,bind([[_10477, _10598, _10538], [4 ^ [], 1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], 5 ^ []]]))).
% 0.57/1.42 cnf('1.1.1.1.1.1',plain,[member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(4 ^ [], 5 ^ [])), -(difference(union(4 ^ [], 5 ^ []), 5 ^ []) = difference(4 ^ [], 5 ^ [])), member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(union(4 ^ [], 5 ^ []), 5 ^ []))],extension(2,bind([[_9559, _9503], [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])]]))).
% 0.57/1.42 cnf('1.1.1.1.1.1.1',plain,[difference(union(4 ^ [], 5 ^ []), 5 ^ []) = difference(4 ^ [], 5 ^ [])],extension(1)).
% 0.57/1.42 cnf('1.1.1.1.1.1.2',plain,[-(member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(union(4 ^ [], 5 ^ []), 5 ^ [])))],reduction('1.1')).
% 0.57/1.42 cnf('1.1.1.1.1.2',plain,[member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], 5 ^ []), member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(union(4 ^ [], 5 ^ []), 5 ^ []))],extension(7,bind([[_10598, _10477, _10538], [1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], union(4 ^ [], 5 ^ []), 5 ^ []]]))).
% 0.57/1.42 cnf('1.1.1.1.1.2.1',plain,[-(member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(union(4 ^ [], 5 ^ []), 5 ^ [])))],reduction('1.1')).
% 0.57/1.42 cnf('1.1.1.1.2',plain,[member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], 5 ^ []), member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(union(4 ^ [], 5 ^ []), 5 ^ []))],extension(7,bind([[_10598, _10477, _10538], [1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], union(4 ^ [], 5 ^ []), 5 ^ []]]))).
% 0.57/1.42 cnf('1.1.1.1.2.1',plain,[-(member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(union(4 ^ [], 5 ^ []), 5 ^ [])))],reduction('1.1')).
% 0.57/1.42 cnf('1.1.2',plain,[member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(4 ^ [], 5 ^ [])), -(difference(union(4 ^ [], 5 ^ []), 5 ^ []) = difference(4 ^ [], 5 ^ [])), member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(union(4 ^ [], 5 ^ []), 5 ^ []))],extension(2,bind([[_9559, _9503], [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])]]))).
% 0.57/1.42 cnf('1.1.2.1',plain,[difference(union(4 ^ [], 5 ^ []), 5 ^ []) = difference(4 ^ [], 5 ^ [])],extension(1)).
% 0.57/1.42 cnf('1.1.2.2',plain,[-(member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(union(4 ^ [], 5 ^ []), 5 ^ []))), member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], union(4 ^ [], 5 ^ [])), -(member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], 5 ^ []))],extension(8,bind([[_10477, _10598, _10538], [union(4 ^ [], 5 ^ []), 1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], 5 ^ []]]))).
% 0.57/1.42 cnf('1.1.2.2.1',plain,[-(member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], union(4 ^ [], 5 ^ []))), member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], 4 ^ [])],extension(4,bind([[_10023, _10081, _9964], [5 ^ [], 1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], 4 ^ []]]))).
% 0.57/1.42 cnf('1.1.2.2.1.1',plain,[-(member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], 4 ^ [])), member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(4 ^ [], 5 ^ []))],extension(6,bind([[_10598, _10477, _10538], [1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], 4 ^ [], 5 ^ []]]))).
% 0.57/1.42 cnf('1.1.2.2.1.1.1',plain,[-(member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(4 ^ [], 5 ^ [])))],reduction('1.1')).
% 0.57/1.42 cnf('1.1.2.2.2',plain,[member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], 5 ^ []), member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(4 ^ [], 5 ^ []))],extension(7,bind([[_10598, _10477, _10538], [1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], 4 ^ [], 5 ^ []]]))).
% 0.57/1.42 cnf('1.1.2.2.2.1',plain,[-(member(1 ^ [difference(4 ^ [], 5 ^ []), difference(union(4 ^ [], 5 ^ []), 5 ^ [])], difference(4 ^ [], 5 ^ [])))],reduction('1.1')).
% 0.57/1.42 %-----------------------------------------------------
% 0.57/1.43
% 0.57/1.43 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------