%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KRS089+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n020.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 : Sun Jul 17 03:13:39 EDT 2022
% Result : Unsatisfiable 106.42s 107.13s
% Output : Proof 106.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : KRS089+1 : TPTP v8.1.0. Released v3.1.0.
% 0.13/0.13 % Command : leancop_casc.sh %s %d
% 0.14/0.34 % Computer : n020.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 600
% 0.14/0.34 % DateTime : Tue Jun 7 20:11:51 EDT 2022
% 0.14/0.34 % CPUTime :
% 106.42/107.13 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 106.42/107.14 % SZS output start Proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
% 106.42/107.15
% 106.42/107.15 %-----------------------------------------------------
% 106.42/107.15 fof(axiom_3, axiom, ! [_44154] : (cowlThing(_44154) => ? [_44169] : (rp(_44154, _44169) & _44169 = ispy)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 106.42/107.15 fof(axiom_2, axiom, ! [_44347] : (cUnsatisfiable(_44347) => ? [_44362, _44365, _44368] : (rr(_44347, _44362) & rr(_44347, _44365) & rr(_44347, _44368) & (! _44362) = _44365 & (! _44362) = _44368 & (! _44365) = _44368)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 106.42/107.15 fof(rinvP_substitution_1, axiom, ! [_44706, _44709, _44712] : (_44706 = _44709 & rinvP(_44706, _44712) => rinvP(_44709, _44712)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', rinvP_substitution_1)).
% 106.42/107.15 fof(axiom_0, axiom, ! [_44894] : (cowlThing(_44894) & ~ cowlNothing(_44894)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 106.42/107.15 fof(axiom_4, axiom, ! [_45048, _45051] : (rp(_45048, _45051) <=> rinvP(_45051, _45048)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 106.42/107.15 fof(axiom_7, axiom, cUnsatisfiable(i2003_11_14_17_19_53168), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 106.42/107.15 fof(axiom_5, axiom, ! [_45243, _45246, _45249] : (rinvP(ispy, _45243) & rinvP(ispy, _45246) & rinvP(ispy, _45249) => _45243 = _45246 | _45243 = _45249 | _45246 = _45249), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 106.42/107.15
% 106.42/107.15 cnf(1, plain, [-(6 ^ [_20441]), -(5 ^ [_20441] = ispy)], clausify(axiom_3)).
% 106.42/107.15 cnf(2, plain, [-(6 ^ [_20441]), -(rp(_20441, 5 ^ [_20441]))], clausify(axiom_3)).
% 106.42/107.15 cnf(3, plain, [-(4 ^ [_19467]), 2 ^ [_19467] = 3 ^ [_19467]], clausify(axiom_2)).
% 106.42/107.15 cnf(4, plain, [-(4 ^ [_19467]), 1 ^ [_19467] = 3 ^ [_19467]], clausify(axiom_2)).
% 106.42/107.15 cnf(5, plain, [-(4 ^ [_19467]), 1 ^ [_19467] = 2 ^ [_19467]], clausify(axiom_2)).
% 106.42/107.15 cnf(6, plain, [-(rinvP(_15565, _15620)), _15509 = _15565, rinvP(_15509, _15620)], clausify(rinvP_substitution_1)).
% 106.42/107.15 cnf(7, plain, [-(cowlThing(_19011))], clausify(axiom_0)).
% 106.42/107.15 cnf(8, plain, [cUnsatisfiable(_19467), 4 ^ [_19467]], clausify(axiom_2)).
% 106.42/107.15 cnf(9, plain, [cowlThing(_20441), 6 ^ [_20441]], clausify(axiom_3)).
% 106.42/107.15 cnf(10, plain, [rp(_20810, _20855), -(rinvP(_20855, _20810))], clausify(axiom_4)).
% 106.42/107.15 cnf(11, plain, [-(cUnsatisfiable(i2003_11_14_17_19_53168))], clausify(axiom_7)).
% 106.42/107.15 cnf(12, plain, [rinvP(ispy, _21267), rinvP(ispy, _21194), rinvP(ispy, _21120), -(_21120 = _21194), -(_21120 = _21267), -(_21194 = _21267)], clausify(axiom_5)).
% 106.42/107.15
% 106.42/107.15 cnf('1',plain,[cUnsatisfiable(i2003_11_14_17_19_53168), 4 ^ [i2003_11_14_17_19_53168]],start(8,bind([[_19467], [i2003_11_14_17_19_53168]]))).
% 106.42/107.15 cnf('1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_19_53168))],extension(11)).
% 106.42/107.15 cnf('1.2',plain,[-(4 ^ [i2003_11_14_17_19_53168]), 2 ^ [i2003_11_14_17_19_53168] = 3 ^ [i2003_11_14_17_19_53168]],extension(3,bind([[_19467], [i2003_11_14_17_19_53168]]))).
% 106.42/107.15 cnf('1.2.1',plain,[-(2 ^ [i2003_11_14_17_19_53168] = 3 ^ [i2003_11_14_17_19_53168]), rinvP(ispy, 3 ^ [i2003_11_14_17_19_53168]), rinvP(ispy, 2 ^ [i2003_11_14_17_19_53168]), rinvP(ispy, 1 ^ [i2003_11_14_17_19_53168]), -(1 ^ [i2003_11_14_17_19_53168] = 2 ^ [i2003_11_14_17_19_53168]), -(1 ^ [i2003_11_14_17_19_53168] = 3 ^ [i2003_11_14_17_19_53168])],extension(12,bind([[_21194, _21120, _21267], [2 ^ [i2003_11_14_17_19_53168], 1 ^ [i2003_11_14_17_19_53168], 3 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.1',plain,[-(rinvP(ispy, 3 ^ [i2003_11_14_17_19_53168])), 5 ^ [3 ^ [i2003_11_14_17_19_53168]] = ispy, rinvP(5 ^ [3 ^ [i2003_11_14_17_19_53168]], 3 ^ [i2003_11_14_17_19_53168])],extension(6,bind([[_15565, _15509, _15620], [ispy, 5 ^ [3 ^ [i2003_11_14_17_19_53168]], 3 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.1.1',plain,[-(5 ^ [3 ^ [i2003_11_14_17_19_53168]] = ispy), -(6 ^ [3 ^ [i2003_11_14_17_19_53168]])],extension(1,bind([[_20441], [3 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.1.1.1',plain,[6 ^ [3 ^ [i2003_11_14_17_19_53168]], cowlThing(3 ^ [i2003_11_14_17_19_53168])],extension(9,bind([[_20441], [3 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.1.1.1.1',plain,[-(cowlThing(3 ^ [i2003_11_14_17_19_53168]))],extension(7,bind([[_19011], [3 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.1.2',plain,[-(rinvP(5 ^ [3 ^ [i2003_11_14_17_19_53168]], 3 ^ [i2003_11_14_17_19_53168])), rp(3 ^ [i2003_11_14_17_19_53168], 5 ^ [3 ^ [i2003_11_14_17_19_53168]])],extension(10,bind([[_20810, _20855], [3 ^ [i2003_11_14_17_19_53168], 5 ^ [3 ^ [i2003_11_14_17_19_53168]]]]))).
% 106.42/107.15 cnf('1.2.1.1.2.1',plain,[-(rp(3 ^ [i2003_11_14_17_19_53168], 5 ^ [3 ^ [i2003_11_14_17_19_53168]])), -(6 ^ [3 ^ [i2003_11_14_17_19_53168]])],extension(2,bind([[_20441], [3 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.1.2.1.1',plain,[6 ^ [3 ^ [i2003_11_14_17_19_53168]], cowlThing(3 ^ [i2003_11_14_17_19_53168])],extension(9,bind([[_20441], [3 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.1.2.1.1.1',plain,[-(cowlThing(3 ^ [i2003_11_14_17_19_53168]))],extension(7,bind([[_19011], [3 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.2',plain,[-(rinvP(ispy, 2 ^ [i2003_11_14_17_19_53168])), 5 ^ [2 ^ [i2003_11_14_17_19_53168]] = ispy, rinvP(5 ^ [2 ^ [i2003_11_14_17_19_53168]], 2 ^ [i2003_11_14_17_19_53168])],extension(6,bind([[_15565, _15509, _15620], [ispy, 5 ^ [2 ^ [i2003_11_14_17_19_53168]], 2 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.2.1',plain,[-(5 ^ [2 ^ [i2003_11_14_17_19_53168]] = ispy), -(6 ^ [2 ^ [i2003_11_14_17_19_53168]])],extension(1,bind([[_20441], [2 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.2.1.1',plain,[6 ^ [2 ^ [i2003_11_14_17_19_53168]], cowlThing(2 ^ [i2003_11_14_17_19_53168])],extension(9,bind([[_20441], [2 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.2.1.1.1',plain,[-(cowlThing(2 ^ [i2003_11_14_17_19_53168]))],extension(7,bind([[_19011], [2 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.2.2',plain,[-(rinvP(5 ^ [2 ^ [i2003_11_14_17_19_53168]], 2 ^ [i2003_11_14_17_19_53168])), rp(2 ^ [i2003_11_14_17_19_53168], 5 ^ [2 ^ [i2003_11_14_17_19_53168]])],extension(10,bind([[_20810, _20855], [2 ^ [i2003_11_14_17_19_53168], 5 ^ [2 ^ [i2003_11_14_17_19_53168]]]]))).
% 106.42/107.15 cnf('1.2.1.2.2.1',plain,[-(rp(2 ^ [i2003_11_14_17_19_53168], 5 ^ [2 ^ [i2003_11_14_17_19_53168]])), -(6 ^ [2 ^ [i2003_11_14_17_19_53168]])],extension(2,bind([[_20441], [2 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.2.2.1.1',plain,[6 ^ [2 ^ [i2003_11_14_17_19_53168]], cowlThing(2 ^ [i2003_11_14_17_19_53168])],extension(9,bind([[_20441], [2 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.2.2.1.1.1',plain,[-(cowlThing(2 ^ [i2003_11_14_17_19_53168]))],extension(7,bind([[_19011], [2 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.3',plain,[-(rinvP(ispy, 1 ^ [i2003_11_14_17_19_53168])), 5 ^ [1 ^ [i2003_11_14_17_19_53168]] = ispy, rinvP(5 ^ [1 ^ [i2003_11_14_17_19_53168]], 1 ^ [i2003_11_14_17_19_53168])],extension(6,bind([[_15565, _15509, _15620], [ispy, 5 ^ [1 ^ [i2003_11_14_17_19_53168]], 1 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.3.1',plain,[-(5 ^ [1 ^ [i2003_11_14_17_19_53168]] = ispy), -(6 ^ [1 ^ [i2003_11_14_17_19_53168]])],extension(1,bind([[_20441], [1 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.3.1.1',plain,[6 ^ [1 ^ [i2003_11_14_17_19_53168]], cowlThing(1 ^ [i2003_11_14_17_19_53168])],extension(9,bind([[_20441], [1 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.3.1.1.1',plain,[-(cowlThing(1 ^ [i2003_11_14_17_19_53168]))],extension(7,bind([[_19011], [1 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.3.2',plain,[-(rinvP(5 ^ [1 ^ [i2003_11_14_17_19_53168]], 1 ^ [i2003_11_14_17_19_53168])), rp(1 ^ [i2003_11_14_17_19_53168], 5 ^ [1 ^ [i2003_11_14_17_19_53168]])],extension(10,bind([[_20810, _20855], [1 ^ [i2003_11_14_17_19_53168], 5 ^ [1 ^ [i2003_11_14_17_19_53168]]]]))).
% 106.42/107.15 cnf('1.2.1.3.2.1',plain,[-(rp(1 ^ [i2003_11_14_17_19_53168], 5 ^ [1 ^ [i2003_11_14_17_19_53168]])), -(6 ^ [1 ^ [i2003_11_14_17_19_53168]])],extension(2,bind([[_20441], [1 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.3.2.1.1',plain,[6 ^ [1 ^ [i2003_11_14_17_19_53168]], cowlThing(1 ^ [i2003_11_14_17_19_53168])],extension(9,bind([[_20441], [1 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.3.2.1.1.1',plain,[-(cowlThing(1 ^ [i2003_11_14_17_19_53168]))],extension(7,bind([[_19011], [1 ^ [i2003_11_14_17_19_53168]]]))).
% 106.42/107.15 cnf('1.2.1.4',plain,[1 ^ [i2003_11_14_17_19_53168] = 2 ^ [i2003_11_14_17_19_53168], -(4 ^ [i2003_11_14_17_19_53168])],extension(5,bind([[_19467], [i2003_11_14_17_19_53168]]))).
% 106.42/107.15 cnf('1.2.1.4.1',plain,[4 ^ [i2003_11_14_17_19_53168]],reduction('1')).
% 106.42/107.15 cnf('1.2.1.5',plain,[1 ^ [i2003_11_14_17_19_53168] = 3 ^ [i2003_11_14_17_19_53168], -(4 ^ [i2003_11_14_17_19_53168])],extension(4,bind([[_19467], [i2003_11_14_17_19_53168]]))).
% 106.42/107.15 cnf('1.2.1.5.1',plain,[4 ^ [i2003_11_14_17_19_53168]],reduction('1')).
% 106.42/107.15 %-----------------------------------------------------
% 106.42/107.15
% 106.42/107.15 % SZS output end Proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------