%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NUN070+2 : TPTP v8.1.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n026.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 : Mon Jul 18 16:33:37 EDT 2022
% Result : Theorem 0.36s 1.44s
% Output : Proof 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : NUN070+2 : TPTP v8.1.0. Released v7.3.0.
% 0.12/0.14 % Command : leancop_casc.sh %s %d
% 0.15/0.36 % Computer : n026.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 600
% 0.15/0.36 % DateTime : Thu Jun 2 10:04:42 EDT 2022
% 0.15/0.36 % CPUTime :
% 0.36/1.44 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.45 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.45
% 0.36/1.45 %-----------------------------------------------------
% 0.36/1.45 fof(onepluszeroeqone, conjecture, ? [_32292] : (? [_32300] : (? [_32308] : (r1(_32308) & r3(_32300, _32308, _32292)) & ? [_32336] : (r1(_32336) & r2(_32336, _32300))) & ? [_32361] : (_32292 = _32361 & ? [_32375] : (r1(_32375) & r2(_32375, _32361)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', onepluszeroeqone)).
% 0.36/1.45 fof(axiom_1a, axiom, ! [_32707, _32710] : ? [_32718] : (? [_32726] : (? [_32734] : (r2(_32710, _32734) & r3(_32707, _32734, _32726)) & _32726 = _32718) & ? [_32771] : (r2(_32771, _32718) & r3(_32707, _32710, _32771))), file('/export/starexec/sandbox2/benchmark/Axioms/NUM008+0.ax', axiom_1a)).
% 0.36/1.45 fof(axiom_4a, axiom, ! [_33077] : ? [_33085] : (? [_33093] : (r1(_33093) & r3(_33077, _33093, _33085)) & _33085 = _33077), file('/export/starexec/sandbox2/benchmark/Axioms/NUM008+0.ax', axiom_4a)).
% 0.36/1.45
% 0.36/1.45 cnf(1, plain, [r2(_22423, _22309), r1(_22423), _21752 = _22309, r3(_21856, _21932, _21752), r1(_21932), r1(_22130), r2(_22130, _21856)], clausify(onepluszeroeqone)).
% 0.36/1.45 cnf(2, plain, [-(r2(_16824, 7 ^ [_16824, _16739]))], clausify(axiom_1a)).
% 0.36/1.45 cnf(3, plain, [-(r1(14 ^ [_19442]))], clausify(axiom_4a)).
% 0.36/1.45 cnf(4, plain, [-(r3(_19442, 14 ^ [_19442], 13 ^ [_19442]))], clausify(axiom_4a)).
% 0.36/1.45 cnf(5, plain, [-(13 ^ [_19442] = _19442)], clausify(axiom_4a)).
% 0.36/1.45
% 0.36/1.45 cnf('1',plain,[r2(14 ^ [_29322], 7 ^ [14 ^ [_29322], _29301]), r1(14 ^ [_29322]), 13 ^ [7 ^ [14 ^ [_29322], _29301]] = 7 ^ [14 ^ [_29322], _29301], r3(7 ^ [14 ^ [_29322], _29301], 14 ^ [7 ^ [14 ^ [_29322], _29301]], 13 ^ [7 ^ [14 ^ [_29322], _29301]]), r1(14 ^ [7 ^ [14 ^ [_29322], _29301]]), r1(14 ^ [_29322]), r2(14 ^ [_29322], 7 ^ [14 ^ [_29322], _29301])],start(1,bind([[_22423, _22309, _21752, _21932, _22130, _21856], [14 ^ [_29322], 7 ^ [14 ^ [_29322], _29301], 13 ^ [7 ^ [14 ^ [_29322], _29301]], 14 ^ [7 ^ [14 ^ [_29322], _29301]], 14 ^ [_29322], 7 ^ [14 ^ [_29322], _29301]]]))).
% 0.36/1.45 cnf('1.1',plain,[-(r2(14 ^ [_29322], 7 ^ [14 ^ [_29322], _29301]))],extension(2,bind([[_16824, _16739], [14 ^ [_29322], _29301]]))).
% 0.36/1.45 cnf('1.2',plain,[-(r1(14 ^ [_29322]))],extension(3,bind([[_19442], [_29322]]))).
% 0.36/1.45 cnf('1.3',plain,[-(13 ^ [7 ^ [14 ^ [_29322], _29301]] = 7 ^ [14 ^ [_29322], _29301])],extension(5,bind([[_19442], [7 ^ [14 ^ [_29322], _29301]]]))).
% 0.36/1.45 cnf('1.4',plain,[-(r3(7 ^ [14 ^ [_29322], _29301], 14 ^ [7 ^ [14 ^ [_29322], _29301]], 13 ^ [7 ^ [14 ^ [_29322], _29301]]))],extension(4,bind([[_19442], [7 ^ [14 ^ [_29322], _29301]]]))).
% 0.36/1.45 cnf('1.5',plain,[-(r1(14 ^ [7 ^ [14 ^ [_29322], _29301]]))],extension(3,bind([[_19442], [7 ^ [14 ^ [_29322], _29301]]]))).
% 0.36/1.45 cnf('1.6',plain,[-(r1(14 ^ [_29322]))],extension(3,bind([[_19442], [_29322]]))).
% 0.36/1.45 cnf('1.7',plain,[-(r2(14 ^ [_29322], 7 ^ [14 ^ [_29322], _29301]))],extension(2,bind([[_16824, _16739], [14 ^ [_29322], _29301]]))).
% 0.36/1.45 %-----------------------------------------------------
% 0.36/1.46
% 0.46/1.46 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------