%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SWX185+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n004.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:29 PM UTC 2026
% Result : Theorem 43.87s 44.05s
% Output : CNFRefutation 43.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 47
% Syntax : Number of formulae : 204 ( 111 unt; 0 def)
% Number of atoms : 339 ( 338 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 272 ( 137 ~; 130 |; 0 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-2 aty)
% Number of variables : 328 ( 39 sgn 55 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_021,axiom,
! [X,X2] : proj12(x2(X,X2)) = X ).
fof(axiom_022,axiom,
! [X,X2] : proj22(x2(X,X2)) = X2 ).
fof(axiom_025,axiom,
! [X,X2] : z(X,X2) != eY ).
fof(axiom_027,axiom,
! [X,X2] : x2(X,X2) != eY ).
fof(axiom_029,axiom,
! [X] :
( X != z(proj1(X),proj2(X))
=> ( X != x2(proj12(X),proj22(X))
=> assoc(X) = X ) ) ).
fof(axiom_032,axiom,
! [A2,B2] : assoc(x2(A2,B2)) = x2(assoc(A2),assoc(B2)) ).
fof(axiom_033,axiom,
! [Y] : append(nil,Y) = Y ).
fof(axiom_034,axiom,
! [Y,Z,Xs] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) ).
fof(axiom_038,axiom,
! [A3,B2] : lin(x2(A3,B2)) = append(lin(A3),append(cons(mul,nil),lin(B2))) ).
fof(axiom_039,axiom,
lin(eX) = cons(x,nil) ).
fof(goal_041,conjecture,
? [U,V] :
~ ( lin(U) = lin(V)
=> assoc(U) = assoc(V) ) ).
fof(subgoal_0,plain,
? [U,V] :
~ ( lin(U) = lin(V)
=> assoc(U) = assoc(V) ),
inference(strip,[],[goal_041]) ).
fof(negate_0_0,plain,
~ ? [U,V] :
~ ( lin(U) = lin(V)
=> assoc(U) = assoc(V) ),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
! [X,X2] : z(X,X2) != eY,
inference(canonicalize,[],[axiom_025]) ).
fof(normalize_0_1,plain,
! [X,X2] : z(X,X2) != eY,
inference(specialize,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
! [X] :
( X = x2(proj12(X),proj22(X))
| X = z(proj1(X),proj2(X))
| assoc(X) = X ),
inference(canonicalize,[],[axiom_029]) ).
fof(normalize_0_3,plain,
! [X] :
( X = x2(proj12(X),proj22(X))
| X = z(proj1(X),proj2(X))
| assoc(X) = X ),
inference(specialize,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
! [X,X2] : proj22(x2(X,X2)) = X2,
inference(canonicalize,[],[axiom_022]) ).
fof(normalize_0_5,plain,
! [X,X2] : proj22(x2(X,X2)) = X2,
inference(specialize,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
! [A2,B2] : assoc(x2(A2,B2)) = x2(assoc(A2),assoc(B2)),
inference(canonicalize,[],[axiom_032]) ).
fof(normalize_0_7,plain,
! [A2,B2] : assoc(x2(A2,B2)) = x2(assoc(A2),assoc(B2)),
inference(specialize,[],[normalize_0_6]) ).
fof(normalize_0_8,plain,
! [U,V] :
( lin(U) != lin(V)
| assoc(U) = assoc(V) ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_9,plain,
! [U,V] :
( lin(U) != lin(V)
| assoc(U) = assoc(V) ),
inference(specialize,[],[normalize_0_8]) ).
fof(normalize_0_10,plain,
! [Xs,Y,Z] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)),
inference(canonicalize,[],[axiom_034]) ).
fof(normalize_0_11,plain,
! [Xs,Y,Z] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)),
inference(specialize,[],[normalize_0_10]) ).
fof(normalize_0_12,plain,
! [A3,B2] : lin(x2(A3,B2)) = append(lin(A3),append(cons(mul,nil),lin(B2))),
inference(canonicalize,[],[axiom_038]) ).
fof(normalize_0_13,plain,
! [A3,B2] : lin(x2(A3,B2)) = append(lin(A3),append(cons(mul,nil),lin(B2))),
inference(specialize,[],[normalize_0_12]) ).
fof(normalize_0_14,plain,
! [Y] : append(nil,Y) = Y,
inference(canonicalize,[],[axiom_033]) ).
fof(normalize_0_15,plain,
! [Y] : append(nil,Y) = Y,
inference(specialize,[],[normalize_0_14]) ).
fof(normalize_0_16,plain,
lin(eX) = cons(x,nil),
inference(canonicalize,[],[axiom_039]) ).
fof(normalize_0_17,plain,
! [X,X2] : proj12(x2(X,X2)) = X,
inference(canonicalize,[],[axiom_021]) ).
fof(normalize_0_18,plain,
! [X,X2] : proj12(x2(X,X2)) = X,
inference(specialize,[],[normalize_0_17]) ).
fof(normalize_0_19,plain,
! [X,X2] : x2(X,X2) != eY,
inference(canonicalize,[],[axiom_027]) ).
fof(normalize_0_20,plain,
! [X,X2] : x2(X,X2) != eY,
inference(specialize,[],[normalize_0_19]) ).
cnf(refute_0_0,plain,
z(X,X2) != eY,
inference(canonicalize,[],[normalize_0_1]) ).
cnf(refute_0_1,plain,
z(proj1(X_662),proj2(X_662)) != eY,
inference(subst,[],[refute_0_0:[bind(X,$fot(proj1(X_662))),bind(X2,$fot(proj2(X_662)))]]) ).
cnf(refute_0_2,plain,
( X = x2(proj12(X),proj22(X))
| X = z(proj1(X),proj2(X))
| assoc(X) = X ),
inference(canonicalize,[],[normalize_0_3]) ).
cnf(refute_0_3,plain,
( X_662 = x2(proj12(X_662),proj22(X_662))
| X_662 = z(proj1(X_662),proj2(X_662))
| assoc(X_662) = X_662 ),
inference(subst,[],[refute_0_2:[bind(X,$fot(X_662))]]) ).
cnf(refute_0_4,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_5,plain,
( X0 != X0
| X0 != Y0
| Y0 = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).
cnf(refute_0_6,plain,
( X0 != Y0
| Y0 = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_4,refute_0_5]) ).
cnf(refute_0_7,plain,
( X_662 != z(proj1(X_662),proj2(X_662))
| z(proj1(X_662),proj2(X_662)) = X_662 ),
inference(subst,[],[refute_0_6:[bind(X0,$fot(X_662)),bind(Y0,$fot(z(proj1(X_662),proj2(X_662))))]]) ).
cnf(refute_0_8,plain,
( X_662 = x2(proj12(X_662),proj22(X_662))
| assoc(X_662) = X_662
| z(proj1(X_662),proj2(X_662)) = X_662 ),
inference(resolve,[$cnf( $equal(X_662,z(proj1(X_662),proj2(X_662))) )],[refute_0_3,refute_0_7]) ).
cnf(refute_0_9,plain,
( X_662 != eY
| z(proj1(X_662),proj2(X_662)) != X_662
| z(proj1(X_662),proj2(X_662)) = eY ),
introduced(tautology,[equality,[$cnf( $equal(z(proj1(X_662),proj2(X_662)),X_662) ),[1],$fot(eY)]]) ).
cnf(refute_0_10,plain,
( X_662 != eY
| X_662 = x2(proj12(X_662),proj22(X_662))
| assoc(X_662) = X_662
| z(proj1(X_662),proj2(X_662)) = eY ),
inference(resolve,[$cnf( $equal(z(proj1(X_662),proj2(X_662)),X_662) )],[refute_0_8,refute_0_9]) ).
cnf(refute_0_11,plain,
( X_662 != eY
| X_662 = x2(proj12(X_662),proj22(X_662))
| assoc(X_662) = X_662 ),
inference(resolve,[$cnf( $equal(z(proj1(X_662),proj2(X_662)),eY) )],[refute_0_10,refute_0_1]) ).
cnf(refute_0_12,plain,
( eY != eY
| assoc(eY) = eY
| eY = x2(proj12(eY),proj22(eY)) ),
inference(subst,[],[refute_0_11:[bind(X_662,$fot(eY))]]) ).
cnf(refute_0_13,plain,
eY = eY,
introduced(tautology,[refl,[$fot(eY)]]) ).
cnf(refute_0_14,plain,
( assoc(eY) = eY
| eY = x2(proj12(eY),proj22(eY)) ),
inference(resolve,[$cnf( $equal(eY,eY) )],[refute_0_13,refute_0_12]) ).
cnf(refute_0_15,plain,
proj22(x2(X,X2)) = X2,
inference(canonicalize,[],[normalize_0_5]) ).
cnf(refute_0_16,plain,
proj22(x2(assoc(X_21),assoc(X_22))) = assoc(X_22),
inference(subst,[],[refute_0_15:[bind(X,$fot(assoc(X_21))),bind(X2,$fot(assoc(X_22)))]]) ).
cnf(refute_0_17,plain,
assoc(x2(A2,B2)) = x2(assoc(A2),assoc(B2)),
inference(canonicalize,[],[normalize_0_7]) ).
cnf(refute_0_18,plain,
assoc(x2(X_21,X_22)) = x2(assoc(X_21),assoc(X_22)),
inference(subst,[],[refute_0_17:[bind(A2,$fot(X_21)),bind(B2,$fot(X_22))]]) ).
cnf(refute_0_19,plain,
( assoc(x2(X_21,X_22)) != x2(assoc(X_21),assoc(X_22))
| x2(assoc(X_21),assoc(X_22)) = assoc(x2(X_21,X_22)) ),
inference(subst,[],[refute_0_6:[bind(X0,$fot(assoc(x2(X_21,X_22)))),bind(Y0,$fot(x2(assoc(X_21),assoc(X_22))))]]) ).
cnf(refute_0_20,plain,
x2(assoc(X_21),assoc(X_22)) = assoc(x2(X_21,X_22)),
inference(resolve,[$cnf( $equal(assoc(x2(X_21,X_22)),x2(assoc(X_21),assoc(X_22))) )],[refute_0_18,refute_0_19]) ).
cnf(refute_0_21,plain,
( proj22(x2(assoc(X_21),assoc(X_22))) != assoc(X_22)
| x2(assoc(X_21),assoc(X_22)) != assoc(x2(X_21,X_22))
| proj22(assoc(x2(X_21,X_22))) = assoc(X_22) ),
introduced(tautology,[equality,[$cnf( $equal(proj22(x2(assoc(X_21),assoc(X_22))),assoc(X_22)) ),[0,0],$fot(assoc(x2(X_21,X_22)))]]) ).
cnf(refute_0_22,plain,
( proj22(x2(assoc(X_21),assoc(X_22))) != assoc(X_22)
| proj22(assoc(x2(X_21,X_22))) = assoc(X_22) ),
inference(resolve,[$cnf( $equal(x2(assoc(X_21),assoc(X_22)),assoc(x2(X_21,X_22))) )],[refute_0_20,refute_0_21]) ).
cnf(refute_0_23,plain,
proj22(assoc(x2(X_21,X_22))) = assoc(X_22),
inference(resolve,[$cnf( $equal(proj22(x2(assoc(X_21),assoc(X_22))),assoc(X_22)) )],[refute_0_16,refute_0_22]) ).
cnf(refute_0_24,plain,
proj22(assoc(x2(x2(eX,X_349),X_22))) = assoc(X_22),
inference(subst,[],[refute_0_23:[bind(X_21,$fot(x2(eX,X_349)))]]) ).
cnf(refute_0_25,plain,
( lin(U) != lin(V)
| assoc(U) = assoc(V) ),
inference(canonicalize,[],[normalize_0_9]) ).
cnf(refute_0_26,plain,
( lin(U) != lin(x2(x2(eX,X_347),X_346))
| assoc(U) = assoc(x2(x2(eX,X_347),X_346)) ),
inference(subst,[],[refute_0_25:[bind(V,$fot(x2(x2(eX,X_347),X_346)))]]) ).
cnf(refute_0_27,plain,
append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)),
inference(canonicalize,[],[normalize_0_11]) ).
cnf(refute_0_28,plain,
append(cons(x,cons(mul,lin(X_98))),Y) = cons(x,append(cons(mul,lin(X_98)),Y)),
inference(subst,[],[refute_0_27:[bind(Xs,$fot(cons(mul,lin(X_98)))),bind(Z,$fot(x))]]) ).
cnf(refute_0_29,plain,
lin(x2(A3,B2)) = append(lin(A3),append(cons(mul,nil),lin(B2))),
inference(canonicalize,[],[normalize_0_13]) ).
cnf(refute_0_30,plain,
append(nil,Y) = Y,
inference(canonicalize,[],[normalize_0_15]) ).
cnf(refute_0_31,plain,
append(nil,lin(B2)) = lin(B2),
inference(subst,[],[refute_0_30:[bind(Y,$fot(lin(B2)))]]) ).
cnf(refute_0_32,plain,
cons(mul,append(nil,lin(B2))) = cons(mul,append(nil,lin(B2))),
introduced(tautology,[refl,[$fot(cons(mul,append(nil,lin(B2))))]]) ).
cnf(refute_0_33,plain,
( cons(mul,append(nil,lin(B2))) != cons(mul,append(nil,lin(B2)))
| append(nil,lin(B2)) != lin(B2)
| cons(mul,append(nil,lin(B2))) = cons(mul,lin(B2)) ),
introduced(tautology,[equality,[$cnf( $equal(cons(mul,append(nil,lin(B2))),cons(mul,append(nil,lin(B2)))) ),[1,1],$fot(lin(B2))]]) ).
cnf(refute_0_34,plain,
( append(nil,lin(B2)) != lin(B2)
| cons(mul,append(nil,lin(B2))) = cons(mul,lin(B2)) ),
inference(resolve,[$cnf( $equal(cons(mul,append(nil,lin(B2))),cons(mul,append(nil,lin(B2)))) )],[refute_0_32,refute_0_33]) ).
cnf(refute_0_35,plain,
cons(mul,append(nil,lin(B2))) = cons(mul,lin(B2)),
inference(resolve,[$cnf( $equal(append(nil,lin(B2)),lin(B2)) )],[refute_0_31,refute_0_34]) ).
cnf(refute_0_36,plain,
append(cons(mul,nil),lin(B2)) = cons(mul,append(nil,lin(B2))),
inference(subst,[],[refute_0_27:[bind(Xs,$fot(nil)),bind(Y,$fot(lin(B2))),bind(Z,$fot(mul))]]) ).
cnf(refute_0_37,plain,
( Y0 != X0
| Y0 != Z0
| X0 = Z0 ),
introduced(tautology,[equality,[$cnf( $equal(Y0,Z0) ),[0],$fot(X0)]]) ).
cnf(refute_0_38,plain,
( X0 != Y0
| Y0 != Z0
| X0 = Z0 ),
inference(resolve,[$cnf( $equal(Y0,X0) )],[refute_0_6,refute_0_37]) ).
cnf(refute_0_39,plain,
( cons(mul,append(nil,lin(B2))) != cons(mul,lin(B2))
| append(cons(mul,nil),lin(B2)) != cons(mul,append(nil,lin(B2)))
| append(cons(mul,nil),lin(B2)) = cons(mul,lin(B2)) ),
inference(subst,[],[refute_0_38:[bind(X0,$fot(append(cons(mul,nil),lin(B2)))),bind(Y0,$fot(cons(mul,append(nil,lin(B2))))),bind(Z0,$fot(cons(mul,lin(B2))))]]) ).
cnf(refute_0_40,plain,
( cons(mul,append(nil,lin(B2))) != cons(mul,lin(B2))
| append(cons(mul,nil),lin(B2)) = cons(mul,lin(B2)) ),
inference(resolve,[$cnf( $equal(append(cons(mul,nil),lin(B2)),cons(mul,append(nil,lin(B2)))) )],[refute_0_36,refute_0_39]) ).
cnf(refute_0_41,plain,
append(cons(mul,nil),lin(B2)) = cons(mul,lin(B2)),
inference(resolve,[$cnf( $equal(cons(mul,append(nil,lin(B2))),cons(mul,lin(B2))) )],[refute_0_35,refute_0_40]) ).
cnf(refute_0_42,plain,
append(lin(A3),append(cons(mul,nil),lin(B2))) = append(lin(A3),append(cons(mul,nil),lin(B2))),
introduced(tautology,[refl,[$fot(append(lin(A3),append(cons(mul,nil),lin(B2))))]]) ).
cnf(refute_0_43,plain,
( append(cons(mul,nil),lin(B2)) != cons(mul,lin(B2))
| append(lin(A3),append(cons(mul,nil),lin(B2))) != append(lin(A3),append(cons(mul,nil),lin(B2)))
| append(lin(A3),append(cons(mul,nil),lin(B2))) = append(lin(A3),cons(mul,lin(B2))) ),
introduced(tautology,[equality,[$cnf( $equal(append(lin(A3),append(cons(mul,nil),lin(B2))),append(lin(A3),append(cons(mul,nil),lin(B2)))) ),[1,1],$fot(cons(mul,lin(B2)))]]) ).
cnf(refute_0_44,plain,
( append(cons(mul,nil),lin(B2)) != cons(mul,lin(B2))
| append(lin(A3),append(cons(mul,nil),lin(B2))) = append(lin(A3),cons(mul,lin(B2))) ),
inference(resolve,[$cnf( $equal(append(lin(A3),append(cons(mul,nil),lin(B2))),append(lin(A3),append(cons(mul,nil),lin(B2)))) )],[refute_0_42,refute_0_43]) ).
cnf(refute_0_45,plain,
append(lin(A3),append(cons(mul,nil),lin(B2))) = append(lin(A3),cons(mul,lin(B2))),
inference(resolve,[$cnf( $equal(append(cons(mul,nil),lin(B2)),cons(mul,lin(B2))) )],[refute_0_41,refute_0_44]) ).
cnf(refute_0_46,plain,
( append(lin(A3),append(cons(mul,nil),lin(B2))) != append(lin(A3),cons(mul,lin(B2)))
| lin(x2(A3,B2)) != append(lin(A3),append(cons(mul,nil),lin(B2)))
| lin(x2(A3,B2)) = append(lin(A3),cons(mul,lin(B2))) ),
introduced(tautology,[equality,[$cnf( $equal(lin(x2(A3,B2)),append(lin(A3),append(cons(mul,nil),lin(B2)))) ),[1],$fot(append(lin(A3),cons(mul,lin(B2))))]]) ).
cnf(refute_0_47,plain,
( lin(x2(A3,B2)) != append(lin(A3),append(cons(mul,nil),lin(B2)))
| lin(x2(A3,B2)) = append(lin(A3),cons(mul,lin(B2))) ),
inference(resolve,[$cnf( $equal(append(lin(A3),append(cons(mul,nil),lin(B2))),append(lin(A3),cons(mul,lin(B2)))) )],[refute_0_45,refute_0_46]) ).
cnf(refute_0_48,plain,
lin(x2(A3,B2)) = append(lin(A3),cons(mul,lin(B2))),
inference(resolve,[$cnf( $equal(lin(x2(A3,B2)),append(lin(A3),append(cons(mul,nil),lin(B2)))) )],[refute_0_29,refute_0_47]) ).
cnf(refute_0_49,plain,
lin(x2(eX,B2)) = append(lin(eX),cons(mul,lin(B2))),
inference(subst,[],[refute_0_48:[bind(A3,$fot(eX))]]) ).
cnf(refute_0_50,plain,
append(cons(x,nil),X_87) = cons(x,append(nil,X_87)),
inference(subst,[],[refute_0_27:[bind(Xs,$fot(nil)),bind(Y,$fot(X_87)),bind(Z,$fot(x))]]) ).
cnf(refute_0_51,plain,
lin(eX) = cons(x,nil),
inference(canonicalize,[],[normalize_0_16]) ).
cnf(refute_0_52,plain,
( lin(eX) != cons(x,nil)
| cons(x,nil) = lin(eX) ),
inference(subst,[],[refute_0_6:[bind(X0,$fot(lin(eX))),bind(Y0,$fot(cons(x,nil)))]]) ).
cnf(refute_0_53,plain,
cons(x,nil) = lin(eX),
inference(resolve,[$cnf( $equal(lin(eX),cons(x,nil)) )],[refute_0_51,refute_0_52]) ).
cnf(refute_0_54,plain,
( cons(x,nil) != lin(eX)
| append(cons(x,nil),X_87) != cons(x,append(nil,X_87))
| append(lin(eX),X_87) = cons(x,append(nil,X_87)) ),
introduced(tautology,[equality,[$cnf( $equal(append(cons(x,nil),X_87),cons(x,append(nil,X_87))) ),[0,0],$fot(lin(eX))]]) ).
cnf(refute_0_55,plain,
( append(cons(x,nil),X_87) != cons(x,append(nil,X_87))
| append(lin(eX),X_87) = cons(x,append(nil,X_87)) ),
inference(resolve,[$cnf( $equal(cons(x,nil),lin(eX)) )],[refute_0_53,refute_0_54]) ).
cnf(refute_0_56,plain,
append(lin(eX),X_87) = cons(x,append(nil,X_87)),
inference(resolve,[$cnf( $equal(append(cons(x,nil),X_87),cons(x,append(nil,X_87))) )],[refute_0_50,refute_0_55]) ).
cnf(refute_0_57,plain,
append(nil,X_87) = X_87,
inference(subst,[],[refute_0_30:[bind(Y,$fot(X_87))]]) ).
cnf(refute_0_58,plain,
cons(x,append(nil,X_87)) = cons(x,append(nil,X_87)),
introduced(tautology,[refl,[$fot(cons(x,append(nil,X_87)))]]) ).
cnf(refute_0_59,plain,
( cons(x,append(nil,X_87)) != cons(x,append(nil,X_87))
| append(nil,X_87) != X_87
| cons(x,append(nil,X_87)) = cons(x,X_87) ),
introduced(tautology,[equality,[$cnf( $equal(cons(x,append(nil,X_87)),cons(x,append(nil,X_87))) ),[1,1],$fot(X_87)]]) ).
cnf(refute_0_60,plain,
( append(nil,X_87) != X_87
| cons(x,append(nil,X_87)) = cons(x,X_87) ),
inference(resolve,[$cnf( $equal(cons(x,append(nil,X_87)),cons(x,append(nil,X_87))) )],[refute_0_58,refute_0_59]) ).
cnf(refute_0_61,plain,
cons(x,append(nil,X_87)) = cons(x,X_87),
inference(resolve,[$cnf( $equal(append(nil,X_87),X_87) )],[refute_0_57,refute_0_60]) ).
cnf(refute_0_62,plain,
( cons(x,append(nil,X_87)) != cons(x,X_87)
| append(lin(eX),X_87) != cons(x,append(nil,X_87))
| append(lin(eX),X_87) = cons(x,X_87) ),
introduced(tautology,[equality,[$cnf( $equal(append(lin(eX),X_87),cons(x,append(nil,X_87))) ),[1],$fot(cons(x,X_87))]]) ).
cnf(refute_0_63,plain,
( append(lin(eX),X_87) != cons(x,append(nil,X_87))
| append(lin(eX),X_87) = cons(x,X_87) ),
inference(resolve,[$cnf( $equal(cons(x,append(nil,X_87)),cons(x,X_87)) )],[refute_0_61,refute_0_62]) ).
cnf(refute_0_64,plain,
append(lin(eX),X_87) = cons(x,X_87),
inference(resolve,[$cnf( $equal(append(lin(eX),X_87),cons(x,append(nil,X_87))) )],[refute_0_56,refute_0_63]) ).
cnf(refute_0_65,plain,
append(lin(eX),cons(mul,lin(B2))) = cons(x,cons(mul,lin(B2))),
inference(subst,[],[refute_0_64:[bind(X_87,$fot(cons(mul,lin(B2))))]]) ).
cnf(refute_0_66,plain,
( append(lin(eX),cons(mul,lin(B2))) != cons(x,cons(mul,lin(B2)))
| lin(x2(eX,B2)) != append(lin(eX),cons(mul,lin(B2)))
| lin(x2(eX,B2)) = cons(x,cons(mul,lin(B2))) ),
introduced(tautology,[equality,[$cnf( $equal(lin(x2(eX,B2)),append(lin(eX),cons(mul,lin(B2)))) ),[1],$fot(cons(x,cons(mul,lin(B2))))]]) ).
cnf(refute_0_67,plain,
( lin(x2(eX,B2)) != append(lin(eX),cons(mul,lin(B2)))
| lin(x2(eX,B2)) = cons(x,cons(mul,lin(B2))) ),
inference(resolve,[$cnf( $equal(append(lin(eX),cons(mul,lin(B2))),cons(x,cons(mul,lin(B2)))) )],[refute_0_65,refute_0_66]) ).
cnf(refute_0_68,plain,
lin(x2(eX,B2)) = cons(x,cons(mul,lin(B2))),
inference(resolve,[$cnf( $equal(lin(x2(eX,B2)),append(lin(eX),cons(mul,lin(B2)))) )],[refute_0_49,refute_0_67]) ).
cnf(refute_0_69,plain,
lin(x2(eX,X_98)) = cons(x,cons(mul,lin(X_98))),
inference(subst,[],[refute_0_68:[bind(B2,$fot(X_98))]]) ).
cnf(refute_0_70,plain,
( lin(x2(eX,X_98)) != cons(x,cons(mul,lin(X_98)))
| cons(x,cons(mul,lin(X_98))) = lin(x2(eX,X_98)) ),
inference(subst,[],[refute_0_6:[bind(X0,$fot(lin(x2(eX,X_98)))),bind(Y0,$fot(cons(x,cons(mul,lin(X_98)))))]]) ).
cnf(refute_0_71,plain,
cons(x,cons(mul,lin(X_98))) = lin(x2(eX,X_98)),
inference(resolve,[$cnf( $equal(lin(x2(eX,X_98)),cons(x,cons(mul,lin(X_98)))) )],[refute_0_69,refute_0_70]) ).
cnf(refute_0_72,plain,
( cons(x,cons(mul,lin(X_98))) != lin(x2(eX,X_98))
| append(cons(x,cons(mul,lin(X_98))),Y) != cons(x,append(cons(mul,lin(X_98)),Y))
| append(lin(x2(eX,X_98)),Y) = cons(x,append(cons(mul,lin(X_98)),Y)) ),
introduced(tautology,[equality,[$cnf( $equal(append(cons(x,cons(mul,lin(X_98))),Y),cons(x,append(cons(mul,lin(X_98)),Y))) ),[0,0],$fot(lin(x2(eX,X_98)))]]) ).
cnf(refute_0_73,plain,
( append(cons(x,cons(mul,lin(X_98))),Y) != cons(x,append(cons(mul,lin(X_98)),Y))
| append(lin(x2(eX,X_98)),Y) = cons(x,append(cons(mul,lin(X_98)),Y)) ),
inference(resolve,[$cnf( $equal(cons(x,cons(mul,lin(X_98))),lin(x2(eX,X_98))) )],[refute_0_71,refute_0_72]) ).
cnf(refute_0_74,plain,
append(lin(x2(eX,X_98)),Y) = cons(x,append(cons(mul,lin(X_98)),Y)),
inference(resolve,[$cnf( $equal(append(cons(x,cons(mul,lin(X_98))),Y),cons(x,append(cons(mul,lin(X_98)),Y))) )],[refute_0_28,refute_0_73]) ).
cnf(refute_0_75,plain,
append(cons(mul,lin(X_98)),Y) = cons(mul,append(lin(X_98),Y)),
inference(subst,[],[refute_0_27:[bind(Xs,$fot(lin(X_98))),bind(Z,$fot(mul))]]) ).
cnf(refute_0_76,plain,
cons(x,append(cons(mul,lin(X_98)),Y)) = cons(x,append(cons(mul,lin(X_98)),Y)),
introduced(tautology,[refl,[$fot(cons(x,append(cons(mul,lin(X_98)),Y)))]]) ).
cnf(refute_0_77,plain,
( cons(x,append(cons(mul,lin(X_98)),Y)) != cons(x,append(cons(mul,lin(X_98)),Y))
| append(cons(mul,lin(X_98)),Y) != cons(mul,append(lin(X_98),Y))
| cons(x,append(cons(mul,lin(X_98)),Y)) = cons(x,cons(mul,append(lin(X_98),Y))) ),
introduced(tautology,[equality,[$cnf( $equal(cons(x,append(cons(mul,lin(X_98)),Y)),cons(x,append(cons(mul,lin(X_98)),Y))) ),[1,1],$fot(cons(mul,append(lin(X_98),Y)))]]) ).
cnf(refute_0_78,plain,
( append(cons(mul,lin(X_98)),Y) != cons(mul,append(lin(X_98),Y))
| cons(x,append(cons(mul,lin(X_98)),Y)) = cons(x,cons(mul,append(lin(X_98),Y))) ),
inference(resolve,[$cnf( $equal(cons(x,append(cons(mul,lin(X_98)),Y)),cons(x,append(cons(mul,lin(X_98)),Y))) )],[refute_0_76,refute_0_77]) ).
cnf(refute_0_79,plain,
cons(x,append(cons(mul,lin(X_98)),Y)) = cons(x,cons(mul,append(lin(X_98),Y))),
inference(resolve,[$cnf( $equal(append(cons(mul,lin(X_98)),Y),cons(mul,append(lin(X_98),Y))) )],[refute_0_75,refute_0_78]) ).
cnf(refute_0_80,plain,
( cons(x,append(cons(mul,lin(X_98)),Y)) != cons(x,cons(mul,append(lin(X_98),Y)))
| append(lin(x2(eX,X_98)),Y) != cons(x,append(cons(mul,lin(X_98)),Y))
| append(lin(x2(eX,X_98)),Y) = cons(x,cons(mul,append(lin(X_98),Y))) ),
introduced(tautology,[equality,[$cnf( $equal(append(lin(x2(eX,X_98)),Y),cons(x,append(cons(mul,lin(X_98)),Y))) ),[1],$fot(cons(x,cons(mul,append(lin(X_98),Y))))]]) ).
cnf(refute_0_81,plain,
( append(lin(x2(eX,X_98)),Y) != cons(x,append(cons(mul,lin(X_98)),Y))
| append(lin(x2(eX,X_98)),Y) = cons(x,cons(mul,append(lin(X_98),Y))) ),
inference(resolve,[$cnf( $equal(cons(x,append(cons(mul,lin(X_98)),Y)),cons(x,cons(mul,append(lin(X_98),Y)))) )],[refute_0_79,refute_0_80]) ).
cnf(refute_0_82,plain,
append(lin(x2(eX,X_98)),Y) = cons(x,cons(mul,append(lin(X_98),Y))),
inference(resolve,[$cnf( $equal(append(lin(x2(eX,X_98)),Y),cons(x,append(cons(mul,lin(X_98)),Y))) )],[refute_0_74,refute_0_81]) ).
cnf(refute_0_83,plain,
append(lin(x2(eX,X_169)),cons(mul,lin(B2))) = cons(x,cons(mul,append(lin(X_169),cons(mul,lin(B2))))),
inference(subst,[],[refute_0_82:[bind(Y,$fot(cons(mul,lin(B2)))),bind(X_98,$fot(X_169))]]) ).
cnf(refute_0_84,plain,
lin(x2(X_169,B2)) = append(lin(X_169),cons(mul,lin(B2))),
inference(subst,[],[refute_0_48:[bind(A3,$fot(X_169))]]) ).
cnf(refute_0_85,plain,
( lin(x2(X_169,B2)) != append(lin(X_169),cons(mul,lin(B2)))
| append(lin(X_169),cons(mul,lin(B2))) = lin(x2(X_169,B2)) ),
inference(subst,[],[refute_0_6:[bind(X0,$fot(lin(x2(X_169,B2)))),bind(Y0,$fot(append(lin(X_169),cons(mul,lin(B2)))))]]) ).
cnf(refute_0_86,plain,
append(lin(X_169),cons(mul,lin(B2))) = lin(x2(X_169,B2)),
inference(resolve,[$cnf( $equal(lin(x2(X_169,B2)),append(lin(X_169),cons(mul,lin(B2)))) )],[refute_0_84,refute_0_85]) ).
cnf(refute_0_87,plain,
( append(lin(X_169),cons(mul,lin(B2))) != lin(x2(X_169,B2))
| append(lin(x2(eX,X_169)),cons(mul,lin(B2))) != cons(x,cons(mul,append(lin(X_169),cons(mul,lin(B2)))))
| append(lin(x2(eX,X_169)),cons(mul,lin(B2))) = cons(x,cons(mul,lin(x2(X_169,B2)))) ),
introduced(tautology,[equality,[$cnf( $equal(append(lin(x2(eX,X_169)),cons(mul,lin(B2))),cons(x,cons(mul,append(lin(X_169),cons(mul,lin(B2)))))) ),[1,1,1],$fot(lin(x2(X_169,B2)))]]) ).
cnf(refute_0_88,plain,
( append(lin(x2(eX,X_169)),cons(mul,lin(B2))) != cons(x,cons(mul,append(lin(X_169),cons(mul,lin(B2)))))
| append(lin(x2(eX,X_169)),cons(mul,lin(B2))) = cons(x,cons(mul,lin(x2(X_169,B2)))) ),
inference(resolve,[$cnf( $equal(append(lin(X_169),cons(mul,lin(B2))),lin(x2(X_169,B2))) )],[refute_0_86,refute_0_87]) ).
cnf(refute_0_89,plain,
append(lin(x2(eX,X_169)),cons(mul,lin(B2))) = cons(x,cons(mul,lin(x2(X_169,B2)))),
inference(resolve,[$cnf( $equal(append(lin(x2(eX,X_169)),cons(mul,lin(B2))),cons(x,cons(mul,append(lin(X_169),cons(mul,lin(B2)))))) )],[refute_0_83,refute_0_88]) ).
cnf(refute_0_90,plain,
( lin(x2(A3,B2)) != append(lin(A3),cons(mul,lin(B2)))
| append(lin(A3),cons(mul,lin(B2))) = lin(x2(A3,B2)) ),
inference(subst,[],[refute_0_6:[bind(X0,$fot(lin(x2(A3,B2)))),bind(Y0,$fot(append(lin(A3),cons(mul,lin(B2)))))]]) ).
cnf(refute_0_91,plain,
append(lin(A3),cons(mul,lin(B2))) = lin(x2(A3,B2)),
inference(resolve,[$cnf( $equal(lin(x2(A3,B2)),append(lin(A3),cons(mul,lin(B2)))) )],[refute_0_48,refute_0_90]) ).
cnf(refute_0_92,plain,
append(lin(x2(eX,X_169)),cons(mul,lin(B2))) = lin(x2(x2(eX,X_169),B2)),
inference(subst,[],[refute_0_91:[bind(A3,$fot(x2(eX,X_169)))]]) ).
cnf(refute_0_93,plain,
( append(lin(x2(eX,X_169)),cons(mul,lin(B2))) != cons(x,cons(mul,lin(x2(X_169,B2))))
| append(lin(x2(eX,X_169)),cons(mul,lin(B2))) != lin(x2(x2(eX,X_169),B2))
| lin(x2(x2(eX,X_169),B2)) = cons(x,cons(mul,lin(x2(X_169,B2)))) ),
introduced(tautology,[equality,[$cnf( $equal(append(lin(x2(eX,X_169)),cons(mul,lin(B2))),cons(x,cons(mul,lin(x2(X_169,B2))))) ),[0],$fot(lin(x2(x2(eX,X_169),B2)))]]) ).
cnf(refute_0_94,plain,
( append(lin(x2(eX,X_169)),cons(mul,lin(B2))) != cons(x,cons(mul,lin(x2(X_169,B2))))
| lin(x2(x2(eX,X_169),B2)) = cons(x,cons(mul,lin(x2(X_169,B2)))) ),
inference(resolve,[$cnf( $equal(append(lin(x2(eX,X_169)),cons(mul,lin(B2))),lin(x2(x2(eX,X_169),B2))) )],[refute_0_92,refute_0_93]) ).
cnf(refute_0_95,plain,
( lin(x2(eX,B2)) != cons(x,cons(mul,lin(B2)))
| cons(x,cons(mul,lin(B2))) = lin(x2(eX,B2)) ),
inference(subst,[],[refute_0_6:[bind(X0,$fot(lin(x2(eX,B2)))),bind(Y0,$fot(cons(x,cons(mul,lin(B2)))))]]) ).
cnf(refute_0_96,plain,
cons(x,cons(mul,lin(B2))) = lin(x2(eX,B2)),
inference(resolve,[$cnf( $equal(lin(x2(eX,B2)),cons(x,cons(mul,lin(B2)))) )],[refute_0_68,refute_0_95]) ).
cnf(refute_0_97,plain,
cons(x,cons(mul,lin(x2(X_169,B2)))) = lin(x2(eX,x2(X_169,B2))),
inference(subst,[],[refute_0_96:[bind(B2,$fot(x2(X_169,B2)))]]) ).
cnf(refute_0_98,plain,
( cons(x,cons(mul,lin(x2(X_169,B2)))) != lin(x2(eX,x2(X_169,B2)))
| lin(x2(x2(eX,X_169),B2)) != cons(x,cons(mul,lin(x2(X_169,B2))))
| lin(x2(x2(eX,X_169),B2)) = lin(x2(eX,x2(X_169,B2))) ),
introduced(tautology,[equality,[$cnf( $equal(lin(x2(x2(eX,X_169),B2)),cons(x,cons(mul,lin(x2(X_169,B2))))) ),[1],$fot(lin(x2(eX,x2(X_169,B2))))]]) ).
cnf(refute_0_99,plain,
( lin(x2(x2(eX,X_169),B2)) != cons(x,cons(mul,lin(x2(X_169,B2))))
| lin(x2(x2(eX,X_169),B2)) = lin(x2(eX,x2(X_169,B2))) ),
inference(resolve,[$cnf( $equal(cons(x,cons(mul,lin(x2(X_169,B2)))),lin(x2(eX,x2(X_169,B2)))) )],[refute_0_97,refute_0_98]) ).
cnf(refute_0_100,plain,
( append(lin(x2(eX,X_169)),cons(mul,lin(B2))) != cons(x,cons(mul,lin(x2(X_169,B2))))
| lin(x2(x2(eX,X_169),B2)) = lin(x2(eX,x2(X_169,B2))) ),
inference(resolve,[$cnf( $equal(lin(x2(x2(eX,X_169),B2)),cons(x,cons(mul,lin(x2(X_169,B2))))) )],[refute_0_94,refute_0_99]) ).
cnf(refute_0_101,plain,
lin(x2(x2(eX,X_169),B2)) = lin(x2(eX,x2(X_169,B2))),
inference(resolve,[$cnf( $equal(append(lin(x2(eX,X_169)),cons(mul,lin(B2))),cons(x,cons(mul,lin(x2(X_169,B2))))) )],[refute_0_89,refute_0_100]) ).
cnf(refute_0_102,plain,
lin(x2(x2(eX,X_347),X_346)) = lin(x2(eX,x2(X_347,X_346))),
inference(subst,[],[refute_0_101:[bind(B2,$fot(X_346)),bind(X_169,$fot(X_347))]]) ).
cnf(refute_0_103,plain,
( lin(U) != lin(x2(eX,x2(X_347,X_346)))
| lin(x2(x2(eX,X_347),X_346)) != lin(x2(eX,x2(X_347,X_346)))
| lin(U) = lin(x2(x2(eX,X_347),X_346)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(lin(U),lin(x2(x2(eX,X_347),X_346))) ),[1],$fot(lin(x2(eX,x2(X_347,X_346))))]]) ).
cnf(refute_0_104,plain,
( lin(U) != lin(x2(eX,x2(X_347,X_346)))
| lin(U) = lin(x2(x2(eX,X_347),X_346)) ),
inference(resolve,[$cnf( $equal(lin(x2(x2(eX,X_347),X_346)),lin(x2(eX,x2(X_347,X_346)))) )],[refute_0_102,refute_0_103]) ).
cnf(refute_0_105,plain,
( lin(U) != lin(x2(eX,x2(X_347,X_346)))
| assoc(U) = assoc(x2(x2(eX,X_347),X_346)) ),
inference(resolve,[$cnf( $equal(lin(U),lin(x2(x2(eX,X_347),X_346))) )],[refute_0_104,refute_0_26]) ).
cnf(refute_0_106,plain,
( lin(x2(eX,x2(X_347,X_346))) != lin(x2(eX,x2(X_347,X_346)))
| assoc(x2(eX,x2(X_347,X_346))) = assoc(x2(x2(eX,X_347),X_346)) ),
inference(subst,[],[refute_0_105:[bind(U,$fot(x2(eX,x2(X_347,X_346))))]]) ).
cnf(refute_0_107,plain,
lin(x2(eX,x2(X_347,X_346))) = lin(x2(eX,x2(X_347,X_346))),
introduced(tautology,[refl,[$fot(lin(x2(eX,x2(X_347,X_346))))]]) ).
cnf(refute_0_108,plain,
assoc(x2(eX,x2(X_347,X_346))) = assoc(x2(x2(eX,X_347),X_346)),
inference(resolve,[$cnf( $equal(lin(x2(eX,x2(X_347,X_346))),lin(x2(eX,x2(X_347,X_346)))) )],[refute_0_107,refute_0_106]) ).
cnf(refute_0_109,plain,
assoc(x2(eX,x2(X_349,X_22))) = assoc(x2(x2(eX,X_349),X_22)),
inference(subst,[],[refute_0_108:[bind(X_346,$fot(X_22)),bind(X_347,$fot(X_349))]]) ).
cnf(refute_0_110,plain,
( assoc(x2(eX,x2(X_349,X_22))) != assoc(x2(x2(eX,X_349),X_22))
| assoc(x2(x2(eX,X_349),X_22)) = assoc(x2(eX,x2(X_349,X_22))) ),
inference(subst,[],[refute_0_6:[bind(X0,$fot(assoc(x2(eX,x2(X_349,X_22))))),bind(Y0,$fot(assoc(x2(x2(eX,X_349),X_22))))]]) ).
cnf(refute_0_111,plain,
assoc(x2(x2(eX,X_349),X_22)) = assoc(x2(eX,x2(X_349,X_22))),
inference(resolve,[$cnf( $equal(assoc(x2(eX,x2(X_349,X_22))),assoc(x2(x2(eX,X_349),X_22))) )],[refute_0_109,refute_0_110]) ).
cnf(refute_0_112,plain,
( assoc(x2(x2(eX,X_349),X_22)) != assoc(x2(eX,x2(X_349,X_22)))
| proj22(assoc(x2(x2(eX,X_349),X_22))) != assoc(X_22)
| proj22(assoc(x2(eX,x2(X_349,X_22)))) = assoc(X_22) ),
introduced(tautology,[equality,[$cnf( $equal(proj22(assoc(x2(x2(eX,X_349),X_22))),assoc(X_22)) ),[0,0],$fot(assoc(x2(eX,x2(X_349,X_22))))]]) ).
cnf(refute_0_113,plain,
( proj22(assoc(x2(x2(eX,X_349),X_22))) != assoc(X_22)
| proj22(assoc(x2(eX,x2(X_349,X_22)))) = assoc(X_22) ),
inference(resolve,[$cnf( $equal(assoc(x2(x2(eX,X_349),X_22)),assoc(x2(eX,x2(X_349,X_22)))) )],[refute_0_111,refute_0_112]) ).
cnf(refute_0_114,plain,
proj22(assoc(x2(eX,x2(X_349,X_22)))) = assoc(X_22),
inference(resolve,[$cnf( $equal(proj22(assoc(x2(x2(eX,X_349),X_22))),assoc(X_22)) )],[refute_0_24,refute_0_113]) ).
cnf(refute_0_115,plain,
proj22(assoc(x2(eX,x2(X_349,X_22)))) = assoc(x2(X_349,X_22)),
inference(subst,[],[refute_0_23:[bind(X_21,$fot(eX)),bind(X_22,$fot(x2(X_349,X_22)))]]) ).
cnf(refute_0_116,plain,
( proj22(assoc(x2(eX,x2(X_349,X_22)))) != assoc(X_22)
| proj22(assoc(x2(eX,x2(X_349,X_22)))) != assoc(x2(X_349,X_22))
| assoc(x2(X_349,X_22)) = assoc(X_22) ),
introduced(tautology,[equality,[$cnf( $equal(proj22(assoc(x2(eX,x2(X_349,X_22)))),assoc(X_22)) ),[0],$fot(assoc(x2(X_349,X_22)))]]) ).
cnf(refute_0_117,plain,
( proj22(assoc(x2(eX,x2(X_349,X_22)))) != assoc(X_22)
| assoc(x2(X_349,X_22)) = assoc(X_22) ),
inference(resolve,[$cnf( $equal(proj22(assoc(x2(eX,x2(X_349,X_22)))),assoc(x2(X_349,X_22))) )],[refute_0_115,refute_0_116]) ).
cnf(refute_0_118,plain,
assoc(x2(X_349,X_22)) = assoc(X_22),
inference(resolve,[$cnf( $equal(proj22(assoc(x2(eX,x2(X_349,X_22)))),assoc(X_22)) )],[refute_0_114,refute_0_117]) ).
cnf(refute_0_119,plain,
proj12(x2(X,X2)) = X,
inference(canonicalize,[],[normalize_0_18]) ).
cnf(refute_0_120,plain,
proj12(x2(assoc(X_21),assoc(X_22))) = assoc(X_21),
inference(subst,[],[refute_0_119:[bind(X,$fot(assoc(X_21))),bind(X2,$fot(assoc(X_22)))]]) ).
cnf(refute_0_121,plain,
( proj12(x2(assoc(X_21),assoc(X_22))) != assoc(X_21)
| x2(assoc(X_21),assoc(X_22)) != assoc(x2(X_21,X_22))
| proj12(assoc(x2(X_21,X_22))) = assoc(X_21) ),
introduced(tautology,[equality,[$cnf( $equal(proj12(x2(assoc(X_21),assoc(X_22))),assoc(X_21)) ),[0,0],$fot(assoc(x2(X_21,X_22)))]]) ).
cnf(refute_0_122,plain,
( proj12(x2(assoc(X_21),assoc(X_22))) != assoc(X_21)
| proj12(assoc(x2(X_21,X_22))) = assoc(X_21) ),
inference(resolve,[$cnf( $equal(x2(assoc(X_21),assoc(X_22)),assoc(x2(X_21,X_22))) )],[refute_0_20,refute_0_121]) ).
cnf(refute_0_123,plain,
proj12(assoc(x2(X_21,X_22))) = assoc(X_21),
inference(resolve,[$cnf( $equal(proj12(x2(assoc(X_21),assoc(X_22))),assoc(X_21)) )],[refute_0_120,refute_0_122]) ).
cnf(refute_0_124,plain,
proj12(assoc(x2(x2(eX,X_349),X_22))) = assoc(x2(eX,X_349)),
inference(subst,[],[refute_0_123:[bind(X_21,$fot(x2(eX,X_349)))]]) ).
cnf(refute_0_125,plain,
( assoc(x2(x2(eX,X_349),X_22)) != assoc(x2(eX,x2(X_349,X_22)))
| proj12(assoc(x2(x2(eX,X_349),X_22))) != assoc(x2(eX,X_349))
| proj12(assoc(x2(eX,x2(X_349,X_22)))) = assoc(x2(eX,X_349)) ),
introduced(tautology,[equality,[$cnf( $equal(proj12(assoc(x2(x2(eX,X_349),X_22))),assoc(x2(eX,X_349))) ),[0,0],$fot(assoc(x2(eX,x2(X_349,X_22))))]]) ).
cnf(refute_0_126,plain,
( proj12(assoc(x2(x2(eX,X_349),X_22))) != assoc(x2(eX,X_349))
| proj12(assoc(x2(eX,x2(X_349,X_22)))) = assoc(x2(eX,X_349)) ),
inference(resolve,[$cnf( $equal(assoc(x2(x2(eX,X_349),X_22)),assoc(x2(eX,x2(X_349,X_22)))) )],[refute_0_111,refute_0_125]) ).
cnf(refute_0_127,plain,
proj12(assoc(x2(eX,x2(X_349,X_22)))) = assoc(x2(eX,X_349)),
inference(resolve,[$cnf( $equal(proj12(assoc(x2(x2(eX,X_349),X_22))),assoc(x2(eX,X_349))) )],[refute_0_124,refute_0_126]) ).
cnf(refute_0_128,plain,
proj12(assoc(x2(eX,x2(X_349,X_22)))) = assoc(eX),
inference(subst,[],[refute_0_123:[bind(X_21,$fot(eX)),bind(X_22,$fot(x2(X_349,X_22)))]]) ).
cnf(refute_0_129,plain,
( proj12(assoc(x2(eX,x2(X_349,X_22)))) != assoc(eX)
| proj12(assoc(x2(eX,x2(X_349,X_22)))) != assoc(x2(eX,X_349))
| assoc(eX) = assoc(x2(eX,X_349)) ),
introduced(tautology,[equality,[$cnf( $equal(proj12(assoc(x2(eX,x2(X_349,X_22)))),assoc(x2(eX,X_349))) ),[0],$fot(assoc(eX))]]) ).
cnf(refute_0_130,plain,
( proj12(assoc(x2(eX,x2(X_349,X_22)))) != assoc(x2(eX,X_349))
| assoc(eX) = assoc(x2(eX,X_349)) ),
inference(resolve,[$cnf( $equal(proj12(assoc(x2(eX,x2(X_349,X_22)))),assoc(eX)) )],[refute_0_128,refute_0_129]) ).
cnf(refute_0_131,plain,
assoc(eX) = assoc(x2(eX,X_349)),
inference(resolve,[$cnf( $equal(proj12(assoc(x2(eX,x2(X_349,X_22)))),assoc(x2(eX,X_349))) )],[refute_0_127,refute_0_130]) ).
cnf(refute_0_132,plain,
assoc(x2(eX,X_349)) = assoc(X_349),
inference(subst,[],[refute_0_118:[bind(X_22,$fot(X_349)),bind(X_349,$fot(eX))]]) ).
cnf(refute_0_133,plain,
( assoc(eX) != assoc(x2(eX,X_349))
| assoc(x2(eX,X_349)) != assoc(X_349)
| assoc(eX) = assoc(X_349) ),
introduced(tautology,[equality,[$cnf( ~ $equal(assoc(eX),assoc(X_349)) ),[0],$fot(assoc(x2(eX,X_349)))]]) ).
cnf(refute_0_134,plain,
( assoc(eX) != assoc(x2(eX,X_349))
| assoc(eX) = assoc(X_349) ),
inference(resolve,[$cnf( $equal(assoc(x2(eX,X_349)),assoc(X_349)) )],[refute_0_132,refute_0_133]) ).
cnf(refute_0_135,plain,
assoc(eX) = assoc(X_349),
inference(resolve,[$cnf( $equal(assoc(eX),assoc(x2(eX,X_349))) )],[refute_0_131,refute_0_134]) ).
cnf(refute_0_136,plain,
( assoc(eX) != assoc(X_349)
| assoc(X_349) = assoc(eX) ),
inference(subst,[],[refute_0_6:[bind(X0,$fot(assoc(eX))),bind(Y0,$fot(assoc(X_349)))]]) ).
cnf(refute_0_137,plain,
assoc(X_349) = assoc(eX),
inference(resolve,[$cnf( $equal(assoc(eX),assoc(X_349)) )],[refute_0_135,refute_0_136]) ).
cnf(refute_0_138,plain,
assoc(x2(X_349,X_22)) = assoc(eX),
inference(subst,[],[refute_0_137:[bind(X_349,$fot(x2(X_349,X_22)))]]) ).
cnf(refute_0_139,plain,
( assoc(x2(X_349,X_22)) != assoc(X_22)
| assoc(x2(X_349,X_22)) != assoc(eX)
| assoc(eX) = assoc(X_22) ),
introduced(tautology,[equality,[$cnf( $equal(assoc(x2(X_349,X_22)),assoc(X_22)) ),[0],$fot(assoc(eX))]]) ).
cnf(refute_0_140,plain,
( assoc(x2(X_349,X_22)) != assoc(X_22)
| assoc(eX) = assoc(X_22) ),
inference(resolve,[$cnf( $equal(assoc(x2(X_349,X_22)),assoc(eX)) )],[refute_0_138,refute_0_139]) ).
cnf(refute_0_141,plain,
assoc(eX) = assoc(X_22),
inference(resolve,[$cnf( $equal(assoc(x2(X_349,X_22)),assoc(X_22)) )],[refute_0_118,refute_0_140]) ).
cnf(refute_0_142,plain,
( assoc(eX) != assoc(X_22)
| assoc(X_22) = assoc(eX) ),
inference(subst,[],[refute_0_6:[bind(X0,$fot(assoc(eX))),bind(Y0,$fot(assoc(X_22)))]]) ).
cnf(refute_0_143,plain,
assoc(X_22) = assoc(eX),
inference(resolve,[$cnf( $equal(assoc(eX),assoc(X_22)) )],[refute_0_141,refute_0_142]) ).
cnf(refute_0_144,plain,
assoc(eY) = assoc(eX),
inference(subst,[],[refute_0_143:[bind(X_22,$fot(eY))]]) ).
cnf(refute_0_145,plain,
( assoc(eY) != assoc(eX)
| assoc(eY) != eY
| assoc(eX) = eY ),
introduced(tautology,[equality,[$cnf( $equal(assoc(eY),eY) ),[0],$fot(assoc(eX))]]) ).
cnf(refute_0_146,plain,
( assoc(eY) != eY
| assoc(eX) = eY ),
inference(resolve,[$cnf( $equal(assoc(eY),assoc(eX)) )],[refute_0_144,refute_0_145]) ).
cnf(refute_0_147,plain,
( assoc(eX) = eY
| eY = x2(proj12(eY),proj22(eY)) ),
inference(resolve,[$cnf( $equal(assoc(eY),eY) )],[refute_0_14,refute_0_146]) ).
cnf(refute_0_148,plain,
x2(X,X2) != eY,
inference(canonicalize,[],[normalize_0_20]) ).
cnf(refute_0_149,plain,
x2(assoc(X_21),assoc(X_22)) != eY,
inference(subst,[],[refute_0_148:[bind(X,$fot(assoc(X_21))),bind(X2,$fot(assoc(X_22)))]]) ).
cnf(refute_0_150,plain,
( assoc(x2(X_21,X_22)) != eY
| x2(assoc(X_21),assoc(X_22)) != assoc(x2(X_21,X_22))
| x2(assoc(X_21),assoc(X_22)) = eY ),
introduced(tautology,[equality,[$cnf( $equal(x2(assoc(X_21),assoc(X_22)),assoc(x2(X_21,X_22))) ),[1],$fot(eY)]]) ).
cnf(refute_0_151,plain,
( assoc(x2(X_21,X_22)) != eY
| x2(assoc(X_21),assoc(X_22)) = eY ),
inference(resolve,[$cnf( $equal(x2(assoc(X_21),assoc(X_22)),assoc(x2(X_21,X_22))) )],[refute_0_20,refute_0_150]) ).
cnf(refute_0_152,plain,
assoc(x2(X_21,X_22)) != eY,
inference(resolve,[$cnf( $equal(x2(assoc(X_21),assoc(X_22)),eY) )],[refute_0_151,refute_0_149]) ).
cnf(refute_0_153,plain,
assoc(x2(x2(eX,X_349),X_22)) != eY,
inference(subst,[],[refute_0_152:[bind(X_21,$fot(x2(eX,X_349)))]]) ).
cnf(refute_0_154,plain,
( assoc(x2(eX,x2(X_349,X_22))) != eY
| assoc(x2(x2(eX,X_349),X_22)) != assoc(x2(eX,x2(X_349,X_22)))
| assoc(x2(x2(eX,X_349),X_22)) = eY ),
introduced(tautology,[equality,[$cnf( $equal(assoc(x2(x2(eX,X_349),X_22)),assoc(x2(eX,x2(X_349,X_22)))) ),[1],$fot(eY)]]) ).
cnf(refute_0_155,plain,
( assoc(x2(eX,x2(X_349,X_22))) != eY
| assoc(x2(x2(eX,X_349),X_22)) = eY ),
inference(resolve,[$cnf( $equal(assoc(x2(x2(eX,X_349),X_22)),assoc(x2(eX,x2(X_349,X_22)))) )],[refute_0_111,refute_0_154]) ).
cnf(refute_0_156,plain,
assoc(x2(eX,x2(X_349,X_22))) != eY,
inference(resolve,[$cnf( $equal(assoc(x2(x2(eX,X_349),X_22)),eY) )],[refute_0_155,refute_0_153]) ).
cnf(refute_0_157,plain,
assoc(x2(eX,x2(X_349,X_22))) = assoc(x2(X_349,X_22)),
inference(subst,[],[refute_0_118:[bind(X_22,$fot(x2(X_349,X_22))),bind(X_349,$fot(eX))]]) ).
cnf(refute_0_158,plain,
( assoc(x2(X_349,X_22)) != assoc(X_22)
| assoc(x2(eX,x2(X_349,X_22))) != assoc(x2(X_349,X_22))
| assoc(x2(eX,x2(X_349,X_22))) = assoc(X_22) ),
inference(subst,[],[refute_0_38:[bind(X0,$fot(assoc(x2(eX,x2(X_349,X_22))))),bind(Y0,$fot(assoc(x2(X_349,X_22)))),bind(Z0,$fot(assoc(X_22)))]]) ).
cnf(refute_0_159,plain,
( assoc(x2(X_349,X_22)) != assoc(X_22)
| assoc(x2(eX,x2(X_349,X_22))) = assoc(X_22) ),
inference(resolve,[$cnf( $equal(assoc(x2(eX,x2(X_349,X_22))),assoc(x2(X_349,X_22))) )],[refute_0_157,refute_0_158]) ).
cnf(refute_0_160,plain,
assoc(x2(eX,x2(X_349,X_22))) = assoc(X_22),
inference(resolve,[$cnf( $equal(assoc(x2(X_349,X_22)),assoc(X_22)) )],[refute_0_118,refute_0_159]) ).
cnf(refute_0_161,plain,
( assoc(X_22) != eY
| assoc(x2(eX,x2(X_349,X_22))) != assoc(X_22)
| assoc(x2(eX,x2(X_349,X_22))) = eY ),
introduced(tautology,[equality,[$cnf( $equal(assoc(x2(eX,x2(X_349,X_22))),assoc(X_22)) ),[1],$fot(eY)]]) ).
cnf(refute_0_162,plain,
( assoc(X_22) != eY
| assoc(x2(eX,x2(X_349,X_22))) = eY ),
inference(resolve,[$cnf( $equal(assoc(x2(eX,x2(X_349,X_22))),assoc(X_22)) )],[refute_0_160,refute_0_161]) ).
cnf(refute_0_163,plain,
assoc(X_22) != eY,
inference(resolve,[$cnf( $equal(assoc(x2(eX,x2(X_349,X_22))),eY) )],[refute_0_162,refute_0_156]) ).
cnf(refute_0_164,plain,
assoc(eX) != eY,
inference(subst,[],[refute_0_163:[bind(X_22,$fot(eX))]]) ).
cnf(refute_0_165,plain,
eY = x2(proj12(eY),proj22(eY)),
inference(resolve,[$cnf( $equal(assoc(eX),eY) )],[refute_0_147,refute_0_164]) ).
cnf(refute_0_166,plain,
( eY != x2(X,X2)
| x2(X,X2) = eY ),
inference(subst,[],[refute_0_6:[bind(X0,$fot(eY)),bind(Y0,$fot(x2(X,X2)))]]) ).
cnf(refute_0_167,plain,
eY != x2(X,X2),
inference(resolve,[$cnf( $equal(x2(X,X2),eY) )],[refute_0_166,refute_0_148]) ).
cnf(refute_0_168,plain,
eY != x2(proj12(eY),proj22(eY)),
inference(subst,[],[refute_0_167:[bind(X,$fot(proj12(eY))),bind(X2,$fot(proj22(eY)))]]) ).
cnf(refute_0_169,plain,
$false,
inference(resolve,[$cnf( $equal(eY,x2(proj12(eY),proj22(eY))) )],[refute_0_165,refute_0_168]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : SWX185+1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.14 % Command : metis --show proof --show saturation %s
% 0.17/0.35 % Computer : n004.cluster.edu
% 0.17/0.35 % Model : x86_64 x86_64
% 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.35 % Memory : 8042.1875MB
% 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.35 % CPULimit : 300
% 0.17/0.35 % WCLimit : 300
% 0.17/0.35 % DateTime : Tue May 5 09:32:17 EDT 2026
% 0.17/0.35 % CPUTime :
% 0.17/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 43.87/44.05 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 43.87/44.05
% 43.87/44.05 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 43.87/44.06
%------------------------------------------------------------------------------