%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN708-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:20:23 PM UTC 2026
% Result : Unsatisfiable 1.13s 0.71s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN708-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n020.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 11:13:48 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 1.13/0.71 % Refutation found
% 1.13/0.71 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.13/0.71 % SZS output start CNFRefutation for theBenchmark
% 1.13/0.71 fof(f1,negated_conjecture,(
% 1.13/0.71 p38(c56) ),
% 1.13/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.13/0.71 fof(f3,negated_conjecture,(
% 1.13/0.71 (![X0]: (p10(X0,X0) ))),
% 1.13/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.13/0.71 fof(f13,negated_conjecture,(
% 1.13/0.71 p37(f15(c56),c48) ),
% 1.13/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.13/0.71 fof(f15,negated_conjecture,(
% 1.13/0.71 (![X27]: (( p38(f15(X27))| ~ p38(X27) ) ))),
% 1.13/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.13/0.71 fof(f19,negated_conjecture,(
% 1.13/0.71 (![X97,X98]: (( p38(X97)| ~ p38(X98)| ~ p10(X98,X97) ) ))),
% 1.13/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.13/0.71 fof(f32,negated_conjecture,(
% 1.13/0.71 (![X25,X26]: (( p16(f19(X25),f19(X26))| ~ p10(X25,X26) ) ))),
% 1.13/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.13/0.71 fof(f36,negated_conjecture,(
% 1.13/0.71 (![X27]: (( p16(f19(f15(X27)),f28(f19(X27)))| ~ p38(X27) ) ))),
% 1.13/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.13/0.71 fof(f37,negated_conjecture,(
% 1.13/0.71 (![X1,X2,X0]: (( p10(X1,X2)| ~ p10(X0,X1)| ~ p10(X0,X2) ) ))),
% 1.13/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.13/0.71 fof(f52,negated_conjecture,(
% 1.13/0.71 (![X99,X100,X102,X101]: (( p39(X99,X100)| ~ p16(X102,X100)| ~ p39(X101,X102)| ~ p16(X101,X99) ) ))),
% 1.13/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.13/0.71 fof(f54,negated_conjecture,(
% 1.13/0.71 (![X91,X92]: (( p39(f19(X91),f19(X92))| ~ p38(X92)| ~ p38(X91)| ~ p37(X91,X92) ) ))),
% 1.13/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.13/0.71 fof(f64,negated_conjecture,(
% 1.13/0.71 p38(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))) ),
% 1.13/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.13/0.71 fof(f66,negated_conjecture,(
% 1.13/0.71 p10(c48,f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))) ),
% 1.13/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.13/0.71 fof(f69,negated_conjecture,(
% 1.13/0.71 ~ p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))) ),
% 1.13/0.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.13/0.71 fof(f84,plain,(
% 1.13/0.71 p38(c56)),
% 1.13/0.71 inference(cnf_transformation,[status(thm)],[f1])).
% 1.13/0.71 fof(f86,plain,(
% 1.13/0.71 ![X0]: (p10(X0,X0))),
% 1.13/0.71 inference(cnf_transformation,[status(thm)],[f3])).
% 1.13/0.71 fof(f96,plain,(
% 1.13/0.71 p37(f15(c56),c48)),
% 1.13/0.71 inference(cnf_transformation,[status(thm)],[f13])).
% 1.13/0.71 fof(f98,plain,(
% 1.13/0.71 ![X0]: (p38(f15(X0))|~p38(X0))),
% 1.13/0.71 inference(cnf_transformation,[status(thm)],[f15])).
% 1.13/0.71 fof(f102,plain,(
% 1.13/0.71 ![X0,X1]: (p38(X0)|~p38(X1)|~p10(X1,X0))),
% 1.13/0.71 inference(cnf_transformation,[status(thm)],[f19])).
% 1.13/0.71 fof(f115,plain,(
% 1.13/0.71 ![X0,X1]: (p16(f19(X0),f19(X1))|~p10(X0,X1))),
% 1.13/0.71 inference(cnf_transformation,[status(thm)],[f32])).
% 1.13/0.71 fof(f119,plain,(
% 1.13/0.71 ![X0]: (p16(f19(f15(X0)),f28(f19(X0)))|~p38(X0))),
% 1.13/0.71 inference(cnf_transformation,[status(thm)],[f36])).
% 1.13/0.71 fof(f120,plain,(
% 1.13/0.71 ![X2,X0]: ((![X1]: (p10(X1,X2)|~p10(X0,X1)))|~p10(X0,X2))),
% 1.13/0.71 inference(miniscoping,[status(thm)],[f37])).
% 1.13/0.71 fof(f121,plain,(
% 1.13/0.71 ![X0,X1,X2]: (p10(X0,X1)|~p10(X2,X0)|~p10(X2,X1))),
% 1.13/0.71 inference(cnf_transformation,[status(thm)],[f120])).
% 1.13/0.71 fof(f147,plain,(
% 1.13/0.71 ![X99,X101]: ((![X102]: ((![X100]: (p39(X99,X100)|~p16(X102,X100)))|~p39(X101,X102)))|~p16(X101,X99))),
% 1.13/0.71 inference(miniscoping,[status(thm)],[f52])).
% 1.13/0.71 fof(f148,plain,(
% 1.13/0.71 ![X0,X1,X2,X3]: (p39(X0,X1)|~p16(X2,X1)|~p39(X3,X2)|~p16(X3,X0))),
% 1.13/0.71 inference(cnf_transformation,[status(thm)],[f147])).
% 1.13/0.71 fof(f151,plain,(
% 1.13/0.71 ![X0,X1]: (p39(f19(X0),f19(X1))|~p38(X1)|~p38(X0)|~p37(X0,X1))),
% 1.13/0.71 inference(cnf_transformation,[status(thm)],[f54])).
% 1.13/0.71 fof(f169,plain,(
% 1.13/0.71 p38(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),
% 1.13/0.71 inference(cnf_transformation,[status(thm)],[f64])).
% 1.13/0.71 fof(f171,plain,(
% 1.13/0.71 p10(c48,f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),
% 1.13/0.71 inference(cnf_transformation,[status(thm)],[f66])).
% 1.13/0.71 fof(f174,plain,(
% 1.13/0.71 ~p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))))),
% 1.13/0.71 inference(cnf_transformation,[status(thm)],[f69])).
% 1.13/0.71 fof(f189,plain,(
% 1.13/0.71 p38(f15(c56))),
% 1.13/0.71 inference(resolution,[status(thm)],[f98,f84])).
% 1.13/0.72 fof(f217,plain,(
% 1.13/0.72 ![X0,X1]: (p10(X0,X1)|~p10(X1,X0))),
% 1.13/0.72 inference(resolution,[status(thm)],[f121,f86])).
% 1.13/0.72 fof(f221,plain,(
% 1.13/0.72 p16(f19(f15(c56)),f28(f19(c56)))),
% 1.13/0.72 inference(resolution,[status(thm)],[f119,f84])).
% 1.13/0.72 fof(f260,plain,(
% 1.13/0.72 p39(f19(f15(c56)),f19(c48))|~p38(c48)|~p38(f15(c56))),
% 1.13/0.72 inference(resolution,[status(thm)],[f151,f96])).
% 1.13/0.72 fof(f261,plain,(
% 1.13/0.72 p39(f19(f15(c56)),f19(c48))|~p38(c48)),
% 1.13/0.72 inference(forward_subsumption_resolution,[status(thm)],[f260,f189])).
% 1.13/0.72 fof(f290,plain,(
% 1.13/0.72 ![X0]: (p38(X0)|~p10(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))),X0))),
% 1.13/0.72 inference(resolution,[status(thm)],[f169,f102])).
% 1.13/0.72 fof(f307,plain,(
% 1.13/0.72 p10(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))),c48)),
% 1.13/0.72 inference(resolution,[status(thm)],[f171,f217])).
% 1.13/0.72 fof(f313,plain,(
% 1.13/0.72 p16(f19(c48),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))))),
% 1.13/0.72 inference(resolution,[status(thm)],[f171,f115])).
% 1.13/0.72 fof(f1783,plain,(
% 1.13/0.72 p38(c48)),
% 1.13/0.72 inference(resolution,[status(thm)],[f307,f290])).
% 1.13/0.72 fof(f1820,plain,(
% 1.13/0.72 p39(f19(f15(c56)),f19(c48))),
% 1.13/0.72 inference(backward_subsumption_resolution,[status(thm)],[f261,f1783])).
% 1.13/0.72 fof(f1825,plain,(
% 1.13/0.72 ![X0,X1]: (p39(X0,X1)|~p16(f19(c48),X1)|~p16(f19(f15(c56)),X0))),
% 1.13/0.72 inference(resolution,[status(thm)],[f1820,f148])).
% 1.13/0.72 fof(f3738,plain,(
% 1.13/0.72 ![X0]: (p39(f28(f19(c56)),X0)|~p16(f19(c48),X0))),
% 1.13/0.72 inference(resolution,[status(thm)],[f1825,f221])).
% 1.13/0.72 fof(f3798,plain,(
% 1.13/0.72 p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))))),
% 1.13/0.72 inference(resolution,[status(thm)],[f3738,f313])).
% 1.13/0.72 fof(f3800,plain,(
% 1.13/0.72 $false),
% 1.13/0.72 inference(forward_subsumption_resolution,[status(thm)],[f3798,f174])).
% 1.13/0.72 % SZS output end CNFRefutation for theBenchmark.p
% 2.04/1.93 % Elapsed time: 1.351802 seconds
% 2.04/1.93 % CPU time: 2.479011 seconds
% 2.04/1.93 % Total memory used: 110.693 MB
% 2.04/1.93 % Net memory used: 106.673 MB
%------------------------------------------------------------------------------