%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEV606+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n027.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 : 300s
% DateTime : Tue May 5 06:53:10 PM UTC 2026
% Result : Theorem 7.75s 8.66s
% Output : Proof 7.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEV606+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.13 % Command : leancop_casc.sh %s %d
% 0.16/0.34 % Computer : n027.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Tue May 5 05:22:04 EDT 2026
% 0.16/0.35 % CPUTime :
% 4.77/4.87 *** Overflow of the global/trail stack in spite of garbage collection!
% 4.77/4.87 You can use the "-g kBytes" (GLOBALSIZE) option to have a larger stack.
% 4.77/4.87 Peak sizes were: global stack 130976 kbytes, trail stack 4192 kbytes
% 7.75/8.66 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.75/8.67 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.75/8.67
% 7.75/8.67 %-----------------------------------------------------
% 7.75/8.67 fof('_HAMMER_GOAL', conjecture, ! [_816756] : (cCoq_2eNumbers_2eBinNums_2eZ___24t(_816756) => ! [_816771] : (cCoq_2eNumbers_2eBinNums_2eZ___24t(_816771) => p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, _816756)) => p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, _816771)) => p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(_816771, _816771), cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(_816756, _816756))) => p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(_816771, _816756)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', '_HAMMER_GOAL')).
% 7.75/8.67 fof('Coq.ZArith.BinInt.Z.square_le_simpl_nonneg', axiom, ! [_818824] : (cCoq_2eNumbers_2eBinNums_2eZ___24t(_818824) => ! [_818839] : (cCoq_2eNumbers_2eBinNums_2eZ___24t(_818839) => p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, _818839)) => p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(_818824, _818824), cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(_818839, _818839))) => p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(_818824, _818839)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'Coq.ZArith.BinInt.Z.square_le_simpl_nonneg')).
% 7.75/8.67
% 7.75/8.67 cnf(1, plain, [-(cCoq_2eNumbers_2eBinNums_2eZ___24t(1364 ^ []))], clausify('_HAMMER_GOAL')).
% 7.75/8.67 cnf(2, plain, [-(cCoq_2eNumbers_2eBinNums_2eZ___24t(1365 ^ []))], clausify('_HAMMER_GOAL')).
% 7.75/8.67 cnf(3, plain, [-(p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, 1364 ^ [])))], clausify('_HAMMER_GOAL')).
% 7.75/8.67 cnf(4, plain, [-(p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(1365 ^ [], 1365 ^ []), cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(1364 ^ [], 1364 ^ []))))], clausify('_HAMMER_GOAL')).
% 7.75/8.67 cnf(5, plain, [p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(1365 ^ [], 1364 ^ []))], clausify('_HAMMER_GOAL')).
% 7.75/8.67 cnf(6, plain, [cCoq_2eNumbers_2eBinNums_2eZ___24t(_192659), cCoq_2eNumbers_2eBinNums_2eZ___24t(_192662), p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, _192662)), p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(_192659, _192659), cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(_192662, _192662))), -(p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(_192659, _192662)))], clausify('Coq.ZArith.BinInt.Z.square_le_simpl_nonneg')).
% 7.75/8.67
% 7.75/8.67 cnf('1',plain,[-(p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(1365 ^ [], 1365 ^ []), cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(1364 ^ [], 1364 ^ []))))],start(4)).
% 7.75/8.67 cnf('1.1',plain,[p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(1365 ^ [], 1365 ^ []), cCoq_2eZArith_2eBinIntDef_2eZ_2emul___24a2(1364 ^ [], 1364 ^ []))), cCoq_2eNumbers_2eBinNums_2eZ___24t(1365 ^ []), cCoq_2eNumbers_2eBinNums_2eZ___24t(1364 ^ []), p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, 1364 ^ [])), -(p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(1365 ^ [], 1364 ^ [])))],extension(6,bind([[_192659, _192662], [1365 ^ [], 1364 ^ []]]))).
% 7.75/8.67 cnf('1.1.1',plain,[-(cCoq_2eNumbers_2eBinNums_2eZ___24t(1365 ^ []))],extension(2)).
% 7.75/8.67 cnf('1.1.2',plain,[-(cCoq_2eNumbers_2eBinNums_2eZ___24t(1364 ^ []))],extension(1)).
% 7.75/8.67 cnf('1.1.3',plain,[-(p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(cCoq_2eNumbers_2eBinNums_2eZ0, 1364 ^ [])))],extension(3)).
% 7.75/8.67 cnf('1.1.4',plain,[p(cCoq_2eZArith_2eBinInt_2eZ_2ele___24a2(1365 ^ [], 1364 ^ []))],extension(5)).
% 7.75/8.67 %-----------------------------------------------------
% 7.75/8.68
% 7.75/8.68 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------