%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM017-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 01:42:09 PM UTC 2026
% Result : Unsatisfiable 72.32s 9.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM017-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n009.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 01:59:12 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 72.32/9.52 % Refutation found
% 72.32/9.52 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 72.32/9.52 % SZS output start CNFRefutation for theBenchmark
% 72.32/9.52 fof(f2,axiom,(
% 72.32/9.52 (![X,Y]: (( ~ equalish(X,Y)| equalish(Y,X) ) ))),
% 72.32/9.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.32/9.52 fof(f5,axiom,(
% 72.32/9.52 (![D,B,C,A]: (( ~ equalish(D,B)| ~ product(C,D,A)| product(C,B,A) ) ))),
% 72.32/9.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.32/9.52 fof(f7,axiom,(
% 72.32/9.52 (![B,A,C]: (( ~ equalish(B,A)| ~ divides(C,B)| divides(C,A) ) ))),
% 72.32/9.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.32/9.52 fof(f10,axiom,(
% 72.32/9.52 (![A,B]: (product(A,B,multiply(A,B)) ))),
% 72.32/9.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.32/9.52 fof(f12,axiom,(
% 72.32/9.52 (![A,B,C,D,E,F]: (( ~ product(A,B,C)| ~ product(D,B,E)| ~ product(F,D,A)| product(F,E,C) ) ))),
% 72.32/9.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.32/9.52 fof(f13,axiom,(
% 72.32/9.52 (![A,B,C]: (( ~ product(A,B,C)| product(B,A,C) ) ))),
% 72.32/9.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.32/9.52 fof(f14,axiom,(
% 72.32/9.52 (![A,B,C,D]: (( ~ product(A,B,C)| ~ product(A,D,C)| equalish(B,D) ) ))),
% 72.32/9.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.32/9.52 fof(f17,axiom,(
% 72.32/9.52 (![A,B]: (( ~ divides(A,B)| product(A,second_divided_by_1st(A,B),B) ) ))),
% 72.32/9.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.32/9.52 fof(f18,axiom,(
% 72.32/9.52 (![A,B,C]: (( ~ product(A,B,C)| divides(A,C) ) ))),
% 72.32/9.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.32/9.52 fof(f19,axiom,(
% 72.32/9.52 (![A,B,C]: (( ~ divides(A,B)| ~ product(C,C,B)| ~ prime(A)| divides(A,C) ) ))),
% 72.32/9.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.32/9.52 fof(f20,hypothesis,(
% 72.32/9.52 prime(a) ),
% 72.32/9.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.32/9.52 fof(f24,negated_conjecture,(
% 72.32/9.52 (![A]: (( ~ divides(A,c)| ~ divides(A,b) ) ))),
% 72.32/9.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.32/9.52 fof(f26,plain,(
% 72.32/9.52 ![X0,X1]: (~equalish(X0,X1)|equalish(X1,X0))),
% 72.32/9.52 inference(cnf_transformation,[status(thm)],[f2])).
% 72.32/9.52 fof(f31,plain,(
% 72.32/9.52 ![B,C,A]: ((![D]: (~equalish(D,B)|~product(C,D,A)))|product(C,B,A))),
% 72.32/9.52 inference(miniscoping,[status(thm)],[f5])).
% 72.32/9.52 fof(f32,plain,(
% 72.32/9.52 ![X0,X1,X2,X3]: (~equalish(X0,X1)|~product(X2,X0,X3)|product(X2,X1,X3))),
% 72.32/9.52 inference(cnf_transformation,[status(thm)],[f31])).
% 72.32/9.52 fof(f35,plain,(
% 72.32/9.52 ![A,C]: ((![B]: (~equalish(B,A)|~divides(C,B)))|divides(C,A))),
% 72.32/9.52 inference(miniscoping,[status(thm)],[f7])).
% 72.32/9.52 fof(f36,plain,(
% 72.32/9.52 ![X0,X1,X2]: (~equalish(X0,X1)|~divides(X2,X0)|divides(X2,X1))),
% 72.32/9.52 inference(cnf_transformation,[status(thm)],[f35])).
% 72.32/9.52 fof(f41,plain,(
% 72.32/9.52 ![X0,X1]: (product(X0,X1,multiply(X0,X1)))),
% 72.32/9.52 inference(cnf_transformation,[status(thm)],[f10])).
% 72.32/9.52 fof(f44,plain,(
% 72.32/9.52 ![C,E,F]: ((![A,D]: ((![B]: (~product(A,B,C)|~product(D,B,E)))|~product(F,D,A)))|product(F,E,C))),
% 72.32/9.52 inference(miniscoping,[status(thm)],[f12])).
% 72.32/9.52 fof(f45,plain,(
% 72.32/9.52 ![X0,X1,X2,X3,X4,X5]: (~product(X0,X1,X2)|~product(X3,X1,X4)|~product(X5,X3,X0)|product(X5,X4,X2))),
% 72.32/9.52 inference(cnf_transformation,[status(thm)],[f44])).
% 72.32/9.52 fof(f46,plain,(
% 72.32/9.52 ![X0,X1,X2]: (~product(X0,X1,X2)|product(X1,X0,X2))),
% 72.32/9.52 inference(cnf_transformation,[status(thm)],[f13])).
% 72.32/9.52 fof(f47,plain,(
% 72.32/9.52 ![B,D]: ((![A,C]: (~product(A,B,C)|~product(A,D,C)))|equalish(B,D))),
% 72.32/9.52 inference(miniscoping,[status(thm)],[f14])).
% 72.32/9.52 fof(f48,plain,(
% 72.32/9.52 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X3,X2)|equalish(X1,X3))),
% 72.32/9.52 inference(cnf_transformation,[status(thm)],[f47])).
% 72.32/9.52 fof(f53,plain,(
% 72.32/9.52 ![X0,X1]: (~divides(X0,X1)|product(X0,second_divided_by_1st(X0,X1),X1))),
% 72.32/9.52 inference(cnf_transformation,[status(thm)],[f17])).
% 72.32/9.52 fof(f54,plain,(
% 72.32/9.52 ![A,C]: ((![B]: ~product(A,B,C))|divides(A,C))),
% 72.32/9.52 inference(miniscoping,[status(thm)],[f18])).
% 72.32/9.52 fof(f55,plain,(
% 72.32/9.52 ![X0,X1,X2]: (~product(X0,X1,X2)|divides(X0,X2))),
% 72.32/9.52 inference(cnf_transformation,[status(thm)],[f54])).
% 72.32/9.52 fof(f56,plain,(
% 72.32/9.52 ![A,C]: (((![B]: (~divides(A,B)|~product(C,C,B)))|~prime(A))|divides(A,C))),
% 72.32/9.52 inference(miniscoping,[status(thm)],[f19])).
% 72.32/9.52 fof(f57,plain,(
% 72.32/9.52 ![X0,X1,X2]: (~divides(X0,X1)|~product(X2,X2,X1)|~prime(X0)|divides(X0,X2))),
% 72.32/9.52 inference(cnf_transformation,[status(thm)],[f56])).
% 72.32/9.52 fof(f58,plain,(
% 72.32/9.52 prime(a)),
% 72.32/9.52 inference(cnf_transformation,[status(thm)],[f20])).
% 72.32/9.52 fof(f62,plain,(
% 72.32/9.52 ![X0]: (~divides(X0,c)|~divides(X0,b))),
% 72.32/9.52 inference(cnf_transformation,[status(thm)],[f24])).
% 72.32/9.52 fof(f101,plain,(
% 72.32/9.52 ![X0,X1,X2]: (~product(X0,X1,X2)|divides(X1,X2))),
% 72.32/9.52 inference(resolution,[status(thm)],[f46,f55])).
% 72.32/9.52 fof(f105,plain,(
% 72.32/9.52 ![X0,X1]: (divides(X0,multiply(X1,X0)))),
% 72.32/9.52 inference(resolution,[status(thm)],[f101,f41])).
% 72.32/9.52 fof(f111,plain,(
% 72.32/9.52 ![X0,X1,X2]: (~equalish(multiply(X0,X1),X2)|divides(X1,X2))),
% 72.32/9.52 inference(resolution,[status(thm)],[f105,f36])).
% 72.32/9.52 fof(f126,plain,(
% 72.32/9.52 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|product(X0,X3,X2)|~equalish(X3,X1))),
% 72.32/9.52 inference(resolution,[status(thm)],[f32,f26])).
% 72.32/9.52 fof(f192,plain,(
% 72.32/9.52 ![X0,X1]: (~divides(X0,X1)|divides(second_divided_by_1st(X0,X1),X1))),
% 72.32/9.52 inference(resolution,[status(thm)],[f53,f101])).
% 72.32/9.52 fof(f443,plain,(
% 72.32/9.52 ![X0,X1,X2]: (~product(X0,X1,X2)|equalish(X1,second_divided_by_1st(X0,X2))|~divides(X0,X2))),
% 72.32/9.52 inference(resolution,[status(thm)],[f48,f53])).
% 72.32/9.52 fof(f444,plain,(
% 72.32/9.52 ![X0,X1,X2]: (~product(X0,X1,multiply(X0,X2))|equalish(X1,X2))),
% 72.32/9.52 inference(resolution,[status(thm)],[f48,f41])).
% 72.32/9.52 fof(f448,plain,(
% 72.32/9.52 ![X0,X1,X2]: (~product(X0,X1,X2)|equalish(X1,second_divided_by_1st(X0,X2)))),
% 72.32/9.52 inference(forward_subsumption_resolution,[status(thm)],[f443,f55])).
% 72.32/9.52 fof(f475,plain,(
% 72.32/9.52 ![X0,X1]: (~divides(a,X0)|~product(X1,X1,X0)|divides(a,X1))),
% 72.32/9.52 inference(resolution,[status(thm)],[f57,f58])).
% 72.32/9.52 fof(f488,plain,(
% 72.32/9.52 ![X0,X1,X2]: (equalish(X0,second_divided_by_1st(X1,X2))|~product(X0,X1,X2))),
% 72.32/9.52 inference(resolution,[status(thm)],[f448,f46])).
% 72.32/9.52 fof(f571,plain,(
% 72.32/9.52 ![X0,X1]: (equalish(X0,second_divided_by_1st(second_divided_by_1st(X0,X1),X1))|~divides(X0,X1))),
% 72.32/9.52 inference(resolution,[status(thm)],[f488,f53])).
% 72.32/9.52 fof(f572,plain,(
% 72.32/9.52 ![X0,X1]: (equalish(X0,second_divided_by_1st(X1,multiply(X0,X1))))),
% 72.32/9.52 inference(resolution,[status(thm)],[f488,f41])).
% 72.32/9.52 fof(f649,plain,(
% 72.32/9.52 ![X0,X1,X2,X3,X4,X5]: (equalish(X0,X1)|~product(X2,X3,multiply(X4,X1))|~product(X5,X3,X0)|~product(X4,X5,X2))),
% 72.32/9.52 inference(resolution,[status(thm)],[f444,f45])).
% 72.32/9.52 fof(f767,plain,(
% 72.32/9.52 ![X0,X1,X2]: (product(X0,X1,X2)|~equalish(X1,second_divided_by_1st(X0,X2))|~divides(X0,X2))),
% 72.32/9.52 inference(resolution,[status(thm)],[f126,f53])).
% 72.32/9.52 fof(f1783,plain,(
% 72.32/9.52 ![X0]: (~divides(a,multiply(X0,X0))|divides(a,X0))),
% 72.32/9.52 inference(resolution,[status(thm)],[f475,f41])).
% 72.32/9.52 fof(f2089,plain,(
% 72.32/9.52 divides(a,a)),
% 72.32/9.52 inference(resolution,[status(thm)],[f1783,f105])).
% 72.32/9.52 fof(f6688,plain,(
% 72.32/9.52 ![X0,X1,X2,X3]: (equalish(X0,X1)|~product(X2,X1,X0)|~product(X3,X2,X3))),
% 72.32/9.52 inference(resolution,[status(thm)],[f649,f41])).
% 72.32/9.52 fof(f7982,plain,(
% 72.32/9.52 ![X0,X1]: (product(second_divided_by_1st(X0,X1),X0,X1)|~divides(second_divided_by_1st(X0,X1),X1)|~divides(X0,X1))),
% 72.32/9.52 inference(resolution,[status(thm)],[f767,f571])).
% 72.32/9.52 fof(f7983,plain,(
% 72.32/9.52 ![X0,X1]: (product(X0,X1,multiply(X1,X0))|~divides(X0,multiply(X1,X0)))),
% 72.32/9.52 inference(resolution,[status(thm)],[f767,f572])).
% 72.32/9.52 fof(f7987,plain,(
% 72.32/9.52 ![X0,X1]: (product(second_divided_by_1st(X0,X1),X0,X1)|~divides(X0,X1))),
% 72.32/9.52 inference(forward_subsumption_resolution,[status(thm)],[f7982,f192])).
% 72.32/9.52 fof(f7988,plain,(
% 72.32/9.52 ![X0,X1]: (product(X0,X1,multiply(X1,X0)))),
% 72.32/9.52 inference(forward_subsumption_resolution,[status(thm)],[f7983,f105])).
% 72.32/9.52 fof(f8202,plain,(
% 72.32/9.52 product(second_divided_by_1st(a,a),a,a)),
% 72.32/9.52 inference(resolution,[status(thm)],[f7987,f2089])).
% 72.32/9.52 fof(f9748,plain,(
% 72.32/9.52 ![X0,X1,X2,X3]: (equalish(X0,X1)|~product(X2,X1,X0)|~product(X2,X3,X3))),
% 72.32/9.52 inference(resolution,[status(thm)],[f6688,f46])).
% 72.32/9.52 fof(f14655,plain,(
% 72.32/9.52 ![X0,X1]: (equalish(X0,X1)|~product(second_divided_by_1st(a,a),X1,X0))),
% 72.32/9.52 inference(resolution,[status(thm)],[f9748,f8202])).
% 72.32/9.52 fof(f14810,plain,(
% 72.32/9.52 ![X0]: (equalish(multiply(X0,second_divided_by_1st(a,a)),X0))),
% 72.32/9.52 inference(resolution,[status(thm)],[f14655,f7988])).
% 72.32/9.52 fof(f14847,plain,(
% 72.32/9.52 ![X0]: (divides(second_divided_by_1st(a,a),X0))),
% 72.32/9.52 inference(resolution,[status(thm)],[f14810,f111])).
% 72.32/9.52 fof(f15286,plain,(
% 72.32/9.52 ~divides(second_divided_by_1st(a,a),b)),
% 72.32/9.52 inference(resolution,[status(thm)],[f14847,f62])).
% 72.32/9.52 fof(f15293,plain,(
% 72.32/9.52 $false),
% 72.32/9.52 inference(forward_subsumption_resolution,[status(thm)],[f15286,f14847])).
% 72.32/9.52 % SZS output end CNFRefutation for theBenchmark.p
% 72.32/9.58 % Elapsed time: 9.208324 seconds
% 72.32/9.58 % CPU time: 72.793996 seconds
% 72.32/9.58 % Total memory used: 344.696 MB
% 72.32/9.58 % Net memory used: 283.491 MB
%------------------------------------------------------------------------------