%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : ARI765-2 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n010.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:16:51 PM UTC 2026
% Result : Unsatisfiable 106.92s 27.11s
% Output : CNFRefutation 106.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : ARI765-2 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.15/0.34 % Computer : n010.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Mon May 4 18:43:06 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 14293: Facts:
% 0.15/0.34 14293: Id : 2, {_}: le zero ?3 =>= true [3] by rule1 ?3
% 0.15/0.34 14293: Id : 3, {_}: le (s ?5) zero =>= false [5] by rule2 ?5
% 0.15/0.34 14293: Id : 4, {_}: le (s ?7) (s ?8) =>= le ?7 ?8 [8, 7] by rule3 ?7 ?8
% 0.15/0.34 14293: Id : 5, {_}: minus zero ?10 =>= zero [10] by rule4 ?10
% 0.15/0.34 14293: Id : 6, {_}:
% 0.15/0.34 minus (s ?12) ?13 =<= if_minus (le (s ?12) ?13) (s ?12) ?13
% 0.15/0.34 [13, 12] by rule5 ?12 ?13
% 0.15/0.34 14293: Id : 7, {_}: if_minus true (s ?15) ?16 =>= zero [16, 15] by rule6 ?15 ?16
% 0.15/0.34 14293: Id : 8, {_}:
% 0.15/0.34 if_minus false (s ?18) ?19 =>= s (minus ?18 ?19)
% 0.15/0.34 [19, 18] by rule7 ?18 ?19
% 0.15/0.34 14293: Id : 9, {_}: quot zero (s ?21) =>= zero [21] by rule8 ?21
% 0.15/0.34 14293: Id : 10, {_}:
% 0.15/0.34 quot (s ?23) (s ?24) =<= s (quot (minus ?23 ?24) (s ?24))
% 0.15/0.34 [24, 23] by rule9 ?23 ?24
% 0.15/0.34 14293: Id : 11, {_}: log (s zero) =>= zero [] by rule10
% 0.15/0.34 14293: Id : 12, {_}:
% 0.15/0.34 log (s (s ?27)) =<= s (log (s (quot ?27 (s (s zero)))))
% 0.15/0.34 [27] by rule11 ?27
% 0.15/0.34 14293: Id : 13, {_}: d zero =>= zero [] by double1
% 0.15/0.34 14293: Id : 14, {_}: d (s ?30) =<= s (s (d ?30)) [30] by double2 ?30
% 0.15/0.34 14293: Id : 15, {_}: e zero =>= s zero [] by exp1
% 0.15/0.34 14293: Id : 16, {_}: e (s ?33) =>= d (e ?33) [33] by exp2 ?33
% 0.15/0.34 14293: Goal:
% 0.15/0.34 14293: Id : 1, {_}: log (e ?1) =?= s (s (s (s zero))) [1] by goal ?1
% 106.92/27.11 Goal subsumed
% 106.92/27.11 Statistics :
% 106.92/27.11 Max weight : 12
% 106.92/27.11 Found proof, 26.770347s
% 106.92/27.11 % SZS status Unsatisfiable for theBenchmark.p
% 106.92/27.11 % SZS output start CNFRefutation for theBenchmark.p
% 106.92/27.11 Id : 15, {_}: e zero =>= s zero [] by exp1
% 106.92/27.11 Id : 16, {_}: e (s ?33) =>= d (e ?33) [33] by exp2 ?33
% 106.92/27.11 Id : 95, {_}: e (s ?184) =>= d (e ?184) [184] by exp2 ?184
% 106.92/27.11 Id : 11, {_}: log (s zero) =>= zero [] by rule10
% 106.92/27.11 Id : 64, {_}: log (s (s ?143)) =<= s (log (s (quot ?143 (s (s zero))))) [143] by rule11 ?143
% 106.92/27.11 Id : 9, {_}: quot zero (s ?21) =>= zero [21] by rule8 ?21
% 106.92/27.11 Id : 7, {_}: if_minus true (s ?15) ?16 =>= zero [16, 15] by rule6 ?15 ?16
% 106.92/27.11 Id : 2, {_}: le zero ?3 =>= true [3] by rule1 ?3
% 106.92/27.11 Id : 8, {_}: if_minus false (s ?18) ?19 =>= s (minus ?18 ?19) [19, 18] by rule7 ?18 ?19
% 106.92/27.11 Id : 3, {_}: le (s ?5) zero =>= false [5] by rule2 ?5
% 106.92/27.11 Id : 4, {_}: le (s ?7) (s ?8) =>= le ?7 ?8 [8, 7] by rule3 ?7 ?8
% 106.92/27.11 Id : 25, {_}: minus (s ?50) ?51 =<= if_minus (le (s ?50) ?51) (s ?50) ?51 [51, 50] by rule5 ?50 ?51
% 106.92/27.11 Id : 10, {_}: quot (s ?23) (s ?24) =<= s (quot (minus ?23 ?24) (s ?24)) [24, 23] by rule9 ?23 ?24
% 106.92/27.12 Id : 12, {_}: log (s (s ?27)) =<= s (log (s (quot ?27 (s (s zero))))) [27] by rule11 ?27
% 106.92/27.12 Id : 14, {_}: d (s ?30) =<= s (s (d ?30)) [30] by double2 ?30
% 106.92/27.12 Id : 13, {_}: d zero =>= zero [] by double1
% 106.92/27.12 Id : 85, {_}: d (s ?177) =<= s (s (d ?177)) [177] by double2 ?177
% 106.92/27.12 Id : 86, {_}: d (s zero) =<= s (s zero) [] by Super 85 with 13 at 1,1,3
% 106.92/27.12 Id : 101, {_}: log (s (s ?27)) =<= s (log (s (quot ?27 (d (s zero))))) [27] by Demod 12 with 86 at 2,1,1,1,3
% 106.92/27.12 Id : 103, {_}: quot (s ?196) (s (s zero)) =<= s (quot (minus ?196 (s zero)) (d (s zero))) [196] by Super 10 with 86 at 2,1,3
% 106.92/27.12 Id : 118, {_}: quot (s ?196) (d (s zero)) =<= s (quot (minus ?196 (s zero)) (d (s zero))) [196] by Demod 103 with 86 at 2,2
% 106.92/27.12 Id : 27, {_}: minus (s ?55) (s ?56) =<= if_minus (le ?55 ?56) (s ?55) (s ?56) [56, 55] by Super 25 with 4 at 1,3
% 106.92/27.12 Id : 234, {_}: le (d (s ?326)) zero =>= false [326] by Super 3 with 14 at 1,2
% 106.92/27.12 Id : 236, {_}: le (d (d (s ?331))) zero =>= false [331] by Super 234 with 14 at 1,1,2
% 106.92/27.12 Id : 803, {_}: minus (s (d (d (s ?979)))) (s zero) =<= if_minus false (s (d (d (s ?979)))) (s zero) [979] by Super 27 with 236 at 1,3
% 106.92/27.12 Id : 813, {_}: minus (s (d (d (s ?979)))) (s zero) =<= s (minus (d (d (s ?979))) (s zero)) [979] by Demod 803 with 8 at 3
% 106.92/27.12 Id : 77, {_}: if_minus false (d (s ?155)) ?156 =<= s (minus (s (d ?155)) ?156) [156, 155] by Super 8 with 14 at 2,2
% 106.92/27.12 Id : 82, {_}: le (d (s ?170)) zero =>= false [170] by Super 3 with 14 at 1,2
% 106.92/27.12 Id : 233, {_}: minus (s (d (s ?324))) (s zero) =<= if_minus false (s (d (s ?324))) (s zero) [324] by Super 27 with 82 at 1,3
% 106.92/27.12 Id : 241, {_}: minus (s (d (s ?324))) (s zero) =<= s (minus (d (s ?324)) (s zero)) [324] by Demod 233 with 8 at 3
% 106.92/27.12 Id : 5157, {_}: minus (s (d (d (s ?6720)))) (s zero) =<= s (minus (d (d (s ?6720))) (s zero)) [6720] by Demod 803 with 8 at 3
% 106.92/27.12 Id : 5163, {_}: minus (s (d (d (s (s zero))))) (s zero) =<= s (minus (d (d (d (s zero)))) (s zero)) [] by Super 5157 with 86 at 1,1,1,1,3
% 106.92/27.12 Id : 5265, {_}: minus (s (d (d (d (s zero))))) (s zero) =<= s (minus (d (d (d (s zero)))) (s zero)) [] by Demod 5163 with 86 at 1,1,1,1,2
% 106.92/27.12 Id : 1571, {_}: minus (s (d (s ?2084))) (s zero) =<= s (minus (d (s ?2084)) (s zero)) [2084] by Demod 233 with 8 at 3
% 106.92/27.12 Id : 1576, {_}: minus (s (d (s (s zero)))) (s zero) =<= s (minus (d (d (s zero))) (s zero)) [] by Super 1571 with 86 at 1,1,1,3
% 106.92/27.12 Id : 1606, {_}: minus (s (d (d (s zero)))) (s zero) =<= s (minus (d (d (s zero))) (s zero)) [] by Demod 1576 with 86 at 1,1,1,2
% 106.92/27.12 Id : 190, {_}: minus (s ?267) (s ?268) =<= if_minus (le ?267 ?268) (s ?267) (s ?268) [268, 267] by Super 25 with 4 at 1,3
% 106.92/27.12 Id : 202, {_}: minus (s (s ?302)) (s zero) =<= if_minus false (s (s ?302)) (s zero) [302] by Super 190 with 3 at 1,3
% 106.92/27.12 Id : 217, {_}: minus (s (s ?302)) (s zero) =<= s (minus (s ?302) (s zero)) [302] by Demod 202 with 8 at 3
% 106.92/27.12 Id : 730, {_}: minus (s (s ?929)) (s zero) =<= s (minus (s ?929) (s zero)) [929] by Demod 202 with 8 at 3
% 106.92/27.12 Id : 734, {_}: minus (s (s (s zero))) (s zero) =<= s (minus (d (s zero)) (s zero)) [] by Super 730 with 86 at 1,1,3
% 106.92/27.12 Id : 755, {_}: minus (s (d (s zero))) (s zero) =<= s (minus (d (s zero)) (s zero)) [] by Demod 734 with 86 at 1,1,2
% 106.92/27.12 Id : 201, {_}: minus (s zero) (s ?300) =<= if_minus true (s zero) (s ?300) [300] by Super 190 with 2 at 1,3
% 106.92/27.12 Id : 216, {_}: minus (s zero) (s ?300) =>= zero [300] by Demod 201 with 7 at 3
% 106.92/27.12 Id : 738, {_}: minus (s (s zero)) (s zero) =>= s zero [] by Super 730 with 216 at 1,3
% 106.92/27.12 Id : 761, {_}: minus (d (s zero)) (s zero) =>= s zero [] by Demod 738 with 86 at 1,2
% 106.92/27.12 Id : 1090, {_}: minus (s (d (s zero))) (s zero) =>= s (s zero) [] by Demod 755 with 761 at 1,3
% 106.92/27.12 Id : 1091, {_}: minus (s (d (s zero))) (s zero) =>= d (s zero) [] by Demod 1090 with 86 at 3
% 106.92/27.12 Id : 1092, {_}: minus (s (s (d (s zero)))) (s zero) =>= s (d (s zero)) [] by Super 217 with 1091 at 1,3
% 106.92/27.12 Id : 1115, {_}: minus (d (s (s zero))) (s zero) =>= s (d (s zero)) [] by Demod 1092 with 14 at 1,2
% 106.92/27.12 Id : 1116, {_}: minus (d (d (s zero))) (s zero) =>= s (d (s zero)) [] by Demod 1115 with 86 at 1,1,2
% 106.92/27.12 Id : 1607, {_}: minus (s (d (d (s zero)))) (s zero) =>= s (s (d (s zero))) [] by Demod 1606 with 1116 at 1,3
% 106.92/27.12 Id : 1608, {_}: minus (s (d (d (s zero)))) (s zero) =>= d (s (s zero)) [] by Demod 1607 with 14 at 3
% 106.92/27.12 Id : 1609, {_}: minus (s (d (d (s zero)))) (s zero) =>= d (d (s zero)) [] by Demod 1608 with 86 at 1,3
% 106.92/27.12 Id : 2724, {_}: if_minus false (d (s (d (s zero)))) (s zero) =>= s (d (d (s zero))) [] by Super 77 with 1609 at 1,3
% 106.92/27.12 Id : 1232, {_}: minus (s (s (d ?1502))) (s zero) =>= if_minus false (d (s ?1502)) (s zero) [1502] by Super 217 with 77 at 3
% 106.92/27.12 Id : 1248, {_}: minus (d (s ?1502)) (s zero) =<= if_minus false (d (s ?1502)) (s zero) [1502] by Demod 1232 with 14 at 1,2
% 106.92/27.12 Id : 2727, {_}: minus (d (s (d (s zero)))) (s zero) =>= s (d (d (s zero))) [] by Demod 2724 with 1248 at 2
% 106.92/27.12 Id : 3272, {_}: minus (s (d (s (d (s zero))))) (s zero) =>= s (s (d (d (s zero)))) [] by Super 241 with 2727 at 1,3
% 106.92/27.12 Id : 3287, {_}: minus (s (d (s (d (s zero))))) (s zero) =>= d (s (d (s zero))) [] by Demod 3272 with 14 at 3
% 106.92/27.12 Id : 9251, {_}: if_minus false (d (s (s (d (s zero))))) (s zero) =>= s (d (s (d (s zero)))) [] by Super 77 with 3287 at 1,3
% 106.92/27.12 Id : 9261, {_}: minus (d (s (s (d (s zero))))) (s zero) =>= s (d (s (d (s zero)))) [] by Demod 9251 with 1248 at 2
% 106.92/27.12 Id : 9262, {_}: minus (d (d (s (s zero)))) (s zero) =>= s (d (s (d (s zero)))) [] by Demod 9261 with 14 at 1,1,2
% 106.92/27.12 Id : 9263, {_}: minus (d (d (d (s zero)))) (s zero) =>= s (d (s (d (s zero)))) [] by Demod 9262 with 86 at 1,1,1,2
% 106.92/27.12 Id : 10002, {_}: minus (s (d (d (d (s zero))))) (s zero) =>= s (s (d (s (d (s zero))))) [] by Demod 5265 with 9263 at 1,3
% 106.92/27.12 Id : 10003, {_}: minus (s (d (d (d (s zero))))) (s zero) =>= d (s (s (d (s zero)))) [] by Demod 10002 with 14 at 3
% 106.92/27.12 Id : 10004, {_}: minus (s (d (d (d (s zero))))) (s zero) =>= d (d (s (s zero))) [] by Demod 10003 with 14 at 1,3
% 106.92/27.12 Id : 10005, {_}: minus (s (d (d (d (s zero))))) (s zero) =>= d (d (d (s zero))) [] by Demod 10004 with 86 at 1,1,3
% 106.92/27.12 Id : 10012, {_}: if_minus false (d (s (d (d (s zero))))) (s zero) =>= s (d (d (d (s zero)))) [] by Super 77 with 10005 at 1,3
% 106.92/27.12 Id : 10016, {_}: minus (d (s (d (d (s zero))))) (s zero) =>= s (d (d (d (s zero)))) [] by Demod 10012 with 1248 at 2
% 106.92/27.12 Id : 10918, {_}: minus (s (d (s (d (d (s zero)))))) (s zero) =>= s (s (d (d (d (s zero))))) [] by Super 241 with 10016 at 1,3
% 106.92/27.12 Id : 10935, {_}: minus (s (d (s (d (d (s zero)))))) (s zero) =>= d (s (d (d (s zero)))) [] by Demod 10918 with 14 at 3
% 106.92/27.12 Id : 35754, {_}: if_minus false (d (s (s (d (d (s zero)))))) (s zero) =>= s (d (s (d (d (s zero))))) [] by Super 77 with 10935 at 1,3
% 106.92/27.12 Id : 35770, {_}: minus (d (s (s (d (d (s zero)))))) (s zero) =>= s (d (s (d (d (s zero))))) [] by Demod 35754 with 1248 at 2
% 106.92/27.12 Id : 35771, {_}: minus (d (d (s (d (s zero))))) (s zero) =>= s (d (s (d (d (s zero))))) [] by Demod 35770 with 14 at 1,1,2
% 106.92/27.12 Id : 35815, {_}: minus (s (d (d (s (d (s zero)))))) (s zero) =>= s (s (d (s (d (d (s zero)))))) [] by Super 813 with 35771 at 1,3
% 106.92/27.12 Id : 35820, {_}: minus (s (d (d (s (d (s zero)))))) (s zero) =>= d (s (s (d (d (s zero))))) [] by Demod 35815 with 14 at 3
% 106.92/27.12 Id : 35821, {_}: minus (s (d (d (s (d (s zero)))))) (s zero) =>= d (d (s (d (s zero)))) [] by Demod 35820 with 14 at 1,3
% 106.92/27.12 Id : 47381, {_}: quot (s (s (d (d (s (d (s zero))))))) (d (s zero)) =>= s (quot (d (d (s (d (s zero))))) (d (s zero))) [] by Super 118 with 35821 at 1,1,3
% 106.92/27.12 Id : 47389, {_}: quot (d (s (d (s (d (s zero)))))) (d (s zero)) =<= s (quot (d (d (s (d (s zero))))) (d (s zero))) [] by Demod 47381 with 14 at 1,2
% 106.92/27.12 Id : 35757, {_}: quot (s (s (d (s (d (d (s zero))))))) (d (s zero)) =>= s (quot (d (s (d (d (s zero))))) (d (s zero))) [] by Super 118 with 10935 at 1,1,3
% 106.92/27.12 Id : 35762, {_}: quot (d (s (s (d (d (s zero)))))) (d (s zero)) =<= s (quot (d (s (d (d (s zero))))) (d (s zero))) [] by Demod 35757 with 14 at 1,2
% 106.92/27.12 Id : 10011, {_}: quot (s (s (d (d (d (s zero)))))) (s (s zero)) =>= s (quot (d (d (d (s zero)))) (s (s zero))) [] by Super 10 with 10005 at 1,1,3
% 106.92/27.12 Id : 10017, {_}: quot (d (s (d (d (s zero))))) (s (s zero)) =<= s (quot (d (d (d (s zero)))) (s (s zero))) [] by Demod 10011 with 14 at 1,2
% 106.92/27.12 Id : 10018, {_}: quot (d (s (d (d (s zero))))) (d (s zero)) =<= s (quot (d (d (d (s zero)))) (s (s zero))) [] by Demod 10017 with 86 at 2,2
% 106.92/27.12 Id : 10019, {_}: quot (d (s (d (d (s zero))))) (d (s zero)) =<= s (quot (d (d (d (s zero)))) (d (s zero))) [] by Demod 10018 with 86 at 2,1,3
% 106.92/27.12 Id : 9250, {_}: quot (s (s (d (s (d (s zero)))))) (s (s zero)) =>= s (quot (d (s (d (s zero)))) (s (s zero))) [] by Super 10 with 3287 at 1,1,3
% 106.92/27.12 Id : 9264, {_}: quot (d (s (s (d (s zero))))) (s (s zero)) =<= s (quot (d (s (d (s zero)))) (s (s zero))) [] by Demod 9250 with 14 at 1,2
% 106.92/27.12 Id : 9265, {_}: quot (d (s (s (d (s zero))))) (d (s zero)) =<= s (quot (d (s (d (s zero)))) (s (s zero))) [] by Demod 9264 with 86 at 2,2
% 106.92/27.12 Id : 9266, {_}: quot (d (s (s (d (s zero))))) (d (s zero)) =<= s (quot (d (s (d (s zero)))) (d (s zero))) [] by Demod 9265 with 86 at 2,1,3
% 106.92/27.12 Id : 9267, {_}: quot (d (d (s (s zero)))) (d (s zero)) =<= s (quot (d (s (d (s zero)))) (d (s zero))) [] by Demod 9266 with 14 at 1,1,2
% 106.92/27.12 Id : 2723, {_}: quot (s (s (d (d (s zero))))) (s (s zero)) =>= s (quot (d (d (s zero))) (s (s zero))) [] by Super 10 with 1609 at 1,1,3
% 106.92/27.12 Id : 2728, {_}: quot (d (s (d (s zero)))) (s (s zero)) =<= s (quot (d (d (s zero))) (s (s zero))) [] by Demod 2723 with 14 at 1,2
% 106.92/27.12 Id : 2729, {_}: quot (d (s (d (s zero)))) (d (s zero)) =<= s (quot (d (d (s zero))) (s (s zero))) [] by Demod 2728 with 86 at 2,2
% 106.92/27.12 Id : 2730, {_}: quot (d (s (d (s zero)))) (d (s zero)) =<= s (quot (d (d (s zero))) (d (s zero))) [] by Demod 2729 with 86 at 2,1,3
% 106.92/27.12 Id : 1096, {_}: quot (s (s (d (s zero)))) (s (s zero)) =>= s (quot (d (s zero)) (s (s zero))) [] by Super 10 with 1091 at 1,1,3
% 106.92/27.12 Id : 1099, {_}: quot (d (s (s zero))) (s (s zero)) =<= s (quot (d (s zero)) (s (s zero))) [] by Demod 1096 with 14 at 1,2
% 106.92/27.12 Id : 1100, {_}: quot (d (s (s zero))) (d (s zero)) =<= s (quot (d (s zero)) (s (s zero))) [] by Demod 1099 with 86 at 2,2
% 106.92/27.12 Id : 1101, {_}: quot (d (s (s zero))) (d (s zero)) =<= s (quot (d (s zero)) (d (s zero))) [] by Demod 1100 with 86 at 2,1,3
% 106.92/27.12 Id : 1102, {_}: quot (d (d (s zero))) (d (s zero)) =<= s (quot (d (s zero)) (d (s zero))) [] by Demod 1101 with 86 at 1,1,2
% 106.92/27.12 Id : 378, {_}: quot (s (s zero)) (s (s ?510)) =>= s (quot zero (s (s ?510))) [510] by Super 10 with 216 at 1,1,3
% 106.92/27.12 Id : 387, {_}: quot (d (s zero)) (s (s ?510)) =>= s (quot zero (s (s ?510))) [510] by Demod 378 with 86 at 1,2
% 106.92/27.12 Id : 1892, {_}: quot (d (s zero)) (s (s ?2407)) =>= s zero [2407] by Demod 387 with 9 at 1,3
% 106.92/27.12 Id : 1905, {_}: quot (d (s zero)) (d (s zero)) =>= s zero [] by Super 1892 with 86 at 2,2
% 106.92/27.12 Id : 2452, {_}: quot (d (d (s zero))) (d (s zero)) =>= s (s zero) [] by Demod 1102 with 1905 at 1,3
% 106.92/27.12 Id : 2453, {_}: quot (d (d (s zero))) (d (s zero)) =>= d (s zero) [] by Demod 2452 with 86 at 3
% 106.92/27.12 Id : 2731, {_}: quot (d (s (d (s zero)))) (d (s zero)) =>= s (d (s zero)) [] by Demod 2730 with 2453 at 1,3
% 106.92/27.12 Id : 9268, {_}: quot (d (d (s (s zero)))) (d (s zero)) =>= s (s (d (s zero))) [] by Demod 9267 with 2731 at 1,3
% 106.92/27.12 Id : 9269, {_}: quot (d (d (d (s zero)))) (d (s zero)) =>= s (s (d (s zero))) [] by Demod 9268 with 86 at 1,1,1,2
% 106.92/27.12 Id : 9270, {_}: quot (d (d (d (s zero)))) (d (s zero)) =>= d (s (s zero)) [] by Demod 9269 with 14 at 3
% 106.92/27.12 Id : 9271, {_}: quot (d (d (d (s zero)))) (d (s zero)) =>= d (d (s zero)) [] by Demod 9270 with 86 at 1,3
% 106.92/27.12 Id : 34619, {_}: quot (d (s (d (d (s zero))))) (d (s zero)) =>= s (d (d (s zero))) [] by Demod 10019 with 9271 at 1,3
% 106.92/27.12 Id : 35763, {_}: quot (d (s (s (d (d (s zero)))))) (d (s zero)) =>= s (s (d (d (s zero)))) [] by Demod 35762 with 34619 at 1,3
% 106.92/27.12 Id : 35764, {_}: quot (d (d (s (d (s zero))))) (d (s zero)) =>= s (s (d (d (s zero)))) [] by Demod 35763 with 14 at 1,1,2
% 106.92/27.12 Id : 35765, {_}: quot (d (d (s (d (s zero))))) (d (s zero)) =>= d (s (d (s zero))) [] by Demod 35764 with 14 at 3
% 106.92/27.12 Id : 47390, {_}: quot (d (s (d (s (d (s zero)))))) (d (s zero)) =>= s (d (s (d (s zero)))) [] by Demod 47389 with 35765 at 1,3
% 106.92/27.12 Id : 225610, {_}: log (s (s (d (s (d (s (d (s zero)))))))) =>= s (log (s (s (d (s (d (s zero))))))) [] by Super 101 with 47390 at 1,1,1,3
% 106.92/27.12 Id : 225681, {_}: log (d (s (s (d (s (d (s zero))))))) =>= s (log (s (s (d (s (d (s zero))))))) [] by Demod 225610 with 14 at 1,2
% 106.92/27.12 Id : 225682, {_}: log (d (s (s (d (s (d (s zero))))))) =>= s (log (d (s (s (d (s zero)))))) [] by Demod 225681 with 14 at 1,1,3
% 106.92/27.12 Id : 225683, {_}: log (d (d (s (s (d (s zero)))))) =>= s (log (d (s (s (d (s zero)))))) [] by Demod 225682 with 14 at 1,1,2
% 106.92/27.12 Id : 225684, {_}: log (d (d (s (s (d (s zero)))))) =>= s (log (d (d (s (s zero))))) [] by Demod 225683 with 14 at 1,1,1,3
% 106.92/27.12 Id : 225685, {_}: log (d (d (d (s (s zero))))) =>= s (log (d (d (s (s zero))))) [] by Demod 225684 with 14 at 1,1,1,2
% 106.92/27.12 Id : 225686, {_}: log (d (d (d (s (s zero))))) =>= s (log (d (d (d (s zero))))) [] by Demod 225685 with 86 at 1,1,1,1,3
% 106.92/27.12 Id : 225687, {_}: log (d (d (d (d (s zero))))) =>= s (log (d (d (d (s zero))))) [] by Demod 225686 with 86 at 1,1,1,1,2
% 106.92/27.12 Id : 9091, {_}: log (s (s (d (s (d (s zero)))))) =>= s (log (s (s (d (s zero))))) [] by Super 101 with 2731 at 1,1,1,3
% 106.92/27.12 Id : 9101, {_}: log (d (s (s (d (s zero))))) =>= s (log (s (s (d (s zero))))) [] by Demod 9091 with 14 at 1,2
% 106.92/27.12 Id : 9102, {_}: log (d (s (s (d (s zero))))) =>= s (log (d (s (s zero)))) [] by Demod 9101 with 14 at 1,1,3
% 106.92/27.12 Id : 9103, {_}: log (d (d (s (s zero)))) =>= s (log (d (s (s zero)))) [] by Demod 9102 with 14 at 1,1,2
% 106.92/27.12 Id : 9104, {_}: log (d (d (s (s zero)))) =>= s (log (d (d (s zero)))) [] by Demod 9103 with 86 at 1,1,1,3
% 106.92/27.12 Id : 9105, {_}: log (d (d (d (s zero)))) =>= s (log (d (d (s zero)))) [] by Demod 9104 with 86 at 1,1,1,2
% 106.92/27.12 Id : 1915, {_}: log (s (s (d (s zero)))) =>= s (log (s (s zero))) [] by Super 101 with 1905 at 1,1,1,3
% 106.92/27.12 Id : 1918, {_}: log (d (s (s zero))) =>= s (log (s (s zero))) [] by Demod 1915 with 14 at 1,2
% 106.92/27.12 Id : 1919, {_}: log (d (s (s zero))) =>= s (log (d (s zero))) [] by Demod 1918 with 86 at 1,1,3
% 106.92/27.12 Id : 1920, {_}: log (d (d (s zero))) =>= s (log (d (s zero))) [] by Demod 1919 with 86 at 1,1,2
% 106.92/27.12 Id : 65, {_}: log (s (s zero)) =>= s (log (s zero)) [] by Super 64 with 9 at 1,1,1,3
% 106.92/27.12 Id : 73, {_}: log (s (s zero)) =>= s zero [] by Demod 65 with 11 at 1,3
% 106.92/27.12 Id : 126, {_}: log (d (s zero)) =>= s zero [] by Demod 73 with 86 at 1,2
% 106.92/27.12 Id : 1921, {_}: log (d (d (s zero))) =>= s (s zero) [] by Demod 1920 with 126 at 1,3
% 106.92/27.12 Id : 1922, {_}: log (d (d (s zero))) =>= d (s zero) [] by Demod 1921 with 86 at 3
% 106.92/27.12 Id : 9106, {_}: log (d (d (d (s zero)))) =>= s (d (s zero)) [] by Demod 9105 with 1922 at 1,3
% 106.92/27.12 Id : 225688, {_}: log (d (d (d (d (s zero))))) =>= s (s (d (s zero))) [] by Demod 225687 with 9106 at 1,3
% 106.92/27.12 Id : 98, {_}: e (d (s ?191)) =<= d (e (s (d ?191))) [191] by Super 95 with 14 at 1,2
% 106.92/27.12 Id : 261, {_}: e (d (s ?355)) =<= d (d (e (d ?355))) [355] by Demod 98 with 16 at 1,3
% 106.92/27.12 Id : 102, {_}: e (d (s zero)) =>= d (e (s zero)) [] by Super 16 with 86 at 1,2
% 106.92/27.12 Id : 119, {_}: e (d (s zero)) =>= d (d (e zero)) [] by Demod 102 with 16 at 1,3
% 106.92/27.12 Id : 120, {_}: e (d (s zero)) =>= d (d (s zero)) [] by Demod 119 with 15 at 1,1,3
% 106.92/27.12 Id : 264, {_}: e (d (s (s zero))) =<= d (d (d (d (s zero)))) [] by Super 261 with 120 at 1,1,3
% 106.92/27.12 Id : 268, {_}: e (d (d (s zero))) =<= d (d (d (d (s zero)))) [] by Demod 264 with 86 at 1,1,2
% 106.92/27.12 Id : 225689, {_}: log (e (d (d (s zero)))) =>= s (s (d (s zero))) [] by Demod 225688 with 268 at 1,2
% 106.92/27.12 Id : 225690, {_}: log (e (d (d (s zero)))) =>= d (s (s zero)) [] by Demod 225689 with 14 at 3
% 106.92/27.12 Id : 225691, {_}: log (e (d (d (s zero)))) =>= d (d (s zero)) [] by Demod 225690 with 86 at 1,3
% 106.92/27.12 Id : 225826, {_}: d (d (s zero)) === d (d (s zero)) [] by Super 225825 with 225691 at 2
% 106.92/27.12 Id : 225825, {_}: log (e ?1) =?= d (d (s zero)) [1] by Demod 225824 with 86 at 1,3
% 106.92/27.12 Id : 225824, {_}: log (e ?1) =?= d (s (s zero)) [1] by Demod 225823 with 14 at 3
% 106.92/27.12 Id : 225823, {_}: log (e ?1) =?= s (s (d (s zero))) [1] by Demod 1 with 86 at 1,1,3
% 106.92/27.12 Id : 1, {_}: log (e ?1) =?= s (s (s (s zero))) [1] by goal ?1
% 106.92/27.12 % SZS output end CNFRefutation for theBenchmark.p
% 106.92/27.12 14293: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 26.780581 using nrkbo
%------------------------------------------------------------------------------