%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN719-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:24 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN719-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % 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 11:19:00 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 0.14/0.40 % Refutation found
% 0.14/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.40 fof(f3,negated_conjecture,(
% 0.14/0.40 (![X231]: (p7(X231,X231) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f38,negated_conjecture,(
% 0.14/0.40 (![X13]: (p14(X13,X13) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f41,negated_conjecture,(
% 0.14/0.40 p66(f12(c78,c77),c79) ),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f42,negated_conjecture,(
% 0.14/0.40 p67(f16(c80,c81),c82) ),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f43,negated_conjecture,(
% 0.14/0.40 (![X242,X243]: (p70(f30(c88,X242),f38(c85,X243)) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f45,negated_conjecture,(
% 0.14/0.40 (![X20]: (p14(f23(f26(c84,c85),X20),X20) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f46,negated_conjecture,(
% 0.14/0.40 ~ p68(f19(f21(c83,c77),c79),c81) ),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f48,negated_conjecture,(
% 0.14/0.40 (![X216,X215]: (( p68(X216,X215)| ~ p67(f16(c80,X215),X216) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f50,negated_conjecture,(
% 0.14/0.40 (![X215,X216]: (( p67(f16(c80,X215),X216)| ~ p68(X216,X215) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f52,negated_conjecture,(
% 0.14/0.40 (![X229,X230]: (( p69(f36(c86,X229),X230)| ~ p70(X230,X229) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f90,negated_conjecture,(
% 0.14/0.40 (![X14,X15,X13]: (( p14(X14,X15)| ~ p14(X13,X14)| ~ p14(X13,X15) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f97,negated_conjecture,(
% 0.14/0.40 (![X217,X218,X220,X219]: (( p68(X217,X218)| ~ p68(X220,X219)| ~ p7(X220,X217)| ~ p14(X219,X218) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f126,negated_conjecture,(
% 0.14/0.40 (![X221,X222,X224,X223]: (( p68(f19(f21(c83,c77),X221),X222)| ~ p67(f16(c80,X224),c82)| ~ p66(f12(c78,c77),X221)| ~ p14(X222,f23(f26(c84,X223),X224))| ~ p69(f36(c86,f38(X223,f40(f42(f44(f46(c87,X221),X222),X223),X224))),f30(c88,f32(c89,f8(c75,c76)))) ) ))),
% 0.14/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f129,plain,(
% 0.14/0.40 ![X0]: (p7(X0,X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f3])).
% 0.14/0.40 fof(f164,plain,(
% 0.14/0.40 ![X0]: (p14(X0,X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f38])).
% 0.14/0.40 fof(f167,plain,(
% 0.14/0.40 p66(f12(c78,c77),c79)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f41])).
% 0.14/0.40 fof(f168,plain,(
% 0.14/0.40 p67(f16(c80,c81),c82)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.14/0.40 fof(f169,plain,(
% 0.14/0.40 ![X0,X1]: (p70(f30(c88,X0),f38(c85,X1)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f43])).
% 0.14/0.40 fof(f171,plain,(
% 0.14/0.40 ![X0]: (p14(f23(f26(c84,c85),X0),X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.40 fof(f172,plain,(
% 0.14/0.40 ~p68(f19(f21(c83,c77),c79),c81)),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f46])).
% 0.14/0.40 fof(f174,plain,(
% 0.14/0.40 ![X0,X1]: (p68(X0,X1)|~p67(f16(c80,X1),X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f48])).
% 0.14/0.40 fof(f176,plain,(
% 0.14/0.40 ![X0,X1]: (p67(f16(c80,X0),X1)|~p68(X1,X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f50])).
% 0.14/0.40 fof(f178,plain,(
% 0.14/0.40 ![X0,X1]: (p69(f36(c86,X0),X1)|~p70(X1,X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f52])).
% 0.14/0.40 fof(f253,plain,(
% 0.14/0.40 ![X15,X13]: ((![X14]: (p14(X14,X15)|~p14(X13,X14)))|~p14(X13,X15))),
% 0.14/0.40 inference(miniscoping,[status(thm)],[f90])).
% 0.14/0.40 fof(f254,plain,(
% 0.14/0.40 ![X0,X1,X2]: (p14(X0,X1)|~p14(X2,X0)|~p14(X2,X1))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f253])).
% 0.14/0.40 fof(f267,plain,(
% 0.14/0.40 ![X218,X219]: ((![X217,X220]: ((p68(X217,X218)|~p68(X220,X219))|~p7(X220,X217)))|~p14(X219,X218))),
% 0.14/0.40 inference(miniscoping,[status(thm)],[f97])).
% 0.14/0.40 fof(f268,plain,(
% 0.14/0.40 ![X0,X1,X2,X3]: (p68(X0,X1)|~p68(X2,X3)|~p7(X2,X0)|~p14(X3,X1))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f267])).
% 0.14/0.40 fof(f324,plain,(
% 0.14/0.40 ![X0,X1,X2,X3]: (p68(f19(f21(c83,c77),X0),X1)|~p67(f16(c80,X2),c82)|~p66(f12(c78,c77),X0)|~p14(X1,f23(f26(c84,X3),X2))|~p69(f36(c86,f38(X3,f40(f42(f44(f46(c87,X0),X1),X3),X2))),f30(c88,f32(c89,f8(c75,c76)))))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f126])).
% 0.14/0.40 fof(f325,plain,(
% 0.14/0.40 p68(c82,c81)),
% 0.14/0.40 inference(resolution,[status(thm)],[f174,f168])).
% 0.14/0.40 fof(f327,plain,(
% 0.14/0.40 ![X0,X1]: (p69(f36(c86,f38(c85,X0)),f30(c88,X1)))),
% 0.14/0.40 inference(resolution,[status(thm)],[f178,f169])).
% 0.14/0.40 fof(f365,plain,(
% 0.14/0.40 ![X0,X1]: (p14(X0,X1)|~p14(f23(f26(c84,c85),X0),X1))),
% 0.14/0.40 inference(resolution,[status(thm)],[f254,f171])).
% 0.14/0.40 fof(f373,plain,(
% 0.14/0.40 ![X0,X1]: (p68(X0,X1)|~p7(c82,X0)|~p14(c81,X1))),
% 0.14/0.40 inference(resolution,[status(thm)],[f268,f325])).
% 0.14/0.40 fof(f376,plain,(
% 0.14/0.40 ![X0]: (p68(c82,X0)|~p14(c81,X0))),
% 0.14/0.40 inference(resolution,[status(thm)],[f373,f129])).
% 0.14/0.40 fof(f416,plain,(
% 0.14/0.40 ![X0,X1,X2]: (p68(f19(f21(c83,c77),X0),X1)|~p67(f16(c80,X2),c82)|~p66(f12(c78,c77),X0)|~p14(X1,f23(f26(c84,c85),X2)))),
% 0.14/0.40 inference(resolution,[status(thm)],[f327,f324])).
% 0.14/0.40 fof(f421,plain,(
% 0.14/0.40 ![X0]: (p14(X0,f23(f26(c84,c85),X0)))),
% 0.14/0.40 inference(resolution,[status(thm)],[f365,f164])).
% 0.14/0.40 fof(f423,plain,(
% 0.14/0.40 ![X0]: (p14(X0,f23(f26(c84,c85),f23(f26(c84,c85),X0))))),
% 0.14/0.40 inference(resolution,[status(thm)],[f421,f365])).
% 0.14/0.40 fof(f424,plain,(
% 0.14/0.40 p68(c82,f23(f26(c84,c85),c81))),
% 0.14/0.40 inference(resolution,[status(thm)],[f421,f376])).
% 0.14/0.40 fof(f453,plain,(
% 0.14/0.40 ![X0,X1]: (p68(f19(f21(c83,c77),c79),X0)|~p67(f16(c80,X1),c82)|~p14(X0,f23(f26(c84,c85),X1)))),
% 0.14/0.40 inference(resolution,[status(thm)],[f416,f167])).
% 0.14/0.40 fof(f455,plain,(
% 0.14/0.40 p67(f16(c80,f23(f26(c84,c85),c81)),c82)),
% 0.14/0.40 inference(resolution,[status(thm)],[f424,f176])).
% 0.14/0.40 fof(f500,plain,(
% 0.14/0.40 ![X0]: (p68(f19(f21(c83,c77),c79),X0)|~p67(f16(c80,f23(f26(c84,c85),X0)),c82))),
% 0.14/0.40 inference(resolution,[status(thm)],[f453,f423])).
% 0.14/0.40 fof(f610,plain,(
% 0.14/0.40 p68(f19(f21(c83,c77),c79),c81)),
% 0.14/0.40 inference(resolution,[status(thm)],[f500,f455])).
% 0.14/0.40 fof(f611,plain,(
% 0.14/0.40 $false),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f610,f172])).
% 0.14/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.42 % Elapsed time: 0.049229 seconds
% 0.14/0.42 % CPU time: 0.152577 seconds
% 0.14/0.42 % Total memory used: 48.181 MB
% 0.14/0.42 % Net memory used: 48.064 MB
%------------------------------------------------------------------------------