%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP385-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 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 : Fri Sep 25 01:33:37 PM UTC 2026
% Result : Unsatisfiable 18.88s 3.29s
% Output : CNFRefutation 18.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 40
% Syntax : Number of formulae : 421 ( 131 unt; 11 def)
% Number of atoms : 1724 ( 829 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 755 ( 287 ~; 468 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 16 ( 14 usr; 15 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 134 ( 0 sgn 134 !; 0 ?; 99 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
inverse(sk_c10) = sk_c9,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,negated_conjecture,
( multiply(sk_c10,sk_c4) = sk_c9
| multiply(sk_c9,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f7,plain,
( sk_c9 = multiply(sk_c10,sk_c4)
| sk_c10 = multiply(sk_c9,sk_c8) ),
inference(reorient_equations,[],[f6]) ).
fof(f8,negated_conjecture,
( multiply(sk_c3,sk_c10) = sk_c4
| multiply(sk_c9,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f9,plain,
( sk_c4 = multiply(sk_c3,sk_c10)
| sk_c10 = multiply(sk_c9,sk_c8) ),
inference(reorient_equations,[],[f8]) ).
fof(f10,negated_conjecture,
( inverse(sk_c3) = sk_c10
| multiply(sk_c9,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c10 = inverse(sk_c3)
| sk_c10 = multiply(sk_c9,sk_c8) ),
inference(reorient_equations,[],[f10]) ).
fof(f18,negated_conjecture,
( inverse(sk_c7) = sk_c10
| multiply(sk_c9,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_8) ).
fof(f19,plain,
( sk_c10 = inverse(sk_c7)
| sk_c10 = multiply(sk_c9,sk_c8) ),
inference(reorient_equations,[],[f18]) ).
fof(f20,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c10
| multiply(sk_c9,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_9) ).
fof(f21,plain,
( sk_c10 = multiply(sk_c7,sk_c8)
| sk_c10 = multiply(sk_c9,sk_c8) ),
inference(reorient_equations,[],[f20]) ).
fof(f22,negated_conjecture,
( multiply(sk_c10,sk_c4) = sk_c9
| multiply(sk_c10,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_10) ).
fof(f23,plain,
( sk_c9 = multiply(sk_c10,sk_c4)
| sk_c9 = multiply(sk_c10,sk_c8) ),
inference(reorient_equations,[],[f22]) ).
fof(f24,negated_conjecture,
( multiply(sk_c3,sk_c10) = sk_c4
| multiply(sk_c10,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f25,plain,
( sk_c4 = multiply(sk_c3,sk_c10)
| sk_c9 = multiply(sk_c10,sk_c8) ),
inference(reorient_equations,[],[f24]) ).
fof(f26,negated_conjecture,
( inverse(sk_c3) = sk_c10
| multiply(sk_c10,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f27,plain,
( sk_c10 = inverse(sk_c3)
| sk_c9 = multiply(sk_c10,sk_c8) ),
inference(reorient_equations,[],[f26]) ).
fof(f36,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c10
| multiply(sk_c10,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_17) ).
fof(f37,plain,
( sk_c10 = multiply(sk_c7,sk_c8)
| sk_c9 = multiply(sk_c10,sk_c8) ),
inference(reorient_equations,[],[f36]) ).
fof(f38,negated_conjecture,
( multiply(sk_c10,sk_c4) = sk_c9
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_18) ).
fof(f39,plain,
( sk_c9 = multiply(sk_c10,sk_c4)
| sk_c9 = multiply(sk_c10,sk_c2) ),
inference(reorient_equations,[],[f38]) ).
fof(f40,negated_conjecture,
( multiply(sk_c3,sk_c10) = sk_c4
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_19) ).
fof(f41,plain,
( sk_c4 = multiply(sk_c3,sk_c10)
| sk_c9 = multiply(sk_c10,sk_c2) ),
inference(reorient_equations,[],[f40]) ).
fof(f42,negated_conjecture,
( inverse(sk_c3) = sk_c10
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_20) ).
fof(f43,plain,
( sk_c10 = inverse(sk_c3)
| sk_c9 = multiply(sk_c10,sk_c2) ),
inference(reorient_equations,[],[f42]) ).
fof(f52,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c10
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f53,plain,
( sk_c10 = multiply(sk_c7,sk_c8)
| sk_c9 = multiply(sk_c10,sk_c2) ),
inference(reorient_equations,[],[f52]) ).
fof(f54,negated_conjecture,
( multiply(sk_c10,sk_c4) = sk_c9
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f55,plain,
( sk_c9 = multiply(sk_c10,sk_c4)
| sk_c2 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f54]) ).
fof(f56,negated_conjecture,
( multiply(sk_c3,sk_c10) = sk_c4
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_27) ).
fof(f57,plain,
( sk_c4 = multiply(sk_c3,sk_c10)
| sk_c2 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f56]) ).
fof(f58,negated_conjecture,
( inverse(sk_c3) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_28) ).
fof(f59,plain,
( sk_c10 = inverse(sk_c3)
| sk_c2 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f58]) ).
fof(f68,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_33) ).
fof(f69,plain,
( sk_c10 = multiply(sk_c7,sk_c8)
| sk_c2 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f68]) ).
fof(f70,negated_conjecture,
( multiply(sk_c10,sk_c4) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f71,plain,
( sk_c9 = multiply(sk_c10,sk_c4)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f70]) ).
fof(f72,negated_conjecture,
( multiply(sk_c3,sk_c10) = sk_c4
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_35) ).
fof(f73,plain,
( sk_c4 = multiply(sk_c3,sk_c10)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f72]) ).
fof(f74,negated_conjecture,
( inverse(sk_c3) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f75,plain,
( sk_c10 = inverse(sk_c3)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f74]) ).
fof(f82,negated_conjecture,
( inverse(sk_c7) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_40) ).
fof(f83,plain,
( sk_c10 = inverse(sk_c7)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f82]) ).
fof(f84,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_41) ).
fof(f85,plain,
( sk_c10 = multiply(sk_c7,sk_c8)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f84]) ).
fof(f86,negated_conjecture,
! [X2,X3,X0,X1,X6,X4,X5] :
( multiply(X6,sk_c8) != sk_c10
| inverse(X6) != sk_c10
| multiply(X5,sk_c9) != sk_c8
| inverse(X4) != X5
| multiply(X4,X5) != sk_c8
| inverse(X3) != sk_c10
| multiply(X3,sk_c10) != X2
| multiply(sk_c10,X2) != sk_c9
| inverse(X1) != sk_c10
| multiply(X1,sk_c10) != X0
| multiply(sk_c10,X0) != sk_c9
| multiply(sk_c10,sk_c8) != sk_c9
| multiply(sk_c9,sk_c8) != sk_c10
| inverse(sk_c10) != sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f87,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( sk_c10 != multiply(X6,sk_c8)
| sk_c10 != inverse(X6)
| sk_c8 != multiply(X5,sk_c9)
| inverse(X4) != X5
| sk_c8 != multiply(X4,X5)
| sk_c10 != inverse(X3)
| multiply(X3,sk_c10) != X2
| sk_c9 != multiply(sk_c10,X2)
| sk_c10 != inverse(X1)
| multiply(X1,sk_c10) != X0
| sk_c9 != multiply(sk_c10,X0)
| sk_c9 != multiply(sk_c10,sk_c8)
| sk_c10 != multiply(sk_c9,sk_c8)
| inverse(sk_c10) != sk_c9 ),
inference(reorient_equations,[],[f86]) ).
fof(f88,plain,
! [X2,X3,X1,X6,X4,X5] :
( sk_c10 != multiply(X6,sk_c8)
| sk_c10 != inverse(X6)
| sk_c8 != multiply(X5,sk_c9)
| inverse(X4) != X5
| sk_c8 != multiply(X4,X5)
| sk_c10 != inverse(X3)
| multiply(X3,sk_c10) != X2
| sk_c9 != multiply(sk_c10,X2)
| sk_c10 != inverse(X1)
| sk_c9 != multiply(sk_c10,multiply(X1,sk_c10))
| sk_c9 != multiply(sk_c10,sk_c8)
| sk_c10 != multiply(sk_c9,sk_c8)
| inverse(sk_c10) != sk_c9 ),
inference(equality_resolution,[],[f87]) ).
fof(f89,plain,
! [X3,X1,X6,X4,X5] :
( sk_c10 != multiply(X6,sk_c8)
| sk_c10 != inverse(X6)
| sk_c8 != multiply(X5,sk_c9)
| inverse(X4) != X5
| sk_c8 != multiply(X4,X5)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(sk_c10,multiply(X3,sk_c10))
| sk_c10 != inverse(X1)
| sk_c9 != multiply(sk_c10,multiply(X1,sk_c10))
| sk_c9 != multiply(sk_c10,sk_c8)
| sk_c10 != multiply(sk_c9,sk_c8)
| inverse(sk_c10) != sk_c9 ),
inference(equality_resolution,[],[f88]) ).
fof(f90,plain,
! [X3,X1,X6,X4] :
( sk_c10 != multiply(X6,sk_c8)
| sk_c10 != inverse(X6)
| sk_c8 != multiply(inverse(X4),sk_c9)
| sk_c8 != multiply(X4,inverse(X4))
| sk_c10 != inverse(X3)
| sk_c9 != multiply(sk_c10,multiply(X3,sk_c10))
| sk_c10 != inverse(X1)
| sk_c9 != multiply(sk_c10,multiply(X1,sk_c10))
| sk_c9 != multiply(sk_c10,sk_c8)
| sk_c10 != multiply(sk_c9,sk_c8)
| inverse(sk_c10) != sk_c9 ),
inference(equality_resolution,[],[f89]) ).
tcf(c_94,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_95,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_97,negated_conjecture,
inverse(sk_c10) = sk_c9,
inference(cnf_transformation,[],[f5]) ).
tcf(c_98,negated_conjecture,
( ( multiply(sk_c9,sk_c8) = sk_c10 )
| ( multiply(sk_c10,sk_c4) = sk_c9 ) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_99,negated_conjecture,
( ( multiply(sk_c3,sk_c10) = sk_c4 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_100,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_104,negated_conjecture,
( ( inverse(sk_c7) = sk_c10 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_105,negated_conjecture,
( ( multiply(sk_c7,sk_c8) = sk_c10 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_106,negated_conjecture,
( ( multiply(sk_c10,sk_c4) = sk_c9 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_107,negated_conjecture,
( ( multiply(sk_c3,sk_c10) = sk_c4 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_108,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_113,negated_conjecture,
( ( multiply(sk_c7,sk_c8) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_114,negated_conjecture,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ( multiply(sk_c10,sk_c4) = sk_c9 ) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_115,negated_conjecture,
( ( multiply(sk_c3,sk_c10) = sk_c4 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_116,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_121,negated_conjecture,
( ( multiply(sk_c7,sk_c8) = sk_c10 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_122,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( multiply(sk_c10,sk_c4) = sk_c9 ) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_123,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( multiply(sk_c3,sk_c10) = sk_c4 ) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_124,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c2 ) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_129,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( multiply(sk_c7,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_130,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c10,sk_c4) = sk_c9 ) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c3,sk_c10) = sk_c4 ) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_132,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_136,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c7) = sk_c10 ) ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c7,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_138,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( inverse(sk_c10) != sk_c9 )
| ( inverse(X2) != sk_c10 )
| ( inverse(X1) != sk_c10 )
| ( inverse(X0) != sk_c10 )
| ( multiply(sk_c9,sk_c8) != sk_c10 )
| ( multiply(sk_c10,sk_c8) != sk_c9 )
| ( multiply(X0,sk_c8) != sk_c10 )
| ( multiply(inverse(X3),sk_c9) != sk_c8 )
| ( multiply(X3,inverse(X3)) != sk_c8 )
| ( multiply(sk_c10,multiply(X2,sk_c10)) != sk_c9 )
| ( multiply(sk_c10,multiply(X1,sk_c10)) != sk_c9 ) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_143,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(sk_c10,multiply(X1,sk_c10)) != sk_c9 )
| ( multiply(sk_c10,multiply(X2,sk_c10)) != sk_c9 )
| ( multiply(X3,inverse(X3)) != sk_c8 )
| ( multiply(inverse(X3),sk_c9) != sk_c8 )
| ( multiply(X0,sk_c8) != sk_c10 )
| ( multiply(sk_c10,sk_c8) != sk_c9 )
| ( multiply(sk_c9,sk_c8) != sk_c10 )
| ( inverse(X0) != sk_c10 )
| ( inverse(X1) != sk_c10 )
| ( inverse(X2) != sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_138,c_97,c_138]) ).
tcf(c_144,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( inverse(X3) != sk_c10 )
| ( inverse(X1) != sk_c10 )
| ( inverse(X0) != sk_c10 )
| ( multiply(sk_c9,sk_c8) != sk_c10 )
| ( multiply(sk_c10,sk_c8) != sk_c9 )
| ( multiply(X3,sk_c8) != sk_c10 )
| ( multiply(inverse(X2),sk_c9) != sk_c8 )
| ( multiply(X2,inverse(X2)) != sk_c8 )
| ( multiply(sk_c10,multiply(X1,sk_c10)) != sk_c9 )
| ( multiply(sk_c10,multiply(X0,sk_c10)) != sk_c9 ) ),
inference(renaming,[status(thm)],[c_143]) ).
tcf(c_516,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( multiply(inverse(X0),sk_c9) != sk_c8 )
| ( multiply(X0,inverse(X0)) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_144]) ).
tcf(c_517,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(sk_c10,multiply(X0,sk_c10)) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_144]) ).
tcf(c_518,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c8) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_144]) ).
tcf(c_519,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c9,sk_c8) != sk_c10 )
| ( multiply(sk_c10,sk_c8) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_144]) ).
tcf(c_520,definition,
iPr_def_13 = multiply(sk_c10,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_521,definition,
iPr_def_14 = multiply(sk_c9,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_522,definition,
iPr_def_15 = multiply(sk_c7,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_523,definition,
iPr_def_16 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_524,definition,
iPr_def_17 = inverse(sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_528,definition,
iPr_def_21 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_529,definition,
iPr_def_22 = multiply(sk_c3,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_530,definition,
iPr_def_23 = multiply(sk_c10,sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_531,definition,
iPr_def_24 = multiply(sk_c1,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_532,definition,
iPr_def_25 = multiply(sk_c10,sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_533,definition,
iPr_def_26 = inverse(sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_534,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_14 != sk_c10 )
| ( iPr_def_13 != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_519,c_521,c_520]) ).
tcf(c_536,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c8) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_518]) ).
tcf(c_537,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(sk_c10,multiply(X0,sk_c10)) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_517]) ).
tcf(c_538,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( multiply(inverse(X0),sk_c9) != sk_c8 )
| ( multiply(X0,inverse(X0)) != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_516]) ).
tcf(c_539,negated_conjecture,
( ( iPr_def_16 = sk_c10 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_137,c_523,c_522]) ).
tcf(c_540,negated_conjecture,
( ( iPr_def_17 = sk_c10 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_136,c_524]) ).
tcf(c_544,negated_conjecture,
( ( iPr_def_21 = sk_c10 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_132,c_528]) ).
tcf(c_545,negated_conjecture,
( ( iPr_def_22 = sk_c4 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_131,c_529]) ).
tcf(c_546,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_130,c_530]) ).
tcf(c_547,negated_conjecture,
( ( iPr_def_24 = sk_c2 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_129,c_531]) ).
tcf(c_552,negated_conjecture,
( ( iPr_def_24 = sk_c2 )
| ( iPr_def_21 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_124]) ).
tcf(c_553,negated_conjecture,
( ( iPr_def_24 = sk_c2 )
| ( iPr_def_22 = sk_c4 ) ),
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_554,negated_conjecture,
( ( iPr_def_24 = sk_c2 )
| ( iPr_def_23 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_122]) ).
tcf(c_555,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_121,c_532]) ).
tcf(c_560,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_21 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_116]) ).
tcf(c_561,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_22 = sk_c4 ) ),
inference(demodulation,[status(thm)],[c_115]) ).
tcf(c_562,negated_conjecture,
( ( iPr_def_25 = sk_c9 )
| ( iPr_def_23 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_114]) ).
tcf(c_563,negated_conjecture,
( ( iPr_def_15 = sk_c10 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_113]) ).
tcf(c_568,negated_conjecture,
( ( iPr_def_21 = sk_c10 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_108]) ).
tcf(c_569,negated_conjecture,
( ( iPr_def_22 = sk_c4 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_107]) ).
tcf(c_570,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_571,negated_conjecture,
( ( iPr_def_15 = sk_c10 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_105]) ).
tcf(c_572,negated_conjecture,
( ( iPr_def_17 = sk_c10 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_104]) ).
tcf(c_576,negated_conjecture,
( ( iPr_def_21 = sk_c10 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_100]) ).
tcf(c_577,negated_conjecture,
( ( iPr_def_22 = sk_c4 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_99]) ).
tcf(c_578,negated_conjecture,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_98]) ).
tcf(c_579,negated_conjecture,
iPr_def_26 = sk_c9,
inference(demodulation,[status(thm)],[c_97,c_533]) ).
tcf(c_580,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_581,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_900,plain,
multiply(iPr_def_26,sk_c8) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_521,c_579]) ).
tcf(c_913,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c10 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_546,c_579]) ).
tcf(c_923,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( multiply(iPr_def_16,sk_c8) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_913,c_520]) ).
tcf(c_990,plain,
( ( sk_c10 = iPr_def_16 )
| ( multiply(iPr_def_21,sk_c4) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_544,c_530]) ).
tcf(c_1019,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( multiply(iPr_def_16,sk_c2) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_913,c_532]) ).
tcf(c_1022,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_16,sk_c2) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_539,c_532]) ).
tcf(c_1046,plain,
multiply(iPr_def_26,sk_c10) = identity,
inference(superposition,[status(thm)],[c_533,c_95]) ).
tcf(c_1047,plain,
multiply(iPr_def_21,sk_c3) = identity,
inference(superposition,[status(thm)],[c_528,c_95]) ).
tcf(c_1049,plain,
multiply(iPr_def_17,sk_c7) = identity,
inference(superposition,[status(thm)],[c_524,c_95]) ).
tcf(c_1050,plain,
multiply(iPr_def_16,sk_c1) = identity,
inference(superposition,[status(thm)],[c_523,c_95]) ).
tcf(c_1066,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1067,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c2 = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_554,c_579]) ).
tcf(c_1077,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1066]) ).
tcf(c_1078,plain,
sk_c9 = sk_c9,
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_1081,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_555,c_579]) ).
tcf(c_1095,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( multiply(iPr_def_15,sk_c4) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1081,c_530]) ).
tcf(c_1099,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( multiply(iPr_def_15,sk_c8) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_1081,c_520]) ).
tcf(c_1134,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1137,plain,
( ( sk_c9 = iPr_def_26 )
| ( iPr_def_26 != sk_c9 )
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1077]) ).
tcf(c_1187,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1066]) ).
tcf(c_1267,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_26 )
| ( iPr_def_26 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1270,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( sk_c10 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_560,c_579]) ).
tcf(c_1287,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( multiply(iPr_def_21,sk_c4) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1270,c_530]) ).
tcf(c_1346,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( sk_c4 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_561,c_579]) ).
tcf(c_1356,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( iPr_def_23 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_562,c_579]) ).
tcf(c_1365,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( multiply(iPr_def_25,sk_c8) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1356,c_900]) ).
tcf(c_1374,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_563,c_579]) ).
tcf(c_1428,plain,
! [X0: $i] :
( ( iPr_def_13 = iPr_def_23 )
| ( iPr_def_23 != X0 )
| ( iPr_def_13 != X0 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1435,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_23 )
| ( iPr_def_23 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1441,plain,
iPr_def_23 = iPr_def_23,
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_1500,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_26 = X0 )
| ( iPr_def_26 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1503,plain,
! [X0: $i] :
( ( X0 = iPr_def_26 )
| ( iPr_def_26 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1267]) ).
tcf(c_1582,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( sk_c10 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_568,c_579]) ).
tcf(c_1603,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( multiply(iPr_def_21,sk_c4) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1582,c_530]) ).
tcf(c_1646,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( sk_c4 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_569,c_579]) ).
tcf(c_1660,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( iPr_def_26 != sk_c9 )
| ( iPr_def_23 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1503]) ).
tcf(c_1661,plain,
( ( iPr_def_26 = iPr_def_26 )
| ( iPr_def_26 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1503]) ).
tcf(c_1664,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( iPr_def_13 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_570,c_579]) ).
tcf(c_1703,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(sk_c1,iPr_def_15) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_571,c_531]) ).
tcf(c_1749,plain,
iPr_def_25 = iPr_def_25,
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_1807,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != iPr_def_13 )
| ( X0 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1134]) ).
tcf(c_1855,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_13 = X0 )
| ( iPr_def_13 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1903,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_21,sk_c4) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_576,c_530]) ).
tcf(c_1963,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_578,c_579]) ).
tcf(c_1997,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_1963,c_913]) ).
tcf(c_2059,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_23 = X0 )
| ( iPr_def_23 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_2062,plain,
! [X0: $i] :
( ( X0 = iPr_def_23 )
| ( iPr_def_23 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1435]) ).
tcf(c_2118,plain,
! [X0: $i] : multiply(sk_c3,multiply(sk_c10,X0)) = multiply(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_529,c_96]) ).
tcf(c_2121,plain,
! [X0: $i] : multiply(sk_c10,multiply(sk_c8,X0)) = multiply(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_520,c_96]) ).
tcf(c_2125,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_95,c_96]) ).
tcf(c_2129,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c10,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1046,c_96]) ).
tcf(c_2130,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1047,c_96]) ).
tcf(c_2132,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c7,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1049,c_96]) ).
tcf(c_2133,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1050,c_96]) ).
tcf(c_2135,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2133,c_94]) ).
tcf(c_2136,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c7,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2132,c_94]) ).
tcf(c_2138,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2130,c_94]) ).
tcf(c_2139,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c10,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2129,c_94]) ).
tcf(c_2165,plain,
! [X0: $i] :
( ( iPr_def_26 = X0 )
| ( iPr_def_26 != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1500]) ).
tcf(c_2473,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_13 != iPr_def_26 )
| ( sk_c10 != iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_534,c_579]) ).
tcf(c_2493,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_23 = iPr_def_26 )
| ( iPr_def_13 != iPr_def_25 )
| ( sk_c10 != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1356,c_2473]) ).
tcf(c_2550,plain,
( ~ iPr_def_12
| ( sk_c10 != iPr_def_13 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_520,c_536]) ).
tcf(c_2554,plain,
( ~ iPr_def_12
| ( sk_c10 != iPr_def_14 )
| ( inverse(iPr_def_26) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_900,c_536]) ).
tcf(c_2569,plain,
( ~ iPr_def_12
| ( sk_c10 != iPr_def_26 )
| ( sk_c10 != iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_2550,c_533]) ).
tcf(c_2690,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(sk_c10,multiply(X0,sk_c10)) != iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_537,c_579]) ).
tcf(c_2735,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_16 )
| ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(iPr_def_21,multiply(X0,iPr_def_21)) != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_544,c_2690]) ).
tcf(c_2885,plain,
! [X0: $i] :
( ~ iPr_def_10
| ( multiply(inverse(X0),iPr_def_26) != sk_c8 )
| ( multiply(X0,inverse(X0)) != sk_c8 ) ),
inference(light_normalisation,[status(thm)],[c_538,c_579]) ).
tcf(c_2900,plain,
( ~ iPr_def_10
| ( multiply(sk_c7,iPr_def_17) != sk_c8 )
| ( multiply(inverse(sk_c7),iPr_def_26) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_524,c_2885]) ).
tcf(c_3044,plain,
( ( iPr_def_26 = iPr_def_23 )
| ( iPr_def_26 != sk_c9 )
| ( iPr_def_23 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2062]) ).
tcf(c_3177,plain,
( ( iPr_def_13 = iPr_def_23 )
| ( iPr_def_23 != iPr_def_26 )
| ( iPr_def_13 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1428]) ).
tcf(c_3179,plain,
( ( sk_c9 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_26 )
| ( sk_c9 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1187]) ).
tcf(c_3340,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( iPr_def_26 != sk_c9 )
| ( iPr_def_25 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1503]) ).
tcf(c_3729,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_25 = X0 )
| ( iPr_def_25 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_3865,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_13 )
| ( iPr_def_13 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_3937,plain,
multiply(iPr_def_16,iPr_def_24) = sk_c10,
inference(superposition,[status(thm)],[c_531,c_2135]) ).
tcf(c_4168,plain,
multiply(iPr_def_17,iPr_def_15) = sk_c8,
inference(superposition,[status(thm)],[c_522,c_2136]) ).
tcf(c_4180,plain,
multiply(iPr_def_21,iPr_def_22) = sk_c10,
inference(superposition,[status(thm)],[c_529,c_2138]) ).
tcf(c_4208,plain,
multiply(iPr_def_26,iPr_def_23) = sk_c4,
inference(superposition,[status(thm)],[c_530,c_2139]) ).
tcf(c_4209,plain,
multiply(iPr_def_26,iPr_def_13) = sk_c8,
inference(superposition,[status(thm)],[c_520,c_2139]) ).
tcf(c_4210,plain,
multiply(iPr_def_26,iPr_def_25) = sk_c2,
inference(superposition,[status(thm)],[c_532,c_2139]) ).
tcf(c_4221,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_26,multiply(iPr_def_17,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_572,c_2139]) ).
tcf(c_4231,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_16 )
| ( multiply(iPr_def_26,multiply(iPr_def_17,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_540,c_2139]) ).
tcf(c_4425,plain,
! [X0: $i] :
( ( iPr_def_13 = X0 )
| ( iPr_def_13 != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1855]) ).
tcf(c_4426,plain,
( ( iPr_def_13 = sk_c10 )
| ( iPr_def_13 != iPr_def_26 )
| ( sk_c10 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_4425]) ).
tcf(c_4440,plain,
! [X0: $i] :
( ( iPr_def_23 = X0 )
| ( iPr_def_23 != iPr_def_23 )
| ( X0 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_2059]) ).
tcf(c_4975,plain,
( ( iPr_def_26 = iPr_def_23 )
| ( iPr_def_26 != iPr_def_26 )
| ( iPr_def_23 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_2165]) ).
tcf(c_4977,plain,
( ( iPr_def_26 = iPr_def_13 )
| ( iPr_def_26 != iPr_def_26 )
| ( iPr_def_13 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_2165]) ).
tcf(c_5351,plain,
( ( sk_c10 = iPr_def_16 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_545,c_990]) ).
tcf(c_5353,plain,
( ( sk_c10 = iPr_def_23 )
| ( sk_c10 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_5351,c_4180]) ).
tcf(c_5410,plain,
( ( iPr_def_23 = iPr_def_26 )
| ~ iPr_def_12
| ( sk_c10 != iPr_def_13 )
| ( inverse(iPr_def_16) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_923,c_536]) ).
tcf(c_5470,plain,
( ( iPr_def_21 = iPr_def_23 )
| ( sk_c10 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_5353,c_544]) ).
tcf(c_5471,plain,
( ( iPr_def_17 = iPr_def_23 )
| ( sk_c10 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_5353,c_540]) ).
tcf(c_5607,plain,
! [X0: $i] :
( ( iPr_def_26 = X0 )
| ( iPr_def_26 != iPr_def_23 )
| ( X0 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_1500]) ).
tcf(c_5608,plain,
! [X0: $i] :
( ( X0 = iPr_def_26 )
| ( iPr_def_26 != iPr_def_23 )
| ( X0 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_1267]) ).
tcf(c_5609,plain,
( ( sk_c10 = iPr_def_26 )
| ( iPr_def_26 != iPr_def_23 )
| ( sk_c10 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_5608]) ).
tcf(c_5610,plain,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_26 != iPr_def_23 )
| ( sk_c10 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_5607]) ).
tcf(c_5740,plain,
( ( iPr_def_26 = iPr_def_25 )
| ( iPr_def_26 != iPr_def_26 )
| ( iPr_def_25 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_2165]) ).
tcf(c_6571,plain,
! [X0: $i] :
( ( X0 = iPr_def_26 )
| ( iPr_def_26 != iPr_def_13 )
| ( X0 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1267]) ).
tcf(c_6572,plain,
( ( sk_c10 = iPr_def_26 )
| ( iPr_def_26 != iPr_def_13 )
| ( sk_c10 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_6571]) ).
tcf(c_6649,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_16,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_547,c_1022]) ).
tcf(c_6651,plain,
( ( sk_c10 = iPr_def_25 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_6649,c_3937]) ).
tcf(c_6804,plain,
! [X0: $i] :
( ( iPr_def_25 = X0 )
| ( iPr_def_25 != iPr_def_25 )
| ( X0 != iPr_def_25 ) ),
inference(instantiation,[status(thm)],[c_3729]) ).
tcf(c_6805,plain,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_25 != iPr_def_25 )
| ( sk_c10 != iPr_def_25 ) ),
inference(instantiation,[status(thm)],[c_6804]) ).
tcf(c_7471,plain,
( ( iPr_def_16 = iPr_def_25 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_6651,c_539]) ).
tcf(c_8241,plain,
! [X0: $i] :
( ( X0 = iPr_def_26 )
| ( iPr_def_26 != iPr_def_25 )
| ( X0 != iPr_def_25 ) ),
inference(instantiation,[status(thm)],[c_1267]) ).
tcf(c_8242,plain,
( ( sk_c10 = iPr_def_26 )
| ( iPr_def_26 != iPr_def_25 )
| ( sk_c10 != iPr_def_25 ) ),
inference(instantiation,[status(thm)],[c_8241]) ).
tcf(c_8429,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_16,iPr_def_24) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_1703,c_2135]) ).
tcf(c_8430,plain,
( ( sk_c10 = iPr_def_15 )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_8429,c_3937]) ).
tcf(c_9407,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( multiply(iPr_def_16,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1067,c_1019]) ).
tcf(c_9414,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c10 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_9407,c_3937]) ).
tcf(c_9555,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( iPr_def_14 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_9414,c_1963]) ).
tcf(c_9565,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( multiply(iPr_def_26,iPr_def_25) = identity ) ),
inference(superposition,[status(thm)],[c_9414,c_1046]) ).
tcf(c_9571,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( inverse(iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_9414,c_533]) ).
tcf(c_9592,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c2 = identity ) ),
inference(light_normalisation,[status(thm)],[c_9565,c_4210]) ).
tcf(c_10301,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_577,c_1903]) ).
tcf(c_10307,plain,
( ( sk_c10 = iPr_def_23 )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_10301,c_4180]) ).
tcf(c_10971,plain,
( ( iPr_def_21 = iPr_def_23 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_10307,c_576]) ).
tcf(c_10972,plain,
( ( iPr_def_17 = iPr_def_23 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_10307,c_572]) ).
tcf(c_11186,plain,
( ( iPr_def_21 = iPr_def_23 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_10971,c_5470]) ).
tcf(c_11452,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( identity = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_9592,c_1067]) ).
tcf(c_11553,plain,
( ( iPr_def_17 = iPr_def_23 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_10972,c_5471]) ).
tcf(c_12092,plain,
( ( iPr_def_23 = iPr_def_13 )
| ( iPr_def_23 != iPr_def_23 )
| ( iPr_def_13 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_4440]) ).
tcf(c_12410,plain,
! [X0: $i] :
( ( iPr_def_23 = iPr_def_26 )
| ( multiply(iPr_def_24,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_11452,c_94]) ).
tcf(c_12798,plain,
! [X0: $i] :
( ( X0 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_23 )
| ( X0 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_3865]) ).
tcf(c_12799,plain,
( ( sk_c10 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_23 )
| ( sk_c10 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_12798]) ).
tcf(c_12800,plain,
! [X0: $i] :
( ( X0 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_3865]) ).
tcf(c_12801,plain,
( ( sk_c10 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_26 )
| ( sk_c10 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_12800]) ).
tcf(c_13049,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( multiply(iPr_def_15,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1346,c_1095]) ).
tcf(c_13091,plain,
( ( iPr_def_25 = iPr_def_26 )
| ~ iPr_def_12
| ( sk_c10 != iPr_def_13 )
| ( inverse(iPr_def_15) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_1099,c_536]) ).
tcf(c_13839,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1346,c_1287]) ).
tcf(c_13843,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_13839,c_4180]) ).
tcf(c_13977,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( multiply(iPr_def_26,iPr_def_23) = identity ) ),
inference(superposition,[status(thm)],[c_13843,c_1046]) ).
tcf(c_14006,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( sk_c4 = identity ) ),
inference(light_normalisation,[status(thm)],[c_13977,c_4208]) ).
tcf(c_14913,plain,
( ( iPr_def_23 = iPr_def_26 )
| ~ iPr_def_12
| ( sk_c10 != iPr_def_14 )
| ( inverse(iPr_def_25) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_1365,c_536]) ).
tcf(c_17417,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_26,sk_c8) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_4168,c_4221]) ).
tcf(c_17421,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_17417,c_900]) ).
tcf(c_17747,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1646,c_1603]) ).
tcf(c_17754,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_17747,c_4180]) ).
tcf(c_17876,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( inverse(iPr_def_23) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_17754,c_533]) ).
tcf(c_18152,plain,
( ( iPr_def_16 = iPr_def_25 )
| ( iPr_def_14 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_17421,c_7471]) ).
tcf(c_18175,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( iPr_def_13 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_17421,c_1374]) ).
tcf(c_18178,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( iPr_def_14 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_17421,c_1081]) ).
tcf(c_18768,plain,
( ( sk_c10 = iPr_def_16 )
| ( multiply(iPr_def_26,sk_c8) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_4168,c_4231]) ).
tcf(c_18772,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( sk_c10 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_18768,c_900]) ).
tcf(c_19121,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_14 = iPr_def_15 )
| ( sk_c10 != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_18175,c_2473]) ).
tcf(c_19240,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( iPr_def_13 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_18178,c_18175]) ).
tcf(c_20583,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( inverse(iPr_def_16) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_18772,c_533]) ).
tcf(c_20694,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( iPr_def_13 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_18152,c_19240]) ).
tcf(c_20701,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( multiply(iPr_def_26,iPr_def_13) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_19240,c_4210]) ).
tcf(c_20704,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( sk_c8 = sk_c2 ) ),
inference(light_normalisation,[status(thm)],[c_20701,c_4209]) ).
tcf(c_21762,plain,
( ( iPr_def_23 = sk_c9 )
| ( iPr_def_23 != iPr_def_13 )
| ( sk_c9 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1807]) ).
tcf(c_23566,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( inverse(iPr_def_13) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_20694,c_20583]) ).
tcf(c_23693,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( sk_c8 = iPr_def_24 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_20704,c_547]) ).
tcf(c_26646,plain,
! [X0: $i] :
( ( iPr_def_25 = iPr_def_26 )
| ( iPr_def_26 != X0 )
| ( iPr_def_25 != X0 ) ),
inference(instantiation,[status(thm)],[c_1267]) ).
tcf(c_26649,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( iPr_def_26 != sk_c10 )
| ( iPr_def_25 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_26646]) ).
tcf(c_28073,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_2125,c_94]) ).
tcf(c_28124,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_95,c_28073]) ).
tcf(c_28144,plain,
multiply(inverse(iPr_def_26),iPr_def_14) = sk_c8,
inference(superposition,[status(thm)],[c_900,c_28073]) ).
tcf(c_28276,plain,
! [X0: $i] : multiply(inverse(iPr_def_26),X0) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_2139,c_28073]) ).
tcf(c_28277,plain,
! [X0: $i] : multiply(inverse(iPr_def_21),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_2138,c_28073]) ).
tcf(c_28279,plain,
! [X0: $i] : multiply(inverse(iPr_def_17),X0) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_2136,c_28073]) ).
tcf(c_28314,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_28073,c_28073]) ).
tcf(c_29175,plain,
multiply(sk_c10,iPr_def_14) = sk_c8,
inference(demodulation,[status(thm)],[c_28144,c_28276]) ).
tcf(c_29721,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_28124,c_28314]) ).
tcf(c_31050,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_555,c_579]) ).
tcf(c_31070,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( iPr_def_15 = iPr_def_16 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_31050,c_539]) ).
tcf(c_34039,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( sk_c10 = iPr_def_15 ) ),
inference(global_subsumption_just,[status(thm)],[c_31070,c_562,c_579,c_1749,c_3044,c_3340,c_5610,c_6651,c_6805,c_13843,c_26649]) ).
tcf(c_35032,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( iPr_def_26 != iPr_def_13 )
| ( iPr_def_25 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_6571]) ).
tcf(c_42494,plain,
( ( iPr_def_25 = iPr_def_13 )
| ( iPr_def_25 != iPr_def_25 )
| ( iPr_def_13 != iPr_def_25 ) ),
inference(instantiation,[status(thm)],[c_6804]) ).
tcf(c_42497,plain,
! [X0: $i] :
( ( iPr_def_13 = iPr_def_25 )
| ( iPr_def_25 != X0 )
| ( iPr_def_13 != X0 ) ),
inference(instantiation,[status(thm)],[c_1855]) ).
tcf(c_42501,plain,
( ( iPr_def_13 = iPr_def_25 )
| ( iPr_def_25 != sk_c10 )
| ( iPr_def_13 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_42497]) ).
tcf(c_43044,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( multiply(iPr_def_26,iPr_def_13) = identity ) ),
inference(superposition,[status(thm)],[c_23566,c_95]) ).
tcf(c_43045,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( sk_c8 = identity ) ),
inference(light_normalisation,[status(thm)],[c_43044,c_4209]) ).
tcf(c_45914,plain,
multiply(sk_c10,iPr_def_26) = identity,
inference(superposition,[status(thm)],[c_28276,c_95]) ).
tcf(c_45918,plain,
! [X0: $i] : multiply(sk_c10,multiply(iPr_def_26,X0)) = X0,
inference(superposition,[status(thm)],[c_28276,c_28073]) ).
tcf(c_45919,plain,
multiply(sk_c10,identity) = inverse(iPr_def_26),
inference(superposition,[status(thm)],[c_28276,c_29721]) ).
tcf(c_46808,plain,
inverse(iPr_def_26) = sk_c10,
inference(demodulation,[status(thm)],[c_45919,c_29721]) ).
tcf(c_46829,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( inverse(iPr_def_23) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_1664,c_46808]) ).
tcf(c_46830,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( inverse(iPr_def_25) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_1356,c_46808]) ).
tcf(c_46832,plain,
( ~ iPr_def_10
| ( multiply(iPr_def_26,sk_c10) != sk_c8 )
| ( multiply(inverse(iPr_def_26),iPr_def_26) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_46808,c_2885]) ).
tcf(c_46876,plain,
( ~ iPr_def_10
| ( sk_c8 != identity ) ),
inference(light_normalisation,[status(thm)],[c_46832,c_1046,c_45914,c_46808]) ).
tcf(c_46929,plain,
( ( iPr_def_14 = iPr_def_15 )
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_43045,c_46876]) ).
tcf(c_48510,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( sk_c10 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_46829,c_17876]) ).
tcf(c_48692,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c10 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_46830,c_9571]) ).
tcf(c_49087,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_26 )
| ( inverse(iPr_def_26) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_45918,c_2690]) ).
tcf(c_49241,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_26 ) ),
inference(ground_joinability,[status(thm)],[c_49087,c_46808]) ).
tcf(c_51524,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( sk_c10 = iPr_def_15 ) ),
inference(global_subsumption_just,[status(thm)],[c_23693,c_579,c_1661,c_2569,c_5740,c_6651,c_8242,c_8430,c_12801,c_18175,c_19121,c_34039,c_46929,c_49241]) ).
tcf(c_51602,plain,
iPr_def_14 = iPr_def_15,
inference(superposition,[status(thm)],[c_51524,c_17421]) ).
tcf(c_51780,plain,
multiply(iPr_def_17,iPr_def_14) = sk_c8,
inference(demodulation,[status(thm)],[c_4168,c_51602]) ).
tcf(c_51789,plain,
sk_c10 = iPr_def_14,
inference(demodulation,[status(thm)],[c_571,c_51602]) ).
tcf(c_51803,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_13 != iPr_def_26 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2473,c_51789]) ).
tcf(c_51813,plain,
inverse(iPr_def_26) = iPr_def_14,
inference(demodulation,[status(thm)],[c_46808,c_51789]) ).
tcf(c_51814,plain,
multiply(iPr_def_14,iPr_def_26) = identity,
inference(demodulation,[status(thm)],[c_45914,c_51789]) ).
tcf(c_51829,plain,
multiply(iPr_def_14,iPr_def_14) = sk_c8,
inference(demodulation,[status(thm)],[c_29175,c_51789]) ).
tcf(c_51832,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(sk_c8,X0)) = multiply(iPr_def_13,X0),
inference(demodulation,[status(thm)],[c_2121,c_51789]) ).
tcf(c_51835,plain,
! [X0: $i] : multiply(sk_c3,multiply(iPr_def_14,X0)) = multiply(iPr_def_22,X0),
inference(demodulation,[status(thm)],[c_2118,c_51789]) ).
tcf(c_51842,plain,
( ( iPr_def_14 = iPr_def_23 )
| ( iPr_def_13 = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_17754,c_51789]) ).
tcf(c_51895,plain,
multiply(iPr_def_21,iPr_def_22) = iPr_def_14,
inference(demodulation,[status(thm)],[c_4180,c_51789]) ).
tcf(c_51900,plain,
multiply(iPr_def_16,iPr_def_24) = iPr_def_14,
inference(demodulation,[status(thm)],[c_3937,c_51789]) ).
tcf(c_51915,plain,
multiply(iPr_def_26,iPr_def_14) = identity,
inference(demodulation,[status(thm)],[c_1046,c_51789]) ).
tcf(c_51919,plain,
multiply(sk_c3,iPr_def_14) = iPr_def_22,
inference(demodulation,[status(thm)],[c_529,c_51789]) ).
tcf(c_51923,plain,
inverse(iPr_def_14) = iPr_def_26,
inference(demodulation,[status(thm)],[c_533,c_51789]) ).
tcf(c_51924,plain,
multiply(iPr_def_14,sk_c8) = iPr_def_13,
inference(demodulation,[status(thm)],[c_520,c_51789]) ).
tcf(c_52525,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(iPr_def_14,X0)) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_51780,c_96]) ).
tcf(c_52768,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(iPr_def_14,X0)) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_51829,c_96]) ).
tcf(c_52774,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(iPr_def_22,X0)) = multiply(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_51895,c_96]) ).
tcf(c_53307,plain,
( ~ iPr_def_11
| ( iPr_def_14 != iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_49241,c_51789]) ).
tcf(c_53325,plain,
( ( iPr_def_13 = iPr_def_26 )
| ~ iPr_def_11
| ( iPr_def_14 != iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1664,c_53307]) ).
tcf(c_53326,plain,
( ( iPr_def_23 = iPr_def_26 )
| ~ iPr_def_11
| ( iPr_def_14 != iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1356,c_53307]) ).
tcf(c_53621,plain,
( ~ iPr_def_12
| ( inverse(iPr_def_26) != sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_2554,c_2554,c_51789]) ).
tcf(c_53623,plain,
~ iPr_def_12,
inference(ground_joinability,[status(thm)],[c_53621,c_51789,c_51813]) ).
tcf(c_53719,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( iPr_def_13 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_48510,c_51789]) ).
tcf(c_53742,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( multiply(iPr_def_14,iPr_def_14) = identity ) ),
inference(superposition,[status(thm)],[c_53719,c_51915]) ).
tcf(c_53778,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( multiply(iPr_def_14,sk_c8) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_53719,c_900]) ).
tcf(c_53782,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( iPr_def_13 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_53778,c_51924]) ).
tcf(c_53804,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( sk_c8 = identity ) ),
inference(light_normalisation,[status(thm)],[c_53742,c_51829]) ).
tcf(c_54029,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( iPr_def_14 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_48692,c_51789]) ).
tcf(c_55005,plain,
( iPr_def_11
| iPr_def_10
| ( iPr_def_13 != iPr_def_26 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_51803,c_53623]) ).
tcf(c_55016,plain,
( iPr_def_11
| iPr_def_10
| ( iPr_def_13 = iPr_def_26 )
| ( iPr_def_13 != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_53719,c_55005]) ).
tcf(c_55379,plain,
iPr_def_13 = iPr_def_26,
inference(global_subsumption_just,[status(thm)],[c_51842,c_46876,c_51842,c_53325,c_53804,c_53782,c_55016]) ).
tcf(c_55382,plain,
( iPr_def_11
| iPr_def_10
| ( iPr_def_13 != iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_55005,c_55379]) ).
tcf(c_55386,plain,
( ( iPr_def_13 = iPr_def_23 )
| ( iPr_def_13 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_54029,c_55379]) ).
tcf(c_55398,plain,
( ~ iPr_def_11
| ( iPr_def_13 != iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_53307,c_55379]) ).
tcf(c_55399,plain,
multiply(iPr_def_13,iPr_def_14) = identity,
inference(demodulation,[status(thm)],[c_51915,c_55379]) ).
tcf(c_55400,plain,
multiply(iPr_def_14,iPr_def_13) = identity,
inference(demodulation,[status(thm)],[c_51814,c_55379]) ).
tcf(c_55401,plain,
inverse(iPr_def_14) = iPr_def_13,
inference(demodulation,[status(thm)],[c_51923,c_55379]) ).
tcf(c_55436,plain,
( ( iPr_def_13 = iPr_def_25 )
| ( sk_c4 = identity ) ),
inference(demodulation,[status(thm)],[c_14006,c_55379]) ).
tcf(c_55455,plain,
( ( iPr_def_13 = iPr_def_23 )
| ( sk_c2 = identity ) ),
inference(demodulation,[status(thm)],[c_9592,c_55379]) ).
tcf(c_55473,plain,
multiply(iPr_def_13,iPr_def_25) = sk_c2,
inference(demodulation,[status(thm)],[c_4210,c_55379]) ).
tcf(c_55474,plain,
multiply(iPr_def_13,iPr_def_13) = sk_c8,
inference(demodulation,[status(thm)],[c_4209,c_55379]) ).
tcf(c_55477,plain,
multiply(iPr_def_13,iPr_def_23) = sk_c4,
inference(demodulation,[status(thm)],[c_4208,c_55379]) ).
tcf(c_55478,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( iPr_def_13 = iPr_def_23 ) ),
inference(demodulation,[status(thm)],[c_1997,c_55379]) ).
tcf(c_55486,plain,
( ( iPr_def_13 = iPr_def_25 )
| ( iPr_def_13 = iPr_def_23 ) ),
inference(demodulation,[status(thm)],[c_1356,c_55379]) ).
tcf(c_55497,plain,
( iPr_def_11
| iPr_def_10 ),
inference(equality_resolution_simp,[status(thm)],[c_55382]) ).
tcf(c_55632,plain,
( ( iPr_def_23 = iPr_def_26 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_5410,c_14913,c_46830,c_51789]) ).
tcf(c_55662,plain,
( ( iPr_def_25 = iPr_def_26 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_13091,c_579,c_1661,c_2569,c_3177,c_4975,c_5609,c_12799,c_13843,c_46876,c_51842,c_53325,c_53804,c_53782,c_55016,c_55632]) ).
tcf(c_56492,plain,
( ( sk_c10 = iPr_def_16 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_2735,c_579,c_1661,c_4977,c_5353,c_6572,c_12799,c_46876,c_49241,c_51842,c_53325,c_53804,c_53782,c_55016,c_55398,c_55386]) ).
tcf(c_56494,plain,
( ( iPr_def_14 = iPr_def_16 )
| ~ iPr_def_11 ),
inference(light_normalisation,[status(thm)],[c_56492,c_51789]) ).
tcf(c_56501,plain,
( iPr_def_10
| ( iPr_def_14 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_55497,c_56494]) ).
tcf(c_57348,plain,
( ( iPr_def_13 = iPr_def_23 )
| ( multiply(iPr_def_13,iPr_def_13) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_55486,c_55473]) ).
tcf(c_57360,plain,
( ( iPr_def_13 = iPr_def_23 )
| ( sk_c8 = sk_c2 ) ),
inference(light_normalisation,[status(thm)],[c_57348,c_55474]) ).
tcf(c_57638,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( iPr_def_13 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_55478,c_11553]) ).
tcf(c_57639,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( iPr_def_13 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_55478,c_11186]) ).
tcf(c_58035,plain,
( ( iPr_def_13 = iPr_def_23 )
| ( sk_c8 = identity ) ),
inference(superposition,[status(thm)],[c_57360,c_55455]) ).
tcf(c_58088,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(iPr_def_13,iPr_def_14) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_57638,c_51780]) ).
tcf(c_58094,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c8 = identity ) ),
inference(light_normalisation,[status(thm)],[c_58088,c_55399]) ).
tcf(c_58100,plain,
iPr_def_14 = iPr_def_16,
inference(global_subsumption_just,[status(thm)],[c_57639,c_46876,c_56501,c_58094]) ).
tcf(c_58140,plain,
multiply(iPr_def_14,iPr_def_24) = iPr_def_14,
inference(demodulation,[status(thm)],[c_51900,c_58100]) ).
tcf(c_58172,plain,
iPr_def_23 = iPr_def_26,
inference(global_subsumption_just,[status(thm)],[c_12410,c_579,c_1078,c_1137,c_1441,c_1660,c_1749,c_2493,c_3179,c_4426,c_6805,c_9414,c_9555,c_12092,c_21762,c_42501,c_46876,c_48692,c_51789,c_51842,c_53326,c_53325,c_53804,c_53782,c_55016,c_55632,c_58035]) ).
tcf(c_58174,plain,
iPr_def_13 = iPr_def_23,
inference(light_normalisation,[status(thm)],[c_58172,c_55379]) ).
tcf(c_58193,plain,
multiply(iPr_def_13,iPr_def_13) = sk_c4,
inference(demodulation,[status(thm)],[c_55477,c_58174]) ).
tcf(c_58211,plain,
sk_c8 = sk_c4,
inference(light_normalisation,[status(thm)],[c_58193,c_55474]) ).
tcf(c_58245,plain,
( ( iPr_def_13 = iPr_def_25 )
| ( sk_c8 = identity ) ),
inference(demodulation,[status(thm)],[c_55436,c_58211]) ).
tcf(c_58258,plain,
multiply(inverse(iPr_def_14),iPr_def_14) = iPr_def_24,
inference(superposition,[status(thm)],[c_58140,c_28073]) ).
tcf(c_58261,plain,
identity = iPr_def_24,
inference(light_normalisation,[status(thm)],[c_58258,c_55399,c_55401]) ).
tcf(c_58264,plain,
multiply(iPr_def_14,iPr_def_13) = iPr_def_24,
inference(demodulation,[status(thm)],[c_55400,c_58261]) ).
tcf(c_58266,plain,
( ~ iPr_def_10
| ( sk_c8 != iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_46876,c_58261]) ).
tcf(c_58268,plain,
! [X0: $i] : multiply(X0,iPr_def_24) = X0,
inference(demodulation,[status(thm)],[c_29721,c_58261]) ).
tcf(c_58271,plain,
multiply(iPr_def_21,sk_c3) = iPr_def_24,
inference(demodulation,[status(thm)],[c_1047,c_58261]) ).
tcf(c_58272,plain,
! [X0: $i] : multiply(inverse(X0),X0) = iPr_def_24,
inference(demodulation,[status(thm)],[c_95,c_58261]) ).
tcf(c_58326,plain,
iPr_def_25 = iPr_def_26,
inference(global_subsumption_just,[status(thm)],[c_13049,c_579,c_1661,c_1749,c_4975,c_4977,c_5609,c_13843,c_35032,c_42494,c_46876,c_49241,c_51803,c_51842,c_53325,c_53804,c_53782,c_55016,c_55662,c_58172,c_58245]) ).
tcf(c_58328,plain,
iPr_def_13 = iPr_def_25,
inference(light_normalisation,[status(thm)],[c_58326,c_55379]) ).
tcf(c_58332,plain,
multiply(iPr_def_13,iPr_def_13) = sk_c2,
inference(demodulation,[status(thm)],[c_55473,c_58328]) ).
tcf(c_58343,plain,
sk_c8 = sk_c2,
inference(light_normalisation,[status(thm)],[c_58332,c_55474]) ).
tcf(c_58756,plain,
multiply(sk_c3,iPr_def_21) = iPr_def_24,
inference(superposition,[status(thm)],[c_28277,c_58272]) ).
tcf(c_58757,plain,
! [X0: $i] : multiply(sk_c3,multiply(iPr_def_21,X0)) = X0,
inference(superposition,[status(thm)],[c_28277,c_28073]) ).
tcf(c_58758,plain,
multiply(sk_c3,iPr_def_24) = inverse(iPr_def_21),
inference(superposition,[status(thm)],[c_28277,c_58268]) ).
tcf(c_58767,plain,
inverse(iPr_def_21) = sk_c3,
inference(demodulation,[status(thm)],[c_58758,c_58268]) ).
tcf(c_58771,plain,
multiply(sk_c3,iPr_def_24) = sk_c3,
inference(superposition,[status(thm)],[c_58271,c_58757]) ).
tcf(c_58857,plain,
multiply(sk_c7,iPr_def_17) = iPr_def_24,
inference(superposition,[status(thm)],[c_28279,c_58272]) ).
tcf(c_58859,plain,
multiply(sk_c7,iPr_def_24) = inverse(iPr_def_17),
inference(superposition,[status(thm)],[c_28279,c_58268]) ).
tcf(c_58868,plain,
inverse(iPr_def_17) = sk_c7,
inference(demodulation,[status(thm)],[c_58859,c_58268]) ).
tcf(c_58886,plain,
multiply(sk_c8,sk_c8) = multiply(iPr_def_17,iPr_def_13),
inference(superposition,[status(thm)],[c_51924,c_52525]) ).
tcf(c_58888,plain,
multiply(sk_c8,iPr_def_14) = multiply(iPr_def_17,sk_c8),
inference(superposition,[status(thm)],[c_51829,c_52525]) ).
tcf(c_58889,plain,
multiply(sk_c8,iPr_def_13) = multiply(iPr_def_17,iPr_def_24),
inference(superposition,[status(thm)],[c_58264,c_52525]) ).
tcf(c_58960,plain,
multiply(sk_c8,iPr_def_13) = iPr_def_17,
inference(demodulation,[status(thm)],[c_58889,c_58268]) ).
tcf(c_58984,plain,
multiply(iPr_def_13,iPr_def_24) = multiply(iPr_def_14,sk_c8),
inference(superposition,[status(thm)],[c_58268,c_51832]) ).
tcf(c_59026,plain,
multiply(sk_c3,iPr_def_14) = multiply(iPr_def_22,iPr_def_24),
inference(superposition,[status(thm)],[c_58268,c_51835]) ).
tcf(c_59029,plain,
multiply(sk_c3,iPr_def_24) = multiply(iPr_def_22,iPr_def_13),
inference(superposition,[status(thm)],[c_58264,c_51835]) ).
tcf(c_59035,plain,
multiply(iPr_def_22,iPr_def_24) = iPr_def_22,
inference(light_normalisation,[status(thm)],[c_59026,c_51919]) ).
tcf(c_59043,plain,
multiply(sk_c8,sk_c8) = multiply(iPr_def_14,iPr_def_13),
inference(superposition,[status(thm)],[c_51924,c_52768]) ).
tcf(c_59046,plain,
multiply(sk_c8,iPr_def_14) = multiply(iPr_def_14,sk_c8),
inference(superposition,[status(thm)],[c_51829,c_52768]) ).
tcf(c_59047,plain,
multiply(sk_c8,iPr_def_13) = multiply(iPr_def_14,iPr_def_24),
inference(superposition,[status(thm)],[c_58264,c_52768]) ).
tcf(c_59057,plain,
multiply(iPr_def_14,iPr_def_24) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_59047,c_58960]) ).
tcf(c_59058,plain,
multiply(sk_c8,iPr_def_14) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_59046,c_51924,c_58888]) ).
tcf(c_59060,plain,
multiply(sk_c8,sk_c8) = iPr_def_24,
inference(light_normalisation,[status(thm)],[c_59043,c_58264,c_58886]) ).
tcf(c_59072,plain,
multiply(iPr_def_14,iPr_def_24) = multiply(iPr_def_21,iPr_def_22),
inference(superposition,[status(thm)],[c_58268,c_52774]) ).
tcf(c_59078,plain,
iPr_def_14 = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_59072,c_51895,c_59057]) ).
tcf(c_59080,plain,
multiply(sk_c8,iPr_def_13) = iPr_def_14,
inference(demodulation,[status(thm)],[c_58960,c_59078]) ).
tcf(c_59083,plain,
inverse(iPr_def_14) = sk_c7,
inference(demodulation,[status(thm)],[c_58868,c_59078]) ).
tcf(c_59088,plain,
inverse(sk_c7) = iPr_def_14,
inference(demodulation,[status(thm)],[c_524,c_59078]) ).
tcf(c_59089,plain,
sk_c7 = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_59083,c_55401]) ).
tcf(c_59152,plain,
multiply(iPr_def_13,sk_c8) = multiply(iPr_def_14,iPr_def_24),
inference(superposition,[status(thm)],[c_59060,c_51832]) ).
tcf(c_59535,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_59152,c_59089,c_59088,c_59083,c_59080,c_59078,c_59058,c_59057,c_59046,c_59035,c_59029,c_59026,c_58984,c_58857,c_58771,c_58767,c_58756,c_58343,c_58266,c_58261,c_58211,c_55497,c_55398,c_51814,c_51789,c_2900,c_553,c_552]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP385-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.37 % Computer : n017.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Wed Sep 23 14:33:29 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.42
% 0.11/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.42
% 0.11/0.42 % Detected problem language: tptp
% 0.11/0.43 % Proving...
% 18.88/3.29 % SZS status Started for theBenchmark.p
% 18.88/3.29 % SZS status Unsatisfiable for theBenchmark.p
% 18.88/3.29
% 18.88/3.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 18.88/3.29
% 18.88/3.29 % ------ iProver source info
% 18.88/3.29
% 18.88/3.29 % git: date: 2026-07-19 20:42:38 +0200
% 18.88/3.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 18.88/3.29 % git: non_committed_changes: false
% 18.88/3.29
% 18.88/3.29 % ------ Parsing...% successful
% 18.88/3.29
% 18.88/3.29
% 18.88/3.29 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 18.88/3.29
% 18.88/3.29 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 18.88/3.29
% 18.88/3.29 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 18.88/3.29
% 18.88/3.29 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 18.88/3.29 % ------ Proving...
% 18.88/3.29 % ------ Problem Properties
% 18.88/3.29
% 18.88/3.29 %
% 18.88/3.29 % clauses 62
% 18.88/3.29 % conjectures 45
% 18.88/3.29 % EPR 42
% 18.88/3.29 % Horn 21
% 18.88/3.29 % unary 18
% 18.88/3.29 % binary 40
% 18.88/3.29 % lits 112
% 18.88/3.29 % lits eq 106
% 18.88/3.29 % fd_pure 0
% 18.88/3.29 % fd_pseudo 0
% 18.88/3.29 % fd_cond 0
% 18.88/3.29 % fd_pseudo_cond 0
% 18.88/3.29 % AC symbols 0
% 18.88/3.29
% 18.88/3.29 % ------ Schedule dynamic 5 is on
% 18.88/3.29
% 18.88/3.29 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 18.88/3.29
% 18.88/3.29
% 18.88/3.29 % ------
% 18.88/3.29 % Current options:
% 18.88/3.29 % ------
% 18.88/3.29
% 18.88/3.29
% 18.88/3.29 %
% 18.88/3.29
% 18.88/3.29 % ------ Proving...
% 18.88/3.29 %
% 18.88/3.29
% 18.88/3.29 % SZS status Unsatisfiable for theBenchmark.p
% 18.88/3.29
% 18.88/3.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 18.90/3.30
% 18.90/3.30
%------------------------------------------------------------------------------