%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : GRA075+1 : TPTP v8.1.0. Released v6.4.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n032.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 07:19:57 EDT 2022 % Result : Satisfiable 0.16s 0.33s % Output : Saturation 0.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.10 % Problem : GRA075+1 : TPTP v8.1.0. Released v6.4.0. % 0.09/0.11 % Command : metis --show proof --show saturation %s % 0.10/0.30 % Computer : n032.cluster.edu % 0.10/0.30 % Model : x86_64 x86_64 % 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.30 % Memory : 8042.1875MB % 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.30 % CPULimit : 300 % 0.10/0.30 % WCLimit : 600 % 0.10/0.30 % DateTime : Tue May 31 02:15:13 EDT 2022 % 0.10/0.30 % CPUTime : % 0.10/0.30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.16/0.33 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.16/0.33 % 0.16/0.33 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.16/0.33 |- ~(head_of $E = tail_of $E) \/ ~edge $E % 0.16/0.33 |- ~edge $E \/ vertex (head_of $E) % 0.16/0.33 |- ~edge $E \/ vertex (tail_of $E) % 0.16/0.33 |- ~complete \/ ~vertex $V1 \/ ~vertex $V2 \/ $V1 = $V2 \/ % 0.16/0.33 edge (skolemFOFtoCNF_E $V1 $V2) % 0.16/0.33 |- ~complete \/ ~vertex $V1 \/ ~vertex $V2 \/ $V1 = $V2 \/ % 0.16/0.33 $V1 = head_of (skolemFOFtoCNF_E $V1 $V2) \/ % 0.16/0.33 $V1 = tail_of (skolemFOFtoCNF_E $V1 $V2) % 0.16/0.33 |- ~complete \/ ~vertex $V1 \/ ~vertex $V2 \/ $V1 = $V2 \/ % 0.16/0.33 $V1 = head_of (skolemFOFtoCNF_E $V1 $V2) \/ % 0.16/0.33 $V2 = head_of (skolemFOFtoCNF_E $V1 $V2) % 0.16/0.33 |- ~complete \/ ~vertex $V1 \/ ~vertex $V2 \/ $V1 = $V2 \/ % 0.16/0.33 $V1 = tail_of (skolemFOFtoCNF_E $V1 $V2) \/ % 0.16/0.33 $V2 = tail_of (skolemFOFtoCNF_E $V1 $V2) % 0.16/0.33 |- ~complete \/ ~vertex $V1 \/ ~vertex $V2 \/ $V1 = $V2 \/ % 0.16/0.33 $V2 = head_of (skolemFOFtoCNF_E $V1 $V2) \/ % 0.16/0.33 $V2 = tail_of (skolemFOFtoCNF_E $V1 $V2) % 0.16/0.33 |- ~edge $E \/ ~path (head_of $E) $V2 $TP \/ ~vertex $V2 \/ % 0.16/0.33 ~vertex (tail_of $E) \/ path (tail_of $E) $V2 (path_cons $E $TP) % 0.16/0.33 |- ~edge $E \/ ~vertex (head_of $E) \/ ~vertex (tail_of $E) \/ % 0.16/0.33 path (tail_of $E) (head_of $E) (path_cons $E empty) % 0.16/0.33 |- ~path $V1 $V2 $P \/ $V1 = tail_of (skolemFOFtoCNF_E_1 $P $V1 $V2) % 0.16/0.33 |- ~path $V1 $V2 $P \/ edge (skolemFOFtoCNF_E_1 $P $V1 $V2) % 0.16/0.33 |- ~path $V1 $V2 $P \/ vertex $V1 % 0.16/0.33 |- ~path $V1 $V2 $P \/ vertex $V2 % 0.16/0.33 |- ~path $V1 $V2 $P \/ % 0.16/0.33 $P = path_cons (skolemFOFtoCNF_E_1 $P $V1 $V2) empty \/ % 0.16/0.33 $P = % 0.16/0.33 path_cons (skolemFOFtoCNF_E_1 $P $V1 $V2) (skolemFOFtoCNF_TP $P $V1 $V2) % 0.16/0.33 |- ~path $V1 $V2 $P \/ % 0.16/0.33 $P = path_cons (skolemFOFtoCNF_E_1 $P $V1 $V2) empty \/ % 0.16/0.33 path (head_of (skolemFOFtoCNF_E_1 $P $V1 $V2)) $V2 % 0.16/0.33 (skolemFOFtoCNF_TP $P $V1 $V2) % 0.16/0.33 |- ~path $V1 $V2 $P \/ % 0.16/0.33 $P = % 0.16/0.33 path_cons (skolemFOFtoCNF_E_1 $P $V1 $V2) % 0.16/0.33 (skolemFOFtoCNF_TP $P $V1 $V2) \/ % 0.16/0.33 $V2 = head_of (skolemFOFtoCNF_E_1 $P $V1 $V2) % 0.16/0.33 |- ~path $V1 $V2 $P \/ $V2 = head_of (skolemFOFtoCNF_E_1 $P $V1 $V2) \/ % 0.16/0.33 path (head_of (skolemFOFtoCNF_E_1 $P $V1 $V2)) $V2 % 0.16/0.33 (skolemFOFtoCNF_TP $P $V1 $V2) % 0.16/0.33 |- ~($P = path_cons (skolemFOFtoCNF_E_1 $P $V1 $V2) $TP) \/ % 0.16/0.33 ~($P = path_cons (skolemFOFtoCNF_E_1 $P $V1 $V2) empty) \/ % 0.16/0.33 ~($V2 = head_of (skolemFOFtoCNF_E_1 $P $V1 $V2)) \/ ~path $V1 $V2 $P \/ % 0.16/0.33 ~path $V2 $V2 $TP % 0.16/0.33 |- ~on_path $E $P \/ ~path $V1 $V2 $P \/ edge $E % 0.16/0.33 |- ~on_path $E $P \/ ~path $V1 $V2 $P \/ in_path (head_of $E) $P % 0.16/0.33 |- ~on_path $E $P \/ ~path $V1 $V2 $P \/ in_path (tail_of $E) $P % 0.16/0.33 |- ~in_path $V $P \/ ~path $V1 $V2 $P \/ % 0.16/0.33 on_path (skolemFOFtoCNF_E_2 $P $V) $P % 0.16/0.33 |- ~in_path $V $P \/ ~path $V1 $V2 $P \/ vertex $V % 0.16/0.33 |- ~in_path $V $P \/ ~path $V1 $V2 $P \/ % 0.16/0.33 $V = head_of (skolemFOFtoCNF_E_2 $P $V) \/ % 0.16/0.33 $V = tail_of (skolemFOFtoCNF_E_2 $P $V) % 0.16/0.33 |- ~sequential $E2 $E2 % 0.16/0.33 |- ~sequential $E1 $E2 \/ head_of $E1 = tail_of $E2 % 0.16/0.33 |- ~sequential $E1 $E2 \/ edge $E1 % 0.16/0.33 |- ~sequential $E1 $E2 \/ edge $E2 % 0.16/0.33 |- ~(head_of $E1 = tail_of $E2) \/ ~edge $E1 \/ ~edge $E2 \/ $E1 = $E2 \/ % 0.16/0.33 sequential $E1 $E2 % 0.16/0.33 |- ~on_path $E1 $P \/ ~on_path $E2 $P \/ ~path $V1 $V2 $P \/ % 0.16/0.33 ~sequential $E1 $E2 \/ precedes $E1 $E2 $P % 0.16/0.33 |- ~on_path $E1 $P \/ ~on_path $E2 $P \/ ~path $V1 $V2 $P \/ % 0.16/0.33 ~precedes $E3 $E2 $P \/ ~sequential $E1 $E3 \/ precedes $E1 $E2 $P % 0.16/0.33 |- ~path $V1 $V2 $P \/ ~precedes $E1 $E2 $P \/ on_path $E1 $P % 0.16/0.33 |- ~path $V1 $V2 $P \/ ~precedes $E1 $E2 $P \/ on_path $E2 $P % 0.16/0.33 |- ~path $V1 $V2 $P \/ ~precedes $E1 $E2 $P \/ % 0.16/0.33 precedes (skolemFOFtoCNF_E3 $E1 $E2 $P) $E2 $P \/ sequential $E1 $E2 % 0.16/0.33 |- ~path $V1 $V2 $P \/ ~precedes $E1 $E2 $P \/ sequential $E1 $E2 \/ % 0.16/0.33 sequential $E1 (skolemFOFtoCNF_E3 $E1 $E2 $P) % 0.16/0.33 |- ~path $V1 $V2 $P \/ ~precedes $E1 $E2 $P \/ ~precedes $E3 $E2 $P \/ % 0.16/0.33 ~sequential $E1 $E2 \/ ~sequential $E1 $E3 % 0.16/0.33 |- ~shortest_path $V2 $V2 $SP % 0.16/0.33 |- ~shortest_path $V1 $V2 $SP \/ path $V1 $V2 $SP % 0.16/0.34 |- ~path $V1 $V2 $P \/ ~shortest_path $V1 $V2 $SP \/ % 0.16/0.34 less_or_equal (length_of $SP) (length_of $P) % 0.16/0.34 |- ~less_or_equal (length_of $SP) % 0.16/0.34 (length_of (skolemFOFtoCNF_P $SP $V1 $V2)) \/ ~path $V1 $V2 $SP \/ % 0.16/0.34 $V1 = $V2 \/ shortest_path $V1 $V2 $SP % 0.16/0.34 |- ~path $V1 $V2 $SP \/ $V1 = $V2 \/ % 0.16/0.34 path $V1 $V2 (skolemFOFtoCNF_P $SP $V1 $V2) \/ shortest_path $V1 $V2 $SP % 0.16/0.34 |- ~precedes $E1 $E2 $P \/ ~precedes $E2 $E1 $P \/ % 0.16/0.34 ~shortest_path $V1 $V2 $P % 0.16/0.34 |- ~(head_of $E3 = head_of $E2) \/ ~(tail_of $E3 = tail_of $E1) \/ % 0.16/0.34 ~precedes $E1 $E2 $P \/ ~shortest_path $V1 $V2 $P % 0.16/0.34 |- ~precedes $E2 $E2 $P \/ ~shortest_path $V1 $V2 $P % 0.16/0.34 |- ~(head_of $E1 = head_of $E2) \/ ~precedes $E1 $E2 $P \/ % 0.16/0.34 ~shortest_path $V1 $V2 $P % 0.16/0.34 |- ~($P = path_cons (skolemFOFtoCNF_E_1 $P $V1 $V2) empty) \/ % 0.16/0.34 ~($V2 = head_of (skolemFOFtoCNF_E_1 $P $V1 $V2)) \/ ~path $V1 $V2 $P \/ % 0.16/0.34 ~path $V2 $V2 empty % 0.16/0.34 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.16/0.34 %------------------------------------------------------------------------------