%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : ALG201+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n027.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 : Thu Jul 14 17:21:58 EDT 2022
% Result : Theorem 0.38s 1.40s
% Output : Proof 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : ALG201+1 : TPTP v8.1.0. Released v2.7.0.
% 0.10/0.12 % Command : leancop_casc.sh %s %d
% 0.13/0.33 % Computer : n027.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Wed Jun 8 11:23:26 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.38/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/1.40 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/1.41
% 0.38/1.41 %-----------------------------------------------------
% 0.38/1.41 fof(co1, conjecture, ! [_18230] : (sorti1(_18230) => sorti2(h(_18230))) & ! [_18256] : (sorti2(_18256) => sorti1(j(_18256))) => ~ (! [_18284] : (sorti1(_18284) => ! [_18299] : (sorti1(_18299) => h(op1(_18284, _18299)) = op2(h(_18284), h(_18299)))) & ! [_18346] : (sorti2(_18346) => ! [_18361] : (sorti2(_18361) => j(op2(_18346, _18361)) = op1(j(_18346), j(_18361)))) & ! [_18408] : (sorti2(_18408) => h(j(_18408)) = _18408) & ! [_18437] : (sorti1(_18437) => j(h(_18437)) = _18437)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 0.38/1.41 fof(ax4, axiom, ~ ! [_19021] : (sorti2(_19021) => (! op2(_19021, _19021)) = _19021), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax4)).
% 0.38/1.41 fof(ax3, axiom, ! [_19185] : (sorti1(_19185) => (! op1(_19185, _19185)) = _19185), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax3)).
% 0.38/1.41
% 0.38/1.41 cnf(1, plain, [sorti2(_11280), -(sorti1(j(_11280)))], clausify(co1)).
% 0.38/1.41 cnf(2, plain, [sorti2(_11874), sorti2(_11973), -(j(op2(_11874, _11973)) = op1(j(_11874), j(_11973)))], clausify(co1)).
% 0.38/1.41 cnf(3, plain, [-(sorti2(1 ^ []))], clausify(ax4)).
% 0.38/1.41 cnf(4, plain, [-(op2(1 ^ [], 1 ^ []) = 1 ^ [])], clausify(ax4)).
% 0.38/1.41 cnf(5, plain, [sorti1(_10480), op1(_10480, _10480) = _10480], clausify(ax3)).
% 0.38/1.41 cnf(6, plain, [_8102 = _8151, -(j(_8102) = j(_8151))], theory(equality)).
% 0.38/1.41 cnf(7, plain, [_6340 = _6385, -(_6385 = _6340)], theory(equality)).
% 0.38/1.41 cnf(8, plain, [-(_6619 = _6730), _6619 = _6675, _6675 = _6730], theory(equality)).
% 0.38/1.41
% 0.38/1.41 cnf('1',plain,[sorti1(j(1 ^ [])), op1(j(1 ^ []), j(1 ^ [])) = j(1 ^ [])],start(5,bind([[_10480], [j(1 ^ [])]]))).
% 0.38/1.41 cnf('1.1',plain,[-(sorti1(j(1 ^ []))), sorti2(1 ^ [])],extension(1,bind([[_11280], [1 ^ []]]))).
% 0.38/1.41 cnf('1.1.1',plain,[-(sorti2(1 ^ []))],extension(3)).
% 0.38/1.41 cnf('1.2',plain,[-(op1(j(1 ^ []), j(1 ^ [])) = j(1 ^ [])), op1(j(1 ^ []), j(1 ^ [])) = j(op2(1 ^ [], 1 ^ [])), j(op2(1 ^ [], 1 ^ [])) = j(1 ^ [])],extension(8,bind([[_6619, _6675, _6730], [op1(j(1 ^ []), j(1 ^ [])), j(op2(1 ^ [], 1 ^ [])), j(1 ^ [])]]))).
% 0.38/1.41 cnf('1.2.1',plain,[-(op1(j(1 ^ []), j(1 ^ [])) = j(op2(1 ^ [], 1 ^ []))), j(op2(1 ^ [], 1 ^ [])) = op1(j(1 ^ []), j(1 ^ []))],extension(7,bind([[_6340, _6385], [j(op2(1 ^ [], 1 ^ [])), op1(j(1 ^ []), j(1 ^ []))]]))).
% 0.38/1.41 cnf('1.2.1.1',plain,[-(j(op2(1 ^ [], 1 ^ [])) = op1(j(1 ^ []), j(1 ^ []))), sorti2(1 ^ []), sorti2(1 ^ [])],extension(2,bind([[_11874, _11973], [1 ^ [], 1 ^ []]]))).
% 0.38/1.41 cnf('1.2.1.1.1',plain,[-(sorti2(1 ^ []))],extension(3)).
% 0.38/1.41 cnf('1.2.1.1.2',plain,[-(sorti2(1 ^ []))],extension(3)).
% 0.38/1.41 cnf('1.2.2',plain,[-(j(op2(1 ^ [], 1 ^ [])) = j(1 ^ [])), op2(1 ^ [], 1 ^ []) = 1 ^ []],extension(6,bind([[_8102, _8151], [op2(1 ^ [], 1 ^ []), 1 ^ []]]))).
% 0.38/1.41 cnf('1.2.2.1',plain,[-(op2(1 ^ [], 1 ^ []) = 1 ^ [])],extension(4)).
% 0.38/1.41 %-----------------------------------------------------
% 0.38/1.41
% 0.38/1.41 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------