%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : TOP053-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 : n020.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 0.10s 0.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP053-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n020.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 12:48:48 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.10/0.48 % Refutation found
% 0.10/0.48 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.48 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.48 fof(f1,axiom,(
% 0.10/0.48 (![X]: (product(X,X) = X ))),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f2,axiom,(
% 0.10/0.48 (![X,Y]: (product(product(X,Y),Y) = X ))),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f3,axiom,(
% 0.10/0.48 (![X,Y,Z]: (product(product(X,Y),Z) = product(product(X,Z),product(Y,Z)) ))),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f4,axiom,(
% 0.10/0.48 product(a1,a2) = a3 ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f5,axiom,(
% 0.10/0.48 product(a3,a4) = a5 ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f6,axiom,(
% 0.10/0.48 product(a5,a6) = a7 ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f7,axiom,(
% 0.10/0.48 product(a7,a3) = a8 ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f8,axiom,(
% 0.10/0.48 product(a8,a2) = a9 ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f9,axiom,(
% 0.10/0.48 product(a9,a1) = a10 ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f10,axiom,(
% 0.10/0.48 product(a10,a11) = a12 ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f11,axiom,(
% 0.10/0.48 product(a12,a3) = a13 ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f12,axiom,(
% 0.10/0.48 product(a13,a8) = a6 ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f13,axiom,(
% 0.10/0.48 product(a6,a7) = a2 ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f14,axiom,(
% 0.10/0.48 product(a2,a12) = a14 ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f15,axiom,(
% 0.10/0.48 product(a14,a3) = a15 ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f16,axiom,(
% 0.10/0.48 product(a15,a8) = a4 ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f17,axiom,(
% 0.10/0.48 product(a4,a7) = a11 ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f18,axiom,(
% 0.10/0.48 product(a11,a10) = a1 ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f19,negated_conjecture,(
% 0.10/0.48 tuple(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14) != tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15) ),
% 0.10/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.48 fof(f20,plain,(
% 0.10/0.48 ![X0]: (product(X0,X0)=X0)),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f1])).
% 0.10/0.48 fof(f21,plain,(
% 0.10/0.48 ![X0,X1]: (product(product(X0,X1),X1)=X0)),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f2])).
% 0.10/0.48 fof(f22,plain,(
% 0.10/0.48 ![X0,X1,X2]: (product(product(X0,X1),X2)=product(product(X0,X2),product(X1,X2)))),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f3])).
% 0.10/0.48 fof(f23,plain,(
% 0.10/0.48 product(a1,a2)=a3),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.48 fof(f24,plain,(
% 0.10/0.48 product(a3,a4)=a5),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.48 fof(f25,plain,(
% 0.10/0.48 product(a5,a6)=a7),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.48 fof(f26,plain,(
% 0.10/0.48 product(a7,a3)=a8),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f7])).
% 0.10/0.48 fof(f27,plain,(
% 0.10/0.48 product(a8,a2)=a9),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f8])).
% 0.10/0.48 fof(f28,plain,(
% 0.10/0.48 product(a9,a1)=a10),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f9])).
% 0.10/0.48 fof(f29,plain,(
% 0.10/0.48 product(a10,a11)=a12),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f10])).
% 0.10/0.48 fof(f30,plain,(
% 0.10/0.48 product(a12,a3)=a13),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f11])).
% 0.10/0.48 fof(f31,plain,(
% 0.10/0.48 product(a13,a8)=a6),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f12])).
% 0.10/0.48 fof(f32,plain,(
% 0.10/0.48 product(a6,a7)=a2),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f13])).
% 0.10/0.48 fof(f33,plain,(
% 0.10/0.48 product(a2,a12)=a14),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f14])).
% 0.10/0.48 fof(f34,plain,(
% 0.10/0.48 product(a14,a3)=a15),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.48 fof(f35,plain,(
% 0.10/0.48 product(a15,a8)=a4),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f16])).
% 0.10/0.48 fof(f36,plain,(
% 0.10/0.48 product(a4,a7)=a11),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f17])).
% 0.10/0.48 fof(f37,plain,(
% 0.10/0.48 product(a11,a10)=a1),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f18])).
% 0.10/0.48 fof(f38,plain,(
% 0.10/0.48 ~tuple(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14)=tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15)),
% 0.10/0.48 inference(cnf_transformation,[status(thm)],[f19])).
% 0.10/0.48 fof(f39,definition,(
% 0.10/0.48 sF0_fnc=tuple(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14)),
% 0.10/0.48 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.10/0.48 fof(f40,definition,(
% 0.10/0.48 sF1_fnc=tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15)),
% 0.10/0.48 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 0.10/0.48 fof(f41,plain,(
% 0.10/0.48 ~sF0_fnc=sF1_fnc),
% 0.10/0.48 inference(definition_folding,[],[f38,f40,f39])).
% 0.10/0.48 fof(f43,plain,(
% 0.10/0.48 product(a8,a3)=a7),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f26,f21])).
% 0.10/0.48 fof(f44,plain,(
% 0.10/0.48 product(a7,a6)=a5),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f25,f21])).
% 0.10/0.48 fof(f46,plain,(
% 0.10/0.48 product(a3,a2)=a1),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f23,f21])).
% 0.10/0.48 fof(f48,plain,(
% 0.10/0.48 product(a9,a2)=a8),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f27,f21])).
% 0.10/0.48 fof(f49,plain,(
% 0.10/0.48 product(a10,a1)=a9),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f28,f21])).
% 0.10/0.48 fof(f50,plain,(
% 0.10/0.48 product(a12,a11)=a10),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f29,f21])).
% 0.10/0.48 fof(f52,plain,(
% 0.10/0.48 product(a6,a8)=a13),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f31,f21])).
% 0.10/0.48 fof(f53,plain,(
% 0.10/0.48 product(a2,a7)=a6),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f32,f21])).
% 0.10/0.48 fof(f58,plain,(
% 0.10/0.48 ![X0]: (product(product(a10,X0),a11)=product(a12,product(X0,a11)))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f29,f22])).
% 0.10/0.48 fof(f60,plain,(
% 0.10/0.48 ![X0]: (product(product(a8,X0),a2)=product(a9,product(X0,a2)))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f27,f22])).
% 0.10/0.48 fof(f62,plain,(
% 0.10/0.48 ![X0,X1,X2]: (product(product(product(X0,X1),X2),X1)=product(X0,product(X2,X1)))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f21,f22])).
% 0.10/0.48 fof(f63,plain,(
% 0.10/0.48 ![X0]: (product(product(a7,X0),a3)=product(a8,product(X0,a3)))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f26,f22])).
% 0.10/0.48 fof(f64,plain,(
% 0.10/0.48 ![X0]: (product(product(a5,X0),a6)=product(a7,product(X0,a6)))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f25,f22])).
% 0.10/0.48 fof(f65,plain,(
% 0.10/0.48 ![X0]: (product(product(a3,X0),a4)=product(a5,product(X0,a4)))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f24,f22])).
% 0.10/0.48 fof(f66,plain,(
% 0.10/0.48 ![X0]: (product(product(a1,X0),a2)=product(a3,product(X0,a2)))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f23,f22])).
% 0.10/0.48 fof(f67,plain,(
% 0.10/0.48 ![X0,X1]: (product(product(X0,X1),X0)=product(X0,product(X1,X0)))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f20,f22])).
% 0.10/0.48 fof(f68,plain,(
% 0.10/0.48 ![X0]: (product(product(X0,a6),a7)=product(product(X0,a7),a2))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f32,f22])).
% 0.10/0.48 fof(f70,plain,(
% 0.10/0.48 ![X0]: (product(product(X0,a12),a3)=product(product(X0,a3),a13))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f30,f22])).
% 0.10/0.48 fof(f86,plain,(
% 0.10/0.48 product(a14,a12)=a2),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f33,f21])).
% 0.10/0.48 fof(f89,plain,(
% 0.10/0.48 product(a15,a3)=a14),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f34,f21])).
% 0.10/0.48 fof(f92,plain,(
% 0.10/0.48 product(a4,a8)=a15),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f35,f21])).
% 0.10/0.48 fof(f95,plain,(
% 0.10/0.48 product(a11,a7)=a4),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f36,f21])).
% 0.10/0.48 fof(f98,plain,(
% 0.10/0.48 product(a1,a10)=a11),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f37,f21])).
% 0.10/0.48 fof(f166,plain,(
% 0.10/0.48 product(a1,a11)=product(a11,product(a10,a11))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f37,f67])).
% 0.10/0.48 fof(f182,plain,(
% 0.10/0.48 product(a9,a10)=product(a10,product(a1,a10))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f49,f67])).
% 0.10/0.48 fof(f183,plain,(
% 0.10/0.48 product(a12,a10)=product(a10,product(a11,a10))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f29,f67])).
% 0.10/0.48 fof(f192,plain,(
% 0.10/0.48 product(a5,a7)=product(a7,product(a6,a7))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f44,f67])).
% 0.10/0.48 fof(f193,plain,(
% 0.10/0.48 product(a8,a7)=product(a7,product(a3,a7))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f26,f67])).
% 0.10/0.48 fof(f197,plain,(
% 0.10/0.48 product(a5,a3)=product(a3,product(a4,a3))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f24,f67])).
% 0.10/0.48 fof(f208,plain,(
% 0.10/0.48 product(a1,a11)=product(a11,a12)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f29,f166])).
% 0.10/0.48 fof(f210,plain,(
% 0.10/0.48 product(a9,a10)=product(a10,a11)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f98,f182])).
% 0.10/0.48 fof(f211,plain,(
% 0.10/0.48 product(a9,a10)=a12),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f29,f210])).
% 0.10/0.48 fof(f212,plain,(
% 0.10/0.48 product(a12,a10)=product(a10,a1)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f37,f183])).
% 0.10/0.48 fof(f213,plain,(
% 0.10/0.48 product(a12,a10)=a9),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f49,f212])).
% 0.10/0.48 fof(f217,plain,(
% 0.10/0.48 product(a5,a7)=product(a7,a2)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f32,f192])).
% 0.10/0.48 fof(f250,plain,(
% 0.10/0.48 product(product(a1,a11),a12)=a11),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f208,f21])).
% 0.10/0.48 fof(f256,plain,(
% 0.10/0.48 product(product(a5,a7),a2)=a7),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f217,f21])).
% 0.10/0.48 fof(f337,plain,(
% 0.10/0.48 product(a9,a11)=product(a12,product(a1,a11))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f49,f58])).
% 0.10/0.48 fof(f474,plain,(
% 0.10/0.48 product(a7,a2)=product(a9,product(a3,a2))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f43,f60])).
% 0.10/0.48 fof(f485,plain,(
% 0.10/0.48 product(a5,a7)=product(a9,product(a3,a2))),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f217,f474])).
% 0.10/0.48 fof(f486,plain,(
% 0.10/0.48 product(a5,a7)=product(a9,a1)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f46,f485])).
% 0.10/0.48 fof(f487,plain,(
% 0.10/0.48 product(a5,a7)=a10),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f28,f486])).
% 0.10/0.48 fof(f494,plain,(
% 0.10/0.48 product(a10,a2)=a7),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f487,f256])).
% 0.10/0.48 fof(f495,plain,(
% 0.10/0.48 a10=product(a7,a2)),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f487,f217])).
% 0.10/0.48 fof(f1211,plain,(
% 0.10/0.48 product(product(a9,a11),a12)=product(a12,product(product(a1,a11),a12))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f337,f67])).
% 0.10/0.48 fof(f1217,plain,(
% 0.10/0.48 product(product(a9,a11),a12)=product(a12,a11)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f250,f1211])).
% 0.10/0.48 fof(f1218,plain,(
% 0.10/0.48 product(product(a9,a11),a12)=a10),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f50,f1217])).
% 0.10/0.48 fof(f1470,plain,(
% 0.10/0.48 product(a11,a2)=product(a3,product(a10,a2))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f98,f66])).
% 0.10/0.48 fof(f1487,plain,(
% 0.10/0.48 product(a11,a2)=product(a3,a7)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f494,f1470])).
% 0.10/0.48 fof(f1501,plain,(
% 0.10/0.48 product(product(a3,a7),a2)=a11),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f1487,f21])).
% 0.10/0.48 fof(f1503,plain,(
% 0.10/0.48 product(a11,a7)=product(a3,product(a2,a7))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f1501,f62])).
% 0.10/0.48 fof(f1512,plain,(
% 0.10/0.48 a4=product(a3,product(a2,a7))),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f95,f1503])).
% 0.10/0.48 fof(f1513,plain,(
% 0.10/0.48 a4=product(a3,a6)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f53,f1512])).
% 0.10/0.48 fof(f1518,plain,(
% 0.10/0.48 product(a4,a4)=product(a5,product(a6,a4))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f1513,f65])).
% 0.10/0.48 fof(f1525,plain,(
% 0.10/0.48 product(a4,a6)=a3),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f1513,f21])).
% 0.10/0.48 fof(f1526,plain,(
% 0.10/0.48 a4=product(a5,product(a6,a4))),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f20,f1518])).
% 0.10/0.48 fof(f1531,plain,(
% 0.10/0.48 product(a3,a4)=product(a4,product(a6,a4))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f1525,f67])).
% 0.10/0.48 fof(f1536,plain,(
% 0.10/0.48 a5=product(a4,product(a6,a4))),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f24,f1531])).
% 0.10/0.48 fof(f1552,plain,(
% 0.10/0.48 product(a4,a6)=product(a7,product(product(a6,a4),a6))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f1526,f64])).
% 0.10/0.48 fof(f1561,plain,(
% 0.10/0.48 a3=product(a7,product(product(a6,a4),a6))),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f1525,f1552])).
% 0.10/0.48 fof(f1562,plain,(
% 0.10/0.48 a3=product(a7,product(a6,product(a4,a6)))),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f67,f1561])).
% 0.10/0.48 fof(f1563,plain,(
% 0.10/0.48 a3=product(a7,product(a6,a3))),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f1525,f1562])).
% 0.10/0.48 fof(f1629,plain,(
% 0.10/0.48 product(a3,a3)=product(a8,product(product(a6,a3),a3))),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f1563,f63])).
% 0.10/0.48 fof(f1638,plain,(
% 0.10/0.48 a3=product(a8,product(product(a6,a3),a3))),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f20,f1629])).
% 0.10/0.48 fof(f1639,plain,(
% 0.10/0.48 a3=product(a8,a6)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f21,f1638])).
% 0.10/0.48 fof(f1651,plain,(
% 0.10/0.48 product(a3,a6)=a8),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f1639,f21])).
% 0.10/0.48 fof(f1656,plain,(
% 0.10/0.48 a4=a8),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f1513,f1651])).
% 0.10/0.48 fof(f1663,plain,(
% 0.10/0.48 product(a4,a7)=product(a7,product(a3,a7))),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f1656,f193])).
% 0.10/0.48 fof(f1672,plain,(
% 0.10/0.48 product(a4,a4)=a15),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f1656,f92])).
% 0.10/0.48 fof(f1673,plain,(
% 0.10/0.48 product(a6,a4)=a13),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f1656,f52])).
% 0.10/0.48 fof(f1674,plain,(
% 0.10/0.48 sF1_fnc=tuple(a2,a3,a4,a5,a6,a7,a4,a9,a10,a11,a12,a13,a14,a15)),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f1656,f40])).
% 0.10/0.48 fof(f1675,plain,(
% 0.10/0.48 product(a9,a2)=a4),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f1656,f48])).
% 0.10/0.48 fof(f1676,plain,(
% 0.10/0.48 sF0_fnc=tuple(a1,a2,a3,a4,a5,a6,a7,a4,a9,a10,a11,a12,a13,a14)),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f1656,f39])).
% 0.10/0.48 fof(f1677,plain,(
% 0.10/0.48 product(a4,a3)=a7),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f1656,f43])).
% 0.10/0.48 fof(f1681,plain,(
% 0.10/0.48 product(a7,a3)=a4),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f1656,f26])).
% 0.10/0.48 fof(f1685,plain,(
% 0.10/0.48 a11=product(a7,product(a3,a7))),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f36,f1663])).
% 0.10/0.48 fof(f1695,plain,(
% 0.10/0.48 a4=a15),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f20,f1672])).
% 0.10/0.48 fof(f1698,plain,(
% 0.10/0.48 product(a4,a3)=a14),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f1695,f89])).
% 0.10/0.48 fof(f1712,plain,(
% 0.10/0.48 sF1_fnc=tuple(a2,a3,a4,a5,a6,a7,a4,a9,a10,a11,a12,a13,a14,a4)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f1695,f1674])).
% 0.10/0.48 fof(f1747,plain,(
% 0.10/0.48 product(a5,a3)=product(a3,a7)),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f1677,f197])).
% 0.10/0.48 fof(f1758,plain,(
% 0.10/0.48 sF0_fnc=tuple(a1,a2,a3,a4,a5,a6,a7,a4,a9,a10,a11,a12,a13,a7)),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f1765,f1676])).
% 0.10/0.48 fof(f1760,plain,(
% 0.10/0.48 sF1_fnc=tuple(a2,a3,a4,a5,a6,a7,a4,a9,a10,a11,a12,a13,a7,a4)),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f1765,f1712])).
% 0.10/0.48 fof(f1763,plain,(
% 0.10/0.48 product(a7,a12)=a2),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f1765,f86])).
% 0.10/0.48 fof(f1765,plain,(
% 0.10/0.48 a7=a14),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f1677,f1698])).
% 0.10/0.48 fof(f1790,plain,(
% 0.10/0.48 a5=product(a4,a13)),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f1673,f1536])).
% 0.10/0.48 fof(f1998,plain,(
% 0.10/0.48 product(a2,a3)=product(product(a7,a3),a13)),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f1763,f70])).
% 0.10/0.48 fof(f2023,plain,(
% 0.10/0.48 product(a2,a3)=product(a4,a13)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f1681,f1998])).
% 0.10/0.48 fof(f2024,plain,(
% 0.10/0.48 product(a2,a3)=a5),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f1790,f2023])).
% 0.10/0.48 fof(f2043,plain,(
% 0.10/0.48 product(a5,a3)=a2),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f2024,f21])).
% 0.10/0.48 fof(f2046,plain,(
% 0.10/0.48 a2=product(a3,a7)),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2043,f1747])).
% 0.10/0.48 fof(f2057,plain,(
% 0.10/0.48 a11=product(a7,a2)),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2046,f1685])).
% 0.10/0.48 fof(f2060,plain,(
% 0.10/0.48 product(product(a3,a6),a7)=product(a2,a2)),
% 0.10/0.48 inference(paramodulation,[status(thm)],[f2046,f68])).
% 0.10/0.48 fof(f2068,plain,(
% 0.10/0.48 a11=a10),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f495,f2057])).
% 0.10/0.48 fof(f2070,plain,(
% 0.10/0.48 product(a4,a7)=product(a2,a2)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f1513,f2060])).
% 0.10/0.48 fof(f2071,plain,(
% 0.10/0.48 a11=product(a2,a2)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f36,f2070])).
% 0.10/0.48 fof(f2072,plain,(
% 0.10/0.48 a11=a2),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f20,f2071])).
% 0.10/0.48 fof(f2077,plain,(
% 0.10/0.48 sF1_fnc=tuple(a2,a3,a4,a5,a6,a7,a4,a9,a10,a10,a12,a13,a7,a4)),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2068,f1760])).
% 0.10/0.48 fof(f2078,plain,(
% 0.10/0.48 sF0_fnc=tuple(a1,a2,a3,a4,a5,a6,a7,a4,a9,a10,a10,a12,a13,a7)),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2068,f1758])).
% 0.10/0.48 fof(f2082,plain,(
% 0.10/0.48 product(product(a9,a10),a12)=a10),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2068,f1218])).
% 0.10/0.48 fof(f2092,plain,(
% 0.10/0.48 product(a12,a10)=a10),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2068,f50])).
% 0.10/0.48 fof(f2093,plain,(
% 0.10/0.48 product(a10,a10)=a1),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2068,f37])).
% 0.10/0.48 fof(f2094,plain,(
% 0.10/0.48 product(a4,a7)=a10),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2068,f36])).
% 0.10/0.48 fof(f2101,plain,(
% 0.10/0.48 product(a12,a12)=a10),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f211,f2082])).
% 0.10/0.48 fof(f2102,plain,(
% 0.10/0.48 a12=a10),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f20,f2101])).
% 0.10/0.48 fof(f2114,plain,(
% 0.10/0.48 a9=a10),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f213,f2092])).
% 0.10/0.48 fof(f2115,plain,(
% 0.10/0.48 a10=a1),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f20,f2093])).
% 0.10/0.48 fof(f2117,plain,(
% 0.10/0.48 a2=a10),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2072,f2068])).
% 0.10/0.48 fof(f2131,plain,(
% 0.10/0.48 product(a10,a3)=a13),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2102,f30])).
% 0.10/0.48 fof(f2136,plain,(
% 0.10/0.48 sF1_fnc=tuple(a2,a3,a4,a5,a6,a7,a4,a9,a10,a10,a10,a13,a7,a4)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f2102,f2077])).
% 0.10/0.48 fof(f2137,plain,(
% 0.10/0.48 sF1_fnc=tuple(a2,a3,a4,a5,a6,a7,a4,a9,a10,a10,a9,a13,a7,a4)),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2114,f2136])).
% 0.10/0.48 fof(f2138,plain,(
% 0.10/0.48 a12=a9),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2114,f2102])).
% 0.10/0.48 fof(f2149,plain,(
% 0.10/0.48 product(a9,a2)=a7),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2114,f494])).
% 0.10/0.48 fof(f2155,plain,(
% 0.10/0.48 sF1_fnc=tuple(a2,a3,a4,a5,a6,a7,a4,a9,a9,a10,a9,a13,a7,a4)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f2114,f2137])).
% 0.10/0.48 fof(f2156,plain,(
% 0.10/0.48 sF1_fnc=tuple(a2,a3,a4,a5,a6,a7,a4,a9,a9,a9,a9,a13,a7,a4)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f2114,f2155])).
% 0.10/0.48 fof(f2158,plain,(
% 0.10/0.48 a4=a7),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f1675,f2149])).
% 0.10/0.48 fof(f2159,plain,(
% 0.10/0.48 a9=a1),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2115,f2114])).
% 0.10/0.48 fof(f2160,plain,(
% 0.10/0.48 a12=a1),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2159,f2138])).
% 0.10/0.48 fof(f2164,plain,(
% 0.10/0.48 sF0_fnc=tuple(a1,a2,a3,a4,a5,a6,a7,a4,a1,a10,a10,a12,a13,a7)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f2159,f2078])).
% 0.10/0.48 fof(f2165,plain,(
% 0.10/0.48 sF0_fnc=tuple(a1,a2,a3,a4,a5,a6,a7,a4,a1,a1,a10,a12,a13,a7)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f2115,f2164])).
% 0.10/0.48 fof(f2166,plain,(
% 0.10/0.48 sF0_fnc=tuple(a1,a2,a3,a4,a5,a6,a7,a4,a1,a1,a1,a12,a13,a7)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f2115,f2165])).
% 0.10/0.48 fof(f2167,plain,(
% 0.10/0.48 sF0_fnc=tuple(a1,a2,a3,a4,a5,a6,a7,a4,a1,a1,a1,a1,a13,a7)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f2160,f2166])).
% 0.10/0.48 fof(f2168,plain,(
% 0.10/0.48 sF0_fnc=tuple(a1,a1,a3,a4,a5,a6,a7,a4,a1,a1,a1,a1,a13,a7)),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2184,f2167])).
% 0.10/0.48 fof(f2180,plain,(
% 0.10/0.48 product(a1,a7)=a6),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2184,f53])).
% 0.10/0.48 fof(f2183,plain,(
% 0.10/0.48 product(a1,a1)=a3),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2184,f23])).
% 0.10/0.48 fof(f2184,plain,(
% 0.10/0.48 a2=a1),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f2115,f2117])).
% 0.10/0.48 fof(f2189,plain,(
% 0.10/0.48 a1=a3),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f20,f2183])).
% 0.10/0.48 fof(f2198,plain,(
% 0.10/0.48 product(a4,a6)=a5),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2158,f44])).
% 0.10/0.48 fof(f2201,plain,(
% 0.10/0.48 a3=a5),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f1525,f2198])).
% 0.10/0.48 fof(f2209,plain,(
% 0.10/0.48 product(a4,a4)=a10),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f2158,f2094])).
% 0.10/0.48 fof(f2210,plain,(
% 0.10/0.48 a4=a10),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f20,f2209])).
% 0.10/0.48 fof(f2212,plain,(
% 0.10/0.48 a1=a7),
% 0.10/0.48 inference(backward_demodulation,[status(thm)],[f2220,f2158])).
% 0.10/0.48 fof(f2220,plain,(
% 0.10/0.48 a4=a1),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f2115,f2210])).
% 0.10/0.48 fof(f2222,plain,(
% 0.10/0.48 a1=a5),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f2189,f2201])).
% 0.10/0.48 fof(f2255,plain,(
% 0.10/0.48 product(a1,a3)=a13),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f2115,f2131])).
% 0.10/0.48 fof(f2256,plain,(
% 0.10/0.48 product(a1,a1)=a13),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f2189,f2255])).
% 0.10/0.48 fof(f2258,plain,(
% 0.10/0.48 a1=a13),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f20,f2256])).
% 0.10/0.48 fof(f2272,plain,(
% 0.10/0.48 sF1_fnc=tuple(a1,a3,a4,a5,a6,a7,a4,a9,a9,a9,a9,a13,a7,a4)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f2184,f2156])).
% 0.10/0.48 fof(f2273,plain,(
% 0.10/0.48 sF1_fnc=tuple(a1,a1,a4,a5,a6,a7,a4,a9,a9,a9,a9,a13,a7,a4)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f2189,f2272])).
% 0.10/0.48 fof(f2274,plain,(
% 0.10/0.48 sF1_fnc=tuple(a1,a1,a1,a5,a6,a7,a4,a9,a9,a9,a9,a13,a7,a4)),
% 0.10/0.48 inference(forward_demodulation,[status(thm)],[f2220,f2273])).
% 0.10/0.49 fof(f2275,plain,(
% 0.10/0.49 sF1_fnc=tuple(a1,a1,a1,a1,a6,a7,a4,a9,a9,a9,a9,a13,a7,a4)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2222,f2274])).
% 0.10/0.49 fof(f2276,plain,(
% 0.10/0.49 sF1_fnc=tuple(a1,a1,a1,a1,a6,a1,a4,a9,a9,a9,a9,a13,a7,a4)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2212,f2275])).
% 0.10/0.49 fof(f2277,plain,(
% 0.10/0.49 sF1_fnc=tuple(a1,a1,a1,a1,a6,a1,a1,a9,a9,a9,a9,a13,a7,a4)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2220,f2276])).
% 0.10/0.49 fof(f2278,plain,(
% 0.10/0.49 sF1_fnc=tuple(a1,a1,a1,a1,a6,a1,a1,a1,a9,a9,a9,a13,a7,a4)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2159,f2277])).
% 0.10/0.49 fof(f2279,plain,(
% 0.10/0.49 sF1_fnc=tuple(a1,a1,a1,a1,a6,a1,a1,a1,a1,a9,a9,a13,a7,a4)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2159,f2278])).
% 0.10/0.49 fof(f2280,plain,(
% 0.10/0.49 sF1_fnc=tuple(a1,a1,a1,a1,a6,a1,a1,a1,a1,a1,a9,a13,a7,a4)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2159,f2279])).
% 0.10/0.49 fof(f2281,plain,(
% 0.10/0.49 sF1_fnc=tuple(a1,a1,a1,a1,a6,a1,a1,a1,a1,a1,a1,a13,a7,a4)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2159,f2280])).
% 0.10/0.49 fof(f2282,plain,(
% 0.10/0.49 sF1_fnc=tuple(a1,a1,a1,a1,a6,a1,a1,a1,a1,a1,a1,a1,a7,a4)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2258,f2281])).
% 0.10/0.49 fof(f2283,plain,(
% 0.10/0.49 sF1_fnc=tuple(a1,a1,a1,a1,a6,a1,a1,a1,a1,a1,a1,a1,a1,a4)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2212,f2282])).
% 0.10/0.49 fof(f2284,plain,(
% 0.10/0.49 sF1_fnc=tuple(a1,a1,a1,a1,a6,a1,a1,a1,a1,a1,a1,a1,a1,a1)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2220,f2283])).
% 0.10/0.49 fof(f2297,plain,(
% 0.10/0.49 product(a1,a1)=a6),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2212,f2180])).
% 0.10/0.49 fof(f2298,plain,(
% 0.10/0.49 sF1_fnc=tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1)),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f2299,f2284])).
% 0.10/0.49 fof(f2299,plain,(
% 0.10/0.49 a1=a6),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f20,f2297])).
% 0.10/0.49 fof(f2315,plain,(
% 0.10/0.49 sF0_fnc=tuple(a1,a1,a1,a4,a5,a6,a7,a4,a1,a1,a1,a1,a13,a7)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2189,f2168])).
% 0.10/0.49 fof(f2316,plain,(
% 0.10/0.49 sF0_fnc=tuple(a1,a1,a1,a1,a5,a6,a7,a4,a1,a1,a1,a1,a13,a7)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2220,f2315])).
% 0.10/0.49 fof(f2317,plain,(
% 0.10/0.49 sF0_fnc=tuple(a1,a1,a1,a1,a1,a6,a7,a4,a1,a1,a1,a1,a13,a7)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2222,f2316])).
% 0.10/0.49 fof(f2318,plain,(
% 0.10/0.49 sF0_fnc=tuple(a1,a1,a1,a1,a1,a1,a7,a4,a1,a1,a1,a1,a13,a7)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2299,f2317])).
% 0.10/0.49 fof(f2319,plain,(
% 0.10/0.49 sF0_fnc=tuple(a1,a1,a1,a1,a1,a1,a1,a4,a1,a1,a1,a1,a13,a7)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2212,f2318])).
% 0.10/0.49 fof(f2320,plain,(
% 0.10/0.49 sF0_fnc=tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a13,a7)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2220,f2319])).
% 0.10/0.49 fof(f2321,plain,(
% 0.10/0.49 sF0_fnc=tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a7)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2258,f2320])).
% 0.10/0.49 fof(f2322,plain,(
% 0.10/0.49 sF0_fnc=tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2212,f2321])).
% 0.10/0.49 fof(f2354,plain,(
% 0.10/0.49 sF1_fnc=sF0_fnc),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f2322,f2298])).
% 0.10/0.49 fof(f2355,plain,(
% 0.10/0.49 $false),
% 0.10/0.49 inference(forward_subsumption_resolution,[status(thm)],[f2354,f41])).
% 0.10/0.49 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.50 % Elapsed time: 0.124304 seconds
% 0.10/0.50 % CPU time: 0.856843 seconds
% 0.10/0.50 % Total memory used: 42.041 MB
% 0.10/0.50 % Net memory used: 41.662 MB
%------------------------------------------------------------------------------