%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SWX228-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %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 07:04:37 PM UTC 2026
% Result : Unsatisfiable 0.54s 0.76s
% Output : CNFRefutation 0.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 44
% Syntax : Number of clauses : 121 ( 68 unt; 0 nHn; 57 RR)
% Number of literals : 200 ( 199 equ; 83 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 4 con; 0-4 aty)
% Number of variables : 190 ( 25 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom_001,axiom,
aux(Y,Z,Xs,bfalse) = cons(Z,union(Xs,Y)) ).
cnf(axiom_003,axiom,
barbar(bfalse,Y) = Y ).
cnf(axiom_005,axiom,
eqNat(s(Z),z) = bfalse ).
cnf(axiom_006,axiom,
eqNat(z,s(X2)) = bfalse ).
cnf(axiom_008,axiom,
elem(X,nil) = bfalse ).
cnf(axiom_009,axiom,
elem(X,cons(Z,Xs)) = barbar(eqNat(X,Z),elem(X,Xs)) ).
cnf(axiom_010,axiom,
union(nil,Y) = Y ).
cnf(axiom_011,axiom,
union(cons(Z,Xs),Y) = aux(Y,Z,Xs,elem(Z,Y)) ).
cnf(axiom_012,axiom,
prop_union_comm(X,Y) = eq(union(X,Y),union(Y,X)) ).
cnf(axiom_016,axiom,
eq2(s(X),z) = bfalse ).
cnf(axiom_020,axiom,
eq3(X,X) = btrue ).
cnf(axiom_021,axiom,
( eq2(X,Z) != bfalse
| eq(cons(X,Y),cons(Z,X2)) = bfalse ) ).
cnf(goal,negated_conjecture,
eq3(prop_union_comm(X,Y),bfalse) != btrue ).
cnf(refute_0_0,plain,
eq3(prop_union_comm(cons(s(X_358),nil),cons(z,nil)),bfalse) != btrue,
inference(subst,[],[goal:[bind(X,$fot(cons(s(X_358),nil))),bind(Y,$fot(cons(z,nil)))]]) ).
cnf(refute_0_1,plain,
prop_union_comm(cons(s(X_87),X_88),cons(z,nil)) = eq(union(cons(s(X_87),X_88),cons(z,nil)),union(cons(z,nil),cons(s(X_87),X_88))),
inference(subst,[],[axiom_012:[bind(X,$fot(cons(s(X_87),X_88))),bind(Y,$fot(cons(z,nil)))]]) ).
cnf(refute_0_2,plain,
union(cons(Z,Xs),cons(X_50,nil)) = aux(cons(X_50,nil),Z,Xs,elem(Z,cons(X_50,nil))),
inference(subst,[],[axiom_011:[bind(Y,$fot(cons(X_50,nil)))]]) ).
cnf(refute_0_3,plain,
elem(X_43,cons(X_45,nil)) = barbar(eqNat(X_43,X_45),elem(X_43,nil)),
inference(subst,[],[axiom_009:[bind(X,$fot(X_43)),bind(Xs,$fot(nil)),bind(Z,$fot(X_45))]]) ).
cnf(refute_0_4,plain,
elem(X_43,nil) = bfalse,
inference(subst,[],[axiom_008:[bind(X,$fot(X_43))]]) ).
cnf(refute_0_5,plain,
( elem(X_43,cons(X_45,nil)) != barbar(eqNat(X_43,X_45),elem(X_43,nil))
| elem(X_43,nil) != bfalse
| elem(X_43,cons(X_45,nil)) = barbar(eqNat(X_43,X_45),bfalse) ),
introduced(tautology,[equality,[$cnf( $equal(elem(X_43,cons(X_45,nil)),barbar(eqNat(X_43,X_45),elem(X_43,nil))) ),[1,1],$fot(bfalse)]]) ).
cnf(refute_0_6,plain,
( elem(X_43,cons(X_45,nil)) != barbar(eqNat(X_43,X_45),elem(X_43,nil))
| elem(X_43,cons(X_45,nil)) = barbar(eqNat(X_43,X_45),bfalse) ),
inference(resolve,[$cnf( $equal(elem(X_43,nil),bfalse) )],[refute_0_4,refute_0_5]) ).
cnf(refute_0_7,plain,
elem(X_43,cons(X_45,nil)) = barbar(eqNat(X_43,X_45),bfalse),
inference(resolve,[$cnf( $equal(elem(X_43,cons(X_45,nil)),barbar(eqNat(X_43,X_45),elem(X_43,nil))) )],[refute_0_3,refute_0_6]) ).
cnf(refute_0_8,plain,
elem(Z,cons(X_50,nil)) = barbar(eqNat(Z,X_50),bfalse),
inference(subst,[],[refute_0_7:[bind(X_43,$fot(Z)),bind(X_45,$fot(X_50))]]) ).
cnf(refute_0_9,plain,
( elem(Z,cons(X_50,nil)) != barbar(eqNat(Z,X_50),bfalse)
| union(cons(Z,Xs),cons(X_50,nil)) != aux(cons(X_50,nil),Z,Xs,elem(Z,cons(X_50,nil)))
| union(cons(Z,Xs),cons(X_50,nil)) = aux(cons(X_50,nil),Z,Xs,barbar(eqNat(Z,X_50),bfalse)) ),
introduced(tautology,[equality,[$cnf( $equal(union(cons(Z,Xs),cons(X_50,nil)),aux(cons(X_50,nil),Z,Xs,elem(Z,cons(X_50,nil)))) ),[1,3],$fot(barbar(eqNat(Z,X_50),bfalse))]]) ).
cnf(refute_0_10,plain,
( union(cons(Z,Xs),cons(X_50,nil)) != aux(cons(X_50,nil),Z,Xs,elem(Z,cons(X_50,nil)))
| union(cons(Z,Xs),cons(X_50,nil)) = aux(cons(X_50,nil),Z,Xs,barbar(eqNat(Z,X_50),bfalse)) ),
inference(resolve,[$cnf( $equal(elem(Z,cons(X_50,nil)),barbar(eqNat(Z,X_50),bfalse)) )],[refute_0_8,refute_0_9]) ).
cnf(refute_0_11,plain,
union(cons(Z,Xs),cons(X_50,nil)) = aux(cons(X_50,nil),Z,Xs,barbar(eqNat(Z,X_50),bfalse)),
inference(resolve,[$cnf( $equal(union(cons(Z,Xs),cons(X_50,nil)),aux(cons(X_50,nil),Z,Xs,elem(Z,cons(X_50,nil)))) )],[refute_0_2,refute_0_10]) ).
cnf(refute_0_12,plain,
union(cons(s(Z),X_84),cons(z,nil)) = aux(cons(z,nil),s(Z),X_84,barbar(eqNat(s(Z),z),bfalse)),
inference(subst,[],[refute_0_11:[bind(Xs,$fot(X_84)),bind(Z,$fot(s(Z))),bind(X_50,$fot(z))]]) ).
cnf(refute_0_13,plain,
( eqNat(s(Z),z) != bfalse
| union(cons(s(Z),X_84),cons(z,nil)) != aux(cons(z,nil),s(Z),X_84,barbar(eqNat(s(Z),z),bfalse))
| union(cons(s(Z),X_84),cons(z,nil)) = aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)) ),
introduced(tautology,[equality,[$cnf( $equal(union(cons(s(Z),X_84),cons(z,nil)),aux(cons(z,nil),s(Z),X_84,barbar(eqNat(s(Z),z),bfalse))) ),[1,3,0],$fot(bfalse)]]) ).
cnf(refute_0_14,plain,
( union(cons(s(Z),X_84),cons(z,nil)) != aux(cons(z,nil),s(Z),X_84,barbar(eqNat(s(Z),z),bfalse))
| union(cons(s(Z),X_84),cons(z,nil)) = aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)) ),
inference(resolve,[$cnf( $equal(eqNat(s(Z),z),bfalse) )],[axiom_005,refute_0_13]) ).
cnf(refute_0_15,plain,
union(cons(s(Z),X_84),cons(z,nil)) = aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)),
inference(resolve,[$cnf( $equal(union(cons(s(Z),X_84),cons(z,nil)),aux(cons(z,nil),s(Z),X_84,barbar(eqNat(s(Z),z),bfalse))) )],[refute_0_12,refute_0_14]) ).
cnf(refute_0_16,plain,
aux(cons(z,nil),s(Z),X_84,bfalse) = cons(s(Z),union(X_84,cons(z,nil))),
inference(subst,[],[axiom_001:[bind(Xs,$fot(X_84)),bind(Y,$fot(cons(z,nil))),bind(Z,$fot(s(Z)))]]) ).
cnf(refute_0_17,plain,
barbar(bfalse,bfalse) = bfalse,
inference(subst,[],[axiom_003:[bind(Y,$fot(bfalse))]]) ).
cnf(refute_0_18,plain,
aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)) = aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)),
introduced(tautology,[refl,[$fot(aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)))]]) ).
cnf(refute_0_19,plain,
( aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)) != aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse))
| barbar(bfalse,bfalse) != bfalse
| aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)) = aux(cons(z,nil),s(Z),X_84,bfalse) ),
introduced(tautology,[equality,[$cnf( $equal(aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)),aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse))) ),[1,3],$fot(bfalse)]]) ).
cnf(refute_0_20,plain,
( barbar(bfalse,bfalse) != bfalse
| aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)) = aux(cons(z,nil),s(Z),X_84,bfalse) ),
inference(resolve,[$cnf( $equal(aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)),aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse))) )],[refute_0_18,refute_0_19]) ).
cnf(refute_0_21,plain,
aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)) = aux(cons(z,nil),s(Z),X_84,bfalse),
inference(resolve,[$cnf( $equal(barbar(bfalse,bfalse),bfalse) )],[refute_0_17,refute_0_20]) ).
cnf(refute_0_22,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_23,plain,
( X0 != X0
| X0 != Y0
| Y0 = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).
cnf(refute_0_24,plain,
( X0 != Y0
| Y0 = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_22,refute_0_23]) ).
cnf(refute_0_25,plain,
( Y0 != X0
| Y0 != Z0
| X0 = Z0 ),
introduced(tautology,[equality,[$cnf( $equal(Y0,Z0) ),[0],$fot(X0)]]) ).
cnf(refute_0_26,plain,
( X0 != Y0
| Y0 != Z0
| X0 = Z0 ),
inference(resolve,[$cnf( $equal(Y0,X0) )],[refute_0_24,refute_0_25]) ).
cnf(refute_0_27,plain,
( aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)) != aux(cons(z,nil),s(Z),X_84,bfalse)
| aux(cons(z,nil),s(Z),X_84,bfalse) != cons(s(Z),union(X_84,cons(z,nil)))
| aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)) = cons(s(Z),union(X_84,cons(z,nil))) ),
inference(subst,[],[refute_0_26:[bind(X0,$fot(aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)))),bind(Y0,$fot(aux(cons(z,nil),s(Z),X_84,bfalse))),bind(Z0,$fot(cons(s(Z),union(X_84,cons(z,nil)))))]]) ).
cnf(refute_0_28,plain,
( aux(cons(z,nil),s(Z),X_84,bfalse) != cons(s(Z),union(X_84,cons(z,nil)))
| aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)) = cons(s(Z),union(X_84,cons(z,nil))) ),
inference(resolve,[$cnf( $equal(aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)),aux(cons(z,nil),s(Z),X_84,bfalse)) )],[refute_0_21,refute_0_27]) ).
cnf(refute_0_29,plain,
aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)) = cons(s(Z),union(X_84,cons(z,nil))),
inference(resolve,[$cnf( $equal(aux(cons(z,nil),s(Z),X_84,bfalse),cons(s(Z),union(X_84,cons(z,nil)))) )],[refute_0_16,refute_0_28]) ).
cnf(refute_0_30,plain,
( aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)) != cons(s(Z),union(X_84,cons(z,nil)))
| union(cons(s(Z),X_84),cons(z,nil)) != aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse))
| union(cons(s(Z),X_84),cons(z,nil)) = cons(s(Z),union(X_84,cons(z,nil))) ),
introduced(tautology,[equality,[$cnf( $equal(union(cons(s(Z),X_84),cons(z,nil)),aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse))) ),[1],$fot(cons(s(Z),union(X_84,cons(z,nil))))]]) ).
cnf(refute_0_31,plain,
( union(cons(s(Z),X_84),cons(z,nil)) != aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse))
| union(cons(s(Z),X_84),cons(z,nil)) = cons(s(Z),union(X_84,cons(z,nil))) ),
inference(resolve,[$cnf( $equal(aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse)),cons(s(Z),union(X_84,cons(z,nil)))) )],[refute_0_29,refute_0_30]) ).
cnf(refute_0_32,plain,
union(cons(s(Z),X_84),cons(z,nil)) = cons(s(Z),union(X_84,cons(z,nil))),
inference(resolve,[$cnf( $equal(union(cons(s(Z),X_84),cons(z,nil)),aux(cons(z,nil),s(Z),X_84,barbar(bfalse,bfalse))) )],[refute_0_15,refute_0_31]) ).
cnf(refute_0_33,plain,
union(cons(s(X_87),X_88),cons(z,nil)) = cons(s(X_87),union(X_88,cons(z,nil))),
inference(subst,[],[refute_0_32:[bind(Z,$fot(X_87)),bind(X_84,$fot(X_88))]]) ).
cnf(refute_0_34,plain,
( prop_union_comm(cons(s(X_87),X_88),cons(z,nil)) != eq(union(cons(s(X_87),X_88),cons(z,nil)),union(cons(z,nil),cons(s(X_87),X_88)))
| union(cons(s(X_87),X_88),cons(z,nil)) != cons(s(X_87),union(X_88,cons(z,nil)))
| prop_union_comm(cons(s(X_87),X_88),cons(z,nil)) = eq(cons(s(X_87),union(X_88,cons(z,nil))),union(cons(z,nil),cons(s(X_87),X_88))) ),
introduced(tautology,[equality,[$cnf( $equal(prop_union_comm(cons(s(X_87),X_88),cons(z,nil)),eq(union(cons(s(X_87),X_88),cons(z,nil)),union(cons(z,nil),cons(s(X_87),X_88)))) ),[1,0],$fot(cons(s(X_87),union(X_88,cons(z,nil))))]]) ).
cnf(refute_0_35,plain,
( prop_union_comm(cons(s(X_87),X_88),cons(z,nil)) != eq(union(cons(s(X_87),X_88),cons(z,nil)),union(cons(z,nil),cons(s(X_87),X_88)))
| prop_union_comm(cons(s(X_87),X_88),cons(z,nil)) = eq(cons(s(X_87),union(X_88,cons(z,nil))),union(cons(z,nil),cons(s(X_87),X_88))) ),
inference(resolve,[$cnf( $equal(union(cons(s(X_87),X_88),cons(z,nil)),cons(s(X_87),union(X_88,cons(z,nil)))) )],[refute_0_33,refute_0_34]) ).
cnf(refute_0_36,plain,
prop_union_comm(cons(s(X_87),X_88),cons(z,nil)) = eq(cons(s(X_87),union(X_88,cons(z,nil))),union(cons(z,nil),cons(s(X_87),X_88))),
inference(resolve,[$cnf( $equal(prop_union_comm(cons(s(X_87),X_88),cons(z,nil)),eq(union(cons(s(X_87),X_88),cons(z,nil)),union(cons(z,nil),cons(s(X_87),X_88)))) )],[refute_0_1,refute_0_35]) ).
cnf(refute_0_37,plain,
prop_union_comm(cons(s(X_120),nil),cons(z,nil)) = eq(cons(s(X_120),union(nil,cons(z,nil))),union(cons(z,nil),cons(s(X_120),nil))),
inference(subst,[],[refute_0_36:[bind(X_87,$fot(X_120)),bind(X_88,$fot(nil))]]) ).
cnf(refute_0_38,plain,
union(cons(z,Xs),cons(s(X_47),X_48)) = aux(cons(s(X_47),X_48),z,Xs,elem(z,cons(s(X_47),X_48))),
inference(subst,[],[axiom_011:[bind(Y,$fot(cons(s(X_47),X_48))),bind(Z,$fot(z))]]) ).
cnf(refute_0_39,plain,
elem(z,cons(s(X2),X_44)) = barbar(eqNat(z,s(X2)),elem(z,X_44)),
inference(subst,[],[axiom_009:[bind(X,$fot(z)),bind(Xs,$fot(X_44)),bind(Z,$fot(s(X2)))]]) ).
cnf(refute_0_40,plain,
( elem(z,cons(s(X2),X_44)) != barbar(eqNat(z,s(X2)),elem(z,X_44))
| eqNat(z,s(X2)) != bfalse
| elem(z,cons(s(X2),X_44)) = barbar(bfalse,elem(z,X_44)) ),
introduced(tautology,[equality,[$cnf( $equal(elem(z,cons(s(X2),X_44)),barbar(eqNat(z,s(X2)),elem(z,X_44))) ),[1,0],$fot(bfalse)]]) ).
cnf(refute_0_41,plain,
( elem(z,cons(s(X2),X_44)) != barbar(eqNat(z,s(X2)),elem(z,X_44))
| elem(z,cons(s(X2),X_44)) = barbar(bfalse,elem(z,X_44)) ),
inference(resolve,[$cnf( $equal(eqNat(z,s(X2)),bfalse) )],[axiom_006,refute_0_40]) ).
cnf(refute_0_42,plain,
elem(z,cons(s(X2),X_44)) = barbar(bfalse,elem(z,X_44)),
inference(resolve,[$cnf( $equal(elem(z,cons(s(X2),X_44)),barbar(eqNat(z,s(X2)),elem(z,X_44))) )],[refute_0_39,refute_0_41]) ).
cnf(refute_0_43,plain,
barbar(bfalse,elem(z,X_44)) = elem(z,X_44),
inference(subst,[],[axiom_003:[bind(Y,$fot(elem(z,X_44)))]]) ).
cnf(refute_0_44,plain,
( barbar(bfalse,elem(z,X_44)) != elem(z,X_44)
| elem(z,cons(s(X2),X_44)) != barbar(bfalse,elem(z,X_44))
| elem(z,cons(s(X2),X_44)) = elem(z,X_44) ),
introduced(tautology,[equality,[$cnf( $equal(elem(z,cons(s(X2),X_44)),barbar(bfalse,elem(z,X_44))) ),[1],$fot(elem(z,X_44))]]) ).
cnf(refute_0_45,plain,
( elem(z,cons(s(X2),X_44)) != barbar(bfalse,elem(z,X_44))
| elem(z,cons(s(X2),X_44)) = elem(z,X_44) ),
inference(resolve,[$cnf( $equal(barbar(bfalse,elem(z,X_44)),elem(z,X_44)) )],[refute_0_43,refute_0_44]) ).
cnf(refute_0_46,plain,
elem(z,cons(s(X2),X_44)) = elem(z,X_44),
inference(resolve,[$cnf( $equal(elem(z,cons(s(X2),X_44)),barbar(bfalse,elem(z,X_44))) )],[refute_0_42,refute_0_45]) ).
cnf(refute_0_47,plain,
elem(z,cons(s(X_47),X_48)) = elem(z,X_48),
inference(subst,[],[refute_0_46:[bind(X2,$fot(X_47)),bind(X_44,$fot(X_48))]]) ).
cnf(refute_0_48,plain,
( elem(z,cons(s(X_47),X_48)) != elem(z,X_48)
| union(cons(z,Xs),cons(s(X_47),X_48)) != aux(cons(s(X_47),X_48),z,Xs,elem(z,cons(s(X_47),X_48)))
| union(cons(z,Xs),cons(s(X_47),X_48)) = aux(cons(s(X_47),X_48),z,Xs,elem(z,X_48)) ),
introduced(tautology,[equality,[$cnf( $equal(union(cons(z,Xs),cons(s(X_47),X_48)),aux(cons(s(X_47),X_48),z,Xs,elem(z,cons(s(X_47),X_48)))) ),[1,3],$fot(elem(z,X_48))]]) ).
cnf(refute_0_49,plain,
( union(cons(z,Xs),cons(s(X_47),X_48)) != aux(cons(s(X_47),X_48),z,Xs,elem(z,cons(s(X_47),X_48)))
| union(cons(z,Xs),cons(s(X_47),X_48)) = aux(cons(s(X_47),X_48),z,Xs,elem(z,X_48)) ),
inference(resolve,[$cnf( $equal(elem(z,cons(s(X_47),X_48)),elem(z,X_48)) )],[refute_0_47,refute_0_48]) ).
cnf(refute_0_50,plain,
union(cons(z,Xs),cons(s(X_47),X_48)) = aux(cons(s(X_47),X_48),z,Xs,elem(z,X_48)),
inference(resolve,[$cnf( $equal(union(cons(z,Xs),cons(s(X_47),X_48)),aux(cons(s(X_47),X_48),z,Xs,elem(z,cons(s(X_47),X_48)))) )],[refute_0_38,refute_0_49]) ).
cnf(refute_0_51,plain,
union(cons(z,X_79),cons(s(X_80),nil)) = aux(cons(s(X_80),nil),z,X_79,elem(z,nil)),
inference(subst,[],[refute_0_50:[bind(Xs,$fot(X_79)),bind(X_47,$fot(X_80)),bind(X_48,$fot(nil))]]) ).
cnf(refute_0_52,plain,
elem(z,nil) = bfalse,
inference(subst,[],[axiom_008:[bind(X,$fot(z))]]) ).
cnf(refute_0_53,plain,
( elem(z,nil) != bfalse
| union(cons(z,X_79),cons(s(X_80),nil)) != aux(cons(s(X_80),nil),z,X_79,elem(z,nil))
| union(cons(z,X_79),cons(s(X_80),nil)) = aux(cons(s(X_80),nil),z,X_79,bfalse) ),
introduced(tautology,[equality,[$cnf( $equal(union(cons(z,X_79),cons(s(X_80),nil)),aux(cons(s(X_80),nil),z,X_79,elem(z,nil))) ),[1,3],$fot(bfalse)]]) ).
cnf(refute_0_54,plain,
( union(cons(z,X_79),cons(s(X_80),nil)) != aux(cons(s(X_80),nil),z,X_79,elem(z,nil))
| union(cons(z,X_79),cons(s(X_80),nil)) = aux(cons(s(X_80),nil),z,X_79,bfalse) ),
inference(resolve,[$cnf( $equal(elem(z,nil),bfalse) )],[refute_0_52,refute_0_53]) ).
cnf(refute_0_55,plain,
union(cons(z,X_79),cons(s(X_80),nil)) = aux(cons(s(X_80),nil),z,X_79,bfalse),
inference(resolve,[$cnf( $equal(union(cons(z,X_79),cons(s(X_80),nil)),aux(cons(s(X_80),nil),z,X_79,elem(z,nil))) )],[refute_0_51,refute_0_54]) ).
cnf(refute_0_56,plain,
aux(cons(s(X_80),nil),z,X_79,bfalse) = cons(z,union(X_79,cons(s(X_80),nil))),
inference(subst,[],[axiom_001:[bind(Xs,$fot(X_79)),bind(Y,$fot(cons(s(X_80),nil))),bind(Z,$fot(z))]]) ).
cnf(refute_0_57,plain,
( aux(cons(s(X_80),nil),z,X_79,bfalse) != cons(z,union(X_79,cons(s(X_80),nil)))
| union(cons(z,X_79),cons(s(X_80),nil)) != aux(cons(s(X_80),nil),z,X_79,bfalse)
| union(cons(z,X_79),cons(s(X_80),nil)) = cons(z,union(X_79,cons(s(X_80),nil))) ),
introduced(tautology,[equality,[$cnf( $equal(union(cons(z,X_79),cons(s(X_80),nil)),aux(cons(s(X_80),nil),z,X_79,bfalse)) ),[1],$fot(cons(z,union(X_79,cons(s(X_80),nil))))]]) ).
cnf(refute_0_58,plain,
( union(cons(z,X_79),cons(s(X_80),nil)) != aux(cons(s(X_80),nil),z,X_79,bfalse)
| union(cons(z,X_79),cons(s(X_80),nil)) = cons(z,union(X_79,cons(s(X_80),nil))) ),
inference(resolve,[$cnf( $equal(aux(cons(s(X_80),nil),z,X_79,bfalse),cons(z,union(X_79,cons(s(X_80),nil)))) )],[refute_0_56,refute_0_57]) ).
cnf(refute_0_59,plain,
union(cons(z,X_79),cons(s(X_80),nil)) = cons(z,union(X_79,cons(s(X_80),nil))),
inference(resolve,[$cnf( $equal(union(cons(z,X_79),cons(s(X_80),nil)),aux(cons(s(X_80),nil),z,X_79,bfalse)) )],[refute_0_55,refute_0_58]) ).
cnf(refute_0_60,plain,
union(cons(z,nil),cons(s(X_120),nil)) = cons(z,union(nil,cons(s(X_120),nil))),
inference(subst,[],[refute_0_59:[bind(X_79,$fot(nil)),bind(X_80,$fot(X_120))]]) ).
cnf(refute_0_61,plain,
( prop_union_comm(cons(s(X_120),nil),cons(z,nil)) != eq(cons(s(X_120),union(nil,cons(z,nil))),union(cons(z,nil),cons(s(X_120),nil)))
| union(cons(z,nil),cons(s(X_120),nil)) != cons(z,union(nil,cons(s(X_120),nil)))
| prop_union_comm(cons(s(X_120),nil),cons(z,nil)) = eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))) ),
introduced(tautology,[equality,[$cnf( $equal(prop_union_comm(cons(s(X_120),nil),cons(z,nil)),eq(cons(s(X_120),union(nil,cons(z,nil))),union(cons(z,nil),cons(s(X_120),nil)))) ),[1,1],$fot(cons(z,union(nil,cons(s(X_120),nil))))]]) ).
cnf(refute_0_62,plain,
( prop_union_comm(cons(s(X_120),nil),cons(z,nil)) != eq(cons(s(X_120),union(nil,cons(z,nil))),union(cons(z,nil),cons(s(X_120),nil)))
| prop_union_comm(cons(s(X_120),nil),cons(z,nil)) = eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))) ),
inference(resolve,[$cnf( $equal(union(cons(z,nil),cons(s(X_120),nil)),cons(z,union(nil,cons(s(X_120),nil)))) )],[refute_0_60,refute_0_61]) ).
cnf(refute_0_63,plain,
prop_union_comm(cons(s(X_120),nil),cons(z,nil)) = eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))),
inference(resolve,[$cnf( $equal(prop_union_comm(cons(s(X_120),nil),cons(z,nil)),eq(cons(s(X_120),union(nil,cons(z,nil))),union(cons(z,nil),cons(s(X_120),nil)))) )],[refute_0_37,refute_0_62]) ).
cnf(refute_0_64,plain,
union(nil,cons(s(X_120),nil)) = cons(s(X_120),nil),
inference(subst,[],[axiom_010:[bind(Y,$fot(cons(s(X_120),nil)))]]) ).
cnf(refute_0_65,plain,
cons(z,union(nil,cons(s(X_120),nil))) = cons(z,union(nil,cons(s(X_120),nil))),
introduced(tautology,[refl,[$fot(cons(z,union(nil,cons(s(X_120),nil))))]]) ).
cnf(refute_0_66,plain,
( cons(z,union(nil,cons(s(X_120),nil))) != cons(z,union(nil,cons(s(X_120),nil)))
| union(nil,cons(s(X_120),nil)) != cons(s(X_120),nil)
| cons(z,union(nil,cons(s(X_120),nil))) = cons(z,cons(s(X_120),nil)) ),
introduced(tautology,[equality,[$cnf( $equal(cons(z,union(nil,cons(s(X_120),nil))),cons(z,union(nil,cons(s(X_120),nil)))) ),[1,1],$fot(cons(s(X_120),nil))]]) ).
cnf(refute_0_67,plain,
( union(nil,cons(s(X_120),nil)) != cons(s(X_120),nil)
| cons(z,union(nil,cons(s(X_120),nil))) = cons(z,cons(s(X_120),nil)) ),
inference(resolve,[$cnf( $equal(cons(z,union(nil,cons(s(X_120),nil))),cons(z,union(nil,cons(s(X_120),nil)))) )],[refute_0_65,refute_0_66]) ).
cnf(refute_0_68,plain,
cons(z,union(nil,cons(s(X_120),nil))) = cons(z,cons(s(X_120),nil)),
inference(resolve,[$cnf( $equal(union(nil,cons(s(X_120),nil)),cons(s(X_120),nil)) )],[refute_0_64,refute_0_67]) ).
cnf(refute_0_69,plain,
eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil)))) = eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil)))),
introduced(tautology,[refl,[$fot(eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil)))))]]) ).
cnf(refute_0_70,plain,
( cons(z,union(nil,cons(s(X_120),nil))) != cons(z,cons(s(X_120),nil))
| eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil)))) != eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil))))
| eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil)))) = eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil))) ),
introduced(tautology,[equality,[$cnf( $equal(eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil)))),eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil))))) ),[1,1],$fot(cons(z,cons(s(X_120),nil)))]]) ).
cnf(refute_0_71,plain,
( cons(z,union(nil,cons(s(X_120),nil))) != cons(z,cons(s(X_120),nil))
| eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil)))) = eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil))) ),
inference(resolve,[$cnf( $equal(eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil)))),eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil))))) )],[refute_0_69,refute_0_70]) ).
cnf(refute_0_72,plain,
eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil)))) = eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil))),
inference(resolve,[$cnf( $equal(cons(z,union(nil,cons(s(X_120),nil))),cons(z,cons(s(X_120),nil))) )],[refute_0_68,refute_0_71]) ).
cnf(refute_0_73,plain,
union(nil,cons(z,nil)) = cons(z,nil),
inference(subst,[],[axiom_010:[bind(Y,$fot(cons(z,nil)))]]) ).
cnf(refute_0_74,plain,
cons(s(X_120),union(nil,cons(z,nil))) = cons(s(X_120),union(nil,cons(z,nil))),
introduced(tautology,[refl,[$fot(cons(s(X_120),union(nil,cons(z,nil))))]]) ).
cnf(refute_0_75,plain,
( cons(s(X_120),union(nil,cons(z,nil))) != cons(s(X_120),union(nil,cons(z,nil)))
| union(nil,cons(z,nil)) != cons(z,nil)
| cons(s(X_120),union(nil,cons(z,nil))) = cons(s(X_120),cons(z,nil)) ),
introduced(tautology,[equality,[$cnf( $equal(cons(s(X_120),union(nil,cons(z,nil))),cons(s(X_120),union(nil,cons(z,nil)))) ),[1,1],$fot(cons(z,nil))]]) ).
cnf(refute_0_76,plain,
( union(nil,cons(z,nil)) != cons(z,nil)
| cons(s(X_120),union(nil,cons(z,nil))) = cons(s(X_120),cons(z,nil)) ),
inference(resolve,[$cnf( $equal(cons(s(X_120),union(nil,cons(z,nil))),cons(s(X_120),union(nil,cons(z,nil)))) )],[refute_0_74,refute_0_75]) ).
cnf(refute_0_77,plain,
cons(s(X_120),union(nil,cons(z,nil))) = cons(s(X_120),cons(z,nil)),
inference(resolve,[$cnf( $equal(union(nil,cons(z,nil)),cons(z,nil)) )],[refute_0_73,refute_0_76]) ).
cnf(refute_0_78,plain,
eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))) = eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))),
introduced(tautology,[refl,[$fot(eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))))]]) ).
cnf(refute_0_79,plain,
( cons(s(X_120),union(nil,cons(z,nil))) != cons(s(X_120),cons(z,nil))
| eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))) != eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil))))
| eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))) = eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil)))) ),
introduced(tautology,[equality,[$cnf( $equal(eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))),eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil))))) ),[1,0],$fot(cons(s(X_120),cons(z,nil)))]]) ).
cnf(refute_0_80,plain,
( cons(s(X_120),union(nil,cons(z,nil))) != cons(s(X_120),cons(z,nil))
| eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))) = eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil)))) ),
inference(resolve,[$cnf( $equal(eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))),eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil))))) )],[refute_0_78,refute_0_79]) ).
cnf(refute_0_81,plain,
eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))) = eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil)))),
inference(resolve,[$cnf( $equal(cons(s(X_120),union(nil,cons(z,nil))),cons(s(X_120),cons(z,nil))) )],[refute_0_77,refute_0_80]) ).
cnf(refute_0_82,plain,
( eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil)))) != eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil)))
| eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))) != eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil))))
| eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))) = eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil))) ),
inference(subst,[],[refute_0_26:[bind(X0,$fot(eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))))),bind(Y0,$fot(eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil)))))),bind(Z0,$fot(eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil)))))]]) ).
cnf(refute_0_83,plain,
( eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil)))) != eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil)))
| eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))) = eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil))) ),
inference(resolve,[$cnf( $equal(eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))),eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil))))) )],[refute_0_81,refute_0_82]) ).
cnf(refute_0_84,plain,
eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))) = eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil))),
inference(resolve,[$cnf( $equal(eq(cons(s(X_120),cons(z,nil)),cons(z,union(nil,cons(s(X_120),nil)))),eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil)))) )],[refute_0_72,refute_0_83]) ).
cnf(refute_0_85,plain,
( eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))) != eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil)))
| prop_union_comm(cons(s(X_120),nil),cons(z,nil)) != eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil))))
| prop_union_comm(cons(s(X_120),nil),cons(z,nil)) = eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil))) ),
introduced(tautology,[equality,[$cnf( $equal(prop_union_comm(cons(s(X_120),nil),cons(z,nil)),eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil))))) ),[1],$fot(eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil))))]]) ).
cnf(refute_0_86,plain,
( prop_union_comm(cons(s(X_120),nil),cons(z,nil)) != eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil))))
| prop_union_comm(cons(s(X_120),nil),cons(z,nil)) = eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil))) ),
inference(resolve,[$cnf( $equal(eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil)))),eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil)))) )],[refute_0_84,refute_0_85]) ).
cnf(refute_0_87,plain,
prop_union_comm(cons(s(X_120),nil),cons(z,nil)) = eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil))),
inference(resolve,[$cnf( $equal(prop_union_comm(cons(s(X_120),nil),cons(z,nil)),eq(cons(s(X_120),union(nil,cons(z,nil))),cons(z,union(nil,cons(s(X_120),nil))))) )],[refute_0_63,refute_0_86]) ).
cnf(refute_0_88,plain,
( eq2(s(X),z) != bfalse
| eq(cons(s(X),X_356),cons(z,X_355)) = bfalse ),
inference(subst,[],[axiom_021:[bind(X,$fot(s(X))),bind(X2,$fot(X_355)),bind(Y,$fot(X_356)),bind(Z,$fot(z))]]) ).
cnf(refute_0_89,plain,
( bfalse != bfalse
| eq2(s(X),z) != bfalse
| eq2(s(X),z) = bfalse ),
introduced(tautology,[equality,[$cnf( $equal(eq2(s(X),z),bfalse) ),[1],$fot(bfalse)]]) ).
cnf(refute_0_90,plain,
( bfalse != bfalse
| eq2(s(X),z) = bfalse ),
inference(resolve,[$cnf( $equal(eq2(s(X),z),bfalse) )],[axiom_016,refute_0_89]) ).
cnf(refute_0_91,plain,
( bfalse != bfalse
| eq(cons(s(X),X_356),cons(z,X_355)) = bfalse ),
inference(resolve,[$cnf( $equal(eq2(s(X),z),bfalse) )],[refute_0_90,refute_0_88]) ).
cnf(refute_0_92,plain,
bfalse = bfalse,
introduced(tautology,[refl,[$fot(bfalse)]]) ).
cnf(refute_0_93,plain,
eq(cons(s(X),X_356),cons(z,X_355)) = bfalse,
inference(resolve,[$cnf( $equal(bfalse,bfalse) )],[refute_0_92,refute_0_91]) ).
cnf(refute_0_94,plain,
eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil))) = bfalse,
inference(subst,[],[refute_0_93:[bind(X,$fot(X_120)),bind(X_355,$fot(cons(s(X_120),nil))),bind(X_356,$fot(cons(z,nil)))]]) ).
cnf(refute_0_95,plain,
( eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil))) != bfalse
| prop_union_comm(cons(s(X_120),nil),cons(z,nil)) != eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil)))
| prop_union_comm(cons(s(X_120),nil),cons(z,nil)) = bfalse ),
introduced(tautology,[equality,[$cnf( $equal(prop_union_comm(cons(s(X_120),nil),cons(z,nil)),eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil)))) ),[1],$fot(bfalse)]]) ).
cnf(refute_0_96,plain,
( prop_union_comm(cons(s(X_120),nil),cons(z,nil)) != eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil)))
| prop_union_comm(cons(s(X_120),nil),cons(z,nil)) = bfalse ),
inference(resolve,[$cnf( $equal(eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil))),bfalse) )],[refute_0_94,refute_0_95]) ).
cnf(refute_0_97,plain,
prop_union_comm(cons(s(X_120),nil),cons(z,nil)) = bfalse,
inference(resolve,[$cnf( $equal(prop_union_comm(cons(s(X_120),nil),cons(z,nil)),eq(cons(s(X_120),cons(z,nil)),cons(z,cons(s(X_120),nil)))) )],[refute_0_87,refute_0_96]) ).
cnf(refute_0_98,plain,
prop_union_comm(cons(s(X_358),nil),cons(z,nil)) = bfalse,
inference(subst,[],[refute_0_97:[bind(X_120,$fot(X_358))]]) ).
cnf(refute_0_99,plain,
( eq3(bfalse,bfalse) != btrue
| prop_union_comm(cons(s(X_358),nil),cons(z,nil)) != bfalse
| eq3(prop_union_comm(cons(s(X_358),nil),cons(z,nil)),bfalse) = btrue ),
introduced(tautology,[equality,[$cnf( ~ $equal(eq3(prop_union_comm(cons(s(X_358),nil),cons(z,nil)),bfalse),btrue) ),[0,0],$fot(bfalse)]]) ).
cnf(refute_0_100,plain,
( eq3(bfalse,bfalse) != btrue
| eq3(prop_union_comm(cons(s(X_358),nil),cons(z,nil)),bfalse) = btrue ),
inference(resolve,[$cnf( $equal(prop_union_comm(cons(s(X_358),nil),cons(z,nil)),bfalse) )],[refute_0_98,refute_0_99]) ).
cnf(refute_0_101,plain,
eq3(bfalse,bfalse) != btrue,
inference(resolve,[$cnf( $equal(eq3(prop_union_comm(cons(s(X_358),nil),cons(z,nil)),bfalse),btrue) )],[refute_0_100,refute_0_0]) ).
cnf(refute_0_102,plain,
eq3(bfalse,bfalse) = btrue,
inference(subst,[],[axiom_020:[bind(X,$fot(bfalse))]]) ).
cnf(refute_0_103,plain,
( btrue != btrue
| eq3(bfalse,bfalse) != btrue
| eq3(bfalse,bfalse) = btrue ),
introduced(tautology,[equality,[$cnf( $equal(eq3(bfalse,bfalse),btrue) ),[1],$fot(btrue)]]) ).
cnf(refute_0_104,plain,
( btrue != btrue
| eq3(bfalse,bfalse) = btrue ),
inference(resolve,[$cnf( $equal(eq3(bfalse,bfalse),btrue) )],[refute_0_102,refute_0_103]) ).
cnf(refute_0_105,plain,
btrue != btrue,
inference(resolve,[$cnf( $equal(eq3(bfalse,bfalse),btrue) )],[refute_0_104,refute_0_101]) ).
cnf(refute_0_106,plain,
btrue = btrue,
introduced(tautology,[refl,[$fot(btrue)]]) ).
cnf(refute_0_107,plain,
$false,
inference(resolve,[$cnf( $equal(btrue,btrue) )],[refute_0_106,refute_0_105]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX228-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.12 % Command : metis --show proof --show saturation %s
% 0.15/0.33 % Computer : n010.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 12:55:36 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.54/0.76 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.54/0.76
% 0.54/0.76 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.54/0.78
%------------------------------------------------------------------------------