%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWV109+1 : TPTP v8.1.0. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n005.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 : Wed Jul 20 19:49:34 EDT 2022
% Result : Theorem 0.40s 1.42s
% Output : Proof 0.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SWV109+1 : TPTP v8.1.0. Bugfixed v3.3.0.
% 0.04/0.13 % Command : leancop_casc.sh %s %d
% 0.14/0.34 % Computer : n005.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 600
% 0.14/0.34 % DateTime : Tue Jun 14 18:47:24 EDT 2022
% 0.14/0.34 % CPUTime :
% 0.40/1.42 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/1.43 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/1.43
% 0.40/1.43 %-----------------------------------------------------
% 0.40/1.43 fof(quaternion_ds1_symm_0002, conjecture, leq(n0, pv5) & leq(n0, pv47) & leq(pv5, minus(n999, n1)) & leq(pv47, minus(n6, n1)) & ! [_234604, _234607] : (leq(n0, _234604) & leq(n0, _234607) & leq(_234604, minus(n6, n1)) & leq(_234607, minus(n6, n1)) => a_select3(q_ds1_filter, _234604, _234607) = a_select3(q_ds1_filter, _234607, _234604)) & ! [_234695, _234698] : (leq(n0, _234695) & leq(n0, _234698) & leq(_234695, minus(n3, n1)) & leq(_234698, minus(n3, n1)) => a_select3(r_ds1_filter, _234695, _234698) = a_select3(r_ds1_filter, _234698, _234695)) & ! [_234786, _234789] : (leq(n0, _234786) & leq(n0, _234789) & leq(_234786, minus(n6, n1)) & leq(_234789, minus(n6, n1)) => a_select3(pminus_ds1_filter, _234786, _234789) = a_select3(pminus_ds1_filter, _234789, _234786)) & ! [_234877, _234880] : (leq(n0, _234877) & leq(n0, _234880) & leq(_234877, minus(n6, n1)) & leq(_234880, minus(n6, n1)) => a_select3(pminus_ds1_filter, _234877, _234880) = a_select3(pminus_ds1_filter, _234880, _234877)) & ! [_234968] : (leq(n0, _234968) & leq(_234968, minus(n6, n1)) => ! [_235003] : (leq(n0, _235003) & leq(_235003, minus(n6, n1)) => a_select3(id_ds1_filter, _234968, _235003) = a_select3(id_ds1_filter, _235003, _234968))) => leq(n0, pv5) & leq(pv5, minus(n999, n1)) & ! [_235091, _235094] : (leq(n0, _235091) & leq(n0, _235094) & leq(_235091, minus(n6, n1)) & leq(_235094, minus(n6, n1)) => a_select3(q_ds1_filter, _235091, _235094) = a_select3(q_ds1_filter, _235094, _235091)) & ! [_235182, _235185] : (leq(n0, _235182) & leq(n0, _235185) & leq(_235182, minus(n3, n1)) & leq(_235185, minus(n3, n1)) => a_select3(r_ds1_filter, _235182, _235185) = a_select3(r_ds1_filter, _235185, _235182)) & ! [_235273, _235276] : (leq(n0, _235273) & leq(n0, _235276) & leq(_235273, minus(n6, n1)) & leq(_235276, minus(n6, n1)) => a_select3(pminus_ds1_filter, _235273, _235276) = a_select3(pminus_ds1_filter, _235276, _235273)) & ! [_235364, _235367] : (leq(n0, _235364) & leq(n0, _235367) & leq(_235364, minus(n6, n1)) & leq(_235367, minus(n6, n1)) => a_select3(pminus_ds1_filter, _235364, _235367) = a_select3(pminus_ds1_filter, _235367, _235364)) & ! [_235455] : (leq(n0, _235455) & leq(_235455, minus(n6, n1)) => ! [_235490] : (leq(n0, _235490) & leq(_235490, minus(n6, n1)) => a_select3(id_ds1_filter, _235455, _235490) = a_select3(id_ds1_filter, _235490, _235455))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', quaternion_ds1_symm_0002)).
% 0.40/1.43
% 0.40/1.43 cnf(1, plain, [-(42 ^ []), a_select3(id_ds1_filter, 40 ^ [], 41 ^ []) = a_select3(id_ds1_filter, 41 ^ [], 40 ^ [])], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(2, plain, [-(42 ^ []), -(leq(41 ^ [], minus(n6, n1)))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(3, plain, [-(42 ^ []), -(leq(n0, 41 ^ []))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(4, plain, [-(42 ^ []), -(leq(40 ^ [], minus(n6, n1)))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(5, plain, [-(42 ^ []), -(leq(n0, 40 ^ []))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(6, plain, [-(39 ^ []), a_select3(pminus_ds1_filter, 37 ^ [], 38 ^ []) = a_select3(pminus_ds1_filter, 38 ^ [], 37 ^ [])], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(7, plain, [-(39 ^ []), -(leq(38 ^ [], minus(n6, n1)))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(8, plain, [-(39 ^ []), -(leq(37 ^ [], minus(n6, n1)))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(9, plain, [-(39 ^ []), -(leq(n0, 38 ^ []))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(10, plain, [-(39 ^ []), -(leq(n0, 37 ^ []))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(11, plain, [-(36 ^ []), a_select3(pminus_ds1_filter, 34 ^ [], 35 ^ []) = a_select3(pminus_ds1_filter, 35 ^ [], 34 ^ [])], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(12, plain, [-(36 ^ []), -(leq(35 ^ [], minus(n6, n1)))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(13, plain, [-(36 ^ []), -(leq(34 ^ [], minus(n6, n1)))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(14, plain, [-(36 ^ []), -(leq(n0, 35 ^ []))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(15, plain, [-(36 ^ []), -(leq(n0, 34 ^ []))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(16, plain, [-(33 ^ []), a_select3(r_ds1_filter, 31 ^ [], 32 ^ []) = a_select3(r_ds1_filter, 32 ^ [], 31 ^ [])], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(17, plain, [-(33 ^ []), -(leq(32 ^ [], minus(n3, n1)))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(18, plain, [-(33 ^ []), -(leq(31 ^ [], minus(n3, n1)))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(19, plain, [-(33 ^ []), -(leq(n0, 32 ^ []))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(20, plain, [-(33 ^ []), -(leq(n0, 31 ^ []))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(21, plain, [-(30 ^ []), a_select3(q_ds1_filter, 28 ^ [], 29 ^ []) = a_select3(q_ds1_filter, 29 ^ [], 28 ^ [])], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(22, plain, [-(30 ^ []), -(leq(29 ^ [], minus(n6, n1)))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(23, plain, [-(30 ^ []), -(leq(28 ^ [], minus(n6, n1)))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(24, plain, [-(30 ^ []), -(leq(n0, 29 ^ []))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(25, plain, [-(30 ^ []), -(leq(n0, 28 ^ []))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(26, plain, [leq(n0, pv5), leq(pv5, minus(n999, n1)), 30 ^ [], 33 ^ [], 36 ^ [], 39 ^ [], 42 ^ []], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(27, plain, [-(leq(n0, pv5))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(28, plain, [-(leq(pv5, minus(n999, n1)))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(29, plain, [-(a_select3(q_ds1_filter, _119084, _119155) = a_select3(q_ds1_filter, _119155, _119084)), leq(n0, _119084), leq(n0, _119155), leq(_119084, minus(n6, n1)), leq(_119155, minus(n6, n1))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(30, plain, [-(a_select3(r_ds1_filter, _119822, _119893) = a_select3(r_ds1_filter, _119893, _119822)), leq(n0, _119822), leq(n0, _119893), leq(_119822, minus(n3, n1)), leq(_119893, minus(n3, n1))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(31, plain, [-(a_select3(pminus_ds1_filter, _120560, _120631) = a_select3(pminus_ds1_filter, _120631, _120560)), leq(n0, _120560), leq(n0, _120631), leq(_120560, minus(n6, n1)), leq(_120631, minus(n6, n1))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43 cnf(32, plain, [leq(_122026, minus(n6, n1)), leq(n0, _122026), -(a_select3(id_ds1_filter, _122026, _122267) = a_select3(id_ds1_filter, _122267, _122026)), leq(n0, _122267), leq(_122267, minus(n6, n1))], clausify(quaternion_ds1_symm_0002)).
% 0.40/1.43
% 0.40/1.43 cnf('1',plain,[leq(n0, pv5), leq(pv5, minus(n999, n1)), 30 ^ [], 33 ^ [], 36 ^ [], 39 ^ [], 42 ^ []],start(26)).
% 0.40/1.43 cnf('1.1',plain,[-(leq(n0, pv5))],extension(27)).
% 0.40/1.43 cnf('1.2',plain,[-(leq(pv5, minus(n999, n1)))],extension(28)).
% 0.40/1.43 cnf('1.3',plain,[-(30 ^ []), a_select3(q_ds1_filter, 28 ^ [], 29 ^ []) = a_select3(q_ds1_filter, 29 ^ [], 28 ^ [])],extension(21)).
% 0.40/1.43 cnf('1.3.1',plain,[-(a_select3(q_ds1_filter, 28 ^ [], 29 ^ []) = a_select3(q_ds1_filter, 29 ^ [], 28 ^ [])), leq(n0, 28 ^ []), leq(n0, 29 ^ []), leq(28 ^ [], minus(n6, n1)), leq(29 ^ [], minus(n6, n1))],extension(29,bind([[_119084, _119155], [28 ^ [], 29 ^ []]]))).
% 0.40/1.43 cnf('1.3.1.1',plain,[-(leq(n0, 28 ^ [])), -(30 ^ [])],extension(25)).
% 0.40/1.43 cnf('1.3.1.1.1',plain,[30 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.3.1.2',plain,[-(leq(n0, 29 ^ [])), -(30 ^ [])],extension(24)).
% 0.40/1.43 cnf('1.3.1.2.1',plain,[30 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.3.1.3',plain,[-(leq(28 ^ [], minus(n6, n1))), -(30 ^ [])],extension(23)).
% 0.40/1.43 cnf('1.3.1.3.1',plain,[30 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.3.1.4',plain,[-(leq(29 ^ [], minus(n6, n1))), -(30 ^ [])],extension(22)).
% 0.40/1.43 cnf('1.3.1.4.1',plain,[30 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.4',plain,[-(33 ^ []), a_select3(r_ds1_filter, 31 ^ [], 32 ^ []) = a_select3(r_ds1_filter, 32 ^ [], 31 ^ [])],extension(16)).
% 0.40/1.43 cnf('1.4.1',plain,[-(a_select3(r_ds1_filter, 31 ^ [], 32 ^ []) = a_select3(r_ds1_filter, 32 ^ [], 31 ^ [])), leq(n0, 31 ^ []), leq(n0, 32 ^ []), leq(31 ^ [], minus(n3, n1)), leq(32 ^ [], minus(n3, n1))],extension(30,bind([[_119822, _119893], [31 ^ [], 32 ^ []]]))).
% 0.40/1.43 cnf('1.4.1.1',plain,[-(leq(n0, 31 ^ [])), -(33 ^ [])],extension(20)).
% 0.40/1.43 cnf('1.4.1.1.1',plain,[33 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.4.1.2',plain,[-(leq(n0, 32 ^ [])), -(33 ^ [])],extension(19)).
% 0.40/1.43 cnf('1.4.1.2.1',plain,[33 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.4.1.3',plain,[-(leq(31 ^ [], minus(n3, n1))), -(33 ^ [])],extension(18)).
% 0.40/1.43 cnf('1.4.1.3.1',plain,[33 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.4.1.4',plain,[-(leq(32 ^ [], minus(n3, n1))), -(33 ^ [])],extension(17)).
% 0.40/1.43 cnf('1.4.1.4.1',plain,[33 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.5',plain,[-(36 ^ []), a_select3(pminus_ds1_filter, 34 ^ [], 35 ^ []) = a_select3(pminus_ds1_filter, 35 ^ [], 34 ^ [])],extension(11)).
% 0.40/1.43 cnf('1.5.1',plain,[-(a_select3(pminus_ds1_filter, 34 ^ [], 35 ^ []) = a_select3(pminus_ds1_filter, 35 ^ [], 34 ^ [])), leq(n0, 34 ^ []), leq(n0, 35 ^ []), leq(34 ^ [], minus(n6, n1)), leq(35 ^ [], minus(n6, n1))],extension(31,bind([[_120560, _120631], [34 ^ [], 35 ^ []]]))).
% 0.40/1.43 cnf('1.5.1.1',plain,[-(leq(n0, 34 ^ [])), -(36 ^ [])],extension(15)).
% 0.40/1.43 cnf('1.5.1.1.1',plain,[36 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.5.1.2',plain,[-(leq(n0, 35 ^ [])), -(36 ^ [])],extension(14)).
% 0.40/1.43 cnf('1.5.1.2.1',plain,[36 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.5.1.3',plain,[-(leq(34 ^ [], minus(n6, n1))), -(36 ^ [])],extension(13)).
% 0.40/1.43 cnf('1.5.1.3.1',plain,[36 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.5.1.4',plain,[-(leq(35 ^ [], minus(n6, n1))), -(36 ^ [])],extension(12)).
% 0.40/1.43 cnf('1.5.1.4.1',plain,[36 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.6',plain,[-(39 ^ []), a_select3(pminus_ds1_filter, 37 ^ [], 38 ^ []) = a_select3(pminus_ds1_filter, 38 ^ [], 37 ^ [])],extension(6)).
% 0.40/1.43 cnf('1.6.1',plain,[-(a_select3(pminus_ds1_filter, 37 ^ [], 38 ^ []) = a_select3(pminus_ds1_filter, 38 ^ [], 37 ^ [])), leq(n0, 37 ^ []), leq(n0, 38 ^ []), leq(37 ^ [], minus(n6, n1)), leq(38 ^ [], minus(n6, n1))],extension(31,bind([[_120560, _120631], [37 ^ [], 38 ^ []]]))).
% 0.40/1.43 cnf('1.6.1.1',plain,[-(leq(n0, 37 ^ [])), -(39 ^ [])],extension(10)).
% 0.40/1.43 cnf('1.6.1.1.1',plain,[39 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.6.1.2',plain,[-(leq(n0, 38 ^ [])), -(39 ^ [])],extension(9)).
% 0.40/1.43 cnf('1.6.1.2.1',plain,[39 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.6.1.3',plain,[-(leq(37 ^ [], minus(n6, n1))), -(39 ^ [])],extension(8)).
% 0.40/1.43 cnf('1.6.1.3.1',plain,[39 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.6.1.4',plain,[-(leq(38 ^ [], minus(n6, n1))), -(39 ^ [])],extension(7)).
% 0.40/1.43 cnf('1.6.1.4.1',plain,[39 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.7',plain,[-(42 ^ []), a_select3(id_ds1_filter, 40 ^ [], 41 ^ []) = a_select3(id_ds1_filter, 41 ^ [], 40 ^ [])],extension(1)).
% 0.40/1.43 cnf('1.7.1',plain,[-(a_select3(id_ds1_filter, 40 ^ [], 41 ^ []) = a_select3(id_ds1_filter, 41 ^ [], 40 ^ [])), leq(40 ^ [], minus(n6, n1)), leq(n0, 40 ^ []), leq(n0, 41 ^ []), leq(41 ^ [], minus(n6, n1))],extension(32,bind([[_122026, _122267], [40 ^ [], 41 ^ []]]))).
% 0.40/1.43 cnf('1.7.1.1',plain,[-(leq(40 ^ [], minus(n6, n1))), -(42 ^ [])],extension(4)).
% 0.40/1.43 cnf('1.7.1.1.1',plain,[42 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.7.1.2',plain,[-(leq(n0, 40 ^ [])), -(42 ^ [])],extension(5)).
% 0.40/1.43 cnf('1.7.1.2.1',plain,[42 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.7.1.3',plain,[-(leq(n0, 41 ^ [])), -(42 ^ [])],extension(3)).
% 0.40/1.43 cnf('1.7.1.3.1',plain,[42 ^ []],reduction('1')).
% 0.40/1.43 cnf('1.7.1.4',plain,[-(leq(41 ^ [], minus(n6, n1))), -(42 ^ [])],extension(2)).
% 0.40/1.43 cnf('1.7.1.4.1',plain,[42 ^ []],reduction('1')).
% 0.40/1.43 %-----------------------------------------------------
% 0.40/1.44
% 0.40/1.44 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------