%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN706-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 : n015.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 0.10s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN706-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 : n015.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.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 11:16:06 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.10/0.40 % Refutation found
% 0.10/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.40 fof(f5,negated_conjecture,(
% 0.10/0.40 (![X143]: (p47(X143,X143) ))),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f11,negated_conjecture,(
% 0.10/0.40 (![X88]: (p36(X88,X88) ))),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f27,negated_conjecture,(
% 0.10/0.40 p45(f20(c52,c50),c58) ),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f29,negated_conjecture,(
% 0.10/0.40 ~ p48(f38(f40(c59,c50),c58),c60) ),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f57,negated_conjecture,(
% 0.10/0.40 (![X146,X147,X149,X148]: (( p48(X146,X147)| ~ p47(X149,X147)| ~ p48(X148,X149)| ~ p37(X148,X146) ) ))),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f59,negated_conjecture,(
% 0.10/0.40 (![X166,X167]: (p7(f8(f11(c54,f14(f17(c55,X166),f35(X167,X166))),X167),X167) ))),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f67,negated_conjecture,(
% 0.10/0.40 (![X98,X99,X100,X101]: (( p37(f38(X98,X99),f38(X100,X101))| ~ p36(X98,X100)| ~ p7(X99,X101) ) ))),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f78,negated_conjecture,(
% 0.10/0.40 (![X137,X142,X136]: (( p46(f23(c53,f35(X137,X142)),f5(c49,X136))| ~ p45(f20(c52,X136),X137) ) ))),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f81,negated_conjecture,(
% 0.10/0.40 (![X150,X151]: (( p48(f38(f40(c59,c50),f8(f11(c54,f14(f17(c55,c61),X150)),X151)),c60)| ~ p45(f20(c52,c50),X151)| ~ p46(f23(c53,X150),f5(c49,c50)) ) ))),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f86,plain,(
% 0.10/0.40 ![X0]: (p47(X0,X0))),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.40 fof(f92,plain,(
% 0.10/0.40 ![X0]: (p36(X0,X0))),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f11])).
% 0.10/0.40 fof(f108,plain,(
% 0.10/0.40 p45(f20(c52,c50),c58)),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f27])).
% 0.10/0.40 fof(f110,plain,(
% 0.10/0.40 ~p48(f38(f40(c59,c50),c58),c60)),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f29])).
% 0.10/0.40 fof(f165,plain,(
% 0.10/0.40 ![X146,X148]: ((![X149]: ((![X147]: (p48(X146,X147)|~p47(X149,X147)))|~p48(X148,X149)))|~p37(X148,X146))),
% 0.10/0.40 inference(miniscoping,[status(thm)],[f57])).
% 0.10/0.40 fof(f166,plain,(
% 0.10/0.40 ![X0,X1,X2,X3]: (p48(X0,X1)|~p47(X2,X1)|~p48(X3,X2)|~p37(X3,X0))),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f165])).
% 0.10/0.40 fof(f169,plain,(
% 0.10/0.40 ![X0,X1]: (p7(f8(f11(c54,f14(f17(c55,X0),f35(X1,X0))),X1),X1))),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f59])).
% 0.10/0.40 fof(f183,plain,(
% 0.10/0.40 ![X99,X101]: ((![X98,X100]: (p37(f38(X98,X99),f38(X100,X101))|~p36(X98,X100)))|~p7(X99,X101))),
% 0.10/0.40 inference(miniscoping,[status(thm)],[f67])).
% 0.10/0.40 fof(f184,plain,(
% 0.10/0.40 ![X0,X1,X2,X3]: (p37(f38(X0,X1),f38(X2,X3))|~p36(X0,X2)|~p7(X1,X3))),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f183])).
% 0.10/0.40 fof(f205,plain,(
% 0.10/0.40 ![X137,X136]: ((![X142]: p46(f23(c53,f35(X137,X142)),f5(c49,X136)))|~p45(f20(c52,X136),X137))),
% 0.10/0.40 inference(miniscoping,[status(thm)],[f78])).
% 0.10/0.40 fof(f206,plain,(
% 0.10/0.40 ![X0,X1,X2]: (p46(f23(c53,f35(X0,X1)),f5(c49,X2))|~p45(f20(c52,X2),X0))),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f205])).
% 0.10/0.40 fof(f210,plain,(
% 0.10/0.40 ![X150]: ((![X151]: (p48(f38(f40(c59,c50),f8(f11(c54,f14(f17(c55,c61),X150)),X151)),c60)|~p45(f20(c52,c50),X151)))|~p46(f23(c53,X150),f5(c49,c50)))),
% 0.10/0.40 inference(miniscoping,[status(thm)],[f81])).
% 0.10/0.40 fof(f211,plain,(
% 0.10/0.40 ![X0,X1]: (p48(f38(f40(c59,c50),f8(f11(c54,f14(f17(c55,c61),X0)),X1)),c60)|~p45(f20(c52,c50),X1)|~p46(f23(c53,X0),f5(c49,c50)))),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f210])).
% 0.10/0.40 fof(f240,plain,(
% 0.10/0.40 ![X0,X1,X2]: (p48(X0,X1)|~p48(X2,X1)|~p37(X2,X0))),
% 0.10/0.40 inference(resolution,[status(thm)],[f166,f86])).
% 0.10/0.40 fof(f252,plain,(
% 0.10/0.40 ![X0,X1,X2]: (p37(f38(X0,X1),f38(X0,X2))|~p7(X1,X2))),
% 0.10/0.40 inference(resolution,[status(thm)],[f184,f92])).
% 0.10/0.40 fof(f268,plain,(
% 0.10/0.40 ![X0,X1,X2]: (p37(f38(X0,f8(f11(c54,f14(f17(c55,X1),f35(X2,X1))),X2)),f38(X0,X2)))),
% 0.10/0.40 inference(resolution,[status(thm)],[f252,f169])).
% 0.10/0.40 fof(f273,plain,(
% 0.10/0.40 ![X0]: (p46(f23(c53,f35(c58,X0)),f5(c49,c50)))),
% 0.10/0.40 inference(resolution,[status(thm)],[f206,f108])).
% 0.10/0.40 fof(f276,plain,(
% 0.10/0.40 ![X0]: (p48(f38(f40(c59,c50),f8(f11(c54,f14(f17(c55,c61),X0)),c58)),c60)|~p46(f23(c53,X0),f5(c49,c50)))),
% 0.10/0.41 inference(resolution,[status(thm)],[f211,f108])).
% 0.10/0.41 fof(f297,plain,(
% 0.10/0.41 ![X0]: (p48(f38(f40(c59,c50),f8(f11(c54,f14(f17(c55,c61),f35(c58,X0))),c58)),c60))),
% 0.10/0.41 inference(resolution,[status(thm)],[f276,f273])).
% 0.10/0.41 fof(f343,plain,(
% 0.10/0.41 ![X0,X1]: (p48(X0,c60)|~p37(f38(f40(c59,c50),f8(f11(c54,f14(f17(c55,c61),f35(c58,X1))),c58)),X0))),
% 0.10/0.41 inference(resolution,[status(thm)],[f297,f240])).
% 0.10/0.41 fof(f489,plain,(
% 0.10/0.41 p48(f38(f40(c59,c50),c58),c60)),
% 0.10/0.41 inference(resolution,[status(thm)],[f343,f268])).
% 0.10/0.41 fof(f492,plain,(
% 0.10/0.41 $false),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f489,f110])).
% 0.10/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.44 % Elapsed time: 0.059468 seconds
% 0.10/0.44 % CPU time: 0.179448 seconds
% 0.10/0.44 % Total memory used: 59.777 MB
% 0.10/0.44 % Net memory used: 59.625 MB
%------------------------------------------------------------------------------