%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEV185^5 : TPTP v6.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n094.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32286.75MB % OS : Linux 2.6.32-431.20.3.el6.x86_64 % CPULimit : 300s % DateTime : Thu Jul 17 13:33:51 EDT 2014 % Result : Theorem 1.54s % Output : Proof 1.54s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEV185^5 : TPTP v6.1.0. Released v4.0.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n094.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 32286.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Thu Jul 17 08:24:06 CDT 2014 % % CPUTime : 1.54 % Python 2.7.5 % Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % FOF formula (<kernel.Constant object at 0xc5b9e0>, <kernel.Type object at 0xc5b1b8>) of role type named b_type % Using role type % Declaring b:Type % FOF formula (forall (P:((b->Prop)->(b->Prop))) (S:((b->Prop)->Prop)), ((forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Xy))->(Xx Xy)))))->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))->(forall (S0:(b->Prop)), ((S S0)->(S0 Xy))))))) of role conjecture named cTHM564_pme % Conjecture to prove = (forall (P:((b->Prop)->(b->Prop))) (S:((b->Prop)->Prop)), ((forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Xy))->(Xx Xy)))))->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))->(forall (S0:(b->Prop)), ((S S0)->(S0 Xy))))))):Prop % Parameter b_DUMMY:b. % We need to prove ['(forall (P:((b->Prop)->(b->Prop))) (S:((b->Prop)->Prop)), ((forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Xy))->(Xx Xy)))))->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))->(forall (S0:(b->Prop)), ((S S0)->(S0 Xy)))))))'] % Parameter b:Type. % Trying to prove (forall (P:((b->Prop)->(b->Prop))) (S:((b->Prop)->Prop)), ((forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Xy))->(Xx Xy)))))->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))->(forall (S0:(b->Prop)), ((S S0)->(S0 Xy))))))) % Found x1:(S S0) % Found x1 as proof of (S S00) % Found x3:(X0 Xx0) % Found x3 as proof of (S0 Xx0) % Found (fun (x3:(X0 Xx0))=> x3) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x3:(X0 Xx0))=> x3) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x3:(X0 Xx0))=> x3) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x3:(X0 Xx0) % Found x3 as proof of (S0 Xx0) % Found (fun (x3:(X0 Xx0))=> x3) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x3:(X0 Xx0))=> x3) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x3:(X0 Xx0))=> x3) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x3:((P X) Xy) % Instantiate: X0:=X:(b->Prop) % Found x3 as proof of ((P X0) Xy) % Found x3:((P X) Xy) % Instantiate: X0:=X:(b->Prop) % Found x3 as proof of ((P X0) Xy) % Found x5:(X0 Xx0) % Found x5 as proof of (S0 Xx0) % Found (fun (x5:(X0 Xx0))=> x5) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x5:(X0 Xx0))=> x5) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x5:(X0 Xx0))=> x5) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x5:(X0 Xx0) % Found x5 as proof of (S0 Xx0) % Found (fun (x5:(X0 Xx0))=> x5) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x5:(X0 Xx0))=> x5) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x5:(X0 Xx0))=> x5) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x4:((P X) Xy) % Instantiate: X0:=X:(b->Prop) % Found (fun (x4:((P X) Xy))=> x4) as proof of ((P X0) Xy) % Found (fun (x3:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x4:((P X) Xy))=> x4) as proof of (((P X) Xy)->((P X0) Xy)) % Found (fun (x3:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x4:((P X) Xy))=> x4) as proof of ((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->((P X0) Xy))) % Found (and_rect00 (fun (x3:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x4:((P X) Xy))=> x4)) as proof of ((P X0) Xy) % Found ((and_rect0 ((P X0) Xy)) (fun (x3:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x4:((P X) Xy))=> x4)) as proof of ((P X0) Xy) % Found (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy)) P0) x3) x0)) ((P X0) Xy)) (fun (x3:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x4:((P X) Xy))=> x4)) as proof of ((P X0) Xy) % Found (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy)) P0) x3) x0)) ((P X0) Xy)) (fun (x3:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x4:((P X) Xy))=> x4)) as proof of ((P X0) Xy) % Found x4:((P X) Xy) % Instantiate: X0:=X:(b->Prop) % Found (fun (x4:((P X) Xy))=> x4) as proof of ((P X0) Xy) % Found (fun (x3:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x4:((P X) Xy))=> x4) as proof of (((P X) Xy)->((P X0) Xy)) % Found (fun (x3:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x4:((P X) Xy))=> x4) as proof of ((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->((P X0) Xy))) % Found (and_rect00 (fun (x3:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x4:((P X) Xy))=> x4)) as proof of ((P X0) Xy) % Found ((and_rect0 ((P X0) Xy)) (fun (x3:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x4:((P X) Xy))=> x4)) as proof of ((P X0) Xy) % Found (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy)) P0) x3) x0)) ((P X0) Xy)) (fun (x3:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x4:((P X) Xy))=> x4)) as proof of ((P X0) Xy) % Found (((fun (P0:Type) (x3:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy)) P0) x3) x0)) ((P X0) Xy)) (fun (x3:(forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) (x4:((P X) Xy))=> x4)) as proof of ((P X0) Xy) % Found x4:((P X) Xy) % Instantiate: X0:=X:(b->Prop) % Found x4 as proof of ((P X0) Xy) % Found x4:((P X) Xy) % Instantiate: X0:=X:(b->Prop) % Found x4 as proof of ((P X0) Xy) % Found x5:(X0 Xx0) % Instantiate: X0:=S0:(b->Prop) % Found x5 as proof of (S0 Xx0) % Found (fun (x5:(X0 Xx0))=> x5) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x5:(X0 Xx0))=> x5) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x5:(X0 Xx0))=> x5) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x5:(X0 Xx0) % Instantiate: X0:=S0:(b->Prop) % Found x5 as proof of (S0 Xx0) % Found (fun (x5:(X0 Xx0))=> x5) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x5:(X0 Xx0))=> x5) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x5:(X0 Xx0))=> x5) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found x20000:=(x2000 x1):(S0 Xx0) % Found (x2000 x1) as proof of (S0 Xx0) % Found ((x200 S0) x1) as proof of (S0 Xx0) % Found (((x20 x5) S0) x1) as proof of (S0 Xx0) % Found ((((x2 Xx0) x5) S0) x1) as proof of (S0 Xx0) % Found (fun (x5:(X0 Xx0))=> ((((x2 Xx0) x5) S0) x1)) as proof of (S0 Xx0) % Found (fun (Xx0:b) (x5:(X0 Xx0))=> ((((x2 Xx0) x5) S0) x1)) as proof of ((X0 Xx0)->(S0 Xx0)) % Found (fun (Xx0:b) (x5:(X0 Xx0))=> ((((x2 Xx0) x5) S0) x1)) as proof of (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0))) % Found ((conj00 (fun (Xx0:b) (x5:(X0 Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3) as proof of ((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Xy)) % Found (((conj0 ((P X0) Xy)) (fun (Xx0:b) (x5:(X0 Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3) as proof of ((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Xy)) % Found ((((conj (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Xy)) (fun (Xx0:b) (x5:(X0 Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3) as proof of ((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Xy)) % Found ((((conj (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Xy)) (fun (Xx0:b) (x5:(X0 Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3) as proof of ((and (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Xy)) % Found (x4000 ((((conj (forall (Xx0:b), ((X0 Xx0)->(S0 Xx0)))) ((P X0) Xy)) (fun (Xx0:b) (x5:(X0 Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3)) as proof of (S0 Xy) % Found ((x400 X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3)) as proof of (S0 Xy) % Found (((fun (X0:(b->Prop))=> ((x40 X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3)) as proof of (S0 Xy) % Found (((fun (X0:(b->Prop))=> (((x4 x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3)) as proof of (S0 Xy) % Found (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3)) as proof of (S0 Xy) % Found (fun (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3))) as proof of (S0 Xy) % Found (fun (x2:(forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))) (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3))) as proof of (((P X) Xy)->(S0 Xy)) % Found (fun (x2:(forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))) (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3))) as proof of ((forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))->(((P X) Xy)->(S0 Xy))) % Found (and_rect00 (fun (x2:(forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))) (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3)))) as proof of (S0 Xy) % Found ((and_rect0 (S0 Xy)) (fun (x2:(forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))) (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3)))) as proof of (S0 Xy) % Found (((fun (P0:Type) (x2:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy)) P0) x2) x0)) (S0 Xy)) (fun (x2:(forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))) (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3)))) as proof of (S0 Xy) % Found (fun (x1:(S S0))=> (((fun (P0:Type) (x2:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy)) P0) x2) x0)) (S0 Xy)) (fun (x2:(forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))) (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3))))) as proof of (S0 Xy) % Found (fun (S0:(b->Prop)) (x1:(S S0))=> (((fun (P0:Type) (x2:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy)) P0) x2) x0)) (S0 Xy)) (fun (x2:(forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))) (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3))))) as proof of ((S S0)->(S0 Xy)) % Found (fun (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))) (S0:(b->Prop)) (x1:(S S0))=> (((fun (P0:Type) (x2:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy)) P0) x2) x0)) (S0 Xy)) (fun (x2:(forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))) (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3))))) as proof of (forall (S0:(b->Prop)), ((S S0)->(S0 Xy))) % Found (fun (Xy:b) (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))) (S0:(b->Prop)) (x1:(S S0))=> (((fun (P0:Type) (x2:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy)) P0) x2) x0)) (S0 Xy)) (fun (x2:(forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))) (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3))))) as proof of (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))->(forall (S0:(b->Prop)), ((S S0)->(S0 Xy)))) % Found (fun (X:(b->Prop)) (Xy:b) (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))) (S0:(b->Prop)) (x1:(S S0))=> (((fun (P0:Type) (x2:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy)) P0) x2) x0)) (S0 Xy)) (fun (x2:(forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))) (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3))))) as proof of (forall (Xy:b), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))->(forall (S0:(b->Prop)), ((S S0)->(S0 Xy))))) % Found (fun (x:(forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Xy))->(Xx Xy)))))) (X:(b->Prop)) (Xy:b) (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))) (S0:(b->Prop)) (x1:(S S0))=> (((fun (P0:Type) (x2:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy)) P0) x2) x0)) (S0 Xy)) (fun (x2:(forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))) (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3))))) as proof of (forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))->(forall (S0:(b->Prop)), ((S S0)->(S0 Xy))))) % Found (fun (S:((b->Prop)->Prop)) (x:(forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Xy))->(Xx Xy)))))) (X:(b->Prop)) (Xy:b) (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))) (S0:(b->Prop)) (x1:(S S0))=> (((fun (P0:Type) (x2:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy)) P0) x2) x0)) (S0 Xy)) (fun (x2:(forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))) (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3))))) as proof of ((forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Xy))->(Xx Xy)))))->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))->(forall (S0:(b->Prop)), ((S S0)->(S0 Xy)))))) % Found (fun (P:((b->Prop)->(b->Prop))) (S:((b->Prop)->Prop)) (x:(forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Xy))->(Xx Xy)))))) (X:(b->Prop)) (Xy:b) (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))) (S0:(b->Prop)) (x1:(S S0))=> (((fun (P0:Type) (x2:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy)) P0) x2) x0)) (S0 Xy)) (fun (x2:(forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))) (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3))))) as proof of (forall (S:((b->Prop)->Prop)), ((forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Xy))->(Xx Xy)))))->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))->(forall (S0:(b->Prop)), ((S S0)->(S0 Xy))))))) % Found (fun (P:((b->Prop)->(b->Prop))) (S:((b->Prop)->Prop)) (x:(forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Xy))->(Xx Xy)))))) (X:(b->Prop)) (Xy:b) (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))) (S0:(b->Prop)) (x1:(S S0))=> (((fun (P0:Type) (x2:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy)) P0) x2) x0)) (S0 Xy)) (fun (x2:(forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))) (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3))))) as proof of (forall (P:((b->Prop)->(b->Prop))) (S:((b->Prop)->Prop)), ((forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Xy))->(Xx Xy)))))->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))->(forall (S0:(b->Prop)), ((S S0)->(S0 Xy))))))) % Got proof (fun (P:((b->Prop)->(b->Prop))) (S:((b->Prop)->Prop)) (x:(forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Xy))->(Xx Xy)))))) (X:(b->Prop)) (Xy:b) (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))) (S0:(b->Prop)) (x1:(S S0))=> (((fun (P0:Type) (x2:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy)) P0) x2) x0)) (S0 Xy)) (fun (x2:(forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))) (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3))))) % Time elapsed = 1.220782s % node=279 cost=925.000000 depth=30 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (P:((b->Prop)->(b->Prop))) (S:((b->Prop)->Prop)) (x:(forall (Xx:(b->Prop)), ((S Xx)->(forall (X:(b->Prop)) (Xy:b), (((and (forall (Xx0:b), ((X Xx0)->(Xx Xx0)))) ((P X) Xy))->(Xx Xy)))))) (X:(b->Prop)) (Xy:b) (x0:((and (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy))) (S0:(b->Prop)) (x1:(S S0))=> (((fun (P0:Type) (x2:((forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))->(((P X) Xy)->P0)))=> (((((and_rect (forall (Xx:b), ((X Xx)->(forall (S0:(b->Prop)), ((S S0)->(S0 Xx)))))) ((P X) Xy)) P0) x2) x0)) (S0 Xy)) (fun (x2:(forall (Xx:b), ((X Xx)->(forall (S00:(b->Prop)), ((S S00)->(S00 Xx)))))) (x3:((P X) Xy))=> (((fun (X0:(b->Prop))=> ((((x S0) x1) X0) Xy)) X) ((((conj (forall (Xx0:b), ((X Xx0)->(S0 Xx0)))) ((P X) Xy)) (fun (Xx0:b) (x5:(X Xx0))=> ((((x2 Xx0) x5) S0) x1))) x3))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------