%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : SYO846+1 : TPTP v7.5.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % 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 01:53:55 EDT 2022 % Result : CounterSatisfiable 0.61s 0.78s % Output : Model 0.61s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYO846+1 : TPTP v7.5.0. Released v7.5.0. % 0.11/0.13 % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % 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 : Wed Mar 16 03:29:39 EDT 2022 % 0.20/0.34 % CPUTime : % 0.20/0.34 E-Darwin 1.5 2012/06/20 (based on Darwin 1.3) % 0.20/0.34 % 0.20/0.34 % 0.20/0.34 Defaulting to tptp format. % 0.20/0.34 Parsing /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.20/0.35 % 0.20/0.35 % 0.20/0.35 % 0.20/0.37 Proving ... % 0.20/0.37 % 0.61/0.78 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.61/0.78 % 0.61/0.78 START OF MODEL (DIG): % 0.61/0.78 (a3 = aint(aun(apow(a2), asing(asing(a2))), aun(a4, asing(asm(apow(a2), a2))))) % 0.61/0.78 (asm(asm(a4, asing(a1)), asing(a3)) = asm(a3, asing(a1))) % 0.61/0.78 (asm(asm(apow(a2), apow(asing(a2))), asing(a2)) = aun(asing(a1), asing(asing(a1)))) % 0.61/0.78 (aun(asing(a2), apow(asing(a2))) = aint(aun(aun(asing(a2), apow(asing(a2))), asing(asm(a3, asing(a1)))), aun(asm(apow(a2), apow(asing(a2))), aun(apow(asing(a2)), asing(apow(a2)))))) % 0.61/0.78 aal2(asm(a4, a2)) % 0.61/0.78 aal3(asm(a4, asing(a2))) % 0.61/0.78 aal3(asm(apow(aun(asing(a1), asing(asing(a1)))), asing(aun(asing(a1), asing(asing(a1)))))) % 0.61/0.78 aal3(aun(a2, asing(apow(a2)))) % 0.61/0.78 aal4(apow(a2)) % 0.61/0.78 aal4(aun(asm(apow(a2), asing(a2)), asing(asm(apow(a2), apow(asing(a2)))))) % 0.61/0.78 aal4(asm(apow(aun(asing(a1), asing(asing(a1)))), asing(aun(asing(a1), asing(asing(a1)))))) % 0.61/0.78 aal5(aun(apow(a2), asing(asing(a2)))) % 0.61/0.78 aex2(aint(aun(apow(a2), asing(asing(a2))), asm(a4, asing(a1)))) % 0.61/0.78 aex2(asm(a3, asing(a1))) % 0.61/0.78 aex2(aun(asing(a1), asing(asing(a1)))) % 0.61/0.78 aex3(aun(a2, asing(apow(a2)))) % 0.61/0.78 aex3(asm(a4, asing(a2))) % 0.61/0.78 aex5(aun(a4, asing(apow(a2)))) % 0.61/0.78 aex5(aun(asm(apow(a2), apow(asing(a2))), apow(asing(asing(a1))))) % 0.61/0.78 ain(_0, apow(_0)) % 0.61/0.78 ain(a1, a3) % 0.61/0.78 ain(a1, aun(asing(asing(a1)), aun(a4, asing(apow(a2))))) % 0.61/0.78 ain(a1, aun(asm(apow(a2), apow(asing(a1))), aun(asing(asing(a2)), asing(apow(a2))))) % 0.61/0.78 ain(a1, aun(asm(apow(a2), apow(asing(a2))), asing(asing(asing(a1))))) % 0.61/0.78 ain(a1, asm(aun(asing(asing(a2)), a4), asm(apow(a2), asing(a1)))) % 0.61/0.78 ain(a2, a3) % 0.61/0.78 ain(a2, asm(a4, asing(a1))) % 0.61/0.78 ain(a2, aun(asing(asing(a1)), aun(asing(asing(a2)), a4))) % 0.61/0.78 ain(a2, aun(asm(apow(a2), apow(asing(a2))), aun(apow(asing(a2)), asing(apow(a2))))) % 0.61/0.78 ain(asing(a1), aun(asing(asing(a1)), asing(asing(asing(a1))))) % 0.61/0.78 ain(asing(asing(a1)), asing(asing(asing(a1)))) % 0.61/0.78 ain(asing(asing(a1)), aun(asm(apow(a2), a2), apow(asing(asing(a1))))) % 0.61/0.78 ain(a0, a3) % 0.61/0.78 ain(a0, apow(asing(asing(a1)))) % 0.61/0.78 ain(a0, apow(apow(asing(a1)))) % 0.61/0.78 ain(a0, apow(aun(asing(a1), asing(asing(a1))))) % 0.61/0.78 asubq(a1, asm(a2, asing(a1))) % 0.61/0.78 asubq(_0, _0) % 0.61/0.78 asubq(a2, asm(a3, asing(a2))) % 0.61/0.78 asubq(asing(asing(a1)), a0) % 0.61/0.78 asubq(asing(asing(a1)), asm(asm(apow(a2), a2), asing(a2))) % 0.61/0.78 asubq(asing(a2), asm(asm(apow(a2), a2), asing(asing(a1)))) % 0.61/0.78 asubq(apow(a2), aun(asing(asing(a1)), aun(a4, asing(apow(a2))))) % 0.61/0.78 asubq(apow(asing(a1)), a0) % 0.61/0.78 asubq(asm(aint(aun(aun(asing(a1), asing(asing(a1))), aun(apow(asing(a2)), asing(a3))), aun(asing(asing(a2)), a4)), asing(a0)), asm(aun(asing(asing(a2)), a4), asm(apow(a2), asing(a1)))) % 0.61/0.78 asubq(asm(a2, asing(a1)), a1) % 0.61/0.78 asubq(asm(a3, asing(a2)), a2) % 0.61/0.78 asubq(asm(apow(a2), asing(a2)), aun(asing(a1), asing(asing(a1)))) % 0.61/0.78 asubq(asm(asm(a4, asing(a2)), asing(a0)), aun(asing(a1), asing(a3))) % 0.61/0.78 asubq(asm(asm(apow(a2), a2), asing(asing(a1))), asing(a2)) % 0.61/0.78 asubq(asm(asm(apow(a2), a2), asing(a2)), asing(asing(a1))) % 0.61/0.78 asubq(asm(aun(asing(asing(a2)), a4), asm(apow(a2), asing(a1))), asm(aint(aun(aun(asing(a1), asing(asing(a1))), aun(apow(asing(a2)), asing(a3))), aun(asing(asing(a2)), a4)), asing(a0))) % 0.61/0.78 asubq(aun(asing(a1), asing(asing(a1))), asm(apow(a2), asing(a2))) % 0.61/0.78 asubq(aun(asing(a1), asing(asing(a1))), a0) % 0.61/0.78 asubq(aun(asing(a1), asing(a3)), asm(asm(a4, asing(a2)), asing(a0))) % 0.61/0.78 asubq(aun(asing(asing(a1)), aun(a4, asing(apow(a2)))), apow(a2)) % 0.61/0.78 asubq(a0, asing(asing(a1))) % 0.61/0.78 asubq(a0, apow(asing(a1))) % 0.61/0.78 asubq(a0, aun(asing(a1), asing(asing(a1)))) % 0.61/0.78 END OF MODEL %------------------------------------------------------------------------------