%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KRS114+1 : TPTP v8.1.0. Released v3.1.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 : Sun Jul 17 03:13:44 EDT 2022
% Result : Unsatisfiable 0.88s 1.41s
% Output : Proof 0.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : KRS114+1 : TPTP v8.1.0. Released v3.1.0.
% 0.08/0.14 % Command : leancop_casc.sh %s %d
% 0.13/0.35 % Computer : n029.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Tue Jun 7 07:25:50 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.88/1.41 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.88/1.42 % SZS output start Proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.88/1.43
% 0.88/1.43 %-----------------------------------------------------
% 0.88/1.43 fof(axiom_8, axiom, ! [_58668] : (ca_Ax4(_58668) <=> ! [_58683, _58686] : (rinvR(_58668, _58683) & rinvR(_58668, _58686) => _58683 = _58686) & ? [_58720] : (rinvR(_58668, _58720) & ca_Vx5(_58720))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 0.88/1.43 fof(axiom_7, axiom, ! [_58990] : (ca_Ax3(_58990) <=> cqxcomp(_58990) & cpxcomp(_58990)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.88/1.43 fof(axiom_2, axiom, ! [_59133] : (cUnsatisfiable(_59133) <=> ? [_59148] : (rr(_59133, _59148) & ca_Ax4(_59148)) & ? [_59148] : (rs(_59133, _59148) & ca_Ax3(_59148))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.88/1.43 fof(axiom_3, axiom, ! [_59465] : (cp(_59465) <=> ~ ? [_59482] : ra_Px1(_59465, _59482)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.88/1.43 fof(axiom_4, axiom, ! [_59631] : (cpxcomp(_59631) <=> ? [_59646] : ra_Px1(_59631, _59646)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.88/1.43 fof(axiom_11, axiom, cUnsatisfiable(i2003_11_14_17_21_262), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_11)).
% 0.88/1.43 fof(axiom_10, axiom, ! [_59867, _59870] : (rinvR(_59867, _59870) <=> rr(_59870, _59867)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_10)).
% 0.88/1.43 fof(axiom_9, axiom, ! [_60014] : (ca_Vx5(_60014) <=> ! [_60029] : (rs(_60014, _60029) => cp(_60029))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_9)).
% 0.88/1.43
% 0.88/1.43 cnf(1, plain, [-(10 ^ [_35881]), -(_36006 = _36061), rinvR(_35881, _36006), rinvR(_35881, _36061)], clausify(axiom_8)).
% 0.88/1.43 cnf(2, plain, [-(10 ^ [_35881]), -(ca_Vx5(9 ^ [_35881]))], clausify(axiom_8)).
% 0.88/1.43 cnf(3, plain, [-(10 ^ [_35881]), -(rinvR(_35881, 9 ^ [_35881]))], clausify(axiom_8)).
% 0.88/1.43 cnf(4, plain, [-(8 ^ [_35613]), -(cpxcomp(_35613))], clausify(axiom_7)).
% 0.88/1.43 cnf(5, plain, [-(3 ^ [_33905]), -(ca_Ax3(2 ^ [_33905]))], clausify(axiom_2)).
% 0.88/1.43 cnf(6, plain, [-(3 ^ [_33905]), -(rs(_33905, 2 ^ [_33905]))], clausify(axiom_2)).
% 0.88/1.43 cnf(7, plain, [-(3 ^ [_33905]), -(ca_Ax4(1 ^ [_33905]))], clausify(axiom_2)).
% 0.88/1.43 cnf(8, plain, [-(3 ^ [_33905]), -(rr(_33905, 1 ^ [_33905]))], clausify(axiom_2)).
% 0.88/1.43 cnf(9, plain, [cUnsatisfiable(_33905), 3 ^ [_33905]], clausify(axiom_2)).
% 0.88/1.43 cnf(10, plain, [cp(_34445), ra_Px1(_34445, _34538)], clausify(axiom_3)).
% 0.88/1.43 cnf(11, plain, [cpxcomp(_34746), -(ra_Px1(_34746, 5 ^ [_34746]))], clausify(axiom_4)).
% 0.88/1.43 cnf(12, plain, [ca_Ax3(_35613), 8 ^ [_35613]], clausify(axiom_7)).
% 0.88/1.43 cnf(13, plain, [ca_Ax4(_35881), 10 ^ [_35881]], clausify(axiom_8)).
% 0.88/1.43 cnf(14, plain, [-(cUnsatisfiable(i2003_11_14_17_21_262))], clausify(axiom_11)).
% 0.88/1.43 cnf(15, plain, [-(rinvR(_36945, _36990)), rr(_36990, _36945)], clausify(axiom_10)).
% 0.88/1.43 cnf(16, plain, [ca_Vx5(_36600), rs(_36600, _36687), -(cp(_36687))], clausify(axiom_9)).
% 0.88/1.43 cnf(17, plain, [-(_16329 = _16329)], theory(equality)).
% 0.88/1.43 cnf(18, plain, [-(rs(_23090, _23221)), rs(_23023, _23156), _23023 = _23090, _23156 = _23221], theory(equality)).
% 0.88/1.43
% 0.88/1.43 cnf('1',plain,[cp(2 ^ [i2003_11_14_17_21_262]), ra_Px1(2 ^ [i2003_11_14_17_21_262], 5 ^ [2 ^ [i2003_11_14_17_21_262]])],start(10,bind([[_34445, _34538], [2 ^ [i2003_11_14_17_21_262], 5 ^ [2 ^ [i2003_11_14_17_21_262]]]]))).
% 0.88/1.43 cnf('1.1',plain,[-(cp(2 ^ [i2003_11_14_17_21_262])), ca_Vx5(9 ^ [1 ^ [i2003_11_14_17_21_262]]), rs(9 ^ [1 ^ [i2003_11_14_17_21_262]], 2 ^ [i2003_11_14_17_21_262])],extension(16,bind([[_36600, _36687], [9 ^ [1 ^ [i2003_11_14_17_21_262]], 2 ^ [i2003_11_14_17_21_262]]]))).
% 0.88/1.43 cnf('1.1.1',plain,[-(ca_Vx5(9 ^ [1 ^ [i2003_11_14_17_21_262]])), -(10 ^ [1 ^ [i2003_11_14_17_21_262]])],extension(2,bind([[_35881], [1 ^ [i2003_11_14_17_21_262]]]))).
% 0.88/1.43 cnf('1.1.1.1',plain,[10 ^ [1 ^ [i2003_11_14_17_21_262]], ca_Ax4(1 ^ [i2003_11_14_17_21_262])],extension(13,bind([[_35881], [1 ^ [i2003_11_14_17_21_262]]]))).
% 0.88/1.43 cnf('1.1.1.1.1',plain,[-(ca_Ax4(1 ^ [i2003_11_14_17_21_262])), -(3 ^ [i2003_11_14_17_21_262])],extension(7,bind([[_33905], [i2003_11_14_17_21_262]]))).
% 0.88/1.43 cnf('1.1.1.1.1.1',plain,[3 ^ [i2003_11_14_17_21_262], cUnsatisfiable(i2003_11_14_17_21_262)],extension(9,bind([[_33905], [i2003_11_14_17_21_262]]))).
% 0.88/1.43 cnf('1.1.1.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_262))],extension(14)).
% 0.88/1.43 cnf('1.1.2',plain,[-(rs(9 ^ [1 ^ [i2003_11_14_17_21_262]], 2 ^ [i2003_11_14_17_21_262])), rs(i2003_11_14_17_21_262, 2 ^ [i2003_11_14_17_21_262]), i2003_11_14_17_21_262 = 9 ^ [1 ^ [i2003_11_14_17_21_262]], 2 ^ [i2003_11_14_17_21_262] = 2 ^ [i2003_11_14_17_21_262]],extension(18,bind([[_23023, _23090, _23156, _23221], [i2003_11_14_17_21_262, 9 ^ [1 ^ [i2003_11_14_17_21_262]], 2 ^ [i2003_11_14_17_21_262], 2 ^ [i2003_11_14_17_21_262]]]))).
% 0.88/1.43 cnf('1.1.2.1',plain,[-(rs(i2003_11_14_17_21_262, 2 ^ [i2003_11_14_17_21_262])), -(3 ^ [i2003_11_14_17_21_262])],extension(6,bind([[_33905], [i2003_11_14_17_21_262]]))).
% 0.88/1.43 cnf('1.1.2.1.1',plain,[3 ^ [i2003_11_14_17_21_262], cUnsatisfiable(i2003_11_14_17_21_262)],extension(9,bind([[_33905], [i2003_11_14_17_21_262]]))).
% 0.88/1.43 cnf('1.1.2.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_262))],extension(14)).
% 0.88/1.43 cnf('1.1.2.2',plain,[-(i2003_11_14_17_21_262 = 9 ^ [1 ^ [i2003_11_14_17_21_262]]), -(10 ^ [1 ^ [i2003_11_14_17_21_262]]), rinvR(1 ^ [i2003_11_14_17_21_262], i2003_11_14_17_21_262), rinvR(1 ^ [i2003_11_14_17_21_262], 9 ^ [1 ^ [i2003_11_14_17_21_262]])],extension(1,bind([[_36006, _35881, _36061], [i2003_11_14_17_21_262, 1 ^ [i2003_11_14_17_21_262], 9 ^ [1 ^ [i2003_11_14_17_21_262]]]]))).
% 0.88/1.43 cnf('1.1.2.2.1',plain,[10 ^ [1 ^ [i2003_11_14_17_21_262]], ca_Ax4(1 ^ [i2003_11_14_17_21_262])],extension(13,bind([[_35881], [1 ^ [i2003_11_14_17_21_262]]]))).
% 0.88/1.43 cnf('1.1.2.2.1.1',plain,[-(ca_Ax4(1 ^ [i2003_11_14_17_21_262])), -(3 ^ [i2003_11_14_17_21_262])],extension(7,bind([[_33905], [i2003_11_14_17_21_262]]))).
% 0.88/1.43 cnf('1.1.2.2.1.1.1',plain,[3 ^ [i2003_11_14_17_21_262], cUnsatisfiable(i2003_11_14_17_21_262)],extension(9,bind([[_33905], [i2003_11_14_17_21_262]]))).
% 0.88/1.43 cnf('1.1.2.2.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_262))],extension(14)).
% 0.88/1.43 cnf('1.1.2.2.2',plain,[-(rinvR(1 ^ [i2003_11_14_17_21_262], i2003_11_14_17_21_262)), rr(i2003_11_14_17_21_262, 1 ^ [i2003_11_14_17_21_262])],extension(15,bind([[_36990, _36945], [i2003_11_14_17_21_262, 1 ^ [i2003_11_14_17_21_262]]]))).
% 0.88/1.43 cnf('1.1.2.2.2.1',plain,[-(rr(i2003_11_14_17_21_262, 1 ^ [i2003_11_14_17_21_262])), -(3 ^ [i2003_11_14_17_21_262])],extension(8,bind([[_33905], [i2003_11_14_17_21_262]]))).
% 0.88/1.43 cnf('1.1.2.2.2.1.1',plain,[3 ^ [i2003_11_14_17_21_262], cUnsatisfiable(i2003_11_14_17_21_262)],extension(9,bind([[_33905], [i2003_11_14_17_21_262]]))).
% 0.88/1.43 cnf('1.1.2.2.2.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_262))],extension(14)).
% 0.88/1.43 cnf('1.1.2.2.3',plain,[-(rinvR(1 ^ [i2003_11_14_17_21_262], 9 ^ [1 ^ [i2003_11_14_17_21_262]])), -(10 ^ [1 ^ [i2003_11_14_17_21_262]])],extension(3,bind([[_35881], [1 ^ [i2003_11_14_17_21_262]]]))).
% 0.88/1.43 cnf('1.1.2.2.3.1',plain,[10 ^ [1 ^ [i2003_11_14_17_21_262]]],lemmata('1.1.2.2')).
% 0.88/1.43 cnf('1.1.2.3',plain,[-(2 ^ [i2003_11_14_17_21_262] = 2 ^ [i2003_11_14_17_21_262])],extension(17,bind([[_16329], [2 ^ [i2003_11_14_17_21_262]]]))).
% 0.88/1.43 cnf('1.2',plain,[-(ra_Px1(2 ^ [i2003_11_14_17_21_262], 5 ^ [2 ^ [i2003_11_14_17_21_262]])), cpxcomp(2 ^ [i2003_11_14_17_21_262])],extension(11,bind([[_34746], [2 ^ [i2003_11_14_17_21_262]]]))).
% 0.88/1.43 cnf('1.2.1',plain,[-(cpxcomp(2 ^ [i2003_11_14_17_21_262])), -(8 ^ [2 ^ [i2003_11_14_17_21_262]])],extension(4,bind([[_35613], [2 ^ [i2003_11_14_17_21_262]]]))).
% 0.88/1.43 cnf('1.2.1.1',plain,[8 ^ [2 ^ [i2003_11_14_17_21_262]], ca_Ax3(2 ^ [i2003_11_14_17_21_262])],extension(12,bind([[_35613], [2 ^ [i2003_11_14_17_21_262]]]))).
% 0.88/1.43 cnf('1.2.1.1.1',plain,[-(ca_Ax3(2 ^ [i2003_11_14_17_21_262])), -(3 ^ [i2003_11_14_17_21_262])],extension(5,bind([[_33905], [i2003_11_14_17_21_262]]))).
% 0.88/1.43 cnf('1.2.1.1.1.1',plain,[3 ^ [i2003_11_14_17_21_262], cUnsatisfiable(i2003_11_14_17_21_262)],extension(9,bind([[_33905], [i2003_11_14_17_21_262]]))).
% 0.88/1.43 cnf('1.2.1.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_262))],extension(14)).
% 0.88/1.43 %-----------------------------------------------------
% 0.88/1.43
% 0.88/1.43 % SZS output end Proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------