%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : TOP050-1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:53:48 PM UTC 2026
% Result : Unsatisfiable 6.39s 1.34s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP050-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.41 % Computer : n017.cluster.edu
% 0.17/0.41 % Model : x86_64 x86_64
% 0.17/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.41 % Memory : 8046.5625MB
% 0.17/0.41 % OS : Linux 6.8.0-71-generic
% 0.17/0.41 % CPULimit : 300
% 0.17/0.41 % WCLimit : 300
% 0.17/0.41 % DateTime : Mon Sep 21 12:42:42 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.42 % Drodi V4.1.1
% 6.39/1.34 % Refutation found
% 6.39/1.34 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 6.39/1.34 % SZS output start CNFRefutation for theBenchmark
% 6.39/1.34 fof(f1,axiom,(
% 6.39/1.34 (![X]: (product(X,X) = X ))),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f2,axiom,(
% 6.39/1.34 (![X,Y]: (product(product(X,Y),Y) = X ))),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f3,axiom,(
% 6.39/1.34 (![X,Y,Z]: (product(product(X,Y),Z) = product(product(X,Z),product(Y,Z)) ))),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f4,axiom,(
% 6.39/1.34 product(a1,a31) = a2 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f5,axiom,(
% 6.39/1.34 product(a2,a25) = a3 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f6,axiom,(
% 6.39/1.34 product(a3,a29) = a4 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f7,axiom,(
% 6.39/1.34 product(a4,a11) = a5 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f8,axiom,(
% 6.39/1.34 product(a5,a15) = a6 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f9,axiom,(
% 6.39/1.34 product(a7,a19) = a8 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f10,axiom,(
% 6.39/1.34 product(a8,a5) = a9 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f11,axiom,(
% 6.39/1.34 product(a9,a17) = a10 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f12,axiom,(
% 6.39/1.34 product(a10,a7) = a11 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f13,axiom,(
% 6.39/1.34 product(a11,a5) = a12 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f14,axiom,(
% 6.39/1.34 product(a12,a19) = a13 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f15,axiom,(
% 6.39/1.34 product(a13,a7) = a14 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f16,axiom,(
% 6.39/1.34 product(a14,a17) = a15 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f17,axiom,(
% 6.39/1.34 product(a15,a5) = a16 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f18,axiom,(
% 6.39/1.34 product(a16,a19) = a17 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f19,axiom,(
% 6.39/1.34 product(a17,a9) = a18 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f20,axiom,(
% 6.39/1.34 product(a18,a15) = a19 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f21,axiom,(
% 6.39/1.34 product(a19,a11) = a20 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f22,axiom,(
% 6.39/1.34 product(a20,a29) = a21 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f23,axiom,(
% 6.39/1.34 product(a21,a25) = a22 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f24,axiom,(
% 6.39/1.34 product(a22,a31) = a23 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f25,axiom,(
% 6.39/1.34 product(a23,a21) = a24 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f26,axiom,(
% 6.39/1.34 product(a24,a3) = a25 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f27,axiom,(
% 6.39/1.34 product(a25,a23) = a26 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f28,axiom,(
% 6.39/1.34 product(a26,a1) = a27 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f29,axiom,(
% 6.39/1.34 product(a27,a21) = a28 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f30,axiom,(
% 6.39/1.34 product(a28,a3) = a29 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f31,axiom,(
% 6.39/1.34 product(a29,a1) = a30 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f32,axiom,(
% 6.39/1.34 product(a30,a23) = a31 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f33,axiom,(
% 6.39/1.34 product(a31,a3) = a32 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f34,axiom,(
% 6.39/1.34 product(a32,a21) = a1 ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f35,negated_conjecture,(
% 6.39/1.34 tuple(a1,a30,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27) != tuple(a2,a31,a32,a3,a25,a26,a4,a29,a30,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a27,a28) ),
% 6.39/1.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.39/1.34 fof(f36,plain,(
% 6.39/1.34 ![X0]: (product(X0,X0)=X0)),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f1])).
% 6.39/1.34 fof(f37,plain,(
% 6.39/1.34 ![X0,X1]: (product(product(X0,X1),X1)=X0)),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f2])).
% 6.39/1.34 fof(f38,plain,(
% 6.39/1.34 ![X0,X1,X2]: (product(product(X0,X1),X2)=product(product(X0,X2),product(X1,X2)))),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f3])).
% 6.39/1.34 fof(f39,plain,(
% 6.39/1.34 product(a1,a31)=a2),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f4])).
% 6.39/1.34 fof(f40,plain,(
% 6.39/1.34 product(a2,a25)=a3),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f5])).
% 6.39/1.34 fof(f41,plain,(
% 6.39/1.34 product(a3,a29)=a4),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f6])).
% 6.39/1.34 fof(f42,plain,(
% 6.39/1.34 product(a4,a11)=a5),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f7])).
% 6.39/1.34 fof(f43,plain,(
% 6.39/1.34 product(a5,a15)=a6),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f8])).
% 6.39/1.34 fof(f44,plain,(
% 6.39/1.34 product(a7,a19)=a8),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f9])).
% 6.39/1.34 fof(f45,plain,(
% 6.39/1.34 product(a8,a5)=a9),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f10])).
% 6.39/1.34 fof(f46,plain,(
% 6.39/1.34 product(a9,a17)=a10),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f11])).
% 6.39/1.34 fof(f47,plain,(
% 6.39/1.34 product(a10,a7)=a11),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f12])).
% 6.39/1.34 fof(f48,plain,(
% 6.39/1.34 product(a11,a5)=a12),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f13])).
% 6.39/1.34 fof(f49,plain,(
% 6.39/1.34 product(a12,a19)=a13),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f14])).
% 6.39/1.34 fof(f50,plain,(
% 6.39/1.34 product(a13,a7)=a14),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f15])).
% 6.39/1.34 fof(f51,plain,(
% 6.39/1.34 product(a14,a17)=a15),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f16])).
% 6.39/1.34 fof(f52,plain,(
% 6.39/1.34 product(a15,a5)=a16),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f17])).
% 6.39/1.34 fof(f53,plain,(
% 6.39/1.34 product(a16,a19)=a17),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f18])).
% 6.39/1.34 fof(f54,plain,(
% 6.39/1.34 product(a17,a9)=a18),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f19])).
% 6.39/1.34 fof(f55,plain,(
% 6.39/1.34 product(a18,a15)=a19),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f20])).
% 6.39/1.34 fof(f56,plain,(
% 6.39/1.34 product(a19,a11)=a20),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f21])).
% 6.39/1.34 fof(f57,plain,(
% 6.39/1.34 product(a20,a29)=a21),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f22])).
% 6.39/1.34 fof(f58,plain,(
% 6.39/1.34 product(a21,a25)=a22),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f23])).
% 6.39/1.34 fof(f59,plain,(
% 6.39/1.34 product(a22,a31)=a23),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f24])).
% 6.39/1.34 fof(f60,plain,(
% 6.39/1.34 product(a23,a21)=a24),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f25])).
% 6.39/1.34 fof(f61,plain,(
% 6.39/1.34 product(a24,a3)=a25),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f26])).
% 6.39/1.34 fof(f62,plain,(
% 6.39/1.34 product(a25,a23)=a26),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f27])).
% 6.39/1.34 fof(f63,plain,(
% 6.39/1.34 product(a26,a1)=a27),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f28])).
% 6.39/1.34 fof(f64,plain,(
% 6.39/1.34 product(a27,a21)=a28),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f29])).
% 6.39/1.34 fof(f65,plain,(
% 6.39/1.34 product(a28,a3)=a29),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f30])).
% 6.39/1.34 fof(f66,plain,(
% 6.39/1.34 product(a29,a1)=a30),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f31])).
% 6.39/1.34 fof(f67,plain,(
% 6.39/1.34 product(a30,a23)=a31),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f32])).
% 6.39/1.34 fof(f68,plain,(
% 6.39/1.34 product(a31,a3)=a32),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f33])).
% 6.39/1.34 fof(f69,plain,(
% 6.39/1.34 product(a32,a21)=a1),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f34])).
% 6.39/1.34 fof(f70,plain,(
% 6.39/1.34 ~tuple(a1,a30,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27)=tuple(a2,a31,a32,a3,a25,a26,a4,a29,a30,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a27,a28)),
% 6.39/1.34 inference(cnf_transformation,[status(thm)],[f35])).
% 6.39/1.34 fof(f71,definition,(
% 6.39/1.34 sF0_fnc=tuple(a1,a30,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27)),
% 6.39/1.34 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 6.39/1.34 fof(f72,definition,(
% 6.39/1.34 sF1_fnc=tuple(a2,a31,a32,a3,a25,a26,a4,a29,a30,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a27,a28)),
% 6.39/1.34 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 6.39/1.34 fof(f73,plain,(
% 6.39/1.34 ~sF0_fnc=sF1_fnc),
% 6.39/1.34 inference(definition_folding,[],[f70,f72,f71])).
% 6.39/1.34 fof(f75,plain,(
% 6.39/1.34 product(a20,a11)=a19),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f56,f37])).
% 6.39/1.34 fof(f76,plain,(
% 6.39/1.34 product(a19,a15)=a18),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f55,f37])).
% 6.39/1.34 fof(f77,plain,(
% 6.39/1.34 product(a18,a9)=a17),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f54,f37])).
% 6.39/1.34 fof(f79,plain,(
% 6.39/1.34 product(a16,a5)=a15),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f52,f37])).
% 6.39/1.34 fof(f80,plain,(
% 6.39/1.34 product(a15,a17)=a14),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f51,f37])).
% 6.39/1.34 fof(f83,plain,(
% 6.39/1.34 product(a12,a5)=a11),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f48,f37])).
% 6.39/1.34 fof(f84,plain,(
% 6.39/1.34 product(a11,a7)=a10),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f47,f37])).
% 6.39/1.34 fof(f85,plain,(
% 6.39/1.34 product(a10,a17)=a9),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f46,f37])).
% 6.39/1.34 fof(f86,plain,(
% 6.39/1.34 product(a9,a5)=a8),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f45,f37])).
% 6.39/1.34 fof(f87,plain,(
% 6.39/1.34 product(a8,a19)=a7),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f44,f37])).
% 6.39/1.34 fof(f89,plain,(
% 6.39/1.34 product(a5,a11)=a4),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f42,f37])).
% 6.39/1.34 fof(f91,plain,(
% 6.39/1.34 product(a3,a25)=a2),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f40,f37])).
% 6.39/1.34 fof(f92,plain,(
% 6.39/1.34 product(a2,a31)=a1),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f39,f37])).
% 6.39/1.34 fof(f94,plain,(
% 6.39/1.34 product(a21,a29)=a20),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f57,f37])).
% 6.39/1.34 fof(f95,plain,(
% 6.39/1.34 product(a22,a25)=a21),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f58,f37])).
% 6.39/1.34 fof(f96,plain,(
% 6.39/1.34 product(a23,a31)=a22),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f59,f37])).
% 6.39/1.34 fof(f97,plain,(
% 6.39/1.34 product(a24,a21)=a23),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f60,f37])).
% 6.39/1.34 fof(f98,plain,(
% 6.39/1.34 product(a25,a3)=a24),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f61,f37])).
% 6.39/1.34 fof(f99,plain,(
% 6.39/1.34 product(a26,a23)=a25),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f62,f37])).
% 6.39/1.34 fof(f100,plain,(
% 6.39/1.34 product(a27,a1)=a26),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f63,f37])).
% 6.39/1.34 fof(f102,plain,(
% 6.39/1.34 product(a29,a3)=a28),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f65,f37])).
% 6.39/1.34 fof(f103,plain,(
% 6.39/1.34 product(a30,a1)=a29),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f66,f37])).
% 6.39/1.34 fof(f104,plain,(
% 6.39/1.34 product(a31,a23)=a30),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f67,f37])).
% 6.39/1.34 fof(f105,plain,(
% 6.39/1.34 product(a32,a3)=a31),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f68,f37])).
% 6.39/1.34 fof(f106,plain,(
% 6.39/1.34 product(a1,a21)=a32),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f69,f37])).
% 6.39/1.34 fof(f112,plain,(
% 6.39/1.34 ![X0]: (product(product(a31,X0),a3)=product(a32,product(X0,a3)))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f68,f38])).
% 6.39/1.34 fof(f113,plain,(
% 6.39/1.34 ![X0]: (product(product(a30,X0),a23)=product(a31,product(X0,a23)))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f67,f38])).
% 6.39/1.34 fof(f116,plain,(
% 6.39/1.34 ![X0]: (product(product(a27,X0),a21)=product(a28,product(X0,a21)))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f64,f38])).
% 6.39/1.34 fof(f121,plain,(
% 6.39/1.34 ![X0]: (product(product(a22,X0),a31)=product(a23,product(X0,a31)))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f59,f38])).
% 6.39/1.34 fof(f147,plain,(
% 6.39/1.34 ![X0,X1]: (product(product(X0,X1),X0)=product(X0,product(X1,X0)))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f36,f38])).
% 6.39/1.34 fof(f149,plain,(
% 6.39/1.34 ![X0]: (product(product(X0,a31),a3)=product(product(X0,a3),a32))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f68,f38])).
% 6.39/1.34 fof(f157,plain,(
% 6.39/1.34 ![X0]: (product(product(X0,a23),a21)=product(product(X0,a21),a24))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f60,f38])).
% 6.39/1.34 fof(f182,plain,(
% 6.39/1.34 ![X0]: (product(product(X0,a2),a25)=product(product(X0,a25),a3))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f40,f38])).
% 6.39/1.34 fof(f183,plain,(
% 6.39/1.34 ![X0]: (product(product(X0,a1),a31)=product(product(X0,a31),a2))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f39,f38])).
% 6.39/1.34 fof(f216,plain,(
% 6.39/1.34 ![X0]: (product(product(a8,X0),a19)=product(a7,product(X0,a19)))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f87,f38])).
% 6.39/1.34 fof(f231,plain,(
% 6.39/1.34 ![X0]: (product(product(a2,X0),a31)=product(a1,product(X0,a31)))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f92,f38])).
% 6.39/1.34 fof(f236,plain,(
% 6.39/1.34 ![X0]: (product(product(X0,a22),a25)=product(product(X0,a25),a21))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f95,f38])).
% 6.39/1.34 fof(f245,plain,(
% 6.39/1.34 ![X0]: (product(product(X0,a25),a3)=product(product(X0,a3),a24))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f98,f38])).
% 6.39/1.34 fof(f277,plain,(
% 6.39/1.34 product(a30,a31)=product(a31,product(a23,a31))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f104,f147])).
% 6.39/1.34 fof(f333,plain,(
% 6.39/1.34 product(a2,a3)=product(a3,product(a25,a3))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f91,f147])).
% 6.39/1.34 fof(f347,plain,(
% 6.39/1.34 product(a30,a31)=product(a31,a22)),
% 6.39/1.34 inference(forward_demodulation,[status(thm)],[f96,f277])).
% 6.39/1.34 fof(f360,plain,(
% 6.39/1.34 product(a2,a3)=product(a3,a24)),
% 6.39/1.34 inference(forward_demodulation,[status(thm)],[f98,f333])).
% 6.39/1.34 fof(f471,plain,(
% 6.39/1.34 product(a29,a23)=product(a31,product(a1,a23))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f103,f113])).
% 6.39/1.34 fof(f705,plain,(
% 6.39/1.34 product(a26,a21)=product(a28,product(a1,a21))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f100,f116])).
% 6.39/1.34 fof(f717,plain,(
% 6.39/1.34 product(a26,a21)=product(a28,a32)),
% 6.39/1.34 inference(forward_demodulation,[status(thm)],[f106,f705])).
% 6.39/1.34 fof(f1119,plain,(
% 6.39/1.34 product(a21,a31)=product(a23,product(a25,a31))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f95,f121])).
% 6.39/1.34 fof(f6134,plain,(
% 6.39/1.34 product(a1,a3)=product(product(a2,a3),a32)),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f92,f149])).
% 6.39/1.34 fof(f6168,plain,(
% 6.39/1.34 product(a1,a3)=product(product(a3,a24),a32)),
% 6.39/1.34 inference(forward_demodulation,[status(thm)],[f360,f6134])).
% 6.39/1.34 fof(f6688,plain,(
% 6.39/1.34 product(a25,a21)=product(product(a26,a21),a24)),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f99,f157])).
% 6.39/1.34 fof(f10027,plain,(
% 6.39/1.34 product(a30,a31)=product(product(a29,a31),a2)),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f66,f183])).
% 6.39/1.34 fof(f10068,plain,(
% 6.39/1.34 product(a31,a22)=product(product(a29,a31),a2)),
% 6.39/1.34 inference(forward_demodulation,[status(thm)],[f347,f10027])).
% 6.39/1.34 fof(f11968,plain,(
% 6.39/1.34 product(a9,a19)=product(a7,product(a5,a19))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f45,f216])).
% 6.39/1.34 fof(f12835,plain,(
% 6.39/1.34 product(a3,a31)=product(a1,product(a25,a31))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f40,f231])).
% 6.39/1.34 fof(f13738,plain,(
% 6.39/1.34 ![X0]: (product(product(X0,a2),a25)=product(product(X0,a3),a24))),
% 6.39/1.34 inference(backward_demodulation,[status(thm)],[f245,f182])).
% 6.39/1.34 fof(f14104,plain,(
% 6.39/1.34 product(product(a31,a22),a25)=product(product(product(a29,a31),a3),a24)),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f10068,f13738])).
% 6.39/1.34 fof(f14149,plain,(
% 6.39/1.34 product(product(a31,a25),a21)=product(product(product(a29,a31),a3),a24)),
% 6.39/1.34 inference(forward_demodulation,[status(thm)],[f236,f14104])).
% 6.39/1.34 fof(f14150,plain,(
% 6.39/1.34 product(product(a31,a25),a21)=product(product(product(a29,a3),a32),a24)),
% 6.39/1.34 inference(forward_demodulation,[status(thm)],[f149,f14149])).
% 6.39/1.34 fof(f14151,plain,(
% 6.39/1.34 product(product(a31,a25),a21)=product(product(a28,a32),a24)),
% 6.39/1.34 inference(forward_demodulation,[status(thm)],[f102,f14150])).
% 6.39/1.34 fof(f14152,plain,(
% 6.39/1.34 product(product(a31,a25),a21)=product(product(a26,a21),a24)),
% 6.39/1.34 inference(forward_demodulation,[status(thm)],[f717,f14151])).
% 6.39/1.34 fof(f14153,plain,(
% 6.39/1.34 product(product(a31,a25),a21)=product(a25,a21)),
% 6.39/1.34 inference(forward_demodulation,[status(thm)],[f6688,f14152])).
% 6.39/1.34 fof(f14341,plain,(
% 6.39/1.34 product(product(a25,a21),a21)=product(a31,a25)),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f14153,f37])).
% 6.39/1.34 fof(f14359,plain,(
% 6.39/1.34 a25=product(a31,a25)),
% 6.39/1.34 inference(forward_demodulation,[status(thm)],[f37,f14341])).
% 6.39/1.34 fof(f14364,plain,(
% 6.39/1.34 product(a25,a3)=product(a32,product(a25,a3))),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f14359,f112])).
% 6.39/1.34 fof(f14378,plain,(
% 6.39/1.34 product(a25,a25)=a31),
% 6.39/1.34 inference(paramodulation,[status(thm)],[f14359,f37])).
% 6.39/1.34 fof(f14382,plain,(
% 6.39/1.34 a24=product(a32,product(a25,a3))),
% 6.39/1.34 inference(forward_demodulation,[status(thm)],[f98,f14364])).
% 6.39/1.34 fof(f14383,plain,(
% 6.39/1.34 a24=product(a32,a24)),
% 6.39/1.34 inference(forward_demodulation,[status(thm)],[f98,f14382])).
% 6.39/1.34 fof(f14398,plain,(
% 6.39/1.34 a25=a31),
% 6.39/1.34 inference(forward_demodulation,[status(thm)],[f36,f14378])).
% 6.39/1.34 fof(f14412,plain,(
% 6.39/1.34 product(a3,a31)=product(a1,product(a31,a31))),
% 6.39/1.34 inference(backward_demodulation,[status(thm)],[f14398,f12835])).
% 6.39/1.34 fof(f14426,plain,(
% 6.39/1.34 product(a21,a31)=product(a23,product(a31,a31))),
% 6.39/1.34 inference(backward_demodulation,[status(thm)],[f14398,f1119])).
% 6.39/1.35 fof(f14441,plain,(
% 6.39/1.35 product(a22,a31)=a21),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14398,f95])).
% 6.39/1.35 fof(f14443,plain,(
% 6.39/1.35 product(a31,a23)=a26),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14398,f62])).
% 6.39/1.35 fof(f14447,plain,(
% 6.39/1.35 sF1_fnc=tuple(a2,a31,a32,a3,a31,a26,a4,a29,a30,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a27,a28)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14398,f72])).
% 6.39/1.35 fof(f14448,plain,(
% 6.39/1.35 sF0_fnc=tuple(a1,a30,a31,a2,a24,a31,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14398,f71])).
% 6.39/1.35 fof(f14456,plain,(
% 6.39/1.35 product(a3,a31)=product(a1,a31)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f14412])).
% 6.39/1.35 fof(f14457,plain,(
% 6.39/1.35 product(a3,a31)=a2),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f39,f14456])).
% 6.39/1.35 fof(f14467,plain,(
% 6.39/1.35 product(a21,a31)=product(a23,a31)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f14426])).
% 6.39/1.35 fof(f14468,plain,(
% 6.39/1.35 product(a21,a31)=a22),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f96,f14467])).
% 6.39/1.35 fof(f14474,plain,(
% 6.39/1.35 a26=a30),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14443,f104])).
% 6.39/1.35 fof(f14488,plain,(
% 6.39/1.35 product(a26,a23)=a31),
% 6.39/1.35 inference(paramodulation,[status(thm)],[f14443,f37])).
% 6.39/1.35 fof(f14496,plain,(
% 6.39/1.35 sF0_fnc=tuple(a1,a26,a31,a2,a24,a31,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14474,f14448])).
% 6.39/1.35 fof(f14497,plain,(
% 6.39/1.35 sF1_fnc=tuple(a2,a31,a32,a3,a31,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a27,a28)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14474,f14447])).
% 6.39/1.35 fof(f14516,plain,(
% 6.39/1.35 product(a26,a1)=a29),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14474,f103])).
% 6.39/1.35 fof(f14542,plain,(
% 6.39/1.35 product(a24,a24)=a32),
% 6.39/1.35 inference(paramodulation,[status(thm)],[f14383,f37])).
% 6.39/1.35 fof(f14558,plain,(
% 6.39/1.35 a24=a32),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f14542])).
% 6.39/1.35 fof(f14561,plain,(
% 6.39/1.35 product(a1,a3)=product(product(a3,a24),a24)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14558,f6168])).
% 6.39/1.35 fof(f14576,plain,(
% 6.39/1.35 product(a24,a3)=a31),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14558,f105])).
% 6.39/1.35 fof(f14577,plain,(
% 6.39/1.35 product(a24,a21)=a1),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14558,f69])).
% 6.39/1.35 fof(f14579,plain,(
% 6.39/1.35 product(a1,a3)=a3),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f37,f14561])).
% 6.39/1.35 fof(f14588,plain,(
% 6.39/1.35 a23=a1),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f97,f14577])).
% 6.39/1.35 fof(f14596,plain,(
% 6.39/1.35 product(a29,a23)=product(a31,product(a23,a23))),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14588,f471])).
% 6.39/1.35 fof(f14603,plain,(
% 6.39/1.35 product(a27,a23)=a26),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14588,f100])).
% 6.39/1.35 fof(f14610,plain,(
% 6.39/1.35 product(a29,a23)=product(a31,a23)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f14596])).
% 6.39/1.35 fof(f14611,plain,(
% 6.39/1.35 product(a29,a23)=a26),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14443,f14610])).
% 6.39/1.35 fof(f14696,plain,(
% 6.39/1.35 a21=a23),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14441,f59])).
% 6.39/1.35 fof(f14716,plain,(
% 6.39/1.35 a21=a1),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14696,f14588])).
% 6.39/1.35 fof(f14733,plain,(
% 6.39/1.35 product(a21,a21)=a24),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14696,f60])).
% 6.39/1.35 fof(f14742,plain,(
% 6.39/1.35 a21=a24),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f14733])).
% 6.39/1.35 fof(f14745,plain,(
% 6.39/1.35 a21=a32),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14742,f14558])).
% 6.39/1.35 fof(f14768,plain,(
% 6.39/1.35 product(a26,a21)=a31),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14696,f14488])).
% 6.39/1.35 fof(f14785,plain,(
% 6.39/1.35 product(a26,a21)=a29),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14716,f14516])).
% 6.39/1.35 fof(f14811,plain,(
% 6.39/1.35 product(a31,a3)=a28),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14817,f102])).
% 6.39/1.35 fof(f14812,plain,(
% 6.39/1.35 product(a21,a31)=a20),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14817,f94])).
% 6.39/1.35 fof(f14816,plain,(
% 6.39/1.35 product(a3,a31)=a4),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14817,f41])).
% 6.39/1.35 fof(f14817,plain,(
% 6.39/1.35 a31=a29),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14768,f14785])).
% 6.39/1.35 fof(f14834,plain,(
% 6.39/1.35 a2=a4),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14457,f14816])).
% 6.39/1.35 fof(f14850,plain,(
% 6.39/1.35 product(a5,a11)=a2),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14834,f89])).
% 6.39/1.35 fof(f14851,plain,(
% 6.39/1.35 product(a2,a11)=a5),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14834,f42])).
% 6.39/1.35 fof(f14879,plain,(
% 6.39/1.35 product(a21,a3)=a3),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14716,f14579])).
% 6.39/1.35 fof(f14890,plain,(
% 6.39/1.35 product(a3,a3)=a21),
% 6.39/1.35 inference(paramodulation,[status(thm)],[f14879,f37])).
% 6.39/1.35 fof(f14902,plain,(
% 6.39/1.35 a3=a21),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f14890])).
% 6.39/1.35 fof(f14906,plain,(
% 6.39/1.35 a3=a32),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14902,f14745])).
% 6.39/1.35 fof(f14907,plain,(
% 6.39/1.35 a3=a24),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14902,f14742])).
% 6.39/1.35 fof(f14908,plain,(
% 6.39/1.35 a3=a1),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14902,f14716])).
% 6.39/1.35 fof(f14909,plain,(
% 6.39/1.35 a3=a23),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14902,f14696])).
% 6.39/1.35 fof(f14911,plain,(
% 6.39/1.35 product(a3,a31)=a22),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14902,f14468])).
% 6.39/1.35 fof(f14918,plain,(
% 6.39/1.35 a2=a22),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14457,f14911])).
% 6.39/1.35 fof(f14921,plain,(
% 6.39/1.35 sF0_fnc=tuple(a1,a26,a31,a2,a24,a31,a3,a28,a31,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14817,f14496])).
% 6.39/1.35 fof(f14922,plain,(
% 6.39/1.35 sF0_fnc=tuple(a1,a26,a31,a2,a24,a31,a3,a28,a31,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14834,f14921])).
% 6.39/1.35 fof(f14923,plain,(
% 6.39/1.35 sF0_fnc=tuple(a1,a26,a31,a2,a24,a31,a3,a28,a31,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a3,a22,a23,a26,a27)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14902,f14922])).
% 6.39/1.35 fof(f14924,plain,(
% 6.39/1.35 sF1_fnc=tuple(a2,a31,a3,a3,a31,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a27,a28)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14906,f14497])).
% 6.39/1.35 fof(f14925,plain,(
% 6.39/1.35 sF1_fnc=tuple(a2,a31,a3,a3,a31,a26,a2,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a27,a28)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14834,f14924])).
% 6.39/1.35 fof(f14926,plain,(
% 6.39/1.35 sF1_fnc=tuple(a2,a31,a3,a3,a31,a26,a2,a31,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a27,a28)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14817,f14925])).
% 6.39/1.35 fof(f14927,plain,(
% 6.39/1.35 sF1_fnc=tuple(a2,a31,a3,a3,a31,a26,a2,a31,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a3,a22,a23,a24,a27,a28)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14902,f14926])).
% 6.39/1.35 fof(f14944,plain,(
% 6.39/1.35 sF1_fnc=tuple(a2,a31,a3,a3,a31,a26,a2,a31,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a3,a22,a23,a3,a27,a28)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14907,f14927])).
% 6.39/1.35 fof(f14945,plain,(
% 6.39/1.35 sF0_fnc=tuple(a1,a26,a31,a2,a3,a31,a3,a28,a31,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a3,a22,a23,a26,a27)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14907,f14923])).
% 6.39/1.35 fof(f14946,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a26,a31,a2,a3,a31,a3,a28,a31,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a3,a22,a23,a26,a27)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14908,f14945])).
% 6.39/1.35 fof(f14947,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a26,a31,a2,a3,a31,a3,a28,a31,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a3,a22,a3,a26,a27)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14909,f14946])).
% 6.39/1.35 fof(f14948,plain,(
% 6.39/1.35 sF1_fnc=tuple(a2,a31,a3,a3,a31,a26,a2,a31,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a3,a22,a3,a3,a27,a28)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14909,f14944])).
% 6.39/1.35 fof(f14949,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a26,a31,a2,a3,a31,a3,a28,a31,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a3,a2,a3,a26,a27)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14918,f14947])).
% 6.39/1.35 fof(f14953,plain,(
% 6.39/1.35 product(a3,a3)=a31),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14907,f14576])).
% 6.39/1.35 fof(f14954,plain,(
% 6.39/1.35 a3=a29),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14960,f14817])).
% 6.39/1.35 fof(f14956,plain,(
% 6.39/1.35 product(a3,a3)=a2),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14960,f14457])).
% 6.39/1.35 fof(f14960,plain,(
% 6.39/1.35 a3=a31),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f14953])).
% 6.39/1.35 fof(f14961,plain,(
% 6.39/1.35 a3=a2),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f14956])).
% 6.39/1.35 fof(f14964,plain,(
% 6.39/1.35 a3=a22),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f14961,f14918])).
% 6.39/1.35 fof(f14966,plain,(
% 6.39/1.35 product(a3,a23)=a26),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14954,f14611])).
% 6.39/1.35 fof(f14967,plain,(
% 6.39/1.35 product(a3,a3)=a26),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14909,f14966])).
% 6.39/1.35 fof(f14969,plain,(
% 6.39/1.35 a3=a26),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f14967])).
% 6.39/1.35 fof(f14970,plain,(
% 6.39/1.35 product(a27,a3)=a26),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14909,f14603])).
% 6.39/1.35 fof(f14971,plain,(
% 6.39/1.35 product(a27,a3)=a3),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14969,f14970])).
% 6.39/1.35 fof(f14982,plain,(
% 6.39/1.35 product(a3,a3)=a27),
% 6.39/1.35 inference(paramodulation,[status(thm)],[f14971,f37])).
% 6.39/1.35 fof(f14994,plain,(
% 6.39/1.35 a3=a27),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f14982])).
% 6.39/1.35 fof(f15034,plain,(
% 6.39/1.35 product(a3,a3)=a28),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14960,f14811])).
% 6.39/1.35 fof(f15035,plain,(
% 6.39/1.35 a3=a28),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f15034])).
% 6.39/1.35 fof(f15036,plain,(
% 6.39/1.35 product(a3,a31)=a20),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14902,f14812])).
% 6.39/1.35 fof(f15037,plain,(
% 6.39/1.35 product(a3,a3)=a20),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14960,f15036])).
% 6.39/1.35 fof(f15048,plain,(
% 6.39/1.35 product(a3,a11)=a19),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15050,f75])).
% 6.39/1.35 fof(f15050,plain,(
% 6.39/1.35 a3=a20),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f15037])).
% 6.39/1.35 fof(f15060,plain,(
% 6.39/1.35 product(a5,a11)=a3),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14961,f14850])).
% 6.39/1.35 fof(f15080,plain,(
% 6.39/1.35 product(a3,a11)=a5),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14961,f14851])).
% 6.39/1.35 fof(f15101,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a31,a3,a3,a31,a26,a2,a31,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a3,a22,a3,a3,a27,a28)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14961,f14948])).
% 6.39/1.35 fof(f15102,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a31,a26,a2,a31,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a3,a22,a3,a3,a27,a28)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14960,f15101])).
% 6.39/1.35 fof(f15103,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a26,a2,a31,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a3,a22,a3,a3,a27,a28)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14960,f15102])).
% 6.39/1.35 fof(f15104,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a2,a31,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a3,a22,a3,a3,a27,a28)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14969,f15103])).
% 6.39/1.35 fof(f15105,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a31,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a3,a22,a3,a3,a27,a28)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14961,f15104])).
% 6.39/1.35 fof(f15106,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a3,a22,a3,a3,a27,a28)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14960,f15105])).
% 6.39/1.35 fof(f15107,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a3,a22,a3,a3,a27,a28)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14969,f15106])).
% 6.39/1.35 fof(f15108,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a15,a16,a7,a8,a19,a3,a9,a10,a17,a18,a13,a14,a3,a22,a3,a3,a27,a28)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15050,f15107])).
% 6.39/1.35 fof(f15109,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a15,a16,a7,a8,a19,a3,a9,a10,a17,a18,a13,a14,a3,a3,a3,a3,a27,a28)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14964,f15108])).
% 6.39/1.35 fof(f15110,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a15,a16,a7,a8,a19,a3,a9,a10,a17,a18,a13,a14,a3,a3,a3,a3,a3,a28)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14994,f15109])).
% 6.39/1.35 fof(f15111,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a15,a16,a7,a8,a19,a3,a9,a10,a17,a18,a13,a14,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15035,f15110])).
% 6.39/1.35 fof(f15112,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a31,a2,a3,a31,a3,a28,a31,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a3,a2,a3,a26,a27)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14969,f14949])).
% 6.39/1.35 fof(f15113,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a2,a3,a31,a3,a28,a31,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a3,a2,a3,a26,a27)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14960,f15112])).
% 6.39/1.35 fof(f15114,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a31,a3,a28,a31,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a3,a2,a3,a26,a27)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14961,f15113])).
% 6.39/1.35 fof(f15115,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a28,a31,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a3,a2,a3,a26,a27)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14960,f15114])).
% 6.39/1.35 fof(f15116,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a31,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a3,a2,a3,a26,a27)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15035,f15115])).
% 6.39/1.35 fof(f15117,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a2,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a3,a2,a3,a26,a27)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14960,f15116])).
% 6.39/1.35 fof(f15118,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a3,a2,a3,a26,a27)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14961,f15117])).
% 6.39/1.35 fof(f15119,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a3,a3,a2,a3,a26,a27)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15050,f15118])).
% 6.39/1.35 fof(f15120,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a3,a3,a3,a3,a26,a27)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14961,f15119])).
% 6.39/1.35 fof(f15121,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a3,a3,a3,a3,a3,a27)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14969,f15120])).
% 6.39/1.35 fof(f15122,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f14994,f15121])).
% 6.39/1.35 fof(f15133,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a10,a11,a5,a14,a15,a6,a7,a18,a5,a8,a9,a16,a17,a12,a13,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15188,f15122])).
% 6.39/1.35 fof(f15134,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a15,a16,a7,a8,a5,a3,a9,a10,a17,a18,a13,a14,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15188,f15111])).
% 6.39/1.35 fof(f15135,plain,(
% 6.39/1.35 product(a9,a19)=product(a7,product(a5,a5))),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15188,f11968])).
% 6.39/1.35 fof(f15180,plain,(
% 6.39/1.35 product(a8,a5)=a7),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15188,f87])).
% 6.39/1.35 fof(f15183,plain,(
% 6.39/1.35 product(a5,a15)=a18),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15188,f76])).
% 6.39/1.35 fof(f15184,plain,(
% 6.39/1.35 product(a18,a15)=a5),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15188,f55])).
% 6.39/1.35 fof(f15185,plain,(
% 6.39/1.35 product(a16,a5)=a17),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15188,f53])).
% 6.39/1.35 fof(f15186,plain,(
% 6.39/1.35 product(a12,a5)=a13),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15188,f49])).
% 6.39/1.35 fof(f15188,plain,(
% 6.39/1.35 a5=a19),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15080,f15048])).
% 6.39/1.35 fof(f15189,plain,(
% 6.39/1.35 product(a9,a5)=product(a7,product(a5,a5))),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15188,f15135])).
% 6.39/1.35 fof(f15190,plain,(
% 6.39/1.35 a8=product(a7,product(a5,a5))),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f86,f15189])).
% 6.39/1.35 fof(f15191,plain,(
% 6.39/1.35 a8=product(a7,a5)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f15190])).
% 6.39/1.35 fof(f15241,plain,(
% 6.39/1.35 a15=a17),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f79,f15185])).
% 6.39/1.35 fof(f15242,plain,(
% 6.39/1.35 a11=a13),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f83,f15186])).
% 6.39/1.35 fof(f15271,plain,(
% 6.39/1.35 product(a10,a15)=a9),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15241,f85])).
% 6.39/1.35 fof(f15272,plain,(
% 6.39/1.35 product(a15,a15)=a14),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15241,f80])).
% 6.39/1.35 fof(f15273,plain,(
% 6.39/1.35 product(a18,a9)=a15),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15241,f77])).
% 6.39/1.35 fof(f15274,plain,(
% 6.39/1.35 product(a15,a9)=a18),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15241,f54])).
% 6.39/1.35 fof(f15305,plain,(
% 6.39/1.35 a15=a14),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f15272])).
% 6.39/1.35 fof(f15313,plain,(
% 6.39/1.35 product(a11,a7)=a14),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15242,f50])).
% 6.39/1.35 fof(f15318,plain,(
% 6.39/1.35 a10=a14),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f84,f15313])).
% 6.39/1.35 fof(f15330,plain,(
% 6.39/1.35 product(a15,a7)=a11),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15331,f47])).
% 6.39/1.35 fof(f15331,plain,(
% 6.39/1.35 a10=a15),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15305,f15318])).
% 6.39/1.35 fof(f15346,plain,(
% 6.39/1.35 product(a8,a5)=a7),
% 6.39/1.35 inference(paramodulation,[status(thm)],[f15191,f37])).
% 6.39/1.35 fof(f15370,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a15,a11,a5,a14,a15,a6,a7,a18,a5,a8,a9,a16,a17,a12,a13,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15331,f15133])).
% 6.39/1.35 fof(f15371,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a15,a11,a5,a15,a15,a6,a7,a18,a5,a8,a9,a16,a17,a12,a13,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15305,f15370])).
% 6.39/1.35 fof(f15372,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a15,a11,a5,a15,a15,a6,a7,a18,a5,a8,a9,a16,a15,a12,a13,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15241,f15371])).
% 6.39/1.35 fof(f15373,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a15,a11,a5,a15,a15,a6,a7,a18,a5,a8,a9,a16,a15,a12,a11,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15242,f15372])).
% 6.39/1.35 fof(f15374,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a15,a16,a7,a8,a5,a3,a9,a15,a17,a18,a13,a14,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15331,f15134])).
% 6.39/1.35 fof(f15375,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a15,a16,a7,a8,a5,a3,a9,a15,a15,a18,a13,a14,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15241,f15374])).
% 6.39/1.35 fof(f15376,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a15,a16,a7,a8,a5,a3,a9,a15,a15,a18,a11,a14,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15242,f15375])).
% 6.39/1.35 fof(f15377,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a15,a16,a7,a8,a5,a3,a9,a15,a15,a18,a11,a15,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15305,f15376])).
% 6.39/1.35 fof(f15380,plain,(
% 6.39/1.35 a7=a9),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15180,f45])).
% 6.39/1.35 fof(f15399,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a15,a16,a7,a8,a5,a3,a7,a15,a15,a18,a11,a15,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15380,f15377])).
% 6.39/1.35 fof(f15400,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a15,a11,a5,a15,a15,a6,a7,a18,a5,a8,a7,a16,a15,a12,a11,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15380,f15373])).
% 6.39/1.35 fof(f15412,plain,(
% 6.39/1.35 a18=a6),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15183,f43])).
% 6.39/1.35 fof(f15470,plain,(
% 6.39/1.35 product(a15,a15)=a9),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15331,f15271])).
% 6.39/1.35 fof(f15471,plain,(
% 6.39/1.35 a7=a15),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15472,f15380])).
% 6.39/1.35 fof(f15472,plain,(
% 6.39/1.35 a15=a9),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f15470])).
% 6.39/1.35 fof(f15475,plain,(
% 6.39/1.35 product(a18,a15)=a15),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15472,f15273])).
% 6.39/1.35 fof(f15476,plain,(
% 6.39/1.35 a7=a5),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15490,f15471])).
% 6.39/1.35 fof(f15477,plain,(
% 6.39/1.35 a5=a9),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15490,f15472])).
% 6.39/1.35 fof(f15489,plain,(
% 6.39/1.35 product(a5,a5)=a16),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15490,f52])).
% 6.39/1.35 fof(f15490,plain,(
% 6.39/1.35 a5=a15),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15184,f15475])).
% 6.39/1.35 fof(f15495,plain,(
% 6.39/1.35 a5=a16),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f15489])).
% 6.39/1.35 fof(f15496,plain,(
% 6.39/1.35 product(a5,a9)=a18),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15490,f15274])).
% 6.39/1.35 fof(f15497,plain,(
% 6.39/1.35 product(a5,a5)=a18),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15477,f15496])).
% 6.39/1.35 fof(f15498,plain,(
% 6.39/1.35 a5=a6),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15499,f15412])).
% 6.39/1.35 fof(f15499,plain,(
% 6.39/1.35 a5=a18),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f15497])).
% 6.39/1.35 fof(f15528,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a5,a16,a7,a8,a5,a3,a7,a15,a15,a18,a11,a15,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15490,f15399])).
% 6.39/1.35 fof(f15529,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a5,a16,a5,a8,a5,a3,a7,a15,a15,a18,a11,a15,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15476,f15528])).
% 6.39/1.35 fof(f15530,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a5,a16,a5,a8,a5,a3,a5,a15,a15,a18,a11,a15,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15476,f15529])).
% 6.39/1.35 fof(f15531,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a5,a16,a5,a8,a5,a3,a5,a5,a15,a18,a11,a15,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15490,f15530])).
% 6.39/1.35 fof(f15532,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a5,a16,a5,a8,a5,a3,a5,a5,a5,a18,a11,a15,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15490,f15531])).
% 6.39/1.35 fof(f15533,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a5,a16,a5,a8,a5,a3,a5,a5,a5,a5,a11,a15,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15499,f15532])).
% 6.39/1.35 fof(f15534,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a5,a16,a5,a8,a5,a3,a5,a5,a5,a5,a11,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15490,f15533])).
% 6.39/1.35 fof(f15535,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a5,a15,a15,a6,a7,a18,a5,a8,a7,a16,a15,a12,a11,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15490,f15400])).
% 6.39/1.35 fof(f15536,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a5,a5,a15,a6,a7,a18,a5,a8,a7,a16,a15,a12,a11,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15490,f15535])).
% 6.39/1.35 fof(f15537,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a5,a5,a5,a6,a7,a18,a5,a8,a7,a16,a15,a12,a11,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15490,f15536])).
% 6.39/1.35 fof(f15538,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a5,a5,a5,a6,a5,a18,a5,a8,a7,a16,a15,a12,a11,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15476,f15537])).
% 6.39/1.35 fof(f15539,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a5,a5,a5,a6,a5,a5,a5,a8,a7,a16,a15,a12,a11,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15499,f15538])).
% 6.39/1.35 fof(f15540,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a5,a5,a5,a6,a5,a5,a5,a8,a5,a16,a15,a12,a11,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15476,f15539])).
% 6.39/1.35 fof(f15541,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a5,a5,a5,a6,a5,a5,a5,a8,a5,a16,a5,a12,a11,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15490,f15540])).
% 6.39/1.35 fof(f15543,plain,(
% 6.39/1.35 product(a5,a7)=a11),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15490,f15330])).
% 6.39/1.35 fof(f15544,plain,(
% 6.39/1.35 product(a5,a5)=a11),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15476,f15543])).
% 6.39/1.35 fof(f15545,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a5,a5,a5,a6,a5,a5,a5,a8,a5,a16,a5,a12,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15557,f15541])).
% 6.39/1.35 fof(f15546,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a11,a12,a6,a5,a16,a5,a8,a5,a3,a5,a5,a5,a5,a5,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15557,f15534])).
% 6.39/1.35 fof(f15549,plain,(
% 6.39/1.35 product(a5,a5)=a3),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15557,f15060])).
% 6.39/1.35 fof(f15556,plain,(
% 6.39/1.35 product(a5,a5)=a12),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15557,f48])).
% 6.39/1.35 fof(f15557,plain,(
% 6.39/1.35 a5=a11),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f15544])).
% 6.39/1.35 fof(f15558,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a5,a5,a5,a5,a6,a5,a5,a5,a8,a5,a16,a5,a12,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15557,f15545])).
% 6.39/1.35 fof(f15559,plain,(
% 6.39/1.35 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a5,a12,a6,a5,a16,a5,a8,a5,a3,a5,a5,a5,a5,a5,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15557,f15546])).
% 6.39/1.35 fof(f15560,plain,(
% 6.39/1.35 a5=a3),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f15549])).
% 6.39/1.35 fof(f15564,plain,(
% 6.39/1.35 a5=a12),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f36,f15556])).
% 6.39/1.35 fof(f15567,plain,(
% 6.39/1.35 a3=a6),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15560,f15498])).
% 6.39/1.35 fof(f15568,plain,(
% 6.39/1.35 a3=a16),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15560,f15495])).
% 6.39/1.35 fof(f15575,plain,(
% 6.39/1.35 a7=a3),
% 6.39/1.35 inference(backward_demodulation,[status(thm)],[f15560,f15476])).
% 6.39/1.35 fof(f15578,plain,(
% 6.39/1.35 a3=a12),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15560,f15564])).
% 6.39/1.35 fof(f15604,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a5,a5,a5,a6,a5,a5,a5,a8,a5,a16,a5,a12,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15560,f15558])).
% 6.39/1.35 fof(f15605,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a5,a5,a6,a5,a5,a5,a8,a5,a16,a5,a12,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15560,f15604])).
% 6.39/1.35 fof(f15606,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a5,a6,a5,a5,a5,a8,a5,a16,a5,a12,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15560,f15605])).
% 6.39/1.35 fof(f15607,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a6,a5,a5,a5,a8,a5,a16,a5,a12,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15560,f15606])).
% 6.39/1.35 fof(f15608,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a6,a5,a5,a5,a8,a5,a16,a5,a12,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15560,f15607])).
% 6.39/1.35 fof(f15609,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a5,a5,a8,a5,a16,a5,a12,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15567,f15608])).
% 6.39/1.35 fof(f15610,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a5,a8,a5,a16,a5,a12,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15560,f15609])).
% 6.39/1.35 fof(f15611,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a8,a5,a16,a5,a12,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15560,f15610])).
% 6.39/1.35 fof(f15612,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a8,a5,a16,a5,a12,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15560,f15611])).
% 6.39/1.35 fof(f15613,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a8,a3,a16,a5,a12,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15560,f15612])).
% 6.39/1.35 fof(f15614,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a8,a3,a3,a5,a12,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15568,f15613])).
% 6.39/1.35 fof(f15615,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a8,a3,a3,a3,a12,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15560,f15614])).
% 6.39/1.35 fof(f15616,plain,(
% 6.39/1.35 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a8,a3,a3,a3,a3,a5,a3,a3,a3,a3,a3,a3)),
% 6.39/1.35 inference(forward_demodulation,[status(thm)],[f15578,f15615])).
% 6.39/1.35 fof(f15617,plain,(
% 6.91/1.39 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a8,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15560,f15616])).
% 6.91/1.39 fof(f15625,plain,(
% 6.91/1.39 product(a8,a3)=a7),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15560,f15346])).
% 6.91/1.39 fof(f15626,plain,(
% 6.91/1.39 product(a8,a3)=a3),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15575,f15625])).
% 6.91/1.39 fof(f15637,plain,(
% 6.91/1.39 product(a3,a3)=a8),
% 6.91/1.39 inference(paramodulation,[status(thm)],[f15626,f37])).
% 6.91/1.39 fof(f15649,plain,(
% 6.91/1.39 a3=a8),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f36,f15637])).
% 6.91/1.39 fof(f15651,plain,(
% 6.91/1.39 sF0_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(backward_demodulation,[status(thm)],[f15649,f15617])).
% 6.91/1.39 fof(f15673,plain,(
% 6.91/1.39 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a12,a6,a5,a16,a5,a8,a5,a3,a5,a5,a5,a5,a5,a5,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15560,f15559])).
% 6.91/1.39 fof(f15674,plain,(
% 6.91/1.39 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a12,a6,a5,a16,a5,a8,a5,a3,a5,a5,a5,a5,a5,a5,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15560,f15673])).
% 6.91/1.39 fof(f15675,plain,(
% 6.91/1.39 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a6,a5,a16,a5,a8,a5,a3,a5,a5,a5,a5,a5,a5,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15578,f15674])).
% 6.91/1.39 fof(f15676,plain,(
% 6.91/1.39 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a16,a5,a8,a5,a3,a5,a5,a5,a5,a5,a5,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15567,f15675])).
% 6.91/1.39 fof(f15677,plain,(
% 6.91/1.39 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a16,a5,a8,a5,a3,a5,a5,a5,a5,a5,a5,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15560,f15676])).
% 6.91/1.39 fof(f15678,plain,(
% 6.91/1.39 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a8,a5,a3,a5,a5,a5,a5,a5,a5,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15568,f15677])).
% 6.91/1.39 fof(f15679,plain,(
% 6.91/1.39 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a8,a5,a3,a5,a5,a5,a5,a5,a5,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15560,f15678])).
% 6.91/1.39 fof(f15680,plain,(
% 6.91/1.39 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a3,a5,a5,a5,a5,a5,a5,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15649,f15679])).
% 6.91/1.39 fof(f15681,plain,(
% 6.91/1.39 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a5,a5,a5,a5,a5,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15560,f15680])).
% 6.91/1.39 fof(f15682,plain,(
% 6.91/1.39 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a5,a5,a5,a5,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15560,f15681])).
% 6.91/1.39 fof(f15683,plain,(
% 6.91/1.39 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a5,a5,a5,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15560,f15682])).
% 6.91/1.39 fof(f15684,plain,(
% 6.91/1.39 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a5,a5,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15560,f15683])).
% 6.91/1.39 fof(f15685,plain,(
% 6.91/1.39 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a5,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15560,f15684])).
% 6.91/1.39 fof(f15686,plain,(
% 6.91/1.39 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a5,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15560,f15685])).
% 6.91/1.39 fof(f15687,plain,(
% 6.91/1.39 sF1_fnc=tuple(a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3,a3)),
% 6.91/1.39 inference(forward_demodulation,[status(thm)],[f15560,f15686])).
% 6.91/1.39 fof(f15690,plain,(
% 6.91/1.39 sF1_fnc=sF0_fnc),
% 6.91/1.39 inference(backward_demodulation,[status(thm)],[f15651,f15687])).
% 6.91/1.39 fof(f15691,plain,(
% 6.91/1.39 $false),
% 6.91/1.39 inference(forward_subsumption_resolution,[status(thm)],[f15690,f73])).
% 6.91/1.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.72/1.42 % Elapsed time: 0.985451 seconds
% 0.72/1.42 % CPU time: 7.447062 seconds
% 0.72/1.42 % Total memory used: 173.442 MB
% 0.72/1.42 % Net memory used: 171.844 MB
%------------------------------------------------------------------------------