%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP025-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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 12:35:27 PM UTC 2026
% Result : Unsatisfiable 0.14s 5.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP025-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.37 % Computer : n013.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Sun Sep 20 19:53:44 UTC 2026
% 0.11/5.37 % CPUTime :
% 0.11/5.39 % Drodi V4.1.1
% 0.14/5.49 % Refutation found
% 0.14/5.49 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/5.49 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.49 fof(f1,axiom,(
% 0.14/5.49 (![Xg]: (group_member(identity_for(Xg),Xg) ))),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f2,axiom,(
% 0.14/5.49 (![Xg,X]: (product(Xg,identity_for(Xg),X,X) ))),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f4,axiom,(
% 0.14/5.49 (![X,Xg]: (( ~ group_member(X,Xg)| group_member(inverse(Xg,X),Xg) ) ))),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f6,axiom,(
% 0.14/5.49 (![Xg,X]: (product(Xg,X,inverse(Xg,X),identity_for(Xg)) ))),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f9,axiom,(
% 0.14/5.49 (![Xg,X,Y,Z,W]: (( ~ product(Xg,X,Y,Z)| ~ product(Xg,X,Y,W)| W = Z ) ))),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f12,hypothesis,(
% 0.14/5.49 group_member(a,g1) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f13,hypothesis,(
% 0.14/5.49 group_member(b,g1) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f14,hypothesis,(
% 0.14/5.49 group_member(c,g2) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f15,hypothesis,(
% 0.14/5.49 group_member(d,g2) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f16,hypothesis,(
% 0.14/5.49 (![X]: (( ~ group_member(X,g1)| X = a| X = b ) ))),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f17,hypothesis,(
% 0.14/5.49 (![X]: (( ~ group_member(X,g2)| X = c| X = d ) ))),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f18,hypothesis,(
% 0.14/5.49 product(g1,a,a,a) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f19,hypothesis,(
% 0.14/5.49 product(g1,a,b,b) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f20,hypothesis,(
% 0.14/5.49 product(g1,b,a,b) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f21,hypothesis,(
% 0.14/5.49 product(g1,b,b,a) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f22,hypothesis,(
% 0.14/5.49 product(g2,c,c,c) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f23,hypothesis,(
% 0.14/5.49 product(g2,c,d,d) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f24,hypothesis,(
% 0.14/5.49 product(g2,d,c,d) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f25,hypothesis,(
% 0.14/5.49 product(g2,d,d,c) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f26,hypothesis,(
% 0.14/5.49 an_isomorphism(a) = c ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f27,hypothesis,(
% 0.14/5.49 an_isomorphism(b) = d ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f28,hypothesis,(
% 0.14/5.49 group_member(d1,g1) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f29,hypothesis,(
% 0.14/5.49 group_member(d2,g1) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f30,hypothesis,(
% 0.14/5.49 group_member(d3,g1) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f31,hypothesis,(
% 0.14/5.49 product(g1,d1,d2,d3) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f32,negated_conjecture,(
% 0.14/5.49 ~ product(g2,an_isomorphism(d1),an_isomorphism(d2),an_isomorphism(d3)) ),
% 0.14/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.49 fof(f33,plain,(
% 0.14/5.49 ![X0]: (group_member(identity_for(X0),X0))),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f1])).
% 0.14/5.49 fof(f34,plain,(
% 0.14/5.49 ![X0,X1]: (product(X0,identity_for(X0),X1,X1))),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f2])).
% 0.14/5.49 fof(f36,plain,(
% 0.14/5.49 ![X0,X1]: (~group_member(X0,X1)|group_member(inverse(X1,X0),X1))),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/5.49 fof(f38,plain,(
% 0.14/5.49 ![X0,X1]: (product(X0,X1,inverse(X0,X1),identity_for(X0)))),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f6])).
% 0.14/5.49 fof(f41,plain,(
% 0.14/5.49 ![Z,W]: ((![Xg,X,Y]: (~product(Xg,X,Y,Z)|~product(Xg,X,Y,W)))|W=Z)),
% 0.14/5.49 inference(miniscoping,[status(thm)],[f9])).
% 0.14/5.49 fof(f42,plain,(
% 0.14/5.49 ![X0,X1,X2,X3,X4]: (~product(X0,X1,X2,X3)|~product(X0,X1,X2,X4)|X4=X3)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f41])).
% 0.14/5.49 fof(f47,plain,(
% 0.14/5.49 group_member(a,g1)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/5.49 fof(f48,plain,(
% 0.14/5.49 group_member(b,g1)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f13])).
% 0.14/5.49 fof(f49,plain,(
% 0.14/5.49 group_member(c,g2)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f14])).
% 0.14/5.49 fof(f50,plain,(
% 0.14/5.49 group_member(d,g2)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f15])).
% 0.14/5.49 fof(f51,plain,(
% 0.14/5.49 ![X0]: (~group_member(X0,g1)|X0=a|X0=b)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f16])).
% 0.14/5.49 fof(f52,plain,(
% 0.14/5.49 ![X0]: (~group_member(X0,g2)|X0=c|X0=d)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f17])).
% 0.14/5.49 fof(f53,plain,(
% 0.14/5.49 product(g1,a,a,a)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f18])).
% 0.14/5.49 fof(f54,plain,(
% 0.14/5.49 product(g1,a,b,b)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f19])).
% 0.14/5.49 fof(f55,plain,(
% 0.14/5.49 product(g1,b,a,b)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f20])).
% 0.14/5.49 fof(f56,plain,(
% 0.14/5.49 product(g1,b,b,a)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f21])).
% 0.14/5.49 fof(f57,plain,(
% 0.14/5.49 product(g2,c,c,c)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f22])).
% 0.14/5.49 fof(f58,plain,(
% 0.14/5.49 product(g2,c,d,d)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f23])).
% 0.14/5.49 fof(f59,plain,(
% 0.14/5.49 product(g2,d,c,d)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f24])).
% 0.14/5.49 fof(f60,plain,(
% 0.14/5.49 product(g2,d,d,c)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f25])).
% 0.14/5.49 fof(f61,plain,(
% 0.14/5.49 an_isomorphism(a)=c),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f26])).
% 0.14/5.49 fof(f62,plain,(
% 0.14/5.49 an_isomorphism(b)=d),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f27])).
% 0.14/5.49 fof(f63,plain,(
% 0.14/5.49 group_member(d1,g1)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f28])).
% 0.14/5.49 fof(f64,plain,(
% 0.14/5.49 group_member(d2,g1)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f29])).
% 0.14/5.49 fof(f65,plain,(
% 0.14/5.49 group_member(d3,g1)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f30])).
% 0.14/5.49 fof(f66,plain,(
% 0.14/5.49 product(g1,d1,d2,d3)),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f31])).
% 0.14/5.49 fof(f67,plain,(
% 0.14/5.49 ~product(g2,an_isomorphism(d1),an_isomorphism(d2),an_isomorphism(d3))),
% 0.14/5.49 inference(cnf_transformation,[status(thm)],[f32])).
% 0.14/5.49 fof(f70,plain,(
% 0.14/5.49 ![X0,X1,X2]: (~product(X0,identity_for(X0),X1,X2)|X2=X1)),
% 0.14/5.49 inference(resolution,[status(thm)],[f34,f42])).
% 0.14/5.49 fof(f74,plain,(
% 0.14/5.49 group_member(inverse(g1,b),g1)),
% 0.14/5.49 inference(resolution,[status(thm)],[f36,f48])).
% 0.14/5.49 fof(f76,plain,(
% 0.14/5.49 ![X0]: (group_member(inverse(X0,identity_for(X0)),X0))),
% 0.14/5.49 inference(resolution,[status(thm)],[f36,f33])).
% 0.14/5.49 fof(f79,plain,(
% 0.14/5.49 identity_for(g2)=c|identity_for(g2)=d),
% 0.14/5.49 inference(resolution,[status(thm)],[f52,f33])).
% 0.14/5.49 fof(f80,plain,(
% 0.14/5.49 d=c|d=d),
% 0.14/5.49 inference(resolution,[status(thm)],[f52,f50])).
% 0.14/5.49 fof(f81,plain,(
% 0.14/5.49 c=c|c=d),
% 0.14/5.49 inference(resolution,[status(thm)],[f52,f49])).
% 0.14/5.49 fof(f82,definition,(
% 0.14/5.49 sQ0_spl <=> (identity_for(g2)=c)),
% 0.14/5.49 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/5.49 fof(f83,plain,(
% 0.14/5.49 identity_for(g2)=c|~sQ0_spl),
% 0.14/5.49 inference(component_clause,[status(thm)],[f82])).
% 0.14/5.49 fof(f85,definition,(
% 0.14/5.49 sQ1_spl <=> (identity_for(g2)=d)),
% 0.14/5.49 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/5.49 fof(f86,plain,(
% 0.14/5.49 identity_for(g2)=d|~sQ1_spl),
% 0.14/5.49 inference(component_clause,[status(thm)],[f85])).
% 0.14/5.49 fof(f88,plain,(
% 0.14/5.49 sQ0_spl|sQ1_spl),
% 0.14/5.49 inference(split_clause,[status(thm)],[f79,f82,f85])).
% 0.14/5.49 fof(f89,definition,(
% 0.14/5.49 sQ2_spl <=> (d=c)),
% 0.14/5.49 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/5.49 fof(f90,plain,(
% 0.14/5.49 d=c|~sQ2_spl),
% 0.14/5.49 inference(component_clause,[status(thm)],[f89])).
% 0.14/5.49 fof(f92,definition,(
% 0.14/5.49 sQ3_spl <=> (d=d)),
% 0.14/5.49 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/5.49 fof(f95,plain,(
% 0.14/5.49 sQ2_spl|sQ3_spl),
% 0.14/5.49 inference(split_clause,[status(thm)],[f80,f89,f92])).
% 0.14/5.49 fof(f96,definition,(
% 0.14/5.49 sQ4_spl <=> (c=c)),
% 0.14/5.49 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/5.49 fof(f99,plain,(
% 0.14/5.49 sQ4_spl|sQ2_spl),
% 0.14/5.49 inference(split_clause,[status(thm)],[f81,f96,f89])).
% 0.14/5.49 fof(f100,plain,(
% 0.14/5.49 ![X0]: (~group_member(X0,g2)|X0=c|X0=c|~sQ2_spl)),
% 0.14/5.49 inference(backward_demodulation,[status(thm)],[f90,f52])).
% 0.14/5.49 fof(f102,plain,(
% 0.14/5.49 ![X0]: (~group_member(X0,g2)|X0=c|~sQ2_spl)),
% 0.14/5.49 inference(duplicate_literals_removal,[status(thm)],[f100])).
% 0.14/5.49 fof(f128,plain,(
% 0.14/5.49 ![X0]: (product(g2,c,X0,X0)|~sQ0_spl)),
% 0.14/5.49 inference(paramodulation,[status(thm)],[f83,f34])).
% 0.14/5.49 fof(f132,plain,(
% 0.14/5.49 identity_for(g2)=c|~sQ2_spl),
% 0.14/5.49 inference(resolution,[status(thm)],[f102,f33])).
% 0.14/5.49 fof(f141,plain,(
% 0.14/5.49 ![X0]: (~product(g1,d1,d2,X0)|X0=d3)),
% 0.14/5.49 inference(resolution,[status(thm)],[f66,f42])).
% 0.14/5.49 fof(f162,plain,(
% 0.14/5.49 inverse(g1,identity_for(g1))=a|inverse(g1,identity_for(g1))=b),
% 0.14/5.49 inference(resolution,[status(thm)],[f51,f76])).
% 0.14/5.49 fof(f163,plain,(
% 0.14/5.49 d3=a|d3=b),
% 0.14/5.49 inference(resolution,[status(thm)],[f51,f65])).
% 0.14/5.49 fof(f164,plain,(
% 0.14/5.49 d2=a|d2=b),
% 0.14/5.49 inference(resolution,[status(thm)],[f51,f64])).
% 0.14/5.49 fof(f165,plain,(
% 0.14/5.49 d1=a|d1=b),
% 0.14/5.49 inference(resolution,[status(thm)],[f51,f63])).
% 0.14/5.49 fof(f166,plain,(
% 0.14/5.49 b=a|b=b),
% 0.14/5.49 inference(resolution,[status(thm)],[f51,f48])).
% 0.14/5.49 fof(f167,plain,(
% 0.14/5.49 a=a|a=b),
% 0.14/5.49 inference(resolution,[status(thm)],[f51,f47])).
% 0.14/5.49 fof(f168,plain,(
% 0.14/5.49 identity_for(g1)=a|identity_for(g1)=b),
% 0.14/5.49 inference(resolution,[status(thm)],[f51,f33])).
% 0.14/5.49 fof(f169,definition,(
% 0.14/5.49 sQ5_spl <=> (inverse(g1,identity_for(g1))=a)),
% 0.14/5.49 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/5.49 fof(f170,plain,(
% 0.14/5.49 inverse(g1,identity_for(g1))=a|~sQ5_spl),
% 0.14/5.49 inference(component_clause,[status(thm)],[f169])).
% 0.14/5.49 fof(f172,definition,(
% 0.14/5.49 sQ6_spl <=> (inverse(g1,identity_for(g1))=b)),
% 0.14/5.49 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.14/5.49 fof(f173,plain,(
% 0.14/5.49 inverse(g1,identity_for(g1))=b|~sQ6_spl),
% 0.14/5.49 inference(component_clause,[status(thm)],[f172])).
% 0.14/5.49 fof(f175,plain,(
% 0.14/5.49 sQ5_spl|sQ6_spl),
% 0.14/5.49 inference(split_clause,[status(thm)],[f162,f169,f172])).
% 0.14/5.49 fof(f176,definition,(
% 0.14/5.49 sQ7_spl <=> (d3=a)),
% 0.14/5.49 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/5.49 fof(f177,plain,(
% 0.14/5.49 d3=a|~sQ7_spl),
% 0.14/5.49 inference(component_clause,[status(thm)],[f176])).
% 0.14/5.49 fof(f178,plain,(
% 0.14/5.49 ~d3=a|sQ7_spl),
% 0.14/5.49 inference(component_clause,[status(thm)],[f176])).
% 0.14/5.49 fof(f179,definition,(
% 0.14/5.49 sQ8_spl <=> (d3=b)),
% 0.14/5.49 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/5.50 fof(f180,plain,(
% 0.14/5.50 d3=b|~sQ8_spl),
% 0.14/5.50 inference(component_clause,[status(thm)],[f179])).
% 0.14/5.50 fof(f182,plain,(
% 0.14/5.50 sQ7_spl|sQ8_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f163,f176,f179])).
% 0.14/5.50 fof(f183,definition,(
% 0.14/5.50 sQ9_spl <=> (d2=a)),
% 0.14/5.50 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/5.50 fof(f184,plain,(
% 0.14/5.50 d2=a|~sQ9_spl),
% 0.14/5.50 inference(component_clause,[status(thm)],[f183])).
% 0.14/5.50 fof(f186,definition,(
% 0.14/5.50 sQ10_spl <=> (d2=b)),
% 0.14/5.50 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/5.50 fof(f187,plain,(
% 0.14/5.50 d2=b|~sQ10_spl),
% 0.14/5.50 inference(component_clause,[status(thm)],[f186])).
% 0.14/5.50 fof(f188,plain,(
% 0.14/5.50 ~d2=b|sQ10_spl),
% 0.14/5.50 inference(component_clause,[status(thm)],[f186])).
% 0.14/5.50 fof(f189,plain,(
% 0.14/5.50 sQ9_spl|sQ10_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f164,f183,f186])).
% 0.14/5.50 fof(f190,definition,(
% 0.14/5.50 sQ11_spl <=> (d1=a)),
% 0.14/5.50 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/5.50 fof(f191,plain,(
% 0.14/5.50 d1=a|~sQ11_spl),
% 0.14/5.50 inference(component_clause,[status(thm)],[f190])).
% 0.14/5.50 fof(f193,definition,(
% 0.14/5.50 sQ12_spl <=> (d1=b)),
% 0.14/5.50 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/5.50 fof(f194,plain,(
% 0.14/5.50 d1=b|~sQ12_spl),
% 0.14/5.50 inference(component_clause,[status(thm)],[f193])).
% 0.14/5.50 fof(f195,plain,(
% 0.14/5.50 ~d1=b|sQ12_spl),
% 0.14/5.50 inference(component_clause,[status(thm)],[f193])).
% 0.14/5.50 fof(f196,plain,(
% 0.14/5.50 sQ11_spl|sQ12_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f165,f190,f193])).
% 0.14/5.50 fof(f197,definition,(
% 0.14/5.50 sQ13_spl <=> (b=a)),
% 0.14/5.50 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/5.50 fof(f198,plain,(
% 0.14/5.50 b=a|~sQ13_spl),
% 0.14/5.50 inference(component_clause,[status(thm)],[f197])).
% 0.14/5.50 fof(f199,plain,(
% 0.14/5.50 ~b=a|sQ13_spl),
% 0.14/5.50 inference(component_clause,[status(thm)],[f197])).
% 0.14/5.50 fof(f200,definition,(
% 0.14/5.50 sQ14_spl <=> (b=b)),
% 0.14/5.50 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/5.50 fof(f203,plain,(
% 0.14/5.50 sQ13_spl|sQ14_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f166,f197,f200])).
% 0.14/5.50 fof(f204,definition,(
% 0.14/5.50 sQ15_spl <=> (a=a)),
% 0.14/5.50 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/5.50 fof(f207,plain,(
% 0.14/5.50 sQ15_spl|sQ13_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f167,f204,f197])).
% 0.14/5.50 fof(f208,definition,(
% 0.14/5.50 sQ16_spl <=> (identity_for(g1)=a)),
% 0.14/5.50 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.14/5.50 fof(f211,definition,(
% 0.14/5.50 sQ17_spl <=> (identity_for(g1)=b)),
% 0.14/5.50 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.14/5.50 fof(f214,plain,(
% 0.14/5.50 sQ16_spl|sQ17_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f168,f208,f211])).
% 0.14/5.50 fof(f217,plain,(
% 0.14/5.50 ![X0]: (~product(g1,a,a,X0)|X0=a)),
% 0.14/5.50 inference(resolution,[status(thm)],[f53,f42])).
% 0.14/5.50 fof(f220,plain,(
% 0.14/5.50 ~product(g2,an_isomorphism(a),an_isomorphism(d2),an_isomorphism(d3))|~sQ11_spl),
% 0.14/5.50 inference(backward_demodulation,[status(thm)],[f191,f67])).
% 0.14/5.50 fof(f221,plain,(
% 0.14/5.50 ~product(g2,c,an_isomorphism(d2),an_isomorphism(d3))|~sQ11_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f61,f220])).
% 0.14/5.50 fof(f222,plain,(
% 0.14/5.50 ~product(g2,c,an_isomorphism(a),an_isomorphism(d3))|~sQ9_spl|~sQ11_spl),
% 0.14/5.50 inference(backward_demodulation,[status(thm)],[f184,f221])).
% 0.14/5.50 fof(f224,plain,(
% 0.14/5.50 ~product(g2,c,c,an_isomorphism(d3))|~sQ9_spl|~sQ11_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f61,f222])).
% 0.14/5.50 fof(f228,plain,(
% 0.14/5.50 ~product(g2,c,c,an_isomorphism(a))|~sQ7_spl|~sQ9_spl|~sQ11_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f177,f224])).
% 0.14/5.50 fof(f229,plain,(
% 0.14/5.50 ~product(g2,c,c,c)|~sQ7_spl|~sQ9_spl|~sQ11_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f61,f228])).
% 0.14/5.50 fof(f235,plain,(
% 0.14/5.50 sQ0_spl|~sQ2_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f132,f82,f89])).
% 0.14/5.50 fof(f240,plain,(
% 0.14/5.50 d3=a|~sQ13_spl|~sQ8_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f198,f180])).
% 0.14/5.50 fof(f252,plain,(
% 0.14/5.50 ~a=a|~sQ13_spl|~sQ8_spl|sQ7_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f240,f178])).
% 0.14/5.50 fof(f253,plain,(
% 0.14/5.50 $false|~sQ13_spl|~sQ8_spl|sQ7_spl),
% 0.14/5.50 inference(trivial_equality_resolution,[status(thm)],[f252])).
% 0.14/5.50 fof(f254,plain,(
% 0.14/5.50 ~sQ13_spl|~sQ8_spl|sQ7_spl),
% 0.14/5.50 inference(contradiction_clause,[status(thm)],[f253])).
% 0.14/5.50 fof(f267,plain,(
% 0.14/5.50 product(g1,d1,d2,a)|~sQ7_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f177,f66])).
% 0.14/5.50 fof(f274,plain,(
% 0.14/5.50 ~product(g2,an_isomorphism(d1),an_isomorphism(d2),an_isomorphism(a))|~sQ7_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f177,f67])).
% 0.14/5.50 fof(f275,plain,(
% 0.14/5.50 ~product(g2,an_isomorphism(d1),an_isomorphism(d2),c)|~sQ7_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f61,f274])).
% 0.14/5.50 fof(f276,plain,(
% 0.14/5.50 ~product(g2,an_isomorphism(d1),an_isomorphism(b),c)|~sQ10_spl|~sQ7_spl),
% 0.14/5.50 inference(backward_demodulation,[status(thm)],[f187,f275])).
% 0.14/5.50 fof(f288,plain,(
% 0.14/5.50 ~product(g2,c,an_isomorphism(b),an_isomorphism(d3))|~sQ10_spl|~sQ11_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f187,f221])).
% 0.14/5.50 fof(f289,plain,(
% 0.14/5.50 ~product(g2,c,an_isomorphism(b),an_isomorphism(a))|~sQ7_spl|~sQ10_spl|~sQ11_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f177,f288])).
% 0.14/5.50 fof(f290,plain,(
% 0.14/5.50 ~product(g2,c,an_isomorphism(b),c)|~sQ7_spl|~sQ10_spl|~sQ11_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f61,f289])).
% 0.14/5.50 fof(f296,plain,(
% 0.14/5.50 ![X0]: (~product(g1,b,b,X0)|X0=a)),
% 0.14/5.50 inference(resolution,[status(thm)],[f56,f42])).
% 0.14/5.50 fof(f299,plain,(
% 0.14/5.50 ![X0]: (~product(g1,b,a,X0)|X0=b)),
% 0.14/5.50 inference(resolution,[status(thm)],[f55,f42])).
% 0.14/5.50 fof(f323,plain,(
% 0.14/5.50 ~product(g2,c,d,c)|~sQ7_spl|~sQ10_spl|~sQ11_spl),
% 0.14/5.50 inference(backward_demodulation,[status(thm)],[f62,f290])).
% 0.14/5.50 fof(f354,plain,(
% 0.14/5.50 inverse(g2,identity_for(g2))=c|inverse(g2,identity_for(g2))=d),
% 0.14/5.50 inference(resolution,[status(thm)],[f52,f76])).
% 0.14/5.50 fof(f358,definition,(
% 0.14/5.50 sQ18_spl <=> (inverse(g2,identity_for(g2))=c)),
% 0.14/5.50 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.14/5.50 fof(f359,plain,(
% 0.14/5.50 inverse(g2,identity_for(g2))=c|~sQ18_spl),
% 0.14/5.50 inference(component_clause,[status(thm)],[f358])).
% 0.14/5.50 fof(f361,definition,(
% 0.14/5.50 sQ19_spl <=> (inverse(g2,identity_for(g2))=d)),
% 0.14/5.50 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/5.50 fof(f362,plain,(
% 0.14/5.50 inverse(g2,identity_for(g2))=d|~sQ19_spl),
% 0.14/5.50 inference(component_clause,[status(thm)],[f361])).
% 0.14/5.50 fof(f364,plain,(
% 0.14/5.50 sQ18_spl|sQ19_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f354,f358,f361])).
% 0.14/5.50 fof(f408,plain,(
% 0.14/5.50 ![X0]: (identity_for(X0)=inverse(X0,identity_for(X0)))),
% 0.14/5.50 inference(resolution,[status(thm)],[f70,f38])).
% 0.14/5.50 fof(f457,plain,(
% 0.14/5.50 inverse(g1,b)=a|inverse(g1,b)=b),
% 0.14/5.50 inference(resolution,[status(thm)],[f74,f51])).
% 0.14/5.50 fof(f461,definition,(
% 0.14/5.50 sQ20_spl <=> (inverse(g1,b)=a)),
% 0.14/5.50 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/5.50 fof(f462,plain,(
% 0.14/5.50 inverse(g1,b)=a|~sQ20_spl),
% 0.14/5.50 inference(component_clause,[status(thm)],[f461])).
% 0.14/5.50 fof(f464,definition,(
% 0.14/5.50 sQ21_spl <=> (inverse(g1,b)=b)),
% 0.14/5.50 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/5.50 fof(f467,plain,(
% 0.14/5.50 sQ20_spl|sQ21_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f457,f461,f464])).
% 0.14/5.50 fof(f488,plain,(
% 0.14/5.50 c=d|~sQ0_spl|~sQ1_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f83,f86])).
% 0.14/5.50 fof(f492,plain,(
% 0.14/5.50 ~product(g2,c,c,c)|~sQ0_spl|~sQ1_spl|~sQ7_spl|~sQ10_spl|~sQ11_spl),
% 0.14/5.50 inference(backward_demodulation,[status(thm)],[f488,f323])).
% 0.14/5.50 fof(f496,plain,(
% 0.14/5.50 $false|~sQ0_spl|~sQ1_spl|~sQ7_spl|~sQ10_spl|~sQ11_spl),
% 0.14/5.50 inference(forward_subsumption_resolution,[status(thm)],[f492,f128])).
% 0.14/5.50 fof(f497,plain,(
% 0.14/5.50 ~sQ0_spl|~sQ1_spl|~sQ7_spl|~sQ10_spl|~sQ11_spl),
% 0.14/5.50 inference(contradiction_clause,[status(thm)],[f496])).
% 0.14/5.50 fof(f506,plain,(
% 0.14/5.50 product(g1,d1,a,a)|~sQ9_spl|~sQ7_spl),
% 0.14/5.50 inference(backward_demodulation,[status(thm)],[f184,f267])).
% 0.14/5.50 fof(f507,plain,(
% 0.14/5.50 ~product(g2,an_isomorphism(d1),an_isomorphism(a),c)|~sQ9_spl|~sQ7_spl),
% 0.14/5.50 inference(backward_demodulation,[status(thm)],[f184,f275])).
% 0.14/5.50 fof(f508,plain,(
% 0.14/5.50 ~product(g2,an_isomorphism(d1),c,c)|~sQ9_spl|~sQ7_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f61,f507])).
% 0.14/5.50 fof(f520,plain,(
% 0.14/5.50 ~product(g2,an_isomorphism(b),c,c)|~sQ12_spl|~sQ9_spl|~sQ7_spl),
% 0.14/5.50 inference(backward_demodulation,[status(thm)],[f194,f508])).
% 0.14/5.50 fof(f544,plain,(
% 0.14/5.50 product(g1,b,a,a)|~sQ12_spl|~sQ9_spl|~sQ7_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f194,f506])).
% 0.14/5.50 fof(f552,plain,(
% 0.14/5.50 ~product(g2,d,c,c)|~sQ12_spl|~sQ9_spl|~sQ7_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f62,f520])).
% 0.14/5.50 fof(f575,plain,(
% 0.14/5.50 identity_for(g1)=a|~sQ5_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f408,f170])).
% 0.14/5.50 fof(f766,plain,(
% 0.14/5.50 sQ16_spl|~sQ5_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f575,f208,f169])).
% 0.14/5.50 fof(f771,plain,(
% 0.14/5.50 identity_for(g1)=b|~sQ6_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f408,f173])).
% 0.14/5.50 fof(f776,plain,(
% 0.14/5.50 ~product(g2,an_isomorphism(b),an_isomorphism(b),c)|~sQ12_spl|~sQ10_spl|~sQ7_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f194,f276])).
% 0.14/5.50 fof(f777,plain,(
% 0.14/5.50 ~product(g2,d,an_isomorphism(b),c)|~sQ12_spl|~sQ10_spl|~sQ7_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f62,f776])).
% 0.14/5.50 fof(f778,plain,(
% 0.14/5.50 ~product(g2,d,d,c)|~sQ12_spl|~sQ10_spl|~sQ7_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f62,f777])).
% 0.14/5.50 fof(f779,plain,(
% 0.14/5.50 $false|~sQ12_spl|~sQ10_spl|~sQ7_spl),
% 0.14/5.50 inference(forward_subsumption_resolution,[status(thm)],[f778,f60])).
% 0.14/5.50 fof(f780,plain,(
% 0.14/5.50 ~sQ12_spl|~sQ10_spl|~sQ7_spl),
% 0.14/5.50 inference(contradiction_clause,[status(thm)],[f779])).
% 0.14/5.50 fof(f800,plain,(
% 0.14/5.50 ~a=b|~sQ11_spl|sQ12_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f191,f195])).
% 0.14/5.50 fof(f832,plain,(
% 0.14/5.50 identity_for(g1)=inverse(g1,b)|~sQ6_spl),
% 0.14/5.50 inference(paramodulation,[status(thm)],[f771,f408])).
% 0.14/5.50 fof(f839,plain,(
% 0.14/5.50 b=inverse(g1,b)|~sQ6_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f771,f832])).
% 0.14/5.50 fof(f840,plain,(
% 0.14/5.50 b=a|~sQ20_spl|~sQ6_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f462,f839])).
% 0.14/5.50 fof(f841,plain,(
% 0.14/5.50 $false|sQ13_spl|~sQ20_spl|~sQ6_spl),
% 0.14/5.50 inference(forward_subsumption_resolution,[status(thm)],[f840,f199])).
% 0.14/5.50 fof(f842,plain,(
% 0.14/5.50 sQ13_spl|~sQ20_spl|~sQ6_spl),
% 0.14/5.50 inference(contradiction_clause,[status(thm)],[f841])).
% 0.14/5.50 fof(f849,plain,(
% 0.14/5.50 ![X0]: (~product(g1,a,d2,X0)|X0=d3|~sQ11_spl)),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f191,f141])).
% 0.14/5.50 fof(f850,plain,(
% 0.14/5.50 ![X0]: (~product(g1,a,b,X0)|X0=d3|~sQ10_spl|~sQ11_spl)),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f187,f849])).
% 0.14/5.50 fof(f851,plain,(
% 0.14/5.50 ![X0]: (~product(g1,a,b,X0)|X0=a|~sQ7_spl|~sQ10_spl|~sQ11_spl)),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f177,f850])).
% 0.14/5.50 fof(f852,plain,(
% 0.14/5.50 b=a|~sQ7_spl|~sQ10_spl|~sQ11_spl),
% 0.14/5.50 inference(resolution,[status(thm)],[f851,f54])).
% 0.14/5.50 fof(f854,plain,(
% 0.14/5.50 sQ13_spl|~sQ7_spl|~sQ10_spl|~sQ11_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f852,f197,f176,f186,f190])).
% 0.14/5.50 fof(f856,plain,(
% 0.14/5.50 ~product(g2,c,an_isomorphism(b),an_isomorphism(d3))|~sQ10_spl|~sQ11_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f187,f221])).
% 0.14/5.50 fof(f857,plain,(
% 0.14/5.50 ~product(g2,c,d,an_isomorphism(d3))|~sQ10_spl|~sQ11_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f62,f856])).
% 0.14/5.50 fof(f867,plain,(
% 0.14/5.50 product(g1,a,d2,d3)|~sQ11_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f191,f66])).
% 0.14/5.50 fof(f871,plain,(
% 0.14/5.50 ~product(g2,c,d,an_isomorphism(b))|~sQ8_spl|~sQ10_spl|~sQ11_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f180,f857])).
% 0.14/5.50 fof(f872,plain,(
% 0.14/5.50 ~product(g2,c,d,d)|~sQ8_spl|~sQ10_spl|~sQ11_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f62,f871])).
% 0.14/5.50 fof(f875,plain,(
% 0.14/5.50 product(g1,a,d2,b)|~sQ8_spl|~sQ11_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f180,f867])).
% 0.14/5.50 fof(f893,plain,(
% 0.14/5.50 ~a=b|~sQ9_spl|sQ10_spl),
% 0.14/5.50 inference(backward_demodulation,[status(thm)],[f184,f188])).
% 0.14/5.50 fof(f906,plain,(
% 0.14/5.50 product(g1,a,a,b)|~sQ9_spl|~sQ8_spl|~sQ11_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f184,f875])).
% 0.14/5.50 fof(f1017,plain,(
% 0.14/5.50 b=a|~sQ9_spl|~sQ8_spl|~sQ11_spl),
% 0.14/5.50 inference(resolution,[status(thm)],[f217,f906])).
% 0.14/5.50 fof(f1020,plain,(
% 0.14/5.50 sQ13_spl|~sQ9_spl|~sQ8_spl|~sQ11_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f1017,f197,f183,f179,f190])).
% 0.14/5.50 fof(f1051,plain,(
% 0.14/5.50 ~product(g2,an_isomorphism(b),an_isomorphism(d2),an_isomorphism(d3))|~sQ12_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f194,f67])).
% 0.14/5.50 fof(f1052,plain,(
% 0.14/5.50 ~product(g2,d,an_isomorphism(d2),an_isomorphism(d3))|~sQ12_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f62,f1051])).
% 0.14/5.50 fof(f1053,plain,(
% 0.14/5.50 ~product(g2,d,an_isomorphism(d2),an_isomorphism(b))|~sQ8_spl|~sQ12_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f180,f1052])).
% 0.14/5.50 fof(f1054,plain,(
% 0.14/5.50 ~product(g2,d,an_isomorphism(d2),d)|~sQ8_spl|~sQ12_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f62,f1053])).
% 0.14/5.50 fof(f1055,plain,(
% 0.14/5.50 product(g1,b,d2,d3)|~sQ12_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f194,f66])).
% 0.14/5.50 fof(f1056,plain,(
% 0.14/5.50 product(g1,b,d2,b)|~sQ8_spl|~sQ12_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f180,f1055])).
% 0.14/5.50 fof(f1064,plain,(
% 0.14/5.50 product(g1,b,b,b)|~sQ10_spl|~sQ8_spl|~sQ12_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f187,f1056])).
% 0.14/5.50 fof(f1124,plain,(
% 0.14/5.50 b=a|~sQ10_spl|~sQ8_spl|~sQ12_spl),
% 0.14/5.50 inference(resolution,[status(thm)],[f296,f1064])).
% 0.14/5.50 fof(f1126,plain,(
% 0.14/5.50 sQ13_spl|~sQ10_spl|~sQ8_spl|~sQ12_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f1124,f197,f186,f179,f193])).
% 0.14/5.50 fof(f1133,plain,(
% 0.14/5.50 ~sQ13_spl|~sQ9_spl|sQ10_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f893,f197,f183,f186])).
% 0.14/5.50 fof(f1135,plain,(
% 0.14/5.50 ~sQ13_spl|~sQ11_spl|sQ12_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f800,f197,f190,f193])).
% 0.14/5.50 fof(f1138,plain,(
% 0.14/5.50 identity_for(g2)=c|~sQ18_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f408,f359])).
% 0.14/5.50 fof(f1211,plain,(
% 0.14/5.50 c=d|~sQ18_spl|~sQ1_spl),
% 0.14/5.50 inference(backward_demodulation,[status(thm)],[f1138,f86])).
% 0.14/5.50 fof(f1222,plain,(
% 0.14/5.50 sQ2_spl|~sQ18_spl|~sQ1_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f1211,f89,f358,f85])).
% 0.14/5.50 fof(f1224,plain,(
% 0.14/5.50 identity_for(g2)=d|~sQ19_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f408,f362])).
% 0.14/5.50 fof(f1302,plain,(
% 0.14/5.50 $false|~sQ7_spl|~sQ9_spl|~sQ11_spl),
% 0.14/5.50 inference(forward_subsumption_resolution,[status(thm)],[f57,f229])).
% 0.14/5.50 fof(f1303,plain,(
% 0.14/5.50 ~sQ7_spl|~sQ9_spl|~sQ11_spl),
% 0.14/5.50 inference(contradiction_clause,[status(thm)],[f1302])).
% 0.14/5.50 fof(f1311,plain,(
% 0.14/5.50 ~product(g2,d,an_isomorphism(a),d)|~sQ9_spl|~sQ8_spl|~sQ12_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f184,f1054])).
% 0.14/5.50 fof(f1312,plain,(
% 0.14/5.50 ~product(g2,d,c,d)|~sQ9_spl|~sQ8_spl|~sQ12_spl),
% 0.14/5.50 inference(forward_demodulation,[status(thm)],[f61,f1311])).
% 0.14/5.50 fof(f1313,plain,(
% 0.14/5.50 $false|~sQ9_spl|~sQ8_spl|~sQ12_spl),
% 0.14/5.50 inference(forward_subsumption_resolution,[status(thm)],[f1312,f59])).
% 0.14/5.50 fof(f1314,plain,(
% 0.14/5.50 ~sQ9_spl|~sQ8_spl|~sQ12_spl),
% 0.14/5.50 inference(contradiction_clause,[status(thm)],[f1313])).
% 0.14/5.50 fof(f1315,plain,(
% 0.14/5.50 $false|~sQ8_spl|~sQ10_spl|~sQ11_spl),
% 0.14/5.50 inference(forward_subsumption_resolution,[status(thm)],[f872,f58])).
% 0.14/5.50 fof(f1316,plain,(
% 0.14/5.50 ~sQ8_spl|~sQ10_spl|~sQ11_spl),
% 0.14/5.50 inference(contradiction_clause,[status(thm)],[f1315])).
% 0.14/5.50 fof(f1421,plain,(
% 0.14/5.50 ~product(g2,c,c,c)|~sQ2_spl|~sQ12_spl|~sQ9_spl|~sQ7_spl),
% 0.14/5.50 inference(backward_demodulation,[status(thm)],[f90,f552])).
% 0.14/5.50 fof(f1429,plain,(
% 0.14/5.50 $false|~sQ2_spl|~sQ12_spl|~sQ9_spl|~sQ7_spl),
% 0.14/5.50 inference(forward_subsumption_resolution,[status(thm)],[f1421,f57])).
% 0.14/5.50 fof(f1430,plain,(
% 0.14/5.50 ~sQ2_spl|~sQ12_spl|~sQ9_spl|~sQ7_spl),
% 0.14/5.50 inference(contradiction_clause,[status(thm)],[f1429])).
% 0.14/5.50 fof(f1431,plain,(
% 0.14/5.50 sQ1_spl|~sQ19_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f1224,f85,f361])).
% 0.14/5.50 fof(f1512,plain,(
% 0.14/5.50 sQ2_spl|~sQ0_spl|~sQ1_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f488,f89,f82,f85])).
% 0.14/5.50 fof(f1540,plain,(
% 0.14/5.50 a=b|~sQ12_spl|~sQ9_spl|~sQ7_spl),
% 0.14/5.50 inference(resolution,[status(thm)],[f299,f544])).
% 0.14/5.50 fof(f1541,plain,(
% 0.14/5.50 sQ13_spl|~sQ12_spl|~sQ9_spl|~sQ7_spl),
% 0.14/5.50 inference(split_clause,[status(thm)],[f1540,f197,f193,f183,f176])).
% 0.14/5.50 fof(f1542,plain,(
% 0.14/5.50 $false),
% 0.14/5.50 inference(sat_refutation,[status(thm)],[f88,f95,f99,f175,f182,f189,f196,f203,f207,f214,f235,f254,f364,f467,f497,f766,f780,f842,f854,f1020,f1126,f1133,f1135,f1222,f1303,f1314,f1316,f1430,f1431,f1512,f1541])).
% 0.14/5.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.51 % Elapsed time: 0.130991 seconds
% 0.14/5.51 % CPU time: 0.796570 seconds
% 0.14/5.51 % Total memory used: 115.097 MB
% 0.14/5.51 % Net memory used: 113.863 MB
%------------------------------------------------------------------------------