%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP103-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n008.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:30:44 PM UTC 2026
% Result : Unsatisfiable 8.54s 1.64s
% Output : CNFRefutation 8.54s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))),double_divide(identity,identity)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,axiom,
! [X0,X1] : multiply(X0,X1) = double_divide(double_divide(X1,X0),identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiply) ).
fof(f3,axiom,
! [X0] : inverse(X0) = double_divide(X0,identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inverse) ).
fof(f4,axiom,
! [X0] : identity = double_divide(X0,inverse(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity) ).
fof(f5,negated_conjecture,
( multiply(a4,b4) != multiply(b4,a4)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(identity,a2) != a2
| multiply(inverse(a1),a1) != identity ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms) ).
fof(f6,plain,
( multiply(a4,b4) != multiply(b4,a4)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| a2 != multiply(identity,a2)
| identity != multiply(inverse(a1),a1) ),
inference(reorient_equations,[],[f5]) ).
fof(f7,plain,
! [X0] : identity = double_divide(X0,double_divide(X0,identity)),
inference(definition_unfolding,[],[f4,f3]) ).
fof(f8,plain,
( double_divide(double_divide(b4,a4),identity) != double_divide(double_divide(a4,b4),identity)
| double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity) != double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity)
| a2 != double_divide(double_divide(a2,identity),identity)
| identity != double_divide(double_divide(a1,double_divide(a1,identity)),identity) ),
inference(definition_unfolding,[],[f6,f2,f3,f2,f2,f2,f2,f2,f2,f2]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))),double_divide(identity,identity)) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_55,plain,
! [X0: $i] : double_divide(X0,double_divide(X0,identity)) = identity,
inference(cnf_transformation,[],[f7]) ).
tcf(c_56,negated_conjecture,
( ( double_divide(double_divide(a4,b4),identity) != double_divide(double_divide(b4,a4),identity) )
| ( double_divide(double_divide(a2,identity),identity) != a2 )
| ( double_divide(double_divide(a1,double_divide(a1,identity)),identity) != identity )
| ( double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity) != double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity) ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0))))),double_divide(X3,X2))),double_divide(identity,identity)) = X3,
inference(superposition,[status(thm)],[c_54,c_54]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,double_divide(identity,double_divide(X1,double_divide(double_divide(identity,identity),X0)))),double_divide(identity,identity)) = X1,
inference(superposition,[status(thm)],[c_55,c_54]) ).
tcf(c_112,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(double_divide(X0,identity),double_divide(double_divide(identity,X0),double_divide(X1,identity))),double_divide(identity,identity)) = X1,
inference(superposition,[status(thm)],[c_55,c_54]) ).
tcf(c_113,plain,
! [X0: $i] : double_divide(double_divide(identity,double_divide(double_divide(identity,X0),identity)),double_divide(identity,identity)) = X0,
inference(superposition,[status(thm)],[c_55,c_54]) ).
tcf(c_121,plain,
( ( double_divide(identity,identity) != identity )
| ( double_divide(double_divide(a4,b4),identity) != double_divide(double_divide(b4,a4),identity) )
| ( double_divide(double_divide(a2,identity),identity) != a2 )
| ( double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity) != double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity) ) ),
inference(demodulation,[status(thm)],[c_56,c_55]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(identity,double_divide(X1,X0))))) = double_divide(double_divide(double_divide(identity,identity),identity),double_divide(identity,identity)),
inference(superposition,[status(thm)],[c_55,c_106]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(identity,double_divide(double_divide(identity,identity),X0))),double_divide(X1,double_divide(X2,double_divide(double_divide(identity,X3),double_divide(X0,double_divide(X3,X2))))))),double_divide(identity,identity)) = X1,
inference(superposition,[status(thm)],[c_54,c_106]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(double_divide(identity,identity),double_divide(X1,X0))))),X2)),double_divide(identity,identity)) = double_divide(X3,double_divide(double_divide(identity,X4),double_divide(X2,double_divide(X4,X3)))),
inference(superposition,[status(thm)],[c_54,c_106]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(double_divide(X2,identity),double_divide(X1,X0))))),identity)),double_divide(identity,identity)) = X2,
inference(superposition,[status(thm)],[c_55,c_106]) ).
tcf(c_136,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0))))),double_divide(X3,X2))) = double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X3)),double_divide(identity,identity)),
inference(superposition,[status(thm)],[c_106,c_54]) ).
tcf(c_137,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(double_divide(identity,identity),double_divide(X1,X0))))),X2)),double_divide(identity,identity)) = double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(X3,double_divide(double_divide(identity,X4),double_divide(X5,double_divide(X4,X3))))),double_divide(X2,X5))),
inference(superposition,[status(thm)],[c_106,c_106]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))) = iPr_def_10(X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_130]) ).
tcf(c_149,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(double_divide(identity,identity),double_divide(X1,X0))))),X2)),double_divide(identity,identity)) = iPr_def_10(X2),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_130]) ).
tcf(c_152,plain,
! [X0: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,iPr_def_10(double_divide(identity,identity))),X0)),double_divide(identity,identity)) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_149,c_148]) ).
tcf(c_156,plain,
! [X0: $i] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),double_divide(identity,identity)) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_137,c_136,c_148,c_152]) ).
tcf(c_234,plain,
double_divide(double_divide(identity,double_divide(identity,identity)),double_divide(identity,identity)) = double_divide(identity,identity),
inference(superposition,[status(thm)],[c_55,c_111]) ).
tcf(c_236,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(X0,double_divide(identity,double_divide(X1,double_divide(double_divide(identity,identity),X0))))),double_divide(X2,X1)))),double_divide(X3,X2))),double_divide(identity,identity)) = X3,
inference(superposition,[status(thm)],[c_111,c_106]) ).
tcf(c_239,plain,
! [X0: $i,X1: $i] : double_divide(X0,double_divide(identity,double_divide(X1,double_divide(double_divide(identity,identity),X0)))) = double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X1)),double_divide(identity,identity)),
inference(superposition,[status(thm)],[c_111,c_54]) ).
tcf(c_241,plain,
double_divide(identity,identity) = identity,
inference(demodulation,[status(thm)],[c_234,c_55]) ).
tcf(c_245,plain,
! [X0: $i,X1: $i] : double_divide(X0,double_divide(identity,double_divide(X1,double_divide(identity,X0)))) = double_divide(double_divide(identity,double_divide(identity,X1)),identity),
inference(demodulation,[status(thm)],[c_239,c_241]) ).
tcf(c_253,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(identity,X0)),identity)),double_divide(X1,X0)))),double_divide(X2,X1))),identity) = X2,
inference(demodulation,[status(thm)],[c_236,c_241,c_245]) ).
tcf(c_254,plain,
( ( double_divide(double_divide(a4,b4),identity) != double_divide(double_divide(b4,a4),identity) )
| ( double_divide(double_divide(a2,identity),identity) != a2 )
| ( double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity) != double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity) ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_121,c_241]) ).
tcf(c_325,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(double_divide(X0,identity),double_divide(double_divide(identity,X0),double_divide(X1,identity))),identity) = X1,
inference(demodulation,[status(thm)],[c_112,c_241]) ).
tcf(c_330,plain,
! [X0: $i] : double_divide(double_divide(double_divide(X0,identity),identity),identity) = double_divide(identity,X0),
inference(superposition,[status(thm)],[c_55,c_325]) ).
tcf(c_340,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(identity,double_divide(X1,X0))))),X2)),double_divide(identity,identity)) = double_divide(double_divide(X3,identity),double_divide(double_divide(identity,X3),double_divide(X2,identity))),
inference(superposition,[status(thm)],[c_325,c_106]) ).
tcf(c_341,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(double_divide(X0,identity),double_divide(double_divide(identity,X0),X1)),identity) = double_divide(double_divide(X2,identity),double_divide(double_divide(identity,X2),double_divide(X1,identity))),
inference(superposition,[status(thm)],[c_325,c_325]) ).
tcf(c_350,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(double_divide(X0,identity),double_divide(double_divide(identity,X0),X1)),identity) = iPr_def_11(X1),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_341]) ).
tcf(c_351,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,identity),double_divide(double_divide(identity,X0),double_divide(X1,identity))) = iPr_def_11(X1),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_341]) ).
tcf(c_360,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(identity,double_divide(X1,X0))))),X2)),double_divide(identity,identity)) = iPr_def_11(X2),
inference(demodulation,[status(thm)],[c_340,c_351]) ).
tcf(c_361,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(identity,double_divide(X1,X0))))),X2)),identity) = iPr_def_11(X2),
inference(light_normalisation,[status(thm)],[c_360,c_241]) ).
tcf(c_362,plain,
! [X0: $i] : double_divide(double_divide(identity,double_divide(identity,X0)),identity) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_361,c_122,c_241]) ).
tcf(c_405,plain,
! [X0: $i] : double_divide(double_divide(identity,double_divide(double_divide(identity,X0),identity)),identity) = X0,
inference(demodulation,[status(thm)],[c_113,c_241]) ).
tcf(c_412,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(double_divide(X0,identity),double_divide(double_divide(identity,X0),X1)),identity) = double_divide(identity,double_divide(double_divide(identity,X1),identity)),
inference(superposition,[status(thm)],[c_405,c_325]) ).
tcf(c_414,plain,
! [X0: $i] : double_divide(identity,double_divide(double_divide(identity,X0),identity)) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_412,c_350]) ).
tcf(c_439,plain,
double_divide(identity,iPr_def_10(identity)) = identity,
inference(demodulation,[status(thm)],[c_122,c_148,c_241]) ).
tcf(c_441,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,double_divide(identity,double_divide(X1,double_divide(iPr_def_10(identity),X0)))),double_divide(identity,identity)) = X1,
inference(superposition,[status(thm)],[c_439,c_54]) ).
tcf(c_445,plain,
double_divide(double_divide(identity,double_divide(identity,identity)),identity) = iPr_def_10(identity),
inference(superposition,[status(thm)],[c_439,c_405]) ).
tcf(c_446,plain,
! [X0: $i] : double_divide(double_divide(double_divide(iPr_def_10(identity),identity),double_divide(identity,double_divide(X0,identity))),identity) = X0,
inference(superposition,[status(thm)],[c_439,c_325]) ).
tcf(c_447,plain,
iPr_def_10(identity) = identity,
inference(light_normalisation,[status(thm)],[c_445,c_241]) ).
tcf(c_449,plain,
! [X0: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(identity,double_divide(X0,identity))),identity) = X0,
inference(demodulation,[status(thm)],[c_446,c_447]) ).
tcf(c_450,plain,
! [X0: $i] : double_divide(double_divide(identity,double_divide(identity,double_divide(X0,identity))),identity) = X0,
inference(light_normalisation,[status(thm)],[c_449,c_241]) ).
tcf(c_451,plain,
! [X0: $i] : iPr_def_11(double_divide(X0,identity)) = X0,
inference(demodulation,[status(thm)],[c_450,c_362]) ).
tcf(c_457,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,double_divide(identity,double_divide(X1,double_divide(identity,X0)))),double_divide(identity,identity)) = X1,
inference(demodulation,[status(thm)],[c_441,c_447]) ).
tcf(c_458,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,double_divide(identity,double_divide(X1,double_divide(identity,X0)))),identity) = X1,
inference(light_normalisation,[status(thm)],[c_457,c_241]) ).
tcf(c_459,plain,
! [X0: $i] : double_divide(iPr_def_11(X0),identity) = X0,
inference(demodulation,[status(thm)],[c_458,c_245,c_362]) ).
tcf(c_485,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(identity,X0))),double_divide(X1,iPr_def_10(X0)))),identity) = X1,
inference(demodulation,[status(thm)],[c_124,c_148,c_241]) ).
tcf(c_496,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(identity,X0))),double_divide(X1,iPr_def_10(X0)))),X1) = identity,
inference(superposition,[status(thm)],[c_485,c_55]) ).
tcf(c_499,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(identity,double_divide(identity,double_divide(identity,X0))),double_divide(X1,iPr_def_10(X0))) = double_divide(double_divide(identity,X1),identity),
inference(superposition,[status(thm)],[c_485,c_405]) ).
tcf(c_512,plain,
! [X0: $i] : double_divide(double_divide(identity,double_divide(double_divide(identity,X0),identity)),X0) = identity,
inference(demodulation,[status(thm)],[c_496,c_499]) ).
tcf(c_513,plain,
! [X0: $i] : double_divide(iPr_def_11(X0),X0) = identity,
inference(demodulation,[status(thm)],[c_512,c_414]) ).
tcf(c_527,plain,
! [X0: $i] : iPr_def_10(double_divide(X0,identity)) = X0,
inference(demodulation,[status(thm)],[c_131,c_148,c_241,c_414,c_459]) ).
tcf(c_531,plain,
! [X0: $i] : double_divide(identity,double_divide(double_divide(identity,X0),identity)) = iPr_def_10(X0),
inference(superposition,[status(thm)],[c_405,c_527]) ).
tcf(c_532,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(identity,X0))),double_divide(X1,iPr_def_10(X0)))) = iPr_def_10(X1),
inference(superposition,[status(thm)],[c_485,c_527]) ).
tcf(c_535,plain,
! [X0: $i] : iPr_def_10(X0) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_531,c_414]) ).
tcf(c_539,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(double_divide(identity,double_divide(identity,double_divide(identity,X0))),double_divide(X1,iPr_def_11(X0)))) = iPr_def_11(X1),
inference(demodulation,[status(thm)],[c_532,c_535]) ).
tcf(c_540,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(double_divide(identity,iPr_def_11(X0)),double_divide(X1,X0))) = iPr_def_11(X1),
inference(demodulation,[status(thm)],[c_136,c_148,c_156,c_241,c_535]) ).
tcf(c_543,plain,
double_divide(identity,double_divide(double_divide(identity,iPr_def_11(identity)),identity)) = iPr_def_11(identity),
inference(superposition,[status(thm)],[c_241,c_540]) ).
tcf(c_562,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(identity,iPr_def_11(X0))),double_divide(X1,iPr_def_10(double_divide(double_divide(identity,iPr_def_11(X2)),double_divide(X0,X2)))))),identity) = X1,
inference(superposition,[status(thm)],[c_540,c_485]) ).
tcf(c_563,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(identity,iPr_def_11(X0)),double_divide(X1,X0)) = double_divide(double_divide(identity,double_divide(iPr_def_11(X1),identity)),identity),
inference(superposition,[status(thm)],[c_540,c_405]) ).
tcf(c_566,plain,
iPr_def_11(iPr_def_11(identity)) = iPr_def_11(identity),
inference(demodulation,[status(thm)],[c_543,c_414]) ).
tcf(c_573,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(identity,iPr_def_11(X0)),double_divide(X1,X0)) = double_divide(double_divide(identity,X1),identity),
inference(demodulation,[status(thm)],[c_563,c_459]) ).
tcf(c_600,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(identity,iPr_def_11(X0))),double_divide(X1,iPr_def_10(double_divide(double_divide(identity,X0),identity))))),identity) = X1,
inference(demodulation,[status(thm)],[c_562,c_573]) ).
tcf(c_601,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(identity,iPr_def_11(X0))),double_divide(X1,double_divide(identity,X0)))),identity) = X1,
inference(demodulation,[status(thm)],[c_600,c_527]) ).
tcf(c_709,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))) = iPr_def_11(X2),
inference(demodulation,[status(thm)],[c_148,c_535]) ).
tcf(c_713,plain,
! [X0: $i,X1: $i] : double_divide(X0,double_divide(identity,double_divide(X1,double_divide(identity,X0)))) = iPr_def_11(X1),
inference(superposition,[status(thm)],[c_241,c_709]) ).
tcf(c_715,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(X0,double_divide(iPr_def_11(X1),double_divide(X2,double_divide(double_divide(double_divide(identity,iPr_def_11(X3)),double_divide(X1,X3)),X0)))) = iPr_def_11(X2),
inference(superposition,[status(thm)],[c_540,c_709]) ).
tcf(c_721,plain,
! [X0: $i,X1: $i] : iPr_def_11(double_divide(X0,double_divide(identity,double_divide(X1,double_divide(double_divide(identity,identity),X0))))) = double_divide(identity,double_divide(double_divide(identity,identity),X1)),
inference(superposition,[status(thm)],[c_111,c_709]) ).
tcf(c_722,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,X1),double_divide(double_divide(identity,double_divide(identity,iPr_def_11(X1))),iPr_def_11(X0))) = iPr_def_11(identity),
inference(superposition,[status(thm)],[c_540,c_709]) ).
tcf(c_737,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(double_divide(double_divide(identity,X0),double_divide(X1,double_divide(X0,X2))),double_divide(double_divide(identity,X2),double_divide(X3,iPr_def_11(X1)))) = iPr_def_11(X3),
inference(superposition,[status(thm)],[c_709,c_709]) ).
tcf(c_738,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(identity,double_divide(double_divide(identity,iPr_def_11(double_divide(double_divide(identity,X0),double_divide(X1,double_divide(X0,X2))))),iPr_def_11(X1))) = iPr_def_11(X2),
inference(superposition,[status(thm)],[c_709,c_540]) ).
tcf(c_741,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(double_divide(identity,double_divide(identity,X1)),iPr_def_11(X0))) = iPr_def_11(X2),
inference(superposition,[status(thm)],[c_709,c_709]) ).
tcf(c_744,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,double_divide(identity,X1)),iPr_def_11(X1)) = iPr_def_11(double_divide(identity,X0)),
inference(superposition,[status(thm)],[c_709,c_709]) ).
tcf(c_749,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(double_divide(double_divide(identity,X2),double_divide(X3,double_divide(X2,X4))),double_divide(X1,X0))))),iPr_def_11(X3))),double_divide(identity,identity)) = X4,
inference(superposition,[status(thm)],[c_709,c_106]) ).
tcf(c_754,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(identity,X0),double_divide(X1,double_divide(X0,identity))) = double_divide(double_divide(identity,double_divide(iPr_def_11(X1),identity)),identity),
inference(superposition,[status(thm)],[c_709,c_405]) ).
tcf(c_777,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(identity,X0),double_divide(X1,double_divide(X0,identity))) = double_divide(double_divide(identity,X1),identity),
inference(demodulation,[status(thm)],[c_754,c_459]) ).
tcf(c_790,plain,
! [X0: $i,X1: $i] : iPr_def_11(double_divide(X0,double_divide(identity,double_divide(X1,double_divide(identity,X0))))) = double_divide(identity,double_divide(identity,X1)),
inference(light_normalisation,[status(thm)],[c_721,c_241]) ).
tcf(c_791,plain,
! [X0: $i] : double_divide(identity,double_divide(identity,X0)) = iPr_def_11(iPr_def_11(X0)),
inference(demodulation,[status(thm)],[c_790,c_245,c_362]) ).
tcf(c_796,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(X0,double_divide(iPr_def_11(X1),double_divide(X2,double_divide(double_divide(double_divide(identity,X1),identity),X0)))) = iPr_def_11(X2),
inference(demodulation,[status(thm)],[c_715,c_573]) ).
tcf(c_831,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,iPr_def_11(double_divide(double_divide(identity,X0),double_divide(X1,double_divide(X0,X2))))),iPr_def_11(X1))),double_divide(identity,identity)) = X2,
inference(demodulation,[status(thm)],[c_749,c_709]) ).
tcf(c_832,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(identity,double_divide(double_divide(identity,iPr_def_11(double_divide(double_divide(identity,X0),double_divide(X1,double_divide(X0,X2))))),iPr_def_11(X1))),identity) = X2,
inference(light_normalisation,[status(thm)],[c_831,c_241]) ).
tcf(c_970,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(identity,double_divide(iPr_def_11(iPr_def_11(double_divide(iPr_def_11(double_divide(identity,X0)),double_divide(X1,X0)))),double_divide(X2,X1))),identity) = X2,
inference(demodulation,[status(thm)],[c_253,c_414,c_791]) ).
tcf(c_972,plain,
! [X0: $i] : iPr_def_11(iPr_def_11(double_divide(iPr_def_11(double_divide(identity,X0)),double_divide(identity,X0)))) = double_divide(double_divide(identity,identity),identity),
inference(superposition,[status(thm)],[c_55,c_970]) ).
tcf(c_980,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(double_divide(identity,double_divide(iPr_def_11(iPr_def_11(double_divide(iPr_def_11(double_divide(identity,double_divide(double_divide(identity,X0),double_divide(X1,double_divide(X0,X2))))),iPr_def_11(X1)))),double_divide(X3,X2))),identity) = X3,
inference(superposition,[status(thm)],[c_709,c_970]) ).
tcf(c_1021,plain,
! [X0: $i] : iPr_def_11(iPr_def_11(double_divide(iPr_def_11(double_divide(identity,X0)),double_divide(identity,X0)))) = identity,
inference(light_normalisation,[status(thm)],[c_972,c_241]) ).
tcf(c_1022,plain,
iPr_def_11(identity) = identity,
inference(demodulation,[status(thm)],[c_1021,c_513,c_566]) ).
tcf(c_1204,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(double_divide(X0,identity),double_divide(double_divide(identity,X0),double_divide(X1,identity)))) = double_divide(double_divide(X1,identity),identity),
inference(superposition,[status(thm)],[c_325,c_330]) ).
tcf(c_1206,plain,
! [X0: $i] : double_divide(identity,double_divide(identity,double_divide(double_divide(identity,X0),identity))) = double_divide(double_divide(X0,identity),identity),
inference(superposition,[status(thm)],[c_405,c_330]) ).
tcf(c_1215,plain,
! [X0: $i] : double_divide(double_divide(double_divide(identity,X0),identity),identity) = double_divide(identity,double_divide(double_divide(X0,identity),identity)),
inference(superposition,[status(thm)],[c_330,c_330]) ).
tcf(c_1216,plain,
! [X0: $i] : double_divide(double_divide(X0,identity),identity) = iPr_def_10(double_divide(identity,X0)),
inference(superposition,[status(thm)],[c_330,c_527]) ).
tcf(c_1222,plain,
! [X0: $i] : double_divide(double_divide(identity,X0),identity) = double_divide(identity,double_divide(X0,identity)),
inference(superposition,[status(thm)],[c_330,c_330]) ).
tcf(c_1229,plain,
! [X0: $i] : double_divide(double_divide(X0,identity),identity) = iPr_def_11(double_divide(identity,X0)),
inference(demodulation,[status(thm)],[c_1216,c_535]) ).
tcf(c_1236,plain,
! [X0: $i] : double_divide(identity,iPr_def_11(double_divide(identity,X0))) = iPr_def_11(double_divide(identity,double_divide(identity,X0))),
inference(demodulation,[status(thm)],[c_1215,c_1229]) ).
tcf(c_1237,plain,
! [X0: $i] : double_divide(identity,iPr_def_11(double_divide(identity,X0))) = iPr_def_11(iPr_def_11(iPr_def_11(X0))),
inference(demodulation,[status(thm)],[c_1236,c_791]) ).
tcf(c_1239,plain,
! [X0: $i] : double_divide(identity,double_divide(identity,double_divide(identity,double_divide(X0,identity)))) = iPr_def_11(double_divide(identity,X0)),
inference(demodulation,[status(thm)],[c_1206,c_1222,c_1229]) ).
tcf(c_1240,plain,
! [X0: $i] : iPr_def_11(iPr_def_11(double_divide(identity,double_divide(X0,identity)))) = iPr_def_11(double_divide(identity,X0)),
inference(demodulation,[status(thm)],[c_1239,c_791]) ).
tcf(c_1256,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(double_divide(X0,identity),double_divide(double_divide(identity,X0),double_divide(X1,identity)))) = iPr_def_11(double_divide(identity,X1)),
inference(demodulation,[status(thm)],[c_1204,c_1229]) ).
tcf(c_1257,plain,
! [X0: $i] : double_divide(identity,iPr_def_11(X0)) = iPr_def_11(double_divide(identity,X0)),
inference(demodulation,[status(thm)],[c_1256,c_351]) ).
tcf(c_1357,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(double_divide(identity,X0),double_divide(double_divide(identity,double_divide(double_divide(X0,identity),identity)),X1)),identity) = iPr_def_11(X1),
inference(superposition,[status(thm)],[c_330,c_350]) ).
tcf(c_1381,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(iPr_def_11(X0),double_divide(double_divide(identity,double_divide(double_divide(X1,identity),double_divide(double_divide(identity,X1),X0))),X2)),identity) = iPr_def_11(X2),
inference(superposition,[status(thm)],[c_350,c_350]) ).
tcf(c_1383,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,identity),double_divide(double_divide(identity,X0),X1)) = iPr_def_10(iPr_def_11(X1)),
inference(superposition,[status(thm)],[c_350,c_527]) ).
tcf(c_1392,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,identity),double_divide(double_divide(identity,X0),X1)) = iPr_def_11(iPr_def_11(X1)),
inference(demodulation,[status(thm)],[c_1383,c_535]) ).
tcf(c_1410,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(double_divide(identity,X0),double_divide(iPr_def_11(iPr_def_11(iPr_def_11(X0))),X1)),identity) = iPr_def_11(X1),
inference(demodulation,[status(thm)],[c_1357,c_1229,c_1237]) ).
tcf(c_1422,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(iPr_def_11(X0),double_divide(double_divide(identity,iPr_def_11(iPr_def_11(X0))),X1)),identity) = iPr_def_11(X1),
inference(demodulation,[status(thm)],[c_1381,c_1392]) ).
tcf(c_1423,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(iPr_def_11(X0),double_divide(iPr_def_11(iPr_def_11(double_divide(identity,X0))),X1)),identity) = iPr_def_11(X1),
inference(demodulation,[status(thm)],[c_1422,c_1257]) ).
tcf(c_1520,plain,
! [X0: $i,X1: $i] : double_divide(iPr_def_11(iPr_def_11(double_divide(identity,X0))),double_divide(X1,iPr_def_11(X0))) = double_divide(identity,double_divide(X1,identity)),
inference(demodulation,[status(thm)],[c_499,c_535,c_791,c_1222]) ).
tcf(c_1530,plain,
! [X0: $i,X1: $i] : double_divide(iPr_def_11(iPr_def_11(double_divide(identity,double_divide(X0,identity)))),double_divide(X1,X0)) = double_divide(identity,double_divide(X1,identity)),
inference(superposition,[status(thm)],[c_451,c_1520]) ).
tcf(c_1534,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(X0,iPr_def_11(X1)),double_divide(double_divide(identity,iPr_def_11(iPr_def_11(double_divide(identity,X1)))),double_divide(X2,double_divide(identity,double_divide(X0,identity))))) = iPr_def_11(X2),
inference(superposition,[status(thm)],[c_1520,c_709]) ).
tcf(c_1542,plain,
! [X0: $i] : double_divide(double_divide(iPr_def_11(X0),double_divide(identity,double_divide(identity,double_divide(double_divide(identity,identity),identity)))),double_divide(identity,identity)) = iPr_def_11(iPr_def_11(double_divide(identity,X0))),
inference(superposition,[status(thm)],[c_1520,c_111]) ).
tcf(c_1559,plain,
! [X0: $i,X1: $i] : double_divide(iPr_def_11(double_divide(identity,X0)),double_divide(X1,X0)) = double_divide(identity,double_divide(X1,identity)),
inference(demodulation,[status(thm)],[c_1530,c_1240]) ).
tcf(c_1564,plain,
! [X0: $i] : iPr_def_11(iPr_def_11(double_divide(identity,X0))) = double_divide(X0,identity),
inference(light_normalisation,[status(thm)],[c_1542,c_241,c_459]) ).
tcf(c_1574,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(X0,iPr_def_11(X1)),double_divide(double_divide(identity,double_divide(X1,identity)),double_divide(X2,double_divide(identity,double_divide(X0,identity))))) = iPr_def_11(X2),
inference(demodulation,[status(thm)],[c_1534,c_1564]) ).
tcf(c_1628,plain,
! [X0: $i,X1: $i] : double_divide(X0,double_divide(double_divide(identity,X1),identity)) = iPr_def_11(iPr_def_11(double_divide(X1,X0))),
inference(superposition,[status(thm)],[c_513,c_709]) ).
tcf(c_1629,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),identity))),double_divide(X2,iPr_def_11(double_divide(X1,X0))))),double_divide(identity,identity)) = X2,
inference(superposition,[status(thm)],[c_513,c_106]) ).
tcf(c_1651,plain,
! [X0: $i,X1: $i] : double_divide(X0,double_divide(identity,double_divide(X1,identity))) = iPr_def_11(iPr_def_11(double_divide(X1,X0))),
inference(demodulation,[status(thm)],[c_1628,c_1222]) ).
tcf(c_1671,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),identity))),double_divide(X2,iPr_def_11(double_divide(X1,X0))))),identity) = X2,
inference(light_normalisation,[status(thm)],[c_1629,c_241]) ).
tcf(c_1672,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(X0,double_divide(identity,double_divide(X1,identity)))),double_divide(X2,iPr_def_11(double_divide(X1,X0)))),identity)) = X2,
inference(demodulation,[status(thm)],[c_1671,c_1222]) ).
tcf(c_1853,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(double_divide(X0,identity),double_divide(X1,iPr_def_11(X0)))) = iPr_def_11(X1),
inference(demodulation,[status(thm)],[c_539,c_791,c_1564]) ).
tcf(c_1890,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,identity),double_divide(X1,iPr_def_11(X0))) = double_divide(double_divide(identity,double_divide(iPr_def_11(X1),identity)),identity),
inference(superposition,[status(thm)],[c_1853,c_405]) ).
tcf(c_1912,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,identity),double_divide(X1,iPr_def_11(X0))) = double_divide(identity,double_divide(X1,identity)),
inference(demodulation,[status(thm)],[c_1890,c_1222,c_1229,c_1257,c_1564]) ).
tcf(c_2013,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(double_divide(iPr_def_11(iPr_def_11(iPr_def_11(X0))),double_divide(X1,double_divide(identity,X0))),identity)) = X1,
inference(demodulation,[status(thm)],[c_601,c_791,c_1222]) ).
tcf(c_2033,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(X0,double_divide(X1,double_divide(X2,double_divide(double_divide(double_divide(iPr_def_11(iPr_def_11(iPr_def_11(X3))),double_divide(X1,double_divide(identity,X3))),identity),X0)))) = iPr_def_11(X2),
inference(superposition,[status(thm)],[c_2013,c_709]) ).
tcf(c_2051,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(iPr_def_11(iPr_def_11(iPr_def_11(X0))),double_divide(X1,double_divide(identity,X0))),identity) = double_divide(double_divide(identity,double_divide(X1,identity)),identity),
inference(superposition,[status(thm)],[c_2013,c_405]) ).
tcf(c_2076,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(iPr_def_11(iPr_def_11(iPr_def_11(X0))),double_divide(X1,double_divide(identity,X0))),identity) = iPr_def_11(iPr_def_11(iPr_def_11(X1))),
inference(demodulation,[status(thm)],[c_2051,c_1222,c_1229,c_1237]) ).
tcf(c_2100,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(X0,double_divide(X1,double_divide(X2,double_divide(iPr_def_11(iPr_def_11(iPr_def_11(X1))),X0)))) = iPr_def_11(X2),
inference(demodulation,[status(thm)],[c_2033,c_2076]) ).
tcf(c_2186,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(double_divide(X0,double_divide(identity,X1)),double_divide(double_divide(identity,identity),iPr_def_11(X0)))),double_divide(X2,X1))),double_divide(identity,identity)) = X2,
inference(superposition,[status(thm)],[c_713,c_106]) ).
tcf(c_2289,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(double_divide(X0,double_divide(identity,X1)),double_divide(identity,iPr_def_11(X0)))),double_divide(X2,X1))),identity) = X2,
inference(light_normalisation,[status(thm)],[c_2186,c_241]) ).
tcf(c_2290,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(double_divide(X0,double_divide(identity,X1)),iPr_def_11(double_divide(identity,X0)))),double_divide(X2,X1)),identity)) = X2,
inference(demodulation,[status(thm)],[c_2289,c_1222,c_1257]) ).
tcf(c_2301,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,X1),double_divide(iPr_def_11(iPr_def_11(iPr_def_11(X1))),iPr_def_11(X0))) = identity,
inference(demodulation,[status(thm)],[c_722,c_791,c_1022]) ).
tcf(c_2341,plain,
! [X0: $i,X1: $i] : double_divide(iPr_def_11(X0),double_divide(double_divide(identity,iPr_def_11(iPr_def_11(iPr_def_11(X1)))),identity)) = iPr_def_11(double_divide(X0,X1)),
inference(superposition,[status(thm)],[c_2301,c_709]) ).
tcf(c_2349,plain,
! [X0: $i] : iPr_def_11(double_divide(iPr_def_11(iPr_def_11(iPr_def_11(X0))),iPr_def_11(identity))) = double_divide(double_divide(double_divide(X0,identity),identity),identity),
inference(superposition,[status(thm)],[c_2301,c_350]) ).
tcf(c_2379,plain,
! [X0: $i] : iPr_def_11(double_divide(iPr_def_11(iPr_def_11(iPr_def_11(X0))),identity)) = double_divide(identity,X0),
inference(light_normalisation,[status(thm)],[c_2349,c_330,c_1022]) ).
tcf(c_2380,plain,
! [X0: $i] : iPr_def_11(iPr_def_11(iPr_def_11(X0))) = double_divide(identity,X0),
inference(demodulation,[status(thm)],[c_2379,c_451]) ).
tcf(c_2382,plain,
! [X0: $i,X1: $i] : double_divide(iPr_def_11(X0),double_divide(double_divide(identity,double_divide(identity,X1)),identity)) = iPr_def_11(double_divide(X0,X1)),
inference(demodulation,[status(thm)],[c_2341,c_2380]) ).
tcf(c_2383,plain,
! [X0: $i,X1: $i] : double_divide(iPr_def_11(X0),iPr_def_11(X1)) = iPr_def_11(double_divide(X0,X1)),
inference(demodulation,[status(thm)],[c_2382,c_451,c_791,c_1222]) ).
tcf(c_2554,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(iPr_def_11(X0),double_divide(double_divide(identity,double_divide(X1,double_divide(identity,X0))),double_divide(X2,iPr_def_11(double_divide(identity,X1))))) = iPr_def_11(X2),
inference(superposition,[status(thm)],[c_709,c_737]) ).
tcf(c_2564,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(double_divide(double_divide(identity,double_divide(identity,X0)),iPr_def_11(X1)),double_divide(double_divide(identity,double_divide(X1,double_divide(X0,X2))),double_divide(X3,iPr_def_11(X2)))) = iPr_def_11(X3),
inference(superposition,[status(thm)],[c_709,c_737]) ).
tcf(c_2570,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(double_divide(identity,double_divide(identity,iPr_def_11(X0))),iPr_def_11(X1)),double_divide(double_divide(identity,double_divide(X1,X0)),double_divide(X2,iPr_def_11(identity)))) = iPr_def_11(X2),
inference(superposition,[status(thm)],[c_540,c_737]) ).
tcf(c_2616,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : double_divide(double_divide(double_divide(identity,X0),double_divide(X1,iPr_def_11(X2))),double_divide(double_divide(identity,double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X0)))),double_divide(X4,iPr_def_11(X1)))) = iPr_def_11(X4),
inference(superposition,[status(thm)],[c_737,c_709]) ).
tcf(c_2618,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,double_divide(double_divide(double_divide(identity,X0),double_divide(X1,iPr_def_11(X2))),double_divide(double_divide(identity,double_divide(double_divide(identity,X3),double_divide(X2,double_divide(X3,X0)))),double_divide(X4,iPr_def_11(X1))))),double_divide(X5,X4))),double_divide(identity,identity)) = X5,
inference(superposition,[status(thm)],[c_737,c_106]) ).
tcf(c_2620,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(double_divide(X0,iPr_def_11(X1)),double_divide(double_divide(identity,double_divide(identity,X2)),iPr_def_11(X0))) = iPr_def_11(double_divide(double_divide(identity,X3),double_divide(X1,double_divide(X3,X2)))),
inference(superposition,[status(thm)],[c_737,c_709]) ).
tcf(c_2622,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(double_divide(double_divide(X0,iPr_def_11(X1)),double_divide(double_divide(identity,double_divide(identity,X2)),iPr_def_11(X0))),double_divide(identity,identity)) = double_divide(double_divide(identity,X3),double_divide(X1,double_divide(X3,X2))),
inference(superposition,[status(thm)],[c_737,c_54]) ).
tcf(c_2672,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(double_divide(identity,double_divide(identity,iPr_def_11(X0))),iPr_def_11(X1)),double_divide(double_divide(identity,double_divide(X1,X0)),double_divide(X2,identity))) = iPr_def_11(X2),
inference(light_normalisation,[status(thm)],[c_2570,c_1022]) ).
tcf(c_2673,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(double_divide(identity,X0),iPr_def_11(X1)),double_divide(double_divide(identity,double_divide(X1,X0)),double_divide(X2,identity))) = iPr_def_11(X2),
inference(demodulation,[status(thm)],[c_2672,c_791,c_2380]) ).
tcf(c_2675,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(double_divide(X0,iPr_def_11(X1)),iPr_def_11(double_divide(iPr_def_11(X2),X0))) = iPr_def_11(double_divide(double_divide(identity,X3),double_divide(X1,double_divide(X3,X2)))),
inference(demodulation,[status(thm)],[c_2620,c_791,c_2383]) ).
tcf(c_2679,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(iPr_def_11(double_divide(iPr_def_11(X0),X1)),double_divide(double_divide(identity,double_divide(X1,double_divide(X0,X2))),double_divide(X3,iPr_def_11(X2)))) = iPr_def_11(X3),
inference(demodulation,[status(thm)],[c_2564,c_791,c_2383]) ).
tcf(c_2699,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(double_divide(double_divide(X0,iPr_def_11(X1)),double_divide(double_divide(identity,double_divide(identity,X2)),iPr_def_11(X0))),identity) = double_divide(double_divide(identity,X3),double_divide(X1,double_divide(X3,X2))),
inference(light_normalisation,[status(thm)],[c_2622,c_241]) ).
tcf(c_2700,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(double_divide(double_divide(X0,iPr_def_11(X1)),iPr_def_11(double_divide(iPr_def_11(X2),X0))),identity) = double_divide(double_divide(identity,X3),double_divide(X1,double_divide(X3,X2))),
inference(demodulation,[status(thm)],[c_2699,c_791,c_2383]) ).
tcf(c_2701,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(identity,X0),double_divide(X1,double_divide(X0,X2))) = iPr_def_12(X1,X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_2700]) ).
tcf(c_2730,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(double_divide(double_divide(identity,X0),double_divide(X1,iPr_def_11(X2))),double_divide(double_divide(identity,iPr_def_12(X2,X0)),double_divide(X3,iPr_def_11(X1)))) = iPr_def_11(X3),
inference(demodulation,[status(thm)],[c_2616,c_2701]) ).
tcf(c_2784,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(identity,iPr_def_11(X0)),double_divide(X1,X0))),double_divide(identity,identity)) = X1,
inference(demodulation,[status(thm)],[c_2618,c_2701,c_2730]) ).
tcf(c_2785,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(identity,double_divide(double_divide(identity,iPr_def_11(X0)),double_divide(X1,X0))),identity) = X1,
inference(light_normalisation,[status(thm)],[c_2784,c_241]) ).
tcf(c_2786,plain,
! [X0: $i] : iPr_def_11(iPr_def_11(X0)) = X0,
inference(demodulation,[status(thm)],[c_2785,c_791,c_1222,c_1229,c_1237,c_1257,c_1559,c_2380]) ).
tcf(c_3131,plain,
! [X0: $i,X1: $i] : iPr_def_11(double_divide(identity,double_divide(double_divide(identity,iPr_def_12(X0,X1)),X0))) = iPr_def_11(X1),
inference(demodulation,[status(thm)],[c_738,c_1257,c_2383,c_2701]) ).
tcf(c_3139,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(iPr_def_11(iPr_def_11(double_divide(identity,double_divide(identity,double_divide(double_divide(identity,iPr_def_12(X0,X1)),X0))))),double_divide(X2,iPr_def_11(X1))) = double_divide(identity,double_divide(X2,identity)),
inference(superposition,[status(thm)],[c_3131,c_1520]) ).
tcf(c_3140,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(double_divide(identity,iPr_def_12(X0,X1)),X0)) = double_divide(iPr_def_11(X1),identity),
inference(superposition,[status(thm)],[c_3131,c_459]) ).
tcf(c_3142,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(identity,double_divide(double_divide(identity,iPr_def_11(X0)),double_divide(X1,double_divide(identity,double_divide(double_divide(identity,iPr_def_12(X2,X0)),X2))))) = iPr_def_11(X1),
inference(superposition,[status(thm)],[c_3131,c_540]) ).
tcf(c_3146,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(double_divide(identity,iPr_def_12(X0,X1)),X0)) = X1,
inference(demodulation,[status(thm)],[c_3140,c_459]) ).
tcf(c_3154,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(double_divide(identity,iPr_def_11(X0)),double_divide(X1,X0))) = iPr_def_11(X1),
inference(demodulation,[status(thm)],[c_3142,c_3146]) ).
tcf(c_3155,plain,
! [X0: $i] : double_divide(X0,identity) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_3154,c_791,c_1257,c_1559,c_2786]) ).
tcf(c_3168,plain,
! [X0: $i,X1: $i] : double_divide(iPr_def_11(iPr_def_11(double_divide(identity,X0))),double_divide(X1,iPr_def_11(X0))) = double_divide(identity,iPr_def_11(X1)),
inference(demodulation,[status(thm)],[c_3139,c_3146,c_3155]) ).
tcf(c_3169,plain,
! [X0: $i] : double_divide(identity,double_divide(X0,identity)) = iPr_def_11(double_divide(identity,X0)),
inference(demodulation,[status(thm)],[c_3168,c_1257,c_1564,c_1912]) ).
tcf(c_3187,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(X1,iPr_def_11(X0))) = iPr_def_11(X2),
inference(demodulation,[status(thm)],[c_741,c_791,c_2786]) ).
tcf(c_3198,plain,
! [X0: $i,X1: $i] : double_divide(iPr_def_11(X0),double_divide(double_divide(X1,identity),iPr_def_11(identity))) = iPr_def_11(double_divide(X0,iPr_def_11(X1))),
inference(superposition,[status(thm)],[c_1853,c_3187]) ).
tcf(c_3205,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,identity),double_divide(X1,iPr_def_11(X0))) = iPr_def_11(double_divide(X1,identity)),
inference(superposition,[status(thm)],[c_55,c_3187]) ).
tcf(c_3208,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(X0,iPr_def_11(X1)),double_divide(X2,iPr_def_11(X0))) = iPr_def_11(double_divide(identity,double_divide(X1,double_divide(identity,X2)))),
inference(superposition,[status(thm)],[c_713,c_3187]) ).
tcf(c_3223,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(X0,iPr_def_11(X1)),double_divide(identity,iPr_def_11(X0))) = iPr_def_11(double_divide(double_divide(X2,identity),double_divide(X1,iPr_def_11(X2)))),
inference(superposition,[status(thm)],[c_1853,c_3187]) ).
tcf(c_3224,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(double_divide(double_divide(iPr_def_11(iPr_def_11(iPr_def_11(X0))),double_divide(X1,double_divide(identity,X0))),identity)) = double_divide(double_divide(X2,X1),double_divide(identity,iPr_def_11(X2))),
inference(superposition,[status(thm)],[c_2013,c_3187]) ).
tcf(c_3225,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(X0,identity),double_divide(double_divide(X1,X2),iPr_def_11(X0))) = iPr_def_11(double_divide(iPr_def_11(iPr_def_11(iPr_def_11(X2))),iPr_def_11(X1))),
inference(superposition,[status(thm)],[c_2301,c_3187]) ).
tcf(c_3235,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(identity,double_divide(double_divide(identity,iPr_def_11(double_divide(X0,iPr_def_11(X1)))),iPr_def_11(X2))) = iPr_def_11(double_divide(X1,double_divide(X0,X2))),
inference(superposition,[status(thm)],[c_3187,c_540]) ).
tcf(c_3248,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(double_divide(iPr_def_11(iPr_def_11(iPr_def_11(iPr_def_11(X0)))),iPr_def_11(X1)),identity)) = double_divide(X0,double_divide(identity,X1)),
inference(superposition,[status(thm)],[c_3187,c_2013]) ).
tcf(c_3269,plain,
! [X0: $i,X1: $i] : double_divide(iPr_def_11(X0),double_divide(X1,iPr_def_11(X0))) = X1,
inference(demodulation,[status(thm)],[c_3205,c_451,c_3155]) ).
tcf(c_3284,plain,
! [X0: $i,X1: $i] : double_divide(iPr_def_11(X0),double_divide(double_divide(X1,identity),identity)) = iPr_def_11(double_divide(X0,iPr_def_11(X1))),
inference(light_normalisation,[status(thm)],[c_3198,c_1022]) ).
tcf(c_3285,plain,
! [X0: $i,X1: $i] : iPr_def_11(double_divide(X0,double_divide(identity,X1))) = iPr_def_11(double_divide(X0,iPr_def_11(X1))),
inference(demodulation,[status(thm)],[c_3284,c_1229,c_2383]) ).
tcf(c_3301,plain,
! [X0: $i,X1: $i] : iPr_def_11(double_divide(double_divide(identity,X0),X1)) = double_divide(X0,double_divide(identity,X1)),
inference(demodulation,[status(thm)],[c_3248,c_1257,c_1564,c_2380,c_2383,c_3155,c_3169]) ).
tcf(c_3318,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(double_divide(identity,double_divide(double_divide(identity,double_divide(X0,iPr_def_11(X1))),X2))) = iPr_def_11(double_divide(X1,double_divide(X0,X2))),
inference(demodulation,[status(thm)],[c_3235,c_1257,c_2383]) ).
tcf(c_3320,plain,
! [X0: $i,X1: $i] : iPr_def_11(double_divide(identity,double_divide(X0,X1))) = double_divide(X1,X0),
inference(demodulation,[status(thm)],[c_3225,c_1912,c_2383,c_2786,c_3169]) ).
tcf(c_3322,plain,
! [X0: $i,X1: $i] : iPr_def_11(double_divide(double_divide(X0,identity),double_divide(X1,iPr_def_11(X0)))) = double_divide(double_divide(identity,identity),X1),
inference(demodulation,[status(thm)],[c_3223,c_3208,c_3320]) ).
tcf(c_3323,plain,
! [X0: $i,X1: $i] : iPr_def_11(double_divide(double_divide(X0,identity),double_divide(X1,iPr_def_11(X0)))) = double_divide(identity,X1),
inference(light_normalisation,[status(thm)],[c_3322,c_241]) ).
tcf(c_3324,plain,
! [X0: $i] : double_divide(identity,X0) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_3323,c_1564,c_1912,c_3155,c_3169]) ).
tcf(c_3357,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(double_divide(double_divide(iPr_def_11(iPr_def_11(iPr_def_11(X0))),double_divide(X1,iPr_def_11(X0))),identity)) = double_divide(double_divide(X2,X1),iPr_def_11(iPr_def_11(X2))),
inference(demodulation,[status(thm)],[c_3224,c_3324]) ).
tcf(c_3358,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(identity,X0),double_divide(X1,iPr_def_11(X0))) = double_divide(double_divide(X2,X1),X2),
inference(demodulation,[status(thm)],[c_3357,c_451,c_2380,c_2786]) ).
tcf(c_3359,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,X1),X0) = iPr_def_13(X1),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_3358]) ).
tcf(c_3360,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(identity,X0),double_divide(X1,iPr_def_11(X0))) = iPr_def_13(X1),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_3358]) ).
tcf(c_3363,plain,
! [X0: $i] : iPr_def_13(X0) = X0,
inference(demodulation,[status(thm)],[c_3360,c_3269,c_3324]) ).
tcf(c_3725,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,iPr_def_11(X1)),iPr_def_11(X1)) = X0,
inference(demodulation,[status(thm)],[c_744,c_2786,c_3324]) ).
tcf(c_3734,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,X1),X1) = X0,
inference(superposition,[status(thm)],[c_451,c_3725]) ).
tcf(c_3740,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(double_divide(identity,iPr_def_11(iPr_def_11(X0))),X1)) = iPr_def_11(double_divide(X1,iPr_def_11(X0))),
inference(superposition,[status(thm)],[c_3725,c_540]) ).
tcf(c_3749,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(double_divide(X0,identity),X1)) = iPr_def_11(double_divide(X1,iPr_def_11(X0))),
inference(superposition,[status(thm)],[c_3725,c_1853]) ).
tcf(c_3758,plain,
! [X0: $i,X1: $i] : iPr_def_11(double_divide(iPr_def_11(X0),X1)) = iPr_def_11(double_divide(X1,iPr_def_11(X0))),
inference(demodulation,[status(thm)],[c_3749,c_3155,c_3324]) ).
tcf(c_3763,plain,
! [X0: $i,X1: $i] : iPr_def_11(double_divide(X0,iPr_def_11(X1))) = double_divide(X1,iPr_def_11(X0)),
inference(demodulation,[status(thm)],[c_3740,c_2786,c_3301,c_3324]) ).
tcf(c_3785,plain,
( ( double_divide(double_divide(a4,b4),identity) != double_divide(double_divide(b4,a4),identity) )
| ( double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity) != double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity) ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_254,c_3734]) ).
tcf(c_3786,plain,
( ( iPr_def_11(double_divide(a4,b4)) != iPr_def_11(double_divide(b4,a4)) )
| ( iPr_def_11(double_divide(iPr_def_11(double_divide(c3,b3)),a3)) != iPr_def_11(double_divide(c3,iPr_def_11(double_divide(b3,a3)))) ) ),
inference(demodulation,[status(thm)],[c_3785,c_3155]) ).
tcf(c_3825,plain,
( ( iPr_def_11(double_divide(a4,b4)) != iPr_def_11(double_divide(b4,a4)) )
| ( double_divide(double_divide(b3,a3),iPr_def_11(c3)) != double_divide(double_divide(c3,b3),iPr_def_11(a3)) ) ),
inference(demodulation,[status(thm)],[c_3786,c_3758,c_3763]) ).
tcf(c_3826,plain,
! [X0: $i] : iPr_def_12(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_777,c_1222,c_2701,c_2786,c_3169,c_3324]) ).
tcf(c_3831,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(X0,double_divide(iPr_def_11(X1),double_divide(X2,double_divide(X1,X0)))) = iPr_def_11(X2),
inference(demodulation,[status(thm)],[c_796,c_1222,c_2786,c_3169,c_3324]) ).
tcf(c_3848,plain,
! [X0: $i,X1: $i] : double_divide(X0,double_divide(iPr_def_11(X1),identity)) = iPr_def_11(iPr_def_11(double_divide(X1,X0))),
inference(superposition,[status(thm)],[c_513,c_3831]) ).
tcf(c_3937,plain,
! [X0: $i,X1: $i] : double_divide(X0,X1) = double_divide(X1,X0),
inference(demodulation,[status(thm)],[c_3848,c_459,c_2786]) ).
tcf(c_4203,plain,
! [X0: $i,X1: $i] : double_divide(iPr_def_11(X0),iPr_def_12(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_832,c_1222,c_1257,c_2701,c_3169,c_3320,c_3937]) ).
tcf(c_4221,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(X0,X1),double_divide(iPr_def_11(X2),iPr_def_11(X0))) = iPr_def_11(iPr_def_12(X2,X1)),
inference(superposition,[status(thm)],[c_4203,c_3187]) ).
tcf(c_4233,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(X0,X1),iPr_def_11(double_divide(X2,X0))) = iPr_def_11(iPr_def_12(X2,X1)),
inference(demodulation,[status(thm)],[c_4221,c_2383]) ).
tcf(c_4290,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(X0,X1),iPr_def_12(iPr_def_11(X2),double_divide(X2,X1))) = X0,
inference(demodulation,[status(thm)],[c_980,c_1222,c_2383,c_2701,c_2786,c_3169,c_3301,c_3320,c_3324,c_3937]) ).
tcf(c_4307,plain,
! [X0: $i,X1: $i] : double_divide(identity,iPr_def_12(iPr_def_11(X0),double_divide(X0,X1))) = iPr_def_11(X1),
inference(superposition,[status(thm)],[c_513,c_4290]) ).
tcf(c_4353,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(iPr_def_12(iPr_def_11(X0),double_divide(X0,X1)),double_divide(iPr_def_11(double_divide(X2,X1)),double_divide(X3,X2))) = iPr_def_11(X3),
inference(superposition,[status(thm)],[c_4290,c_3831]) ).
tcf(c_4356,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(identity,double_divide(double_divide(identity,iPr_def_11(iPr_def_12(iPr_def_11(X0),double_divide(X0,X1)))),X2)) = iPr_def_11(double_divide(X2,X1)),
inference(superposition,[status(thm)],[c_4290,c_540]) ).
tcf(c_4380,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_12(iPr_def_11(X0),double_divide(X0,X1))) = iPr_def_11(X1),
inference(demodulation,[status(thm)],[c_4307,c_3324]) ).
tcf(c_4427,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(double_divide(identity,iPr_def_11(X0)),X1)) = iPr_def_11(double_divide(X1,X0)),
inference(demodulation,[status(thm)],[c_4356,c_4380]) ).
tcf(c_4428,plain,
! [X0: $i,X1: $i] : iPr_def_11(double_divide(X0,X1)) = iPr_def_11(double_divide(X1,X0)),
inference(demodulation,[status(thm)],[c_4427,c_2383,c_3301,c_3324]) ).
tcf(c_4526,plain,
double_divide(double_divide(b3,a3),iPr_def_11(c3)) != double_divide(double_divide(c3,b3),iPr_def_11(a3)),
inference(backward_subsumption_resolution,[status(thm)],[c_3825,c_4428]) ).
tcf(c_4527,plain,
double_divide(iPr_def_11(a3),double_divide(b3,c3)) != double_divide(iPr_def_11(c3),double_divide(b3,a3)),
inference(demodulation,[status(thm)],[c_4526,c_3937]) ).
tcf(c_4706,plain,
! [X0: $i,X1: $i] : double_divide(iPr_def_11(X0),double_divide(iPr_def_11(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_1392,c_2786,c_3155,c_3324]) ).
tcf(c_4716,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(X0,double_divide(identity,iPr_def_11(X1)))) = double_divide(iPr_def_11(X1),iPr_def_11(X0)),
inference(superposition,[status(thm)],[c_713,c_4706]) ).
tcf(c_4719,plain,
! [X0: $i,X1: $i] : double_divide(iPr_def_11(iPr_def_11(double_divide(identity,X0))),double_divide(identity,double_divide(X1,identity))) = double_divide(X1,iPr_def_11(X0)),
inference(superposition,[status(thm)],[c_1520,c_4706]) ).
tcf(c_4721,plain,
! [X0: $i,X1: $i] : double_divide(iPr_def_11(X0),X1) = iPr_def_12(X0,X1),
inference(superposition,[status(thm)],[c_4203,c_4706]) ).
tcf(c_4767,plain,
! [X0: $i,X1: $i] : double_divide(identity,double_divide(X0,double_divide(identity,iPr_def_11(X1)))) = iPr_def_12(X1,iPr_def_11(X0)),
inference(demodulation,[status(thm)],[c_4716,c_4721]) ).
tcf(c_4768,plain,
! [X0: $i,X1: $i] : iPr_def_11(double_divide(X0,X1)) = iPr_def_12(X0,iPr_def_11(X1)),
inference(demodulation,[status(thm)],[c_4767,c_2383,c_3285,c_3324,c_3763]) ).
tcf(c_4789,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_11(double_divide(identity,X0)),double_divide(identity,double_divide(X1,identity))) = double_divide(X1,iPr_def_11(X0)),
inference(demodulation,[status(thm)],[c_4719,c_4721]) ).
tcf(c_4790,plain,
! [X0: $i,X1: $i] : double_divide(X0,iPr_def_11(X1)) = iPr_def_12(X1,X0),
inference(demodulation,[status(thm)],[c_4789,c_2786,c_3169,c_3324]) ).
tcf(c_4820,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_12(X0,X1),X0) = iPr_def_11(X1),
inference(demodulation,[status(thm)],[c_1410,c_2786,c_3155,c_3301,c_3324,c_4721,c_4790]) ).
tcf(c_4825,plain,
! [X0: $i] : iPr_def_12(identity,X0) = iPr_def_11(X0),
inference(superposition,[status(thm)],[c_4820,c_3826]) ).
tcf(c_4834,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_12(X0,iPr_def_12(X0,X1))) = iPr_def_11(X1),
inference(demodulation,[status(thm)],[c_1423,c_2786,c_3155,c_3324,c_4721]) ).
tcf(c_4848,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,iPr_def_12(X0,X1)) = double_divide(iPr_def_11(X1),identity),
inference(superposition,[status(thm)],[c_4834,c_459]) ).
tcf(c_4855,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,iPr_def_12(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_4848,c_459]) ).
tcf(c_4890,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(iPr_def_12(X0,X1),double_divide(X0,double_divide(X1,X2))) = iPr_def_11(X2),
inference(demodulation,[status(thm)],[c_1574,c_1651,c_2786,c_3169,c_3324,c_4790]) ).
tcf(c_4901,plain,
! [X0: $i,X1: $i] : double_divide(iPr_def_12(X0,identity),iPr_def_11(X1)) = iPr_def_11(double_divide(X1,double_divide(identity,X0))),
inference(superposition,[status(thm)],[c_713,c_4890]) ).
tcf(c_4934,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(iPr_def_12(X0,double_divide(X1,X2)),double_divide(X0,identity)) = iPr_def_11(double_divide(iPr_def_11(iPr_def_11(iPr_def_11(X2))),iPr_def_11(X1))),
inference(superposition,[status(thm)],[c_2301,c_4890]) ).
tcf(c_4965,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(double_divide(X0,iPr_def_11(X1)),double_divide(iPr_def_12(X2,X3),iPr_def_11(X0))) = iPr_def_11(double_divide(X2,double_divide(X3,X1))),
inference(superposition,[status(thm)],[c_4890,c_3187]) ).
tcf(c_4987,plain,
! [X0: $i,X1: $i] : iPr_def_11(double_divide(X0,double_divide(identity,X1))) = double_divide(X1,iPr_def_11(X0)),
inference(light_normalisation,[status(thm)],[c_4901,c_3826]) ).
tcf(c_4988,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_12(X0,X1)) = iPr_def_12(X1,X0),
inference(demodulation,[status(thm)],[c_4987,c_3324,c_4790]) ).
tcf(c_5036,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(double_divide(X0,double_divide(X1,X2))) = iPr_def_12(iPr_def_12(X0,X1),X2),
inference(demodulation,[status(thm)],[c_4965,c_3208,c_3320,c_3324,c_4721]) ).
tcf(c_5057,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_11(X0),X1) = double_divide(X1,X0),
inference(demodulation,[status(thm)],[c_4934,c_2380,c_3155,c_3324,c_3763,c_3937,c_4721,c_4790,c_4855]) ).
tcf(c_5187,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(double_divide(X0,X1),iPr_def_12(double_divide(X1,X0),X2)) = X2,
inference(demodulation,[status(thm)],[c_1672,c_3155,c_3169,c_3285,c_3320,c_3324,c_3763,c_4768,c_4790]) ).
tcf(c_5248,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_12(double_divide(X0,X1),X2)) = iPr_def_12(X2,double_divide(X1,X0)),
inference(superposition,[status(thm)],[c_5187,c_4820]) ).
tcf(c_5249,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(iPr_def_11(double_divide(X0,X1)),X2) = iPr_def_12(double_divide(X1,X0),X2),
inference(superposition,[status(thm)],[c_5187,c_4203]) ).
tcf(c_5260,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(double_divide(X0,X1),X2) = iPr_def_12(double_divide(X1,X0),X2),
inference(demodulation,[status(thm)],[c_5249,c_4721]) ).
tcf(c_5262,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(X0,double_divide(X1,X2)) = iPr_def_12(X0,double_divide(X2,X1)),
inference(demodulation,[status(thm)],[c_5248,c_4988]) ).
tcf(c_5345,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(X0,double_divide(X1,double_divide(X2,iPr_def_12(X1,X0)))) = iPr_def_11(X2),
inference(demodulation,[status(thm)],[c_2100,c_4721,c_4790,c_5057]) ).
tcf(c_5350,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(X0,X1),double_divide(iPr_def_11(X0),X2)) = iPr_def_11(double_divide(X2,X1)),
inference(superposition,[status(thm)],[c_4290,c_5345]) ).
tcf(c_5401,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(iPr_def_12(X0,X1),iPr_def_11(X2)) = iPr_def_11(double_divide(X2,iPr_def_12(X1,X0))),
inference(superposition,[status(thm)],[c_5345,c_4890]) ).
tcf(c_5413,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(double_divide(X0,iPr_def_12(X1,X2))) = iPr_def_12(X0,iPr_def_12(X2,X1)),
inference(demodulation,[status(thm)],[c_5401,c_4790]) ).
tcf(c_5418,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(X0,X1),iPr_def_12(X0,X2)) = iPr_def_11(double_divide(X2,X1)),
inference(demodulation,[status(thm)],[c_5350,c_4721]) ).
tcf(c_5520,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(X0,iPr_def_12(iPr_def_12(iPr_def_12(X1,X0),X2),X1)) = X2,
inference(demodulation,[status(thm)],[c_2290,c_3169,c_3301,c_3318,c_3324,c_4790,c_5036]) ).
tcf(c_5559,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(double_divide(X0,X1),double_divide(X2,iPr_def_11(X0))) = iPr_def_11(iPr_def_12(iPr_def_12(iPr_def_12(X3,X2),X1),X3)),
inference(superposition,[status(thm)],[c_5520,c_3187]) ).
tcf(c_5582,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(X0,iPr_def_12(iPr_def_12(X0,X1),X2)) = iPr_def_11(double_divide(X1,X2)),
inference(demodulation,[status(thm)],[c_5559,c_4790,c_4988,c_5418]) ).
tcf(c_5671,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(X0,double_divide(iPr_def_12(X1,X0),double_divide(X2,X1))) = iPr_def_11(X2),
inference(demodulation,[status(thm)],[c_2554,c_3285,c_3324,c_3763,c_4721,c_4790,c_5057]) ).
tcf(c_5701,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(X0,double_divide(iPr_def_12(double_divide(X1,iPr_def_11(X2)),X0),iPr_def_11(X3))) = iPr_def_11(double_divide(X2,double_divide(X1,X3))),
inference(superposition,[status(thm)],[c_3187,c_5671]) ).
tcf(c_5704,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(X0,double_divide(iPr_def_12(iPr_def_12(iPr_def_11(X1),double_divide(X1,X2)),X0),X3)) = iPr_def_11(double_divide(X3,X2)),
inference(superposition,[status(thm)],[c_4290,c_5671]) ).
tcf(c_5714,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(iPr_def_12(X0,X1),double_divide(X2,X0)) = double_divide(iPr_def_11(X1),iPr_def_11(X2)),
inference(superposition,[status(thm)],[c_5671,c_4203]) ).
tcf(c_5717,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(iPr_def_12(X0,iPr_def_12(X1,X2)),double_divide(X3,X0)) = double_divide(X2,iPr_def_12(iPr_def_11(X3),X1)),
inference(superposition,[status(thm)],[c_5671,c_5520]) ).
tcf(c_5725,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(iPr_def_12(X0,X1),double_divide(X2,X0)) = iPr_def_11(double_divide(X1,X2)),
inference(demodulation,[status(thm)],[c_5714,c_4721,c_4768]) ).
tcf(c_5735,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(X0,iPr_def_12(iPr_def_11(X1),X2)) = iPr_def_11(double_divide(iPr_def_12(X2,X0),X1)),
inference(demodulation,[status(thm)],[c_5717,c_5725]) ).
tcf(c_5736,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(double_divide(iPr_def_12(X0,X1),X2)) = double_divide(X1,double_divide(X0,X2)),
inference(demodulation,[status(thm)],[c_5735,c_5057]) ).
tcf(c_5761,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(X0,double_divide(iPr_def_12(X1,X0),X2)) = iPr_def_11(double_divide(X2,X1)),
inference(demodulation,[status(thm)],[c_5704,c_3359,c_3363,c_5057]) ).
tcf(c_5771,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(double_divide(iPr_def_11(X0),double_divide(X1,iPr_def_11(X2)))) = iPr_def_11(double_divide(X2,double_divide(X1,X0))),
inference(demodulation,[status(thm)],[c_5701,c_5761]) ).
tcf(c_5772,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(double_divide(double_divide(X0,X1),X2)) = iPr_def_12(iPr_def_12(X2,X0),X1),
inference(demodulation,[status(thm)],[c_5771,c_4768,c_5036,c_5057]) ).
tcf(c_5815,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(double_divide(X0,X1),iPr_def_12(iPr_def_12(X2,X0),X1)) = iPr_def_11(X2),
inference(demodulation,[status(thm)],[c_2673,c_3155,c_3324,c_4721,c_4768,c_4790,c_5772]) ).
tcf(c_5861,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_12(iPr_def_12(X0,X1),X2)) = iPr_def_12(iPr_def_11(X0),double_divide(X1,X2)),
inference(superposition,[status(thm)],[c_5815,c_4820]) ).
tcf(c_5876,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(double_divide(X0,X1),X2) = iPr_def_12(X1,iPr_def_12(X2,X0)),
inference(demodulation,[status(thm)],[c_5861,c_4988,c_5057]) ).
tcf(c_5959,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(X0,iPr_def_12(iPr_def_12(X1,X0),X2)) = iPr_def_12(X2,X1),
inference(demodulation,[status(thm)],[c_2675,c_3301,c_3324,c_4233,c_4721,c_4988,c_5036,c_5057]) ).
tcf(c_5966,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(X0,iPr_def_12(iPr_def_11(X1),X2)) = iPr_def_12(X2,iPr_def_12(X0,X1)),
inference(superposition,[status(thm)],[c_4820,c_5959]) ).
tcf(c_6002,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(iPr_def_12(X0,X1),double_divide(X0,iPr_def_12(X2,X3))) = iPr_def_11(iPr_def_12(iPr_def_12(X3,X1),X2)),
inference(superposition,[status(thm)],[c_5959,c_4890]) ).
tcf(c_6011,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(X0,double_divide(X1,X2)) = iPr_def_12(X1,iPr_def_12(X0,X2)),
inference(demodulation,[status(thm)],[c_5966,c_5057]) ).
tcf(c_6020,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(X0,iPr_def_12(iPr_def_12(X0,X1),iPr_def_12(X2,X3))) = iPr_def_11(iPr_def_12(iPr_def_12(X3,X1),X2)),
inference(demodulation,[status(thm)],[c_6002,c_6011]) ).
tcf(c_6021,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(X0,iPr_def_12(X1,X2)) = iPr_def_12(X2,iPr_def_12(X1,X0)),
inference(demodulation,[status(thm)],[c_6020,c_4988,c_5413,c_5582]) ).
tcf(c_6161,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(iPr_def_12(X0,X1),iPr_def_12(iPr_def_12(X0,iPr_def_12(X1,X2)),iPr_def_12(X2,X3))) = iPr_def_11(X3),
inference(demodulation,[status(thm)],[c_2679,c_4721,c_4790,c_4825,c_4988,c_5876,c_6011,c_6021]) ).
tcf(c_6195,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_11(iPr_def_12(iPr_def_12(X0,iPr_def_12(X1,X2)),iPr_def_12(X2,X3))) = iPr_def_12(iPr_def_11(X3),iPr_def_12(X0,X1)),
inference(superposition,[status(thm)],[c_6161,c_4820]) ).
tcf(c_6201,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(iPr_def_12(X0,iPr_def_12(X1,X2)),iPr_def_12(X2,X3)) = double_divide(X1,iPr_def_12(iPr_def_11(X3),X0)),
inference(superposition,[status(thm)],[c_6161,c_5520]) ).
tcf(c_6209,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(iPr_def_12(X0,iPr_def_12(X1,X2)),iPr_def_12(X2,X3)) = iPr_def_12(X0,iPr_def_12(X1,X3)),
inference(demodulation,[status(thm)],[c_6201,c_5057,c_6011]) ).
tcf(c_6218,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_12(X0,iPr_def_12(X1,X2))) = iPr_def_12(iPr_def_11(X2),iPr_def_12(X0,X1)),
inference(demodulation,[status(thm)],[c_6195,c_6209]) ).
tcf(c_6219,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(iPr_def_12(X0,X1),X2) = iPr_def_12(iPr_def_12(X1,X2),X0),
inference(demodulation,[status(thm)],[c_6218,c_4988,c_5057]) ).
tcf(c_7952,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(double_divide(X0,X1),iPr_def_12(iPr_def_12(double_divide(X1,X2),X3),double_divide(X3,X2))) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_4353,c_4768,c_5260,c_5736,c_5772,c_5876,c_6219]) ).
tcf(c_8074,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : double_divide(iPr_def_12(iPr_def_12(double_divide(X0,X1),X2),double_divide(X2,X1)),iPr_def_12(iPr_def_11(X3),X4)) = iPr_def_12(X4,double_divide(X3,X0)),
inference(superposition,[status(thm)],[c_7952,c_5959]) ).
tcf(c_8089,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(iPr_def_12(double_divide(X0,X1),X2),double_divide(X2,X1)) = iPr_def_12(double_divide(X0,X3),iPr_def_11(X3)),
inference(superposition,[status(thm)],[c_7952,c_5187]) ).
tcf(c_8117,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(iPr_def_12(double_divide(X0,X1),X2),double_divide(X2,X1)) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_8089,c_4768,c_4820,c_5772]) ).
tcf(c_8142,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(iPr_def_11(X0),iPr_def_12(iPr_def_11(X1),X2)) = iPr_def_12(X2,double_divide(X1,X0)),
inference(demodulation,[status(thm)],[c_8074,c_8117]) ).
tcf(c_8143,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(X0,double_divide(X1,X2)) = iPr_def_12(X1,double_divide(X2,X0)),
inference(demodulation,[status(thm)],[c_8142,c_4721,c_5057]) ).
tcf(c_8566,plain,
double_divide(iPr_def_11(a3),double_divide(b3,c3)) != iPr_def_12(c3,double_divide(b3,a3)),
inference(superposition,[status(thm)],[c_4721,c_4527]) ).
tcf(c_8603,plain,
iPr_def_12(a3,double_divide(b3,c3)) != iPr_def_12(c3,double_divide(b3,a3)),
inference(demodulation,[status(thm)],[c_8566,c_4721]) ).
tcf(c_8604,plain,
$false,
inference(ground_joinability,[status(thm)],[c_8603,c_5262,c_8143]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP103-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n008.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 13:32:55 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 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.10/0.41
% 0.10/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.41
% 0.10/0.41 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 8.54/1.64 % SZS status Started for theBenchmark.p
% 8.54/1.64 % SZS status Unsatisfiable for theBenchmark.p
% 8.54/1.64
% 8.54/1.64 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.54/1.64
% 8.54/1.64 % ------ iProver source info
% 8.54/1.64
% 8.54/1.64 % git: date: 2026-07-19 20:42:38 +0200
% 8.54/1.64 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.54/1.64 % git: non_committed_changes: false
% 8.54/1.64
% 8.54/1.64 % ------ Parsing...% successful
% 8.54/1.64
% 8.54/1.64
% 8.54/1.64 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 8.54/1.64
% 8.54/1.64 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 8.54/1.64
% 8.54/1.64 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 8.54/1.64
% 8.54/1.64 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 8.54/1.64 % ------ Proving...
% 8.54/1.64 % ------ Problem Properties
% 8.54/1.64
% 8.54/1.64 %
% 8.54/1.64 % clauses 3
% 8.54/1.64 % conjectures 1
% 8.54/1.64 % EPR 0
% 8.54/1.64 % Horn 3
% 8.54/1.64 % unary 2
% 8.54/1.64 % binary 0
% 8.54/1.64 % lits 6
% 8.54/1.64 % lits eq 6
% 8.54/1.64 % fd_pure 0
% 8.54/1.64 % fd_pseudo 0
% 8.54/1.64 % fd_cond 0
% 8.54/1.64 % fd_pseudo_cond 0
% 8.54/1.64 % AC symbols 0
% 8.54/1.64
% 8.54/1.64 % ------ Input Options Time Limit: Unbounded
% 8.54/1.64
% 8.54/1.64
% 8.54/1.64 % ------
% 8.54/1.64 % Current options:
% 8.54/1.64 % ------
% 8.54/1.64
% 8.54/1.64
% 8.54/1.64 %
% 8.54/1.64
% 8.54/1.64 % ------ Proving...
% 8.54/1.64 %
% 8.54/1.64
% 8.54/1.64 % SZS status Unsatisfiable for theBenchmark.p
% 8.54/1.64
% 8.54/1.64 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.54/1.65
% 8.54/1.65
%------------------------------------------------------------------------------