%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KRS115+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n032.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 74.25s 73.76s
% Output : Proof 74.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.10 % Problem : KRS115+1 : TPTP v8.1.0. Released v3.1.0.
% 0.03/0.10 % Command : leancop_casc.sh %s %d
% 0.10/0.30 % Computer : n032.cluster.edu
% 0.10/0.30 % Model : x86_64 x86_64
% 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.30 % Memory : 8042.1875MB
% 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.30 % CPULimit : 300
% 0.10/0.30 % WCLimit : 600
% 0.10/0.30 % DateTime : Tue Jun 7 15:39:50 EDT 2022
% 0.10/0.30 % CPUTime :
% 74.25/73.76 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 74.25/73.77 % SZS output start Proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
% 74.25/73.77
% 74.25/73.77 %-----------------------------------------------------
% 74.25/73.77 fof(axiom_0, axiom, ! [_52053] : (cowlThing(_52053) & ~ cowlNothing(_52053)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 74.25/73.77 fof(axiom_2, axiom, ! [_52184] : (cUnsatisfiable(_52184) <=> ? [_52199] : (rf2(_52184, _52199) & cp2(_52199)) & ? [_52199] : (rf1(_52184, _52199) & cp1(_52199)) & ? [_52199] : (rr(_52184, _52199) & cowlThing(_52199))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 74.25/73.77 fof(axiom_3, axiom, ! [_52569] : (cp1(_52569) => cp2xcomp(_52569)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 74.25/73.77 fof(axiom_4, axiom, ! [_52690] : (cp2(_52690) <=> ~ ? [_52707] : ra_Px1(_52690, _52707)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 74.25/73.77 fof(axiom_5, axiom, ! [_52856] : (cp2xcomp(_52856) <=> ? [_52871] : ra_Px1(_52856, _52871)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 74.25/73.77 fof(axiom_6, axiom, ! [_53015] : (cowlThing(_53015) => ! [_53030, _53033] : (rf1(_53015, _53030) & rf1(_53015, _53033) => _53030 = _53033)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 74.25/73.77 fof(axiom_7, axiom, ! [_53236] : (cowlThing(_53236) => ! [_53251, _53254] : (rf2(_53236, _53251) & rf2(_53236, _53254) => _53251 = _53254)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 74.25/73.77 fof(axiom_8, axiom, cUnsatisfiable(i2003_11_14_17_21_30578), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 74.25/73.77 fof(axiom_9, axiom, ! [_53504, _53507] : (rr(_53504, _53507) => rf2(_53504, _53507)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_9)).
% 74.25/73.77 fof(axiom_10, axiom, ! [_53650, _53653] : (rr(_53650, _53653) => rf1(_53650, _53653)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_10)).
% 74.25/73.77
% 74.25/73.77 cnf(1, plain, [-(_13102 = _13102)], theory(equality)).
% 74.25/73.77 cnf(2, plain, [-(cowlThing(_14717)), _14668 = _14717, cowlThing(_14668)], theory(equality)).
% 74.25/73.77 cnf(3, plain, [-(cp2xcomp(_15704)), _15655 = _15704, cp2xcomp(_15655)], theory(equality)).
% 74.25/73.77 cnf(4, plain, [-(rf1(_16675, _16806)), rf1(_16608, _16741), _16608 = _16675, _16741 = _16806], theory(equality)).
% 74.25/73.77 cnf(5, plain, [-(rr(_17923, _18054)), rr(_17856, _17989), _17856 = _17923, _17989 = _18054], theory(equality)).
% 74.25/73.77 cnf(6, plain, [-(cowlThing(_25873))], clausify(axiom_0)).
% 74.25/73.77 cnf(7, plain, [cUnsatisfiable(_26329), -(rf2(_26329, 1 ^ [_26329]))], clausify(axiom_2)).
% 74.25/73.77 cnf(8, plain, [cUnsatisfiable(_26329), -(cp2(1 ^ [_26329]))], clausify(axiom_2)).
% 74.25/73.77 cnf(9, plain, [cUnsatisfiable(_26329), -(rf1(_26329, 2 ^ [_26329]))], clausify(axiom_2)).
% 74.25/73.77 cnf(10, plain, [cUnsatisfiable(_26329), -(cp1(2 ^ [_26329]))], clausify(axiom_2)).
% 74.25/73.77 cnf(11, plain, [cUnsatisfiable(_26329), -(rr(_26329, 3 ^ [_26329]))], clausify(axiom_2)).
% 74.25/73.77 cnf(12, plain, [cp1(_27063), -(cp2xcomp(_27063))], clausify(axiom_3)).
% 74.25/73.77 cnf(13, plain, [cp2(_27273), ra_Px1(_27273, _27366)], clausify(axiom_4)).
% 74.25/73.77 cnf(14, plain, [cp2xcomp(_27574), -(ra_Px1(_27574, 5 ^ [_27574]))], clausify(axiom_5)).
% 74.25/73.77 cnf(15, plain, [cowlThing(_27857), -(_27956 = _28011), rf1(_27857, _27956), rf1(_27857, _28011)], clausify(axiom_6)).
% 74.25/73.77 cnf(16, plain, [cowlThing(_28382), -(_28481 = _28536), rf2(_28382, _28481), rf2(_28382, _28536)], clausify(axiom_7)).
% 74.25/73.77 cnf(17, plain, [-(cUnsatisfiable(i2003_11_14_17_21_30578))], clausify(axiom_8)).
% 74.25/73.77 cnf(18, plain, [rr(_29019, _29064), -(rf2(_29019, _29064))], clausify(axiom_9)).
% 74.25/73.77 cnf(19, plain, [rr(_29319, _29364), -(rf1(_29319, _29364))], clausify(axiom_10)).
% 74.25/73.77
% 74.25/73.77 cnf('1',plain,[-(cowlThing(i2003_11_14_17_21_30578)), i2003_11_14_17_21_30578 = i2003_11_14_17_21_30578, cowlThing(i2003_11_14_17_21_30578)],start(2,bind([[_14717, _14668], [i2003_11_14_17_21_30578, i2003_11_14_17_21_30578]]))).
% 74.25/73.77 cnf('1.1',plain,[cowlThing(i2003_11_14_17_21_30578), -(2 ^ [i2003_11_14_17_21_30578] = 1 ^ [i2003_11_14_17_21_30578]), rf1(i2003_11_14_17_21_30578, 2 ^ [i2003_11_14_17_21_30578]), rf1(i2003_11_14_17_21_30578, 1 ^ [i2003_11_14_17_21_30578])],extension(15,bind([[_27956, _27857, _28011], [2 ^ [i2003_11_14_17_21_30578], i2003_11_14_17_21_30578, 1 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.77 cnf('1.1.1',plain,[2 ^ [i2003_11_14_17_21_30578] = 1 ^ [i2003_11_14_17_21_30578], -(cp2xcomp(1 ^ [i2003_11_14_17_21_30578])), cp2xcomp(2 ^ [i2003_11_14_17_21_30578])],extension(3,bind([[_15704, _15655], [1 ^ [i2003_11_14_17_21_30578], 2 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.77 cnf('1.1.1.1',plain,[cp2xcomp(1 ^ [i2003_11_14_17_21_30578]), -(ra_Px1(1 ^ [i2003_11_14_17_21_30578], 5 ^ [1 ^ [i2003_11_14_17_21_30578]]))],extension(14,bind([[_27574], [1 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.77 cnf('1.1.1.1.1',plain,[ra_Px1(1 ^ [i2003_11_14_17_21_30578], 5 ^ [1 ^ [i2003_11_14_17_21_30578]]), cp2(1 ^ [i2003_11_14_17_21_30578])],extension(13,bind([[_27366, _27273], [5 ^ [1 ^ [i2003_11_14_17_21_30578]], 1 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.77 cnf('1.1.1.1.1.1',plain,[-(cp2(1 ^ [i2003_11_14_17_21_30578])), cUnsatisfiable(i2003_11_14_17_21_30578)],extension(8,bind([[_26329], [i2003_11_14_17_21_30578]]))).
% 74.25/73.77 cnf('1.1.1.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_30578))],extension(17)).
% 74.25/73.77 cnf('1.1.1.2',plain,[-(cp2xcomp(2 ^ [i2003_11_14_17_21_30578])), cp1(2 ^ [i2003_11_14_17_21_30578])],extension(12,bind([[_27063], [2 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.77 cnf('1.1.1.2.1',plain,[-(cp1(2 ^ [i2003_11_14_17_21_30578])), cUnsatisfiable(i2003_11_14_17_21_30578)],extension(10,bind([[_26329], [i2003_11_14_17_21_30578]]))).
% 74.25/73.77 cnf('1.1.1.2.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_30578))],extension(17)).
% 74.25/73.77 cnf('1.1.2',plain,[-(rf1(i2003_11_14_17_21_30578, 2 ^ [i2003_11_14_17_21_30578])), rf1(i2003_11_14_17_21_30578, 2 ^ [i2003_11_14_17_21_30578]), i2003_11_14_17_21_30578 = i2003_11_14_17_21_30578, 2 ^ [i2003_11_14_17_21_30578] = 2 ^ [i2003_11_14_17_21_30578]],extension(4,bind([[_16608, _16675, _16741, _16806], [i2003_11_14_17_21_30578, i2003_11_14_17_21_30578, 2 ^ [i2003_11_14_17_21_30578], 2 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.77 cnf('1.1.2.1',plain,[-(rf1(i2003_11_14_17_21_30578, 2 ^ [i2003_11_14_17_21_30578])), rf1(i2003_11_14_17_21_30578, 2 ^ [i2003_11_14_17_21_30578]), i2003_11_14_17_21_30578 = i2003_11_14_17_21_30578, 2 ^ [i2003_11_14_17_21_30578] = 2 ^ [i2003_11_14_17_21_30578]],extension(4,bind([[_16608, _16675, _16741, _16806], [i2003_11_14_17_21_30578, i2003_11_14_17_21_30578, 2 ^ [i2003_11_14_17_21_30578], 2 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.77 cnf('1.1.2.1.1',plain,[-(rf1(i2003_11_14_17_21_30578, 2 ^ [i2003_11_14_17_21_30578])), rf1(i2003_11_14_17_21_30578, 2 ^ [i2003_11_14_17_21_30578]), i2003_11_14_17_21_30578 = i2003_11_14_17_21_30578, 2 ^ [i2003_11_14_17_21_30578] = 2 ^ [i2003_11_14_17_21_30578]],extension(4,bind([[_16608, _16675, _16741, _16806], [i2003_11_14_17_21_30578, i2003_11_14_17_21_30578, 2 ^ [i2003_11_14_17_21_30578], 2 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.77 cnf('1.1.2.1.1.1',plain,[-(rf1(i2003_11_14_17_21_30578, 2 ^ [i2003_11_14_17_21_30578])), cUnsatisfiable(i2003_11_14_17_21_30578)],extension(9,bind([[_26329], [i2003_11_14_17_21_30578]]))).
% 74.25/73.77 cnf('1.1.2.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_30578))],extension(17)).
% 74.25/73.77 cnf('1.1.2.1.1.2',plain,[-(i2003_11_14_17_21_30578 = i2003_11_14_17_21_30578)],extension(1,bind([[_13102], [i2003_11_14_17_21_30578]]))).
% 74.25/73.78 cnf('1.1.2.1.1.3',plain,[-(2 ^ [i2003_11_14_17_21_30578] = 2 ^ [i2003_11_14_17_21_30578])],extension(1,bind([[_13102], [2 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.78 cnf('1.1.2.1.2',plain,[-(i2003_11_14_17_21_30578 = i2003_11_14_17_21_30578)],extension(1,bind([[_13102], [i2003_11_14_17_21_30578]]))).
% 74.25/73.78 cnf('1.1.2.1.3',plain,[-(2 ^ [i2003_11_14_17_21_30578] = 2 ^ [i2003_11_14_17_21_30578])],extension(1,bind([[_13102], [2 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.78 cnf('1.1.2.2',plain,[-(i2003_11_14_17_21_30578 = i2003_11_14_17_21_30578)],extension(1,bind([[_13102], [i2003_11_14_17_21_30578]]))).
% 74.25/73.78 cnf('1.1.2.3',plain,[-(2 ^ [i2003_11_14_17_21_30578] = 2 ^ [i2003_11_14_17_21_30578])],extension(1,bind([[_13102], [2 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.78 cnf('1.1.3',plain,[-(rf1(i2003_11_14_17_21_30578, 1 ^ [i2003_11_14_17_21_30578])), rr(i2003_11_14_17_21_30578, 1 ^ [i2003_11_14_17_21_30578])],extension(19,bind([[_29319, _29364], [i2003_11_14_17_21_30578, 1 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.78 cnf('1.1.3.1',plain,[-(rr(i2003_11_14_17_21_30578, 1 ^ [i2003_11_14_17_21_30578])), rr(i2003_11_14_17_21_30578, 3 ^ [i2003_11_14_17_21_30578]), i2003_11_14_17_21_30578 = i2003_11_14_17_21_30578, 3 ^ [i2003_11_14_17_21_30578] = 1 ^ [i2003_11_14_17_21_30578]],extension(5,bind([[_17856, _17923, _17989, _18054], [i2003_11_14_17_21_30578, i2003_11_14_17_21_30578, 3 ^ [i2003_11_14_17_21_30578], 1 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.78 cnf('1.1.3.1.1',plain,[-(rr(i2003_11_14_17_21_30578, 3 ^ [i2003_11_14_17_21_30578])), rr(i2003_11_14_17_21_30578, 3 ^ [i2003_11_14_17_21_30578]), i2003_11_14_17_21_30578 = i2003_11_14_17_21_30578, 3 ^ [i2003_11_14_17_21_30578] = 3 ^ [i2003_11_14_17_21_30578]],extension(5,bind([[_17856, _17923, _17989, _18054], [i2003_11_14_17_21_30578, i2003_11_14_17_21_30578, 3 ^ [i2003_11_14_17_21_30578], 3 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.78 cnf('1.1.3.1.1.1',plain,[-(rr(i2003_11_14_17_21_30578, 3 ^ [i2003_11_14_17_21_30578])), cUnsatisfiable(i2003_11_14_17_21_30578)],extension(11,bind([[_26329], [i2003_11_14_17_21_30578]]))).
% 74.25/73.78 cnf('1.1.3.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_30578))],extension(17)).
% 74.25/73.78 cnf('1.1.3.1.1.2',plain,[-(i2003_11_14_17_21_30578 = i2003_11_14_17_21_30578)],extension(1,bind([[_13102], [i2003_11_14_17_21_30578]]))).
% 74.25/73.78 cnf('1.1.3.1.1.3',plain,[-(3 ^ [i2003_11_14_17_21_30578] = 3 ^ [i2003_11_14_17_21_30578])],extension(1,bind([[_13102], [3 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.78 cnf('1.1.3.1.2',plain,[-(i2003_11_14_17_21_30578 = i2003_11_14_17_21_30578)],extension(1,bind([[_13102], [i2003_11_14_17_21_30578]]))).
% 74.25/73.78 cnf('1.1.3.1.3',plain,[-(3 ^ [i2003_11_14_17_21_30578] = 1 ^ [i2003_11_14_17_21_30578]), cowlThing(i2003_11_14_17_21_30578), rf2(i2003_11_14_17_21_30578, 3 ^ [i2003_11_14_17_21_30578]), rf2(i2003_11_14_17_21_30578, 1 ^ [i2003_11_14_17_21_30578])],extension(16,bind([[_28481, _28382, _28536], [3 ^ [i2003_11_14_17_21_30578], i2003_11_14_17_21_30578, 1 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.78 cnf('1.1.3.1.3.1',plain,[-(cowlThing(i2003_11_14_17_21_30578))],extension(6,bind([[_25873], [i2003_11_14_17_21_30578]]))).
% 74.25/73.78 cnf('1.1.3.1.3.2',plain,[-(rf2(i2003_11_14_17_21_30578, 3 ^ [i2003_11_14_17_21_30578])), rr(i2003_11_14_17_21_30578, 3 ^ [i2003_11_14_17_21_30578])],extension(18,bind([[_29019, _29064], [i2003_11_14_17_21_30578, 3 ^ [i2003_11_14_17_21_30578]]]))).
% 74.25/73.78 cnf('1.1.3.1.3.2.1',plain,[-(rr(i2003_11_14_17_21_30578, 3 ^ [i2003_11_14_17_21_30578]))],lemmata('1.1.3.1')).
% 74.25/73.78 cnf('1.1.3.1.3.3',plain,[-(rf2(i2003_11_14_17_21_30578, 1 ^ [i2003_11_14_17_21_30578])), cUnsatisfiable(i2003_11_14_17_21_30578)],extension(7,bind([[_26329], [i2003_11_14_17_21_30578]]))).
% 74.25/73.78 cnf('1.1.3.1.3.3.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_30578))],extension(17)).
% 74.25/73.78 cnf('1.2',plain,[-(i2003_11_14_17_21_30578 = i2003_11_14_17_21_30578)],extension(1,bind([[_13102], [i2003_11_14_17_21_30578]]))).
% 74.25/73.78 cnf('1.3',plain,[-(cowlThing(i2003_11_14_17_21_30578))],extension(6,bind([[_25873], [i2003_11_14_17_21_30578]]))).
% 74.25/73.78 %-----------------------------------------------------
% 74.34/73.78
% 74.34/73.78 % SZS output end Proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------