%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SCT165+1 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n016.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 : Mon Jul 18 21:46:11 EDT 2022
% Result : Theorem 149.07s 144.99s
% Output : Proof 149.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SCT165+1 : TPTP v8.1.0. Released v5.2.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n016.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Fri Jul 1 22:41:58 EDT 2022
% 0.12/0.33 % CPUTime :
% 149.07/144.99 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 149.07/145.00 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 149.07/145.00
% 149.07/145.00 %-----------------------------------------------------
% 149.07/145.00 fof(fact_not__add__less2, axiom, ! [_224756, _224759] : ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat), hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _224759), _224756)), _224756)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fact_not__add__less2)).
% 149.07/145.00 fof(fact_finite__indi, axiom, c_Finite__Set_Ofinite(tc_Arrow__Order__Mirabelle_Oindi, c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fact_finite__indi)).
% 149.07/145.00 fof(fact_finite__imageI, axiom, ! [_225483, _225486, _225489, _225492] : (c_Finite__Set_Ofinite(_225492, _225489) => c_Finite__Set_Ofinite(_225486, c_Set_Oimage(_225492, _225486, _225483, _225489))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fact_finite__imageI)).
% 149.07/145.00 fof(fact_rangeI, axiom, ! [_225720, _225723, _225726, _225729] : hBOOL(hAPP(hAPP(c_member(_225729), hAPP(_225726, _225723)), c_Set_Oimage(_225720, _225729, _225726, c_Orderings_Otop__class_Otop(tc_fun(_225720, tc_HOL_Obool))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fact_rangeI)).
% 149.07/145.00 fof(fact_finite__nat__set__iff__bounded, axiom, ! [_225982] : (c_Finite__Set_Ofinite(tc_Nat_Onat, _225982) <=> ? [_226000] : ! [_226008] : (hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat), _226008), _225982)) => hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat), _226008), _226000)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fact_finite__nat__set__iff__bounded)).
% 149.07/145.00
% 149.07/145.00 cnf(1, plain, [hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat), hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _48193), _48192)), _48192))], clausify(fact_not__add__less2)).
% 149.07/145.00 cnf(2, plain, [-(c_Finite__Set_Ofinite(tc_Arrow__Order__Mirabelle_Oindi, c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool))))], clausify(fact_finite__indi)).
% 149.07/145.00 cnf(3, plain, [c_Finite__Set_Ofinite(_73029, _73028), -(c_Finite__Set_Ofinite(_73027, c_Set_Oimage(_73029, _73027, _73026, _73028)))], clausify(fact_finite__imageI)).
% 149.07/145.00 cnf(4, plain, [-(hBOOL(hAPP(hAPP(c_member(_75491), hAPP(_75490, _75489)), c_Set_Oimage(_75488, _75491, _75490, c_Orderings_Otop__class_Otop(tc_fun(_75488, tc_HOL_Obool))))))], clausify(fact_rangeI)).
% 149.07/145.00 cnf(5, plain, [c_Finite__Set_Ofinite(tc_Nat_Onat, _76573), hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat), _122371), _76573)), -(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat), _122371), 212 ^ [_76573])))], clausify(fact_finite__nat__set__iff__bounded)).
% 149.07/145.00
% 149.07/145.00 cnf('1',plain,[hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat), hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), 212 ^ [c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi, tc_Nat_Onat, hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool)))])), 212 ^ [c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi, tc_Nat_Onat, hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool)))]))],start(1,bind([[_48193, _48192], [_219881, 212 ^ [c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi, tc_Nat_Onat, hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool)))]]]))).
% 149.07/145.00 cnf('1.1',plain,[-(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat), hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), 212 ^ [c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi, tc_Nat_Onat, hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool)))])), 212 ^ [c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi, tc_Nat_Onat, hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool)))]))), c_Finite__Set_Ofinite(tc_Nat_Onat, c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi, tc_Nat_Onat, hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool)))), hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat), hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), 212 ^ [c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi, tc_Nat_Onat, hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool)))])), c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi, tc_Nat_Onat, hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool)))))],extension(5,bind([[_122371, _76573], [hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), 212 ^ [c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi, tc_Nat_Onat, hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool)))]), c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi, tc_Nat_Onat, hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool)))]]))).
% 149.07/145.00 cnf('1.1.1',plain,[-(c_Finite__Set_Ofinite(tc_Nat_Onat, c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi, tc_Nat_Onat, hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool))))), c_Finite__Set_Ofinite(tc_Arrow__Order__Mirabelle_Oindi, c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool)))],extension(3,bind([[_73027, _73026, _73029, _73028], [tc_Nat_Onat, hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), tc_Arrow__Order__Mirabelle_Oindi, c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool))]]))).
% 149.07/145.00 cnf('1.1.1.1',plain,[-(c_Finite__Set_Ofinite(tc_Arrow__Order__Mirabelle_Oindi, c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool))))],extension(2)).
% 149.07/145.00 cnf('1.1.2',plain,[-(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat), hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), 212 ^ [c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi, tc_Nat_Onat, hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool)))])), c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi, tc_Nat_Onat, hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool))))))],extension(4,bind([[_75489, _75491, _75490, _75488], [212 ^ [c_Set_Oimage(tc_Arrow__Order__Mirabelle_Oindi, tc_Nat_Onat, hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi, tc_HOL_Obool)))], tc_Nat_Onat, hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat), _219881), tc_Arrow__Order__Mirabelle_Oindi]]))).
% 149.07/145.00 %-----------------------------------------------------
% 149.07/145.01
% 149.07/145.01 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------