%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN656-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:18 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN656-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:14:21 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.13/0.42 % Refutation found
% 0.13/0.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.42 fof(f1,negated_conjecture,(
% 0.13/0.42 (![X0]: (p11(X0,X0) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f5,negated_conjecture,(
% 0.13/0.42 (![X75]: (p4(X75,X75) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f6,negated_conjecture,(
% 0.13/0.42 (![X64]: (p3(X64,X64) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f13,negated_conjecture,(
% 0.13/0.42 (![X3]: (p12(X3,X3) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f22,negated_conjecture,(
% 0.13/0.42 (![X65,X66,X64]: (( p3(X65,X66)| ~ p3(X64,X65)| ~ p3(X64,X66) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f31,negated_conjecture,(
% 0.13/0.42 (![X58]: (p25(f5(c29,f13(c31,f15(c32,X58))),f13(c31,X58)) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f32,negated_conjecture,(
% 0.13/0.42 (![X55,X56,X57]: (( p25(f5(f7(c28,X55),X56),X57)| ~ p25(f5(X55,X56),X57) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f35,negated_conjecture,(
% 0.13/0.42 (![X51,X52,X54,X53]: (( p25(X51,X52)| ~ p3(X54,X52)| ~ p4(X53,X51)| ~ p25(X53,X54) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f42,negated_conjecture,(
% 0.13/0.42 (![X67,X68,X69,X70]: (( p3(f13(X67,X68),f13(X69,X70))| ~ p11(X67,X69)| ~ p12(X68,X70) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f45,negated_conjecture,(
% 0.13/0.42 ~ p25(f5(f7(c28,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)) ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f46,negated_conjecture,(
% 0.13/0.42 (![X55,X56,X57,X62]: (( p25(f5(f7(c28,X55),X56),X57)| ~ p25(f5(X55,X56),X62)| ~ p25(f5(f7(c28,X55),X62),X57) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f49,negated_conjecture,(
% 0.13/0.42 (![X63]: (( p3(f13(c31,c34),f13(c31,f15(f17(c33,c34),X63)))| p25(f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),X63))),f13(c31,c34)) ) ))),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f50,plain,(
% 0.13/0.42 ![X0]: (p11(X0,X0))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.42 fof(f54,plain,(
% 0.13/0.42 ![X0]: (p4(X0,X0))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.42 fof(f55,plain,(
% 0.13/0.42 ![X0]: (p3(X0,X0))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.42 fof(f62,plain,(
% 0.13/0.42 ![X0]: (p12(X0,X0))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f13])).
% 0.13/0.42 fof(f76,plain,(
% 0.13/0.42 ![X66,X64]: ((![X65]: (p3(X65,X66)|~p3(X64,X65)))|~p3(X64,X66))),
% 0.13/0.42 inference(miniscoping,[status(thm)],[f22])).
% 0.13/0.42 fof(f77,plain,(
% 0.13/0.42 ![X0,X1,X2]: (p3(X0,X1)|~p3(X2,X0)|~p3(X2,X1))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f76])).
% 0.13/0.42 fof(f94,plain,(
% 0.13/0.42 ![X0]: (p25(f5(c29,f13(c31,f15(c32,X0))),f13(c31,X0)))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f31])).
% 0.13/0.42 fof(f95,plain,(
% 0.13/0.42 ![X0,X1,X2]: (p25(f5(f7(c28,X0),X1),X2)|~p25(f5(X0,X1),X2))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f32])).
% 0.13/0.42 fof(f99,plain,(
% 0.13/0.42 ![X54,X53]: ((![X51]: ((![X52]: (p25(X51,X52)|~p3(X54,X52)))|~p4(X53,X51)))|~p25(X53,X54))),
% 0.13/0.42 inference(miniscoping,[status(thm)],[f35])).
% 0.13/0.42 fof(f100,plain,(
% 0.13/0.42 ![X0,X1,X2,X3]: (p25(X0,X1)|~p3(X2,X1)|~p4(X3,X0)|~p25(X3,X2))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f99])).
% 0.13/0.42 fof(f113,plain,(
% 0.13/0.42 ![X68,X70]: ((![X67,X69]: (p3(f13(X67,X68),f13(X69,X70))|~p11(X67,X69)))|~p12(X68,X70))),
% 0.13/0.42 inference(miniscoping,[status(thm)],[f42])).
% 0.13/0.42 fof(f114,plain,(
% 0.13/0.42 ![X0,X1,X2,X3]: (p3(f13(X0,X1),f13(X2,X3))|~p11(X0,X2)|~p12(X1,X3))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f113])).
% 0.13/0.42 fof(f119,plain,(
% 0.13/0.42 ~p25(f5(f7(c28,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f45])).
% 0.13/0.42 fof(f120,plain,(
% 0.13/0.42 ![X55,X57,X62]: ((![X56]: (p25(f5(f7(c28,X55),X56),X57)|~p25(f5(X55,X56),X62)))|~p25(f5(f7(c28,X55),X62),X57))),
% 0.13/0.42 inference(miniscoping,[status(thm)],[f46])).
% 0.13/0.42 fof(f121,plain,(
% 0.13/0.42 ![X0,X1,X2,X3]: (p25(f5(f7(c28,X0),X1),X2)|~p25(f5(X0,X1),X3)|~p25(f5(f7(c28,X0),X3),X2))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f120])).
% 0.13/0.42 fof(f124,plain,(
% 0.13/0.42 ![X0]: (p3(f13(c31,c34),f13(c31,f15(f17(c33,c34),X0)))|p25(f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),X0))),f13(c31,c34)))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f49])).
% 0.13/0.42 fof(f127,plain,(
% 0.13/0.42 ![X0,X1,X2]: (p25(X0,X1)|~p3(f13(c31,X2),X1)|~p4(f5(c29,f13(c31,f15(c32,X2))),X0))),
% 0.13/0.42 inference(resolution,[status(thm)],[f94,f100])).
% 0.13/0.42 fof(f133,plain,(
% 0.13/0.42 ![X0,X1,X2,X3]: (p25(X0,X1)|~p4(f5(c29,f13(c31,f15(c32,X2))),X0)|~p3(X3,f13(c31,X2))|~p3(X3,X1))),
% 0.13/0.42 inference(resolution,[status(thm)],[f127,f77])).
% 0.13/0.42 fof(f163,plain,(
% 0.13/0.42 ![X0,X1]: (p3(f13(c31,c34),f13(c31,f15(f17(c33,c34),X0)))|p25(f5(f7(c28,c29),X1),f13(c31,c34))|~p25(f5(c29,X1),f13(c31,f15(f17(c33,c34),X0))))),
% 0.13/0.42 inference(resolution,[status(thm)],[f124,f121])).
% 0.13/0.42 fof(f192,plain,(
% 0.13/0.42 ![X0,X1,X2,X3,X4]: (p25(X0,X1)|~p4(f5(c29,f13(c31,f15(c32,X2))),X0)|~p3(f13(X3,X4),X1)|~p11(X3,c31)|~p12(X4,X2))),
% 0.13/0.42 inference(resolution,[status(thm)],[f133,f114])).
% 0.13/0.42 fof(f203,plain,(
% 0.13/0.42 ![X0]: (p3(f13(c31,c34),f13(c31,f15(f17(c33,c34),X0)))|p25(f5(f7(c28,c29),f13(c31,f15(c32,f15(f17(c33,c34),X0)))),f13(c31,c34)))),
% 0.13/0.42 inference(resolution,[status(thm)],[f163,f94])).
% 0.13/0.42 fof(f351,plain,(
% 0.13/0.42 p3(f13(c31,c34),f13(c31,f15(f17(c33,c34),c35)))),
% 0.13/0.42 inference(resolution,[status(thm)],[f203,f119])).
% 0.13/0.42 fof(f522,plain,(
% 0.13/0.42 ![X0,X1,X2,X3]: (p25(X0,X1)|~p4(f5(c29,f13(c31,f15(c32,X2))),X0)|~p3(f13(c31,X3),X1)|~p12(X3,X2))),
% 0.13/0.42 inference(resolution,[status(thm)],[f192,f50])).
% 0.13/0.42 fof(f525,plain,(
% 0.13/0.42 ![X0,X1,X2]: (p25(f5(c29,f13(c31,f15(c32,X0))),X1)|~p3(f13(c31,X2),X1)|~p12(X2,X0))),
% 0.13/0.42 inference(resolution,[status(thm)],[f522,f54])).
% 0.13/0.42 fof(f539,plain,(
% 0.13/0.42 ![X0,X1]: (p25(f5(c29,f13(c31,f15(c32,X0))),X1)|~p3(f13(c31,X0),X1))),
% 0.13/0.42 inference(resolution,[status(thm)],[f525,f62])).
% 0.13/0.42 fof(f542,plain,(
% 0.13/0.42 ![X0,X1,X2]: (p25(f5(c29,f13(c31,f15(c32,X0))),X1)|~p3(X2,f13(c31,X0))|~p3(X2,X1))),
% 0.13/0.42 inference(resolution,[status(thm)],[f539,f77])).
% 0.13/0.42 fof(f548,plain,(
% 0.13/0.42 ![X0]: (p25(f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35)))),X0)|~p3(f13(c31,c34),X0))),
% 0.13/0.42 inference(resolution,[status(thm)],[f542,f351])).
% 0.13/0.42 fof(f583,plain,(
% 0.13/0.42 p25(f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34))),
% 0.13/0.42 inference(resolution,[status(thm)],[f548,f55])).
% 0.13/0.42 fof(f585,plain,(
% 0.13/0.42 p25(f5(f7(c28,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34))),
% 0.13/0.42 inference(resolution,[status(thm)],[f583,f95])).
% 0.13/0.42 fof(f587,plain,(
% 0.13/0.42 $false),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f585,f119])).
% 0.13/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.44 % Elapsed time: 0.068435 seconds
% 0.13/0.44 % CPU time: 0.271321 seconds
% 0.13/0.44 % Total memory used: 24.324 MB
% 0.13/0.44 % Net memory used: 23.963 MB
%------------------------------------------------------------------------------