%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SYO379^5 : TPTP v7.5.0. Bugfixed v5.2.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n026.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:18 EDT 2022 % Result : Theorem 0.68s 0.84s % Output : Proof 0.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SYO379^5 : TPTP v7.5.0. Bugfixed v5.2.0. % 0.04/0.12 % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % 0.14/0.34 % Computer : n026.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % RAMPerCPU : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % DateTime : Sat Mar 12 09:42:21 EST 2022 % 0.14/0.34 % CPUTime : % 0.14/0.34 ModuleCmd_Load.c(213):ERROR:105: Unable to locate a modulefile for 'python/python27' % 0.14/0.34 Python 2.7.5 % 0.61/0.83 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 0.61/0.83 FOF formula (<kernel.Constant object at 0x1192dd0>, <kernel.Constant object at 0x1192ef0>) of role type named c_type % 0.61/0.83 Using role type % 0.61/0.83 Declaring c:fofType % 0.61/0.83 FOF formula (<kernel.Constant object at 0x1193e18>, <kernel.DependentProduct object at 0x1192f80>) of role type named cQDP0_type % 0.61/0.83 Using role type % 0.61/0.83 Declaring cQDP0:(fofType->Prop) % 0.61/0.83 FOF formula (<kernel.Constant object at 0x1192dd0>, <kernel.DependentProduct object at 0x1192a70>) of role type named cQDP1_type % 0.61/0.83 Using role type % 0.61/0.83 Declaring cQDP1:((fofType->Prop)->Prop) % 0.61/0.83 FOF formula (((eq (fofType->Prop)) cQDP0) (fun (Xz:fofType)=> (((eq fofType) Xz) c))) of role definition named cQDP0_def % 0.61/0.83 A new definition: (((eq (fofType->Prop)) cQDP0) (fun (Xz:fofType)=> (((eq fofType) Xz) c))) % 0.61/0.83 Defined: cQDP0:=(fun (Xz:fofType)=> (((eq fofType) Xz) c)) % 0.61/0.83 FOF formula (((eq ((fofType->Prop)->Prop)) cQDP1) (fun (Xz:(fofType->Prop))=> ((and (((eq (fofType->Prop)) Xz) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (Xz Xt)))))) of role definition named cQDP1_def % 0.61/0.83 A new definition: (((eq ((fofType->Prop)->Prop)) cQDP1) (fun (Xz:(fofType->Prop))=> ((and (((eq (fofType->Prop)) Xz) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (Xz Xt)))))) % 0.61/0.83 Defined: cQDP1:=(fun (Xz:(fofType->Prop))=> ((and (((eq (fofType->Prop)) Xz) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (Xz Xt))))) % 0.61/0.83 FOF formula ((ex (fofType->Prop)) (fun (Xs:(fofType->Prop))=> (cQDP1 Xs))) of role conjecture named cQDTHM1 % 0.61/0.83 Conjecture to prove = ((ex (fofType->Prop)) (fun (Xs:(fofType->Prop))=> (cQDP1 Xs))):Prop % 0.61/0.83 We need to prove ['((ex (fofType->Prop)) (fun (Xs:(fofType->Prop))=> (cQDP1 Xs)))'] % 0.61/0.83 Parameter fofType:Type. % 0.61/0.83 Parameter c:fofType. % 0.61/0.83 Definition cQDP0:=(fun (Xz:fofType)=> (((eq fofType) Xz) c)):(fofType->Prop). % 0.61/0.83 Definition cQDP1:=(fun (Xz:(fofType->Prop))=> ((and (((eq (fofType->Prop)) Xz) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (Xz Xt))))):((fofType->Prop)->Prop). % 0.61/0.83 Trying to prove ((ex (fofType->Prop)) (fun (Xs:(fofType->Prop))=> (cQDP1 Xs))) % 0.61/0.83 Found eq_ref00:=(eq_ref0 x):(((eq (fofType->Prop)) x) x) % 0.61/0.83 Found (eq_ref0 x) as proof of (((eq (fofType->Prop)) x) cQDP0) % 0.61/0.83 Found ((eq_ref (fofType->Prop)) x) as proof of (((eq (fofType->Prop)) x) cQDP0) % 0.61/0.83 Found ((eq_ref (fofType->Prop)) x) as proof of (((eq (fofType->Prop)) x) cQDP0) % 0.61/0.83 Found ((eq_ref (fofType->Prop)) x) as proof of (((eq (fofType->Prop)) x) cQDP0) % 0.61/0.83 Found eq_ref00:=(eq_ref0 x):(((eq (fofType->Prop)) x) x) % 0.61/0.83 Found (eq_ref0 x) as proof of (((eq (fofType->Prop)) x) cQDP0) % 0.61/0.83 Found ((eq_ref (fofType->Prop)) x) as proof of (((eq (fofType->Prop)) x) cQDP0) % 0.61/0.83 Found ((eq_ref (fofType->Prop)) x) as proof of (((eq (fofType->Prop)) x) cQDP0) % 0.61/0.83 Found ((eq_ref (fofType->Prop)) x) as proof of (((eq (fofType->Prop)) x) cQDP0) % 0.61/0.83 Found x1:(P x0) % 0.61/0.83 Instantiate: x0:=c:fofType % 0.61/0.83 Found (fun (x1:(P x0))=> x1) as proof of (P c) % 0.61/0.83 Found (fun (P:(fofType->Prop)) (x1:(P x0))=> x1) as proof of ((P x0)->(P c)) % 0.61/0.83 Found (fun (P:(fofType->Prop)) (x1:(P x0))=> x1) as proof of (x x0) % 0.61/0.83 Found (ex_intro100 (fun (P:(fofType->Prop)) (x1:(P x0))=> x1)) as proof of ((ex fofType) (fun (Xt:fofType)=> (x Xt))) % 0.61/0.83 Found ((ex_intro10 c) (fun (P:(fofType->Prop)) (x1:(P c))=> x1)) as proof of ((ex fofType) (fun (Xt:fofType)=> (x Xt))) % 0.61/0.83 Found (((ex_intro1 (fun (Xt:fofType)=> (x Xt))) c) (fun (P:(fofType->Prop)) (x1:(P c))=> x1)) as proof of ((ex fofType) (fun (Xt:fofType)=> (x Xt))) % 0.61/0.83 Found ((((ex_intro fofType) (fun (Xt:fofType)=> (x Xt))) c) (fun (P:(fofType->Prop)) (x1:(P c))=> x1)) as proof of ((ex fofType) (fun (Xt:fofType)=> (x Xt))) % 0.61/0.83 Found ((((ex_intro fofType) (fun (Xt:fofType)=> (x Xt))) c) (fun (P:(fofType->Prop)) (x1:(P c))=> x1)) as proof of ((ex fofType) (fun (Xt:fofType)=> (x Xt))) % 0.61/0.83 Found ((conj00 ((eq_ref (fofType->Prop)) x)) ((((ex_intro fofType) (fun (Xt:fofType)=> (x Xt))) c) (fun (P:(fofType->Prop)) (x1:(P c))=> x1))) as proof of ((and (((eq (fofType->Prop)) x) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x Xt)))) % 0.61/0.83 Found (((conj0 ((ex fofType) (fun (Xt:fofType)=> (x Xt)))) ((eq_ref (fofType->Prop)) x)) ((((ex_intro fofType) (fun (Xt:fofType)=> (x Xt))) c) (fun (P:(fofType->Prop)) (x1:(P c))=> x1))) as proof of ((and (((eq (fofType->Prop)) x) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x Xt)))) % 0.68/0.84 Found ((((conj (((eq (fofType->Prop)) x) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x Xt)))) ((eq_ref (fofType->Prop)) x)) ((((ex_intro fofType) (fun (Xt:fofType)=> (x Xt))) c) (fun (P:(fofType->Prop)) (x1:(P c))=> x1))) as proof of ((and (((eq (fofType->Prop)) x) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x Xt)))) % 0.68/0.84 Found ((((conj (((eq (fofType->Prop)) x) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x Xt)))) ((eq_ref (fofType->Prop)) x)) ((((ex_intro fofType) (fun (Xt:fofType)=> (x Xt))) c) (fun (P:(fofType->Prop)) (x1:(P c))=> x1))) as proof of ((and (((eq (fofType->Prop)) x) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x Xt)))) % 0.68/0.84 Found ((((conj (((eq (fofType->Prop)) x) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x Xt)))) ((eq_ref (fofType->Prop)) x)) ((((ex_intro fofType) (fun (Xt:fofType)=> (x Xt))) c) (fun (P:(fofType->Prop)) (x1:(P c))=> x1))) as proof of (cQDP1 x) % 0.68/0.84 Found (ex_intro000 ((((conj (((eq (fofType->Prop)) x) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x Xt)))) ((eq_ref (fofType->Prop)) x)) ((((ex_intro fofType) (fun (Xt:fofType)=> (x Xt))) c) (fun (P:(fofType->Prop)) (x1:(P c))=> x1)))) as proof of ((ex (fofType->Prop)) (fun (Xs:(fofType->Prop))=> (cQDP1 Xs))) % 0.68/0.84 Found ((ex_intro00 cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x1:(P c))=> x1)))) as proof of ((ex (fofType->Prop)) (fun (Xs:(fofType->Prop))=> (cQDP1 Xs))) % 0.68/0.84 Found (((ex_intro0 (fun (Xs:(fofType->Prop))=> (cQDP1 Xs))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x1:(P c))=> x1)))) as proof of ((ex (fofType->Prop)) (fun (Xs:(fofType->Prop))=> (cQDP1 Xs))) % 0.68/0.84 Found ((((ex_intro (fofType->Prop)) (fun (Xs:(fofType->Prop))=> (cQDP1 Xs))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x1:(P c))=> x1)))) as proof of ((ex (fofType->Prop)) (fun (Xs:(fofType->Prop))=> (cQDP1 Xs))) % 0.68/0.84 Found ((((ex_intro (fofType->Prop)) (fun (Xs:(fofType->Prop))=> (cQDP1 Xs))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x1:(P c))=> x1)))) as proof of ((ex (fofType->Prop)) (fun (Xs:(fofType->Prop))=> (cQDP1 Xs))) % 0.68/0.84 Got proof ((((ex_intro (fofType->Prop)) (fun (Xs:(fofType->Prop))=> (cQDP1 Xs))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x1:(P c))=> x1)))) % 0.68/0.84 Time elapsed = 0.322400s % 0.68/0.84 node=109 cost=2374.000000 depth=17 % 0.68/0.84 :::::::::::::::::::::: % 0.68/0.84 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.68/0.84 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.68/0.84 ((((ex_intro (fofType->Prop)) (fun (Xs:(fofType->Prop))=> (cQDP1 Xs))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x1:(P c))=> x1)))) % 0.68/0.84 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------