%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SYO150^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 : 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:50:45 EDT 2022 % Result : Unknown 1.16s 1.33s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : SYO150^5 : TPTP v7.5.0. Released v4.0.0. % 0.07/0.12 % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % 0.13/0.33 % Computer : n023.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % RAMPerCPU : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % DateTime : Fri Mar 11 17:02:12 EST 2022 % 0.13/0.33 % CPUTime : % 0.13/0.34 ModuleCmd_Load.c(213):ERROR:105: Unable to locate a modulefile for 'python/python27' % 0.13/0.34 Python 2.7.5 % 1.16/1.33 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 1.16/1.33 FOF formula (<kernel.Constant object at 0x1eac248>, <kernel.Sort object at 0x2b2a27dde638>) of role type named cC % 1.16/1.33 Using role type % 1.16/1.33 Declaring cC:Prop % 1.16/1.33 FOF formula (<kernel.Constant object at 0x1eac560>, <kernel.Constant object at 0x1eacef0>) of role type named x % 1.16/1.33 Using role type % 1.16/1.33 Declaring x:fofType % 1.16/1.33 FOF formula (<kernel.Constant object at 0x2b2a27de53b0>, <kernel.DependentProduct object at 0x1eabcb0>) of role type named cR4 % 1.16/1.33 Using role type % 1.16/1.33 Declaring cR4:(fofType->Prop) % 1.16/1.33 FOF formula (<kernel.Constant object at 0x1e86b00>, <kernel.DependentProduct object at 0x1eab248>) of role type named cR3 % 1.16/1.33 Using role type % 1.16/1.33 Declaring cR3:(fofType->Prop) % 1.16/1.33 FOF formula (<kernel.Constant object at 0x1eac560>, <kernel.DependentProduct object at 0x1eabcf8>) of role type named cR2 % 1.16/1.33 Using role type % 1.16/1.33 Declaring cR2:(fofType->Prop) % 1.16/1.33 FOF formula (<kernel.Constant object at 0x1eac1b8>, <kernel.DependentProduct object at 0x1eabb48>) of role type named cR1 % 1.16/1.33 Using role type % 1.16/1.33 Declaring cR1:(fofType->Prop) % 1.16/1.33 FOF formula (<kernel.Constant object at 0x1eac2d8>, <kernel.DependentProduct object at 0x1eabef0>) of role type named cQ % 1.16/1.33 Using role type % 1.16/1.33 Declaring cQ:(fofType->Prop) % 1.16/1.33 FOF formula (<kernel.Constant object at 0x1eac1b8>, <kernel.DependentProduct object at 0x1eab368>) of role type named cP % 1.16/1.33 Using role type % 1.16/1.33 Declaring cP:(fofType->Prop) % 1.16/1.33 FOF formula (((forall (Xx0:fofType), (cP Xx0))->(forall (Xx0:fofType), (cQ Xx0)))->(((or ((or ((or (cR1 x)) (cR2 x))) (cR3 x))) (cR4 x))->cC)) of role conjecture named cADDHYP8 % 1.16/1.33 Conjecture to prove = (((forall (Xx0:fofType), (cP Xx0))->(forall (Xx0:fofType), (cQ Xx0)))->(((or ((or ((or (cR1 x)) (cR2 x))) (cR3 x))) (cR4 x))->cC)):Prop % 1.16/1.33 We need to prove ['(((forall (Xx0:fofType), (cP Xx0))->(forall (Xx0:fofType), (cQ Xx0)))->(((or ((or ((or (cR1 x)) (cR2 x))) (cR3 x))) (cR4 x))->cC))'] % 1.16/1.33 Parameter cC:Prop. % 1.16/1.33 Parameter fofType:Type. % 1.16/1.33 Parameter x:fofType. % 1.16/1.33 Parameter cR4:(fofType->Prop). % 1.16/1.33 Parameter cR3:(fofType->Prop). % 1.16/1.33 Parameter cR2:(fofType->Prop). % 1.16/1.33 Parameter cR1:(fofType->Prop). % 1.16/1.33 Parameter cQ:(fofType->Prop). % 1.16/1.33 Parameter cP:(fofType->Prop). % 1.16/1.33 Trying to prove (((forall (Xx0:fofType), (cP Xx0))->(forall (Xx0:fofType), (cQ Xx0)))->(((or ((or ((or (cR1 x)) (cR2 x))) (cR3 x))) (cR4 x))->cC)) % 1.16/1.33 % SZS status GaveUp for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------