%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KRS107+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:43 EDT 2022
% Result : Unsatisfiable 2.83s 3.49s
% Output : Proof 2.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS107+1 : TPTP v8.1.0. Released v3.1.0.
% 0.11/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n029.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 : Tue Jun 7 10:00:35 EDT 2022
% 0.12/0.34 % CPUTime :
% 2.83/3.49 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.90/3.50 % SZS output start Proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.90/3.50
% 2.90/3.50 %-----------------------------------------------------
% 2.90/3.50 fof(axiom_2, axiom, ! [_78378] : (cUnsatisfiable(_78378) <=> ? [_78393] : (rrx3(_78378, _78393) & cc1(_78393)) & ? [_78393] : (rrx4(_78378, _78393) & cc2(_78393)) & ca_Cx1(_78378)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 2.90/3.50 fof(cc2_substitution_1, axiom, ! [_78705, _78708] : (_78705 = _78708 & cc2(_78705) => cc2(_78708)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc2_substitution_1)).
% 2.90/3.50 fof(axiom_3, axiom, ! [_78904] : (ca_Ax2(_78904) <=> cc2(_78904) & cc1(_78904)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 2.90/3.50 fof(axiom_4, axiom, ! [_79046] : (ca_Cx1(_79046) <=> ? [_79061] : ra_Px1(_79046, _79061)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 2.90/3.50 fof(axiom_5, axiom, ! [_79206] : (ca_Cx1xcomp(_79206) <=> ? [_79221] : (rrx3(_79206, _79221) & ca_Ax2(_79221))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 2.90/3.50 fof(axiom_6, axiom, ! [_79385] : (ca_Cx1xcomp(_79385) <=> ~ ? [_79402] : ra_Px1(_79385, _79402)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 2.90/3.50 fof(axiom_7, axiom, ! [_79551, _79554, _79557] : (rrx(_79551, _79554) & rrx(_79551, _79557) => _79554 = _79557), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_7)).
% 2.90/3.50 fof(axiom_12, axiom, cUnsatisfiable(i2003_11_14_17_21_01226), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_12)).
% 2.90/3.50 fof(axiom_17, axiom, ! [_79787, _79790] : (rrx4(_79787, _79790) => rrx(_79787, _79790)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_17)).
% 2.90/3.50 fof(axiom_20, axiom, ! [_79935, _79938] : (rrx3(_79935, _79938) => rrx(_79935, _79938)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_20)).
% 2.90/3.50
% 2.90/3.50 cnf(1, plain, [-(3 ^ [_49831]), -(ca_Cx1(_49831))], clausify(axiom_2)).
% 2.90/3.50 cnf(2, plain, [-(3 ^ [_49831]), -(cc2(2 ^ [_49831]))], clausify(axiom_2)).
% 2.90/3.50 cnf(3, plain, [-(3 ^ [_49831]), -(rrx4(_49831, 2 ^ [_49831]))], clausify(axiom_2)).
% 2.90/3.50 cnf(4, plain, [-(3 ^ [_49831]), -(cc1(1 ^ [_49831]))], clausify(axiom_2)).
% 2.90/3.50 cnf(5, plain, [-(3 ^ [_49831]), -(rrx3(_49831, 1 ^ [_49831]))], clausify(axiom_2)).
% 2.90/3.50 cnf(6, plain, [-(cc2(_37400)), _37351 = _37400, cc2(_37351)], clausify(cc2_substitution_1)).
% 2.90/3.50 cnf(7, plain, [cUnsatisfiable(_49831), 3 ^ [_49831]], clausify(axiom_2)).
% 2.90/3.50 cnf(8, plain, [-(ca_Ax2(_50429)), cc2(_50429), cc1(_50429)], clausify(axiom_3)).
% 2.90/3.50 cnf(9, plain, [ca_Cx1(_50697), -(ra_Px1(_50697, 5 ^ [_50697]))], clausify(axiom_4)).
% 2.90/3.50 cnf(10, plain, [-(ca_Cx1xcomp(_50980)), rrx3(_50980, _51068), ca_Ax2(_51068)], clausify(axiom_5)).
% 2.90/3.50 cnf(11, plain, [ca_Cx1xcomp(_51326), ra_Px1(_51326, _51419)], clausify(axiom_6)).
% 2.90/3.50 cnf(12, plain, [-(_51683 = _51738), rrx(_51627, _51683), rrx(_51627, _51738)], clausify(axiom_7)).
% 2.90/3.50 cnf(13, plain, [-(cUnsatisfiable(i2003_11_14_17_21_01226))], clausify(axiom_12)).
% 2.90/3.50 cnf(14, plain, [rrx4(_55314, _55359), -(rrx(_55314, _55359))], clausify(axiom_17)).
% 2.90/3.50 cnf(15, plain, [rrx3(_56234, _56279), -(rrx(_56234, _56279))], clausify(axiom_20)).
% 2.90/3.50
% 2.90/3.50 cnf('1',plain,[cUnsatisfiable(i2003_11_14_17_21_01226), 3 ^ [i2003_11_14_17_21_01226]],start(7,bind([[_49831], [i2003_11_14_17_21_01226]]))).
% 2.90/3.50 cnf('1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_01226))],extension(13)).
% 2.90/3.50 cnf('1.2',plain,[-(3 ^ [i2003_11_14_17_21_01226]), -(cc1(1 ^ [i2003_11_14_17_21_01226]))],extension(4,bind([[_49831], [i2003_11_14_17_21_01226]]))).
% 2.90/3.50 cnf('1.2.1',plain,[cc1(1 ^ [i2003_11_14_17_21_01226]), -(ca_Ax2(1 ^ [i2003_11_14_17_21_01226])), cc2(1 ^ [i2003_11_14_17_21_01226])],extension(8,bind([[_50429], [1 ^ [i2003_11_14_17_21_01226]]]))).
% 2.90/3.50 cnf('1.2.1.1',plain,[ca_Ax2(1 ^ [i2003_11_14_17_21_01226]), -(ca_Cx1xcomp(i2003_11_14_17_21_01226)), rrx3(i2003_11_14_17_21_01226, 1 ^ [i2003_11_14_17_21_01226])],extension(10,bind([[_50980, _51068], [i2003_11_14_17_21_01226, 1 ^ [i2003_11_14_17_21_01226]]]))).
% 2.90/3.50 cnf('1.2.1.1.1',plain,[ca_Cx1xcomp(i2003_11_14_17_21_01226), ra_Px1(i2003_11_14_17_21_01226, 5 ^ [i2003_11_14_17_21_01226])],extension(11,bind([[_51326, _51419], [i2003_11_14_17_21_01226, 5 ^ [i2003_11_14_17_21_01226]]]))).
% 2.90/3.50 cnf('1.2.1.1.1.1',plain,[-(ra_Px1(i2003_11_14_17_21_01226, 5 ^ [i2003_11_14_17_21_01226])), ca_Cx1(i2003_11_14_17_21_01226)],extension(9,bind([[_50697], [i2003_11_14_17_21_01226]]))).
% 2.90/3.50 cnf('1.2.1.1.1.1.1',plain,[-(ca_Cx1(i2003_11_14_17_21_01226)), -(3 ^ [i2003_11_14_17_21_01226])],extension(1,bind([[_49831], [i2003_11_14_17_21_01226]]))).
% 2.90/3.50 cnf('1.2.1.1.1.1.1.1',plain,[3 ^ [i2003_11_14_17_21_01226]],reduction('1')).
% 2.90/3.50 cnf('1.2.1.1.2',plain,[-(rrx3(i2003_11_14_17_21_01226, 1 ^ [i2003_11_14_17_21_01226])), -(3 ^ [i2003_11_14_17_21_01226])],extension(5,bind([[_49831], [i2003_11_14_17_21_01226]]))).
% 2.90/3.50 cnf('1.2.1.1.2.1',plain,[3 ^ [i2003_11_14_17_21_01226]],reduction('1')).
% 2.90/3.50 cnf('1.2.1.2',plain,[-(cc2(1 ^ [i2003_11_14_17_21_01226])), 2 ^ [i2003_11_14_17_21_01226] = 1 ^ [i2003_11_14_17_21_01226], cc2(2 ^ [i2003_11_14_17_21_01226])],extension(6,bind([[_37400, _37351], [1 ^ [i2003_11_14_17_21_01226], 2 ^ [i2003_11_14_17_21_01226]]]))).
% 2.90/3.50 cnf('1.2.1.2.1',plain,[-(2 ^ [i2003_11_14_17_21_01226] = 1 ^ [i2003_11_14_17_21_01226]), rrx(i2003_11_14_17_21_01226, 2 ^ [i2003_11_14_17_21_01226]), rrx(i2003_11_14_17_21_01226, 1 ^ [i2003_11_14_17_21_01226])],extension(12,bind([[_51683, _51627, _51738], [2 ^ [i2003_11_14_17_21_01226], i2003_11_14_17_21_01226, 1 ^ [i2003_11_14_17_21_01226]]]))).
% 2.90/3.50 cnf('1.2.1.2.1.1',plain,[-(rrx(i2003_11_14_17_21_01226, 2 ^ [i2003_11_14_17_21_01226])), rrx4(i2003_11_14_17_21_01226, 2 ^ [i2003_11_14_17_21_01226])],extension(14,bind([[_55314, _55359], [i2003_11_14_17_21_01226, 2 ^ [i2003_11_14_17_21_01226]]]))).
% 2.90/3.50 cnf('1.2.1.2.1.1.1',plain,[-(rrx4(i2003_11_14_17_21_01226, 2 ^ [i2003_11_14_17_21_01226])), -(3 ^ [i2003_11_14_17_21_01226])],extension(3,bind([[_49831], [i2003_11_14_17_21_01226]]))).
% 2.90/3.50 cnf('1.2.1.2.1.1.1.1',plain,[3 ^ [i2003_11_14_17_21_01226]],reduction('1')).
% 2.90/3.50 cnf('1.2.1.2.1.2',plain,[-(rrx(i2003_11_14_17_21_01226, 1 ^ [i2003_11_14_17_21_01226])), rrx3(i2003_11_14_17_21_01226, 1 ^ [i2003_11_14_17_21_01226])],extension(15,bind([[_56234, _56279], [i2003_11_14_17_21_01226, 1 ^ [i2003_11_14_17_21_01226]]]))).
% 2.90/3.50 cnf('1.2.1.2.1.2.1',plain,[-(rrx3(i2003_11_14_17_21_01226, 1 ^ [i2003_11_14_17_21_01226])), -(3 ^ [i2003_11_14_17_21_01226])],extension(5,bind([[_49831], [i2003_11_14_17_21_01226]]))).
% 2.90/3.50 cnf('1.2.1.2.1.2.1.1',plain,[3 ^ [i2003_11_14_17_21_01226]],reduction('1')).
% 2.90/3.50 cnf('1.2.1.2.2',plain,[-(cc2(2 ^ [i2003_11_14_17_21_01226])), -(3 ^ [i2003_11_14_17_21_01226])],extension(2,bind([[_49831], [i2003_11_14_17_21_01226]]))).
% 2.90/3.50 cnf('1.2.1.2.2.1',plain,[3 ^ [i2003_11_14_17_21_01226]],reduction('1')).
% 2.90/3.50 %-----------------------------------------------------
% 2.90/3.51
% 2.90/3.51 % SZS output end Proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------