%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : REL008-4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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 02:03:13 PM UTC 2026
% Result : Unsatisfiable 133.99s 17.49s
% Output : CNFRefutation 102.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 14
% Syntax : Number of formulae : 123 ( 88 unt; 2 def)
% Number of atoms : 158 ( 119 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 69 ( 34 ~; 33 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 215 ( 215 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] : join(A,B) = join(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B,C] : join(A,join(B,C)) = join(join(A,B),C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B] : A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] : meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] : composition(A,one) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B,C] : composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] : converse(converse(A)) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B] : converse(join(A,B)) = join(converse(A),converse(B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A,B] : converse(composition(A,B)) = composition(converse(B),converse(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] : zero = meet(A,complement(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A,B,C] : join(meet(composition(A,B),C),meet(composition(A,meet(B,composition(converse(A),C))),C)) = meet(composition(A,meet(B,composition(converse(A),C))),C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,negated_conjecture,
( join(join(composition(sk1,join(sk2,sk3)),composition(sk1,sk2)),composition(sk1,sk3)) != join(composition(sk1,sk2),composition(sk1,sk3))
| join(join(composition(sk1,sk2),composition(sk1,sk3)),composition(sk1,join(sk2,sk3))) != composition(sk1,join(sk2,sk3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f19,plain,
! [X0,X1,X2] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f20,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f21,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X0,X1),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f23,plain,
! [X0] : X0 = composition(X0,one),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f24,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f25,plain,
! [X0] : converse(converse(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f26,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f27,plain,
! [X0,X1] : composition(converse(X0),converse(X1)) = converse(composition(X1,X0)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f30,plain,
! [X0] : meet(X0,complement(X0)) = zero,
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f32,plain,
! [X0,X1,X2] : meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2) = join(meet(composition(X0,X1),X2),meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2)),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f34,plain,
( join(join(composition(sk1,join(sk2,sk3)),composition(sk1,sk2)),composition(sk1,sk3)) != join(composition(sk1,sk2),composition(sk1,sk3))
| join(join(composition(sk1,sk2),composition(sk1,sk3)),composition(sk1,join(sk2,sk3))) != composition(sk1,join(sk2,sk3)) ),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f35,definition,
( sQ0_spl
<=> join(join(composition(sk1,sk2),composition(sk1,sk3)),composition(sk1,join(sk2,sk3))) = composition(sk1,join(sk2,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f37,plain,
( sQ0_spl
| join(join(composition(sk1,sk2),composition(sk1,sk3)),composition(sk1,join(sk2,sk3))) != composition(sk1,join(sk2,sk3)) ),
inference(component_clause,[status(thm)],[f35]) ).
fof(f38,definition,
( sQ1_spl
<=> join(join(composition(sk1,join(sk2,sk3)),composition(sk1,sk2)),composition(sk1,sk3)) = join(composition(sk1,sk2),composition(sk1,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f40,plain,
( sQ1_spl
| join(join(composition(sk1,join(sk2,sk3)),composition(sk1,sk2)),composition(sk1,sk3)) != join(composition(sk1,sk2),composition(sk1,sk3)) ),
inference(component_clause,[status(thm)],[f38]) ).
fof(f41,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f34,f35,f38]) ).
fof(f43,plain,
( sQ0_spl
| join(composition(sk1,join(sk2,sk3)),join(composition(sk1,sk2),composition(sk1,sk3))) != composition(sk1,join(sk2,sk3)) ),
inference(forward_demodulation,[status(thm)],[f18,f37]) ).
fof(f44,plain,
( sQ0_spl
| join(composition(sk1,join(sk3,sk2)),join(composition(sk1,sk2),composition(sk1,sk3))) != composition(sk1,join(sk2,sk3)) ),
inference(forward_demodulation,[status(thm)],[f18,f43]) ).
fof(f45,plain,
( sQ0_spl
| join(composition(sk1,join(sk3,sk2)),join(composition(sk1,sk3),composition(sk1,sk2))) != composition(sk1,join(sk2,sk3)) ),
inference(forward_demodulation,[status(thm)],[f18,f44]) ).
fof(f46,plain,
( sQ0_spl
| composition(sk1,join(sk3,sk2)) != join(composition(sk1,join(sk3,sk2)),join(composition(sk1,sk3),composition(sk1,sk2))) ),
inference(forward_demodulation,[status(thm)],[f18,f45]) ).
fof(f47,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[status(thm)],[f18,f20]) ).
fof(f48,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),meet(X0,X1)) = X0,
inference(backward_demodulation,[status(thm)],[f21,f47]) ).
fof(f49,plain,
! [X0,X1] : join(meet(X0,X1),complement(join(complement(X0),X1))) = X0,
inference(forward_demodulation,[status(thm)],[f18,f48]) ).
fof(f59,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(paramodulation,[status(thm)],[f18,f19]) ).
fof(f61,plain,
! [X0,X1,X2] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(paramodulation,[status(thm)],[f18,f19]) ).
fof(f65,plain,
( sQ0_spl
| join(composition(sk1,sk3),join(composition(sk1,sk2),composition(sk1,join(sk3,sk2)))) != composition(sk1,join(sk3,sk2)) ),
inference(backward_demodulation,[status(thm)],[f59,f46]) ).
fof(f66,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(forward_demodulation,[status(thm)],[f19,f61]) ).
fof(f93,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X2,join(X1,X0)),
inference(paramodulation,[status(thm)],[f18,f59]) ).
fof(f141,plain,
! [X0,X1,X2] : join(composition(X0,X1),composition(X2,X1)) = composition(join(X2,X0),X1),
inference(paramodulation,[status(thm)],[f24,f18]) ).
fof(f143,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = composition(join(X1,X0),X2),
inference(forward_demodulation,[status(thm)],[f24,f141]) ).
fof(f198,plain,
! [X0,X1,X2] : join(join(X0,X1),X2) = join(X0,join(X2,X1)),
inference(paramodulation,[status(thm)],[f66,f18]) ).
fof(f202,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X0,join(X2,X1)),
inference(forward_demodulation,[status(thm)],[f19,f198]) ).
fof(f226,plain,
! [X0] : join(zero,complement(join(complement(X0),complement(X0)))) = X0,
inference(paramodulation,[status(thm)],[f30,f49]) ).
fof(f227,plain,
! [X0] : X0 = join(zero,meet(X0,X0)),
inference(forward_demodulation,[status(thm)],[f21,f226]) ).
fof(f345,plain,
! [X0,X1] : composition(X0,converse(X1)) = converse(composition(X1,converse(X0))),
inference(paramodulation,[status(thm)],[f25,f27]) ).
fof(f346,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(paramodulation,[status(thm)],[f25,f27]) ).
fof(f354,plain,
! [X0,X1,X2] : join(composition(X0,converse(X1)),converse(composition(X1,X2))) = composition(join(X0,converse(X2)),converse(X1)),
inference(paramodulation,[status(thm)],[f27,f24]) ).
fof(f436,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X1,X0),
inference(paramodulation,[status(thm)],[f18,f21]) ).
fof(f448,plain,
! [X0,X1] : meet(join(complement(X0),complement(X1)),meet(X0,X1)) = zero,
inference(paramodulation,[status(thm)],[f21,f30]) ).
fof(f457,plain,
! [X0,X1] : zero = meet(meet(X0,X1),join(complement(X0),complement(X1))),
inference(backward_demodulation,[status(thm)],[f471,f448]) ).
fof(f470,plain,
! [X0,X1,X2] : meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2) = join(meet(composition(X0,X1),X2),meet(X2,composition(X0,meet(X1,composition(converse(X0),X2))))),
inference(backward_demodulation,[status(thm)],[f471,f32]) ).
fof(f471,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f21,f436]) ).
fof(f481,plain,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),meet(X2,composition(X0,meet(X1,composition(converse(X0),X2))))) = meet(X2,composition(X0,meet(X1,composition(converse(X0),X2)))),
inference(forward_demodulation,[status(thm)],[f471,f470]) ).
fof(f506,plain,
! [X0,X1,X2,X3] : join(meet(X0,composition(X1,meet(X2,composition(converse(X1),X0)))),X3) = join(meet(composition(X1,X2),X0),join(meet(X0,composition(X1,meet(X2,composition(converse(X1),X0)))),X3)),
inference(paramodulation,[status(thm)],[f481,f19]) ).
fof(f518,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X1),converse(X0)),
inference(paramodulation,[status(thm)],[f18,f26]) ).
fof(f520,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(paramodulation,[status(thm)],[f25,f26]) ).
fof(f521,plain,
! [X0,X1] : join(converse(X0),X1) = converse(join(X0,converse(X1))),
inference(paramodulation,[status(thm)],[f25,f26]) ).
fof(f531,plain,
! [X0,X1] : converse(join(X0,X1)) = converse(join(X1,X0)),
inference(forward_demodulation,[status(thm)],[f26,f518]) ).
fof(f1236,plain,
! [X0,X1,X2,X3] : join(X0,join(X1,join(X2,X3))) = join(X0,join(X3,join(X1,X2))),
inference(paramodulation,[status(thm)],[f19,f202]) ).
fof(f1955,plain,
! [X0,X1,X2] : converse(join(converse(composition(X0,X1)),composition(X2,converse(X0)))) = converse(composition(join(X2,converse(X1)),converse(X0))),
inference(paramodulation,[status(thm)],[f354,f531]) ).
fof(f1971,plain,
! [X0,X1,X2] : join(composition(X0,X1),converse(composition(X2,converse(X0)))) = converse(composition(join(X2,converse(X1)),converse(X0))),
inference(forward_demodulation,[status(thm)],[f520,f1955]) ).
fof(f1972,plain,
! [X0,X1,X2] : join(composition(X0,X1),composition(X0,converse(X2))) = converse(composition(join(X2,converse(X1)),converse(X0))),
inference(forward_demodulation,[status(thm)],[f345,f1971]) ).
fof(f1973,plain,
! [X0,X1,X2] : join(composition(X0,X1),composition(X0,converse(X2))) = composition(X0,converse(join(X2,converse(X1)))),
inference(forward_demodulation,[status(thm)],[f345,f1972]) ).
fof(f1974,plain,
! [X0,X1,X2] : join(composition(X0,X1),composition(X0,converse(X2))) = composition(X0,join(converse(X2),X1)),
inference(forward_demodulation,[status(thm)],[f521,f1973]) ).
fof(f2369,plain,
! [X0,X1,X2] : converse(composition(converse(join(X0,X1)),X2)) = composition(converse(X2),join(X1,X0)),
inference(paramodulation,[status(thm)],[f531,f346]) ).
fof(f2405,plain,
! [X0,X1,X2] : composition(converse(X0),join(X1,X2)) = composition(converse(X0),join(X2,X1)),
inference(forward_demodulation,[status(thm)],[f346,f2369]) ).
fof(f2698,plain,
! [X0,X1,X2] : composition(X0,join(X1,X2)) = composition(converse(converse(X0)),join(X2,X1)),
inference(paramodulation,[status(thm)],[f25,f2405]) ).
fof(f2834,plain,
! [X0,X1,X2] : composition(X0,join(X1,X2)) = composition(X0,join(X2,X1)),
inference(forward_demodulation,[status(thm)],[f25,f2698]) ).
fof(f2981,plain,
! [X0,X1,X2,X3] : composition(X0,join(X1,join(X2,X3))) = composition(X0,join(join(X2,X1),X3)),
inference(paramodulation,[status(thm)],[f93,f2834]) ).
fof(f3009,plain,
! [X0,X1,X2,X3] : composition(X0,join(join(X1,X2),X3)) = composition(X0,join(X1,join(X3,X2))),
inference(paramodulation,[status(thm)],[f66,f2834]) ).
fof(f3022,plain,
! [X0,X1,X2,X3] : composition(join(X0,X1),join(X2,X3)) = composition(join(X1,X0),join(X3,X2)),
inference(paramodulation,[status(thm)],[f2834,f143]) ).
fof(f3100,plain,
! [X0,X1,X2,X3] : composition(X0,join(X1,join(X2,X3))) = composition(X0,join(X2,join(X1,X3))),
inference(forward_demodulation,[status(thm)],[f19,f2981]) ).
fof(f3105,plain,
! [X0,X1,X2,X3] : composition(X0,join(X1,join(X2,X3))) = composition(X0,join(X1,join(X3,X2))),
inference(forward_demodulation,[status(thm)],[f19,f3009]) ).
fof(f4095,plain,
! [X0,X1,X2] : join(composition(X0,X1),composition(X0,X2)) = composition(X0,join(converse(converse(X2)),X1)),
inference(paramodulation,[status(thm)],[f25,f1974]) ).
fof(f4202,plain,
( sQ0_spl
| join(composition(sk1,sk3),composition(sk1,join(join(sk3,sk2),sk2))) != composition(sk1,join(sk3,sk2)) ),
inference(backward_demodulation,[status(thm)],[f4208,f65]) ).
fof(f4208,plain,
! [X0,X1,X2] : composition(X0,join(X1,X2)) = join(composition(X0,X2),composition(X0,X1)),
inference(forward_demodulation,[status(thm)],[f25,f4095]) ).
fof(f4210,plain,
( sQ0_spl
| composition(sk1,join(join(join(sk3,sk2),sk2),sk3)) != composition(sk1,join(sk3,sk2)) ),
inference(forward_demodulation,[status(thm)],[f4208,f4202]) ).
fof(f4211,plain,
( sQ0_spl
| composition(sk1,join(sk3,join(join(sk3,sk2),sk2))) != composition(sk1,join(sk3,sk2)) ),
inference(forward_demodulation,[status(thm)],[f2834,f4210]) ).
fof(f4212,plain,
( sQ0_spl
| composition(sk1,join(sk3,join(sk2,join(sk3,sk2)))) != composition(sk1,join(sk3,sk2)) ),
inference(forward_demodulation,[status(thm)],[f3105,f4211]) ).
fof(f4213,plain,
( sQ0_spl
| composition(sk1,join(sk3,sk2)) != composition(sk1,join(sk3,join(sk3,join(sk2,sk2)))) ),
inference(forward_demodulation,[status(thm)],[f1236,f4212]) ).
fof(f4252,plain,
! [X0,X1] : composition(X0,join(X1,X1)) = composition(join(X0,X0),X1),
inference(paramodulation,[status(thm)],[f4208,f24]) ).
fof(f4276,plain,
! [X0,X1,X2,X3] : join(X0,composition(X1,join(X2,X3))) = join(composition(X1,X3),join(composition(X1,X2),X0)),
inference(paramodulation,[status(thm)],[f4208,f59]) ).
fof(f4435,plain,
! [X0,X1,X2] : composition(X0,join(join(X1,X1),X2)) = join(composition(X0,X2),composition(join(X0,X0),X1)),
inference(paramodulation,[status(thm)],[f4252,f4208]) ).
fof(f4461,plain,
! [X0,X1,X2] : composition(X0,join(join(X1,X2),join(X1,X2))) = composition(join(X0,X0),join(X2,X1)),
inference(paramodulation,[status(thm)],[f4252,f3022]) ).
fof(f4506,plain,
! [X0,X1,X2] : composition(X0,join(X1,join(join(X1,X2),X2))) = composition(join(X0,X0),join(X2,X1)),
inference(forward_demodulation,[status(thm)],[f3100,f4461]) ).
fof(f4507,plain,
! [X0,X1,X2] : composition(X0,join(X1,join(X2,join(X1,X2)))) = composition(join(X0,X0),join(X2,X1)),
inference(forward_demodulation,[status(thm)],[f3105,f4506]) ).
fof(f4570,plain,
! [X0,X1,X2] : join(composition(X0,X1),composition(join(X0,X0),X2)) = composition(X0,join(X2,join(X2,X1))),
inference(forward_demodulation,[status(thm)],[f19,f4435]) ).
fof(f5588,plain,
! [X0,X1,X2] : join(meet(X0,composition(X1,meet(X2,composition(converse(X1),X0)))),complement(join(complement(X0),composition(X1,meet(X2,composition(converse(X1),X0)))))) = join(meet(composition(X1,X2),X0),X0),
inference(paramodulation,[status(thm)],[f49,f506]) ).
fof(f5682,plain,
! [X0,X1,X2] : X0 = join(meet(composition(X1,X2),X0),X0),
inference(forward_demodulation,[status(thm)],[f49,f5588]) ).
fof(f5683,plain,
! [X0,X1,X2] : X0 = join(X0,meet(composition(X1,X2),X0)),
inference(forward_demodulation,[status(thm)],[f18,f5682]) ).
fof(f6191,plain,
! [X0,X1] : X0 = join(X0,meet(X1,X0)),
inference(paramodulation,[status(thm)],[f23,f5683]) ).
fof(f6426,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
inference(paramodulation,[status(thm)],[f471,f6191]) ).
fof(f6752,plain,
! [X0,X1] : join(meet(X0,X1),zero) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f457,f6426]) ).
fof(f6790,plain,
! [X0] : meet(X0,X0) = X0,
inference(backward_demodulation,[status(thm)],[f6840,f227]) ).
fof(f6840,plain,
! [X0,X1] : join(zero,meet(X0,X1)) = meet(X0,X1),
inference(forward_demodulation,[status(thm)],[f18,f6752]) ).
fof(f6919,plain,
! [X0] : X0 = join(X0,X0),
inference(paramodulation,[status(thm)],[f6790,f6191]) ).
fof(f6953,plain,
( sQ0_spl
| composition(sk1,join(sk3,join(sk3,sk2))) != composition(sk1,join(sk3,sk2)) ),
inference(backward_demodulation,[status(thm)],[f6919,f4213]) ).
fof(f7028,plain,
! [X0,X1,X2] : join(composition(X0,X1),composition(X0,X2)) = composition(X0,join(X2,join(X2,X1))),
inference(backward_demodulation,[status(thm)],[f6919,f4570]) ).
fof(f7076,plain,
! [X0,X1,X2] : composition(X0,join(X1,join(X2,join(X1,X2)))) = composition(X0,join(X2,X1)),
inference(backward_demodulation,[status(thm)],[f6919,f4507]) ).
fof(f7624,plain,
( sQ0_spl
| composition(sk1,join(sk3,sk2)) != composition(sk1,join(sk3,sk2)) ),
inference(backward_demodulation,[status(thm)],[f7625,f6953]) ).
fof(f7625,plain,
! [X0,X1,X2] : composition(X0,join(X1,join(X1,X2))) = composition(X0,join(X1,X2)),
inference(forward_demodulation,[status(thm)],[f4208,f7028]) ).
fof(f7626,plain,
( sQ0_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f7624]) ).
fof(f7627,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f7626]) ).
fof(f7643,plain,
( sQ1_spl
| join(composition(sk1,join(sk2,sk3)),join(composition(sk1,sk2),composition(sk1,sk3))) != join(composition(sk1,sk2),composition(sk1,sk3)) ),
inference(forward_demodulation,[status(thm)],[f19,f40]) ).
fof(f7644,plain,
( sQ1_spl
| join(composition(sk1,join(sk2,sk3)),join(composition(sk1,sk3),composition(sk1,sk2))) != join(composition(sk1,sk2),composition(sk1,sk3)) ),
inference(forward_demodulation,[status(thm)],[f202,f7643]) ).
fof(f7645,plain,
( sQ1_spl
| join(composition(sk1,sk2),join(composition(sk1,sk3),composition(sk1,join(sk2,sk3)))) != join(composition(sk1,sk2),composition(sk1,sk3)) ),
inference(forward_demodulation,[status(thm)],[f93,f7644]) ).
fof(f7646,plain,
( sQ1_spl
| join(composition(sk1,sk3),join(composition(sk1,sk2),composition(sk1,join(sk2,sk3)))) != join(composition(sk1,sk2),composition(sk1,sk3)) ),
inference(forward_demodulation,[status(thm)],[f66,f7645]) ).
fof(f7647,plain,
( sQ1_spl
| join(composition(sk1,join(sk2,sk3)),composition(sk1,join(sk2,sk3))) != join(composition(sk1,sk2),composition(sk1,sk3)) ),
inference(forward_demodulation,[status(thm)],[f4276,f7646]) ).
fof(f7648,plain,
( sQ1_spl
| composition(sk1,join(join(sk2,sk3),join(sk2,sk3))) != join(composition(sk1,sk2),composition(sk1,sk3)) ),
inference(forward_demodulation,[status(thm)],[f4208,f7647]) ).
fof(f7649,plain,
( sQ1_spl
| composition(sk1,join(join(sk2,sk3),join(sk3,sk2))) != join(composition(sk1,sk2),composition(sk1,sk3)) ),
inference(forward_demodulation,[status(thm)],[f3105,f7648]) ).
fof(f7650,plain,
( sQ1_spl
| composition(sk1,join(join(sk3,sk2),join(sk2,sk3))) != join(composition(sk1,sk2),composition(sk1,sk3)) ),
inference(forward_demodulation,[status(thm)],[f2834,f7649]) ).
fof(f7651,plain,
( sQ1_spl
| composition(sk1,join(join(sk3,sk2),join(sk3,sk2))) != join(composition(sk1,sk2),composition(sk1,sk3)) ),
inference(forward_demodulation,[status(thm)],[f3105,f7650]) ).
fof(f7652,plain,
( sQ1_spl
| composition(sk1,join(sk3,join(join(sk3,sk2),sk2))) != join(composition(sk1,sk2),composition(sk1,sk3)) ),
inference(forward_demodulation,[status(thm)],[f3100,f7651]) ).
fof(f7653,plain,
( sQ1_spl
| composition(sk1,join(sk3,join(sk2,join(sk3,sk2)))) != join(composition(sk1,sk2),composition(sk1,sk3)) ),
inference(forward_demodulation,[status(thm)],[f3105,f7652]) ).
fof(f7654,plain,
( sQ1_spl
| composition(sk1,join(sk2,sk3)) != join(composition(sk1,sk2),composition(sk1,sk3)) ),
inference(forward_demodulation,[status(thm)],[f7076,f7653]) ).
fof(f7655,plain,
( sQ1_spl
| composition(sk1,join(sk3,sk2)) != join(composition(sk1,sk2),composition(sk1,sk3)) ),
inference(forward_demodulation,[status(thm)],[f2834,f7654]) ).
fof(f7656,plain,
( sQ1_spl
| composition(sk1,join(sk3,sk2)) != composition(sk1,join(sk3,sk2)) ),
inference(forward_demodulation,[status(thm)],[f4208,f7655]) ).
fof(f7657,plain,
( sQ1_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f7656]) ).
fof(f7658,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f7657]) ).
fof(f7659,plain,
$false,
inference(sat_refutation,[status(thm)],[f41,f7627,f7658]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : REL008-4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n005.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 03:58:02 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.45 % Drodi V4.1.1
% 133.99/17.49 % Refutation found
% 133.99/17.49 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 133.99/17.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 15.21/17.63 % Elapsed time: 17.179423 seconds
% 15.21/17.63 % CPU time: 135.415461 seconds
% 15.21/17.63 % Total memory used: 572.195 MB
% 15.21/17.63 % Net memory used: 545.759 MB
%------------------------------------------------------------------------------