%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NUN080+1 : TPTP v8.1.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n025.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:39 EDT 2022
% Result : Theorem 0.36s 1.41s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUN080+1 : TPTP v8.1.0. Released v7.3.0.
% 0.00/0.12 % Command : leancop_casc.sh %s %d
% 0.13/0.33 % Computer : n025.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 : Thu Jun 2 06:03:14 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.36/1.41 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/1.41 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/1.42
% 0.36/1.42 %-----------------------------------------------------
% 0.36/1.42 fof(xplustwoidy, conjecture, ? [_34651, _34654, _34657] : (id(_34657, _34654) & ? [_34675] : (r3(_34651, _34675, _34657) & ? [_34696] : (r2(_34696, _34675) & ? [_34714] : (r1(_34714) & r2(_34714, _34696))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', xplustwoidy)).
% 0.36/1.42 fof(axiom_5, axiom, ! [_34990] : id(_34990, _34990), file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_5)).
% 0.36/1.42 fof(axiom_1a, axiom, ! [_35108, _35111] : ? [_35119] : (? [_35127] : (id(_35127, _35119) & ? [_35145] : (r2(_35111, _35145) & r3(_35108, _35145, _35127))) & ? [_35176] : (r2(_35176, _35119) & r3(_35108, _35111, _35176))), file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_1a)).
% 0.36/1.42 fof(axiom_4a, axiom, ! [_35493] : ? [_35501] : (id(_35501, _35493) & ? [_35519] : (r1(_35519) & r3(_35493, _35519, _35501))), file('/export/starexec/sandbox/benchmark/Axioms/NUM009+0.ax', axiom_4a)).
% 0.36/1.42
% 0.36/1.42 cnf(1, plain, [id(_23102, _23019), r3(_22935, _23243, _23102), r2(_23417, _23243), r1(_23543), r2(_23543, _23417)], clausify(xplustwoidy)).
% 0.36/1.42 cnf(2, plain, [-(id(_12348, _12348))], clausify(axiom_5)).
% 0.36/1.42 cnf(3, plain, [-(r2(_17917, 7 ^ [_17917, _17832]))], clausify(axiom_1a)).
% 0.36/1.42 cnf(4, plain, [-(r3(_17832, 7 ^ [_17917, _17832], 6 ^ [_17917, _17832]))], clausify(axiom_1a)).
% 0.36/1.42 cnf(5, plain, [-(r1(14 ^ [_20535]))], clausify(axiom_4a)).
% 0.36/1.42
% 0.36/1.42 cnf('1',plain,[id(6 ^ [7 ^ [14 ^ [_32300], _32323], _32206], 6 ^ [7 ^ [14 ^ [_32300], _32323], _32206]), r3(_32206, 7 ^ [7 ^ [14 ^ [_32300], _32323], _32206], 6 ^ [7 ^ [14 ^ [_32300], _32323], _32206]), r2(7 ^ [14 ^ [_32300], _32323], 7 ^ [7 ^ [14 ^ [_32300], _32323], _32206]), r1(14 ^ [_32300]), r2(14 ^ [_32300], 7 ^ [14 ^ [_32300], _32323])],start(1,bind([[_23019, _22935, _23102, _23243, _23543, _23417], [6 ^ [7 ^ [14 ^ [_32300], _32323], _32206], _32206, 6 ^ [7 ^ [14 ^ [_32300], _32323], _32206], 7 ^ [7 ^ [14 ^ [_32300], _32323], _32206], 14 ^ [_32300], 7 ^ [14 ^ [_32300], _32323]]]))).
% 0.36/1.42 cnf('1.1',plain,[-(id(6 ^ [7 ^ [14 ^ [_32300], _32323], _32206], 6 ^ [7 ^ [14 ^ [_32300], _32323], _32206]))],extension(2,bind([[_12348], [6 ^ [7 ^ [14 ^ [_32300], _32323], _32206]]]))).
% 0.36/1.42 cnf('1.2',plain,[-(r3(_32206, 7 ^ [7 ^ [14 ^ [_32300], _32323], _32206], 6 ^ [7 ^ [14 ^ [_32300], _32323], _32206]))],extension(4,bind([[_17917, _17832], [7 ^ [14 ^ [_32300], _32323], _32206]]))).
% 0.36/1.42 cnf('1.3',plain,[-(r2(7 ^ [14 ^ [_32300], _32323], 7 ^ [7 ^ [14 ^ [_32300], _32323], _32206]))],extension(3,bind([[_17917, _17832], [7 ^ [14 ^ [_32300], _32323], _32206]]))).
% 0.36/1.42 cnf('1.4',plain,[-(r1(14 ^ [_32300]))],extension(5,bind([[_20535], [_32300]]))).
% 0.36/1.42 cnf('1.5',plain,[-(r2(14 ^ [_32300], 7 ^ [14 ^ [_32300], _32323]))],extension(3,bind([[_17917, _17832], [14 ^ [_32300], _32323]]))).
% 0.36/1.42 %-----------------------------------------------------
% 0.36/1.42
% 0.36/1.43 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------