%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NUN068+1 : TPTP v8.1.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n019.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 29.72s 29.49s
% Output : Proof 29.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : NUN068+1 : TPTP v8.1.0. Released v7.3.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n019.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 : 600
% 0.12/0.34 % DateTime : Thu Jun 2 04:34:10 EDT 2022
% 0.12/0.34 % CPUTime :
% 29.72/29.49 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.72/29.50 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.72/29.50
% 29.72/29.50 %-----------------------------------------------------
% 29.72/29.50 fof(nonzerosnononesexistid, conjecture, ? [_42394] : (! [_42402] : (! [_42410] : (~ r1(_42410) | ~ r2(_42410, _42402)) | ~ id(_42394, _42402)) & ! [_42451] : (~ id(_42394, _42451) | ~ r1(_42451))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', nonzerosnononesexistid)).
% 29.72/29.50 fof(axiom_8, axiom, ! [_42785, _42788] : (~ id(_42785, _42788) | ~ r1(_42785) & ~ r1(_42788) | r1(_42785) & r1(_42788)), file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_8)).
% 29.72/29.50 fof(axiom_2, axiom, ! [_43029] : ? [_43037] : ! [_43045] : (id(_43045, _43037) & r2(_43029, _43045) | ~ r2(_43029, _43045) & ~ id(_43045, _43037)), file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_2)).
% 29.72/29.50 fof(axiom_5, axiom, ! [_43338] : id(_43338, _43338), file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_5)).
% 29.72/29.50 fof(axiom_6, axiom, ! [_43445, _43448] : (~ id(_43445, _43448) | id(_43448, _43445)), file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_6)).
% 29.72/29.50 fof(axiom_1a, axiom, ! [_43615, _43618] : ? [_43626] : (? [_43634] : (id(_43634, _43626) & ? [_43652] : (r2(_43618, _43652) & r3(_43615, _43652, _43634))) & ? [_43683] : (r2(_43683, _43626) & r3(_43615, _43618, _43683))), file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_1a)).
% 29.72/29.50 fof(axiom_3a, axiom, ! [_43987, _43990] : (! [_43998] : (! [_44006] : (~ id(_44006, _43998) | ~ r2(_43987, _44006)) | ~ r2(_43990, _43998)) | id(_43987, _43990)), file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_3a)).
% 29.72/29.50 fof(axiom_7a, axiom, ! [_44278, _44281] : (! [_44289] : (~ id(_44289, _44281) | ~ r1(_44289)) | ~ r2(_44278, _44281)), file('/export/starexec/sandbox2/benchmark/Axioms/NUM009+0.ax', axiom_7a)).
% 29.72/29.50
% 29.72/29.50 cnf(1, plain, [-(43 ^ [_22972]), -(r1(42 ^ [_22972]))], clausify(nonzerosnononesexistid)).
% 29.72/29.50 cnf(2, plain, [-(43 ^ [_22972]), -(id(_22972, 42 ^ [_22972]))], clausify(nonzerosnononesexistid)).
% 29.72/29.50 cnf(3, plain, [-(41 ^ [_22972]), -(id(_22972, 39 ^ [_22972]))], clausify(nonzerosnononesexistid)).
% 29.72/29.50 cnf(4, plain, [-(41 ^ [_22972]), -(r2(40 ^ [_22972], 39 ^ [_22972]))], clausify(nonzerosnononesexistid)).
% 29.72/29.50 cnf(5, plain, [-(41 ^ [_22972]), -(r1(40 ^ [_22972]))], clausify(nonzerosnononesexistid)).
% 29.72/29.50 cnf(6, plain, [-(14 ^ [_13465, _13400]), -(r1(_13400))], clausify(axiom_8)).
% 29.72/29.50 cnf(7, plain, [-(13 ^ [_13465, _13400]), r1(_13465)], clausify(axiom_8)).
% 29.72/29.50 cnf(8, plain, [-(6 ^ [_23900, _10217]), id(_23900, 4 ^ [_10217])], clausify(axiom_2)).
% 29.72/29.50 cnf(9, plain, [-(5 ^ [_23900, _10217]), -(r2(_10217, _23900))], clausify(axiom_2)).
% 29.72/29.50 cnf(10, plain, [41 ^ [_22972], 43 ^ [_22972]], clausify(nonzerosnononesexistid)).
% 29.72/29.50 cnf(11, plain, [5 ^ [_23900, _10217], 6 ^ [_23900, _10217]], clausify(axiom_2)).
% 29.72/29.50 cnf(12, plain, [-(id(_12385, _12385))], clausify(axiom_5)).
% 29.72/29.50 cnf(13, plain, [id(_12559, _12606), -(id(_12606, _12559))], clausify(axiom_6)).
% 29.72/29.50 cnf(14, plain, [id(_13400, _13465), 13 ^ [_13465, _13400], 14 ^ [_13465, _13400]], clausify(axiom_8)).
% 29.72/29.50 cnf(15, plain, [-(r2(_17954, 23 ^ [_17954, _17869]))], clausify(axiom_1a)).
% 29.72/29.50 cnf(16, plain, [-(id(_19875, _19948)), r2(_19948, _20030), id(_20105, _20030), r2(_19875, _20105)], clausify(axiom_3a)).
% 29.72/29.50 cnf(17, plain, [r2(_22225, _22286), id(_22356, _22286), r1(_22356)], clausify(axiom_7a)).
% 29.72/29.50
% 29.72/29.50 cnf('1',plain,[41 ^ [4 ^ [23 ^ [_32500, _32523]]], 43 ^ [4 ^ [23 ^ [_32500, _32523]]]],start(10,bind([[_22972], [4 ^ [23 ^ [_32500, _32523]]]]))).
% 29.72/29.50 cnf('1.1',plain,[-(41 ^ [4 ^ [23 ^ [_32500, _32523]]]), -(id(4 ^ [23 ^ [_32500, _32523]], 39 ^ [4 ^ [23 ^ [_32500, _32523]]]))],extension(3,bind([[_22972], [4 ^ [23 ^ [_32500, _32523]]]]))).
% 29.72/29.50 cnf('1.1.1',plain,[id(4 ^ [23 ^ [_32500, _32523]], 39 ^ [4 ^ [23 ^ [_32500, _32523]]]), -(id(39 ^ [4 ^ [23 ^ [_32500, _32523]]], 4 ^ [23 ^ [_32500, _32523]]))],extension(13,bind([[_12606, _12559], [39 ^ [4 ^ [23 ^ [_32500, _32523]]], 4 ^ [23 ^ [_32500, _32523]]]]))).
% 29.72/29.50 cnf('1.1.1.1',plain,[id(39 ^ [4 ^ [23 ^ [_32500, _32523]]], 4 ^ [23 ^ [_32500, _32523]]), -(6 ^ [39 ^ [4 ^ [23 ^ [_32500, _32523]]], 23 ^ [_32500, _32523]])],extension(8,bind([[_23900, _10217], [39 ^ [4 ^ [23 ^ [_32500, _32523]]], 23 ^ [_32500, _32523]]]))).
% 29.72/29.50 cnf('1.1.1.1.1',plain,[6 ^ [39 ^ [4 ^ [23 ^ [_32500, _32523]]], 23 ^ [_32500, _32523]], 5 ^ [39 ^ [4 ^ [23 ^ [_32500, _32523]]], 23 ^ [_32500, _32523]]],extension(11,bind([[_23900, _10217], [39 ^ [4 ^ [23 ^ [_32500, _32523]]], 23 ^ [_32500, _32523]]]))).
% 29.72/29.50 cnf('1.1.1.1.1.1',plain,[-(5 ^ [39 ^ [4 ^ [23 ^ [_32500, _32523]]], 23 ^ [_32500, _32523]]), -(r2(23 ^ [_32500, _32523], 39 ^ [4 ^ [23 ^ [_32500, _32523]]]))],extension(9,bind([[_10217, _23900], [23 ^ [_32500, _32523], 39 ^ [4 ^ [23 ^ [_32500, _32523]]]]]))).
% 29.72/29.50 cnf('1.1.1.1.1.1.1',plain,[r2(23 ^ [_32500, _32523], 39 ^ [4 ^ [23 ^ [_32500, _32523]]]), -(id(23 ^ [_32500, _32523], 40 ^ [4 ^ [23 ^ [_32500, _32523]]])), r2(40 ^ [4 ^ [23 ^ [_32500, _32523]]], 39 ^ [4 ^ [23 ^ [_32500, _32523]]]), id(39 ^ [4 ^ [23 ^ [_32500, _32523]]], 39 ^ [4 ^ [23 ^ [_32500, _32523]]])],extension(16,bind([[_19875, _19948, _20105, _20030], [23 ^ [_32500, _32523], 40 ^ [4 ^ [23 ^ [_32500, _32523]]], 39 ^ [4 ^ [23 ^ [_32500, _32523]]], 39 ^ [4 ^ [23 ^ [_32500, _32523]]]]]))).
% 29.72/29.50 cnf('1.1.1.1.1.1.1.1',plain,[id(23 ^ [_32500, _32523], 40 ^ [4 ^ [23 ^ [_32500, _32523]]]), -(id(40 ^ [4 ^ [23 ^ [_32500, _32523]]], 23 ^ [_32500, _32523]))],extension(13,bind([[_12606, _12559], [40 ^ [4 ^ [23 ^ [_32500, _32523]]], 23 ^ [_32500, _32523]]]))).
% 29.72/29.50 cnf('1.1.1.1.1.1.1.1.1',plain,[id(40 ^ [4 ^ [23 ^ [_32500, _32523]]], 23 ^ [_32500, _32523]), r2(_32500, 23 ^ [_32500, _32523]), r1(40 ^ [4 ^ [23 ^ [_32500, _32523]]])],extension(17,bind([[_22225, _22286, _22356], [_32500, 23 ^ [_32500, _32523], 40 ^ [4 ^ [23 ^ [_32500, _32523]]]]]))).
% 29.72/29.50 cnf('1.1.1.1.1.1.1.1.1.1',plain,[-(r2(_32500, 23 ^ [_32500, _32523]))],extension(15,bind([[_17954, _17869], [_32500, _32523]]))).
% 29.72/29.50 cnf('1.1.1.1.1.1.1.1.1.2',plain,[-(r1(40 ^ [4 ^ [23 ^ [_32500, _32523]]])), -(41 ^ [4 ^ [23 ^ [_32500, _32523]]])],extension(5,bind([[_22972], [4 ^ [23 ^ [_32500, _32523]]]]))).
% 29.72/29.50 cnf('1.1.1.1.1.1.1.1.1.2.1',plain,[41 ^ [4 ^ [23 ^ [_32500, _32523]]]],reduction('1')).
% 29.72/29.50 cnf('1.1.1.1.1.1.1.2',plain,[-(r2(40 ^ [4 ^ [23 ^ [_32500, _32523]]], 39 ^ [4 ^ [23 ^ [_32500, _32523]]])), -(41 ^ [4 ^ [23 ^ [_32500, _32523]]])],extension(4,bind([[_22972], [4 ^ [23 ^ [_32500, _32523]]]]))).
% 29.72/29.50 cnf('1.1.1.1.1.1.1.2.1',plain,[41 ^ [4 ^ [23 ^ [_32500, _32523]]]],reduction('1')).
% 29.72/29.50 cnf('1.1.1.1.1.1.1.3',plain,[-(id(39 ^ [4 ^ [23 ^ [_32500, _32523]]], 39 ^ [4 ^ [23 ^ [_32500, _32523]]]))],extension(12,bind([[_12385], [39 ^ [4 ^ [23 ^ [_32500, _32523]]]]]))).
% 29.72/29.50 cnf('1.2',plain,[-(43 ^ [4 ^ [23 ^ [_32500, _32523]]]), -(r1(42 ^ [4 ^ [23 ^ [_32500, _32523]]]))],extension(1,bind([[_22972], [4 ^ [23 ^ [_32500, _32523]]]]))).
% 29.72/29.50 cnf('1.2.1',plain,[r1(42 ^ [4 ^ [23 ^ [_32500, _32523]]]), -(13 ^ [42 ^ [4 ^ [23 ^ [_32500, _32523]]], 4 ^ [23 ^ [_32500, _32523]]])],extension(7,bind([[_13465, _13400], [42 ^ [4 ^ [23 ^ [_32500, _32523]]], 4 ^ [23 ^ [_32500, _32523]]]]))).
% 29.72/29.50 cnf('1.2.1.1',plain,[13 ^ [42 ^ [4 ^ [23 ^ [_32500, _32523]]], 4 ^ [23 ^ [_32500, _32523]]], id(4 ^ [23 ^ [_32500, _32523]], 42 ^ [4 ^ [23 ^ [_32500, _32523]]]), 14 ^ [42 ^ [4 ^ [23 ^ [_32500, _32523]]], 4 ^ [23 ^ [_32500, _32523]]]],extension(14,bind([[_13465, _13400], [42 ^ [4 ^ [23 ^ [_32500, _32523]]], 4 ^ [23 ^ [_32500, _32523]]]]))).
% 29.72/29.51 cnf('1.2.1.1.1',plain,[-(id(4 ^ [23 ^ [_32500, _32523]], 42 ^ [4 ^ [23 ^ [_32500, _32523]]])), -(43 ^ [4 ^ [23 ^ [_32500, _32523]]])],extension(2,bind([[_22972], [4 ^ [23 ^ [_32500, _32523]]]]))).
% 29.72/29.51 cnf('1.2.1.1.1.1',plain,[43 ^ [4 ^ [23 ^ [_32500, _32523]]]],reduction('1')).
% 29.72/29.51 cnf('1.2.1.1.2',plain,[-(14 ^ [42 ^ [4 ^ [23 ^ [_32500, _32523]]], 4 ^ [23 ^ [_32500, _32523]]]), -(r1(4 ^ [23 ^ [_32500, _32523]]))],extension(6,bind([[_13465, _13400], [42 ^ [4 ^ [23 ^ [_32500, _32523]]], 4 ^ [23 ^ [_32500, _32523]]]]))).
% 29.72/29.51 cnf('1.2.1.1.2.1',plain,[r1(4 ^ [23 ^ [_32500, _32523]]), r2(23 ^ [_32500, _32523], 4 ^ [23 ^ [_32500, _32523]]), id(4 ^ [23 ^ [_32500, _32523]], 4 ^ [23 ^ [_32500, _32523]])],extension(17,bind([[_22225, _22356, _22286], [23 ^ [_32500, _32523], 4 ^ [23 ^ [_32500, _32523]], 4 ^ [23 ^ [_32500, _32523]]]]))).
% 29.72/29.51 cnf('1.2.1.1.2.1.1',plain,[-(r2(23 ^ [_32500, _32523], 4 ^ [23 ^ [_32500, _32523]])), -(5 ^ [4 ^ [23 ^ [_32500, _32523]], 23 ^ [_32500, _32523]])],extension(9,bind([[_23900, _10217], [4 ^ [23 ^ [_32500, _32523]], 23 ^ [_32500, _32523]]]))).
% 29.72/29.51 cnf('1.2.1.1.2.1.1.1',plain,[5 ^ [4 ^ [23 ^ [_32500, _32523]], 23 ^ [_32500, _32523]], 6 ^ [4 ^ [23 ^ [_32500, _32523]], 23 ^ [_32500, _32523]]],extension(11,bind([[_23900, _10217], [4 ^ [23 ^ [_32500, _32523]], 23 ^ [_32500, _32523]]]))).
% 29.72/29.51 cnf('1.2.1.1.2.1.1.1.1',plain,[-(6 ^ [4 ^ [23 ^ [_32500, _32523]], 23 ^ [_32500, _32523]]), id(4 ^ [23 ^ [_32500, _32523]], 4 ^ [23 ^ [_32500, _32523]])],extension(8,bind([[_23900, _10217], [4 ^ [23 ^ [_32500, _32523]], 23 ^ [_32500, _32523]]]))).
% 29.72/29.51 cnf('1.2.1.1.2.1.1.1.1.1',plain,[-(id(4 ^ [23 ^ [_32500, _32523]], 4 ^ [23 ^ [_32500, _32523]]))],extension(12,bind([[_12385], [4 ^ [23 ^ [_32500, _32523]]]]))).
% 29.72/29.51 cnf('1.2.1.1.2.1.2',plain,[-(id(4 ^ [23 ^ [_32500, _32523]], 4 ^ [23 ^ [_32500, _32523]]))],extension(12,bind([[_12385], [4 ^ [23 ^ [_32500, _32523]]]]))).
% 29.72/29.51 %-----------------------------------------------------
% 29.72/29.51
% 29.72/29.51 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------