%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN116-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:18:59 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN116-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n017.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 10:39:27 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 0.14/0.59 % Refutation found
% 0.14/0.59 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.59 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.59 fof(f1,axiom,(
% 0.14/0.59 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 0.14/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.59 fof(f6,axiom,(
% 0.14/0.59 s0(b) = true ),
% 0.14/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.59 fof(f15,axiom,(
% 0.14/0.59 (![X]: (p0(b,X) = true ))),
% 0.14/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.59 fof(f27,axiom,(
% 0.14/0.59 n0(d,c) = true ),
% 0.14/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.59 fof(f41,axiom,(
% 0.14/0.59 (![H,G]: (ifeq(n0(H,G),true,l1(G,G),true) = true ))),
% 0.14/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.59 fof(f68,axiom,(
% 0.14/0.59 (![H,I]: (ifeq(p0(H,I),true,ifeq(s0(H),true,m1(H,I,H),true),true) = true ))),
% 0.14/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.59 fof(f122,axiom,(
% 0.14/0.59 (![C,B]: (ifeq(p0(C,B),true,p1(B,B,B),true) = true ))),
% 0.14/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.59 fof(f173,axiom,(
% 0.14/0.59 (![B,C,A]: (ifeq(p1(B,C,A),true,n2(A),true) = true ))),
% 0.14/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.59 fof(f212,axiom,(
% 0.14/0.59 (![E,D]: (ifeq(m1(E,D,E),true,p2(D,E,D),true) = true ))),
% 0.14/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.59 fof(f278,axiom,(
% 0.14/0.59 (![H]: (ifeq(n2(H),true,p3(H,H,H),true) = true ))),
% 0.14/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.59 fof(f301,axiom,(
% 0.14/0.59 (![B,D,C]: (ifeq(p2(B,D,C),true,r3(B,C,B),true) = true ))),
% 0.14/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.59 fof(f331,axiom,(
% 0.14/0.59 (![B,C,D,A]: (ifeq(p3(B,C,D),true,ifeq(l1(A,C),true,s4(A),true),true) = true ))),
% 0.14/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.59 fof(f332,axiom,(
% 0.14/0.59 (![F,G,E]: (ifeq(s4(F),true,ifeq(r3(G,E,E),true,k5(E),true),true) = true ))),
% 0.14/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.59 fof(f363,negated_conjecture,(
% 0.14/0.59 k5(b) != true ),
% 0.14/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.59 fof(f364,plain,(
% 0.14/0.59 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 0.14/0.59 inference(cnf_transformation,[status(thm)],[f1])).
% 0.14/0.59 fof(f369,plain,(
% 0.14/0.59 s0(b)=true),
% 0.14/0.59 inference(cnf_transformation,[status(thm)],[f6])).
% 0.14/0.59 fof(f378,plain,(
% 0.14/0.59 ![X0]: (p0(b,X0)=true)),
% 0.14/0.59 inference(cnf_transformation,[status(thm)],[f15])).
% 0.14/0.59 fof(f390,plain,(
% 0.14/0.59 n0(d,c)=true),
% 0.14/0.59 inference(cnf_transformation,[status(thm)],[f27])).
% 0.14/0.59 fof(f404,plain,(
% 0.14/0.59 ![X0,X1]: (ifeq(n0(X0,X1),true,l1(X1,X1),true)=true)),
% 0.14/0.59 inference(cnf_transformation,[status(thm)],[f41])).
% 0.14/0.59 fof(f431,plain,(
% 0.14/0.59 ![X0,X1]: (ifeq(p0(X0,X1),true,ifeq(s0(X0),true,m1(X0,X1,X0),true),true)=true)),
% 0.14/0.59 inference(cnf_transformation,[status(thm)],[f68])).
% 0.14/0.59 fof(f485,plain,(
% 0.14/0.59 ![X0,X1]: (ifeq(p0(X0,X1),true,p1(X1,X1,X1),true)=true)),
% 0.14/0.59 inference(cnf_transformation,[status(thm)],[f122])).
% 0.14/0.59 fof(f536,plain,(
% 0.14/0.59 ![X0,X1,X2]: (ifeq(p1(X0,X1,X2),true,n2(X2),true)=true)),
% 0.14/0.59 inference(cnf_transformation,[status(thm)],[f173])).
% 0.14/0.59 fof(f575,plain,(
% 0.14/0.59 ![X0,X1]: (ifeq(m1(X0,X1,X0),true,p2(X1,X0,X1),true)=true)),
% 0.14/0.59 inference(cnf_transformation,[status(thm)],[f212])).
% 0.14/0.59 fof(f641,plain,(
% 0.14/0.59 ![X0]: (ifeq(n2(X0),true,p3(X0,X0,X0),true)=true)),
% 0.14/0.59 inference(cnf_transformation,[status(thm)],[f278])).
% 0.14/0.59 fof(f664,plain,(
% 0.14/0.59 ![X0,X1,X2]: (ifeq(p2(X0,X1,X2),true,r3(X0,X2,X0),true)=true)),
% 0.14/0.59 inference(cnf_transformation,[status(thm)],[f301])).
% 0.14/0.59 fof(f694,plain,(
% 0.14/0.59 ![X0,X1,X2,X3]: (ifeq(p3(X0,X1,X2),true,ifeq(l1(X3,X1),true,s4(X3),true),true)=true)),
% 0.14/0.59 inference(cnf_transformation,[status(thm)],[f331])).
% 0.14/0.59 fof(f695,plain,(
% 0.14/0.59 ![X0,X1,X2]: (ifeq(s4(X0),true,ifeq(r3(X1,X2,X2),true,k5(X2),true),true)=true)),
% 0.14/0.59 inference(cnf_transformation,[status(thm)],[f332])).
% 0.14/0.59 fof(f726,plain,(
% 0.14/0.59 ~k5(b)=true),
% 0.14/0.59 inference(cnf_transformation,[status(thm)],[f363])).
% 0.14/0.59 fof(f727,definition,(
% 0.14/0.59 sF0_fnc=k5(b)),
% 0.14/0.59 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.14/0.59 fof(f728,plain,(
% 0.14/0.59 ~sF0_fnc=true),
% 0.14/0.59 inference(definition_folding,[],[f726,f727])).
% 0.14/0.59 fof(f757,plain,(
% 0.14/0.59 ifeq(true,true,l1(c,c),true)=true),
% 0.14/0.59 inference(paramodulation,[status(thm)],[f390,f404])).
% 0.14/0.59 fof(f765,plain,(
% 0.14/0.59 l1(c,c)=true),
% 0.14/0.59 inference(forward_demodulation,[status(thm)],[f364,f757])).
% 0.14/0.62 fof(f1068,plain,(
% 0.14/0.62 ![X0]: (ifeq(true,true,ifeq(s0(b),true,m1(b,X0,b),true),true)=true)),
% 0.14/0.62 inference(paramodulation,[status(thm)],[f378,f431])).
% 0.14/0.62 fof(f1075,plain,(
% 0.14/0.62 ![X0]: (ifeq(s0(b),true,m1(b,X0,b),true)=true)),
% 0.14/0.62 inference(forward_demodulation,[status(thm)],[f364,f1068])).
% 0.14/0.62 fof(f1076,plain,(
% 0.14/0.62 ![X0]: (ifeq(true,true,m1(b,X0,b),true)=true)),
% 0.14/0.62 inference(forward_demodulation,[status(thm)],[f369,f1075])).
% 0.14/0.62 fof(f1077,plain,(
% 0.14/0.62 ![X0]: (m1(b,X0,b)=true)),
% 0.14/0.62 inference(forward_demodulation,[status(thm)],[f364,f1076])).
% 0.14/0.62 fof(f2609,plain,(
% 0.14/0.62 ![X0]: (ifeq(true,true,p1(X0,X0,X0),true)=true)),
% 0.14/0.62 inference(paramodulation,[status(thm)],[f378,f485])).
% 0.14/0.62 fof(f2617,plain,(
% 0.14/0.62 ![X0]: (p1(X0,X0,X0)=true)),
% 0.14/0.62 inference(forward_demodulation,[status(thm)],[f364,f2609])).
% 0.14/0.62 fof(f3586,plain,(
% 0.14/0.62 ![X0]: (ifeq(true,true,n2(X0),true)=true)),
% 0.14/0.62 inference(paramodulation,[status(thm)],[f2617,f536])).
% 0.14/0.62 fof(f3591,plain,(
% 0.14/0.62 ![X0]: (n2(X0)=true)),
% 0.14/0.62 inference(forward_demodulation,[status(thm)],[f364,f3586])).
% 0.14/0.62 fof(f3999,plain,(
% 0.14/0.62 ![X0]: (ifeq(true,true,p2(X0,b,X0),true)=true)),
% 0.14/0.62 inference(paramodulation,[status(thm)],[f1077,f575])).
% 0.14/0.62 fof(f4007,plain,(
% 0.14/0.62 ![X0]: (p2(X0,b,X0)=true)),
% 0.14/0.62 inference(forward_demodulation,[status(thm)],[f364,f3999])).
% 0.14/0.62 fof(f4517,plain,(
% 0.14/0.62 ![X0]: (ifeq(true,true,p3(X0,X0,X0),true)=true)),
% 0.14/0.62 inference(forward_demodulation,[status(thm)],[f3591,f641])).
% 0.14/0.62 fof(f4518,plain,(
% 0.14/0.62 ![X0]: (p3(X0,X0,X0)=true)),
% 0.14/0.62 inference(forward_demodulation,[status(thm)],[f364,f4517])).
% 0.14/0.62 fof(f5073,plain,(
% 0.14/0.62 ![X0]: (ifeq(true,true,r3(X0,X0,X0),true)=true)),
% 0.14/0.62 inference(paramodulation,[status(thm)],[f4007,f664])).
% 0.14/0.62 fof(f5083,plain,(
% 0.14/0.62 ![X0]: (r3(X0,X0,X0)=true)),
% 0.14/0.62 inference(forward_demodulation,[status(thm)],[f364,f5073])).
% 0.14/0.62 fof(f5400,plain,(
% 0.14/0.62 ![X0,X1]: (ifeq(true,true,ifeq(l1(X0,X1),true,s4(X0),true),true)=true)),
% 0.14/0.62 inference(paramodulation,[status(thm)],[f4518,f694])).
% 0.14/0.62 fof(f5406,plain,(
% 0.14/0.62 ![X0,X1]: (ifeq(l1(X0,X1),true,s4(X0),true)=true)),
% 0.14/0.62 inference(forward_demodulation,[status(thm)],[f364,f5400])).
% 0.14/0.62 fof(f5417,plain,(
% 0.14/0.62 ![X0,X1]: (ifeq(s4(X0),true,ifeq(true,true,k5(X1),true),true)=true)),
% 0.14/0.62 inference(paramodulation,[status(thm)],[f5083,f695])).
% 0.14/0.62 fof(f5419,plain,(
% 0.14/0.62 ![X0,X1]: (ifeq(s4(X0),true,k5(X1),true)=true)),
% 0.14/0.62 inference(forward_demodulation,[status(thm)],[f364,f5417])).
% 0.14/0.62 fof(f5425,plain,(
% 0.14/0.62 ![X0]: (ifeq(s4(X0),true,sF0_fnc,true)=true)),
% 0.14/0.62 inference(paramodulation,[status(thm)],[f727,f5419])).
% 0.14/0.62 fof(f5503,plain,(
% 0.14/0.62 ifeq(true,true,s4(c),true)=true),
% 0.14/0.62 inference(paramodulation,[status(thm)],[f765,f5406])).
% 0.14/0.62 fof(f5508,plain,(
% 0.14/0.62 s4(c)=true),
% 0.14/0.62 inference(forward_demodulation,[status(thm)],[f364,f5503])).
% 0.14/0.62 fof(f5517,plain,(
% 0.14/0.62 ifeq(true,true,sF0_fnc,true)=true),
% 0.14/0.62 inference(paramodulation,[status(thm)],[f5508,f5425])).
% 0.14/0.62 fof(f5522,plain,(
% 0.14/0.62 sF0_fnc=true),
% 0.14/0.62 inference(forward_demodulation,[status(thm)],[f364,f5517])).
% 0.14/0.62 fof(f5523,plain,(
% 0.14/0.62 $false),
% 0.14/0.62 inference(forward_subsumption_resolution,[status(thm)],[f5522,f728])).
% 0.14/0.62 % SZS output end CNFRefutation for theBenchmark.p
% 0.68/0.63 % Elapsed time: 0.254675 seconds
% 0.68/0.63 % CPU time: 1.731513 seconds
% 0.68/0.63 % Total memory used: 81.770 MB
% 0.68/0.63 % Net memory used: 79.305 MB
%------------------------------------------------------------------------------