%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SYO274^5 : TPTP v7.5.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 0s % DateTime : Tue Mar 29 00:51:03 EDT 2022 % Result : Theorem 1.37s 1.62s % Output : Proof 1.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : SYO274^5 : TPTP v7.5.0. Released v4.0.0. % 0.10/0.12 % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.12/0.33 % Computer : n023.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % RAMPerCPU : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % DateTime : Sat Mar 12 00:27:27 EST 2022 % 0.12/0.33 % CPUTime : % 0.12/0.34 ModuleCmd_Load.c(213):ERROR:105: Unable to locate a modulefile for 'python/python27' % 0.12/0.34 Python 2.7.5 % 1.37/1.61 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox2/benchmark/', '/export/starexec/sandbox2/benchmark/'] % 1.37/1.61 FOF formula (<kernel.Constant object at 0x1b42bd8>, <kernel.Type object at 0x1b42cf8>) of role type named c_type % 1.37/1.61 Using role type % 1.37/1.61 Declaring c:Type % 1.37/1.61 FOF formula (<kernel.Constant object at 0x1b69cb0>, <kernel.Type object at 0x1b42e18>) of role type named b_type % 1.37/1.61 Using role type % 1.37/1.61 Declaring b:Type % 1.37/1.61 FOF formula (<kernel.Constant object at 0x1b42ab8>, <kernel.Type object at 0x1b42b48>) of role type named a_type % 1.37/1.61 Using role type % 1.37/1.61 Declaring a:Type % 1.37/1.61 FOF formula (<kernel.Constant object at 0x1b42a28>, <kernel.DependentProduct object at 0x2baa0d1dec68>) of role type named cG % 1.37/1.61 Using role type % 1.37/1.61 Declaring cG:(c->b) % 1.37/1.61 FOF formula (<kernel.Constant object at 0x1b42a70>, <kernel.DependentProduct object at 0x2baa0d1de368>) of role type named cF % 1.37/1.61 Using role type % 1.37/1.61 Declaring cF:(b->a) % 1.37/1.61 FOF formula (((and (forall (Xx:b) (Xy:b), ((forall (Xq:(a->Prop)), ((Xq (cF Xx))->(Xq (cF Xy))))->(forall (Xq:(b->Prop)), ((Xq Xx)->(Xq Xy)))))) (forall (Xx:c) (Xy:c), ((forall (Xq:(b->Prop)), ((Xq (cG Xx))->(Xq (cG Xy))))->(forall (Xq:(c->Prop)), ((Xq Xx)->(Xq Xy))))))->(forall (Xx:c) (Xy:c), ((forall (Xq:(a->Prop)), ((Xq (cF (cG Xx)))->(Xq (cF (cG Xy)))))->(forall (Xq:(c->Prop)), ((Xq Xx)->(Xq Xy)))))) of role conjecture named cTHM48_EXPD % 1.37/1.61 Conjecture to prove = (((and (forall (Xx:b) (Xy:b), ((forall (Xq:(a->Prop)), ((Xq (cF Xx))->(Xq (cF Xy))))->(forall (Xq:(b->Prop)), ((Xq Xx)->(Xq Xy)))))) (forall (Xx:c) (Xy:c), ((forall (Xq:(b->Prop)), ((Xq (cG Xx))->(Xq (cG Xy))))->(forall (Xq:(c->Prop)), ((Xq Xx)->(Xq Xy))))))->(forall (Xx:c) (Xy:c), ((forall (Xq:(a->Prop)), ((Xq (cF (cG Xx)))->(Xq (cF (cG Xy)))))->(forall (Xq:(c->Prop)), ((Xq Xx)->(Xq Xy)))))):Prop % 1.37/1.61 Parameter c_DUMMY:c. % 1.37/1.61 Parameter b_DUMMY:b. % 1.37/1.61 Parameter a_DUMMY:a. % 1.37/1.61 We need to prove ['(((and (forall (Xx:b) (Xy:b), ((forall (Xq:(a->Prop)), ((Xq (cF Xx))->(Xq (cF Xy))))->(forall (Xq:(b->Prop)), ((Xq Xx)->(Xq Xy)))))) (forall (Xx:c) (Xy:c), ((forall (Xq:(b->Prop)), ((Xq (cG Xx))->(Xq (cG Xy))))->(forall (Xq:(c->Prop)), ((Xq Xx)->(Xq Xy))))))->(forall (Xx:c) (Xy:c), ((forall (Xq:(a->Prop)), ((Xq (cF (cG Xx)))->(Xq (cF (cG Xy)))))->(forall (Xq:(c->Prop)), ((Xq Xx)->(Xq Xy))))))'] % 1.37/1.61 Parameter c:Type. % 1.37/1.61 Parameter b:Type. % 1.37/1.61 Parameter a:Type. % 1.37/1.61 Parameter cG:(c->b). % 1.37/1.61 Parameter cF:(b->a). % 1.37/1.61 Trying to prove (((and (forall (Xx:b) (Xy:b), ((forall (Xq:(a->Prop)), ((Xq (cF Xx))->(Xq (cF Xy))))->(forall (Xq:(b->Prop)), ((Xq Xx)->(Xq Xy)))))) (forall (Xx:c) (Xy:c), ((forall (Xq:(b->Prop)), ((Xq (cG Xx))->(Xq (cG Xy))))->(forall (Xq:(c->Prop)), ((Xq Xx)->(Xq Xy))))))->(forall (Xx:c) (Xy:c), ((forall (Xq:(a->Prop)), ((Xq (cF (cG Xx)))->(Xq (cF (cG Xy)))))->(forall (Xq:(c->Prop)), ((Xq Xx)->(Xq Xy)))))) % 1.37/1.61 Found x1000:=(x100 x0):(((eq b) (cG Xx)) (cG Xy)) % 1.37/1.61 Found (x100 x0) as proof of (((eq b) (cG Xx)) (cG Xy)) % 1.37/1.61 Found ((x10 (cG Xy)) x0) as proof of (((eq b) (cG Xx)) (cG Xy)) % 1.37/1.61 Found (((x1 (cG Xx)) (cG Xy)) x0) as proof of (((eq b) (cG Xx)) (cG Xy)) % 1.37/1.61 Found (((x1 (cG Xx)) (cG Xy)) x0) as proof of (((eq b) (cG Xx)) (cG Xy)) % 1.37/1.61 Found (x200 (((x1 (cG Xx)) (cG Xy)) x0)) as proof of (((eq c) Xx) Xy) % 1.37/1.61 Found ((x20 Xy) (((x1 (cG Xx)) (cG Xy)) x0)) as proof of (((eq c) Xx) Xy) % 1.37/1.61 Found (((x2 Xx) Xy) (((x1 (cG Xx)) (cG Xy)) x0)) as proof of (((eq c) Xx) Xy) % 1.37/1.61 Found (fun (x2:(forall (Xx0:c) (Xy0:c), ((((eq b) (cG Xx0)) (cG Xy0))->(((eq c) Xx0) Xy0))))=> (((x2 Xx) Xy) (((x1 (cG Xx)) (cG Xy)) x0))) as proof of (((eq c) Xx) Xy) % 1.37/1.61 Found (fun (x1:(forall (Xx0:b) (Xy0:b), ((((eq a) (cF Xx0)) (cF Xy0))->(((eq b) Xx0) Xy0)))) (x2:(forall (Xx0:c) (Xy0:c), ((((eq b) (cG Xx0)) (cG Xy0))->(((eq c) Xx0) Xy0))))=> (((x2 Xx) Xy) (((x1 (cG Xx)) (cG Xy)) x0))) as proof of ((forall (Xx0:c) (Xy0:c), ((((eq b) (cG Xx0)) (cG Xy0))->(((eq c) Xx0) Xy0)))->(((eq c) Xx) Xy)) % 1.37/1.61 Found (fun (x1:(forall (Xx0:b) (Xy0:b), ((((eq a) (cF Xx0)) (cF Xy0))->(((eq b) Xx0) Xy0)))) (x2:(forall (Xx0:c) (Xy0:c), ((((eq b) (cG Xx0)) (cG Xy0))->(((eq c) Xx0) Xy0))))=> (((x2 Xx) Xy) (((x1 (cG Xx)) (cG Xy)) x0))) as proof of ((forall (Xx0:b) (Xy0:b), ((((eq a) (cF Xx0)) (cF Xy0))->(((eq b) Xx0) Xy0)))->((forall (Xx0:c) (Xy0:c), ((((eq b) (cG Xx0)) (cG Xy0))->(((eq c) Xx0) Xy0)))->(((eq c) Xx) Xy))) % 1.37/1.61 Found (and_rect00 (fun (x1:(forall (Xx0:b) (Xy0:b), ((((eq a) (cF Xx0)) (cF Xy0))->(((eq b) Xx0) Xy0)))) (x2:(forall (Xx0:c) (Xy0:c), ((((eq b) (cG Xx0)) (cG Xy0))->(((eq c) Xx0) Xy0))))=> (((x2 Xx) Xy) (((x1 (cG Xx)) (cG Xy)) x0)))) as proof of (((eq c) Xx) Xy) % 1.37/1.61 Found ((and_rect0 (((eq c) Xx) Xy)) (fun (x1:(forall (Xx0:b) (Xy0:b), ((((eq a) (cF Xx0)) (cF Xy0))->(((eq b) Xx0) Xy0)))) (x2:(forall (Xx0:c) (Xy0:c), ((((eq b) (cG Xx0)) (cG Xy0))->(((eq c) Xx0) Xy0))))=> (((x2 Xx) Xy) (((x1 (cG Xx)) (cG Xy)) x0)))) as proof of (((eq c) Xx) Xy) % 1.37/1.61 Found (((fun (P:Type) (x1:((forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))->((forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))->P)))=> (((((and_rect (forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))) (forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))) P) x1) x)) (((eq c) Xx) Xy)) (fun (x1:(forall (Xx0:b) (Xy0:b), ((((eq a) (cF Xx0)) (cF Xy0))->(((eq b) Xx0) Xy0)))) (x2:(forall (Xx0:c) (Xy0:c), ((((eq b) (cG Xx0)) (cG Xy0))->(((eq c) Xx0) Xy0))))=> (((x2 Xx) Xy) (((x1 (cG Xx)) (cG Xy)) x0)))) as proof of (((eq c) Xx) Xy) % 1.37/1.61 Found (fun (x0:(((eq a) (cF (cG Xx))) (cF (cG Xy))))=> (((fun (P:Type) (x1:((forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))->((forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))->P)))=> (((((and_rect (forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))) (forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))) P) x1) x)) (((eq c) Xx) Xy)) (fun (x1:(forall (Xx0:b) (Xy0:b), ((((eq a) (cF Xx0)) (cF Xy0))->(((eq b) Xx0) Xy0)))) (x2:(forall (Xx0:c) (Xy0:c), ((((eq b) (cG Xx0)) (cG Xy0))->(((eq c) Xx0) Xy0))))=> (((x2 Xx) Xy) (((x1 (cG Xx)) (cG Xy)) x0))))) as proof of (((eq c) Xx) Xy) % 1.37/1.61 Found (fun (Xy:c) (x0:(((eq a) (cF (cG Xx))) (cF (cG Xy))))=> (((fun (P:Type) (x1:((forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))->((forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))->P)))=> (((((and_rect (forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))) (forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))) P) x1) x)) (((eq c) Xx) Xy)) (fun (x1:(forall (Xx0:b) (Xy0:b), ((((eq a) (cF Xx0)) (cF Xy0))->(((eq b) Xx0) Xy0)))) (x2:(forall (Xx0:c) (Xy0:c), ((((eq b) (cG Xx0)) (cG Xy0))->(((eq c) Xx0) Xy0))))=> (((x2 Xx) Xy) (((x1 (cG Xx)) (cG Xy)) x0))))) as proof of ((((eq a) (cF (cG Xx))) (cF (cG Xy)))->(((eq c) Xx) Xy)) % 1.37/1.61 Found (fun (Xx:c) (Xy:c) (x0:(((eq a) (cF (cG Xx))) (cF (cG Xy))))=> (((fun (P:Type) (x1:((forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))->((forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))->P)))=> (((((and_rect (forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))) (forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))) P) x1) x)) (((eq c) Xx) Xy)) (fun (x1:(forall (Xx0:b) (Xy0:b), ((((eq a) (cF Xx0)) (cF Xy0))->(((eq b) Xx0) Xy0)))) (x2:(forall (Xx0:c) (Xy0:c), ((((eq b) (cG Xx0)) (cG Xy0))->(((eq c) Xx0) Xy0))))=> (((x2 Xx) Xy) (((x1 (cG Xx)) (cG Xy)) x0))))) as proof of (forall (Xy:c), ((((eq a) (cF (cG Xx))) (cF (cG Xy)))->(((eq c) Xx) Xy))) % 1.37/1.61 Found (fun (x:((and (forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))) (forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy))))) (Xx:c) (Xy:c) (x0:(((eq a) (cF (cG Xx))) (cF (cG Xy))))=> (((fun (P:Type) (x1:((forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))->((forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))->P)))=> (((((and_rect (forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))) (forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))) P) x1) x)) (((eq c) Xx) Xy)) (fun (x1:(forall (Xx0:b) (Xy0:b), ((((eq a) (cF Xx0)) (cF Xy0))->(((eq b) Xx0) Xy0)))) (x2:(forall (Xx0:c) (Xy0:c), ((((eq b) (cG Xx0)) (cG Xy0))->(((eq c) Xx0) Xy0))))=> (((x2 Xx) Xy) (((x1 (cG Xx)) (cG Xy)) x0))))) as proof of (forall (Xx:c) (Xy:c), ((((eq a) (cF (cG Xx))) (cF (cG Xy)))->(((eq c) Xx) Xy))) % 1.37/1.62 Found (fun (x:((and (forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))) (forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy))))) (Xx:c) (Xy:c) (x0:(((eq a) (cF (cG Xx))) (cF (cG Xy))))=> (((fun (P:Type) (x1:((forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))->((forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))->P)))=> (((((and_rect (forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))) (forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))) P) x1) x)) (((eq c) Xx) Xy)) (fun (x1:(forall (Xx0:b) (Xy0:b), ((((eq a) (cF Xx0)) (cF Xy0))->(((eq b) Xx0) Xy0)))) (x2:(forall (Xx0:c) (Xy0:c), ((((eq b) (cG Xx0)) (cG Xy0))->(((eq c) Xx0) Xy0))))=> (((x2 Xx) Xy) (((x1 (cG Xx)) (cG Xy)) x0))))) as proof of (((and (forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))) (forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy))))->(forall (Xx:c) (Xy:c), ((((eq a) (cF (cG Xx))) (cF (cG Xy)))->(((eq c) Xx) Xy)))) % 1.37/1.62 Found (fun (x:((and (forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))) (forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy))))) (Xx:c) (Xy:c) (x0:(((eq a) (cF (cG Xx))) (cF (cG Xy))))=> (((fun (P:Type) (x1:((forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))->((forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))->P)))=> (((((and_rect (forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))) (forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))) P) x1) x)) (((eq c) Xx) Xy)) (fun (x1:(forall (Xx0:b) (Xy0:b), ((((eq a) (cF Xx0)) (cF Xy0))->(((eq b) Xx0) Xy0)))) (x2:(forall (Xx0:c) (Xy0:c), ((((eq b) (cG Xx0)) (cG Xy0))->(((eq c) Xx0) Xy0))))=> (((x2 Xx) Xy) (((x1 (cG Xx)) (cG Xy)) x0))))) as proof of (((and (forall (Xx:b) (Xy:b), ((forall (Xq:(a->Prop)), ((Xq (cF Xx))->(Xq (cF Xy))))->(forall (Xq:(b->Prop)), ((Xq Xx)->(Xq Xy)))))) (forall (Xx:c) (Xy:c), ((forall (Xq:(b->Prop)), ((Xq (cG Xx))->(Xq (cG Xy))))->(forall (Xq:(c->Prop)), ((Xq Xx)->(Xq Xy))))))->(forall (Xx:c) (Xy:c), ((forall (Xq:(a->Prop)), ((Xq (cF (cG Xx)))->(Xq (cF (cG Xy)))))->(forall (Xq:(c->Prop)), ((Xq Xx)->(Xq Xy)))))) % 1.37/1.62 Got proof (fun (x:((and (forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))) (forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy))))) (Xx:c) (Xy:c) (x0:(((eq a) (cF (cG Xx))) (cF (cG Xy))))=> (((fun (P:Type) (x1:((forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))->((forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))->P)))=> (((((and_rect (forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))) (forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))) P) x1) x)) (((eq c) Xx) Xy)) (fun (x1:(forall (Xx0:b) (Xy0:b), ((((eq a) (cF Xx0)) (cF Xy0))->(((eq b) Xx0) Xy0)))) (x2:(forall (Xx0:c) (Xy0:c), ((((eq b) (cG Xx0)) (cG Xy0))->(((eq c) Xx0) Xy0))))=> (((x2 Xx) Xy) (((x1 (cG Xx)) (cG Xy)) x0))))) % 1.37/1.62 Time elapsed = 1.015630s % 1.37/1.62 node=196 cost=370.000000 depth=18 % 1.37/1.62 :::::::::::::::::::::: % 1.37/1.62 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.37/1.62 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.37/1.62 (fun (x:((and (forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))) (forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy))))) (Xx:c) (Xy:c) (x0:(((eq a) (cF (cG Xx))) (cF (cG Xy))))=> (((fun (P:Type) (x1:((forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))->((forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))->P)))=> (((((and_rect (forall (Xx:b) (Xy:b), ((((eq a) (cF Xx)) (cF Xy))->(((eq b) Xx) Xy)))) (forall (Xx:c) (Xy:c), ((((eq b) (cG Xx)) (cG Xy))->(((eq c) Xx) Xy)))) P) x1) x)) (((eq c) Xx) Xy)) (fun (x1:(forall (Xx0:b) (Xy0:b), ((((eq a) (cF Xx0)) (cF Xy0))->(((eq b) Xx0) Xy0)))) (x2:(forall (Xx0:c) (Xy0:c), ((((eq b) (cG Xx0)) (cG Xy0))->(((eq c) Xx0) Xy0))))=> (((x2 Xx) Xy) (((x1 (cG Xx)) (cG Xy)) x0))))) % 1.37/1.62 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------