%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWX048+1 : TPTP v9.1.0. Released v9.1.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 : 300s
% DateTime : Tue Apr 1 02:14:33 AM UTC 2025
% Result : Theorem 118.30s 114.43s
% Output : Proof 118.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWX048+1 : TPTP v9.1.0. Released v9.1.0.
% 0.11/0.12 % 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 : 300
% 0.12/0.34 % DateTime : Mon Mar 31 14:57:58 EDT 2025
% 0.12/0.34 % CPUTime :
% 118.30/114.43 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 118.30/114.44 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 118.30/114.44
% 118.30/114.44 %-----------------------------------------------------
% 118.30/114.44 fof('lemma-(occ:cons:diff)', conjecture, ! [_183115, _183118, _183121] : (list_succeeds(_183121) & (! _183115) = _183118 => occ(_183115, cons(_183118, _183121)) = occ(_183115, _183121)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'lemma-(occ:cons:diff)')).
% 118.30/114.44 fof(id49, axiom, ! [_183519, _183522, _183525] : (occ_succeeds(_183519, _183522, _183525) <=> ? [_183546, _183549] : (_183522 = cons(_183546, _183549) & (! _183519) = _183546 & occ_succeeds(_183519, _183549, _183525)) | ? [_183591, _183594] : (_183522 = cons(_183519, _183591) & _183525 = s(_183594) & occ_succeeds(_183519, _183591, _183594)) | _183522 = nil & _183525 = '0'), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', id49)).
% 118.30/114.44 fof('occ/2', axiom, ! [_184550, _184553, _184556] : (list_succeeds(_184553) => (occ(_184550, _184553) = _184556 <=> occ_succeeds(_184550, _184553, _184556))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'occ/2')).
% 118.30/114.44 fof('lemma-(occ:types)', axiom, ! [_184769, _184772, _184775] : (occ_succeeds(_184769, _184772, _184775) => list_succeeds(_184772) & nat_succeeds(_184775)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'lemma-(occ:types)')).
% 118.30/114.44
% 118.30/114.44 cnf(1, plain, [-(list_succeeds(134 ^ []))], clausify('lemma-(occ:cons:diff)')).
% 118.30/114.44 cnf(2, plain, [132 ^ [] = 133 ^ []], clausify('lemma-(occ:cons:diff)')).
% 118.30/114.44 cnf(3, plain, [occ(132 ^ [], cons(133 ^ [], 134 ^ [])) = occ(132 ^ [], 134 ^ [])], clausify('lemma-(occ:cons:diff)')).
% 118.30/114.44 cnf(4, plain, [-(cons(_20050, _20052) = cons(_20051, _20053)), _20050 = _20051, _20052 = _20053], theory(equality)).
% 118.30/114.44 cnf(5, plain, [-(_17006 = _17006)], theory(equality)).
% 118.30/114.44 cnf(6, plain, [-(occ_succeeds(_21721, _21722, _21723)), _21722 = cons(_21728, _21729), -(_21721 = _21728), occ_succeeds(_21721, _21729, _21723)], clausify(id49)).
% 118.30/114.44 cnf(7, plain, [list_succeeds(_31762), occ(_31761, _31762) = _31763, -(occ_succeeds(_31761, _31762, _31763))], clausify('occ/2')).
% 118.30/114.44 cnf(8, plain, [list_succeeds(_31762), -(occ(_31761, _31762) = _31763), occ_succeeds(_31761, _31762, _31763)], clausify('occ/2')).
% 118.30/114.44 cnf(9, plain, [occ_succeeds(_32144, _32145, _32146), -(list_succeeds(_32145))], clausify('lemma-(occ:types)')).
% 118.30/114.44
% 118.30/114.44 cnf('1',plain,[132 ^ [] = 133 ^ []],start(2)).
% 118.30/114.44 cnf('1.1',plain,[-(132 ^ [] = 133 ^ []), -(occ_succeeds(132 ^ [], cons(133 ^ [], 134 ^ []), occ(132 ^ [], 134 ^ []))), cons(133 ^ [], 134 ^ []) = cons(133 ^ [], 134 ^ []), occ_succeeds(132 ^ [], 134 ^ [], occ(132 ^ [], 134 ^ []))],extension(6,bind([[_21722, _21728, _21721, _21729, _21723], [cons(133 ^ [], 134 ^ []), 133 ^ [], 132 ^ [], 134 ^ [], occ(132 ^ [], 134 ^ [])]]))).
% 118.30/114.44 cnf('1.1.1',plain,[occ_succeeds(132 ^ [], cons(133 ^ [], 134 ^ []), occ(132 ^ [], 134 ^ [])), list_succeeds(cons(133 ^ [], 134 ^ [])), -(occ(132 ^ [], cons(133 ^ [], 134 ^ [])) = occ(132 ^ [], 134 ^ []))],extension(8,bind([[_31761, _31762, _31763], [132 ^ [], cons(133 ^ [], 134 ^ []), occ(132 ^ [], 134 ^ [])]]))).
% 118.30/114.44 cnf('1.1.1.1',plain,[-(list_succeeds(cons(133 ^ [], 134 ^ []))), occ_succeeds(132 ^ [], cons(133 ^ [], 134 ^ []), occ(132 ^ [], 134 ^ []))],extension(9,bind([[_32144, _32145, _32146], [132 ^ [], cons(133 ^ [], 134 ^ []), occ(132 ^ [], 134 ^ [])]]))).
% 118.30/114.44 cnf('1.1.1.1.1',plain,[-(occ_succeeds(132 ^ [], cons(133 ^ [], 134 ^ []), occ(132 ^ [], 134 ^ [])))],reduction('1.1')).
% 118.30/114.44 cnf('1.1.1.2',plain,[occ(132 ^ [], cons(133 ^ [], 134 ^ [])) = occ(132 ^ [], 134 ^ [])],extension(3)).
% 118.30/114.44 cnf('1.1.2',plain,[-(cons(133 ^ [], 134 ^ []) = cons(133 ^ [], 134 ^ [])), 133 ^ [] = 133 ^ [], 134 ^ [] = 134 ^ []],extension(4,bind([[_20050, _20051, _20052, _20053], [133 ^ [], 133 ^ [], 134 ^ [], 134 ^ []]]))).
% 118.30/114.44 cnf('1.1.2.1',plain,[-(133 ^ [] = 133 ^ [])],extension(5,bind([[_17006], [133 ^ []]]))).
% 118.30/114.44 cnf('1.1.2.2',plain,[-(134 ^ [] = 134 ^ [])],extension(5,bind([[_17006], [134 ^ []]]))).
% 118.30/114.44 cnf('1.1.3',plain,[-(occ_succeeds(132 ^ [], 134 ^ [], occ(132 ^ [], 134 ^ []))), list_succeeds(134 ^ []), occ(132 ^ [], 134 ^ []) = occ(132 ^ [], 134 ^ [])],extension(7,bind([[_31761, _31762, _31763], [132 ^ [], 134 ^ [], occ(132 ^ [], 134 ^ [])]]))).
% 118.30/114.44 cnf('1.1.3.1',plain,[-(list_succeeds(134 ^ []))],extension(1)).
% 118.30/114.44 cnf('1.1.3.2',plain,[-(occ(132 ^ [], 134 ^ []) = occ(132 ^ [], 134 ^ []))],extension(5,bind([[_17006], [occ(132 ^ [], 134 ^ [])]]))).
% 118.30/114.44 %-----------------------------------------------------
% 118.30/114.45
% 118.30/114.45 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------