%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYO631-1 : TPTP v9.3.1. Released v7.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:42:51 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.43s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 26
% Syntax : Number of formulae : 157 ( 24 unt; 0 def)
% Number of atoms : 436 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 595 ( 316 ~; 279 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 6 avg)
% Maximal term depth : 11 ( 3 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 1 con; 0-1 aty)
% Number of variables : 414 ( 414 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [E,A_5] :
( 'E'(f(A_5),f(g(A_5)))
| ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(g(A_5)))
| ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(A_5)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A_23] : iLEQ(A_23,g(A_23)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [LE,A_19,B_12,E] :
( 'LE'(f(B_12),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(B_12))
| ~ iLEQ(A_19,B_12)
| ~ 'LE'(f(A_19),s(s(s(s('0'))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [LE,A_1,B_0,E] :
( 'LE'(f(B_0),s(s(s(s(s(s(s(s(s('0'))))))))))
| 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(B_0))
| ~ iLEQ(A_1,B_0)
| ~ 'LE'(f(A_1),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [E,A_26] : ~ 'E'(f(A_26),f(g(A_26))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A_14] : iLEQ(A_14,A_14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [E,A_11] :
( 'E'(f(A_11),f(g(A_11)))
| ~ 'E'(s(s(s(s(s(s(s('0'))))))),f(g(A_11)))
| ~ 'E'(s(s(s(s(s(s(s('0'))))))),f(A_11)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [LE,A_13,B_8,E] :
( 'LE'(f(B_8),s(s(s(s(s('0'))))))
| 'E'(s(s(s(s(s('0'))))),f(B_8))
| ~ iLEQ(A_13,B_8)
| ~ 'LE'(f(A_13),s(s(s(s(s(s('0'))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [E,A_23] :
( 'E'(f(A_23),f(g(A_23)))
| ~ 'E'(s(s(s('0'))),f(g(A_23)))
| ~ 'E'(s(s(s('0'))),f(A_23)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [LE,A_4,B_2,E] :
( 'LE'(f(B_2),s(s(s(s(s(s(s(s('0')))))))))
| 'E'(s(s(s(s(s(s(s(s('0')))))))),f(B_2))
| ~ iLEQ(A_4,B_2)
| ~ 'LE'(f(A_4),s(s(s(s(s(s(s(s(s('0')))))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [E,A_14] :
( 'E'(f(A_14),f(g(A_14)))
| ~ 'E'(s(s(s(s(s(s('0')))))),f(g(A_14)))
| ~ 'E'(s(s(s(s(s(s('0')))))),f(A_14)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [LE,A_7,B_4,E] :
( 'LE'(f(B_4),s(s(s(s(s(s(s('0'))))))))
| 'E'(s(s(s(s(s(s(s('0'))))))),f(B_4))
| ~ iLEQ(A_7,B_4)
| ~ 'LE'(f(A_7),s(s(s(s(s(s(s(s('0'))))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [LE,A_25,B_16,E] :
( 'LE'(f(B_16),s('0'))
| 'E'(s('0'),f(B_16))
| ~ iLEQ(A_25,B_16)
| ~ 'LE'(f(A_25),s(s('0'))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [E,A_26] :
( 'E'(f(A_26),f(g(A_26)))
| ~ 'E'(s(s('0')),f(g(A_26)))
| ~ 'E'(s(s('0')),f(A_26)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [E,A_17] :
( 'E'(f(A_17),f(g(A_17)))
| ~ 'E'(s(s(s(s(s('0'))))),f(g(A_17)))
| ~ 'E'(s(s(s(s(s('0'))))),f(A_17)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [E,A_30] :
( 'E'(f(A_30),f(g(A_30)))
| ~ 'E'('0',f(g(A_30)))
| ~ 'E'('0',f(A_30)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [LE,A_28,B_18,E] :
( 'LE'(f(B_18),'0')
| 'E'('0',f(B_18))
| ~ iLEQ(A_28,B_18)
| ~ 'LE'(f(A_28),s('0')) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [E,A_2] :
( 'E'(f(A_2),f(g(A_2)))
| ~ 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(g(A_2)))
| ~ 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(A_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [E,A_29] :
( 'E'(f(A_29),f(g(A_29)))
| ~ 'E'(s('0'),f(g(A_29)))
| ~ 'E'(s('0'),f(A_29)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [LE,A_16,B_10,E] :
( 'LE'(f(B_10),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(B_10))
| ~ iLEQ(A_16,B_10)
| ~ 'LE'(f(A_16),s(s(s(s(s('0')))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [E,A,LE] :
( 'LE'(f(A),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [LE,A_10,B_6,E] :
( 'LE'(f(B_6),s(s(s(s(s(s('0')))))))
| 'E'(s(s(s(s(s(s('0')))))),f(B_6))
| ~ iLEQ(A_10,B_6)
| ~ 'LE'(f(A_10),s(s(s(s(s(s(s('0')))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [E,A_20] :
( 'E'(f(A_20),f(g(A_20)))
| ~ 'E'(s(s(s(s('0')))),f(g(A_20)))
| ~ 'E'(s(s(s(s('0')))),f(A_20)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [LE,A_22,B_14,E] :
( 'LE'(f(B_14),s(s('0')))
| 'E'(s(s('0')),f(B_14))
| ~ iLEQ(A_22,B_14)
| ~ 'LE'(f(A_22),s(s(s('0')))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [LE,A_30] : ~ 'LE'(f(A_30),'0'),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [E,A_8] :
( 'E'(f(A_8),f(g(A_8)))
| ~ 'E'(s(s(s(s(s(s(s(s('0')))))))),f(g(A_8)))
| ~ 'E'(s(s(s(s(s(s(s(s('0')))))))),f(A_8)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,plain,
! [A_5] :
( 'E'(f(A_5),f(g(A_5)))
| ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(g(A_5)))
| ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(A_5)) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f59,plain,
! [E,X0] :
( 'E'(f(X0),f(g(X0)))
| ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(g(X0)))
| ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(X0)) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
! [X0] : iLEQ(X0,g(X0)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f61,plain,
! [B_12] :
( 'LE'(f(B_12),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(B_12))
| ! [A_19] :
( ~ iLEQ(A_19,B_12)
| ~ 'LE'(f(A_19),s(s(s(s('0'))))) ) ),
inference(miniscoping,[status(thm)],[f3]) ).
fof(f62,plain,
! [LE,X0,X1,E] :
( 'LE'(f(X1),s(s(s('0'))))
| 'E'(s(s(s('0'))),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s(s('0'))))) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
! [B_0] :
( 'LE'(f(B_0),s(s(s(s(s(s(s(s(s('0'))))))))))
| 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(B_0))
| ! [A_1] :
( ~ iLEQ(A_1,B_0)
| ~ 'LE'(f(A_1),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ) ),
inference(miniscoping,[status(thm)],[f4]) ).
fof(f64,plain,
! [LE,X0,X1,E] :
( 'LE'(f(X1),s(s(s(s(s(s(s(s(s('0'))))))))))
| 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f65,plain,
! [A_26] : ~ 'E'(f(A_26),f(g(A_26))),
inference(miniscoping,[status(thm)],[f5]) ).
fof(f66,plain,
! [E,X0] : ~ 'E'(f(X0),f(g(X0))),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f67,plain,
! [X0] : iLEQ(X0,X0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f68,plain,
! [A_11] :
( 'E'(f(A_11),f(g(A_11)))
| ~ 'E'(s(s(s(s(s(s(s('0'))))))),f(g(A_11)))
| ~ 'E'(s(s(s(s(s(s(s('0'))))))),f(A_11)) ),
inference(miniscoping,[status(thm)],[f7]) ).
fof(f69,plain,
! [E,X0] :
( 'E'(f(X0),f(g(X0)))
| ~ 'E'(s(s(s(s(s(s(s('0'))))))),f(g(X0)))
| ~ 'E'(s(s(s(s(s(s(s('0'))))))),f(X0)) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f74,plain,
! [B_8] :
( 'LE'(f(B_8),s(s(s(s(s('0'))))))
| 'E'(s(s(s(s(s('0'))))),f(B_8))
| ! [A_13] :
( ~ iLEQ(A_13,B_8)
| ~ 'LE'(f(A_13),s(s(s(s(s(s('0'))))))) ) ),
inference(miniscoping,[status(thm)],[f11]) ).
fof(f75,plain,
! [LE,X0,X1,E] :
( 'LE'(f(X1),s(s(s(s(s('0'))))))
| 'E'(s(s(s(s(s('0'))))),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s(s(s(s('0'))))))) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f76,plain,
! [A_23] :
( 'E'(f(A_23),f(g(A_23)))
| ~ 'E'(s(s(s('0'))),f(g(A_23)))
| ~ 'E'(s(s(s('0'))),f(A_23)) ),
inference(miniscoping,[status(thm)],[f12]) ).
fof(f77,plain,
! [E,X0] :
( 'E'(f(X0),f(g(X0)))
| ~ 'E'(s(s(s('0'))),f(g(X0)))
| ~ 'E'(s(s(s('0'))),f(X0)) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f78,plain,
! [B_2] :
( 'LE'(f(B_2),s(s(s(s(s(s(s(s('0')))))))))
| 'E'(s(s(s(s(s(s(s(s('0')))))))),f(B_2))
| ! [A_4] :
( ~ iLEQ(A_4,B_2)
| ~ 'LE'(f(A_4),s(s(s(s(s(s(s(s(s('0')))))))))) ) ),
inference(miniscoping,[status(thm)],[f13]) ).
fof(f79,plain,
! [LE,X0,X1,E] :
( 'LE'(f(X1),s(s(s(s(s(s(s(s('0')))))))))
| 'E'(s(s(s(s(s(s(s(s('0')))))))),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s(s(s(s(s(s(s('0')))))))))) ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f83,plain,
! [A_14] :
( 'E'(f(A_14),f(g(A_14)))
| ~ 'E'(s(s(s(s(s(s('0')))))),f(g(A_14)))
| ~ 'E'(s(s(s(s(s(s('0')))))),f(A_14)) ),
inference(miniscoping,[status(thm)],[f16]) ).
fof(f84,plain,
! [E,X0] :
( 'E'(f(X0),f(g(X0)))
| ~ 'E'(s(s(s(s(s(s('0')))))),f(g(X0)))
| ~ 'E'(s(s(s(s(s(s('0')))))),f(X0)) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f87,plain,
! [B_4] :
( 'LE'(f(B_4),s(s(s(s(s(s(s('0'))))))))
| 'E'(s(s(s(s(s(s(s('0'))))))),f(B_4))
| ! [A_7] :
( ~ iLEQ(A_7,B_4)
| ~ 'LE'(f(A_7),s(s(s(s(s(s(s(s('0'))))))))) ) ),
inference(miniscoping,[status(thm)],[f19]) ).
fof(f88,plain,
! [LE,X0,X1,E] :
( 'LE'(f(X1),s(s(s(s(s(s(s('0'))))))))
| 'E'(s(s(s(s(s(s(s('0'))))))),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f90,plain,
! [B_16] :
( 'LE'(f(B_16),s('0'))
| 'E'(s('0'),f(B_16))
| ! [A_25] :
( ~ iLEQ(A_25,B_16)
| ~ 'LE'(f(A_25),s(s('0'))) ) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f91,plain,
! [LE,X0,X1,E] :
( 'LE'(f(X1),s('0'))
| 'E'(s('0'),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s('0'))) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f92,plain,
! [A_26] :
( 'E'(f(A_26),f(g(A_26)))
| ~ 'E'(s(s('0')),f(g(A_26)))
| ~ 'E'(s(s('0')),f(A_26)) ),
inference(miniscoping,[status(thm)],[f22]) ).
fof(f93,plain,
! [E,X0] :
( 'E'(f(X0),f(g(X0)))
| ~ 'E'(s(s('0')),f(g(X0)))
| ~ 'E'(s(s('0')),f(X0)) ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f94,plain,
! [A_17] :
( 'E'(f(A_17),f(g(A_17)))
| ~ 'E'(s(s(s(s(s('0'))))),f(g(A_17)))
| ~ 'E'(s(s(s(s(s('0'))))),f(A_17)) ),
inference(miniscoping,[status(thm)],[f23]) ).
fof(f95,plain,
! [E,X0] :
( 'E'(f(X0),f(g(X0)))
| ~ 'E'(s(s(s(s(s('0'))))),f(g(X0)))
| ~ 'E'(s(s(s(s(s('0'))))),f(X0)) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f98,plain,
! [A_30] :
( 'E'(f(A_30),f(g(A_30)))
| ~ 'E'('0',f(g(A_30)))
| ~ 'E'('0',f(A_30)) ),
inference(miniscoping,[status(thm)],[f25]) ).
fof(f99,plain,
! [E,X0] :
( 'E'(f(X0),f(g(X0)))
| ~ 'E'('0',f(g(X0)))
| ~ 'E'('0',f(X0)) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f107,plain,
! [B_18] :
( 'LE'(f(B_18),'0')
| 'E'('0',f(B_18))
| ! [A_28] :
( ~ iLEQ(A_28,B_18)
| ~ 'LE'(f(A_28),s('0')) ) ),
inference(miniscoping,[status(thm)],[f31]) ).
fof(f108,plain,
! [LE,X0,X1,E] :
( 'LE'(f(X1),'0')
| 'E'('0',f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s('0')) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f109,plain,
! [A_2] :
( 'E'(f(A_2),f(g(A_2)))
| ~ 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(g(A_2)))
| ~ 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(A_2)) ),
inference(miniscoping,[status(thm)],[f32]) ).
fof(f110,plain,
! [E,X0] :
( 'E'(f(X0),f(g(X0)))
| ~ 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(g(X0)))
| ~ 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(X0)) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f113,plain,
! [A_29] :
( 'E'(f(A_29),f(g(A_29)))
| ~ 'E'(s('0'),f(g(A_29)))
| ~ 'E'(s('0'),f(A_29)) ),
inference(miniscoping,[status(thm)],[f35]) ).
fof(f114,plain,
! [E,X0] :
( 'E'(f(X0),f(g(X0)))
| ~ 'E'(s('0'),f(g(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
! [B_10] :
( 'LE'(f(B_10),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(B_10))
| ! [A_16] :
( ~ iLEQ(A_16,B_10)
| ~ 'LE'(f(A_16),s(s(s(s(s('0')))))) ) ),
inference(miniscoping,[status(thm)],[f36]) ).
fof(f116,plain,
! [LE,X0,X1,E] :
( 'LE'(f(X1),s(s(s(s('0')))))
| 'E'(s(s(s(s('0')))),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s(s(s('0')))))) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f120,plain,
! [A] :
( 'LE'(f(A),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(A)) ),
inference(miniscoping,[status(thm)],[f39]) ).
fof(f121,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(X0)) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f128,plain,
! [B_6] :
( 'LE'(f(B_6),s(s(s(s(s(s('0')))))))
| 'E'(s(s(s(s(s(s('0')))))),f(B_6))
| ! [A_10] :
( ~ iLEQ(A_10,B_6)
| ~ 'LE'(f(A_10),s(s(s(s(s(s(s('0')))))))) ) ),
inference(miniscoping,[status(thm)],[f45]) ).
fof(f129,plain,
! [LE,X0,X1,E] :
( 'LE'(f(X1),s(s(s(s(s(s('0')))))))
| 'E'(s(s(s(s(s(s('0')))))),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s(s(s(s(s('0')))))))) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f132,plain,
! [A_20] :
( 'E'(f(A_20),f(g(A_20)))
| ~ 'E'(s(s(s(s('0')))),f(g(A_20)))
| ~ 'E'(s(s(s(s('0')))),f(A_20)) ),
inference(miniscoping,[status(thm)],[f48]) ).
fof(f133,plain,
! [E,X0] :
( 'E'(f(X0),f(g(X0)))
| ~ 'E'(s(s(s(s('0')))),f(g(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X0)) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f136,plain,
! [B_14] :
( 'LE'(f(B_14),s(s('0')))
| 'E'(s(s('0')),f(B_14))
| ! [A_22] :
( ~ iLEQ(A_22,B_14)
| ~ 'LE'(f(A_22),s(s(s('0')))) ) ),
inference(miniscoping,[status(thm)],[f50]) ).
fof(f137,plain,
! [LE,X0,X1,E] :
( 'LE'(f(X1),s(s('0')))
| 'E'(s(s('0')),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s('0')))) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f140,plain,
! [A_30] : ~ 'LE'(f(A_30),'0'),
inference(miniscoping,[status(thm)],[f52]) ).
fof(f141,plain,
! [LE,X0] : ~ 'LE'(f(X0),'0'),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f144,plain,
! [A_8] :
( 'E'(f(A_8),f(g(A_8)))
| ~ 'E'(s(s(s(s(s(s(s(s('0')))))))),f(g(A_8)))
| ~ 'E'(s(s(s(s(s(s(s(s('0')))))))),f(A_8)) ),
inference(miniscoping,[status(thm)],[f54]) ).
fof(f145,plain,
! [E,X0] :
( 'E'(f(X0),f(g(X0)))
| ~ 'E'(s(s(s(s(s(s(s(s('0')))))))),f(g(X0)))
| ~ 'E'(s(s(s(s(s(s(s(s('0')))))))),f(X0)) ),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f150,plain,
! [E,X0] :
( ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(g(X0)))
| ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f59,f66]) ).
fof(f151,plain,
! [E,X0] :
( ~ 'E'(s(s(s(s(s(s(s('0'))))))),f(g(X0)))
| ~ 'E'(s(s(s(s(s(s(s('0'))))))),f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f69,f66]) ).
fof(f152,plain,
! [E,X0] :
( ~ 'E'(s(s(s('0'))),f(g(X0)))
| ~ 'E'(s(s(s('0'))),f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f77,f66]) ).
fof(f154,plain,
! [E,X0] :
( ~ 'E'('0',f(g(X0)))
| ~ 'E'('0',f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f99,f66]) ).
fof(f155,plain,
! [LE,X0,X1,E] :
( 'E'('0',f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s('0')) ),
inference(forward_subsumption_resolution,[status(thm)],[f108,f141]) ).
fof(f156,plain,
! [LE,X0,X1,E] :
( ~ 'E'('0',f(X1))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s('0')) ),
inference(resolution,[status(thm)],[f155,f154]) ).
fof(f159,plain,
! [LE,X0,X1,X2] :
( ~ iLEQ(X2,X1)
| ~ 'LE'(f(X2),s('0'))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s('0')) ),
inference(resolution,[status(thm)],[f156,f155]) ).
fof(f164,plain,
! [LE,X0,X1] :
( ~ iLEQ(X0,X1)
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s('0')) ),
inference(factoring,[status(thm)],[f159]) ).
fof(f165,plain,
! [LE,X0] :
( ~ iLEQ(X0,X0)
| ~ 'LE'(f(X0),s('0')) ),
inference(resolution,[status(thm)],[f164,f60]) ).
fof(f167,plain,
! [LE,X0] : ~ 'LE'(f(X0),s('0')),
inference(forward_subsumption_resolution,[status(thm)],[f165,f67]) ).
fof(f168,plain,
! [E,X0] :
( ~ 'E'(s(s(s(s(s(s('0')))))),f(g(X0)))
| ~ 'E'(s(s(s(s(s(s('0')))))),f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f84,f66]) ).
fof(f169,plain,
! [LE,X0,X1,E] :
( ~ 'E'(s(s(s(s(s(s(s('0'))))))),f(X1))
| 'LE'(f(g(X1)),s(s(s(s(s(s(s('0'))))))))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(resolution,[status(thm)],[f88,f151]) ).
fof(f170,plain,
! [E,X0] :
( ~ 'E'(s('0'),f(g(X0)))
| ~ 'E'(s('0'),f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f114,f66]) ).
fof(f171,plain,
! [LE,X0,X1,E] :
( 'E'(s('0'),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s('0'))) ),
inference(forward_subsumption_resolution,[status(thm)],[f91,f167]) ).
fof(f172,plain,
! [LE,X0,X1,E] :
( ~ 'E'(s('0'),f(X1))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s('0'))) ),
inference(resolution,[status(thm)],[f171,f170]) ).
fof(f173,plain,
! [E,X0] :
( ~ 'E'(s(s('0')),f(g(X0)))
| ~ 'E'(s(s('0')),f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f93,f66]) ).
fof(f176,plain,
! [LE,X0,X1,X2] :
( ~ iLEQ(X2,X1)
| ~ 'LE'(f(X2),s(s('0')))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s('0'))) ),
inference(resolution,[status(thm)],[f172,f171]) ).
fof(f181,plain,
! [LE,X0,X1] :
( ~ iLEQ(X0,X1)
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s('0'))) ),
inference(factoring,[status(thm)],[f176]) ).
fof(f182,plain,
! [E,X0] :
( ~ 'E'(s(s(s(s(s('0'))))),f(g(X0)))
| ~ 'E'(s(s(s(s(s('0'))))),f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f95,f66]) ).
fof(f184,plain,
! [LE,X0] :
( ~ iLEQ(X0,X0)
| ~ 'LE'(f(X0),s(s('0'))) ),
inference(resolution,[status(thm)],[f181,f60]) ).
fof(f186,plain,
! [LE,X0] : ~ 'LE'(f(X0),s(s('0'))),
inference(forward_subsumption_resolution,[status(thm)],[f184,f67]) ).
fof(f187,plain,
! [E,X0] :
( ~ 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(g(X0)))
| ~ 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f110,f66]) ).
fof(f188,plain,
! [LE,X0,X1,E] :
( 'E'(s(s('0')),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s('0')))) ),
inference(forward_subsumption_resolution,[status(thm)],[f137,f186]) ).
fof(f189,plain,
! [LE,X0,X1,E] :
( ~ 'E'(s(s('0')),f(X1))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s('0')))) ),
inference(resolution,[status(thm)],[f188,f173]) ).
fof(f192,plain,
! [LE,X0,X1,X2] :
( ~ iLEQ(X2,X1)
| ~ 'LE'(f(X2),s(s(s('0'))))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s('0')))) ),
inference(resolution,[status(thm)],[f189,f188]) ).
fof(f197,plain,
! [LE,X0,X1] :
( ~ iLEQ(X0,X1)
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s('0')))) ),
inference(factoring,[status(thm)],[f192]) ).
fof(f198,plain,
! [LE,X0,E] :
( ~ 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(X0))
| 'LE'(f(g(X0)),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ),
inference(resolution,[status(thm)],[f121,f187]) ).
fof(f199,plain,
! [LE,X0] :
( ~ iLEQ(X0,X0)
| ~ 'LE'(f(X0),s(s(s('0')))) ),
inference(resolution,[status(thm)],[f197,f60]) ).
fof(f201,plain,
! [LE,X0] : ~ 'LE'(f(X0),s(s(s('0')))),
inference(forward_subsumption_resolution,[status(thm)],[f199,f67]) ).
fof(f202,plain,
! [LE,X0,X1,E] :
( 'E'(s(s(s('0'))),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s(s('0'))))) ),
inference(backward_subsumption_resolution,[status(thm)],[f62,f201]) ).
fof(f204,plain,
! [LE,X0,X1,E] :
( ~ 'E'(s(s(s('0'))),f(X1))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[f202,f152]) ).
fof(f205,plain,
! [E,X0] :
( ~ 'E'(s(s(s(s('0')))),f(g(X0)))
| ~ 'E'(s(s(s(s('0')))),f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f133,f66]) ).
fof(f209,plain,
! [LE,X0,X1,X2] :
( ~ iLEQ(X2,X1)
| ~ 'LE'(f(X2),s(s(s(s('0')))))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[f204,f202]) ).
fof(f214,plain,
! [LE,X0,X1] :
( ~ iLEQ(X0,X1)
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s('0'))))) ),
inference(factoring,[status(thm)],[f209]) ).
fof(f215,plain,
! [E,X0] :
( ~ 'E'(s(s(s(s(s(s(s(s('0')))))))),f(g(X0)))
| ~ 'E'(s(s(s(s(s(s(s(s('0')))))))),f(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f145,f66]) ).
fof(f216,plain,
! [E,X0,LE,X1] :
( 'LE'(f(g(X0)),s(s(s(s(s(s(s(s('0')))))))))
| ~ iLEQ(X1,g(X0))
| ~ 'LE'(f(X1),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(s(s(s(s(s(s(s(s('0')))))))),f(X0)) ),
inference(resolution,[status(thm)],[f215,f79]) ).
fof(f217,plain,
! [LE,X0] :
( ~ iLEQ(X0,X0)
| ~ 'LE'(f(X0),s(s(s(s('0'))))) ),
inference(resolution,[status(thm)],[f214,f60]) ).
fof(f219,plain,
! [LE,X0] : ~ 'LE'(f(X0),s(s(s(s('0'))))),
inference(forward_subsumption_resolution,[status(thm)],[f217,f67]) ).
fof(f220,plain,
! [LE,X0,X1,E] :
( 'E'(s(s(s(s('0')))),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s(s(s('0')))))) ),
inference(backward_subsumption_resolution,[status(thm)],[f116,f219]) ).
fof(f221,plain,
! [E,X0,LE,X1] :
( 'LE'(f(g(X0)),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ iLEQ(X1,g(X0))
| ~ 'LE'(f(X1),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(X0)) ),
inference(resolution,[status(thm)],[f150,f64]) ).
fof(f222,plain,
! [LE,X0,X1,E] :
( ~ 'E'(s(s(s(s('0')))),f(X1))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s(s('0')))))) ),
inference(resolution,[status(thm)],[f220,f205]) ).
fof(f225,plain,
! [LE,X0,X1,X2] :
( ~ iLEQ(X2,X1)
| ~ 'LE'(f(X2),s(s(s(s(s('0'))))))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s(s('0')))))) ),
inference(resolution,[status(thm)],[f222,f220]) ).
fof(f230,plain,
! [LE,X0,X1] :
( ~ iLEQ(X0,X1)
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s(s('0')))))) ),
inference(factoring,[status(thm)],[f225]) ).
fof(f231,plain,
! [LE,X0] :
( ~ iLEQ(X0,X0)
| ~ 'LE'(f(X0),s(s(s(s(s('0')))))) ),
inference(resolution,[status(thm)],[f230,f60]) ).
fof(f233,plain,
! [LE,X0] : ~ 'LE'(f(X0),s(s(s(s(s('0')))))),
inference(forward_subsumption_resolution,[status(thm)],[f231,f67]) ).
fof(f234,plain,
! [LE,X0,X1,E] :
( 'E'(s(s(s(s(s('0'))))),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s(s(s(s('0'))))))) ),
inference(backward_subsumption_resolution,[status(thm)],[f75,f233]) ).
fof(f235,plain,
! [LE,X0,X1,E] :
( ~ 'E'(s(s(s(s(s('0'))))),f(X1))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s(s(s('0'))))))) ),
inference(resolution,[status(thm)],[f234,f182]) ).
fof(f238,plain,
! [LE,X0,X1,X2] :
( ~ iLEQ(X2,X1)
| ~ 'LE'(f(X2),s(s(s(s(s(s('0')))))))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s(s(s('0'))))))) ),
inference(resolution,[status(thm)],[f235,f234]) ).
fof(f243,plain,
! [LE,X0,X1] :
( ~ iLEQ(X0,X1)
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s(s(s('0'))))))) ),
inference(factoring,[status(thm)],[f238]) ).
fof(f244,plain,
! [LE,X0] :
( ~ iLEQ(X0,X0)
| ~ 'LE'(f(X0),s(s(s(s(s(s('0'))))))) ),
inference(resolution,[status(thm)],[f243,f60]) ).
fof(f246,plain,
! [LE,X0] : ~ 'LE'(f(X0),s(s(s(s(s(s('0'))))))),
inference(forward_subsumption_resolution,[status(thm)],[f244,f67]) ).
fof(f247,plain,
! [LE,X0,X1,E] :
( 'E'(s(s(s(s(s(s('0')))))),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s(s(s(s(s('0')))))))) ),
inference(backward_subsumption_resolution,[status(thm)],[f129,f246]) ).
fof(f248,plain,
! [LE,X0,X1,E] :
( ~ 'E'(s(s(s(s(s(s('0')))))),f(X1))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s(s(s(s('0')))))))) ),
inference(resolution,[status(thm)],[f247,f168]) ).
fof(f252,plain,
! [LE,X0,X1,X2] :
( ~ iLEQ(X2,X1)
| ~ 'LE'(f(X2),s(s(s(s(s(s(s('0'))))))))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s(s(s(s('0')))))))) ),
inference(resolution,[status(thm)],[f248,f247]) ).
fof(f262,plain,
! [LE,X0,X1] :
( ~ iLEQ(X0,X1)
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s(s(s(s('0')))))))) ),
inference(factoring,[status(thm)],[f252]) ).
fof(f264,plain,
! [LE,X0] :
( ~ iLEQ(X0,X0)
| ~ 'LE'(f(X0),s(s(s(s(s(s(s('0')))))))) ),
inference(resolution,[status(thm)],[f262,f60]) ).
fof(f266,plain,
! [LE,X0] : ~ 'LE'(f(X0),s(s(s(s(s(s(s('0')))))))),
inference(forward_subsumption_resolution,[status(thm)],[f264,f67]) ).
fof(f267,plain,
! [LE,X0,X1,E] :
( 'E'(s(s(s(s(s(s(s('0'))))))),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(backward_subsumption_resolution,[status(thm)],[f88,f266]) ).
fof(f268,plain,
! [LE,X0,X1,E] :
( ~ 'E'(s(s(s(s(s(s(s('0'))))))),f(X1))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(backward_subsumption_resolution,[status(thm)],[f169,f266]) ).
fof(f272,plain,
! [LE,X0,X1,X2] :
( ~ iLEQ(X2,X1)
| ~ 'LE'(f(X2),s(s(s(s(s(s(s(s('0')))))))))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(resolution,[status(thm)],[f268,f267]) ).
fof(f283,plain,
! [LE,X0,X1] :
( ~ iLEQ(X0,X1)
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(factoring,[status(thm)],[f272]) ).
fof(f285,plain,
! [LE,X0] :
( ~ iLEQ(X0,X0)
| ~ 'LE'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(resolution,[status(thm)],[f283,f60]) ).
fof(f287,plain,
! [LE,X0] : ~ 'LE'(f(X0),s(s(s(s(s(s(s(s('0'))))))))),
inference(forward_subsumption_resolution,[status(thm)],[f285,f67]) ).
fof(f288,plain,
! [LE,X0,X1,E] :
( 'E'(s(s(s(s(s(s(s(s('0')))))))),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s(s(s(s(s(s(s('0')))))))))) ),
inference(backward_subsumption_resolution,[status(thm)],[f79,f287]) ).
fof(f289,plain,
! [E,X0,LE,X1] :
( ~ iLEQ(X1,g(X0))
| ~ 'LE'(f(X1),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(s(s(s(s(s(s(s(s('0')))))))),f(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f216,f287]) ).
fof(f291,plain,
! [LE,X0,X1,X2] :
( ~ iLEQ(X2,X1)
| ~ 'LE'(f(X2),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s(s(s(s(s(s('0')))))))))) ),
inference(resolution,[status(thm)],[f289,f288]) ).
fof(f304,plain,
! [LE,X0,X1] :
( ~ iLEQ(X0,X1)
| ~ iLEQ(X0,g(X1))
| ~ 'LE'(f(X0),s(s(s(s(s(s(s(s(s('0')))))))))) ),
inference(factoring,[status(thm)],[f291]) ).
fof(f306,plain,
! [LE,X0] :
( ~ iLEQ(X0,X0)
| ~ 'LE'(f(X0),s(s(s(s(s(s(s(s(s('0')))))))))) ),
inference(resolution,[status(thm)],[f304,f60]) ).
fof(f308,plain,
! [LE,X0] : ~ 'LE'(f(X0),s(s(s(s(s(s(s(s(s('0')))))))))),
inference(forward_subsumption_resolution,[status(thm)],[f306,f67]) ).
fof(f309,plain,
! [LE,X0,X1,E] :
( 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(X1))
| ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ),
inference(backward_subsumption_resolution,[status(thm)],[f64,f308]) ).
fof(f310,plain,
! [E,X0,LE,X1] :
( ~ iLEQ(X1,g(X0))
| ~ 'LE'(f(X1),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f221,f308]) ).
fof(f314,plain,
! [E,X0,LE] :
( ~ 'LE'(f(X0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(X0)) ),
inference(resolution,[status(thm)],[f310,f60]) ).
fof(f315,plain,
! [E,X0,LE] :
( ~ 'LE'(f(g(X0)),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(X0)) ),
inference(resolution,[status(thm)],[f310,f67]) ).
fof(f317,plain,
! [E,X0] :
( ~ 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(X0))
| ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(X0)) ),
inference(resolution,[status(thm)],[f315,f198]) ).
fof(f318,plain,
! [E,X0,LE] :
( 'LE'(f(X0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(X0)) ),
inference(resolution,[status(thm)],[f317,f121]) ).
fof(f319,plain,
! [E,X0] : ~ 'E'(s(s(s(s(s(s(s(s(s('0'))))))))),f(X0)),
inference(forward_subsumption_resolution,[status(thm)],[f318,f314]) ).
fof(f320,plain,
! [LE,X0,X1] :
( ~ iLEQ(X0,X1)
| ~ 'LE'(f(X0),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ),
inference(backward_subsumption_resolution,[status(thm)],[f309,f319]) ).
fof(f322,plain,
! [LE,X0] : ~ 'LE'(f(X0),s(s(s(s(s(s(s(s(s(s('0'))))))))))),
inference(resolution,[status(thm)],[f320,f60]) ).
fof(f324,plain,
! [E,X0] : 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(X0)),
inference(backward_subsumption_resolution,[status(thm)],[f121,f322]) ).
fof(f326,plain,
! [E,X0] : ~ 'E'(s(s(s(s(s(s(s(s(s(s('0')))))))))),f(g(X0))),
inference(backward_subsumption_resolution,[status(thm)],[f187,f324]) ).
fof(f327,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f326,f324]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO631-1 : TPTP v9.3.1. Released v7.1.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.33 % Computer : n017.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Mon Sep 21 12:01:11 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.34 % Drodi V4.1.1
% 0.13/0.43 % Refutation found
% 0.13/0.43 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.44 % Elapsed time: 0.101072 seconds
% 0.13/0.44 % CPU time: 0.634707 seconds
% 0.13/0.44 % Total memory used: 9.779 MB
% 0.13/0.44 % Net memory used: 9.109 MB
%------------------------------------------------------------------------------