%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SWX204-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n007.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 07:04:33 PM UTC 2026
% Result : Unsatisfiable 0.20s 0.42s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 35
% Syntax : Number of clauses : 97 ( 55 unt; 0 nHn; 66 RR)
% Number of literals : 161 ( 160 equ; 68 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-2 aty)
% Number of variables : 63 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom,axiom,
x2(z,Y) = Y ).
cnf(axiom_001,axiom,
x2(s(N),Y) = s(x2(N,Y)) ).
cnf(axiom_002,axiom,
x22(z,Y) = z ).
cnf(axiom_003,axiom,
x22(s(N),Y) = x2(Y,x22(N,Y)) ).
cnf(axiom_004,axiom,
mul_idem(X) = eq(x22(X,X),X) ).
cnf(axiom_007,axiom,
eq(s(X),s(Y)) = eq(X,Y) ).
cnf(axiom_009,axiom,
eq(s(X),z) = bfalse ).
cnf(axiom_011,axiom,
eq2(X,X) = btrue ).
cnf(goal,negated_conjecture,
eq2(mul_idem(X),bfalse) != btrue ).
cnf(refute_0_0,plain,
eq2(mul_idem(s(s(z))),bfalse) != btrue,
inference(subst,[],[goal:[bind(X,$fot(s(s(z))))]]) ).
cnf(refute_0_1,plain,
mul_idem(s(s(z))) = eq(x22(s(s(z)),s(s(z))),s(s(z))),
inference(subst,[],[axiom_004:[bind(X,$fot(s(s(z))))]]) ).
cnf(refute_0_2,plain,
x22(s(s(z)),Y) = x2(Y,x22(s(z),Y)),
inference(subst,[],[axiom_003:[bind(N,$fot(s(z)))]]) ).
cnf(refute_0_3,plain,
x22(s(z),X_11) = x2(X_11,x22(z,X_11)),
inference(subst,[],[axiom_003:[bind(N,$fot(z)),bind(Y,$fot(X_11))]]) ).
cnf(refute_0_4,plain,
x22(z,X_11) = z,
inference(subst,[],[axiom_002:[bind(Y,$fot(X_11))]]) ).
cnf(refute_0_5,plain,
( x22(s(z),X_11) != x2(X_11,x22(z,X_11))
| x22(z,X_11) != z
| x22(s(z),X_11) = x2(X_11,z) ),
introduced(tautology,[equality,[$cnf( $equal(x22(s(z),X_11),x2(X_11,x22(z,X_11))) ),[1,1],$fot(z)]]) ).
cnf(refute_0_6,plain,
( x22(s(z),X_11) != x2(X_11,x22(z,X_11))
| x22(s(z),X_11) = x2(X_11,z) ),
inference(resolve,[$cnf( $equal(x22(z,X_11),z) )],[refute_0_4,refute_0_5]) ).
cnf(refute_0_7,plain,
x22(s(z),X_11) = x2(X_11,z),
inference(resolve,[$cnf( $equal(x22(s(z),X_11),x2(X_11,x22(z,X_11))) )],[refute_0_3,refute_0_6]) ).
cnf(refute_0_8,plain,
x22(s(z),Y) = x2(Y,z),
inference(subst,[],[refute_0_7:[bind(X_11,$fot(Y))]]) ).
cnf(refute_0_9,plain,
( x22(s(s(z)),Y) != x2(Y,x22(s(z),Y))
| x22(s(z),Y) != x2(Y,z)
| x22(s(s(z)),Y) = x2(Y,x2(Y,z)) ),
introduced(tautology,[equality,[$cnf( $equal(x22(s(s(z)),Y),x2(Y,x22(s(z),Y))) ),[1,1],$fot(x2(Y,z))]]) ).
cnf(refute_0_10,plain,
( x22(s(s(z)),Y) != x2(Y,x22(s(z),Y))
| x22(s(s(z)),Y) = x2(Y,x2(Y,z)) ),
inference(resolve,[$cnf( $equal(x22(s(z),Y),x2(Y,z)) )],[refute_0_8,refute_0_9]) ).
cnf(refute_0_11,plain,
x22(s(s(z)),Y) = x2(Y,x2(Y,z)),
inference(resolve,[$cnf( $equal(x22(s(s(z)),Y),x2(Y,x22(s(z),Y))) )],[refute_0_2,refute_0_10]) ).
cnf(refute_0_12,plain,
x22(s(s(z)),s(X_15)) = x2(s(X_15),x2(s(X_15),z)),
inference(subst,[],[refute_0_11:[bind(Y,$fot(s(X_15)))]]) ).
cnf(refute_0_13,plain,
x2(s(X_15),x2(s(X_15),z)) = s(x2(X_15,x2(s(X_15),z))),
inference(subst,[],[axiom_001:[bind(N,$fot(X_15)),bind(Y,$fot(x2(s(X_15),z)))]]) ).
cnf(refute_0_14,plain,
( x2(s(X_15),x2(s(X_15),z)) != s(x2(X_15,x2(s(X_15),z)))
| x22(s(s(z)),s(X_15)) != x2(s(X_15),x2(s(X_15),z))
| x22(s(s(z)),s(X_15)) = s(x2(X_15,x2(s(X_15),z))) ),
introduced(tautology,[equality,[$cnf( $equal(x22(s(s(z)),s(X_15)),x2(s(X_15),x2(s(X_15),z))) ),[1],$fot(s(x2(X_15,x2(s(X_15),z))))]]) ).
cnf(refute_0_15,plain,
( x22(s(s(z)),s(X_15)) != x2(s(X_15),x2(s(X_15),z))
| x22(s(s(z)),s(X_15)) = s(x2(X_15,x2(s(X_15),z))) ),
inference(resolve,[$cnf( $equal(x2(s(X_15),x2(s(X_15),z)),s(x2(X_15,x2(s(X_15),z)))) )],[refute_0_13,refute_0_14]) ).
cnf(refute_0_16,plain,
x22(s(s(z)),s(X_15)) = s(x2(X_15,x2(s(X_15),z))),
inference(resolve,[$cnf( $equal(x22(s(s(z)),s(X_15)),x2(s(X_15),x2(s(X_15),z))) )],[refute_0_12,refute_0_15]) ).
cnf(refute_0_17,plain,
x2(s(X_15),z) = s(x2(X_15,z)),
inference(subst,[],[axiom_001:[bind(N,$fot(X_15)),bind(Y,$fot(z))]]) ).
cnf(refute_0_18,plain,
x2(X_15,x2(s(X_15),z)) = x2(X_15,x2(s(X_15),z)),
introduced(tautology,[refl,[$fot(x2(X_15,x2(s(X_15),z)))]]) ).
cnf(refute_0_19,plain,
( x2(X_15,x2(s(X_15),z)) != x2(X_15,x2(s(X_15),z))
| x2(s(X_15),z) != s(x2(X_15,z))
| x2(X_15,x2(s(X_15),z)) = x2(X_15,s(x2(X_15,z))) ),
introduced(tautology,[equality,[$cnf( $equal(x2(X_15,x2(s(X_15),z)),x2(X_15,x2(s(X_15),z))) ),[1,1],$fot(s(x2(X_15,z)))]]) ).
cnf(refute_0_20,plain,
( x2(s(X_15),z) != s(x2(X_15,z))
| x2(X_15,x2(s(X_15),z)) = x2(X_15,s(x2(X_15,z))) ),
inference(resolve,[$cnf( $equal(x2(X_15,x2(s(X_15),z)),x2(X_15,x2(s(X_15),z))) )],[refute_0_18,refute_0_19]) ).
cnf(refute_0_21,plain,
x2(X_15,x2(s(X_15),z)) = x2(X_15,s(x2(X_15,z))),
inference(resolve,[$cnf( $equal(x2(s(X_15),z),s(x2(X_15,z))) )],[refute_0_17,refute_0_20]) ).
cnf(refute_0_22,plain,
s(x2(X_15,x2(s(X_15),z))) = s(x2(X_15,x2(s(X_15),z))),
introduced(tautology,[refl,[$fot(s(x2(X_15,x2(s(X_15),z))))]]) ).
cnf(refute_0_23,plain,
( s(x2(X_15,x2(s(X_15),z))) != s(x2(X_15,x2(s(X_15),z)))
| x2(X_15,x2(s(X_15),z)) != x2(X_15,s(x2(X_15,z)))
| s(x2(X_15,x2(s(X_15),z))) = s(x2(X_15,s(x2(X_15,z)))) ),
introduced(tautology,[equality,[$cnf( $equal(s(x2(X_15,x2(s(X_15),z))),s(x2(X_15,x2(s(X_15),z)))) ),[1,0],$fot(x2(X_15,s(x2(X_15,z))))]]) ).
cnf(refute_0_24,plain,
( x2(X_15,x2(s(X_15),z)) != x2(X_15,s(x2(X_15,z)))
| s(x2(X_15,x2(s(X_15),z))) = s(x2(X_15,s(x2(X_15,z)))) ),
inference(resolve,[$cnf( $equal(s(x2(X_15,x2(s(X_15),z))),s(x2(X_15,x2(s(X_15),z)))) )],[refute_0_22,refute_0_23]) ).
cnf(refute_0_25,plain,
s(x2(X_15,x2(s(X_15),z))) = s(x2(X_15,s(x2(X_15,z)))),
inference(resolve,[$cnf( $equal(x2(X_15,x2(s(X_15),z)),x2(X_15,s(x2(X_15,z)))) )],[refute_0_21,refute_0_24]) ).
cnf(refute_0_26,plain,
( s(x2(X_15,x2(s(X_15),z))) != s(x2(X_15,s(x2(X_15,z))))
| x22(s(s(z)),s(X_15)) != s(x2(X_15,x2(s(X_15),z)))
| x22(s(s(z)),s(X_15)) = s(x2(X_15,s(x2(X_15,z)))) ),
introduced(tautology,[equality,[$cnf( $equal(x22(s(s(z)),s(X_15)),s(x2(X_15,x2(s(X_15),z)))) ),[1],$fot(s(x2(X_15,s(x2(X_15,z)))))]]) ).
cnf(refute_0_27,plain,
( x22(s(s(z)),s(X_15)) != s(x2(X_15,x2(s(X_15),z)))
| x22(s(s(z)),s(X_15)) = s(x2(X_15,s(x2(X_15,z)))) ),
inference(resolve,[$cnf( $equal(s(x2(X_15,x2(s(X_15),z))),s(x2(X_15,s(x2(X_15,z))))) )],[refute_0_25,refute_0_26]) ).
cnf(refute_0_28,plain,
x22(s(s(z)),s(X_15)) = s(x2(X_15,s(x2(X_15,z)))),
inference(resolve,[$cnf( $equal(x22(s(s(z)),s(X_15)),s(x2(X_15,x2(s(X_15),z)))) )],[refute_0_16,refute_0_27]) ).
cnf(refute_0_29,plain,
x22(s(s(z)),s(s(N))) = s(x2(s(N),s(x2(s(N),z)))),
inference(subst,[],[refute_0_28:[bind(X_15,$fot(s(N)))]]) ).
cnf(refute_0_30,plain,
x2(s(N),z) = s(x2(N,z)),
inference(subst,[],[axiom_001:[bind(Y,$fot(z))]]) ).
cnf(refute_0_31,plain,
( x2(s(N),z) != s(x2(N,z))
| x22(s(s(z)),s(s(N))) != s(x2(s(N),s(x2(s(N),z))))
| x22(s(s(z)),s(s(N))) = s(x2(s(N),s(s(x2(N,z))))) ),
introduced(tautology,[equality,[$cnf( $equal(x22(s(s(z)),s(s(N))),s(x2(s(N),s(x2(s(N),z))))) ),[1,0,1,0],$fot(s(x2(N,z)))]]) ).
cnf(refute_0_32,plain,
( x22(s(s(z)),s(s(N))) != s(x2(s(N),s(x2(s(N),z))))
| x22(s(s(z)),s(s(N))) = s(x2(s(N),s(s(x2(N,z))))) ),
inference(resolve,[$cnf( $equal(x2(s(N),z),s(x2(N,z))) )],[refute_0_30,refute_0_31]) ).
cnf(refute_0_33,plain,
x22(s(s(z)),s(s(N))) = s(x2(s(N),s(s(x2(N,z))))),
inference(resolve,[$cnf( $equal(x22(s(s(z)),s(s(N))),s(x2(s(N),s(x2(s(N),z))))) )],[refute_0_29,refute_0_32]) ).
cnf(refute_0_34,plain,
x2(s(N),s(s(x2(N,z)))) = s(x2(N,s(s(x2(N,z))))),
inference(subst,[],[axiom_001:[bind(Y,$fot(s(s(x2(N,z)))))]]) ).
cnf(refute_0_35,plain,
s(x2(s(N),s(s(x2(N,z))))) = s(x2(s(N),s(s(x2(N,z))))),
introduced(tautology,[refl,[$fot(s(x2(s(N),s(s(x2(N,z))))))]]) ).
cnf(refute_0_36,plain,
( s(x2(s(N),s(s(x2(N,z))))) != s(x2(s(N),s(s(x2(N,z)))))
| x2(s(N),s(s(x2(N,z)))) != s(x2(N,s(s(x2(N,z)))))
| s(x2(s(N),s(s(x2(N,z))))) = s(s(x2(N,s(s(x2(N,z)))))) ),
introduced(tautology,[equality,[$cnf( $equal(s(x2(s(N),s(s(x2(N,z))))),s(x2(s(N),s(s(x2(N,z)))))) ),[1,0],$fot(s(x2(N,s(s(x2(N,z))))))]]) ).
cnf(refute_0_37,plain,
( x2(s(N),s(s(x2(N,z)))) != s(x2(N,s(s(x2(N,z)))))
| s(x2(s(N),s(s(x2(N,z))))) = s(s(x2(N,s(s(x2(N,z)))))) ),
inference(resolve,[$cnf( $equal(s(x2(s(N),s(s(x2(N,z))))),s(x2(s(N),s(s(x2(N,z)))))) )],[refute_0_35,refute_0_36]) ).
cnf(refute_0_38,plain,
s(x2(s(N),s(s(x2(N,z))))) = s(s(x2(N,s(s(x2(N,z)))))),
inference(resolve,[$cnf( $equal(x2(s(N),s(s(x2(N,z)))),s(x2(N,s(s(x2(N,z)))))) )],[refute_0_34,refute_0_37]) ).
cnf(refute_0_39,plain,
( s(x2(s(N),s(s(x2(N,z))))) != s(s(x2(N,s(s(x2(N,z))))))
| x22(s(s(z)),s(s(N))) != s(x2(s(N),s(s(x2(N,z)))))
| x22(s(s(z)),s(s(N))) = s(s(x2(N,s(s(x2(N,z)))))) ),
introduced(tautology,[equality,[$cnf( $equal(x22(s(s(z)),s(s(N))),s(x2(s(N),s(s(x2(N,z)))))) ),[1],$fot(s(s(x2(N,s(s(x2(N,z)))))))]]) ).
cnf(refute_0_40,plain,
( x22(s(s(z)),s(s(N))) != s(x2(s(N),s(s(x2(N,z)))))
| x22(s(s(z)),s(s(N))) = s(s(x2(N,s(s(x2(N,z)))))) ),
inference(resolve,[$cnf( $equal(s(x2(s(N),s(s(x2(N,z))))),s(s(x2(N,s(s(x2(N,z))))))) )],[refute_0_38,refute_0_39]) ).
cnf(refute_0_41,plain,
x22(s(s(z)),s(s(N))) = s(s(x2(N,s(s(x2(N,z)))))),
inference(resolve,[$cnf( $equal(x22(s(s(z)),s(s(N))),s(x2(s(N),s(s(x2(N,z)))))) )],[refute_0_33,refute_0_40]) ).
cnf(refute_0_42,plain,
x22(s(s(z)),s(s(z))) = s(s(x2(z,s(s(x2(z,z)))))),
inference(subst,[],[refute_0_41:[bind(N,$fot(z))]]) ).
cnf(refute_0_43,plain,
x2(z,z) = z,
inference(subst,[],[axiom:[bind(Y,$fot(z))]]) ).
cnf(refute_0_44,plain,
( x2(z,z) != z
| x22(s(s(z)),s(s(z))) != s(s(x2(z,s(s(x2(z,z))))))
| x22(s(s(z)),s(s(z))) = s(s(x2(z,s(s(z))))) ),
introduced(tautology,[equality,[$cnf( $equal(x22(s(s(z)),s(s(z))),s(s(x2(z,s(s(x2(z,z))))))) ),[1,0,0,1,0,0],$fot(z)]]) ).
cnf(refute_0_45,plain,
( x22(s(s(z)),s(s(z))) != s(s(x2(z,s(s(x2(z,z))))))
| x22(s(s(z)),s(s(z))) = s(s(x2(z,s(s(z))))) ),
inference(resolve,[$cnf( $equal(x2(z,z),z) )],[refute_0_43,refute_0_44]) ).
cnf(refute_0_46,plain,
x22(s(s(z)),s(s(z))) = s(s(x2(z,s(s(z))))),
inference(resolve,[$cnf( $equal(x22(s(s(z)),s(s(z))),s(s(x2(z,s(s(x2(z,z))))))) )],[refute_0_42,refute_0_45]) ).
cnf(refute_0_47,plain,
x2(z,s(s(z))) = s(s(z)),
inference(subst,[],[axiom:[bind(Y,$fot(s(s(z))))]]) ).
cnf(refute_0_48,plain,
s(x2(z,s(s(z)))) = s(x2(z,s(s(z)))),
introduced(tautology,[refl,[$fot(s(x2(z,s(s(z)))))]]) ).
cnf(refute_0_49,plain,
( s(x2(z,s(s(z)))) != s(x2(z,s(s(z))))
| x2(z,s(s(z))) != s(s(z))
| s(x2(z,s(s(z)))) = s(s(s(z))) ),
introduced(tautology,[equality,[$cnf( $equal(s(x2(z,s(s(z)))),s(x2(z,s(s(z))))) ),[1,0],$fot(s(s(z)))]]) ).
cnf(refute_0_50,plain,
( x2(z,s(s(z))) != s(s(z))
| s(x2(z,s(s(z)))) = s(s(s(z))) ),
inference(resolve,[$cnf( $equal(s(x2(z,s(s(z)))),s(x2(z,s(s(z))))) )],[refute_0_48,refute_0_49]) ).
cnf(refute_0_51,plain,
s(x2(z,s(s(z)))) = s(s(s(z))),
inference(resolve,[$cnf( $equal(x2(z,s(s(z))),s(s(z))) )],[refute_0_47,refute_0_50]) ).
cnf(refute_0_52,plain,
s(s(x2(z,s(s(z))))) = s(s(x2(z,s(s(z))))),
introduced(tautology,[refl,[$fot(s(s(x2(z,s(s(z))))))]]) ).
cnf(refute_0_53,plain,
( s(s(x2(z,s(s(z))))) != s(s(x2(z,s(s(z)))))
| s(x2(z,s(s(z)))) != s(s(s(z)))
| s(s(x2(z,s(s(z))))) = s(s(s(s(z)))) ),
introduced(tautology,[equality,[$cnf( $equal(s(s(x2(z,s(s(z))))),s(s(x2(z,s(s(z)))))) ),[1,0],$fot(s(s(s(z))))]]) ).
cnf(refute_0_54,plain,
( s(x2(z,s(s(z)))) != s(s(s(z)))
| s(s(x2(z,s(s(z))))) = s(s(s(s(z)))) ),
inference(resolve,[$cnf( $equal(s(s(x2(z,s(s(z))))),s(s(x2(z,s(s(z)))))) )],[refute_0_52,refute_0_53]) ).
cnf(refute_0_55,plain,
s(s(x2(z,s(s(z))))) = s(s(s(s(z)))),
inference(resolve,[$cnf( $equal(s(x2(z,s(s(z)))),s(s(s(z)))) )],[refute_0_51,refute_0_54]) ).
cnf(refute_0_56,plain,
( s(s(x2(z,s(s(z))))) != s(s(s(s(z))))
| x22(s(s(z)),s(s(z))) != s(s(x2(z,s(s(z)))))
| x22(s(s(z)),s(s(z))) = s(s(s(s(z)))) ),
introduced(tautology,[equality,[$cnf( $equal(x22(s(s(z)),s(s(z))),s(s(x2(z,s(s(z)))))) ),[1],$fot(s(s(s(s(z)))))]]) ).
cnf(refute_0_57,plain,
( x22(s(s(z)),s(s(z))) != s(s(x2(z,s(s(z)))))
| x22(s(s(z)),s(s(z))) = s(s(s(s(z)))) ),
inference(resolve,[$cnf( $equal(s(s(x2(z,s(s(z))))),s(s(s(s(z))))) )],[refute_0_55,refute_0_56]) ).
cnf(refute_0_58,plain,
x22(s(s(z)),s(s(z))) = s(s(s(s(z)))),
inference(resolve,[$cnf( $equal(x22(s(s(z)),s(s(z))),s(s(x2(z,s(s(z)))))) )],[refute_0_46,refute_0_57]) ).
cnf(refute_0_59,plain,
( mul_idem(s(s(z))) != eq(x22(s(s(z)),s(s(z))),s(s(z)))
| x22(s(s(z)),s(s(z))) != s(s(s(s(z))))
| mul_idem(s(s(z))) = eq(s(s(s(s(z)))),s(s(z))) ),
introduced(tautology,[equality,[$cnf( $equal(mul_idem(s(s(z))),eq(x22(s(s(z)),s(s(z))),s(s(z)))) ),[1,0],$fot(s(s(s(s(z)))))]]) ).
cnf(refute_0_60,plain,
( mul_idem(s(s(z))) != eq(x22(s(s(z)),s(s(z))),s(s(z)))
| mul_idem(s(s(z))) = eq(s(s(s(s(z)))),s(s(z))) ),
inference(resolve,[$cnf( $equal(x22(s(s(z)),s(s(z))),s(s(s(s(z))))) )],[refute_0_58,refute_0_59]) ).
cnf(refute_0_61,plain,
mul_idem(s(s(z))) = eq(s(s(s(s(z)))),s(s(z))),
inference(resolve,[$cnf( $equal(mul_idem(s(s(z))),eq(x22(s(s(z)),s(s(z))),s(s(z)))) )],[refute_0_1,refute_0_60]) ).
cnf(refute_0_62,plain,
eq(s(s(z)),z) = bfalse,
inference(subst,[],[axiom_009:[bind(X,$fot(s(z)))]]) ).
cnf(refute_0_63,plain,
eq(s(s(s(z))),s(z)) = eq(s(s(z)),z),
inference(subst,[],[axiom_007:[bind(X,$fot(s(s(z)))),bind(Y,$fot(z))]]) ).
cnf(refute_0_64,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_65,plain,
( X0 != X0
| X0 != Y0
| Y0 = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).
cnf(refute_0_66,plain,
( X0 != Y0
| Y0 = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_64,refute_0_65]) ).
cnf(refute_0_67,plain,
( Y0 != X0
| Y0 != Z
| X0 = Z ),
introduced(tautology,[equality,[$cnf( $equal(Y0,Z) ),[0],$fot(X0)]]) ).
cnf(refute_0_68,plain,
( X0 != Y0
| Y0 != Z
| X0 = Z ),
inference(resolve,[$cnf( $equal(Y0,X0) )],[refute_0_66,refute_0_67]) ).
cnf(refute_0_69,plain,
( eq(s(s(s(z))),s(z)) != eq(s(s(z)),z)
| eq(s(s(z)),z) != bfalse
| eq(s(s(s(z))),s(z)) = bfalse ),
inference(subst,[],[refute_0_68:[bind(X0,$fot(eq(s(s(s(z))),s(z)))),bind(Y0,$fot(eq(s(s(z)),z))),bind(Z,$fot(bfalse))]]) ).
cnf(refute_0_70,plain,
( eq(s(s(z)),z) != bfalse
| eq(s(s(s(z))),s(z)) = bfalse ),
inference(resolve,[$cnf( $equal(eq(s(s(s(z))),s(z)),eq(s(s(z)),z)) )],[refute_0_63,refute_0_69]) ).
cnf(refute_0_71,plain,
eq(s(s(s(z))),s(z)) = bfalse,
inference(resolve,[$cnf( $equal(eq(s(s(z)),z),bfalse) )],[refute_0_62,refute_0_70]) ).
cnf(refute_0_72,plain,
eq(s(s(s(s(z)))),s(s(z))) = eq(s(s(s(z))),s(z)),
inference(subst,[],[axiom_007:[bind(X,$fot(s(s(s(z))))),bind(Y,$fot(s(z)))]]) ).
cnf(refute_0_73,plain,
( eq(s(s(s(s(z)))),s(s(z))) != eq(s(s(s(z))),s(z))
| eq(s(s(s(z))),s(z)) != bfalse
| eq(s(s(s(s(z)))),s(s(z))) = bfalse ),
inference(subst,[],[refute_0_68:[bind(X0,$fot(eq(s(s(s(s(z)))),s(s(z))))),bind(Y0,$fot(eq(s(s(s(z))),s(z)))),bind(Z,$fot(bfalse))]]) ).
cnf(refute_0_74,plain,
( eq(s(s(s(z))),s(z)) != bfalse
| eq(s(s(s(s(z)))),s(s(z))) = bfalse ),
inference(resolve,[$cnf( $equal(eq(s(s(s(s(z)))),s(s(z))),eq(s(s(s(z))),s(z))) )],[refute_0_72,refute_0_73]) ).
cnf(refute_0_75,plain,
eq(s(s(s(s(z)))),s(s(z))) = bfalse,
inference(resolve,[$cnf( $equal(eq(s(s(s(z))),s(z)),bfalse) )],[refute_0_71,refute_0_74]) ).
cnf(refute_0_76,plain,
( eq(s(s(s(s(z)))),s(s(z))) != bfalse
| mul_idem(s(s(z))) != eq(s(s(s(s(z)))),s(s(z)))
| mul_idem(s(s(z))) = bfalse ),
introduced(tautology,[equality,[$cnf( $equal(mul_idem(s(s(z))),eq(s(s(s(s(z)))),s(s(z)))) ),[1],$fot(bfalse)]]) ).
cnf(refute_0_77,plain,
( mul_idem(s(s(z))) != eq(s(s(s(s(z)))),s(s(z)))
| mul_idem(s(s(z))) = bfalse ),
inference(resolve,[$cnf( $equal(eq(s(s(s(s(z)))),s(s(z))),bfalse) )],[refute_0_75,refute_0_76]) ).
cnf(refute_0_78,plain,
mul_idem(s(s(z))) = bfalse,
inference(resolve,[$cnf( $equal(mul_idem(s(s(z))),eq(s(s(s(s(z)))),s(s(z)))) )],[refute_0_61,refute_0_77]) ).
cnf(refute_0_79,plain,
( eq2(bfalse,bfalse) != btrue
| mul_idem(s(s(z))) != bfalse
| eq2(mul_idem(s(s(z))),bfalse) = btrue ),
introduced(tautology,[equality,[$cnf( ~ $equal(eq2(mul_idem(s(s(z))),bfalse),btrue) ),[0,0],$fot(bfalse)]]) ).
cnf(refute_0_80,plain,
( eq2(bfalse,bfalse) != btrue
| eq2(mul_idem(s(s(z))),bfalse) = btrue ),
inference(resolve,[$cnf( $equal(mul_idem(s(s(z))),bfalse) )],[refute_0_78,refute_0_79]) ).
cnf(refute_0_81,plain,
eq2(bfalse,bfalse) != btrue,
inference(resolve,[$cnf( $equal(eq2(mul_idem(s(s(z))),bfalse),btrue) )],[refute_0_80,refute_0_0]) ).
cnf(refute_0_82,plain,
eq2(bfalse,bfalse) = btrue,
inference(subst,[],[axiom_011:[bind(X,$fot(bfalse))]]) ).
cnf(refute_0_83,plain,
( btrue != btrue
| eq2(bfalse,bfalse) != btrue
| eq2(bfalse,bfalse) = btrue ),
introduced(tautology,[equality,[$cnf( $equal(eq2(bfalse,bfalse),btrue) ),[1],$fot(btrue)]]) ).
cnf(refute_0_84,plain,
( btrue != btrue
| eq2(bfalse,bfalse) = btrue ),
inference(resolve,[$cnf( $equal(eq2(bfalse,bfalse),btrue) )],[refute_0_82,refute_0_83]) ).
cnf(refute_0_85,plain,
btrue != btrue,
inference(resolve,[$cnf( $equal(eq2(bfalse,bfalse),btrue) )],[refute_0_84,refute_0_81]) ).
cnf(refute_0_86,plain,
btrue = btrue,
introduced(tautology,[refl,[$fot(btrue)]]) ).
cnf(refute_0_87,plain,
$false,
inference(resolve,[$cnf( $equal(btrue,btrue) )],[refute_0_86,refute_0_85]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.13 % Problem : SWX204-1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.13 % Command : metis --show proof --show saturation %s
% 0.18/0.34 % Computer : n007.cluster.edu
% 0.18/0.34 % Model : x86_64 x86_64
% 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.34 % Memory : 8042.1875MB
% 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.35 % CPULimit : 300
% 0.18/0.35 % WCLimit : 300
% 0.18/0.35 % DateTime : Tue May 5 11:28:53 EDT 2026
% 0.18/0.35 % CPUTime :
% 0.18/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.20/0.42 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.42
% 0.20/0.42 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.20/0.44
%------------------------------------------------------------------------------