%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWC047+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n017.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 21:09:00 EDT 2022
% Result : Theorem 112.05s 108.95s
% Output : Proof 112.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : SWC047+1 : TPTP v8.1.0. Released v2.4.0.
% 0.11/0.12 % Command : leancop_casc.sh %s %d
% 0.11/0.33 % Computer : n017.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Sun Jun 12 22:14:22 EDT 2022
% 0.11/0.33 % CPUTime :
% 112.05/108.95 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 112.05/108.96 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 112.05/108.96
% 112.05/108.96 %-----------------------------------------------------
% 112.05/108.96 fof(co1, conjecture, ! [_195076] : (ssList(_195076) => ! [_195091] : (ssList(_195091) => ! [_195106] : (ssList(_195106) => ! [_195121] : (ssList(_195121) => (! _195091) = _195121 | (! _195076) = _195106 | (! _195121) = _195106 | ((! nil) = _195091 | nil = _195076) & (~ neq(_195091, nil) | ? [_195186] : (ssList(_195186) & neq(_195186, nil) & rearsegP(_195091, _195186) & rearsegP(_195076, _195186))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 112.05/108.96 fof(ax2, axiom, ? [_195821] : (ssItem(_195821) & ? [_195836] : (ssItem(_195836) & (! _195821) = _195836)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax2)).
% 112.05/108.96 fof(ax15, axiom, ! [_196081] : (ssList(_196081) => ! [_196096] : (ssList(_196096) => (neq(_196081, _196096) <=> (! _196081) = _196096))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax15)).
% 112.05/108.96 fof(ax17, axiom, ssList(nil), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax17)).
% 112.05/108.96 fof(ax19, axiom, ! [_196341] : (ssList(_196341) => ! [_196356] : (ssList(_196356) => ! [_196371] : (ssItem(_196371) => ! [_196386] : (ssItem(_196386) => cons(_196371, _196341) = cons(_196386, _196356) => _196371 = _196386 & _196356 = _196341)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax19)).
% 112.05/108.96 fof(ax49, axiom, ! [_196738] : (ssList(_196738) => rearsegP(_196738, _196738)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax', ax49)).
% 112.05/108.96
% 112.05/108.96 cnf(1, plain, [-(ssList(48 ^ []))], clausify(co1)).
% 112.05/108.96 cnf(2, plain, [-(49 ^ [] = 51 ^ [])], clausify(co1)).
% 112.05/108.96 cnf(3, plain, [-(48 ^ [] = 50 ^ [])], clausify(co1)).
% 112.05/108.96 cnf(4, plain, [-(51 ^ [] = 50 ^ [])], clausify(co1)).
% 112.05/108.96 cnf(5, plain, [-(nil = 49 ^ []), -(neq(49 ^ [], nil))], clausify(co1)).
% 112.05/108.96 cnf(6, plain, [-(nil = 49 ^ []), ssList(_135033), neq(_135033, nil), rearsegP(49 ^ [], _135033), rearsegP(48 ^ [], _135033)], clausify(co1)).
% 112.05/108.96 cnf(7, plain, [nil = 48 ^ [], -(neq(49 ^ [], nil))], clausify(co1)).
% 112.05/108.96 cnf(8, plain, [nil = 48 ^ [], ssList(_135033), neq(_135033, nil), rearsegP(49 ^ [], _135033), rearsegP(48 ^ [], _135033)], clausify(co1)).
% 112.05/108.96 cnf(9, plain, [-(cons(_66383, _66516) = cons(_66450, _66581)), _66383 = _66450, _66516 = _66581], theory(equality)).
% 112.05/108.96 cnf(10, plain, [-(_55670 = _55670)], theory(equality)).
% 112.05/108.96 cnf(11, plain, [_55823 = _55868, -(_55868 = _55823)], theory(equality)).
% 112.05/108.96 cnf(12, plain, [-(_56102 = _56213), _56102 = _56158, _56158 = _56213], theory(equality)).
% 112.05/108.96 cnf(13, plain, [-(neq(_61376, _61507)), neq(_61309, _61442), _61309 = _61376, _61442 = _61507], theory(equality)).
% 112.05/108.96 cnf(14, plain, [-(rearsegP(_62000, _62131)), rearsegP(_61933, _62066), _61933 = _62000, _62066 = _62131], theory(equality)).
% 112.05/108.96 cnf(15, plain, [-(ssItem(1 ^ []))], clausify(ax2)).
% 112.05/108.96 cnf(16, plain, [ssList(_81231), ssList(_81326), -(neq(_81231, _81326)), -(_81231 = _81326)], clausify(ax15)).
% 112.05/108.96 cnf(17, plain, [-(ssList(nil))], clausify(ax17)).
% 112.05/108.96 cnf(18, plain, [ssList(_82567), ssList(_82692), ssItem(_82811), ssItem(_82924), cons(_82811, _82567) = cons(_82924, _82692), -(_82692 = _82567)], clausify(ax19)).
% 112.05/108.96 cnf(19, plain, [ssList(_97038), -(rearsegP(_97038, _97038))], clausify(ax49)).
% 112.05/108.96
% 112.05/108.96 cnf('1',plain,[nil = 48 ^ [], ssList(48 ^ []), neq(48 ^ [], nil), rearsegP(49 ^ [], 48 ^ []), rearsegP(48 ^ [], 48 ^ [])],start(8,bind([[_135033], [48 ^ []]]))).
% 112.05/108.96 cnf('1.1',plain,[-(nil = 48 ^ []), nil = 49 ^ [], 49 ^ [] = 48 ^ []],extension(12,bind([[_56102, _56158, _56213], [nil, 49 ^ [], 48 ^ []]]))).
% 112.05/108.96 cnf('1.1.1',plain,[-(nil = 49 ^ []), ssList(48 ^ []), neq(48 ^ [], nil), rearsegP(49 ^ [], 48 ^ []), rearsegP(48 ^ [], 48 ^ [])],extension(6,bind([[_135033], [48 ^ []]]))).
% 112.05/108.96 cnf('1.1.1.1',plain,[-(ssList(48 ^ []))],extension(1)).
% 112.05/108.96 cnf('1.1.1.2',plain,[-(neq(48 ^ [], nil)), ssList(48 ^ []), ssList(nil), -(48 ^ [] = nil)],extension(16,bind([[_81231, _81326], [48 ^ [], nil]]))).
% 112.05/108.96 cnf('1.1.1.2.1',plain,[-(ssList(48 ^ []))],extension(1)).
% 112.05/108.96 cnf('1.1.1.2.2',plain,[-(ssList(nil))],extension(17)).
% 112.05/108.96 cnf('1.1.1.2.3',plain,[48 ^ [] = nil, -(cons(1 ^ [], 48 ^ []) = cons(1 ^ [], nil)), 1 ^ [] = 1 ^ []],extension(9,bind([[_66516, _66581, _66383, _66450], [48 ^ [], nil, 1 ^ [], 1 ^ []]]))).
% 112.05/108.96 cnf('1.1.1.2.3.1',plain,[cons(1 ^ [], 48 ^ []) = cons(1 ^ [], nil), ssList(48 ^ []), ssList(nil), ssItem(1 ^ []), ssItem(1 ^ []), -(nil = 48 ^ [])],extension(18,bind([[_82811, _82924, _82692, _82567], [1 ^ [], 1 ^ [], nil, 48 ^ []]]))).
% 112.05/108.96 cnf('1.1.1.2.3.1.1',plain,[-(ssList(48 ^ []))],extension(1)).
% 112.05/108.96 cnf('1.1.1.2.3.1.2',plain,[-(ssList(nil))],extension(17)).
% 112.05/108.96 cnf('1.1.1.2.3.1.3',plain,[-(ssItem(1 ^ []))],extension(15)).
% 112.05/108.96 cnf('1.1.1.2.3.1.4',plain,[-(ssItem(1 ^ []))],extension(15)).
% 112.05/108.96 cnf('1.1.1.2.3.1.5',plain,[nil = 48 ^ []],reduction('1')).
% 112.05/108.96 cnf('1.1.1.2.3.2',plain,[-(1 ^ [] = 1 ^ [])],extension(10,bind([[_55670], [1 ^ []]]))).
% 112.05/108.96 cnf('1.1.1.3',plain,[-(rearsegP(49 ^ [], 48 ^ [])), rearsegP(50 ^ [], 50 ^ []), 50 ^ [] = 49 ^ [], 50 ^ [] = 48 ^ []],extension(14,bind([[_61933, _62000, _62066, _62131], [50 ^ [], 49 ^ [], 50 ^ [], 48 ^ []]]))).
% 112.05/108.96 cnf('1.1.1.3.1',plain,[-(rearsegP(50 ^ [], 50 ^ [])), rearsegP(48 ^ [], 48 ^ []), 48 ^ [] = 50 ^ [], 48 ^ [] = 50 ^ []],extension(14,bind([[_61933, _62000, _62066, _62131], [48 ^ [], 50 ^ [], 48 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.1.1.3.1.1',plain,[-(rearsegP(48 ^ [], 48 ^ [])), ssList(48 ^ [])],extension(19,bind([[_97038], [48 ^ []]]))).
% 112.05/108.96 cnf('1.1.1.3.1.1.1',plain,[-(ssList(48 ^ []))],extension(1)).
% 112.05/108.96 cnf('1.1.1.3.1.2',plain,[-(48 ^ [] = 50 ^ [])],extension(3)).
% 112.05/108.96 cnf('1.1.1.3.1.3',plain,[-(48 ^ [] = 50 ^ [])],extension(3)).
% 112.05/108.96 cnf('1.1.1.3.2',plain,[-(50 ^ [] = 49 ^ []), 49 ^ [] = 50 ^ []],extension(11,bind([[_55823, _55868], [49 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.1.1.3.2.1',plain,[-(49 ^ [] = 50 ^ []), 49 ^ [] = 51 ^ [], 51 ^ [] = 50 ^ []],extension(12,bind([[_56102, _56158, _56213], [49 ^ [], 51 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.1.1.3.2.1.1',plain,[-(49 ^ [] = 51 ^ [])],extension(2)).
% 112.05/108.96 cnf('1.1.1.3.2.1.2',plain,[-(51 ^ [] = 50 ^ [])],extension(4)).
% 112.05/108.96 cnf('1.1.1.3.3',plain,[-(50 ^ [] = 48 ^ []), 48 ^ [] = 50 ^ []],extension(11,bind([[_55823, _55868], [48 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.1.1.3.3.1',plain,[-(48 ^ [] = 50 ^ [])],extension(3)).
% 112.05/108.96 cnf('1.1.1.4',plain,[-(rearsegP(48 ^ [], 48 ^ [])), rearsegP(50 ^ [], 50 ^ []), 50 ^ [] = 48 ^ [], 50 ^ [] = 48 ^ []],extension(14,bind([[_61933, _62000, _62066, _62131], [50 ^ [], 48 ^ [], 50 ^ [], 48 ^ []]]))).
% 112.05/108.96 cnf('1.1.1.4.1',plain,[-(rearsegP(50 ^ [], 50 ^ [])), rearsegP(48 ^ [], 48 ^ []), 48 ^ [] = 50 ^ [], 48 ^ [] = 50 ^ []],extension(14,bind([[_61933, _62000, _62066, _62131], [48 ^ [], 50 ^ [], 48 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.1.1.4.1.1',plain,[-(rearsegP(48 ^ [], 48 ^ [])), ssList(48 ^ [])],extension(19,bind([[_97038], [48 ^ []]]))).
% 112.05/108.96 cnf('1.1.1.4.1.1.1',plain,[-(ssList(48 ^ []))],extension(1)).
% 112.05/108.96 cnf('1.1.1.4.1.2',plain,[-(48 ^ [] = 50 ^ [])],extension(3)).
% 112.05/108.96 cnf('1.1.1.4.1.3',plain,[-(48 ^ [] = 50 ^ [])],extension(3)).
% 112.05/108.96 cnf('1.1.1.4.2',plain,[-(50 ^ [] = 48 ^ []), 48 ^ [] = 50 ^ []],extension(11,bind([[_55823, _55868], [48 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.1.1.4.2.1',plain,[-(48 ^ [] = 50 ^ [])],extension(3)).
% 112.05/108.96 cnf('1.1.1.4.3',plain,[-(50 ^ [] = 48 ^ [])],lemmata('1.1.1.4')).
% 112.05/108.96 cnf('1.1.2',plain,[-(49 ^ [] = 48 ^ []), 48 ^ [] = 49 ^ []],extension(11,bind([[_55823, _55868], [48 ^ [], 49 ^ []]]))).
% 112.05/108.96 cnf('1.1.2.1',plain,[-(48 ^ [] = 49 ^ []), 48 ^ [] = 50 ^ [], 50 ^ [] = 49 ^ []],extension(12,bind([[_56102, _56158, _56213], [48 ^ [], 50 ^ [], 49 ^ []]]))).
% 112.05/108.96 cnf('1.1.2.1.1',plain,[-(48 ^ [] = 50 ^ [])],extension(3)).
% 112.05/108.96 cnf('1.1.2.1.2',plain,[-(50 ^ [] = 49 ^ []), 49 ^ [] = 50 ^ []],extension(11,bind([[_55823, _55868], [49 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.1.2.1.2.1',plain,[-(49 ^ [] = 50 ^ []), 49 ^ [] = 51 ^ [], 51 ^ [] = 50 ^ []],extension(12,bind([[_56102, _56158, _56213], [49 ^ [], 51 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.1.2.1.2.1.1',plain,[-(49 ^ [] = 51 ^ [])],extension(2)).
% 112.05/108.96 cnf('1.1.2.1.2.1.2',plain,[-(51 ^ [] = 50 ^ [])],extension(4)).
% 112.05/108.96 cnf('1.2',plain,[-(ssList(48 ^ []))],extension(1)).
% 112.05/108.96 cnf('1.3',plain,[-(neq(48 ^ [], nil)), neq(49 ^ [], nil), 49 ^ [] = 48 ^ [], nil = nil],extension(13,bind([[_61309, _61376, _61442, _61507], [49 ^ [], 48 ^ [], nil, nil]]))).
% 112.05/108.96 cnf('1.3.1',plain,[-(neq(49 ^ [], nil)), -(nil = 49 ^ [])],extension(5)).
% 112.05/108.96 cnf('1.3.1.1',plain,[nil = 49 ^ [], -(49 ^ [] = nil)],extension(11,bind([[_55868, _55823], [49 ^ [], nil]]))).
% 112.05/108.96 cnf('1.3.1.1.1',plain,[49 ^ [] = nil, -(49 ^ [] = 48 ^ []), nil = 48 ^ []],extension(12,bind([[_56102, _56158, _56213], [49 ^ [], nil, 48 ^ []]]))).
% 112.05/108.96 cnf('1.3.1.1.1.1',plain,[49 ^ [] = 48 ^ [], -(nil = 48 ^ []), nil = 49 ^ []],extension(12,bind([[_56213, _56102, _56158], [48 ^ [], nil, 49 ^ []]]))).
% 112.05/108.96 cnf('1.3.1.1.1.1.1',plain,[nil = 48 ^ [], -(neq(49 ^ [], nil))],extension(7)).
% 112.05/108.96 cnf('1.3.1.1.1.1.1.1',plain,[neq(49 ^ [], nil)],reduction('1.3')).
% 112.05/108.96 cnf('1.3.1.1.1.1.2',plain,[-(nil = 49 ^ [])],reduction('1.3.1')).
% 112.05/108.96 cnf('1.3.1.1.1.2',plain,[-(nil = 48 ^ [])],lemmata('1')).
% 112.05/108.96 cnf('1.3.2',plain,[-(49 ^ [] = 48 ^ []), 48 ^ [] = 49 ^ []],extension(11,bind([[_55823, _55868], [48 ^ [], 49 ^ []]]))).
% 112.05/108.96 cnf('1.3.2.1',plain,[-(48 ^ [] = 49 ^ []), 48 ^ [] = 50 ^ [], 50 ^ [] = 49 ^ []],extension(12,bind([[_56102, _56158, _56213], [48 ^ [], 50 ^ [], 49 ^ []]]))).
% 112.05/108.96 cnf('1.3.2.1.1',plain,[-(48 ^ [] = 50 ^ [])],extension(3)).
% 112.05/108.96 cnf('1.3.2.1.2',plain,[-(50 ^ [] = 49 ^ []), 49 ^ [] = 50 ^ []],extension(11,bind([[_55823, _55868], [49 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.3.2.1.2.1',plain,[-(49 ^ [] = 50 ^ []), 49 ^ [] = 51 ^ [], 51 ^ [] = 50 ^ []],extension(12,bind([[_56102, _56158, _56213], [49 ^ [], 51 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.3.2.1.2.1.1',plain,[-(49 ^ [] = 51 ^ [])],extension(2)).
% 112.05/108.96 cnf('1.3.2.1.2.1.2',plain,[-(51 ^ [] = 50 ^ [])],extension(4)).
% 112.05/108.96 cnf('1.3.3',plain,[-(nil = nil)],extension(10,bind([[_55670], [nil]]))).
% 112.05/108.96 cnf('1.4',plain,[-(rearsegP(49 ^ [], 48 ^ [])), rearsegP(50 ^ [], 50 ^ []), 50 ^ [] = 49 ^ [], 50 ^ [] = 48 ^ []],extension(14,bind([[_61933, _62000, _62066, _62131], [50 ^ [], 49 ^ [], 50 ^ [], 48 ^ []]]))).
% 112.05/108.96 cnf('1.4.1',plain,[-(rearsegP(50 ^ [], 50 ^ [])), rearsegP(50 ^ [], 50 ^ []), 50 ^ [] = 50 ^ [], 50 ^ [] = 50 ^ []],extension(14,bind([[_61933, _62000, _62066, _62131], [50 ^ [], 50 ^ [], 50 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.4.1.1',plain,[-(rearsegP(50 ^ [], 50 ^ [])), rearsegP(50 ^ [], 50 ^ []), 50 ^ [] = 50 ^ [], 50 ^ [] = 50 ^ []],extension(14,bind([[_61933, _62000, _62066, _62131], [50 ^ [], 50 ^ [], 50 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.4.1.1.1',plain,[-(rearsegP(50 ^ [], 50 ^ [])), rearsegP(48 ^ [], 48 ^ []), 48 ^ [] = 50 ^ [], 48 ^ [] = 50 ^ []],extension(14,bind([[_61933, _62000, _62066, _62131], [48 ^ [], 50 ^ [], 48 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.4.1.1.1.1',plain,[-(rearsegP(48 ^ [], 48 ^ [])), ssList(48 ^ [])],extension(19,bind([[_97038], [48 ^ []]]))).
% 112.05/108.96 cnf('1.4.1.1.1.1.1',plain,[-(ssList(48 ^ []))],extension(1)).
% 112.05/108.96 cnf('1.4.1.1.1.2',plain,[-(48 ^ [] = 50 ^ [])],extension(3)).
% 112.05/108.96 cnf('1.4.1.1.1.3',plain,[-(48 ^ [] = 50 ^ [])],extension(3)).
% 112.05/108.96 cnf('1.4.1.1.2',plain,[-(50 ^ [] = 50 ^ [])],extension(10,bind([[_55670], [50 ^ []]]))).
% 112.05/108.96 cnf('1.4.1.1.3',plain,[-(50 ^ [] = 50 ^ [])],extension(10,bind([[_55670], [50 ^ []]]))).
% 112.05/108.96 cnf('1.4.1.2',plain,[-(50 ^ [] = 50 ^ [])],extension(10,bind([[_55670], [50 ^ []]]))).
% 112.05/108.96 cnf('1.4.1.3',plain,[-(50 ^ [] = 50 ^ [])],extension(10,bind([[_55670], [50 ^ []]]))).
% 112.05/108.96 cnf('1.4.2',plain,[-(50 ^ [] = 49 ^ []), 49 ^ [] = 50 ^ []],extension(11,bind([[_55823, _55868], [49 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.4.2.1',plain,[-(49 ^ [] = 50 ^ []), 49 ^ [] = 51 ^ [], 51 ^ [] = 50 ^ []],extension(12,bind([[_56102, _56158, _56213], [49 ^ [], 51 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.4.2.1.1',plain,[-(49 ^ [] = 51 ^ [])],extension(2)).
% 112.05/108.96 cnf('1.4.2.1.2',plain,[-(51 ^ [] = 50 ^ [])],extension(4)).
% 112.05/108.96 cnf('1.4.3',plain,[-(50 ^ [] = 48 ^ []), 48 ^ [] = 50 ^ []],extension(11,bind([[_55823, _55868], [48 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.4.3.1',plain,[-(48 ^ [] = 50 ^ [])],extension(3)).
% 112.05/108.96 cnf('1.5',plain,[-(rearsegP(48 ^ [], 48 ^ [])), rearsegP(50 ^ [], 50 ^ []), 50 ^ [] = 48 ^ [], 50 ^ [] = 48 ^ []],extension(14,bind([[_61933, _62000, _62066, _62131], [50 ^ [], 48 ^ [], 50 ^ [], 48 ^ []]]))).
% 112.05/108.96 cnf('1.5.1',plain,[-(rearsegP(50 ^ [], 50 ^ [])), rearsegP(50 ^ [], 50 ^ []), 50 ^ [] = 50 ^ [], 50 ^ [] = 50 ^ []],extension(14,bind([[_61933, _62000, _62066, _62131], [50 ^ [], 50 ^ [], 50 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.5.1.1',plain,[-(rearsegP(50 ^ [], 50 ^ [])), rearsegP(50 ^ [], 50 ^ []), 50 ^ [] = 50 ^ [], 50 ^ [] = 50 ^ []],extension(14,bind([[_61933, _62000, _62066, _62131], [50 ^ [], 50 ^ [], 50 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.5.1.1.1',plain,[-(rearsegP(50 ^ [], 50 ^ [])), rearsegP(48 ^ [], 48 ^ []), 48 ^ [] = 50 ^ [], 48 ^ [] = 50 ^ []],extension(14,bind([[_61933, _62000, _62066, _62131], [48 ^ [], 50 ^ [], 48 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.5.1.1.1.1',plain,[-(rearsegP(48 ^ [], 48 ^ [])), ssList(48 ^ [])],extension(19,bind([[_97038], [48 ^ []]]))).
% 112.05/108.96 cnf('1.5.1.1.1.1.1',plain,[-(ssList(48 ^ []))],extension(1)).
% 112.05/108.96 cnf('1.5.1.1.1.2',plain,[-(48 ^ [] = 50 ^ [])],extension(3)).
% 112.05/108.96 cnf('1.5.1.1.1.3',plain,[-(48 ^ [] = 50 ^ [])],extension(3)).
% 112.05/108.96 cnf('1.5.1.1.2',plain,[-(50 ^ [] = 50 ^ [])],extension(10,bind([[_55670], [50 ^ []]]))).
% 112.05/108.96 cnf('1.5.1.1.3',plain,[-(50 ^ [] = 50 ^ [])],extension(10,bind([[_55670], [50 ^ []]]))).
% 112.05/108.96 cnf('1.5.1.2',plain,[-(50 ^ [] = 50 ^ [])],extension(10,bind([[_55670], [50 ^ []]]))).
% 112.05/108.96 cnf('1.5.1.3',plain,[-(50 ^ [] = 50 ^ [])],extension(10,bind([[_55670], [50 ^ []]]))).
% 112.05/108.96 cnf('1.5.2',plain,[-(50 ^ [] = 48 ^ []), 48 ^ [] = 50 ^ []],extension(11,bind([[_55823, _55868], [48 ^ [], 50 ^ []]]))).
% 112.05/108.96 cnf('1.5.2.1',plain,[-(48 ^ [] = 50 ^ [])],extension(3)).
% 112.05/108.96 cnf('1.5.3',plain,[-(50 ^ [] = 48 ^ [])],lemmata('1.5')).
% 112.05/108.96 %-----------------------------------------------------
% 112.05/108.97
% 112.05/108.97 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------