%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SYO085^5 : TPTP v7.5.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n005.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:50:37 EDT 2022 % Result : Theorem 2.93s 3.15s % Output : Proof 2.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : SYO085^5 : TPTP v7.5.0. Released v4.0.0. % 0.07/0.11 % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % 0.12/0.32 % Computer : n005.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % RAMPerCPU : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % DateTime : Fri Mar 11 14:40:12 EST 2022 % 0.12/0.32 % CPUTime : % 0.12/0.33 ModuleCmd_Load.c(213):ERROR:105: Unable to locate a modulefile for 'python/python27' % 0.12/0.34 Python 2.7.5 % 1.59/1.80 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 1.59/1.80 FOF formula (<kernel.Constant object at 0x122cf80>, <kernel.Sort object at 0x2b848089d638>) of role type named d % 1.59/1.80 Using role type % 1.59/1.80 Declaring d:Prop % 1.59/1.80 FOF formula (<kernel.Constant object at 0x122c4d0>, <kernel.Sort object at 0x2b848089d638>) of role type named c % 1.59/1.80 Using role type % 1.59/1.80 Declaring c:Prop % 1.59/1.80 FOF formula (<kernel.Constant object at 0x122c050>, <kernel.Sort object at 0x2b848089d638>) of role type named b % 1.59/1.80 Using role type % 1.59/1.80 Declaring b:Prop % 1.59/1.80 FOF formula (<kernel.Constant object at 0x122ce18>, <kernel.Sort object at 0x2b848089d638>) of role type named a % 1.59/1.80 Using role type % 1.59/1.80 Declaring a:Prop % 1.59/1.80 FOF formula (<kernel.Constant object at 0x122c248>, <kernel.Sort object at 0x2b848089d638>) of role type named s % 1.59/1.80 Using role type % 1.59/1.80 Declaring s:Prop % 1.59/1.80 FOF formula (((or ((or (((and c) d)->False)) (((and a) b)->False))) s)->((or ((or s) (((and a) b)->False))) (((and c) d)->False))) of role conjecture named cCOM_DMG02 % 1.59/1.80 Conjecture to prove = (((or ((or (((and c) d)->False)) (((and a) b)->False))) s)->((or ((or s) (((and a) b)->False))) (((and c) d)->False))):Prop % 1.59/1.80 We need to prove ['(((or ((or (((and c) d)->False)) (((and a) b)->False))) s)->((or ((or s) (((and a) b)->False))) (((and c) d)->False)))'] % 1.59/1.80 Parameter d:Prop. % 1.59/1.80 Parameter c:Prop. % 1.59/1.80 Parameter b:Prop. % 1.59/1.80 Parameter a:Prop. % 1.59/1.80 Parameter s:Prop. % 1.59/1.80 Trying to prove (((or ((or (((and c) d)->False)) (((and a) b)->False))) s)->((or ((or s) (((and a) b)->False))) (((and c) d)->False))) % 1.59/1.80 Found or_introl10:=(or_introl1 (((and a) b)->False)):(s->((or s) (((and a) b)->False))) % 1.59/1.80 Found (or_introl1 (((and a) b)->False)) as proof of (s->((or s) (((and a) b)->False))) % 1.59/1.80 Found ((or_introl s) (((and a) b)->False)) as proof of (s->((or s) (((and a) b)->False))) % 1.59/1.80 Found ((or_introl s) (((and a) b)->False)) as proof of (s->((or s) (((and a) b)->False))) % 1.59/1.80 Found or_introl10:=(or_introl1 (not ((and a) b))):(s->((or s) (not ((and a) b)))) % 1.59/1.80 Found (or_introl1 (not ((and a) b))) as proof of (s->((or s) (not ((and a) b)))) % 1.59/1.80 Found ((or_introl s) (not ((and a) b))) as proof of (s->((or s) (not ((and a) b)))) % 1.59/1.80 Found ((or_introl s) (not ((and a) b))) as proof of (s->((or s) (not ((and a) b)))) % 1.59/1.80 Found or_intror00:=(or_intror0 (((and a) b)->False)):((((and a) b)->False)->((or s) (((and a) b)->False))) % 1.59/1.80 Found (or_intror0 (((and a) b)->False)) as proof of ((((and a) b)->False)->((or s) (((and a) b)->False))) % 1.59/1.80 Found ((or_intror s) (((and a) b)->False)) as proof of ((((and a) b)->False)->((or s) (((and a) b)->False))) % 1.59/1.80 Found ((or_intror s) (((and a) b)->False)) as proof of ((((and a) b)->False)->((or s) (((and a) b)->False))) % 1.59/1.80 Found or_intror00:=(or_intror0 (((and c) d)->False)):((((and c) d)->False)->((or ((or s) (((and a) b)->False))) (((and c) d)->False))) % 1.59/1.80 Found (or_intror0 (((and c) d)->False)) as proof of ((((and c) d)->False)->((or ((or s) (((and a) b)->False))) (((and c) d)->False))) % 1.59/1.80 Found ((or_intror ((or s) (((and a) b)->False))) (((and c) d)->False)) as proof of ((((and c) d)->False)->((or ((or s) (((and a) b)->False))) (((and c) d)->False))) % 1.59/1.80 Found ((or_intror ((or s) (((and a) b)->False))) (((and c) d)->False)) as proof of ((((and c) d)->False)->((or ((or s) (((and a) b)->False))) (((and c) d)->False))) % 1.59/1.80 Found or_intror00:=(or_intror0 (not ((and a) b))):((not ((and a) b))->((or s) (not ((and a) b)))) % 1.59/1.80 Found (or_intror0 (not ((and a) b))) as proof of ((not ((and a) b))->((or s) (not ((and a) b)))) % 1.59/1.80 Found ((or_intror s) (not ((and a) b))) as proof of ((not ((and a) b))->((or s) (not ((and a) b)))) % 1.59/1.80 Found ((or_intror s) (not ((and a) b))) as proof of ((not ((and a) b))->((or s) (not ((and a) b)))) % 1.59/1.80 Found or_intror00:=(or_intror0 (not ((and c) d))):((not ((and c) d))->((or ((or s) (not ((and a) b)))) (not ((and c) d)))) % 1.59/1.80 Found (or_intror0 (not ((and c) d))) as proof of ((not ((and c) d))->((or ((or s) (not ((and a) b)))) (not ((and c) d)))) % 1.59/1.80 Found ((or_intror ((or s) (not ((and a) b)))) (not ((and c) d))) as proof of ((not ((and c) d))->((or ((or s) (not ((and a) b)))) (not ((and c) d)))) % 1.59/1.80 Found ((or_intror ((or s) (not ((and a) b)))) (not ((and c) d))) as proof of ((not ((and c) d))->((or ((or s) (not ((and a) b)))) (not ((and c) d)))) % 2.62/2.82 Found or_intror00:=(or_intror0 s):(s->((or (((and a) b)->False)) s)) % 2.62/2.82 Found (or_intror0 s) as proof of (s->((or (((and a) b)->False)) s)) % 2.62/2.82 Found ((or_intror (((and a) b)->False)) s) as proof of (s->((or (((and a) b)->False)) s)) % 2.62/2.82 Found ((or_intror (((and a) b)->False)) s) as proof of (s->((or (((and a) b)->False)) s)) % 2.62/2.82 Found or_introl00:=(or_introl0 (((and a) b)->False)):(s->((or s) (((and a) b)->False))) % 2.62/2.82 Found (or_introl0 (((and a) b)->False)) as proof of (s->((or s) (((and a) b)->False))) % 2.62/2.82 Found ((or_introl s) (((and a) b)->False)) as proof of (s->((or s) (((and a) b)->False))) % 2.62/2.82 Found ((or_introl s) (((and a) b)->False)) as proof of (s->((or s) (((and a) b)->False))) % 2.62/2.82 Found x0:s % 2.62/2.82 Found (fun (x0:s)=> x0) as proof of s % 2.62/2.82 Found (fun (x0:s)=> x0) as proof of (s->s) % 2.62/2.82 Found or_intror00:=(or_intror0 s):(s->((or (not ((and a) b))) s)) % 2.62/2.82 Found (or_intror0 s) as proof of (s->((or (not ((and a) b))) s)) % 2.62/2.82 Found ((or_intror (not ((and a) b))) s) as proof of (s->((or (not ((and a) b))) s)) % 2.62/2.82 Found ((or_intror (not ((and a) b))) s) as proof of (s->((or (not ((and a) b))) s)) % 2.62/2.82 Found or_introl00:=(or_introl0 (not ((and a) b))):(s->((or s) (not ((and a) b)))) % 2.62/2.82 Found (or_introl0 (not ((and a) b))) as proof of (s->((or s) (not ((and a) b)))) % 2.62/2.82 Found ((or_introl s) (not ((and a) b))) as proof of (s->((or s) (not ((and a) b)))) % 2.62/2.82 Found ((or_introl s) (not ((and a) b))) as proof of (s->((or s) (not ((and a) b)))) % 2.62/2.82 Found x0:s % 2.62/2.82 Found (fun (x0:s)=> x0) as proof of s % 2.62/2.82 Found (fun (x0:s)=> x0) as proof of (s->s) % 2.62/2.82 Found or_introl10:=(or_introl1 s):((((and a) b)->False)->((or (((and a) b)->False)) s)) % 2.62/2.82 Found (or_introl1 s) as proof of ((((and a) b)->False)->((or (((and a) b)->False)) s)) % 2.62/2.82 Found ((or_introl (((and a) b)->False)) s) as proof of ((((and a) b)->False)->((or (((and a) b)->False)) s)) % 2.62/2.82 Found ((or_introl (((and a) b)->False)) s) as proof of ((((and a) b)->False)->((or (((and a) b)->False)) s)) % 2.62/2.82 Found or_introl10:=(or_introl1 s):((((and a) b)->False)->((or (((and a) b)->False)) s)) % 2.62/2.82 Found (or_introl1 s) as proof of ((((and a) b)->False)->((or (((and a) b)->False)) s)) % 2.62/2.82 Found ((or_introl (((and a) b)->False)) s) as proof of ((((and a) b)->False)->((or (((and a) b)->False)) s)) % 2.62/2.82 Found ((or_introl (((and a) b)->False)) s) as proof of ((((and a) b)->False)->((or (((and a) b)->False)) s)) % 2.62/2.82 Found or_intror10:=(or_intror1 (((and a) b)->False)):((((and a) b)->False)->((or s) (((and a) b)->False))) % 2.62/2.82 Found (or_intror1 (((and a) b)->False)) as proof of ((((and a) b)->False)->((or s) (((and a) b)->False))) % 2.62/2.82 Found ((or_intror s) (((and a) b)->False)) as proof of ((((and a) b)->False)->((or s) (((and a) b)->False))) % 2.62/2.82 Found ((or_intror s) (((and a) b)->False)) as proof of ((((and a) b)->False)->((or s) (((and a) b)->False))) % 2.62/2.82 Found or_introl100:=(or_introl10 (((and a) b)->False)):((or s) (((and a) b)->False)) % 2.62/2.82 Found (or_introl10 (((and a) b)->False)) as proof of ((or s) (((and a) b)->False)) % 2.62/2.82 Found ((fun (B:Prop)=> ((or_introl1 B) x0)) (((and a) b)->False)) as proof of ((or s) (((and a) b)->False)) % 2.62/2.82 Found ((fun (B:Prop)=> (((or_introl s) B) x0)) (((and a) b)->False)) as proof of ((or s) (((and a) b)->False)) % 2.62/2.82 Found ((fun (B:Prop)=> (((or_introl s) B) x0)) (((and a) b)->False)) as proof of ((or s) (((and a) b)->False)) % 2.62/2.82 Found (or_introl00 ((fun (B:Prop)=> (((or_introl s) B) x0)) (((and a) b)->False))) as proof of ((or ((or s) (((and a) b)->False))) (((and c) d)->False)) % 2.62/2.82 Found ((or_introl0 (((and c) d)->False)) ((fun (B:Prop)=> (((or_introl s) B) x0)) (((and a) b)->False))) as proof of ((or ((or s) (((and a) b)->False))) (((and c) d)->False)) % 2.62/2.82 Found (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) ((fun (B:Prop)=> (((or_introl s) B) x0)) (((and a) b)->False))) as proof of ((or ((or s) (((and a) b)->False))) (((and c) d)->False)) % 2.62/2.82 Found (fun (x0:s)=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) ((fun (B:Prop)=> (((or_introl s) B) x0)) (((and a) b)->False)))) as proof of ((or ((or s) (((and a) b)->False))) (((and c) d)->False)) % 2.62/2.82 Found (fun (x0:s)=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) ((fun (B:Prop)=> (((or_introl s) B) x0)) (((and a) b)->False)))) as proof of (s->((or ((or s) (((and a) b)->False))) (((and c) d)->False))) % 2.93/3.10 Found or_introl00:=(or_introl0 ((or s) (((and a) b)->False))):((((and c) d)->False)->((or (((and c) d)->False)) ((or s) (((and a) b)->False)))) % 2.93/3.10 Found (or_introl0 ((or s) (((and a) b)->False))) as proof of ((((and c) d)->False)->((or (((and c) d)->False)) ((or s) (((and a) b)->False)))) % 2.93/3.10 Found ((or_introl (((and c) d)->False)) ((or s) (((and a) b)->False))) as proof of ((((and c) d)->False)->((or (((and c) d)->False)) ((or s) (((and a) b)->False)))) % 2.93/3.10 Found ((or_introl (((and c) d)->False)) ((or s) (((and a) b)->False))) as proof of ((((and c) d)->False)->((or (((and c) d)->False)) ((or s) (((and a) b)->False)))) % 2.93/3.10 Found or_intror00:=(or_intror0 (((and a) b)->False)):((((and a) b)->False)->((or s) (((and a) b)->False))) % 2.93/3.10 Found (or_intror0 (((and a) b)->False)) as proof of ((((and a) b)->False)->((or s) (((and a) b)->False))) % 2.93/3.10 Found ((or_intror s) (((and a) b)->False)) as proof of ((((and a) b)->False)->((or s) (((and a) b)->False))) % 2.93/3.10 Found ((or_intror s) (((and a) b)->False)) as proof of ((((and a) b)->False)->((or s) (((and a) b)->False))) % 2.93/3.10 Found or_intror000:=(or_intror00 x1):((or s) (((and a) b)->False)) % 2.93/3.10 Found (or_intror00 x1) as proof of ((or s) (((and a) b)->False)) % 2.93/3.10 Found ((or_intror0 (((and a) b)->False)) x1) as proof of ((or s) (((and a) b)->False)) % 2.93/3.10 Found (((or_intror s) (((and a) b)->False)) x1) as proof of ((or s) (((and a) b)->False)) % 2.93/3.10 Found (((or_intror s) (((and a) b)->False)) x1) as proof of ((or s) (((and a) b)->False)) % 2.93/3.10 Found (or_introl00 (((or_intror s) (((and a) b)->False)) x1)) as proof of ((or ((or s) (((and a) b)->False))) (((and c) d)->False)) % 2.93/3.10 Found ((or_introl0 (((and c) d)->False)) (((or_intror s) (((and a) b)->False)) x1)) as proof of ((or ((or s) (((and a) b)->False))) (((and c) d)->False)) % 2.93/3.10 Found (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) (((or_intror s) (((and a) b)->False)) x1)) as proof of ((or ((or s) (((and a) b)->False))) (((and c) d)->False)) % 2.93/3.10 Found (fun (x1:(((and a) b)->False))=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) (((or_intror s) (((and a) b)->False)) x1))) as proof of ((or ((or s) (((and a) b)->False))) (((and c) d)->False)) % 2.93/3.10 Found (fun (x1:(((and a) b)->False))=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) (((or_intror s) (((and a) b)->False)) x1))) as proof of ((((and a) b)->False)->((or ((or s) (((and a) b)->False))) (((and c) d)->False))) % 2.93/3.10 Found ((or_ind10 ((or_intror ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x1:(((and a) b)->False))=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) (((or_intror s) (((and a) b)->False)) x1)))) as proof of ((or ((or s) (((and a) b)->False))) (((and c) d)->False)) % 2.93/3.10 Found (((or_ind1 ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) ((or_intror ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x1:(((and a) b)->False))=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) (((or_intror s) (((and a) b)->False)) x1)))) as proof of ((or ((or s) (((and a) b)->False))) (((and c) d)->False)) % 2.93/3.10 Found ((((fun (P:Prop) (x1:((((and c) d)->False)->P)) (x2:((((and a) b)->False)->P))=> ((((((or_ind (((and c) d)->False)) (((and a) b)->False)) P) x1) x2) x0)) ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) ((or_intror ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x1:(((and a) b)->False))=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) (((or_intror s) (((and a) b)->False)) x1)))) as proof of ((or ((or s) (((and a) b)->False))) (((and c) d)->False)) % 2.93/3.10 Found (fun (x0:((or (((and c) d)->False)) (((and a) b)->False)))=> ((((fun (P:Prop) (x1:((((and c) d)->False)->P)) (x2:((((and a) b)->False)->P))=> ((((((or_ind (((and c) d)->False)) (((and a) b)->False)) P) x1) x2) x0)) ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) ((or_intror ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x1:(((and a) b)->False))=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) (((or_intror s) (((and a) b)->False)) x1))))) as proof of ((or ((or s) (((and a) b)->False))) (((and c) d)->False)) % 2.93/3.11 Found (fun (x0:((or (((and c) d)->False)) (((and a) b)->False)))=> ((((fun (P:Prop) (x1:((((and c) d)->False)->P)) (x2:((((and a) b)->False)->P))=> ((((((or_ind (((and c) d)->False)) (((and a) b)->False)) P) x1) x2) x0)) ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) ((or_intror ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x1:(((and a) b)->False))=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) (((or_intror s) (((and a) b)->False)) x1))))) as proof of (((or (((and c) d)->False)) (((and a) b)->False))->((or ((or s) (((and a) b)->False))) (((and c) d)->False))) % 2.93/3.11 Found ((or_ind00 (fun (x0:((or (((and c) d)->False)) (((and a) b)->False)))=> ((((fun (P:Prop) (x1:((((and c) d)->False)->P)) (x2:((((and a) b)->False)->P))=> ((((((or_ind (((and c) d)->False)) (((and a) b)->False)) P) x1) x2) x0)) ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) ((or_intror ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x1:(((and a) b)->False))=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) (((or_intror s) (((and a) b)->False)) x1)))))) (fun (x0:s)=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) ((fun (B:Prop)=> (((or_introl s) B) x0)) (((and a) b)->False))))) as proof of ((or ((or s) (((and a) b)->False))) (((and c) d)->False)) % 2.93/3.11 Found (((or_ind0 ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x0:((or (((and c) d)->False)) (((and a) b)->False)))=> ((((fun (P:Prop) (x1:((((and c) d)->False)->P)) (x2:((((and a) b)->False)->P))=> ((((((or_ind (((and c) d)->False)) (((and a) b)->False)) P) x1) x2) x0)) ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) ((or_intror ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x1:(((and a) b)->False))=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) (((or_intror s) (((and a) b)->False)) x1)))))) (fun (x0:s)=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) ((fun (B:Prop)=> (((or_introl s) B) x0)) (((and a) b)->False))))) as proof of ((or ((or s) (((and a) b)->False))) (((and c) d)->False)) % 2.93/3.11 Found ((((fun (P:Prop) (x0:(((or (((and c) d)->False)) (((and a) b)->False))->P)) (x1:(s->P))=> ((((((or_ind ((or (((and c) d)->False)) (((and a) b)->False))) s) P) x0) x1) x)) ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x0:((or (((and c) d)->False)) (((and a) b)->False)))=> ((((fun (P:Prop) (x1:((((and c) d)->False)->P)) (x2:((((and a) b)->False)->P))=> ((((((or_ind (((and c) d)->False)) (((and a) b)->False)) P) x1) x2) x0)) ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) ((or_intror ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x1:(((and a) b)->False))=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) (((or_intror s) (((and a) b)->False)) x1)))))) (fun (x0:s)=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) ((fun (B:Prop)=> (((or_introl s) B) x0)) (((and a) b)->False))))) as proof of ((or ((or s) (((and a) b)->False))) (((and c) d)->False)) % 2.93/3.11 Found (fun (x:((or ((or (((and c) d)->False)) (((and a) b)->False))) s))=> ((((fun (P:Prop) (x0:(((or (((and c) d)->False)) (((and a) b)->False))->P)) (x1:(s->P))=> ((((((or_ind ((or (((and c) d)->False)) (((and a) b)->False))) s) P) x0) x1) x)) ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x0:((or (((and c) d)->False)) (((and a) b)->False)))=> ((((fun (P:Prop) (x1:((((and c) d)->False)->P)) (x2:((((and a) b)->False)->P))=> ((((((or_ind (((and c) d)->False)) (((and a) b)->False)) P) x1) x2) x0)) ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) ((or_intror ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x1:(((and a) b)->False))=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) (((or_intror s) (((and a) b)->False)) x1)))))) (fun (x0:s)=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) ((fun (B:Prop)=> (((or_introl s) B) x0)) (((and a) b)->False)))))) as proof of ((or ((or s) (((and a) b)->False))) (((and c) d)->False)) % 2.93/3.15 Found (fun (x:((or ((or (((and c) d)->False)) (((and a) b)->False))) s))=> ((((fun (P:Prop) (x0:(((or (((and c) d)->False)) (((and a) b)->False))->P)) (x1:(s->P))=> ((((((or_ind ((or (((and c) d)->False)) (((and a) b)->False))) s) P) x0) x1) x)) ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x0:((or (((and c) d)->False)) (((and a) b)->False)))=> ((((fun (P:Prop) (x1:((((and c) d)->False)->P)) (x2:((((and a) b)->False)->P))=> ((((((or_ind (((and c) d)->False)) (((and a) b)->False)) P) x1) x2) x0)) ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) ((or_intror ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x1:(((and a) b)->False))=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) (((or_intror s) (((and a) b)->False)) x1)))))) (fun (x0:s)=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) ((fun (B:Prop)=> (((or_introl s) B) x0)) (((and a) b)->False)))))) as proof of (((or ((or (((and c) d)->False)) (((and a) b)->False))) s)->((or ((or s) (((and a) b)->False))) (((and c) d)->False))) % 2.93/3.15 Got proof (fun (x:((or ((or (((and c) d)->False)) (((and a) b)->False))) s))=> ((((fun (P:Prop) (x0:(((or (((and c) d)->False)) (((and a) b)->False))->P)) (x1:(s->P))=> ((((((or_ind ((or (((and c) d)->False)) (((and a) b)->False))) s) P) x0) x1) x)) ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x0:((or (((and c) d)->False)) (((and a) b)->False)))=> ((((fun (P:Prop) (x1:((((and c) d)->False)->P)) (x2:((((and a) b)->False)->P))=> ((((((or_ind (((and c) d)->False)) (((and a) b)->False)) P) x1) x2) x0)) ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) ((or_intror ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x1:(((and a) b)->False))=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) (((or_intror s) (((and a) b)->False)) x1)))))) (fun (x0:s)=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) ((fun (B:Prop)=> (((or_introl s) B) x0)) (((and a) b)->False)))))) % 2.93/3.15 Time elapsed = 2.506298s % 2.93/3.15 node=1041 cost=435.000000 depth=18 % 2.93/3.15 :::::::::::::::::::::: % 2.93/3.15 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 2.93/3.15 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % 2.93/3.15 (fun (x:((or ((or (((and c) d)->False)) (((and a) b)->False))) s))=> ((((fun (P:Prop) (x0:(((or (((and c) d)->False)) (((and a) b)->False))->P)) (x1:(s->P))=> ((((((or_ind ((or (((and c) d)->False)) (((and a) b)->False))) s) P) x0) x1) x)) ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x0:((or (((and c) d)->False)) (((and a) b)->False)))=> ((((fun (P:Prop) (x1:((((and c) d)->False)->P)) (x2:((((and a) b)->False)->P))=> ((((((or_ind (((and c) d)->False)) (((and a) b)->False)) P) x1) x2) x0)) ((or ((or s) (((and a) b)->False))) (((and c) d)->False))) ((or_intror ((or s) (((and a) b)->False))) (((and c) d)->False))) (fun (x1:(((and a) b)->False))=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) (((or_intror s) (((and a) b)->False)) x1)))))) (fun (x0:s)=> (((or_introl ((or s) (((and a) b)->False))) (((and c) d)->False)) ((fun (B:Prop)=> (((or_introl s) B) x0)) (((and a) b)->False)))))) % 2.93/3.15 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------