%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET702+4 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n008.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:55:28 EDT 2022
% Result : Theorem 1.05s 1.42s
% Output : Proof 1.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SET702+4 : TPTP v8.1.0. Released v2.2.0.
% 0.12/0.14 % Command : leancop_casc.sh %s %d
% 0.14/0.35 % Computer : n008.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 600
% 0.14/0.35 % DateTime : Sat Jul 9 16:09:53 EDT 2022
% 0.14/0.35 % CPUTime :
% 1.05/1.42 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.05/1.43 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.05/1.44
% 1.05/1.44 %-----------------------------------------------------
% 1.05/1.44 fof(thI36, conjecture, ! [_30043, _30046] : subset(intersection(product(_30043), product(_30046)), product(intersection(_30043, _30046))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', thI36)).
% 1.05/1.44 fof(subset, axiom, ! [_30234, _30237] : (subset(_30234, _30237) <=> ! [_30255] : (member(_30255, _30234) => member(_30255, _30237))), file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', subset)).
% 1.05/1.44 fof(intersection, axiom, ! [_30456, _30459, _30462] : (member(_30456, intersection(_30459, _30462)) <=> member(_30456, _30459) & member(_30456, _30462)), file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', intersection)).
% 1.05/1.44 fof(product, axiom, ! [_30674, _30677] : (member(_30674, product(_30677)) <=> ! [_30699] : (member(_30699, _30677) => member(_30674, _30699))), file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', product)).
% 1.05/1.44
% 1.05/1.44 cnf(1, plain, [subset(intersection(product(4 ^ []), product(5 ^ [])), product(intersection(4 ^ [], 5 ^ [])))], clausify(thI36)).
% 1.05/1.44 cnf(2, plain, [-(subset(_14696, _14752)), -(member(1 ^ [_14752, _14696], _14696))], clausify(subset)).
% 1.05/1.44 cnf(3, plain, [-(subset(_14696, _14752)), member(1 ^ [_14752, _14696], _14752)], clausify(subset)).
% 1.05/1.44 cnf(4, plain, [member(_15883, intersection(_15942, _16000)), -(member(_15883, _15942))], clausify(intersection)).
% 1.05/1.44 cnf(5, plain, [-(member(_18951, product(_19009))), -(member(3 ^ [_19009, _18951], _19009))], clausify(product)).
% 1.05/1.44 cnf(6, plain, [-(member(_18951, product(_19009))), member(_18951, 3 ^ [_19009, _18951])], clausify(product)).
% 1.05/1.44 cnf(7, plain, [member(_18951, product(_19009)), member(_19141, _19009), -(member(_18951, _19141))], clausify(product)).
% 1.05/1.44
% 1.05/1.44 cnf('1',plain,[subset(intersection(product(4 ^ []), product(5 ^ [])), product(intersection(4 ^ [], 5 ^ [])))],start(1)).
% 1.05/1.44 cnf('1.1',plain,[-(subset(intersection(product(4 ^ []), product(5 ^ [])), product(intersection(4 ^ [], 5 ^ [])))), member(1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))], product(intersection(4 ^ [], 5 ^ [])))],extension(3,bind([[_14696, _14752], [intersection(product(4 ^ []), product(5 ^ [])), product(intersection(4 ^ [], 5 ^ []))]]))).
% 1.05/1.44 cnf('1.1.1',plain,[-(member(1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))], product(intersection(4 ^ [], 5 ^ [])))), member(1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))], 3 ^ [intersection(4 ^ [], 5 ^ []), 1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))]])],extension(6,bind([[_19009, _18951], [intersection(4 ^ [], 5 ^ []), 1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))]]]))).
% 1.05/1.44 cnf('1.1.1.1',plain,[-(member(1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))], 3 ^ [intersection(4 ^ [], 5 ^ []), 1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))]])), member(1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))], product(4 ^ [])), member(3 ^ [intersection(4 ^ [], 5 ^ []), 1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))]], 4 ^ [])],extension(7,bind([[_18951, _19141, _19009], [1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))], 3 ^ [intersection(4 ^ [], 5 ^ []), 1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))]], 4 ^ []]]))).
% 1.05/1.44 cnf('1.1.1.1.1',plain,[-(member(1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))], product(4 ^ []))), member(1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))], intersection(product(4 ^ []), product(5 ^ [])))],extension(4,bind([[_15883, _15942, _16000], [1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))], product(4 ^ []), product(5 ^ [])]]))).
% 1.05/1.44 cnf('1.1.1.1.1.1',plain,[-(member(1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))], intersection(product(4 ^ []), product(5 ^ [])))), -(subset(intersection(product(4 ^ []), product(5 ^ [])), product(intersection(4 ^ [], 5 ^ []))))],extension(2,bind([[_14696, _14752], [intersection(product(4 ^ []), product(5 ^ [])), product(intersection(4 ^ [], 5 ^ []))]]))).
% 1.05/1.44 cnf('1.1.1.1.1.1.1',plain,[subset(intersection(product(4 ^ []), product(5 ^ [])), product(intersection(4 ^ [], 5 ^ [])))],extension(1)).
% 1.05/1.44 cnf('1.1.1.1.2',plain,[-(member(3 ^ [intersection(4 ^ [], 5 ^ []), 1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))]], 4 ^ [])), member(3 ^ [intersection(4 ^ [], 5 ^ []), 1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))]], intersection(4 ^ [], 5 ^ []))],extension(4,bind([[_15883, _15942, _16000], [3 ^ [intersection(4 ^ [], 5 ^ []), 1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))]], 4 ^ [], 5 ^ []]]))).
% 1.05/1.44 cnf('1.1.1.1.2.1',plain,[-(member(3 ^ [intersection(4 ^ [], 5 ^ []), 1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))]], intersection(4 ^ [], 5 ^ []))), -(member(1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))], product(intersection(4 ^ [], 5 ^ []))))],extension(5,bind([[_18951, _19009], [1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))], intersection(4 ^ [], 5 ^ [])]]))).
% 1.05/1.44 cnf('1.1.1.1.2.1.1',plain,[member(1 ^ [product(intersection(4 ^ [], 5 ^ [])), intersection(product(4 ^ []), product(5 ^ []))], product(intersection(4 ^ [], 5 ^ [])))],reduction('1.1')).
% 1.05/1.44 %-----------------------------------------------------
% 1.05/1.45
% 1.05/1.45 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------