%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : ALG030+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n029.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:33 EDT 2022
% Result : Theorem 0.57s 1.39s
% Output : Proof 0.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ALG030+1 : TPTP v8.1.0. Released v2.7.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n029.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Thu Jun 9 00:39:36 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.57/1.39 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.57/1.40 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.57/1.40
% 0.57/1.40 %-----------------------------------------------------
% 0.57/1.40 fof(co1, conjecture, ! [_25524] : (sorti1(_25524) => sorti2(h(_25524))) & ! [_25550] : (sorti2(_25550) => sorti1(j(_25550))) => ~ (! [_25578] : (sorti1(_25578) => ! [_25593] : (sorti1(_25593) => h(op1(_25578, _25593)) = op2(h(_25578), h(_25593)))) & ! [_25640] : (sorti2(_25640) => ! [_25655] : (sorti2(_25655) => j(op2(_25640, _25655)) = op1(j(_25640), j(_25655)))) & ! [_25702] : (sorti2(_25702) => h(j(_25702)) = _25702) & ! [_25731] : (sorti1(_25731) => j(h(_25731)) = _25731)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 0.57/1.40 fof(ax3, axiom, ~ ! [_26327] : (sorti1(_26327) => ! [_26342] : (sorti1(_26342) => op1(_26327, _26342) = op1(_26342, _26327))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax3)).
% 0.57/1.40 fof(ax4, axiom, ~ ~ ! [_26567] : (sorti2(_26567) => ! [_26582] : (sorti2(_26582) => op2(_26567, _26582) = op2(_26582, _26567))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax4)).
% 0.57/1.40
% 0.57/1.40 cnf(1, plain, [sorti1(_11754), -(sorti2(h(_11754)))], clausify(co1)).
% 0.57/1.40 cnf(2, plain, [sorti2(_12492), sorti2(_12591), -(j(op2(_12492, _12591)) = op1(j(_12492), j(_12591)))], clausify(co1)).
% 0.57/1.40 cnf(3, plain, [sorti1(_13093), -(j(h(_13093)) = _13093)], clausify(co1)).
% 0.57/1.40 cnf(4, plain, [-(sorti1(1 ^ []))], clausify(ax3)).
% 0.57/1.40 cnf(5, plain, [-(sorti1(2 ^ []))], clausify(ax3)).
% 0.57/1.40 cnf(6, plain, [op1(1 ^ [], 2 ^ []) = op1(2 ^ [], 1 ^ [])], clausify(ax3)).
% 0.57/1.40 cnf(7, plain, [sorti2(_11237), sorti2(_11330), -(op2(_11237, _11330) = op2(_11330, _11237))], clausify(ax4)).
% 0.57/1.40 cnf(8, plain, [_8406 = _8455, -(j(_8406) = j(_8455))], theory(equality)).
% 0.57/1.40 cnf(9, plain, [-(op1(_8735, _8868) = op1(_8802, _8933)), _8735 = _8802, _8868 = _8933], theory(equality)).
% 0.57/1.40 cnf(10, plain, [_6644 = _6689, -(_6689 = _6644)], theory(equality)).
% 0.57/1.40 cnf(11, plain, [-(_6923 = _7034), _6923 = _6979, _6979 = _7034], theory(equality)).
% 0.57/1.40
% 0.57/1.40 cnf('1',plain,[op1(1 ^ [], 2 ^ []) = op1(2 ^ [], 1 ^ [])],start(6)).
% 0.57/1.40 cnf('1.1',plain,[-(op1(1 ^ [], 2 ^ []) = op1(2 ^ [], 1 ^ [])), op1(1 ^ [], 2 ^ []) = j(op2(h(1 ^ []), h(2 ^ []))), j(op2(h(1 ^ []), h(2 ^ []))) = op1(2 ^ [], 1 ^ [])],extension(11,bind([[_6923, _6979, _7034], [op1(1 ^ [], 2 ^ []), j(op2(h(1 ^ []), h(2 ^ []))), op1(2 ^ [], 1 ^ [])]]))).
% 0.57/1.40 cnf('1.1.1',plain,[-(op1(1 ^ [], 2 ^ []) = j(op2(h(1 ^ []), h(2 ^ [])))), j(op2(h(1 ^ []), h(2 ^ []))) = op1(1 ^ [], 2 ^ [])],extension(10,bind([[_6644, _6689], [j(op2(h(1 ^ []), h(2 ^ []))), op1(1 ^ [], 2 ^ [])]]))).
% 0.57/1.40 cnf('1.1.1.1',plain,[-(j(op2(h(1 ^ []), h(2 ^ []))) = op1(1 ^ [], 2 ^ [])), j(op2(h(1 ^ []), h(2 ^ []))) = op1(j(h(1 ^ [])), j(h(2 ^ []))), op1(j(h(1 ^ [])), j(h(2 ^ []))) = op1(1 ^ [], 2 ^ [])],extension(11,bind([[_6923, _6979, _7034], [j(op2(h(1 ^ []), h(2 ^ []))), op1(j(h(1 ^ [])), j(h(2 ^ []))), op1(1 ^ [], 2 ^ [])]]))).
% 0.57/1.40 cnf('1.1.1.1.1',plain,[-(j(op2(h(1 ^ []), h(2 ^ []))) = op1(j(h(1 ^ [])), j(h(2 ^ [])))), sorti2(h(1 ^ [])), sorti2(h(2 ^ []))],extension(2,bind([[_12492, _12591], [h(1 ^ []), h(2 ^ [])]]))).
% 0.57/1.40 cnf('1.1.1.1.1.1',plain,[-(sorti2(h(1 ^ []))), sorti1(1 ^ [])],extension(1,bind([[_11754], [1 ^ []]]))).
% 0.57/1.40 cnf('1.1.1.1.1.1.1',plain,[-(sorti1(1 ^ []))],extension(4)).
% 0.57/1.40 cnf('1.1.1.1.1.2',plain,[-(sorti2(h(2 ^ []))), sorti1(2 ^ [])],extension(1,bind([[_11754], [2 ^ []]]))).
% 0.57/1.40 cnf('1.1.1.1.1.2.1',plain,[-(sorti1(2 ^ []))],extension(5)).
% 0.57/1.40 cnf('1.1.1.1.2',plain,[-(op1(j(h(1 ^ [])), j(h(2 ^ []))) = op1(1 ^ [], 2 ^ [])), j(h(1 ^ [])) = 1 ^ [], j(h(2 ^ [])) = 2 ^ []],extension(9,bind([[_8735, _8802, _8868, _8933], [j(h(1 ^ [])), 1 ^ [], j(h(2 ^ [])), 2 ^ []]]))).
% 0.57/1.40 cnf('1.1.1.1.2.1',plain,[-(j(h(1 ^ [])) = 1 ^ []), sorti1(1 ^ [])],extension(3,bind([[_13093], [1 ^ []]]))).
% 0.57/1.40 cnf('1.1.1.1.2.1.1',plain,[-(sorti1(1 ^ []))],extension(4)).
% 0.57/1.40 cnf('1.1.1.1.2.2',plain,[-(j(h(2 ^ [])) = 2 ^ []), sorti1(2 ^ [])],extension(3,bind([[_13093], [2 ^ []]]))).
% 0.57/1.40 cnf('1.1.1.1.2.2.1',plain,[-(sorti1(2 ^ []))],extension(5)).
% 0.57/1.40 cnf('1.1.2',plain,[-(j(op2(h(1 ^ []), h(2 ^ []))) = op1(2 ^ [], 1 ^ [])), j(op2(h(1 ^ []), h(2 ^ []))) = j(op2(h(2 ^ []), h(1 ^ []))), j(op2(h(2 ^ []), h(1 ^ []))) = op1(2 ^ [], 1 ^ [])],extension(11,bind([[_6923, _6979, _7034], [j(op2(h(1 ^ []), h(2 ^ []))), j(op2(h(2 ^ []), h(1 ^ []))), op1(2 ^ [], 1 ^ [])]]))).
% 0.57/1.40 cnf('1.1.2.1',plain,[-(j(op2(h(1 ^ []), h(2 ^ []))) = j(op2(h(2 ^ []), h(1 ^ [])))), op2(h(1 ^ []), h(2 ^ [])) = op2(h(2 ^ []), h(1 ^ []))],extension(8,bind([[_8406, _8455], [op2(h(1 ^ []), h(2 ^ [])), op2(h(2 ^ []), h(1 ^ []))]]))).
% 0.57/1.40 cnf('1.1.2.1.1',plain,[-(op2(h(1 ^ []), h(2 ^ [])) = op2(h(2 ^ []), h(1 ^ []))), sorti2(h(1 ^ [])), sorti2(h(2 ^ []))],extension(7,bind([[_11237, _11330], [h(1 ^ []), h(2 ^ [])]]))).
% 0.57/1.40 cnf('1.1.2.1.1.1',plain,[-(sorti2(h(1 ^ []))), sorti1(1 ^ [])],extension(1,bind([[_11754], [1 ^ []]]))).
% 0.57/1.40 cnf('1.1.2.1.1.1.1',plain,[-(sorti1(1 ^ []))],extension(4)).
% 0.57/1.40 cnf('1.1.2.1.1.2',plain,[-(sorti2(h(2 ^ []))), sorti1(2 ^ [])],extension(1,bind([[_11754], [2 ^ []]]))).
% 0.57/1.40 cnf('1.1.2.1.1.2.1',plain,[-(sorti1(2 ^ []))],extension(5)).
% 0.57/1.40 cnf('1.1.2.2',plain,[-(j(op2(h(2 ^ []), h(1 ^ []))) = op1(2 ^ [], 1 ^ [])), j(op2(h(2 ^ []), h(1 ^ []))) = op1(j(h(2 ^ [])), j(h(1 ^ []))), op1(j(h(2 ^ [])), j(h(1 ^ []))) = op1(2 ^ [], 1 ^ [])],extension(11,bind([[_6923, _6979, _7034], [j(op2(h(2 ^ []), h(1 ^ []))), op1(j(h(2 ^ [])), j(h(1 ^ []))), op1(2 ^ [], 1 ^ [])]]))).
% 0.57/1.40 cnf('1.1.2.2.1',plain,[-(j(op2(h(2 ^ []), h(1 ^ []))) = op1(j(h(2 ^ [])), j(h(1 ^ [])))), sorti2(h(2 ^ [])), sorti2(h(1 ^ []))],extension(2,bind([[_12492, _12591], [h(2 ^ []), h(1 ^ [])]]))).
% 0.57/1.40 cnf('1.1.2.2.1.1',plain,[-(sorti2(h(2 ^ []))), sorti1(2 ^ [])],extension(1,bind([[_11754], [2 ^ []]]))).
% 0.57/1.40 cnf('1.1.2.2.1.1.1',plain,[-(sorti1(2 ^ []))],extension(5)).
% 0.57/1.40 cnf('1.1.2.2.1.2',plain,[-(sorti2(h(1 ^ []))), sorti1(1 ^ [])],extension(1,bind([[_11754], [1 ^ []]]))).
% 0.57/1.40 cnf('1.1.2.2.1.2.1',plain,[-(sorti1(1 ^ []))],extension(4)).
% 0.57/1.40 cnf('1.1.2.2.2',plain,[-(op1(j(h(2 ^ [])), j(h(1 ^ []))) = op1(2 ^ [], 1 ^ [])), j(h(2 ^ [])) = 2 ^ [], j(h(1 ^ [])) = 1 ^ []],extension(9,bind([[_8735, _8802, _8868, _8933], [j(h(2 ^ [])), 2 ^ [], j(h(1 ^ [])), 1 ^ []]]))).
% 0.57/1.40 cnf('1.1.2.2.2.1',plain,[-(j(h(2 ^ [])) = 2 ^ []), sorti1(2 ^ [])],extension(3,bind([[_13093], [2 ^ []]]))).
% 0.57/1.40 cnf('1.1.2.2.2.1.1',plain,[-(sorti1(2 ^ []))],extension(5)).
% 0.57/1.40 cnf('1.1.2.2.2.2',plain,[-(j(h(1 ^ [])) = 1 ^ []), sorti1(1 ^ [])],extension(3,bind([[_13093], [1 ^ []]]))).
% 0.57/1.40 cnf('1.1.2.2.2.2.1',plain,[-(sorti1(1 ^ []))],extension(4)).
% 0.57/1.40 %-----------------------------------------------------
% 0.57/1.41
% 0.57/1.41 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------