%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : NUM648^1 : TPTP v7.0.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n159.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32218.625MB % OS : Linux 3.10.0-693.2.2.el7.x86_64 % CPULimit : 300s % DateTime : Mon Jan 8 13:11:17 EST 2018 % Result : Theorem 17.57s % Output : Proof 17.57s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM648^1 : TPTP v7.0.0. Released v3.7.0. % 0.00/0.04 % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.03/0.23 % Computer : n159.star.cs.uiowa.edu % 0.03/0.23 % Model : x86_64 x86_64 % 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.23 % Memory : 32218.625MB % 0.03/0.23 % OS : Linux 3.10.0-693.2.2.el7.x86_64 % 0.03/0.24 % CPULimit : 300 % 0.03/0.24 % DateTime : Fri Jan 5 11:31:15 CST 2018 % 0.03/0.24 % CPUTime : % 0.03/0.28 Python 2.7.13 % 8.07/8.50 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox2/benchmark/', '/export/starexec/sandbox2/benchmark/'] % 8.07/8.50 FOF formula (<kernel.Constant object at 0x2ad158184758>, <kernel.Type object at 0x2ad158180050>) of role type named nat_type % 8.07/8.50 Using role type % 8.07/8.50 Declaring nat:Type % 8.07/8.50 FOF formula (<kernel.Constant object at 0x2ad158184170>, <kernel.Constant object at 0x2ad158184b00>) of role type named x % 8.07/8.50 Using role type % 8.07/8.50 Declaring x:nat % 8.07/8.50 FOF formula (<kernel.Constant object at 0x2ad158184d88>, <kernel.Constant object at 0x2ad1581804d0>) of role type named y % 8.07/8.50 Using role type % 8.07/8.50 Declaring y:nat % 8.07/8.50 FOF formula (<kernel.Constant object at 0x2ad158184b00>, <kernel.DependentProduct object at 0x2ad158180098>) of role type named pl % 8.07/8.50 Using role type % 8.07/8.50 Declaring pl:(nat->(nat->nat)) % 8.07/8.50 FOF formula (forall (Xx:nat) (Xy:nat) (Xz:nat), ((((eq nat) ((pl Xx) Xy)) ((pl Xx) Xz))->(((eq nat) Xy) Xz))) of role axiom named satz8a % 8.07/8.50 A new axiom: (forall (Xx:nat) (Xy:nat) (Xz:nat), ((((eq nat) ((pl Xx) Xy)) ((pl Xx) Xz))->(((eq nat) Xy) Xz))) % 8.07/8.50 FOF formula (forall (Xx_0:nat) (Xy_0:nat), ((((eq nat) x) ((pl y) Xx_0))->((((eq nat) x) ((pl y) Xy_0))->(((eq nat) Xx_0) Xy_0)))) of role conjecture named satz8b % 8.07/8.50 Conjecture to prove = (forall (Xx_0:nat) (Xy_0:nat), ((((eq nat) x) ((pl y) Xx_0))->((((eq nat) x) ((pl y) Xy_0))->(((eq nat) Xx_0) Xy_0)))):Prop % 8.07/8.50 We need to prove ['(forall (Xx_0:nat) (Xy_0:nat), ((((eq nat) x) ((pl y) Xx_0))->((((eq nat) x) ((pl y) Xy_0))->(((eq nat) Xx_0) Xy_0))))'] % 8.07/8.50 Parameter nat:Type. % 8.07/8.50 Parameter x:nat. % 8.07/8.50 Parameter y:nat. % 8.07/8.50 Parameter pl:(nat->(nat->nat)). % 8.07/8.50 Axiom satz8a:(forall (Xx:nat) (Xy:nat) (Xz:nat), ((((eq nat) ((pl Xx) Xy)) ((pl Xx) Xz))->(((eq nat) Xy) Xz))). % 8.07/8.50 Trying to prove (forall (Xx_0:nat) (Xy_0:nat), ((((eq nat) x) ((pl y) Xx_0))->((((eq nat) x) ((pl y) Xy_0))->(((eq nat) Xx_0) Xy_0)))) % 8.07/8.50 Found x10:=(x1 (fun (x2:nat)=> (P Xx_0))):((P Xx_0)->(P Xx_0)) % 8.07/8.50 Found (x1 (fun (x2:nat)=> (P Xx_0))) as proof of (P0 Xx_0) % 8.07/8.50 Found (x1 (fun (x2:nat)=> (P Xx_0))) as proof of (P0 Xx_0) % 8.07/8.50 Found eq_ref00:=(eq_ref0 Xx_0):(((eq nat) Xx_0) Xx_0) % 8.07/8.50 Found (eq_ref0 Xx_0) as proof of (((eq nat) Xx_0) b) % 8.07/8.50 Found ((eq_ref nat) Xx_0) as proof of (((eq nat) Xx_0) b) % 8.07/8.50 Found ((eq_ref nat) Xx_0) as proof of (((eq nat) Xx_0) b) % 8.07/8.50 Found ((eq_ref nat) Xx_0) as proof of (((eq nat) Xx_0) b) % 8.07/8.50 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 8.07/8.50 Found (eq_ref0 b) as proof of (((eq nat) b) Xy_0) % 8.07/8.50 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy_0) % 8.07/8.50 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy_0) % 8.07/8.50 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy_0) % 8.07/8.50 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 8.07/8.50 Found (eq_ref0 b) as proof of (((eq nat) b) Xx_0) % 8.07/8.50 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx_0) % 8.07/8.50 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx_0) % 8.07/8.50 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx_0) % 8.07/8.50 Found eq_ref00:=(eq_ref0 Xy_0):(((eq nat) Xy_0) Xy_0) % 8.07/8.50 Found (eq_ref0 Xy_0) as proof of (((eq nat) Xy_0) b) % 8.07/8.50 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 8.07/8.50 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 8.07/8.50 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 8.07/8.50 Found x2:(P Xx_0) % 8.07/8.50 Instantiate: b:=Xx_0:nat % 8.07/8.50 Found x2 as proof of (P0 b) % 8.07/8.50 Found eq_ref00:=(eq_ref0 Xy_0):(((eq nat) Xy_0) Xy_0) % 8.07/8.50 Found (eq_ref0 Xy_0) as proof of (((eq nat) Xy_0) b) % 8.07/8.50 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 8.07/8.50 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 8.07/8.50 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 8.07/8.50 Found x00:=(x0 (fun (x2:nat)=> (P Xx_0))):((P Xx_0)->(P Xx_0)) % 8.07/8.50 Found (x0 (fun (x2:nat)=> (P Xx_0))) as proof of (P0 Xx_0) % 8.07/8.50 Found (x0 (fun (x2:nat)=> (P Xx_0))) as proof of (P0 Xx_0) % 8.07/8.50 Found eq_ref00:=(eq_ref0 Xx_0):(((eq nat) Xx_0) Xx_0) % 8.07/8.50 Found (eq_ref0 Xx_0) as proof of (((eq nat) Xx_0) b) % 8.07/8.50 Found ((eq_ref nat) Xx_0) as proof of (((eq nat) Xx_0) b) % 8.07/8.50 Found ((eq_ref nat) Xx_0) as proof of (((eq nat) Xx_0) b) % 8.07/8.50 Found ((eq_ref nat) Xx_0) as proof of (((eq nat) Xx_0) b) % 8.07/8.50 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 8.07/8.50 Found (eq_ref0 b) as proof of (((eq nat) b) Xy_0) % 8.07/8.50 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy_0) % 8.07/8.50 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy_0) % 8.07/8.50 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy_0) % 16.42/16.89 Found x00:=(x0 (fun (x2:nat)=> (P Xx_0))):((P Xx_0)->(P Xx_0)) % 16.42/16.89 Found (x0 (fun (x2:nat)=> (P Xx_0))) as proof of (P0 Xx_0) % 16.42/16.89 Found (x0 (fun (x2:nat)=> (P Xx_0))) as proof of (P0 Xx_0) % 16.42/16.89 Found eq_ref00:=(eq_ref0 Xx_0):(((eq nat) Xx_0) Xx_0) % 16.42/16.89 Found (eq_ref0 Xx_0) as proof of (((eq nat) Xx_0) b) % 16.42/16.89 Found ((eq_ref nat) Xx_0) as proof of (((eq nat) Xx_0) b) % 16.42/16.89 Found ((eq_ref nat) Xx_0) as proof of (((eq nat) Xx_0) b) % 16.42/16.89 Found ((eq_ref nat) Xx_0) as proof of (((eq nat) Xx_0) b) % 16.42/16.89 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 16.42/16.89 Found (eq_ref0 b) as proof of (((eq nat) b) Xy_0) % 16.42/16.89 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy_0) % 16.42/16.89 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy_0) % 16.42/16.89 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xy_0) % 16.42/16.89 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 16.42/16.89 Found (eq_ref0 b) as proof of (P b) % 16.42/16.89 Found ((eq_ref nat) b) as proof of (P b) % 16.42/16.89 Found ((eq_ref nat) b) as proof of (P b) % 16.42/16.89 Found ((eq_ref nat) b) as proof of (P b) % 16.42/16.89 Found eq_ref00:=(eq_ref0 Xy_0):(((eq nat) Xy_0) Xy_0) % 16.42/16.89 Found (eq_ref0 Xy_0) as proof of (((eq nat) Xy_0) b) % 16.42/16.89 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 16.42/16.89 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 16.42/16.89 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 16.42/16.89 Found x2:(P Xy_0) % 16.42/16.89 Instantiate: b:=Xy_0:nat % 16.42/16.89 Found x2 as proof of (P0 b) % 16.42/16.89 Found eq_ref00:=(eq_ref0 Xx_0):(((eq nat) Xx_0) Xx_0) % 16.42/16.89 Found (eq_ref0 Xx_0) as proof of (((eq nat) Xx_0) b) % 16.42/16.89 Found ((eq_ref nat) Xx_0) as proof of (((eq nat) Xx_0) b) % 16.42/16.89 Found ((eq_ref nat) Xx_0) as proof of (((eq nat) Xx_0) b) % 16.42/16.89 Found ((eq_ref nat) Xx_0) as proof of (((eq nat) Xx_0) b) % 16.42/16.89 Found x10:=(x1 (fun (x2:nat)=> (P ((pl Xx) Xx_0)))):((P ((pl Xx) Xx_0))->(P ((pl Xx) Xx_0))) % 16.42/16.89 Found (x1 (fun (x2:nat)=> (P ((pl Xx) Xx_0)))) as proof of (P0 ((pl Xx) Xx_0)) % 16.42/16.89 Found (x1 (fun (x2:nat)=> (P ((pl Xx) Xx_0)))) as proof of (P0 ((pl Xx) Xx_0)) % 16.42/16.89 Found x10:=(x1 (fun (x2:nat)=> (P Xy_0))):((P Xy_0)->(P Xy_0)) % 16.42/16.89 Found (x1 (fun (x2:nat)=> (P Xy_0))) as proof of (P0 Xy_0) % 16.42/16.89 Found (x1 (fun (x2:nat)=> (P Xy_0))) as proof of (P0 Xy_0) % 16.42/16.89 Found eq_ref00:=(eq_ref0 Xx_0):(((eq nat) Xx_0) Xx_0) % 16.42/16.89 Found (eq_ref0 Xx_0) as proof of (((eq nat) Xx_0) b0) % 16.42/16.89 Found ((eq_ref nat) Xx_0) as proof of (((eq nat) Xx_0) b0) % 16.42/16.89 Found ((eq_ref nat) Xx_0) as proof of (((eq nat) Xx_0) b0) % 16.42/16.89 Found ((eq_ref nat) Xx_0) as proof of (((eq nat) Xx_0) b0) % 16.42/16.89 Found eq_ref00:=(eq_ref0 b0):(((eq nat) b0) b0) % 16.42/16.89 Found (eq_ref0 b0) as proof of (((eq nat) b0) Xy_0) % 16.42/16.89 Found ((eq_ref nat) b0) as proof of (((eq nat) b0) Xy_0) % 16.42/16.89 Found ((eq_ref nat) b0) as proof of (((eq nat) b0) Xy_0) % 16.42/16.89 Found ((eq_ref nat) b0) as proof of (((eq nat) b0) Xy_0) % 16.42/16.89 Found x00:=(x0 (fun (x2:nat)=> (P b))):((P b)->(P b)) % 16.42/16.89 Found (x0 (fun (x2:nat)=> (P b))) as proof of (P0 b) % 16.42/16.89 Found (x0 (fun (x2:nat)=> (P b))) as proof of (P0 b) % 16.42/16.89 Found x1:(((eq nat) x) ((pl y) Xy_0)) % 16.42/16.89 Instantiate: Xx:=y:nat;b:=x:nat % 16.42/16.89 Found x1 as proof of (((eq nat) b) ((pl Xx) Xy_0)) % 16.42/16.89 Found eq_ref00:=(eq_ref0 ((pl Xx) Xx_0)):(((eq nat) ((pl Xx) Xx_0)) ((pl Xx) Xx_0)) % 16.42/16.89 Found (eq_ref0 ((pl Xx) Xx_0)) as proof of (((eq nat) ((pl Xx) Xx_0)) b) % 16.42/16.89 Found ((eq_ref nat) ((pl Xx) Xx_0)) as proof of (((eq nat) ((pl Xx) Xx_0)) b) % 16.42/16.89 Found ((eq_ref nat) ((pl Xx) Xx_0)) as proof of (((eq nat) ((pl Xx) Xx_0)) b) % 16.42/16.89 Found ((eq_ref nat) ((pl Xx) Xx_0)) as proof of (((eq nat) ((pl Xx) Xx_0)) b) % 16.42/16.89 Found x00:=(x0 (fun (x2:nat)=> (P Xy_0))):((P Xy_0)->(P Xy_0)) % 16.42/16.89 Found (x0 (fun (x2:nat)=> (P Xy_0))) as proof of (P0 Xy_0) % 16.42/16.89 Found (x0 (fun (x2:nat)=> (P Xy_0))) as proof of (P0 Xy_0) % 16.42/16.89 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 16.42/16.89 Found (eq_ref0 b) as proof of (((eq nat) b) Xx_0) % 16.42/16.89 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx_0) % 16.42/16.89 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx_0) % 16.42/16.89 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx_0) % 16.42/16.89 Found eq_ref00:=(eq_ref0 Xy_0):(((eq nat) Xy_0) Xy_0) % 16.42/16.89 Found (eq_ref0 Xy_0) as proof of (((eq nat) Xy_0) b) % 16.42/16.89 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 16.42/16.89 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 16.42/16.89 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 16.42/16.89 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 16.42/16.89 Found (eq_ref0 b) as proof of (((eq nat) b) Xx_0) % 16.42/16.89 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx_0) % 17.42/17.84 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx_0) % 17.42/17.84 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx_0) % 17.42/17.84 Found eq_ref00:=(eq_ref0 Xy_0):(((eq nat) Xy_0) Xy_0) % 17.42/17.84 Found (eq_ref0 Xy_0) as proof of (((eq nat) Xy_0) b) % 17.42/17.84 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 17.42/17.84 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 17.42/17.84 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 17.42/17.84 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 17.42/17.84 Found (eq_ref0 b) as proof of (((eq nat) b) Xx_0) % 17.42/17.84 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx_0) % 17.42/17.84 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx_0) % 17.42/17.84 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx_0) % 17.42/17.84 Found eq_ref00:=(eq_ref0 Xy_0):(((eq nat) Xy_0) Xy_0) % 17.42/17.84 Found (eq_ref0 Xy_0) as proof of (((eq nat) Xy_0) b) % 17.42/17.84 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 17.42/17.84 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 17.42/17.84 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 17.42/17.84 Found eq_ref00:=(eq_ref0 Xy_0):(((eq nat) Xy_0) Xy_0) % 17.42/17.84 Found (eq_ref0 Xy_0) as proof of (((eq nat) Xy_0) b) % 17.42/17.84 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 17.42/17.84 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 17.42/17.84 Found ((eq_ref nat) Xy_0) as proof of (((eq nat) Xy_0) b) % 17.42/17.84 Found eq_ref00:=(eq_ref0 b):(((eq nat) b) b) % 17.42/17.84 Found (eq_ref0 b) as proof of (((eq nat) b) Xx_0) % 17.42/17.84 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx_0) % 17.42/17.84 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx_0) % 17.42/17.84 Found ((eq_ref nat) b) as proof of (((eq nat) b) Xx_0) % 17.42/17.84 Found eq_ref00:=(eq_ref0 x):(((eq nat) x) x) % 17.42/17.84 Found (eq_ref0 x) as proof of (((eq nat) x) b) % 17.42/17.84 Found ((eq_ref nat) x) as proof of (((eq nat) x) b) % 17.42/17.84 Found ((eq_ref nat) x) as proof of (((eq nat) x) b) % 17.42/17.84 Found (x00 ((eq_ref nat) x)) as proof of (((eq nat) ((pl Xx) Xx_0)) b) % 17.42/17.84 Found ((x0 (fun (x2:nat)=> (((eq nat) x2) b))) ((eq_ref nat) x)) as proof of (((eq nat) ((pl Xx) Xx_0)) b) % 17.42/17.84 Found ((x0 (fun (x2:nat)=> (((eq nat) x2) b))) ((eq_ref nat) x)) as proof of (((eq nat) ((pl Xx) Xx_0)) b) % 17.42/17.84 Found ((eq_trans0000 ((x0 (fun (x2:nat)=> (((eq nat) x2) b))) ((eq_ref nat) x))) x1) as proof of (((eq nat) ((pl Xx) Xx_0)) ((pl Xx) Xy_0)) % 17.42/17.84 Found (((eq_trans000 x) ((x0 (fun (x2:nat)=> (((eq nat) x2) x))) ((eq_ref nat) x))) x1) as proof of (((eq nat) ((pl Xx) Xx_0)) ((pl Xx) Xy_0)) % 17.42/17.84 Found ((((fun (b:nat)=> ((eq_trans00 b) ((pl Xx) Xy_0))) x) ((x0 (fun (x2:nat)=> (((eq nat) x2) x))) ((eq_ref nat) x))) x1) as proof of (((eq nat) ((pl Xx) Xx_0)) ((pl Xx) Xy_0)) % 17.42/17.84 Found ((((fun (b:nat)=> (((eq_trans0 ((pl Xx) Xx_0)) b) ((pl Xx) Xy_0))) x) ((x0 (fun (x2:nat)=> (((eq nat) x2) x))) ((eq_ref nat) x))) x1) as proof of (((eq nat) ((pl Xx) Xx_0)) ((pl Xx) Xy_0)) % 17.42/17.84 Found ((((fun (b:nat)=> ((((eq_trans nat) ((pl Xx) Xx_0)) b) ((pl Xx) Xy_0))) x) ((x0 (fun (x2:nat)=> (((eq nat) x2) x))) ((eq_ref nat) x))) x1) as proof of (((eq nat) ((pl Xx) Xx_0)) ((pl Xx) Xy_0)) % 17.42/17.84 Found ((((fun (b:nat)=> ((((eq_trans nat) ((pl Xx) Xx_0)) b) ((pl Xx) Xy_0))) x) ((x0 (fun (x2:nat)=> (((eq nat) x2) x))) ((eq_ref nat) x))) x1) as proof of (((eq nat) ((pl Xx) Xx_0)) ((pl Xx) Xy_0)) % 17.42/17.84 Found (satz8a000 ((((fun (b:nat)=> ((((eq_trans nat) ((pl Xx) Xx_0)) b) ((pl Xx) Xy_0))) x) ((x0 (fun (x2:nat)=> (((eq nat) x2) x))) ((eq_ref nat) x))) x1)) as proof of (((eq nat) Xx_0) Xy_0) % 17.42/17.84 Found ((satz8a00 y) ((((fun (b:nat)=> ((((eq_trans nat) ((pl y) Xx_0)) b) ((pl y) Xy_0))) x) ((x0 (fun (x2:nat)=> (((eq nat) x2) x))) ((eq_ref nat) x))) x1)) as proof of (((eq nat) Xx_0) Xy_0) % 17.42/17.84 Found (((fun (Xx:nat)=> ((satz8a0 Xx) Xy_0)) y) ((((fun (b:nat)=> ((((eq_trans nat) ((pl y) Xx_0)) b) ((pl y) Xy_0))) x) ((x0 (fun (x2:nat)=> (((eq nat) x2) x))) ((eq_ref nat) x))) x1)) as proof of (((eq nat) Xx_0) Xy_0) % 17.42/17.84 Found (((fun (Xx:nat)=> (((fun (Xx:nat)=> ((satz8a Xx) Xx_0)) Xx) Xy_0)) y) ((((fun (b:nat)=> ((((eq_trans nat) ((pl y) Xx_0)) b) ((pl y) Xy_0))) x) ((x0 (fun (x2:nat)=> (((eq nat) x2) x))) ((eq_ref nat) x))) x1)) as proof of (((eq nat) Xx_0) Xy_0) % 17.42/17.84 Found (fun (x1:(((eq nat) x) ((pl y) Xy_0)))=> (((fun (Xx:nat)=> (((fun (Xx:nat)=> ((satz8a Xx) Xx_0)) Xx) Xy_0)) y) ((((fun (b:nat)=> ((((eq_trans nat) ((pl y) Xx_0)) b) ((pl y) Xy_0))) x) ((x0 (fun (x2:nat)=> (((eq nat) x2) x))) ((eq_ref nat) x))) x1))) as proof of (((eq nat) Xx_0) Xy_0) % 17.57/17.96 Found (fun (x0:(((eq nat) x) ((pl y) Xx_0))) (x1:(((eq nat) x) ((pl y) Xy_0)))=> (((fun (Xx:nat)=> (((fun (Xx:nat)=> ((satz8a Xx) Xx_0)) Xx) Xy_0)) y) ((((fun (b:nat)=> ((((eq_trans nat) ((pl y) Xx_0)) b) ((pl y) Xy_0))) x) ((x0 (fun (x2:nat)=> (((eq nat) x2) x))) ((eq_ref nat) x))) x1))) as proof of ((((eq nat) x) ((pl y) Xy_0))->(((eq nat) Xx_0) Xy_0)) % 17.57/17.96 Found (fun (Xy_0:nat) (x0:(((eq nat) x) ((pl y) Xx_0))) (x1:(((eq nat) x) ((pl y) Xy_0)))=> (((fun (Xx:nat)=> (((fun (Xx:nat)=> ((satz8a Xx) Xx_0)) Xx) Xy_0)) y) ((((fun (b:nat)=> ((((eq_trans nat) ((pl y) Xx_0)) b) ((pl y) Xy_0))) x) ((x0 (fun (x2:nat)=> (((eq nat) x2) x))) ((eq_ref nat) x))) x1))) as proof of ((((eq nat) x) ((pl y) Xx_0))->((((eq nat) x) ((pl y) Xy_0))->(((eq nat) Xx_0) Xy_0))) % 17.57/17.96 Found (fun (Xx_0:nat) (Xy_0:nat) (x0:(((eq nat) x) ((pl y) Xx_0))) (x1:(((eq nat) x) ((pl y) Xy_0)))=> (((fun (Xx:nat)=> (((fun (Xx:nat)=> ((satz8a Xx) Xx_0)) Xx) Xy_0)) y) ((((fun (b:nat)=> ((((eq_trans nat) ((pl y) Xx_0)) b) ((pl y) Xy_0))) x) ((x0 (fun (x2:nat)=> (((eq nat) x2) x))) ((eq_ref nat) x))) x1))) as proof of (forall (Xy_0:nat), ((((eq nat) x) ((pl y) Xx_0))->((((eq nat) x) ((pl y) Xy_0))->(((eq nat) Xx_0) Xy_0)))) % 17.57/17.96 Found (fun (Xx_0:nat) (Xy_0:nat) (x0:(((eq nat) x) ((pl y) Xx_0))) (x1:(((eq nat) x) ((pl y) Xy_0)))=> (((fun (Xx:nat)=> (((fun (Xx:nat)=> ((satz8a Xx) Xx_0)) Xx) Xy_0)) y) ((((fun (b:nat)=> ((((eq_trans nat) ((pl y) Xx_0)) b) ((pl y) Xy_0))) x) ((x0 (fun (x2:nat)=> (((eq nat) x2) x))) ((eq_ref nat) x))) x1))) as proof of (forall (Xx_0:nat) (Xy_0:nat), ((((eq nat) x) ((pl y) Xx_0))->((((eq nat) x) ((pl y) Xy_0))->(((eq nat) Xx_0) Xy_0)))) % 17.57/17.96 Got proof (fun (Xx_0:nat) (Xy_0:nat) (x0:(((eq nat) x) ((pl y) Xx_0))) (x1:(((eq nat) x) ((pl y) Xy_0)))=> (((fun (Xx:nat)=> (((fun (Xx:nat)=> ((satz8a Xx) Xx_0)) Xx) Xy_0)) y) ((((fun (b:nat)=> ((((eq_trans nat) ((pl y) Xx_0)) b) ((pl y) Xy_0))) x) ((x0 (fun (x2:nat)=> (((eq nat) x2) x))) ((eq_ref nat) x))) x1))) % 17.57/17.96 Time elapsed = 17.093361s % 17.57/17.96 node=3422 cost=1165.000000 depth=20 % 17.57/17.96:::::::::::::::::::::: % 17.57/17.96 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.57/17.96 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.57/17.96 (fun (Xx_0:nat) (Xy_0:nat) (x0:(((eq nat) x) ((pl y) Xx_0))) (x1:(((eq nat) x) ((pl y) Xy_0)))=> (((fun (Xx:nat)=> (((fun (Xx:nat)=> ((satz8a Xx) Xx_0)) Xx) Xy_0)) y) ((((fun (b:nat)=> ((((eq_trans nat) ((pl y) Xx_0)) b) ((pl y) Xy_0))) x) ((x0 (fun (x2:nat)=> (((eq nat) x2) x))) ((eq_ref nat) x))) x1))) % 17.57/17.96 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------