%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR098+1 : TPTP v8.1.0. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n018.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 : Fri Jul 15 21:15:33 EDT 2022
% Result : Theorem 219.81s 212.06s
% Output : Proof 219.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.10 % Problem : CSR098+1 : TPTP v8.1.0. Bugfixed v7.3.0.
% 0.09/0.11 % Command : leancop_casc.sh %s %d
% 0.09/0.31 % Computer : n018.cluster.edu
% 0.09/0.31 % Model : x86_64 x86_64
% 0.09/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.31 % Memory : 8042.1875MB
% 0.09/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.31 % CPULimit : 300
% 0.09/0.31 % WCLimit : 600
% 0.09/0.31 % DateTime : Sat Jun 11 10:51:10 EDT 2022
% 0.09/0.31 % CPUTime :
% 219.81/212.06 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 219.81/212.07 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 219.81/212.08
% 219.81/212.08 %-----------------------------------------------------
% 219.81/212.08 fof(kb_SUMOcache_6302, axiom, s__subclass(s__Amphibian, s__Agent), file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+3.ax', kb_SUMOcache_6302)).
% 219.81/212.08 fof(kb_SUMO_1122, axiom, ! [_1385587, _1385590] : (_1385587 = _1385590 => _1385590 = _1385587), file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax', kb_SUMO_1122)).
% 219.81/212.08 fof(local_3, axiom, s__Frog29_1 = s__Animal29_1, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', local_3)).
% 219.81/212.08 fof(prove_from_SUMO, conjecture, s__instance(s__Animal29_1, s__Amphibian), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_from_SUMO)).
% 219.81/212.08 fof(kb_SUMO_173, axiom, ! [_1387255, _1387258] : (_1387258 = _1387255 => ! [_1387272] : (s__instance(_1387272, s__SetOrClass) => (s__instance(_1387258, _1387272) <=> s__instance(_1387255, _1387272)))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax', kb_SUMO_173)).
% 219.81/212.08 fof(kb_SUMO_26, axiom, ! [_1388383, _1388386] : (s__subclass(_1388383, _1388386) => s__instance(_1388383, s__SetOrClass) & s__instance(_1388386, s__SetOrClass)), file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+0.ax', kb_SUMO_26)).
% 219.81/212.08 fof(local_1, axiom, s__instance(s__Frog29_1, s__Amphibian), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', local_1)).
% 219.81/212.08
% 219.81/212.08 cnf(1, plain, [-(s__subclass(s__Amphibian, s__Agent))], clausify(kb_SUMOcache_6302)).
% 219.81/212.08 cnf(2, plain, [_356748 = _356749, -(_356749 = _356748)], clausify(kb_SUMO_1122)).
% 219.81/212.08 cnf(3, plain, [-(s__Frog29_1 = s__Animal29_1)], clausify(local_3)).
% 219.81/212.08 cnf(4, plain, [s__instance(s__Animal29_1, s__Amphibian)], clausify(prove_from_SUMO)).
% 219.81/212.08 cnf(5, plain, [_343202 = _343201, s__instance(_343206, s__SetOrClass), -(s__instance(_343202, _343206)), s__instance(_343201, _343206)], clausify(kb_SUMO_173)).
% 219.81/212.08 cnf(6, plain, [s__subclass(_340792, _340793), -(s__instance(_340792, s__SetOrClass))], clausify(kb_SUMO_26)).
% 219.81/212.08 cnf(7, plain, [-(s__instance(s__Frog29_1, s__Amphibian))], clausify(local_1)).
% 219.81/212.08
% 219.81/212.08 cnf('1',plain,[s__instance(s__Animal29_1, s__Amphibian)],start(4)).
% 219.81/212.08 cnf('1.1',plain,[-(s__instance(s__Animal29_1, s__Amphibian)), s__Animal29_1 = s__Frog29_1, s__instance(s__Amphibian, s__SetOrClass), s__instance(s__Frog29_1, s__Amphibian)],extension(5,bind([[_343202, _343201, _343206], [s__Animal29_1, s__Frog29_1, s__Amphibian]]))).
% 219.81/212.08 cnf('1.1.1',plain,[-(s__Animal29_1 = s__Frog29_1), s__Frog29_1 = s__Animal29_1],extension(2,bind([[_356748, _356749], [s__Frog29_1, s__Animal29_1]]))).
% 219.81/212.08 cnf('1.1.1.1',plain,[-(s__Frog29_1 = s__Animal29_1)],extension(3)).
% 219.81/212.08 cnf('1.1.2',plain,[-(s__instance(s__Amphibian, s__SetOrClass)), s__subclass(s__Amphibian, s__Agent)],extension(6,bind([[_340792, _340793], [s__Amphibian, s__Agent]]))).
% 219.81/212.08 cnf('1.1.2.1',plain,[-(s__subclass(s__Amphibian, s__Agent))],extension(1)).
% 219.81/212.08 cnf('1.1.3',plain,[-(s__instance(s__Frog29_1, s__Amphibian))],extension(7)).
% 219.81/212.08 %-----------------------------------------------------
% 219.81/212.08
% 219.81/212.08 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------