%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : NUN135-1.006 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n022.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:48:41 PM UTC 2026
% Result : Unsatisfiable 19.99s 5.30s
% Output : CNFRefutation 19.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUN135-1.006 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.16/0.33 % Computer : n022.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 04:48:36 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.33 20652: Facts:
% 0.16/0.33 20652: Id : 2, {_}: minus ?3 zero =>= ?3 [3] by rule1 ?3
% 0.16/0.33 20652: Id : 3, {_}: minus (s ?5) (s ?6) =>= minus ?5 ?6 [6, 5] by rule2 ?5 ?6
% 0.16/0.33 20652: Id : 4, {_}: <= zero ?8 =>= true [8] by rule3 ?8
% 0.16/0.33 20652: Id : 5, {_}: <= (s ?10) zero =>= false [10] by rule4 ?10
% 0.16/0.33 20652: Id : 6, {_}: <= (s ?12) (s ?13) =>= <= ?12 ?13 [13, 12] by rule5 ?12 ?13
% 0.16/0.33 20652: Id : 7, {_}: if true ?15 ?16 =>= ?15 [16, 15] by rule6 ?15 ?16
% 0.16/0.33 20652: Id : 8, {_}: if false ?18 ?19 =>= ?19 [19, 18] by rule7 ?18 ?19
% 0.16/0.33 20652: Id : 9, {_}: perfectp zero =>= false [] by rule8
% 0.16/0.33 20652: Id : 10, {_}:
% 0.16/0.33 perfectp (s ?22) =<= f ?22 (s zero) (s ?22) (s ?22)
% 0.16/0.33 [22] by rule9 ?22
% 0.16/0.33 20652: Id : 11, {_}: f zero ?24 zero ?25 =>= true [25, 24] by rule10 ?24 ?25
% 0.16/0.33 20652: Id : 12, {_}:
% 0.16/0.33 f zero ?27 (s ?28) ?29 =>= false
% 0.16/0.33 [29, 28, 27] by rule11 ?27 ?28 ?29
% 0.16/0.33 20652: Id : 13, {_}:
% 0.16/0.33 f (s ?31) zero ?32 ?33 =<= f ?31 ?33 (minus ?32 (s ?31)) ?33
% 0.16/0.33 [33, 32, 31] by rule12 ?31 ?32 ?33
% 0.16/0.33 20652: Id : 14, {_}:
% 0.16/0.33 f (s ?35) (s ?36) ?37 ?38
% 0.16/0.33 =<=
% 0.16/0.33 if (<= ?35 ?36) (f (s ?35) (minus ?36 ?35) ?37 ?38)
% 0.16/0.33 (f ?35 ?38 ?37 ?38)
% 0.16/0.33 [38, 37, 36, 35] by rule13 ?35 ?36 ?37 ?38
% 0.16/0.33 20652: Goal:
% 0.16/0.33 20652: Id : 1, {_}: perfectp ?1 =>= true [1] by goal ?1
% 19.99/5.30 Statistics :
% 19.99/5.30 Max weight : 44
% 19.99/5.30 Found proof, 4.965801s
% 19.99/5.30 % SZS status Unsatisfiable for theBenchmark.p
% 19.99/5.30 % SZS output start CNFRefutation for theBenchmark.p
% 19.99/5.30 Id : 11, {_}: f zero ?24 zero ?25 =>= true [25, 24] by rule10 ?24 ?25
% 19.99/5.30 Id : 39, {_}: f (s ?90) zero ?91 ?92 =?= f ?90 ?92 (minus ?91 (s ?90)) ?92 [92, 91, 90] by rule12 ?90 ?91 ?92
% 19.99/5.30 Id : 7, {_}: if true ?15 ?16 =>= ?15 [16, 15] by rule6 ?15 ?16
% 19.99/5.30 Id : 4, {_}: <= zero ?8 =>= true [8] by rule3 ?8
% 19.99/5.30 Id : 2, {_}: minus ?3 zero =>= ?3 [3] by rule1 ?3
% 19.99/5.30 Id : 6, {_}: <= (s ?12) (s ?13) =>= <= ?12 ?13 [13, 12] by rule5 ?12 ?13
% 19.99/5.30 Id : 3, {_}: minus (s ?5) (s ?6) =>= minus ?5 ?6 [6, 5] by rule2 ?5 ?6
% 19.99/5.30 Id : 8, {_}: if false ?18 ?19 =>= ?19 [19, 18] by rule7 ?18 ?19
% 19.99/5.30 Id : 5, {_}: <= (s ?10) zero =>= false [10] by rule4 ?10
% 19.99/5.30 Id : 44, {_}: f (s ?110) (s ?111) ?112 ?113 =<= if (<= ?110 ?111) (f (s ?110) (minus ?111 ?110) ?112 ?113) (f ?110 ?113 ?112 ?113) [113, 112, 111, 110] by rule13 ?110 ?111 ?112 ?113
% 19.99/5.30 Id : 10, {_}: perfectp (s ?22) =>= f ?22 (s zero) (s ?22) (s ?22) [22] by rule9 ?22
% 19.99/5.30 Id : 52, {_}: f (s (s ?144)) (s zero) ?145 ?146 =<= if false (f (s (s ?144)) (minus zero (s ?144)) ?145 ?146) (f (s ?144) ?146 ?145 ?146) [146, 145, 144] by Super 44 with 5 at 1,3
% 19.99/5.30 Id : 66, {_}: f (s (s ?144)) (s zero) ?145 ?146 =>= f (s ?144) ?146 ?145 ?146 [146, 145, 144] by Demod 52 with 8 at 3
% 19.99/5.30 Id : 49, {_}: f (s (s ?131)) (s (s ?132)) ?133 ?134 =<= if (<= (s ?131) (s ?132)) (f (s (s ?131)) (minus ?132 ?131) ?133 ?134) (f (s ?131) ?134 ?133 ?134) [134, 133, 132, 131] by Super 44 with 3 at 2,2,3
% 19.99/5.30 Id : 515, {_}: f (s (s ?797)) (s (s ?798)) ?799 ?800 =<= if (<= ?797 ?798) (f (s (s ?797)) (minus ?798 ?797) ?799 ?800) (f (s ?797) ?800 ?799 ?800) [800, 799, 798, 797] by Demod 49 with 6 at 1,3
% 19.99/5.30 Id : 531, {_}: f (s (s (s ?863))) (s (s (s ?864))) ?865 ?866 =<= if (<= (s ?863) (s ?864)) (f (s (s (s ?863))) (minus ?864 ?863) ?865 ?866) (f (s (s ?863)) ?866 ?865 ?866) [866, 865, 864, 863] by Super 515 with 3 at 2,2,3
% 19.99/5.30 Id : 2638, {_}: f (s (s (s ?3485))) (s (s (s ?3486))) ?3487 ?3488 =<= if (<= ?3485 ?3486) (f (s (s (s ?3485))) (minus ?3486 ?3485) ?3487 ?3488) (f (s (s ?3485)) ?3488 ?3487 ?3488) [3488, 3487, 3486, 3485] by Demod 531 with 6 at 1,3
% 19.99/5.30 Id : 2679, {_}: f (s (s (s (s ?3652)))) (s (s (s (s ?3653)))) ?3654 ?3655 =<= if (<= (s ?3652) (s ?3653)) (f (s (s (s (s ?3652)))) (minus ?3653 ?3652) ?3654 ?3655) (f (s (s (s ?3652))) ?3655 ?3654 ?3655) [3655, 3654, 3653, 3652] by Super 2638 with 3 at 2,2,3
% 19.99/5.30 Id : 5061, {_}: f (s (s (s (s ?6773)))) (s (s (s (s ?6774)))) ?6775 ?6776 =<= if (<= ?6773 ?6774) (f (s (s (s (s ?6773)))) (minus ?6774 ?6773) ?6775 ?6776) (f (s (s (s ?6773))) ?6776 ?6775 ?6776) [6776, 6775, 6774, 6773] by Demod 2679 with 6 at 1,3
% 19.99/5.30 Id : 5117, {_}: f (s (s (s (s zero)))) (s (s (s (s ?7001)))) ?7002 ?7003 =?= if (<= zero ?7001) (f (s (s (s (s zero)))) ?7001 ?7002 ?7003) (f (s (s (s zero))) ?7003 ?7002 ?7003) [7003, 7002, 7001] by Super 5061 with 2 at 2,2,3
% 19.99/5.30 Id : 5138, {_}: f (s (s (s (s zero)))) (s (s (s (s ?7001)))) ?7002 ?7003 =?= if true (f (s (s (s (s zero)))) ?7001 ?7002 ?7003) (f (s (s (s zero))) ?7003 ?7002 ?7003) [7003, 7002, 7001] by Demod 5117 with 4 at 1,3
% 19.99/5.30 Id : 5139, {_}: f (s (s (s (s zero)))) (s (s (s (s ?7001)))) ?7002 ?7003 =>= f (s (s (s (s zero)))) ?7001 ?7002 ?7003 [7003, 7002, 7001] by Demod 5138 with 7 at 3
% 19.99/5.30 Id : 535, {_}: f (s (s (s ?880))) (s (s zero)) ?881 ?882 =<= if false (f (s (s (s ?880))) (minus zero (s ?880)) ?881 ?882) (f (s (s ?880)) ?882 ?881 ?882) [882, 881, 880] by Super 515 with 5 at 1,3
% 19.99/5.30 Id : 549, {_}: f (s (s (s ?880))) (s (s zero)) ?881 ?882 =>= f (s (s ?880)) ?882 ?881 ?882 [882, 881, 880] by Demod 535 with 8 at 3
% 19.99/5.30 Id : 2678, {_}: f (s (s (s zero))) (s (s (s ?3648))) ?3649 ?3650 =?= if (<= zero ?3648) (f (s (s (s zero))) ?3648 ?3649 ?3650) (f (s (s zero)) ?3650 ?3649 ?3650) [3650, 3649, 3648] by Super 2638 with 2 at 2,2,3
% 19.99/5.30 Id : 2696, {_}: f (s (s (s zero))) (s (s (s ?3648))) ?3649 ?3650 =?= if true (f (s (s (s zero))) ?3648 ?3649 ?3650) (f (s (s zero)) ?3650 ?3649 ?3650) [3650, 3649, 3648] by Demod 2678 with 4 at 1,3
% 19.99/5.30 Id : 2697, {_}: f (s (s (s zero))) (s (s (s ?3648))) ?3649 ?3650 =>= f (s (s (s zero))) ?3648 ?3649 ?3650 [3650, 3649, 3648] by Demod 2696 with 7 at 3
% 19.99/5.30 Id : 110, {_}: f (s ?266) zero (s ?267) ?268 =?= f ?266 ?268 (minus ?267 ?266) ?268 [268, 267, 266] by Super 39 with 3 at 3,3
% 19.99/5.30 Id : 759, {_}: f (s (s ?1303)) zero (s (s ?1304)) ?1305 =?= f (s ?1303) ?1305 (minus ?1304 ?1303) ?1305 [1305, 1304, 1303] by Super 110 with 3 at 3,3
% 19.99/5.30 Id : 1233, {_}: f (s (s (s ?1936))) zero (s (s (s ?1937))) ?1938 =?= f (s (s ?1936)) ?1938 (minus ?1937 ?1936) ?1938 [1938, 1937, 1936] by Super 759 with 3 at 3,3
% 19.99/5.30 Id : 1234, {_}: f (s (s (s zero))) zero (s (s (s ?1940))) ?1941 =>= f (s (s zero)) ?1941 ?1940 ?1941 [1941, 1940] by Super 1233 with 2 at 3,3
% 19.99/5.30 Id : 530, {_}: f (s (s zero)) (s (s ?859)) ?860 ?861 =?= if (<= zero ?859) (f (s (s zero)) ?859 ?860 ?861) (f (s zero) ?861 ?860 ?861) [861, 860, 859] by Super 515 with 2 at 2,2,3
% 19.99/5.30 Id : 544, {_}: f (s (s zero)) (s (s ?859)) ?860 ?861 =?= if true (f (s (s zero)) ?859 ?860 ?861) (f (s zero) ?861 ?860 ?861) [861, 860, 859] by Demod 530 with 4 at 1,3
% 19.99/5.30 Id : 545, {_}: f (s (s zero)) (s (s ?859)) ?860 ?861 =>= f (s (s zero)) ?859 ?860 ?861 [861, 860, 859] by Demod 544 with 7 at 3
% 19.99/5.30 Id : 760, {_}: f (s (s zero)) zero (s (s ?1307)) ?1308 =>= f (s zero) ?1308 ?1307 ?1308 [1308, 1307] by Super 759 with 2 at 3,3
% 19.99/5.30 Id : 48, {_}: f (s zero) (s ?127) ?128 ?129 =?= if (<= zero ?127) (f (s zero) ?127 ?128 ?129) (f zero ?129 ?128 ?129) [129, 128, 127] by Super 44 with 2 at 2,2,3
% 19.99/5.30 Id : 61, {_}: f (s zero) (s ?127) ?128 ?129 =?= if true (f (s zero) ?127 ?128 ?129) (f zero ?129 ?128 ?129) [129, 128, 127] by Demod 48 with 4 at 1,3
% 19.99/5.30 Id : 62, {_}: f (s zero) (s ?127) ?128 ?129 =>= f (s zero) ?127 ?128 ?129 [129, 128, 127] by Demod 61 with 7 at 3
% 19.99/5.30 Id : 111, {_}: f (s zero) zero (s ?270) ?271 =>= f zero ?271 ?270 ?271 [271, 270] by Super 110 with 2 at 3,3
% 19.99/5.30 Id : 5245, {_}: true === true [] by Demod 5244 with 11 at 2
% 19.99/5.30 Id : 5244, {_}: f zero (s (s (s (s (s (s zero)))))) zero (s (s (s (s (s (s zero)))))) =>= true [] by Demod 5243 with 111 at 2
% 19.99/5.30 Id : 5243, {_}: f (s zero) zero (s zero) (s (s (s (s (s (s zero)))))) =>= true [] by Demod 5242 with 62 at 2
% 19.99/5.30 Id : 5242, {_}: f (s zero) (s zero) (s zero) (s (s (s (s (s (s zero)))))) =>= true [] by Demod 5241 with 62 at 2
% 19.99/5.30 Id : 5241, {_}: f (s zero) (s (s zero)) (s zero) (s (s (s (s (s (s zero)))))) =>= true [] by Demod 5240 with 62 at 2
% 19.99/5.30 Id : 5240, {_}: f (s zero) (s (s (s zero))) (s zero) (s (s (s (s (s (s zero)))))) =>= true [] by Demod 5239 with 62 at 2
% 19.99/5.30 Id : 5239, {_}: f (s zero) (s (s (s (s zero)))) (s zero) (s (s (s (s (s (s zero)))))) =>= true [] by Demod 5238 with 62 at 2
% 19.99/5.30 Id : 5238, {_}: f (s zero) (s (s (s (s (s zero))))) (s zero) (s (s (s (s (s (s zero)))))) =>= true [] by Demod 5237 with 62 at 2
% 19.99/5.30 Id : 5237, {_}: f (s zero) (s (s (s (s (s (s zero)))))) (s zero) (s (s (s (s (s (s zero)))))) =>= true [] by Demod 5236 with 760 at 2
% 19.99/5.30 Id : 5236, {_}: f (s (s zero)) zero (s (s (s zero))) (s (s (s (s (s (s zero)))))) =>= true [] by Demod 5235 with 545 at 2
% 19.99/5.30 Id : 5235, {_}: f (s (s zero)) (s (s zero)) (s (s (s zero))) (s (s (s (s (s (s zero)))))) =>= true [] by Demod 5234 with 545 at 2
% 19.99/5.30 Id : 5234, {_}: f (s (s zero)) (s (s (s (s zero)))) (s (s (s zero))) (s (s (s (s (s (s zero)))))) =>= true [] by Demod 5233 with 545 at 2
% 19.99/5.30 Id : 5233, {_}: f (s (s zero)) (s (s (s (s (s (s zero)))))) (s (s (s zero))) (s (s (s (s (s (s zero)))))) =>= true [] by Demod 5232 with 1234 at 2
% 19.99/5.30 Id : 5232, {_}: f (s (s (s zero))) zero (s (s (s (s (s (s zero)))))) (s (s (s (s (s (s zero)))))) =>= true [] by Demod 5231 with 2697 at 2
% 19.99/5.30 Id : 5231, {_}: f (s (s (s zero))) (s (s (s zero))) (s (s (s (s (s (s zero)))))) (s (s (s (s (s (s zero)))))) =>= true [] by Demod 5230 with 2697 at 2
% 19.99/5.30 Id : 5230, {_}: f (s (s (s zero))) (s (s (s (s (s (s zero)))))) (s (s (s (s (s (s zero)))))) (s (s (s (s (s (s zero)))))) =>= true [] by Demod 5180 with 549 at 2
% 19.99/5.30 Id : 5180, {_}: f (s (s (s (s zero)))) (s (s zero)) (s (s (s (s (s (s zero)))))) (s (s (s (s (s (s zero)))))) =>= true [] by Super 87 with 5139 at 2
% 19.99/5.30 Id : 87, {_}: f (s ?208) (s (s (s ?208))) (s (s (s ?208))) (s (s (s ?208))) =>= true [208] by Super 34 with 66 at 2
% 19.99/5.30 Id : 34, {_}: f ?79 (s zero) (s ?79) (s ?79) =>= true [79] by Super 1 with 10 at 2
% 19.99/5.30 Id : 1, {_}: perfectp ?1 =>= true [1] by goal ?1
% 19.99/5.30 % SZS output end CNFRefutation for theBenchmark.p
% 19.99/5.30 20654: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 4.969916 using lpo
%------------------------------------------------------------------------------