%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : GEO540+1 : TPTP v8.1.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % 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 : 600s % DateTime : Sat Jul 16 05:27:03 EDT 2022 % Result : Satisfiable 0.19s 0.52s % Output : Saturation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : GEO540+1 : TPTP v8.1.0. Released v7.5.0. % 0.11/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n005.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jun 17 21:35:38 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.19/0.52 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.52 % 0.19/0.52 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.52 |- ~coll $A $B $C \/ coll $A $C $B % 0.19/0.52 |- ~coll $A $B $C \/ coll $B $A $C % 0.19/0.52 |- ~coll $A $B $C \/ ~coll $A $B $D \/ coll $C $D $A % 0.19/0.52 |- ~para $A $B $C $D \/ para $A $B $D $C % 0.19/0.52 |- ~para $A $B $C $D \/ para $C $D $A $B % 0.19/0.52 |- ~para $A $B $C $D \/ ~para $C $D $E $F \/ para $A $B $E $F % 0.19/0.52 |- ~perp $A $B $C $D \/ perp $A $B $D $C % 0.19/0.52 |- ~perp $A $B $C $D \/ perp $C $D $A $B % 0.19/0.52 |- ~perp $A $B $C $D \/ ~perp $C $D $E $F \/ para $A $B $E $F % 0.19/0.52 |- ~para $A $B $C $D \/ ~perp $C $D $E $F \/ perp $A $B $E $F % 0.19/0.52 |- ~midp $M $B $A \/ midp $M $A $B % 0.19/0.52 |- ~cong $O $A $O $B \/ ~cong $O $A $O $C \/ circle $O $A $B $C % 0.19/0.52 |- ~cong $O $A $O $B \/ ~cong $O $A $O $C \/ ~cong $O $A $O $D \/ % 0.19/0.52 cyclic $A $B $C $D % 0.19/0.52 |- ~cyclic $A $B $C $D \/ cyclic $A $B $D $C % 0.19/0.52 |- ~cyclic $A $B $C $D \/ cyclic $A $C $B $D % 0.19/0.52 |- ~cyclic $A $B $C $D \/ cyclic $B $A $C $D % 0.19/0.52 |- ~cyclic $A $B $C $D \/ ~cyclic $A $B $C $E \/ cyclic $B $C $D $E % 0.19/0.52 |- ~eqangle $A $B $C $D $P $Q $U $V \/ eqangle $B $A $C $D $P $Q $U $V % 0.19/0.52 |- ~eqangle $A $B $C $D $P $Q $U $V \/ eqangle $C $D $A $B $U $V $P $Q % 0.19/0.52 |- ~eqangle $A $B $C $D $P $Q $U $V \/ eqangle $P $Q $U $V $A $B $C $D % 0.19/0.52 |- ~eqangle $A $B $C $D $P $Q $U $V \/ eqangle $A $B $P $Q $C $D $U $V % 0.19/0.52 |- ~eqangle $A $B $C $D $P $Q $U $V \/ ~eqangle $P $Q $U $V $E $F $G $H \/ % 0.19/0.52 eqangle $A $B $C $D $E $F $G $H % 0.19/0.52 |- ~cong $A $B $C $D \/ cong $A $B $D $C % 0.19/0.52 |- ~cong $A $B $C $D \/ cong $C $D $A $B % 0.19/0.52 |- ~cong $A $B $C $D \/ ~cong $C $D $E $F \/ cong $A $B $E $F % 0.19/0.52 |- ~eqratio $A $B $C $D $P $Q $U $V \/ eqratio $B $A $C $D $P $Q $U $V % 0.19/0.52 |- ~eqratio $A $B $C $D $P $Q $U $V \/ eqratio $C $D $A $B $U $V $P $Q % 0.19/0.52 |- ~eqratio $A $B $C $D $P $Q $U $V \/ eqratio $P $Q $U $V $A $B $C $D % 0.19/0.52 |- ~eqratio $A $B $C $D $P $Q $U $V \/ eqratio $A $B $P $Q $C $D $U $V % 0.19/0.52 |- ~eqratio $A $B $C $D $P $Q $U $V \/ ~eqratio $P $Q $U $V $E $F $G $H \/ % 0.19/0.52 eqratio $A $B $C $D $E $F $G $H % 0.19/0.52 |- ~simtri $A $C $B $P $R $Q \/ simtri $A $B $C $P $Q $R % 0.19/0.52 |- ~simtri $B $A $C $Q $P $R \/ simtri $A $B $C $P $Q $R % 0.19/0.52 |- ~simtri $P $Q $R $A $B $C \/ simtri $A $B $C $P $Q $R % 0.19/0.52 |- ~simtri $A $B $C $E $F $G \/ ~simtri $E $F $G $P $Q $R \/ % 0.19/0.52 simtri $A $B $C $P $Q $R % 0.19/0.52 |- ~contri $A $C $B $P $R $Q \/ contri $A $B $C $P $Q $R % 0.19/0.52 |- ~contri $B $A $C $Q $P $R \/ contri $A $B $C $P $Q $R % 0.19/0.52 |- ~contri $P $Q $R $A $B $C \/ contri $A $B $C $P $Q $R % 0.19/0.53 |- ~contri $A $B $C $E $F $G \/ ~contri $E $F $G $P $Q $R \/ % 0.19/0.53 contri $A $B $C $P $Q $R % 0.19/0.53 |- ~eqangle $A $B $P $Q $C $D $P $Q \/ para $A $B $C $D % 0.19/0.53 |- ~para $A $B $C $D \/ eqangle $A $B $P $Q $C $D $P $Q % 0.19/0.53 |- ~cyclic $A $B $P $Q \/ eqangle $P $A $P $B $Q $A $Q $B % 0.19/0.53 |- ~eqangle $P $A $P $B $Q $A $Q $B \/ coll $P $Q $A \/ cyclic $A $B $P $Q % 0.19/0.53 |- ~coll $P $Q $B \/ ~eqangle $P $A $P $B $Q $A $Q $B \/ cyclic $A $B $P $Q % 0.19/0.53 |- ~cyclic $A $B $C $P \/ ~cyclic $A $B $C $Q \/ ~cyclic $A $B $C $R \/ % 0.19/0.53 ~eqangle $C $A $C $B $R $P $R $Q \/ cong $A $B $P $Q % 0.19/0.53 |- ~midp $E $A $B \/ ~midp $F $A $C \/ para $E $F $B $C % 0.19/0.53 |- ~coll $F $A $C \/ ~midp $E $A $B \/ ~para $E $F $B $C \/ midp $F $A $C % 0.19/0.53 |- ~cong $O $A $O $B \/ eqangle $O $A $A $B $A $B $O $B % 0.19/0.53 |- ~eqangle $O $A $A $B $A $B $O $B \/ coll $O $A $B \/ cong $O $A $O $B % 0.19/0.53 |- ~circle $O $A $B $C \/ ~perp $O $A $A $X \/ % 0.19/0.53 eqangle $A $X $A $B $C $A $C $B % 0.19/0.53 |- ~circle $O $A $B $C \/ ~eqangle $A $X $A $B $C $A $C $B \/ % 0.19/0.53 perp $O $A $A $X % 0.19/0.53 |- ~circle $O $A $B $C \/ ~midp $M $B $C \/ eqangle $A $B $A $C $O $B $O $M % 0.19/0.53 |- ~circle $O $A $B $C \/ ~coll $M $B $C \/ % 0.19/0.53 ~eqangle $A $B $A $C $O $B $O $M \/ midp $M $B $C % 0.19/0.53 |- ~midp $M $A $C \/ ~perp $A $B $B $C \/ cong $A $M $B $M % 0.19/0.53 |- ~circle $O $A $B $C \/ ~coll $O $A $C \/ perp $A $B $B $C % 0.19/0.53 |- ~cyclic $A $B $C $D \/ ~para $A $B $C $D \/ % 0.19/0.53 eqangle $A $D $C $D $C $D $C $B % 0.19/0.53 |- ~midp $M $A $B \/ ~perp $O $M $A $B \/ cong $O $A $O $B % 0.19/0.53 |- ~cong $A $P $B $P \/ ~cong $A $Q $B $Q \/ perp $A $B $P $Q % 0.19/0.53 |- ~cong $A $P $B $P \/ ~cong $A $Q $B $Q \/ ~cyclic $A $B $P $Q \/ % 0.19/0.53 perp $P $A $A $Q % 0.19/0.53 |- ~eqangle $A $B $B $C $P $Q $Q $R \/ ~eqangle $A $C $B $C $P $R $Q $R \/ % 0.19/0.53 coll $A $B $C \/ simtri $A $B $C $P $Q $R % 0.19/0.53 |- ~simtri $A $B $C $P $Q $R \/ eqratio $A $B $A $C $P $Q $P $R % 0.19/0.53 |- ~simtri $A $B $C $P $Q $R \/ eqangle $A $B $B $C $P $Q $Q $R % 0.19/0.53 |- ~cong $A $B $P $Q \/ ~simtri $A $B $C $P $Q $R \/ % 0.19/0.53 contri $A $B $C $P $Q $R % 0.19/0.53 |- ~contri $A $B $C $P $Q $R \/ cong $A $B $P $Q % 0.19/0.53 |- ~midp $M $A $B \/ ~midp $M $C $D \/ para $A $C $B $D % 0.19/0.53 |- ~midp $M $A $B \/ ~para $A $C $B $D \/ ~para $A $D $B $C \/ % 0.19/0.53 midp $M $C $D % 0.19/0.53 |- ~coll $O $A $C \/ ~coll $O $B $D \/ ~para $A $B $C $D \/ % 0.19/0.53 eqratio $O $A $A $C $O $B $B $D % 0.19/0.53 |- ~para $A $B $A $C \/ coll $A $B $C % 0.19/0.53 |- ~coll $A $B $C \/ ~cong $A $B $A $C \/ midp $A $B $C % 0.19/0.53 |- ~midp $A $B $C \/ cong $A $B $A $C % 0.19/0.53 |- ~midp $A $B $C \/ coll $A $B $C % 0.19/0.53 |- ~midp $M $A $B \/ ~midp $N $C $D \/ eqratio $M $A $A $B $N $C $C $D % 0.19/0.53 |- ~eqangle $A $B $C $D $C $D $A $B \/ para $A $B $C $D \/ perp $A $B $C $D % 0.19/0.53 |- ~eqangle $A $B $C $D $P $Q $U $V \/ ~para $P $Q $U $V \/ % 0.19/0.53 para $A $B $C $D % 0.19/0.53 |- ~eqangle $A $B $C $D $P $Q $U $V \/ ~perp $P $Q $U $V \/ % 0.19/0.53 perp $A $B $C $D % 0.19/0.53 |- ~cong $P $Q $U $V \/ ~eqratio $A $B $C $D $P $Q $U $V \/ % 0.19/0.53 cong $A $B $C $D % 0.19/0.53 |- ~eqangle $X $O $M $O $M $O $A $O \/ ~perp $O $M $M $A \/ % 0.19/0.53 coll (skolemFOFtoCNF_B $A $M $O $X) $A $M % 0.19/0.53 |- ~eqangle $X $O $M $O $M $O $A $O \/ ~perp $O $M $M $A \/ % 0.19/0.53 coll (skolemFOFtoCNF_B $A $M $O $X) $O $X % 0.19/0.53 |- ~cong $O $A $O $B \/ ~eqangle $A $O $O $X $O $X $O $B \/ % 0.19/0.53 coll $B $A (skolemFOFtoCNF_M $A $B $O $X) % 0.19/0.53 |- ~cong $O $A $O $B \/ ~eqangle $A $O $O $X $O $X $O $B \/ % 0.19/0.53 coll (skolemFOFtoCNF_M $A $B $O $X) $O $X % 0.19/0.53 |- ~eqangle $A $O $O $X $O $X $O $B \/ ~perp $O $X $A $B \/ % 0.19/0.53 coll $B $A (skolemFOFtoCNF_M_1 $A $B $O $X) % 0.19/0.53 |- ~eqangle $A $O $O $X $O $X $O $B \/ ~perp $O $X $A $B \/ % 0.19/0.53 coll (skolemFOFtoCNF_M_1 $A $B $O $X) $O $X % 0.19/0.53 |- ~cong $O $A $O $B \/ ~perp $O $X $A $B \/ % 0.19/0.53 coll $B $A (skolemFOFtoCNF_M_2 $A $B $O $X) % 0.19/0.53 |- ~cong $O $A $O $B \/ ~perp $O $X $A $B \/ % 0.19/0.53 coll (skolemFOFtoCNF_M_2 $A $B $O $X) $O $X % 0.19/0.53 |- ~eqangle $A $P $B $P $A $X $B $Y \/ coll $A $B $P \/ % 0.19/0.53 cyclic $X $B $P (skolemFOFtoCNF_Q $A $B $P $X) % 0.19/0.53 |- ~eqangle $A $P $B $P $A $X $B $Y \/ coll $A $B $P \/ % 0.19/0.53 eqangle $A $P $B $P $A (skolemFOFtoCNF_Q $A $B $P $X) $B % 0.19/0.53 (skolemFOFtoCNF_Q $A $B $P $X) % 0.19/0.53 |- ~midp $M $A $B \/ ~midp $N $C $D \/ % 0.19/0.53 midp (skolemFOFtoCNF_P $A $B $C $D $M $N) $A $D % 0.19/0.53 |- ~midp $M $A $B \/ ~midp $N $C $D \/ % 0.19/0.53 para (skolemFOFtoCNF_P $A $B $C $D $M $N) $M $B $D % 0.19/0.53 |- ~midp $M $A $B \/ ~midp $N $C $D \/ % 0.19/0.53 para (skolemFOFtoCNF_P $A $B $C $D $M $N) $N $A $C % 0.19/0.53 |- ~coll $C $A $B \/ ~coll $D $A $B \/ ~midp $M $A $B \/ ~midp $N $C $D \/ % 0.19/0.53 midp (skolemFOFtoCNF_P_1 $A $Q) $A $Q % 0.19/0.53 |- ~coll $P $Q $R \/ ~midp $M $A $B \/ ~para $A $P $B $Q \/ % 0.19/0.53 ~para $A $P $R $M \/ coll (skolemFOFtoCNF_X $A $M $Q $R) $A $Q % 0.19/0.53 |- ~coll $P $Q $R \/ ~midp $M $A $B \/ ~para $A $P $B $Q \/ % 0.19/0.53 ~para $A $P $R $M \/ coll (skolemFOFtoCNF_X $A $M $Q $R) $M $R % 0.19/0.53 |- ~cong $O $C $O $D \/ ~perp $A $B $B $O \/ % 0.19/0.53 cong $B $C $B (skolemFOFtoCNF_P_2 $A $B $C $O) % 0.19/0.53 |- ~cong $O $C $O $D \/ ~perp $A $B $B $O \/ % 0.19/0.53 cong $O $C $O (skolemFOFtoCNF_P_2 $A $B $C $O) % 0.19/0.53 |- ~cong $O $C $O $D \/ ~perp $A $B $B $O \/ % 0.19/0.53 para (skolemFOFtoCNF_P_2 $A $B $C $O) $C $A $B % 0.19/0.53 |- ~perp $A $H $B $C \/ ~perp $B $H $A $C \/ % 0.19/0.53 coll (skolemFOFtoCNF_P_3 $A $B $C) $C $B % 0.19/0.53 |- ~perp $A $H $B $C \/ ~perp $B $H $A $C \/ % 0.19/0.53 coll (skolemFOFtoCNF_Q_1 $A $B $C) $C $A % 0.19/0.53 |- ~perp $A $H $B $C \/ ~perp $B $H $A $C \/ % 0.19/0.53 perp $A (skolemFOFtoCNF_P_3 $A $B $C) $C $B % 0.19/0.53 |- ~perp $A $H $B $C \/ ~perp $B $H $A $C \/ % 0.19/0.53 perp $B (skolemFOFtoCNF_Q_1 $A $B $C) $C $A % 0.19/0.53 |- ~circle $O $A $B $C \/ perp (skolemFOFtoCNF_P_4 $A $O) $A $A $O % 0.19/0.53 |- ~circle $M $A $B $C \/ ~cong $M $A $M $D \/ ~cong $N $A $N $B \/ % 0.19/0.53 $M = $N \/ coll (skolemFOFtoCNF_P_5 $A $B $C $D $N) $A $C % 0.19/0.53 |- ~circle $M $A $B $C \/ ~cong $M $A $M $D \/ ~cong $N $A $N $B \/ % 0.19/0.53 $M = $N \/ coll (skolemFOFtoCNF_Q_2 $A $B $C $D $N) $B $D % 0.19/0.53 |- ~circle $M $A $B $C \/ ~cong $M $A $M $D \/ ~cong $N $A $N $B \/ % 0.19/0.53 $M = $N \/ cong (skolemFOFtoCNF_P_5 $A $B $C $D $N) $N $N $A % 0.19/0.53 |- ~circle $M $A $B $C \/ ~cong $M $A $M $D \/ ~cong $N $A $N $B \/ % 0.19/0.53 $M = $N \/ cong (skolemFOFtoCNF_Q_2 $A $B $C $D $N) $N $N $A % 0.19/0.53 |- ~cyclic $A $B $C $D \/ ~midp $M $A $B \/ ~para $A $B $C $D \/ % 0.19/0.53 circle (skolemFOFtoCNF_O $A $B $C) $A $B $C % 0.19/0.53 |- ~cyclic $A $B $C $D \/ ~perp $A $C $C $B \/ % 0.19/0.53 circle (skolemFOFtoCNF_O_1 $A $B $C) $A $B $C % 0.19/0.53 |- ~coll $B $E $F \/ ~perp $A $C $C $B \/ % 0.19/0.53 coll (skolemFOFtoCNF_P_6 $A $E $F) $E $F % 0.19/0.53 |- ~coll $B $E $F \/ ~perp $A $C $C $B \/ % 0.19/0.53 perp (skolemFOFtoCNF_P_6 $A $E $F) $A $E $F % 0.19/0.53 |- ~midp $M $B $D \/ ~perp $A $B $A $C \/ ~perp $C $A $C $D \/ % 0.19/0.53 midp (skolemFOFtoCNF_P_7 $A $C) $A $C % 0.19/0.53 |- ~cong $O $A $O $B \/ ~perp $A $O $O $B \/ % 0.19/0.53 coll $A $O (skolemFOFtoCNF_C $A $O) % 0.19/0.53 |- ~cong $O $A $O $B \/ ~perp $A $O $O $B \/ % 0.19/0.53 cong $O $A $O (skolemFOFtoCNF_C $A $O) % 0.19/0.53 |- ~coll $P $A $C \/ ~coll $P $B $D \/ ~coll $Q $A $B \/ % 0.19/0.53 ~para $A $B $C $D \/ coll $P $Q (skolemFOFtoCNF_R $C $D $P $Q) % 0.19/0.53 |- ~coll $P $A $C \/ ~coll $P $B $D \/ ~coll $Q $A $B \/ % 0.19/0.53 ~para $A $B $C $D \/ coll (skolemFOFtoCNF_R $C $D $P $Q) $C $D % 0.19/0.53 |- ~coll $A $B $D \/ coll $D $D $A % 0.19/0.53 |- ~perp $E $F $E $F \/ para $E $F $E $F % 0.19/0.53 |- ~cong $O $A $O $C \/ circle $O $A $C $C % 0.19/0.53 |- ~cyclic $A $B $C $E \/ cyclic $B $C $E $E % 0.19/0.53 |- ~midp $F $A $C \/ para $F $F $C $C % 0.19/0.53 |- ~cong $A $Q $B $Q \/ perp $A $B $Q $Q % 0.19/0.53 |- ~midp $M $C $D \/ para $C $C $D $D % 0.19/0.53 |- ~midp $N $C $D \/ eqratio $N $C $C $D $N $C $C $D % 0.19/0.53 |- ~midp $N $C $D \/ midp (skolemFOFtoCNF_P $C $D $C $D $N $N) $C $D % 0.19/0.53 |- ~midp $N $C $D \/ para (skolemFOFtoCNF_P $C $D $C $D $N $N) $N $D $D % 0.19/0.53 |- ~midp $N $C $D \/ para (skolemFOFtoCNF_P $C $D $C $D $N $N) $N $C $C % 0.19/0.53 |- ~perp $B $H $B $C \/ coll (skolemFOFtoCNF_P_3 $B $B $C) $C $B % 0.19/0.53 |- ~perp $B $H $B $C \/ coll (skolemFOFtoCNF_Q_1 $B $B $C) $C $B % 0.19/0.53 |- ~perp $B $H $B $C \/ perp $B (skolemFOFtoCNF_P_3 $B $B $C) $C $B % 0.19/0.53 |- ~perp $B $H $B $C \/ perp $B (skolemFOFtoCNF_Q_1 $B $B $C) $C $B % 0.19/0.53 |- ~cong $O $A $O $C \/ ~cong $O $A $O $D \/ cyclic $A $C $C $D % 0.19/0.53 |- ~cong $O $A $O $C \/ ~cong $O $A $O $D \/ cyclic $A $D $C $D % 0.19/0.53 |- ~cong $O $A $O $B \/ ~cong $O $A $O $D \/ cyclic $A $B $D $D % 0.19/0.53 |- ~cong $O $A $O $D \/ cyclic $A $D $D $D % 0.19/0.53 |- ~cong $A $Q $B $Q \/ ~cyclic $A $B $Q $Q \/ perp $Q $A $A $Q % 0.19/0.53 |- ~eqangle $A $C $C $C $P $R $R $R \/ coll $A $C $C \/ % 0.19/0.53 simtri $A $C $C $P $R $R % 0.19/0.53 |- ~midp $M $A $B \/ ~para $A $D $B $D \/ midp $M $D $D % 0.19/0.53 |- ~coll $O $B $D \/ ~para $B $B $D $D \/ eqratio $O $B $B $D $O $B $B $D % 0.19/0.53 |- ~midp $M $D $D \/ ~perp $D $D $D $D \/ % 0.19/0.53 midp (skolemFOFtoCNF_P_7 $D $D) $D $D % 0.19/0.53 |- ~coll $D $A $B \/ ~midp $M $A $B \/ ~midp $N $D $D \/ % 0.19/0.53 midp (skolemFOFtoCNF_P_1 $A $Q) $A $Q % 0.19/0.53 |- ~coll $C $C $D \/ ~coll $D $C $D \/ ~midp $N $C $D \/ % 0.19/0.53 midp (skolemFOFtoCNF_P_1 $C $Q) $C $Q % 0.19/0.53 |- ~coll $D $D $D \/ ~midp $N $D $D \/ % 0.19/0.53 midp (skolemFOFtoCNF_P_1 $D $Q) $D $Q % 0.19/0.53 |- ~coll $P $M $R \/ ~midp $M $A $R \/ ~para $A $P $R $M \/ % 0.19/0.53 coll (skolemFOFtoCNF_X $A $M $M $R) $A $M % 0.19/0.53 |- ~coll $P $M $R \/ ~midp $M $A $R \/ ~para $A $P $R $M \/ % 0.19/0.53 coll (skolemFOFtoCNF_X $A $M $M $R) $M $R % 0.19/0.53 |- ~coll $P $B $D \/ ~coll $Q $B $B \/ ~para $B $B $D $D \/ % 0.19/0.53 coll $P $Q (skolemFOFtoCNF_R $D $D $P $Q) % 0.19/0.53 |- ~coll $Q $A $B \/ ~coll $Q $B $D \/ ~para $A $B $B $D \/ % 0.19/0.53 coll $Q $Q (skolemFOFtoCNF_R $B $D $Q $Q) % 0.19/0.53 |- ~coll $Q $A $A \/ ~coll $Q $A $C \/ ~para $A $A $C $A \/ % 0.19/0.53 coll $Q $Q (skolemFOFtoCNF_R $C $A $Q $Q) % 0.19/0.53 |- ~coll $Q $A $A \/ ~para $A $A $A $A \/ % 0.19/0.53 coll $Q $Q (skolemFOFtoCNF_R $A $A $Q $Q) % 0.19/0.53 |- ~coll $P $B $D \/ ~coll $Q $B $B \/ ~para $B $B $D $D \/ % 0.19/0.53 coll (skolemFOFtoCNF_R $D $D $P $Q) $D $D % 0.19/0.53 |- ~coll $Q $A $B \/ ~coll $Q $B $D \/ ~para $A $B $B $D \/ % 0.19/0.53 coll (skolemFOFtoCNF_R $B $D $Q $Q) $B $D % 0.19/0.53 |- ~coll $Q $A $A \/ ~coll $Q $A $C \/ ~para $A $A $C $A \/ % 0.19/0.53 coll (skolemFOFtoCNF_R $C $A $Q $Q) $C $A % 0.19/0.53 |- ~coll $Q $A $A \/ ~para $A $A $A $A \/ % 0.19/0.53 coll (skolemFOFtoCNF_R $A $A $Q $Q) $A $A % 0.19/0.53 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.53 %------------------------------------------------------------------------------