%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWX185+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 06:56:33 PM UTC 2026
% Result : Theorem 164.18s 143.78s
% Output : CNFRefutation 164.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 22
% Syntax : Number of formulae : 118 ( 85 unt; 0 typ; 0 def)
% Number of atoms : 161 ( 160 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 88 ( 45 ~; 38 |; 0 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 9 con; 0-2 aty)
% Number of variables : 186 ( 184 !; 2 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ z > x2 > cons > append > #nlpp > tail > proj22 > proj2 > proj12 > proj1 > linTerm > lin > head > assoc > y > x > plus > nil > mul > eY > eX > d > c
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(proj2,type,
proj2: $i > $i ).
tff(assoc,type,
assoc: $i > $i ).
tff(plus,type,
plus: $i ).
tff(eY,type,
eY: $i ).
tff(proj12,type,
proj12: $i > $i ).
tff(x,type,
x: $i ).
tff(eX,type,
eX: $i ).
tff(linTerm,type,
linTerm: $i > $i ).
tff(lin,type,
lin: $i > $i ).
tff(y,type,
y: $i ).
tff(mul,type,
mul: $i ).
tff(append,type,
append: ( $i * $i ) > $i ).
tff(proj1,type,
proj1: $i > $i ).
tff(cons,type,
cons: ( $i * $i ) > $i ).
tff(z,type,
z: ( $i * $i ) > $i ).
tff(proj22,type,
proj22: $i > $i ).
tff(d,type,
d: $i ).
tff(tail,type,
tail: $i > $i ).
tff(x2,type,
x2: ( $i * $i ) > $i ).
tff(head,type,
head: $i > $i ).
tff(nil,type,
nil: $i ).
tff(c,type,
c: $i ).
tff(f_103,axiom,
! [A2,B2] : ( assoc(x2(A2,B2)) = x2(assoc(A2),assoc(B2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_032) ).
tff(f_84,axiom,
! [X,X2] : ( x2(X,X2) != eY ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_027) ).
tff(f_65,axiom,
! [X,X2] : ( proj2(z(X,X2)) = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_020) ).
tff(f_94,axiom,
! [X] :
( ( X != z(proj1(X),proj2(X)) )
=> ( ( X != x2(proj12(X),proj22(X)) )
=> ( assoc(X) = X ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_029) ).
tff(f_78,axiom,
! [X,X2] : ( z(X,X2) != eY ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_025) ).
tff(f_75,axiom,
! [X,X2] : ( z(X,X2) != eX ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_024) ).
tff(f_35,axiom,
c != x,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_005) ).
tff(f_112,axiom,
! [X] :
( ( X != x2(proj12(X),proj22(X)) )
=> ( linTerm(X) = lin(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_035) ).
tff(f_81,axiom,
! [X,X2] : ( x2(X,X2) != eX ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_026) ).
tff(f_105,axiom,
! [Y] : ( append(nil,Y) = Y ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_033) ).
tff(f_107,axiom,
! [Y,Z,Xs] : ( append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_034) ).
tff(f_116,axiom,
! [A,B] : ( lin(z(A,B)) = append(linTerm(A),append(cons(plus,nil),linTerm(B))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_037) ).
tff(f_119,axiom,
lin(eX) = cons(x,nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_039) ).
tff(f_26,axiom,
! [X,X2] : ( head(cons(X,X2)) = X ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_001) ).
tff(f_114,axiom,
! [A,B] : ( linTerm(x2(A,B)) = append(cons(c,nil),append(lin(z(A,B)),cons(d,nil))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_036) ).
tff(f_99,axiom,
! [Y,C] :
( ( Y != z(proj1(Y),proj2(Y)) )
=> ( assoc(z(Y,C)) = z(assoc(Y),assoc(C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_030) ).
tff(f_67,axiom,
! [X,X2] : ( proj12(x2(X,X2)) = X ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_021) ).
tff(f_69,axiom,
! [X,X2] : ( proj22(x2(X,X2)) = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_022) ).
tff(f_37,axiom,
c != y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_006) ).
tff(f_120,axiom,
lin(eY) = cons(y,nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_040) ).
tff(f_118,axiom,
! [A3,B2] : ( lin(x2(A3,B2)) = append(lin(A3),append(cons(mul,nil),lin(B2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_038) ).
tff(f_126,negated_conjecture,
~ ? [U,V] :
~ ( ( lin(U) = lin(V) )
=> ( assoc(U) = assoc(V) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal_041) ).
tff(c_64,plain,
! [A2_33,B2_34] : ( x2(assoc(A2_33),assoc(B2_34)) = assoc(x2(A2_33,B2_34)) ),
inference(cnfTransformation,[status(thm)],[f_103]) ).
tff(c_197,plain,
! [A2_77,B2_78] : ( x2(assoc(A2_77),assoc(B2_78)) = assoc(x2(A2_77,B2_78)) ),
inference(cnfTransformation,[status(thm)],[f_103]) ).
tff(c_54,plain,
! [X_25,X2_26] : ( x2(X_25,X2_26) != eY ),
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_254,plain,
! [A2_82,B2_83] : ( assoc(x2(A2_82,B2_83)) != eY ),
inference(superposition,[status(thm),theory(equality)],[c_197,c_54]) ).
tff(c_338,plain,
! [A2_99,B2_100] : ( assoc(assoc(x2(A2_99,B2_100))) != eY ),
inference(superposition,[status(thm),theory(equality)],[c_64,c_254]) ).
tff(c_342,plain,
! [A2_33,B2_34] : ( assoc(assoc(assoc(x2(A2_33,B2_34)))) != eY ),
inference(superposition,[status(thm),theory(equality)],[c_64,c_338]) ).
tff(c_40,plain,
! [X_9,X2_10] : ( proj2(z(X_9,X2_10)) = X2_10 ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_659,plain,
! [X_132] :
( ( assoc(X_132) = X_132 )
| ( x2(proj12(X_132),proj22(X_132)) = X_132 )
| ( z(proj1(X_132),proj2(X_132)) = X_132 ) ),
inference(cnfTransformation,[status(thm)],[f_94]) ).
tff(c_50,plain,
! [X_21,X2_22] : ( z(X_21,X2_22) != eY ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_2027,plain,
! [X_224] :
( ( eY != X_224 )
| ( assoc(X_224) = X_224 )
| ( x2(proj12(X_224),proj22(X_224)) = X_224 ) ),
inference(superposition,[status(thm),theory(equality)],[c_659,c_50]) ).
tff(c_2104,plain,
! [X_224] :
( ( eY != X_224 )
| ( eY != X_224 )
| ( assoc(X_224) = X_224 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2027,c_54]) ).
tff(c_48,plain,
! [X_19,X2_20] : ( z(X_19,X2_20) != eX ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_10,plain,
x != c,
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_218,plain,
! [X_79] :
( ( linTerm(X_79) = lin(X_79) )
| ( x2(proj12(X_79),proj22(X_79)) = X_79 ) ),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_52,plain,
! [X_23,X2_24] : ( x2(X_23,X2_24) != eX ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_231,plain,
! [X_79] :
( ( eX != X_79 )
| ( linTerm(X_79) = lin(X_79) ) ),
inference(superposition,[status(thm),theory(equality)],[c_218,c_52]) ).
tff(c_66,plain,
! [Y_35] : ( append(nil,Y_35) = Y_35 ),
inference(cnfTransformation,[status(thm)],[f_105]) ).
tff(c_292,plain,
! [Z_88,Xs_89,Y_90] : ( cons(Z_88,append(Xs_89,Y_90)) = append(cons(Z_88,Xs_89),Y_90) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_309,plain,
! [Z_88,Y_35] : ( append(cons(Z_88,nil),Y_35) = cons(Z_88,Y_35) ),
inference(superposition,[status(thm),theory(equality)],[c_66,c_292]) ).
tff(c_74,plain,
! [A_42,B_43] : ( append(linTerm(A_42),append(cons(plus,nil),linTerm(B_43))) = lin(z(A_42,B_43)) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_3854,plain,
! [A_321,B_322] : ( append(linTerm(A_321),cons(plus,linTerm(B_322))) = lin(z(A_321,B_322)) ),
inference(demodulation,[status(thm),theory(equality)],[c_309,c_74]) ).
tff(c_19372,plain,
! [X_864,B_865] :
( ( append(lin(X_864),cons(plus,linTerm(B_865))) = lin(z(X_864,B_865)) )
| ( eX != X_864 ) ),
inference(superposition,[status(thm),theory(equality)],[c_231,c_3854]) ).
tff(c_78,plain,
cons(x,nil) = lin(eX),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_635,plain,
! [Z_130,Y_131] : ( append(cons(Z_130,nil),Y_131) = cons(Z_130,Y_131) ),
inference(superposition,[status(thm),theory(equality)],[c_66,c_292]) ).
tff(c_652,plain,
! [Y_131] : ( append(lin(eX),Y_131) = cons(x,Y_131) ),
inference(superposition,[status(thm),theory(equality)],[c_78,c_635]) ).
tff(c_23563,plain,
! [B_978] : ( cons(x,cons(plus,linTerm(B_978))) = lin(z(eX,B_978)) ),
inference(superposition,[status(thm),theory(equality)],[c_19372,c_652]) ).
tff(c_2,plain,
! [X_1,X2_2] : ( head(cons(X_1,X2_2)) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_26]) ).
tff(c_23623,plain,
! [B_980] : ( head(lin(z(eX,B_980))) = x ),
inference(superposition,[status(thm),theory(equality)],[c_23563,c_2]) ).
tff(c_634,plain,
! [A_42,B_43] : ( append(linTerm(A_42),cons(plus,linTerm(B_43))) = lin(z(A_42,B_43)) ),
inference(demodulation,[status(thm),theory(equality)],[c_309,c_74]) ).
tff(c_1373,plain,
! [X_212] :
( ( eX != X_212 )
| ( assoc(X_212) = X_212 )
| ( x2(proj12(X_212),proj22(X_212)) = X_212 ) ),
inference(superposition,[status(thm),theory(equality)],[c_659,c_48]) ).
tff(c_72,plain,
! [A_40,B_41] : ( append(cons(c,nil),append(lin(z(A_40,B_41)),cons(d,nil))) = linTerm(x2(A_40,B_41)) ),
inference(cnfTransformation,[status(thm)],[f_114]) ).
tff(c_68,plain,
! [Z_37,Xs_38,Y_36] : ( cons(Z_37,append(Xs_38,Y_36)) = append(cons(Z_37,Xs_38),Y_36) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_380,plain,
! [Z_105,Xs_106,Y_107] : ( head(append(cons(Z_105,Xs_106),Y_107)) = Z_105 ),
inference(superposition,[status(thm),theory(equality)],[c_292,c_2]) ).
tff(c_1116,plain,
! [Z_182,Xs_183,Y_184,Y_185] : ( head(append(append(cons(Z_182,Xs_183),Y_184),Y_185)) = Z_182 ),
inference(superposition,[status(thm),theory(equality)],[c_68,c_380]) ).
tff(c_1125,plain,
! [A_40,B_41,Y_185] : ( head(append(linTerm(x2(A_40,B_41)),Y_185)) = c ),
inference(superposition,[status(thm),theory(equality)],[c_72,c_1116]) ).
tff(c_10947,plain,
! [X_625,Y_626] :
( ( head(append(linTerm(X_625),Y_626)) = c )
| ( eX != X_625 )
| ( assoc(X_625) = X_625 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1373,c_1125]) ).
tff(c_10983,plain,
! [A_42,B_43] :
( ( head(lin(z(A_42,B_43))) = c )
| ( eX != A_42 )
| ( assoc(A_42) = A_42 ) ),
inference(superposition,[status(thm),theory(equality)],[c_634,c_10947]) ).
tff(c_23628,plain,
( ( x = c )
| ( assoc(eX) = eX ) ),
inference(superposition,[status(thm),theory(equality)],[c_23623,c_10983]) ).
tff(c_23652,plain,
assoc(eX) = eX,
inference(negUnitSimplification,[status(thm)],[c_10,c_23628]) ).
tff(c_60,plain,
! [Y_28,C_29] :
( ( z(assoc(Y_28),assoc(C_29)) = assoc(z(Y_28,C_29)) )
| ( z(proj1(Y_28),proj2(Y_28)) = Y_28 ) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_23905,plain,
! [C_29] :
( ( z(eX,assoc(C_29)) = assoc(z(eX,C_29)) )
| ( z(proj1(eX),proj2(eX)) = eX ) ),
inference(superposition,[status(thm),theory(equality)],[c_23652,c_60]) ).
tff(c_24038,plain,
! [C_981] : ( z(eX,assoc(C_981)) = assoc(z(eX,C_981)) ),
inference(negUnitSimplification,[status(thm)],[c_48,c_23905]) ).
tff(c_49537,plain,
! [X_1506] :
( ( assoc(z(eX,X_1506)) = z(eX,X_1506) )
| ( eY != X_1506 )
| ( eY != X_1506 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2104,c_24038]) ).
tff(c_555,plain,
! [Y_124,C_125] :
( ( z(assoc(Y_124),assoc(C_125)) = assoc(z(Y_124,C_125)) )
| ( z(proj1(Y_124),proj2(Y_124)) = Y_124 ) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_2979,plain,
! [Y_254,C_255] :
( ( eX != Y_254 )
| ( z(assoc(Y_254),assoc(C_255)) = assoc(z(Y_254,C_255)) ) ),
inference(superposition,[status(thm),theory(equality)],[c_555,c_48]) ).
tff(c_3026,plain,
! [Y_254,C_255] :
( ( proj2(assoc(z(Y_254,C_255))) = assoc(C_255) )
| ( eX != Y_254 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2979,c_40]) ).
tff(c_50051,plain,
! [X_1506] :
( ( proj2(z(eX,X_1506)) = assoc(X_1506) )
| ( eY != X_1506 ) ),
inference(superposition,[status(thm),theory(equality)],[c_49537,c_3026]) ).
tff(c_50346,plain,
assoc(eY) = eY,
inference(demodulation,[status(thm),theory(equality)],[c_40,c_50051]) ).
tff(c_42,plain,
! [X_11,X2_12] : ( proj12(x2(X_11,X2_12)) = X_11 ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_208,plain,
! [A2_77,B2_78] : ( proj12(assoc(x2(A2_77,B2_78))) = assoc(A2_77) ),
inference(superposition,[status(thm),theory(equality)],[c_197,c_42]) ).
tff(c_50348,plain,
! [X_1507] :
( ( assoc(X_1507) = X_1507 )
| ( eY != X_1507 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_50051]) ).
tff(c_23912,plain,
! [A2_33] : ( x2(assoc(A2_33),eX) = assoc(x2(A2_33,eX)) ),
inference(superposition,[status(thm),theory(equality)],[c_23652,c_64]) ).
tff(c_53645,plain,
! [X_1508] :
( ( assoc(x2(X_1508,eX)) = x2(X_1508,eX) )
| ( eY != X_1508 ) ),
inference(superposition,[status(thm),theory(equality)],[c_50348,c_23912]) ).
tff(c_343,plain,
! [A2_101,B2_102] : ( proj12(assoc(x2(A2_101,B2_102))) = assoc(A2_101) ),
inference(superposition,[status(thm),theory(equality)],[c_197,c_42]) ).
tff(c_358,plain,
! [A2_33,B2_34] : ( proj12(assoc(assoc(x2(A2_33,B2_34)))) = assoc(assoc(A2_33)) ),
inference(superposition,[status(thm),theory(equality)],[c_64,c_343]) ).
tff(c_54488,plain,
! [X_1508] :
( ( proj12(assoc(x2(X_1508,eX))) = assoc(assoc(X_1508)) )
| ( eY != X_1508 ) ),
inference(superposition,[status(thm),theory(equality)],[c_53645,c_358]) ).
tff(c_54725,plain,
assoc(assoc(eY)) = assoc(eY),
inference(demodulation,[status(thm),theory(equality)],[c_208,c_54488]) ).
tff(c_44,plain,
! [X_13,X2_14] : ( proj22(x2(X_13,X2_14)) = X2_14 ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_361,plain,
! [A2_103,B2_104] : ( proj22(assoc(x2(A2_103,B2_104))) = assoc(B2_104) ),
inference(superposition,[status(thm),theory(equality)],[c_197,c_44]) ).
tff(c_376,plain,
! [A2_33,B2_34] : ( proj22(assoc(assoc(x2(A2_33,B2_34)))) = assoc(assoc(B2_34)) ),
inference(superposition,[status(thm),theory(equality)],[c_64,c_361]) ).
tff(c_12,plain,
y != c,
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_233,plain,
! [X_79] :
( ( eY != X_79 )
| ( linTerm(X_79) = lin(X_79) ) ),
inference(superposition,[status(thm),theory(equality)],[c_218,c_54]) ).
tff(c_17226,plain,
! [X_833,B_834] :
( ( append(lin(X_833),cons(plus,linTerm(B_834))) = lin(z(X_833,B_834)) )
| ( eY != X_833 ) ),
inference(superposition,[status(thm),theory(equality)],[c_233,c_3854]) ).
tff(c_80,plain,
cons(y,nil) = lin(eY),
inference(cnfTransformation,[status(thm)],[f_120]) ).
tff(c_655,plain,
! [Y_131] : ( append(lin(eY),Y_131) = cons(y,Y_131) ),
inference(superposition,[status(thm),theory(equality)],[c_80,c_635]) ).
tff(c_17400,plain,
! [B_835] : ( cons(y,cons(plus,linTerm(B_835))) = lin(z(eY,B_835)) ),
inference(superposition,[status(thm),theory(equality)],[c_17226,c_655]) ).
tff(c_17459,plain,
! [B_837] : ( head(lin(z(eY,B_837))) = y ),
inference(superposition,[status(thm),theory(equality)],[c_17400,c_2]) ).
tff(c_682,plain,
! [X_132] :
( ( eY != X_132 )
| ( assoc(X_132) = X_132 )
| ( x2(proj12(X_132),proj22(X_132)) = X_132 ) ),
inference(superposition,[status(thm),theory(equality)],[c_659,c_50]) ).
tff(c_3926,plain,
! [A_326,B_327,B_328] : ( head(lin(z(x2(A_326,B_327),B_328))) = c ),
inference(superposition,[status(thm),theory(equality)],[c_3854,c_1125]) ).
tff(c_3932,plain,
! [X_132,B_328] :
( ( head(lin(z(X_132,B_328))) = c )
| ( eY != X_132 )
| ( assoc(X_132) = X_132 ) ),
inference(superposition,[status(thm),theory(equality)],[c_682,c_3926]) ).
tff(c_17467,plain,
( ( y = c )
| ( assoc(eY) = eY ) ),
inference(superposition,[status(thm),theory(equality)],[c_17459,c_3932]) ).
tff(c_17489,plain,
assoc(eY) = eY,
inference(negUnitSimplification,[status(thm)],[c_12,c_17467]) ).
tff(c_17736,plain,
! [B2_34] : ( x2(eY,assoc(B2_34)) = assoc(x2(eY,B2_34)) ),
inference(superposition,[status(thm),theory(equality)],[c_17489,c_64]) ).
tff(c_58657,plain,
! [X_1514] :
( ( assoc(x2(eY,X_1514)) = x2(eY,X_1514) )
| ( eY != X_1514 ) ),
inference(superposition,[status(thm),theory(equality)],[c_50348,c_17736]) ).
tff(c_1098,plain,
! [A2_180,B2_181] : ( proj22(assoc(assoc(x2(A2_180,B2_181)))) = assoc(assoc(B2_181)) ),
inference(superposition,[status(thm),theory(equality)],[c_64,c_361]) ).
tff(c_1113,plain,
! [A2_33,B2_34] : ( proj22(assoc(assoc(assoc(x2(A2_33,B2_34))))) = assoc(assoc(assoc(B2_34))) ),
inference(superposition,[status(thm),theory(equality)],[c_64,c_1098]) ).
tff(c_58973,plain,
! [X_1514] :
( ( proj22(assoc(assoc(x2(eY,X_1514)))) = assoc(assoc(assoc(X_1514))) )
| ( eY != X_1514 ) ),
inference(superposition,[status(thm),theory(equality)],[c_58657,c_1113]) ).
tff(c_61831,plain,
assoc(assoc(assoc(eY))) = assoc(assoc(eY)),
inference(demodulation,[status(thm),theory(equality)],[c_376,c_58973]) ).
tff(c_1249,plain,
! [A2_195,B2_196] : ( proj12(assoc(assoc(x2(A2_195,B2_196)))) = assoc(assoc(A2_195)) ),
inference(superposition,[status(thm),theory(equality)],[c_64,c_343]) ).
tff(c_1264,plain,
! [A2_33,B2_34] : ( proj12(assoc(assoc(assoc(x2(A2_33,B2_34))))) = assoc(assoc(assoc(A2_33))) ),
inference(superposition,[status(thm),theory(equality)],[c_64,c_1249]) ).
tff(c_76,plain,
! [A3_44,B2_45] : ( append(lin(A3_44),append(cons(mul,nil),lin(B2_45))) = lin(x2(A3_44,B2_45)) ),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_3750,plain,
! [A3_303,B2_304] : ( append(lin(A3_303),cons(mul,lin(B2_304))) = lin(x2(A3_303,B2_304)) ),
inference(demodulation,[status(thm),theory(equality)],[c_309,c_76]) ).
tff(c_3757,plain,
! [B2_304] : ( cons(y,cons(mul,lin(B2_304))) = lin(x2(eY,B2_304)) ),
inference(superposition,[status(thm),theory(equality)],[c_3750,c_655]) ).
tff(c_633,plain,
! [A3_44,B2_45] : ( append(lin(A3_44),cons(mul,lin(B2_45))) = lin(x2(A3_44,B2_45)) ),
inference(demodulation,[status(thm),theory(equality)],[c_309,c_76]) ).
tff(c_472,plain,
! [A3_117,B2_118] : ( append(lin(A3_117),append(cons(mul,nil),lin(B2_118))) = lin(x2(A3_117,B2_118)) ),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_494,plain,
! [Z_37,A3_117,B2_118] : ( append(cons(Z_37,lin(A3_117)),append(cons(mul,nil),lin(B2_118))) = cons(Z_37,lin(x2(A3_117,B2_118))) ),
inference(superposition,[status(thm),theory(equality)],[c_472,c_68]) ).
tff(c_6917,plain,
! [Z_484,A3_485,B2_486] : ( append(cons(Z_484,lin(A3_485)),cons(mul,lin(B2_486))) = cons(Z_484,lin(x2(A3_485,B2_486))) ),
inference(demodulation,[status(thm),theory(equality)],[c_309,c_494]) ).
tff(c_40755,plain,
! [Z_1347,Z_1348,A3_1349,B2_1350] : ( append(cons(Z_1347,cons(Z_1348,lin(A3_1349))),cons(mul,lin(B2_1350))) = cons(Z_1347,cons(Z_1348,lin(x2(A3_1349,B2_1350)))) ),
inference(superposition,[status(thm),theory(equality)],[c_6917,c_68]) ).
tff(c_40791,plain,
! [B2_304,B2_1350] : ( append(lin(x2(eY,B2_304)),cons(mul,lin(B2_1350))) = cons(y,cons(mul,lin(x2(B2_304,B2_1350)))) ),
inference(superposition,[status(thm),theory(equality)],[c_3757,c_40755]) ).
tff(c_379628,plain,
! [B2_2675,B2_2676] : ( lin(x2(x2(eY,B2_2675),B2_2676)) = lin(x2(eY,x2(B2_2675,B2_2676))) ),
inference(demodulation,[status(thm),theory(equality)],[c_3757,c_633,c_40791]) ).
tff(c_82,plain,
! [V_47,U_46] :
( ( assoc(V_47) = assoc(U_46) )
| ( lin(V_47) != lin(U_46) ) ),
inference(cnfTransformation,[status(thm)],[f_126]) ).
tff(c_379775,plain,
! [B2_2675,B2_2676,V_47] :
( ( assoc(x2(x2(eY,B2_2675),B2_2676)) = assoc(V_47) )
| ( lin(x2(eY,x2(B2_2675,B2_2676))) != lin(V_47) ) ),
inference(superposition,[status(thm),theory(equality)],[c_379628,c_82]) ).
tff(c_412377,plain,
! [B2_2837,B2_2838] : ( assoc(x2(x2(eY,B2_2837),B2_2838)) = assoc(x2(eY,x2(B2_2837,B2_2838))) ),
inference(reflexivity,[status(thm),theory(equality)],[c_379775]) ).
tff(c_413183,plain,
! [B2_2837,B2_2838] : ( proj12(assoc(assoc(assoc(x2(eY,x2(B2_2837,B2_2838)))))) = assoc(assoc(assoc(x2(eY,B2_2837)))) ),
inference(superposition,[status(thm),theory(equality)],[c_412377,c_1264]) ).
tff(c_413652,plain,
! [B2_2837] : ( assoc(assoc(assoc(x2(eY,B2_2837)))) = eY ),
inference(demodulation,[status(thm),theory(equality)],[c_50346,c_54725,c_61831,c_1264,c_413183]) ).
tff(c_413654,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_342,c_413652]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX185+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.16/0.35 % Computer : n026.cluster.edu
% 0.16/0.35 % Model : x86_64 x86_64
% 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.35 % Memory : 8042.1875MB
% 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.35 % CPULimit : 300
% 0.16/0.35 % WCLimit : 300
% 0.16/0.35 % DateTime : Tue May 5 09:33:08 EDT 2026
% 0.16/0.35 % CPUTime :
% 164.18/143.78 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 164.18/143.79
% 164.18/143.79 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------