%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP501-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:34:25 PM UTC 2026
% Result : Unsatisfiable 13.02s 2.77s
% Output : CNFRefutation 13.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 3
% Syntax : Number of formulae : 157 ( 157 unt; 0 def)
% Number of atoms : 597 ( 156 equ)
% Maximal formula atoms : 1 ( 3 avg)
% Number of connectives : 7 ( 7 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 5 usr; 2 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 424 ( 0 sgn 424 !; 0 ?; 418 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,double_divide(X1,X2))),double_divide(X3,double_divide(X1,X3))))) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,axiom,
! [X0,X1] : multiply(X0,X1) = inverse(double_divide(X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiply) ).
fof(f3,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms_3) ).
fof(f4,plain,
inverse(double_divide(c3,inverse(double_divide(b3,a3)))) != inverse(double_divide(inverse(double_divide(c3,b3)),a3)),
inference(definition_unfolding,[],[f3,f2,f2,f2,f2]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,double_divide(X1,X2))),double_divide(X3,double_divide(X1,X3))))) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_53,negated_conjecture,
inverse(double_divide(inverse(double_divide(c3,b3)),a3)) != inverse(double_divide(c3,inverse(double_divide(b3,a3)))),
inference(cnf_transformation,[],[f4]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,X1)),double_divide(X2,double_divide(inverse(X3),X2))))) = inverse(double_divide(inverse(double_divide(X3,double_divide(X4,X1))),double_divide(X5,double_divide(X4,X5)))),
inference(superposition,[status(thm)],[c_52,c_52]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,double_divide(inverse(X1),X2))),double_divide(inverse(double_divide(inverse(double_divide(X1,double_divide(X3,X4))),double_divide(X5,double_divide(X3,X5)))),X4)))) = X2,
inference(superposition,[status(thm)],[c_52,c_52]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(double_divide(inverse(double_divide(X0,double_divide(X1,X2))),double_divide(X3,double_divide(X1,X3)))) = iPr_def_10(X0,X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_61]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,X1)),double_divide(X2,double_divide(inverse(X3),X2))))) = iPr_def_10(X3,X1),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_61]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i] : double_divide(inverse(X0),iPr_def_10(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_52,c_63]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(double_divide(inverse(double_divide(X0,X1)),double_divide(X2,double_divide(inverse(X3),X2)))) = iPr_def_10(X0,iPr_def_10(X3,X1)),
inference(superposition,[status(thm)],[c_65,c_63]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(double_divide(iPr_def_10(X0,X1),double_divide(X2,double_divide(X3,X2)))) = iPr_def_10(inverse(double_divide(X0,double_divide(X4,X1))),double_divide(X4,X3)),
inference(superposition,[status(thm)],[c_63,c_63]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(inverse(X0),iPr_def_10(X0,X1)) = iPr_def_10(X2,double_divide(inverse(X2),X1)),
inference(superposition,[status(thm)],[c_63,c_64]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : double_divide(inverse(inverse(double_divide(X0,double_divide(X1,X2)))),inverse(double_divide(iPr_def_10(X0,X2),double_divide(X3,double_divide(inverse(X4),X3))))) = iPr_def_10(X4,double_divide(X5,double_divide(X1,X5))),
inference(superposition,[status(thm)],[c_63,c_64]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(inverse(inverse(X0)),inverse(double_divide(inverse(X1),double_divide(X2,double_divide(inverse(X3),X2))))) = iPr_def_10(X3,iPr_def_10(X0,X1)),
inference(superposition,[status(thm)],[c_65,c_64]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,X1)),double_divide(iPr_def_10(X2,X3),X3)))) = iPr_def_10(X2,X1),
inference(superposition,[status(thm)],[c_65,c_64]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : double_divide(inverse(inverse(double_divide(X0,double_divide(X1,X2)))),inverse(double_divide(iPr_def_10(X0,X2),double_divide(inverse(double_divide(inverse(double_divide(X3,double_divide(X4,X5))),double_divide(X6,double_divide(X4,X6)))),X5)))) = double_divide(X1,inverse(X3)),
inference(superposition,[status(thm)],[c_63,c_62]) ).
tcf(c_114,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,double_divide(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_82,c_65]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : double_divide(inverse(inverse(double_divide(X0,double_divide(X1,X2)))),inverse(double_divide(iPr_def_10(X0,X2),double_divide(iPr_def_10(X3,X4),X4)))) = double_divide(X1,inverse(X3)),
inference(demodulation,[status(thm)],[c_94,c_63]) ).
tcf(c_245,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,double_divide(inverse(inverse(double_divide(X1,X2))),X3))),double_divide(inverse(double_divide(iPr_def_10(X1,iPr_def_10(X4,X2)),double_divide(X5,double_divide(X6,X5)))),double_divide(inverse(X4),X6))))) = X3,
inference(superposition,[status(thm)],[c_77,c_62]) ).
tcf(c_281,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,iPr_def_10(X1,X2))),double_divide(inverse(double_divide(inverse(double_divide(X3,double_divide(X4,X5))),double_divide(X6,double_divide(X4,X6)))),X5)))) = inverse(double_divide(inverse(double_divide(X3,X2)),double_divide(iPr_def_10(X1,X7),X7))),
inference(superposition,[status(thm)],[c_87,c_62]) ).
tcf(c_284,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(double_divide(inverse(double_divide(X0,X1)),double_divide(iPr_def_10(X2,X3),X3))) = iPr_def_10(X0,iPr_def_10(X2,X1)),
inference(superposition,[status(thm)],[c_87,c_114]) ).
tcf(c_310,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(inverse(inverse(X0)),iPr_def_10(X1,iPr_def_10(X2,X3))) = iPr_def_10(X2,iPr_def_10(X0,double_divide(X1,X3))),
inference(superposition,[status(thm)],[c_77,c_85]) ).
tcf(c_328,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,iPr_def_10(X1,iPr_def_10(X2,X3)))),double_divide(inverse(double_divide(inverse(double_divide(inverse(X2),double_divide(X4,X5))),double_divide(X6,double_divide(X4,X6)))),X5)))) = inverse(double_divide(inverse(X3),double_divide(X7,double_divide(inverse(X1),X7)))),
inference(superposition,[status(thm)],[c_85,c_62]) ).
tcf(c_348,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(double_divide(iPr_def_10(X0,iPr_def_10(X1,X2)),double_divide(X3,double_divide(X4,X3)))) = iPr_def_10(inverse(double_divide(X0,X2)),double_divide(inverse(X1),X4)),
inference(superposition,[status(thm)],[c_65,c_80]) ).
tcf(c_353,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(double_divide(iPr_def_10(X0,X1),double_divide(X2,double_divide(iPr_def_10(X3,X4),X2)))) = iPr_def_10(inverse(double_divide(X0,double_divide(inverse(X3),X1))),X4),
inference(superposition,[status(thm)],[c_65,c_80]) ).
tcf(c_378,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : double_divide(inverse(inverse(double_divide(X0,double_divide(X1,X2)))),inverse(double_divide(iPr_def_10(X0,X2),double_divide(X3,double_divide(X4,X3))))) = double_divide(X1,X4),
inference(superposition,[status(thm)],[c_80,c_65]) ).
tcf(c_379,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(double_divide(iPr_def_10(X0,X1),double_divide(X2,double_divide(X3,X2)))) = inverse(double_divide(iPr_def_10(X0,X1),double_divide(X4,double_divide(X3,X4)))),
inference(superposition,[status(thm)],[c_80,c_80]) ).
tcf(c_380,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,X1)),double_divide(inverse(double_divide(iPr_def_10(X2,X3),double_divide(X4,double_divide(X5,X4)))),double_divide(X6,X5))))) = iPr_def_10(inverse(double_divide(X2,double_divide(X6,X3))),X1),
inference(superposition,[status(thm)],[c_80,c_87]) ).
tcf(c_405,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,double_divide(X1,inverse(X2)))),double_divide(inverse(double_divide(inverse(double_divide(inverse(double_divide(X3,double_divide(X1,X4))),double_divide(X5,X6))),double_divide(X7,double_divide(X5,X7)))),X6)))) = inverse(double_divide(iPr_def_10(X3,X4),double_divide(iPr_def_10(X2,X8),X8))),
inference(superposition,[status(thm)],[c_118,c_62]) ).
tcf(c_430,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : double_divide(inverse(inverse(double_divide(X0,double_divide(X1,X2)))),inverse(double_divide(iPr_def_10(X0,X2),double_divide(iPr_def_10(X3,X4),X4)))) = iPr_def_10(X3,double_divide(X5,double_divide(X1,X5))),
inference(superposition,[status(thm)],[c_65,c_83]) ).
tcf(c_459,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,iPr_def_10(X1,double_divide(X2,double_divide(X3,X2))))),double_divide(inverse(double_divide(inverse(double_divide(inverse(double_divide(X4,double_divide(X3,X5))),double_divide(X6,X7))),double_divide(X8,double_divide(X6,X8)))),X7)))) = inverse(double_divide(iPr_def_10(X4,X5),double_divide(X9,double_divide(inverse(X1),X9)))),
inference(superposition,[status(thm)],[c_83,c_62]) ).
tcf(c_474,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : double_divide(inverse(X0),double_divide(inverse(inverse(double_divide(X1,double_divide(X2,X3)))),inverse(double_divide(iPr_def_10(X1,X3),double_divide(X4,double_divide(inverse(X0),X4)))))) = double_divide(X5,double_divide(X2,X5)),
inference(superposition,[status(thm)],[c_83,c_65]) ).
tcf(c_482,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(double_divide(iPr_def_10(X0,X1),double_divide(X2,double_divide(X3,X2)))) = iPr_def_12(X0,X1,X3),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_379]) ).
tcf(c_484,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : double_divide(inverse(inverse(double_divide(X0,double_divide(X1,X2)))),iPr_def_12(X0,X2,X3)) = double_divide(X1,X3),
inference(demodulation,[status(thm)],[c_378,c_482]) ).
tcf(c_485,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(inverse(double_divide(X0,double_divide(inverse(X1),X2))),X3) = iPr_def_12(X0,X2,iPr_def_10(X1,X3)),
inference(demodulation,[status(thm)],[c_353,c_482]) ).
tcf(c_486,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(inverse(double_divide(X0,X1)),double_divide(inverse(X2),X3)) = iPr_def_12(X0,iPr_def_10(X2,X1),X3),
inference(demodulation,[status(thm)],[c_348,c_482]) ).
tcf(c_493,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,double_divide(X1,double_divide(X2,X1))) = double_divide(X2,inverse(X0)),
inference(demodulation,[status(thm)],[c_430,c_118]) ).
tcf(c_500,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(inverse(X0),double_divide(X1,inverse(X0))) = double_divide(X2,double_divide(X1,X2)),
inference(demodulation,[status(thm)],[c_474,c_482,c_484]) ).
tcf(c_501,plain,
! [X0: $i,X1: $i] : double_divide(X0,double_divide(X1,X0)) = iPr_def_13(X1),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_500]) ).
tcf(c_532,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,X1)),double_divide(iPr_def_12(X2,X3,X4),double_divide(X5,X4))))) = iPr_def_10(inverse(double_divide(X2,double_divide(X5,X3))),X1),
inference(demodulation,[status(thm)],[c_380,c_482]) ).
tcf(c_560,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(X0,iPr_def_10(X1,X2),iPr_def_10(X1,double_divide(inverse(inverse(double_divide(X0,X2))),X3))) = X3,
inference(demodulation,[status(thm)],[c_245,c_482,c_485,c_532]) ).
tcf(c_585,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,iPr_def_10(X1,X2))),double_divide(inverse(double_divide(inverse(double_divide(X3,double_divide(X4,X5))),iPr_def_13(X4))),X5)))) = iPr_def_10(X3,iPr_def_10(X1,X2)),
inference(demodulation,[status(thm)],[c_281,c_284,c_501]) ).
tcf(c_596,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(inverse(X0),iPr_def_10(X1,iPr_def_10(X0,X2))) = inverse(double_divide(inverse(X2),iPr_def_13(inverse(X1)))),
inference(demodulation,[status(thm)],[c_328,c_501,c_585]) ).
tcf(c_616,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,double_divide(X1,inverse(X2)))),double_divide(inverse(double_divide(inverse(double_divide(inverse(double_divide(X3,double_divide(X1,X4))),double_divide(X5,X6))),iPr_def_13(X5))),X6)))) = inverse(double_divide(iPr_def_10(X3,X4),double_divide(iPr_def_10(X2,X7),X7))),
inference(demodulation,[status(thm)],[c_405,c_501]) ).
tcf(c_617,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(double_divide(iPr_def_10(X0,X1),double_divide(iPr_def_10(X2,X3),X3))) = iPr_def_14(X0,X1,X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_616]) ).
tcf(c_618,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,double_divide(X1,inverse(X2)))),double_divide(inverse(double_divide(inverse(double_divide(inverse(double_divide(X3,double_divide(X1,X4))),double_divide(X5,X6))),iPr_def_13(X5))),X6)))) = iPr_def_14(X3,X4,X2),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_616]) ).
tcf(c_627,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(X0,X1,inverse(X2)) = iPr_def_14(X0,X1,X2),
inference(demodulation,[status(thm)],[c_459,c_482,c_493,c_501,c_618]) ).
tcf(c_635,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(inverse(double_divide(X0,double_divide(X1,X2))),double_divide(X1,X3)) = iPr_def_12(X0,X2,X3),
inference(demodulation,[status(thm)],[c_80,c_482]) ).
tcf(c_639,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(double_divide(inverse(double_divide(X0,double_divide(X1,X2))),iPr_def_13(X1))) = iPr_def_10(X0,X2),
inference(demodulation,[status(thm)],[c_63,c_501]) ).
tcf(c_1213,plain,
! [X0: $i,X1: $i] : double_divide(iPr_def_10(X0,X1),X1) = iPr_def_13(inverse(X0)),
inference(superposition,[status(thm)],[c_65,c_501]) ).
tcf(c_1214,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,X1),iPr_def_13(X0)) = iPr_def_13(X1),
inference(superposition,[status(thm)],[c_501,c_501]) ).
tcf(c_1216,plain,
! [X0: $i,X1: $i] : double_divide(X0,inverse(X1)) = iPr_def_10(X1,iPr_def_13(X0)),
inference(superposition,[status(thm)],[c_501,c_114]) ).
tcf(c_1226,plain,
! [X0: $i,X1: $i] : inverse(double_divide(inverse(iPr_def_13(X0)),iPr_def_13(X0))) = iPr_def_10(X1,X1),
inference(superposition,[status(thm)],[c_501,c_639]) ).
tcf(c_1235,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(double_divide(iPr_def_10(X0,X1),iPr_def_13(X2))) = iPr_def_12(X0,X1,X2),
inference(superposition,[status(thm)],[c_501,c_482]) ).
tcf(c_1242,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(iPr_def_13(iPr_def_10(X0,iPr_def_10(X1,X2)))) = iPr_def_14(X1,X2,X0),
inference(superposition,[status(thm)],[c_501,c_617]) ).
tcf(c_1307,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(X0,X0,iPr_def_10(X1,X2)) = iPr_def_10(inverse(iPr_def_13(inverse(X1))),X2),
inference(superposition,[status(thm)],[c_501,c_485]) ).
tcf(c_1358,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(X0,iPr_def_10(inverse(double_divide(X0,X1)),X1),X2) = X2,
inference(superposition,[status(thm)],[c_114,c_560]) ).
tcf(c_1418,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_12(X0,X1,iPr_def_10(X2,iPr_def_10(X3,iPr_def_10(double_divide(X0,double_divide(inverse(X2),X1)),X4)))) = inverse(double_divide(inverse(X4),iPr_def_13(inverse(X3)))),
inference(superposition,[status(thm)],[c_596,c_485]) ).
tcf(c_1617,plain,
inverse(double_divide(inverse(double_divide(c3,b3)),a3)) != inverse(iPr_def_10(double_divide(b3,a3),iPr_def_13(c3))),
inference(demodulation,[status(thm)],[c_53,c_1216]) ).
tcf(c_2855,plain,
! [X0: $i,X1: $i] : double_divide(X0,iPr_def_13(inverse(X1))) = iPr_def_13(iPr_def_10(X1,X0)),
inference(superposition,[status(thm)],[c_65,c_1214]) ).
tcf(c_2884,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_13(iPr_def_10(X1,inverse(X0)))) = iPr_def_13(inverse(X1)),
inference(superposition,[status(thm)],[c_1216,c_1213]) ).
tcf(c_2885,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_10(X1,iPr_def_13(inverse(X0)))) = inverse(X1),
inference(superposition,[status(thm)],[c_1216,c_114]) ).
tcf(c_2902,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(inverse(X0),iPr_def_10(X1,inverse(double_divide(inverse(iPr_def_13(X2)),iPr_def_13(X2))))) = inverse(double_divide(inverse(X0),iPr_def_13(inverse(X1)))),
inference(superposition,[status(thm)],[c_1226,c_596]) ).
tcf(c_2903,plain,
! [X0: $i,X1: $i] : double_divide(inverse(double_divide(inverse(iPr_def_13(X0)),iPr_def_13(X0))),X1) = iPr_def_13(inverse(X1)),
inference(superposition,[status(thm)],[c_1226,c_1213]) ).
tcf(c_2905,plain,
! [X0: $i,X1: $i] : double_divide(inverse(X0),inverse(double_divide(inverse(iPr_def_13(X1)),iPr_def_13(X1)))) = X0,
inference(superposition,[status(thm)],[c_1226,c_65]) ).
tcf(c_2910,plain,
! [X0: $i,X1: $i] : inverse(double_divide(inverse(iPr_def_13(X0)),iPr_def_13(X0))) = inverse(double_divide(inverse(iPr_def_13(X1)),iPr_def_13(X1))),
inference(superposition,[status(thm)],[c_1226,c_1226]) ).
tcf(c_2912,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(X0,iPr_def_12(X0,X1,X1),X2) = X2,
inference(superposition,[status(thm)],[c_635,c_1358]) ).
tcf(c_2928,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,iPr_def_13(X1),X1) = inverse(iPr_def_13(inverse(X0))),
inference(superposition,[status(thm)],[c_1213,c_1235]) ).
tcf(c_2934,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(double_divide(inverse(double_divide(inverse(iPr_def_13(X0)),iPr_def_13(X0))),iPr_def_13(X1))) = iPr_def_12(X2,X2,X1),
inference(superposition,[status(thm)],[c_1226,c_1235]) ).
tcf(c_2949,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(iPr_def_13(inverse(double_divide(inverse(iPr_def_13(X0)),iPr_def_13(X0))))) = iPr_def_14(X1,X2,iPr_def_10(X1,X2)),
inference(superposition,[status(thm)],[c_1226,c_1242]) ).
tcf(c_3100,plain,
! [X0: $i,X1: $i] : iPr_def_10(double_divide(inverse(iPr_def_13(X0)),iPr_def_13(X0)),iPr_def_13(inverse(X1))) = X1,
inference(demodulation,[status(thm)],[c_2905,c_1216]) ).
tcf(c_3108,plain,
! [X0: $i] : inverse(double_divide(inverse(iPr_def_13(X0)),iPr_def_13(X0))) = iPr_def_18,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_18])],[c_2910]) ).
tcf(c_3112,plain,
! [X0: $i,X1: $i] : iPr_def_14(X0,X1,iPr_def_10(X0,X1)) = inverse(iPr_def_13(iPr_def_18)),
inference(demodulation,[status(thm)],[c_2949,c_3108]) ).
tcf(c_3113,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_13(inverse(iPr_def_13(X0)))) = iPr_def_12(X1,X1,X0),
inference(demodulation,[status(thm)],[c_2934,c_2903]) ).
tcf(c_3145,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_13(iPr_def_10(X0,inverse(X1)))) = iPr_def_10(inverse(X1),iPr_def_10(X0,iPr_def_18)),
inference(demodulation,[status(thm)],[c_2902,c_2855,c_3108]) ).
tcf(c_3258,plain,
! [X0: $i] : iPr_def_10(X0,X0) = iPr_def_18,
inference(demodulation,[status(thm)],[c_1226,c_3108]) ).
tcf(c_4076,plain,
! [X0: $i,X1: $i] : inverse(double_divide(iPr_def_18,iPr_def_13(X0))) = iPr_def_12(X1,X1,X0),
inference(superposition,[status(thm)],[c_3258,c_1235]) ).
tcf(c_4077,plain,
! [X0: $i] : double_divide(iPr_def_18,X0) = iPr_def_13(inverse(X0)),
inference(superposition,[status(thm)],[c_3258,c_1213]) ).
tcf(c_4079,plain,
! [X0: $i] : double_divide(inverse(X0),iPr_def_18) = X0,
inference(superposition,[status(thm)],[c_3258,c_65]) ).
tcf(c_4095,plain,
! [X0: $i,X1: $i] : iPr_def_10(double_divide(inverse(iPr_def_13(X0)),iPr_def_13(X0)),iPr_def_13(X1)) = double_divide(X1,iPr_def_18),
inference(superposition,[status(thm)],[c_3108,c_1216]) ).
tcf(c_4156,plain,
! [X0: $i] : inverse(iPr_def_13(iPr_def_10(X0,inverse(iPr_def_13(inverse(X0)))))) = iPr_def_18,
inference(superposition,[status(thm)],[c_2855,c_3108]) ).
tcf(c_4177,plain,
! [X0: $i] : inverse(iPr_def_13(inverse(X0))) = iPr_def_10(X0,iPr_def_18),
inference(superposition,[status(thm)],[c_3258,c_2885]) ).
tcf(c_4192,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,iPr_def_10(X1,double_divide(X2,iPr_def_13(inverse(X2))))) = double_divide(inverse(inverse(X1)),inverse(X0)),
inference(superposition,[status(thm)],[c_2885,c_310]) ).
tcf(c_4193,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(X0,X1,iPr_def_10(X2,iPr_def_10(X3,iPr_def_13(inverse(inverse(double_divide(X0,double_divide(inverse(X2),X1)))))))) = inverse(X3),
inference(superposition,[status(thm)],[c_2885,c_485]) ).
tcf(c_4199,plain,
! [X0: $i,X1: $i] : iPr_def_14(X0,iPr_def_13(inverse(X1)),X1) = inverse(iPr_def_13(inverse(X0))),
inference(superposition,[status(thm)],[c_2928,c_627]) ).
tcf(c_4228,plain,
! [X0: $i] : iPr_def_14(X0,X0,iPr_def_18) = inverse(iPr_def_13(iPr_def_18)),
inference(superposition,[status(thm)],[c_3258,c_3112]) ).
tcf(c_4260,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,inverse(iPr_def_13(inverse(iPr_def_13(X0)))),X1) = X1,
inference(superposition,[status(thm)],[c_3113,c_2912]) ).
tcf(c_4266,plain,
! [X0: $i] : iPr_def_10(X0,iPr_def_13(iPr_def_18)) = iPr_def_13(inverse(inverse(X0))),
inference(superposition,[status(thm)],[c_3258,c_2884]) ).
tcf(c_4309,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(double_divide(inverse(iPr_def_13(X0)),iPr_def_13(X0)),iPr_def_13(iPr_def_10(X1,X2))) = double_divide(inverse(double_divide(X1,double_divide(X3,X2))),iPr_def_13(X3)),
inference(superposition,[status(thm)],[c_639,c_3100]) ).
tcf(c_4310,plain,
! [X0: $i,X1: $i] : iPr_def_10(double_divide(inverse(iPr_def_13(X0)),iPr_def_13(X0)),iPr_def_13(iPr_def_18)) = double_divide(inverse(iPr_def_13(X1)),iPr_def_13(X1)),
inference(superposition,[status(thm)],[c_3108,c_3100]) ).
tcf(c_4334,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(iPr_def_13(inverse(X0))),X0) = iPr_def_12(X1,X1,iPr_def_18),
inference(superposition,[status(thm)],[c_3258,c_1307]) ).
tcf(c_4347,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,iPr_def_10(iPr_def_13(X0),iPr_def_18),X1) = X1,
inference(demodulation,[status(thm)],[c_4260,c_4177]) ).
tcf(c_4348,plain,
! [X0: $i] : inverse(iPr_def_13(iPr_def_10(X0,iPr_def_10(X0,iPr_def_18)))) = iPr_def_18,
inference(demodulation,[status(thm)],[c_4156,c_4177]) ).
tcf(c_4349,plain,
! [X0: $i] : iPr_def_14(X0,iPr_def_18,X0) = iPr_def_18,
inference(demodulation,[status(thm)],[c_4348,c_1242]) ).
tcf(c_4351,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,X0,X1) = iPr_def_10(iPr_def_13(X1),iPr_def_18),
inference(demodulation,[status(thm)],[c_4076,c_4077,c_4177]) ).
tcf(c_4352,plain,
! [X0: $i] : iPr_def_10(iPr_def_10(X0,iPr_def_18),X0) = iPr_def_10(iPr_def_13(iPr_def_18),iPr_def_18),
inference(demodulation,[status(thm)],[c_4334,c_4177,c_4351]) ).
tcf(c_4355,plain,
! [X0: $i,X1: $i] : iPr_def_14(X0,iPr_def_13(inverse(X1)),X1) = iPr_def_10(X0,iPr_def_18),
inference(demodulation,[status(thm)],[c_4199,c_4177]) ).
tcf(c_4392,plain,
! [X0: $i] : double_divide(inverse(iPr_def_13(X0)),iPr_def_13(X0)) = iPr_def_13(inverse(iPr_def_18)),
inference(demodulation,[status(thm)],[c_4310,c_4077,c_4095]) ).
tcf(c_4397,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_10(X1,iPr_def_13(iPr_def_18))) = iPr_def_10(X0,iPr_def_13(inverse(inverse(X1)))),
inference(demodulation,[status(thm)],[c_4192,c_1216,c_2855,c_3258]) ).
tcf(c_4420,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(X0,X1,iPr_def_10(X2,iPr_def_10(X3,iPr_def_10(double_divide(X0,double_divide(inverse(X2),X1)),iPr_def_13(iPr_def_18))))) = inverse(X3),
inference(demodulation,[status(thm)],[c_4193,c_4397]) ).
tcf(c_4421,plain,
! [X0: $i] : iPr_def_10(inverse(iPr_def_13(iPr_def_18)),iPr_def_10(X0,iPr_def_18)) = inverse(X0),
inference(demodulation,[status(thm)],[c_4420,c_1418,c_2855,c_3145]) ).
tcf(c_4433,plain,
! [X0: $i,X1: $i,X2: $i] : double_divide(inverse(double_divide(X0,double_divide(X1,X2))),iPr_def_13(X1)) = double_divide(iPr_def_10(X0,X2),iPr_def_18),
inference(demodulation,[status(thm)],[c_4309,c_4095]) ).
tcf(c_4482,plain,
! [X0: $i,X1: $i] : inverse(double_divide(iPr_def_10(X0,X1),iPr_def_18)) = iPr_def_10(X0,X1),
inference(demodulation,[status(thm)],[c_639,c_4433]) ).
tcf(c_7096,plain,
inverse(iPr_def_13(iPr_def_18)) = iPr_def_18,
inference(superposition,[status(thm)],[c_4228,c_4349]) ).
tcf(c_7129,plain,
! [X0: $i] : inverse(iPr_def_10(X0,iPr_def_13(iPr_def_18))) = iPr_def_10(inverse(X0),iPr_def_18),
inference(superposition,[status(thm)],[c_4266,c_4177]) ).
tcf(c_7169,plain,
iPr_def_10(iPr_def_13(iPr_def_18),iPr_def_18) = iPr_def_18,
inference(superposition,[status(thm)],[c_3258,c_4352]) ).
tcf(c_7247,plain,
! [X0: $i] : iPr_def_10(iPr_def_13(X0),iPr_def_13(inverse(iPr_def_18))) = iPr_def_13(X0),
inference(superposition,[status(thm)],[c_4392,c_114]) ).
tcf(c_7268,plain,
! [X0: $i] : inverse(double_divide(X0,iPr_def_18)) = X0,
inference(superposition,[status(thm)],[c_114,c_4482]) ).
tcf(c_7369,plain,
! [X0: $i] : iPr_def_10(iPr_def_18,iPr_def_10(X0,iPr_def_18)) = inverse(X0),
inference(demodulation,[status(thm)],[c_4421,c_7096]) ).
tcf(c_7372,plain,
! [X0: $i] : iPr_def_10(iPr_def_10(X0,iPr_def_18),X0) = iPr_def_18,
inference(demodulation,[status(thm)],[c_4352,c_7169]) ).
tcf(c_8110,plain,
! [X0: $i] : iPr_def_12(iPr_def_18,iPr_def_18,X0) = X0,
inference(superposition,[status(thm)],[c_7169,c_4347]) ).
tcf(c_8125,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,double_divide(inverse(X1),X2)) = iPr_def_12(X0,iPr_def_10(X1,iPr_def_18),X2),
inference(superposition,[status(thm)],[c_7268,c_486]) ).
tcf(c_8126,plain,
! [X0: $i,X1: $i] : iPr_def_14(X0,iPr_def_13(X1),double_divide(X1,iPr_def_18)) = iPr_def_10(X0,iPr_def_18),
inference(superposition,[status(thm)],[c_7268,c_4355]) ).
tcf(c_8132,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_14(X0,X1,double_divide(X2,iPr_def_18)) = iPr_def_12(X0,X1,X2),
inference(superposition,[status(thm)],[c_7268,c_627]) ).
tcf(c_8161,plain,
! [X0: $i] : double_divide(inverse(iPr_def_10(X0,iPr_def_18)),iPr_def_18) = X0,
inference(superposition,[status(thm)],[c_7372,c_65]) ).
tcf(c_8162,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_10(X0,iPr_def_18),iPr_def_10(X1,double_divide(X2,X0))) = double_divide(inverse(inverse(X1)),iPr_def_10(X2,iPr_def_18)),
inference(superposition,[status(thm)],[c_7372,c_310]) ).
tcf(c_8167,plain,
! [X0: $i] : inverse(iPr_def_10(iPr_def_13(inverse(X0)),iPr_def_18)) = iPr_def_10(X0,iPr_def_18),
inference(superposition,[status(thm)],[c_7372,c_2885]) ).
tcf(c_8168,plain,
! [X0: $i] : iPr_def_13(inverse(iPr_def_10(inverse(X0),iPr_def_18))) = iPr_def_10(X0,iPr_def_13(iPr_def_18)),
inference(superposition,[status(thm)],[c_7372,c_2884]) ).
tcf(c_8220,plain,
inverse(iPr_def_18) = iPr_def_18,
inference(superposition,[status(thm)],[c_3258,c_7369]) ).
tcf(c_8228,plain,
! [X0: $i,X1: $i] : inverse(double_divide(inverse(X0),iPr_def_13(X1))) = iPr_def_12(iPr_def_18,iPr_def_10(X0,iPr_def_18),X1),
inference(superposition,[status(thm)],[c_7369,c_1235]) ).
tcf(c_8275,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_13(X0),iPr_def_13(inverse(iPr_def_18)),X1) = inverse(double_divide(iPr_def_13(X0),iPr_def_13(X1))),
inference(superposition,[status(thm)],[c_7247,c_1235]) ).
tcf(c_8291,plain,
! [X0: $i] : double_divide(iPr_def_10(inverse(X0),iPr_def_18),iPr_def_18) = iPr_def_10(X0,iPr_def_13(iPr_def_18)),
inference(superposition,[status(thm)],[c_7129,c_4079]) ).
tcf(c_8301,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_10(X0,iPr_def_13(iPr_def_18)),iPr_def_13(X1)) = double_divide(X1,iPr_def_10(inverse(X0),iPr_def_18)),
inference(superposition,[status(thm)],[c_7129,c_1216]) ).
tcf(c_8344,plain,
! [X0: $i] : iPr_def_10(iPr_def_13(X0),iPr_def_18) = X0,
inference(demodulation,[status(thm)],[c_8110,c_4351]) ).
tcf(c_8357,plain,
! [X0: $i] : iPr_def_10(X0,iPr_def_18) = X0,
inference(demodulation,[status(thm)],[c_8161,c_4079]) ).
tcf(c_8413,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_8167,c_8344,c_8357]) ).
tcf(c_8427,plain,
! [X0: $i] : double_divide(inverse(X0),iPr_def_18) = iPr_def_10(X0,iPr_def_13(iPr_def_18)),
inference(demodulation,[status(thm)],[c_8291,c_8357]) ).
tcf(c_8428,plain,
! [X0: $i] : iPr_def_10(X0,iPr_def_13(iPr_def_18)) = X0,
inference(demodulation,[status(thm)],[c_8427,c_4079]) ).
tcf(c_8442,plain,
! [X0: $i] : iPr_def_13(X0) = X0,
inference(demodulation,[status(thm)],[c_8168,c_8357,c_8413,c_8428]) ).
tcf(c_8452,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,X1,X1) = X0,
inference(demodulation,[status(thm)],[c_8126,c_8132,c_8357,c_8442]) ).
tcf(c_8470,plain,
! [X0: $i,X1: $i] : inverse(double_divide(inverse(X0),X1)) = iPr_def_12(iPr_def_18,X0,X1),
inference(demodulation,[status(thm)],[c_8228,c_8357,c_8442]) ).
tcf(c_8477,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,double_divide(inverse(X1),X2)) = iPr_def_12(X0,X1,X2),
inference(demodulation,[status(thm)],[c_8125,c_8357]) ).
tcf(c_8478,plain,
! [X0: $i,X1: $i] : double_divide(X0,inverse(X1)) = iPr_def_10(X1,X0),
inference(demodulation,[status(thm)],[c_8301,c_8357,c_8428,c_8442]) ).
tcf(c_8480,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,inverse(iPr_def_18),X1) = inverse(double_divide(X0,X1)),
inference(demodulation,[status(thm)],[c_8275,c_8442]) ).
tcf(c_8522,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,iPr_def_10(X1,double_divide(X2,X0))) = double_divide(X1,X2),
inference(demodulation,[status(thm)],[c_8162,c_8357,c_8413]) ).
tcf(c_8585,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,X1),X0) = iPr_def_13(X1),
inference(demodulation,[status(thm)],[c_1214,c_8442]) ).
tcf(c_8586,plain,
! [X0: $i] : double_divide(iPr_def_18,X0) = inverse(X0),
inference(demodulation,[status(thm)],[c_4077,c_8442]) ).
tcf(c_8591,plain,
inverse(double_divide(inverse(double_divide(c3,b3)),a3)) != inverse(iPr_def_10(double_divide(b3,a3),c3)),
inference(demodulation,[status(thm)],[c_1617,c_8442]) ).
tcf(c_8594,plain,
inverse(iPr_def_10(double_divide(b3,a3),c3)) != iPr_def_12(iPr_def_18,double_divide(c3,b3),a3),
inference(demodulation,[status(thm)],[c_8591,c_8470]) ).
tcf(c_8596,plain,
! [X0: $i,X1: $i] : double_divide(double_divide(X0,X1),X0) = X1,
inference(demodulation,[status(thm)],[c_8585,c_8442]) ).
tcf(c_8757,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(double_divide(X0,X1)),X1) = X0,
inference(superposition,[status(thm)],[c_8452,c_1358]) ).
tcf(c_9035,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(X0),X1) = double_divide(X1,X0),
inference(superposition,[status(thm)],[c_8596,c_8757]) ).
tcf(c_9140,plain,
! [X0: $i,X1: $i] : inverse(double_divide(X0,X1)) = iPr_def_12(X0,iPr_def_18,X1),
inference(superposition,[status(thm)],[c_8220,c_8480]) ).
tcf(c_9172,plain,
! [X0: $i,X1: $i] : iPr_def_12(inverse(X0),iPr_def_18,X1) = iPr_def_12(iPr_def_18,X0,X1),
inference(demodulation,[status(thm)],[c_8470,c_9140]) ).
tcf(c_9243,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,iPr_def_18,inverse(X1)) = inverse(iPr_def_10(X1,X0)),
inference(superposition,[status(thm)],[c_8478,c_9140]) ).
tcf(c_9408,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,double_divide(iPr_def_18,X1)) = iPr_def_12(X0,iPr_def_18,X1),
inference(superposition,[status(thm)],[c_8220,c_8477]) ).
tcf(c_9430,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,inverse(X1)) = iPr_def_12(X0,iPr_def_18,X1),
inference(demodulation,[status(thm)],[c_9408,c_8586]) ).
tcf(c_9451,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,inverse(inverse(X1))) = inverse(iPr_def_10(X1,X0)),
inference(demodulation,[status(thm)],[c_9243,c_9430]) ).
tcf(c_9452,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_10(X0,X1)) = iPr_def_10(X1,X0),
inference(demodulation,[status(thm)],[c_9451,c_8413]) ).
tcf(c_9532,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(X0),inverse(X1)) = iPr_def_12(iPr_def_18,X0,X1),
inference(demodulation,[status(thm)],[c_9172,c_9430]) ).
tcf(c_9533,plain,
! [X0: $i,X1: $i] : double_divide(inverse(X0),X1) = iPr_def_12(iPr_def_18,X1,X0),
inference(demodulation,[status(thm)],[c_9532,c_9035]) ).
tcf(c_9536,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_18,iPr_def_10(X0,X1),X0) = X1,
inference(demodulation,[status(thm)],[c_65,c_9533]) ).
tcf(c_9544,plain,
iPr_def_12(iPr_def_18,double_divide(c3,b3),a3) != iPr_def_10(c3,double_divide(b3,a3)),
inference(demodulation,[status(thm)],[c_8594,c_9452]) ).
tcf(c_10118,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(iPr_def_18,double_divide(X0,X1),X2) = iPr_def_10(X0,double_divide(X1,X2)),
inference(superposition,[status(thm)],[c_8522,c_9536]) ).
tcf(c_10313,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_9544,c_10118]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP501-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.38 % Computer : n010.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 14:55:57 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.42 Running UEQ theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.43
% 0.11/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.43
% 0.11/0.43 % Detected problem language: tptp
% 0.11/0.45 % Proving...
% 13.02/2.77 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 13.02/2.77 % SZS status Started for theBenchmark.p
% 13.02/2.77 % SZS status Unsatisfiable for theBenchmark.p
% 13.02/2.77
% 13.02/2.77 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 13.02/2.77
% 13.02/2.77 % ------ iProver source info
% 13.02/2.77
% 13.02/2.77 % git: date: 2026-07-19 20:42:38 +0200
% 13.02/2.77 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 13.02/2.77 % git: non_committed_changes: false
% 13.02/2.77
% 13.02/2.77 % ------ Parsing...% successful
% 13.02/2.77
% 13.02/2.77
% 13.02/2.77 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 13.02/2.77 % ------ Proving...
% 13.02/2.77 % ------ Problem Properties
% 13.02/2.77
% 13.02/2.77 %
% 13.02/2.77 % clauses 2
% 13.02/2.77 % conjectures 1
% 13.02/2.77 % EPR 0
% 13.02/2.77 % Horn 2
% 13.02/2.77 % unary 2
% 13.02/2.77 % binary 0
% 13.02/2.77 % lits 2
% 13.02/2.77 % lits eq 2
% 13.02/2.77 % fd_pure 0
% 13.02/2.77 % fd_pseudo 0
% 13.02/2.77 % fd_cond 0
% 13.02/2.77 % fd_pseudo_cond 0
% 13.02/2.77 % AC symbols 0
% 13.02/2.77
% 13.02/2.77 % ------ Input Options Time Limit: Unbounded
% 13.02/2.77
% 13.02/2.77
% 13.02/2.77 % ------
% 13.02/2.77 % Current options:
% 13.02/2.77 % ------
% 13.02/2.77
% 13.02/2.77
% 13.02/2.77 %
% 13.02/2.77
% 13.02/2.77 % ------ Proving...
% 13.02/2.77 %
% 13.02/2.77
% 13.02/2.77 % SZS status Unsatisfiable for theBenchmark.p
% 13.02/2.77
% 13.02/2.77 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 13.02/2.77
% 13.02/2.77
%------------------------------------------------------------------------------