%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET621+3 : TPTP v8.1.0. Released v2.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:54:51 EDT 2022
% Result : Theorem 3.30s 3.47s
% Output : Proof 3.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SET621+3 : TPTP v8.1.0. Released v2.2.0.
% 0.03/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n009.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 : Sat Jul 9 18:49:07 EDT 2022
% 0.12/0.34 % CPUTime :
% 3.30/3.47 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.30/3.48 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.30/3.48
% 3.30/3.48 %-----------------------------------------------------
% 3.30/3.48 fof(prove_th97, conjecture, ! [_26903, _26906, _26909] : difference(symmetric_difference(_26903, _26906), _26909) = union(difference(_26903, union(_26906, _26909)), difference(_26906, union(_26903, _26909))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_th97)).
% 3.30/3.48 fof(symmetric_difference_defn, axiom, ! [_27192, _27195] : symmetric_difference(_27192, _27195) = union(difference(_27192, _27195), difference(_27195, _27192)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', symmetric_difference_defn)).
% 3.30/3.48 fof(difference_difference_union, axiom, ! [_27370, _27373, _27376] : difference(difference(_27370, _27373), _27376) = difference(_27370, union(_27373, _27376)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', difference_difference_union)).
% 3.30/3.48 fof(difference_distributes_over_union, axiom, ! [_27559, _27562, _27565] : difference(union(_27559, _27562), _27565) = union(difference(_27559, _27565), difference(_27562, _27565)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', difference_distributes_over_union)).
% 3.30/3.48
% 3.30/3.48 cnf(1, plain, [difference(symmetric_difference(3 ^ [], 4 ^ []), 5 ^ []) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), difference(4 ^ [], union(3 ^ [], 5 ^ [])))], clausify(prove_th97)).
% 3.30/3.48 cnf(2, plain, [-(difference(_9459, _9592) = difference(_9526, _9657)), _9459 = _9526, _9592 = _9657], theory(equality)).
% 3.30/3.48 cnf(3, plain, [-(union(_10697, _10830) = union(_10764, _10895)), _10697 = _10764, _10830 = _10895], theory(equality)).
% 3.30/3.48 cnf(4, plain, [-(_7283 = _7283)], theory(equality)).
% 3.30/3.48 cnf(5, plain, [-(_7715 = _7826), _7715 = _7771, _7771 = _7826], theory(equality)).
% 3.30/3.48 cnf(6, plain, [-(symmetric_difference(_11387, _11438) = union(difference(_11387, _11438), difference(_11438, _11387)))], clausify(symmetric_difference_defn)).
% 3.30/3.48 cnf(7, plain, [-(difference(difference(_11783, _11839), _11894) = difference(_11783, union(_11839, _11894)))], clausify(difference_difference_union)).
% 3.30/3.48 cnf(8, plain, [-(difference(union(_12250, _12309), _12367) = union(difference(_12250, _12367), difference(_12309, _12367)))], clausify(difference_distributes_over_union)).
% 3.30/3.48
% 3.30/3.48 cnf('1',plain,[difference(symmetric_difference(3 ^ [], 4 ^ []), 5 ^ []) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), difference(4 ^ [], union(3 ^ [], 5 ^ [])))],start(1)).
% 3.30/3.48 cnf('1.1',plain,[-(difference(symmetric_difference(3 ^ [], 4 ^ []), 5 ^ []) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), difference(4 ^ [], union(3 ^ [], 5 ^ [])))), difference(symmetric_difference(3 ^ [], 4 ^ []), 5 ^ []) = difference(union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])), 5 ^ []), difference(union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])), 5 ^ []) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), difference(4 ^ [], union(3 ^ [], 5 ^ [])))],extension(5,bind([[_7715, _7771, _7826], [difference(symmetric_difference(3 ^ [], 4 ^ []), 5 ^ []), difference(union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])), 5 ^ []), union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), difference(4 ^ [], union(3 ^ [], 5 ^ [])))]]))).
% 3.30/3.48 cnf('1.1.1',plain,[-(difference(symmetric_difference(3 ^ [], 4 ^ []), 5 ^ []) = difference(union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])), 5 ^ [])), symmetric_difference(3 ^ [], 4 ^ []) = union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])), 5 ^ [] = 5 ^ []],extension(2,bind([[_9459, _9526, _9592, _9657], [symmetric_difference(3 ^ [], 4 ^ []), union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])), 5 ^ [], 5 ^ []]]))).
% 3.30/3.48 cnf('1.1.1.1',plain,[-(symmetric_difference(3 ^ [], 4 ^ []) = union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ []))), symmetric_difference(3 ^ [], 4 ^ []) = union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])), union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])) = union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ []))],extension(5,bind([[_7715, _7771, _7826], [symmetric_difference(3 ^ [], 4 ^ []), union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])), union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ []))]]))).
% 3.30/3.48 cnf('1.1.1.1.1',plain,[-(symmetric_difference(3 ^ [], 4 ^ []) = union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])))],extension(6,bind([[_11438, _11387], [4 ^ [], 3 ^ []]]))).
% 3.30/3.48 cnf('1.1.1.1.2',plain,[-(union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])) = union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])))],extension(4,bind([[_7283], [union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ []))]]))).
% 3.30/3.48 cnf('1.1.1.2',plain,[-(5 ^ [] = 5 ^ [])],extension(4,bind([[_7283], [5 ^ []]]))).
% 3.30/3.48 cnf('1.1.2',plain,[-(difference(union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])), 5 ^ []) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), difference(4 ^ [], union(3 ^ [], 5 ^ [])))), difference(union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])), 5 ^ []) = union(difference(difference(3 ^ [], 4 ^ []), 5 ^ []), difference(difference(4 ^ [], 3 ^ []), 5 ^ [])), union(difference(difference(3 ^ [], 4 ^ []), 5 ^ []), difference(difference(4 ^ [], 3 ^ []), 5 ^ [])) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), difference(4 ^ [], union(3 ^ [], 5 ^ [])))],extension(5,bind([[_7715, _7771, _7826], [difference(union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])), 5 ^ []), union(difference(difference(3 ^ [], 4 ^ []), 5 ^ []), difference(difference(4 ^ [], 3 ^ []), 5 ^ [])), union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), difference(4 ^ [], union(3 ^ [], 5 ^ [])))]]))).
% 3.30/3.48 cnf('1.1.2.1',plain,[-(difference(union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])), 5 ^ []) = union(difference(difference(3 ^ [], 4 ^ []), 5 ^ []), difference(difference(4 ^ [], 3 ^ []), 5 ^ []))), difference(union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])), 5 ^ []) = union(difference(difference(3 ^ [], 4 ^ []), 5 ^ []), difference(difference(4 ^ [], 3 ^ []), 5 ^ [])), union(difference(difference(3 ^ [], 4 ^ []), 5 ^ []), difference(difference(4 ^ [], 3 ^ []), 5 ^ [])) = union(difference(difference(3 ^ [], 4 ^ []), 5 ^ []), difference(difference(4 ^ [], 3 ^ []), 5 ^ []))],extension(5,bind([[_7715, _7771, _7826], [difference(union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])), 5 ^ []), union(difference(difference(3 ^ [], 4 ^ []), 5 ^ []), difference(difference(4 ^ [], 3 ^ []), 5 ^ [])), union(difference(difference(3 ^ [], 4 ^ []), 5 ^ []), difference(difference(4 ^ [], 3 ^ []), 5 ^ []))]]))).
% 3.30/3.48 cnf('1.1.2.1.1',plain,[-(difference(union(difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ [])), 5 ^ []) = union(difference(difference(3 ^ [], 4 ^ []), 5 ^ []), difference(difference(4 ^ [], 3 ^ []), 5 ^ [])))],extension(8,bind([[_12250, _12309, _12367], [difference(3 ^ [], 4 ^ []), difference(4 ^ [], 3 ^ []), 5 ^ []]]))).
% 3.30/3.48 cnf('1.1.2.1.2',plain,[-(union(difference(difference(3 ^ [], 4 ^ []), 5 ^ []), difference(difference(4 ^ [], 3 ^ []), 5 ^ [])) = union(difference(difference(3 ^ [], 4 ^ []), 5 ^ []), difference(difference(4 ^ [], 3 ^ []), 5 ^ [])))],extension(4,bind([[_7283], [union(difference(difference(3 ^ [], 4 ^ []), 5 ^ []), difference(difference(4 ^ [], 3 ^ []), 5 ^ []))]]))).
% 3.30/3.48 cnf('1.1.2.2',plain,[-(union(difference(difference(3 ^ [], 4 ^ []), 5 ^ []), difference(difference(4 ^ [], 3 ^ []), 5 ^ [])) = union(difference(3 ^ [], union(4 ^ [], 5 ^ [])), difference(4 ^ [], union(3 ^ [], 5 ^ [])))), difference(difference(3 ^ [], 4 ^ []), 5 ^ []) = difference(3 ^ [], union(4 ^ [], 5 ^ [])), difference(difference(4 ^ [], 3 ^ []), 5 ^ []) = difference(4 ^ [], union(3 ^ [], 5 ^ []))],extension(3,bind([[_10697, _10764, _10830, _10895], [difference(difference(3 ^ [], 4 ^ []), 5 ^ []), difference(3 ^ [], union(4 ^ [], 5 ^ [])), difference(difference(4 ^ [], 3 ^ []), 5 ^ []), difference(4 ^ [], union(3 ^ [], 5 ^ []))]]))).
% 3.30/3.48 cnf('1.1.2.2.1',plain,[-(difference(difference(3 ^ [], 4 ^ []), 5 ^ []) = difference(3 ^ [], union(4 ^ [], 5 ^ [])))],extension(7,bind([[_11783, _11839, _11894], [3 ^ [], 4 ^ [], 5 ^ []]]))).
% 3.30/3.48 cnf('1.1.2.2.2',plain,[-(difference(difference(4 ^ [], 3 ^ []), 5 ^ []) = difference(4 ^ [], union(3 ^ [], 5 ^ [])))],extension(7,bind([[_11783, _11839, _11894], [4 ^ [], 3 ^ [], 5 ^ []]]))).
% 3.30/3.48 %-----------------------------------------------------
% 3.30/3.49
% 3.30/3.49 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------