%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWX185+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:13:22 PM UTC 2026
% Result : Theorem 206.79s 31.56s
% Output : CNFRefutation 136.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 18
% Syntax : Number of formulae : 85 ( 60 unt; 2 def)
% Number of atoms : 114 ( 97 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 56 ( 27 ~; 22 |; 0 &)
% ( 2 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 7 con; 0-2 aty)
% Number of variables : 149 ( 145 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,X2] : head(cons(X,X2)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,X2] : tail(cons(X,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
c != x,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X,X2,X3,X4] : z(X,X2) != x2(X3,X4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [X,X2] : z(X,X2) != eX,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [X,X2] : x2(X,X2) != eX,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [X] :
( X != z(proj1(X),proj2(X))
=> ( X != x2(proj12(X),proj22(X))
=> assoc(X) = X ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [A2,B2] : assoc(x2(A2,B2)) = x2(assoc(A2),assoc(B2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [Y] : append(nil,Y) = Y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [Y,Z,Xs] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [X] :
( X != x2(proj12(X),proj22(X))
=> linTerm(X) = lin(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A,B] : linTerm(x2(A,B)) = append(cons(c,nil),append(lin(z(A,B)),cons(d,nil))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [A,B] : lin(z(A,B)) = append(linTerm(A),append(cons(plus,nil),linTerm(B))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A3,B2] : lin(x2(A3,B2)) = append(lin(A3),append(cons(mul,nil),lin(B2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
lin(eX) = cons(x,nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,conjecture,
? [U,V] :
~ ( lin(U) = lin(V)
=> assoc(U) = assoc(V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,negated_conjecture,
~ ? [U,V] :
~ ( lin(U) = lin(V)
=> assoc(U) = assoc(V) ),
inference(negated_conjecture,[status(cth)],[f41]) ).
fof(f43,plain,
! [X0,X1] : head(cons(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f44,plain,
! [X0,X1] : X0 = tail(cons(X1,X0)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f47,plain,
c != x,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f65,plain,
! [X0,X1,X2,X3] : z(X0,X1) != x2(X2,X3),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f66,plain,
! [X0,X1] : eX != z(X0,X1),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f68,plain,
! [X0,X1] : eX != x2(X0,X1),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f71,plain,
! [X] :
( assoc(X) = X
| X = x2(proj12(X),proj22(X))
| X = z(proj1(X),proj2(X)) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f72,plain,
! [X0] :
( x2(proj12(X0),proj22(X0)) = X0
| assoc(X0) = X0
| X0 = z(proj1(X0),proj2(X0)) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f77,plain,
! [X0,X1] : x2(assoc(X0),assoc(X1)) = assoc(x2(X0,X1)),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f78,plain,
! [X0] : append(nil,X0) = X0,
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f79,plain,
! [X0,X1,X2] : cons(X0,append(X1,X2)) = append(cons(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f80,plain,
! [X] :
( linTerm(X) = lin(X)
| X = x2(proj12(X),proj22(X)) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f81,plain,
! [X0] :
( x2(proj12(X0),proj22(X0)) = X0
| linTerm(X0) = lin(X0) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f82,plain,
! [X0,X1] : linTerm(x2(X0,X1)) = append(cons(c,nil),append(lin(z(X0,X1)),cons(d,nil))),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f83,plain,
! [X0,X1] : lin(z(X0,X1)) = append(linTerm(X0),append(cons(plus,nil),linTerm(X1))),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f84,plain,
! [X0,X1] : lin(x2(X0,X1)) = append(lin(X0),append(cons(mul,nil),lin(X1))),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f85,plain,
cons(x,nil) = lin(eX),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f87,plain,
! [U,V] :
( assoc(U) = assoc(V)
| lin(U) != lin(V) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f88,plain,
! [X0,X1] :
( lin(X0) != lin(X1)
| assoc(X0) = assoc(X1) ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f598,plain,
! [X0,X1] : cons(X0,X1) = append(cons(X0,nil),X1),
inference(paramodulation,[status(thm)],[f78,f79]) ).
fof(f599,plain,
! [X0,X1,X2] : X0 = head(append(cons(X0,X1),X2)),
inference(paramodulation,[status(thm)],[f79,f43]) ).
fof(f602,plain,
! [X0,X1,X2] : tail(append(cons(X0,X1),X2)) = append(X1,X2),
inference(paramodulation,[status(thm)],[f79,f44]) ).
fof(f960,plain,
! [X0,X1,X2,X3] : head(append(append(cons(X0,X1),X2),X3)) = X0,
inference(paramodulation,[status(thm)],[f79,f599]) ).
fof(f961,plain,
! [X0,X1] : lin(z(X0,X1)) = append(linTerm(X0),cons(plus,linTerm(X1))),
inference(backward_demodulation,[status(thm)],[f598,f83]) ).
fof(f962,plain,
! [X0] : append(lin(eX),X0) = cons(x,X0),
inference(paramodulation,[status(thm)],[f85,f598]) ).
fof(f1221,plain,
! [X0] :
( assoc(X0) = X0
| X0 = z(proj1(X0),proj2(X0))
| eX != X0 ),
inference(paramodulation,[status(thm)],[f72,f68]) ).
fof(f1236,plain,
( assoc(eX) = eX
| eX = z(proj1(eX),proj2(eX)) ),
inference(destructive_equality_resolution,[status(thm)],[f1221]) ).
fof(f1237,plain,
assoc(eX) = eX,
inference(forward_subsumption_resolution,[status(thm)],[f1236,f66]) ).
fof(f1269,plain,
! [X0,X1] : lin(x2(X0,X1)) = append(lin(X0),cons(mul,lin(X1))),
inference(forward_demodulation,[status(thm)],[f598,f84]) ).
fof(f1274,plain,
! [X0,X1,X2] : cons(X0,lin(x2(X1,X2))) = append(cons(X0,lin(X1)),cons(mul,lin(X2))),
inference(paramodulation,[status(thm)],[f1269,f79]) ).
fof(f1278,plain,
! [X0] : assoc(x2(eX,X0)) = x2(eX,assoc(X0)),
inference(paramodulation,[status(thm)],[f1237,f77]) ).
fof(f1283,plain,
! [X0,X1] : linTerm(x2(X0,X1)) = cons(c,append(lin(z(X0,X1)),cons(d,nil))),
inference(forward_demodulation,[status(thm)],[f598,f82]) ).
fof(f1284,plain,
! [X0,X1] : linTerm(x2(X0,X1)) = append(cons(c,lin(z(X0,X1))),cons(d,nil)),
inference(forward_demodulation,[status(thm)],[f79,f1283]) ).
fof(f1386,plain,
! [X0,X1] :
( x2(proj12(z(X0,X1)),proj22(z(X0,X1))) = z(X0,X1)
| linTerm(x2(X0,X1)) = append(cons(c,linTerm(z(X0,X1))),cons(d,nil)) ),
inference(paramodulation,[status(thm)],[f81,f1284]) ).
fof(f1403,definition,
( sQ7_spl
<=> x2(proj12(eX),proj22(eX)) = eX ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1404,plain,
( ~ sQ7_spl
| x2(proj12(eX),proj22(eX)) = eX ),
inference(component_clause,[status(thm)],[f1403]) ).
fof(f1426,plain,
! [X0,X1] : append(cons(c,linTerm(z(X0,X1))),cons(d,nil)) = linTerm(x2(X0,X1)),
inference(forward_subsumption_resolution,[status(thm)],[f1386,f65]) ).
fof(f1443,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1404,f68]) ).
fof(f1444,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f1443]) ).
fof(f1686,plain,
! [X0,X1] : tail(linTerm(x2(X0,X1))) = append(lin(z(X0,X1)),cons(d,nil)),
inference(paramodulation,[status(thm)],[f1284,f602]) ).
fof(f3022,plain,
! [X0,X1,X2,X3] : cons(X0,cons(X1,lin(x2(X2,X3)))) = append(cons(X0,cons(X1,lin(X2))),cons(mul,lin(X3))),
inference(paramodulation,[status(thm)],[f1274,f79]) ).
fof(f3521,plain,
! [X0] :
( x2(proj12(eX),proj22(eX)) = eX
| append(linTerm(eX),X0) = cons(x,X0) ),
inference(paramodulation,[status(thm)],[f81,f962]) ).
fof(f3523,plain,
! [X0] : cons(x,cons(mul,lin(X0))) = lin(x2(eX,X0)),
inference(paramodulation,[status(thm)],[f962,f1269]) ).
fof(f3525,definition,
! [X0] :
( sQ27_spl
<=> append(linTerm(eX),X0) = cons(x,X0) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f3526,plain,
! [X0] :
( ~ sQ27_spl
| append(linTerm(eX),X0) = cons(x,X0) ),
inference(component_clause,[status(thm)],[f3525]) ).
fof(f3528,plain,
( sQ7_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f3521,f3525,f1403]) ).
fof(f3660,plain,
! [X0,X1,X2,X3,X4] : X0 = head(append(append(append(cons(X0,X1),X2),X3),X4)),
inference(paramodulation,[status(thm)],[f79,f960]) ).
fof(f4167,plain,
! [X0] :
( ~ sQ27_spl
| cons(x,cons(plus,linTerm(X0))) = lin(z(eX,X0)) ),
inference(paramodulation,[status(thm)],[f961,f3526]) ).
fof(f7344,plain,
! [X0,X1,X2,X3] : c = head(append(append(linTerm(x2(X0,X1)),X2),X3)),
inference(paramodulation,[status(thm)],[f1426,f3660]) ).
fof(f7687,plain,
! [X0,X1,X2,X3] : c = head(append(lin(z(x2(X0,X1),X2)),X3)),
inference(paramodulation,[status(thm)],[f961,f7344]) ).
fof(f7822,plain,
! [X0,X1,X2,X3] : head(append(lin(z(assoc(x2(X0,X1)),X2)),X3)) = c,
inference(paramodulation,[status(thm)],[f77,f7687]) ).
fof(f22927,plain,
! [X0,X1] :
( ~ sQ27_spl
| x = head(append(lin(z(eX,X0)),X1)) ),
inference(paramodulation,[status(thm)],[f4167,f599]) ).
fof(f23950,plain,
! [X0] :
( ~ sQ27_spl
| x = head(tail(linTerm(x2(eX,X0)))) ),
inference(paramodulation,[status(thm)],[f1686,f22927]) ).
fof(f23959,plain,
! [X0,X1,X2] : head(tail(linTerm(x2(assoc(x2(X0,X1)),X2)))) = c,
inference(paramodulation,[status(thm)],[f1686,f7822]) ).
fof(f25341,plain,
! [X0,X1,X2] : c = head(tail(linTerm(assoc(x2(x2(X0,X1),X2))))),
inference(paramodulation,[status(thm)],[f77,f23959]) ).
fof(f26001,plain,
! [X0,X1,X2] : c = head(tail(linTerm(assoc(x2(assoc(x2(X0,X1)),X2))))),
inference(paramodulation,[status(thm)],[f77,f25341]) ).
fof(f36107,plain,
! [X0,X1,X2] : head(tail(linTerm(assoc(assoc(x2(x2(X0,X1),X2)))))) = c,
inference(paramodulation,[status(thm)],[f77,f26001]) ).
fof(f39038,plain,
! [X0,X1] : cons(x,cons(mul,lin(x2(X0,X1)))) = append(lin(x2(eX,X0)),cons(mul,lin(X1))),
inference(paramodulation,[status(thm)],[f3523,f3022]) ).
fof(f39054,plain,
! [X0,X1] : lin(x2(eX,x2(X0,X1))) = append(lin(x2(eX,X0)),cons(mul,lin(X1))),
inference(forward_demodulation,[status(thm)],[f3523,f39038]) ).
fof(f39055,plain,
! [X0,X1] : lin(x2(x2(eX,X0),X1)) = lin(x2(eX,x2(X0,X1))),
inference(forward_demodulation,[status(thm)],[f1269,f39054]) ).
fof(f56879,plain,
! [X0,X1] : assoc(x2(x2(eX,X0),X1)) = assoc(x2(eX,x2(X0,X1))),
inference(resolution,[status(thm)],[f39055,f88]) ).
fof(f56919,plain,
! [X0,X1] : x2(eX,assoc(x2(X0,X1))) = assoc(x2(x2(eX,X0),X1)),
inference(forward_demodulation,[status(thm)],[f1278,f56879]) ).
fof(f58625,plain,
! [X0,X1] : head(tail(linTerm(assoc(x2(eX,assoc(x2(X0,X1))))))) = c,
inference(paramodulation,[status(thm)],[f56919,f36107]) ).
fof(f59030,plain,
! [X0,X1] : head(tail(linTerm(x2(eX,assoc(assoc(x2(X0,X1))))))) = c,
inference(forward_demodulation,[status(thm)],[f1278,f58625]) ).
fof(f59031,plain,
( ~ sQ27_spl
| x = c ),
inference(forward_demodulation,[status(thm)],[f23950,f59030]) ).
fof(f59032,plain,
( ~ sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f59031,f47]) ).
fof(f59033,plain,
~ sQ27_spl,
inference(contradiction_clause,[status(thm)],[f59032]) ).
fof(f59034,plain,
$false,
inference(sat_refutation,[status(thm)],[f1444,f3528,f59033]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX185+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/5.35 % Computer : n010.cluster.edu
% 0.07/5.35 % Model : x86_64 x86_64
% 0.07/5.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/5.35 % Memory : 8046.5625MB
% 0.07/5.35 % OS : Linux 6.8.0-71-generic
% 0.07/5.35 % CPULimit : 300
% 0.07/5.35 % WCLimit : 300
% 0.07/5.35 % DateTime : Mon Sep 21 10:31:16 UTC 2026
% 0.07/5.36 % CPUTime :
% 0.07/5.37 % Drodi V4.1.1
% 206.79/31.56 % Refutation found
% 206.79/31.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 206.79/31.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 26.50/31.77 % Elapsed time: 26.392394 seconds
% 26.50/31.77 % CPU time: 208.601100 seconds
% 26.50/31.77 % Total memory used: 1.206 GB
% 26.50/31.77 % Net memory used: 1.173 GB
%------------------------------------------------------------------------------