%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SYN351-1 : TPTP v8.1.0. Released v1.2.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n028.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 : Thu Jul 21 09:01:39 EDT 2022 % Result : Satisfiable 0.18s 0.46s % Output : Saturation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYN351-1 : TPTP v8.1.0. Released v1.2.0. % 0.06/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n028.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 : Mon Jul 11 21:53:29 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.18/0.46 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.46 % 0.18/0.46 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.46 |- f a $Y a (z $X $Y) % 0.18/0.46 |- ~f $X b $X $Y \/ f a $X a $Y % 0.18/0.46 |- ~f a $X a $Y \/ f $X b $X $Y % 0.18/0.46 |- f a $X a $Y \/ f a (z $X $Y) $X (z $X $Y) % 0.18/0.46 |- f a $X a $Y \/ f a $Y $X $Y % 0.18/0.46 |- f a $Y $X $Y \/ f a (z $X $Y) $X (z $X $Y) % 0.18/0.46 |- ~f a $X a $Y \/ ~f a $Y $X $Y \/ ~f a (z $X $Y) $X (z $X $Y) % 0.18/0.46 |- f a a a a % 0.18/0.46 |- f a a a (z $X b) % 0.18/0.46 |- f a b a a % 0.18/0.46 |- f $_5 b $_5 (z $X $_5) % 0.18/0.46 |- f b b b a % 0.18/0.46 |- f b b b (z $_7 a) % 0.18/0.46 |- f a $_11 b $_11 \/ f a a a $_11 % 0.18/0.46 |- f $_10 b $_10 $_11 \/ f a $_11 $_10 $_11 % 0.18/0.46 |- f a a a b % 0.18/0.46 |- f $_11 b $_11 $_11 \/ f a a a $_11 % 0.18/0.46 |- f a b a b % 0.18/0.46 |- f b b b b % 0.18/0.46 |- f $_13 b $_13 $_13 \/ f a b a $_13 % 0.18/0.46 |- f $_14 b $_14 $_14 \/ f b b b $_14 % 0.18/0.46 |- f a a a $_16 \/ f (z a $_16) b (z a $_16) (z a $_16) % 0.18/0.46 |- f a $_19 a $_19 \/ f (z a $_19) b (z a $_19) (z a $_19) % 0.18/0.46 |- f a $_21 a $_21 \/ f b b b $_21 % 0.18/0.46 |- ~f a $_27 a $_27 \/ ~f a a a $_27 \/ f b b b (z a $_27) % 0.18/0.46 |- ~f a $_27 b $_27 \/ ~f a b a $_27 \/ f a a a (z b $_27) % 0.18/0.46 |- ~f a $_26 a $_27 \/ ~f a $_27 $_26 $_27 \/ f $_26 b $_26 (z $_26 $_27) % 0.18/0.46 |- ~f a $_26 a $_27 \/ ~f a $_27 $_26 $_27 \/ f a $_26 a (z $_26 $_27) % 0.18/0.46 |- ~f a a a (z a $Y) \/ f a $Y a $Y \/ f b b b (z a (z a $Y)) % 0.18/0.46 |- ~f a a a (z a $Y) \/ f a a a $Y \/ f b b b (z a (z a $Y)) % 0.18/0.46 |- ~f a a a $_28 \/ f b b b $_28 \/ f b b b (z a $_28) % 0.18/0.46 |- ~f a a a $_28 \/ f a $_28 $_28 $_28 \/ f b b b (z a $_28) % 0.18/0.46 |- ~f a $_28 a $_28 \/ f a $_28 b $_28 \/ f b b b (z a $_28) % 0.18/0.46 |- ~f a a a $_29 \/ f a b a (z a $_29) \/ f b b b $_29 % 0.18/0.46 |- ~f a a a $_29 \/ f a $_29 $_29 $_29 \/ f a b a (z a $_29) % 0.18/0.46 |- ~f a $_29 a $_29 \/ f a $_29 b $_29 \/ f a b a (z a $_29) % 0.18/0.46 |- ~f a b a (z b $Y) \/ f a $Y b $Y \/ f a a a (z b (z b $Y)) % 0.18/0.46 |- ~f a b a (z b $Y) \/ f a a a (z b (z b $Y)) \/ f a b a $Y % 0.18/0.46 |- ~f a $_30 b $_30 \/ f a $_30 a $_30 \/ f a a a (z b $_30) % 0.18/0.46 |- ~f a $_30 b $_30 \/ f $_30 b $_30 $_30 \/ f a a a (z b $_30) % 0.18/0.46 |- f a $Y b $Y \/ f a a a (z b (z b $Y)) \/ f a (z b $Y) a (z b $Y) % 0.18/0.46 |- f a a a (z b (z b $Y)) \/ f a b a $Y \/ f a (z b $Y) a (z b $Y) % 0.18/0.46 |- f a $Y b $Y \/ f a a a (z b (z b $Y)) \/ f (z b $Y) b (z b $Y) (z b $Y) % 0.18/0.46 |- f a a a (z b (z b $Y)) \/ f a b a $Y \/ f (z b $Y) b (z b $Y) (z b $Y) % 0.18/0.46 |- f a (z $X a) (z $X a) (z $X a) \/ f b b b (z a (z $X a)) % 0.18/0.46 |- f a (z $X b) (z $X b) (z $X b) \/ f b b b (z a (z $X b)) % 0.18/0.46 |- f a $_34 $_34 $_34 \/ f a $_34 b $_34 \/ f b b b (z a $_34) % 0.18/0.46 |- f a $Y a $Y \/ f a (z a $Y) b (z a $Y) \/ f b b b (z a (z a $Y)) % 0.18/0.46 |- f a a a $Y \/ f a (z a $Y) b (z a $Y) \/ f b b b (z a (z a $Y)) % 0.18/0.47 |- f a b a (z a (z $X a)) \/ f a (z $X a) (z $X a) (z $X a) % 0.18/0.47 |- f a b a (z a (z $X b)) \/ f a (z $X b) (z $X b) (z $X b) % 0.18/0.47 |- f a $_39 $_39 $_39 \/ f a $_39 b $_39 \/ f a b a (z a $_39) % 0.18/0.47 |- f a $Y a $Y \/ f a b a (z a (z a $Y)) \/ f a (z a $Y) b (z a $Y) % 0.18/0.47 |- f a a a $Y \/ f a b a (z a (z a $Y)) \/ f a (z a $Y) b (z a $Y) % 0.18/0.47 |- ~f a $_44 b $_44 \/ f a $_44 a $_44 \/ f b b b (z b $_44) % 0.18/0.47 |- ~f a $_44 b $_44 \/ f $_44 b $_44 $_44 \/ f b b b (z b $_44) % 0.18/0.47 |- ~f a $_43 a (z $_43 $Y) \/ f $_43 b $_43 (z $_43 (z $_43 $Y)) \/ % 0.18/0.47 f a $Y $_43 $Y % 0.18/0.47 |- ~f a $_43 a (z $_43 $Y) \/ f $_43 b $_43 (z $_43 (z $_43 $Y)) \/ % 0.18/0.47 f a $_43 a $Y % 0.18/0.47 |- f a $Y b $Y \/ f a (z b $Y) a (z b $Y) \/ f b b b (z b (z b $Y)) % 0.18/0.47 |- f a b a $Y \/ f a (z b $Y) a (z b $Y) \/ f b b b (z b (z b $Y)) % 0.18/0.47 |- f a $Y b $Y \/ f b b b (z b (z b $Y)) \/ f (z b $Y) b (z b $Y) (z b $Y) % 0.18/0.47 |- f a b a $Y \/ f b b b (z b (z b $Y)) \/ f (z b $Y) b (z b $Y) (z b $Y) % 0.18/0.47 |- ~f a $_48 b $_48 \/ f a $_48 a $_48 \/ f a b a (z b $_48) % 0.18/0.47 |- ~f a $_48 a $_48 \/ f a $_48 b $_48 \/ f a a a (z a $_48) % 0.18/0.47 |- ~f a $_48 b $_48 \/ f $_48 b $_48 $_48 \/ f a b a (z b $_48) % 0.18/0.47 |- ~f a $_47 a (z $_47 $Y) \/ f a $Y $_47 $Y \/ % 0.18/0.47 f a $_47 a (z $_47 (z $_47 $Y)) % 0.18/0.47 |- ~f a $_47 a (z $_47 $Y) \/ f a $_47 a $Y \/ % 0.18/0.47 f a $_47 a (z $_47 (z $_47 $Y)) % 0.18/0.47 |- ~f a a a $_48 \/ f a a a (z a $_48) \/ f b b b $_48 % 0.18/0.47 |- ~f a a a $_48 \/ f a $_48 $_48 $_48 \/ f a a a (z a $_48) % 0.18/0.47 |- f a $Y b $Y \/ f a b a (z b (z b $Y)) \/ f a (z b $Y) a (z b $Y) % 0.18/0.47 |- f a b a $Y \/ f a b a (z b (z b $Y)) \/ f a (z b $Y) a (z b $Y) % 0.18/0.47 |- f a $Y a $Y \/ f a a a (z a (z a $Y)) \/ f a (z a $Y) b (z a $Y) % 0.18/0.47 |- f a a a $Y \/ f a a a (z a (z a $Y)) \/ f a (z a $Y) b (z a $Y) % 0.18/0.47 |- f a $_50 $_50 $_50 \/ f a $_50 b $_50 \/ f a a a (z a $_50) % 0.18/0.47 |- f a $Y b $Y \/ f a b a (z b (z b $Y)) \/ f (z b $Y) b (z b $Y) (z b $Y) % 0.18/0.47 |- f a b a $Y \/ f a b a (z b (z b $Y)) \/ f (z b $Y) b (z b $Y) (z b $Y) % 0.18/0.47 |- f a a a (z a (z $X a)) \/ f a (z $X a) (z $X a) (z $X a) % 0.18/0.47 |- f a a a (z a (z $X b)) \/ f a (z $X b) (z $X b) (z $X b) % 0.18/0.47 |- f a a a (z b (z b a)) \/ f a a b a % 0.18/0.47 |- f a a a (z b (z b b)) \/ f a b b b % 0.18/0.47 |- f a a b a \/ f a b a (z b (z b a)) % 0.18/0.47 |- f a a a (z a (z b (z b a))) \/ f a a b a \/ % 0.18/0.47 f a (z b (z b a)) (z b (z b a)) (z b (z b a)) % 0.18/0.47 |- f a a b a \/ f a b a (z a (z b (z b a))) \/ % 0.18/0.47 f a (z b (z b a)) (z b (z b a)) (z b (z b a)) % 0.18/0.47 |- f a a b a \/ f a (z b (z b a)) (z b (z b a)) (z b (z b a)) \/ % 0.18/0.47 f b b b (z a (z b (z b a))) % 0.18/0.47 |- f a a a (z a (z b (z b b))) \/ f a b b b \/ % 0.18/0.47 f a (z b (z b b)) (z b (z b b)) (z b (z b b)) % 0.18/0.47 |- f a b a (z a (z b (z b b))) \/ f a b b b \/ % 0.18/0.47 f a (z b (z b b)) (z b (z b b)) (z b (z b b)) % 0.18/0.47 |- f a b b b \/ f a (z b (z b b)) (z b (z b b)) (z b (z b b)) \/ % 0.18/0.47 f b b b (z a (z b (z b b))) % 0.18/0.47 |- f a a b a \/ f b b b (z b (z b a)) % 0.18/0.47 |- ~f a b a $_58 \/ f a $_58 $_58 $_58 \/ f a b a (z b $_58) \/ % 0.18/0.47 f b b b (z a $_58) % 0.18/0.47 |- ~f a b a $_58 \/ f a $_58 $_58 $_58 \/ f b b b (z a $_58) \/ % 0.18/0.47 f b b b (z b $_58) % 0.18/0.47 |- ~f a b a $_58 \/ f a $_58 $_58 $_58 \/ f a a a (z b $_58) \/ % 0.18/0.47 f b b b (z a $_58) % 0.18/0.47 |- ~f a b a $_59 \/ f a $_59 $_59 $_59 \/ f a b a (z a $_59) \/ % 0.18/0.47 f a b a (z b $_59) % 0.18/0.47 |- ~f a b a $_59 \/ f a $_59 $_59 $_59 \/ f a b a (z a $_59) \/ % 0.18/0.47 f b b b (z b $_59) % 0.18/0.47 |- ~f a b a $_59 \/ f a $_59 $_59 $_59 \/ f a a a (z b $_59) \/ % 0.18/0.47 f a b a (z a $_59) % 0.18/0.47 |- ~f a b a $_64 \/ f a $_64 $_64 $_64 \/ f a a a (z a $_64) \/ % 0.18/0.47 f a b a (z b $_64) % 0.18/0.47 |- ~f a b a $_64 \/ f a $_64 $_64 $_64 \/ f a a a (z a $_64) \/ % 0.18/0.47 f b b b (z b $_64) % 0.18/0.47 |- ~f a b a $_64 \/ f a $_64 $_64 $_64 \/ f a a a (z a $_64) \/ % 0.18/0.47 f a a a (z b $_64) % 0.18/0.47 |- f a $_64 $_64 $_64 \/ f a $_64 b $_64 \/ f a a a (z a (z a $_64)) \/ % 0.18/0.47 f a (z a $_64) (z a $_64) (z a $_64) % 0.18/0.47 |- f a $_64 $_64 $_64 \/ f a $_64 b $_64 \/ f a b a (z a (z a $_64)) \/ % 0.18/0.47 f a (z a $_64) (z a $_64) (z a $_64) % 0.18/0.47 |- f a $_64 $_64 $_64 \/ f a $_64 b $_64 \/ % 0.18/0.47 f a (z a $_64) (z a $_64) (z a $_64) \/ f b b b (z a (z a $_64)) % 0.18/0.47 |- ~f a a a (z b $_65) \/ f a $_65 b $_65 \/ f a a a (z a (z b $_65)) \/ % 0.18/0.47 f a a a (z b (z b $_65)) % 0.18/0.47 |- ~f a a a (z b $_65) \/ f a $_65 b $_65 \/ f a a a (z b (z b $_65)) \/ % 0.18/0.47 f a b a (z a (z b $_65)) % 0.18/0.47 |- ~f a a a (z b $_65) \/ f a $_65 b $_65 \/ f a a a (z b (z b $_65)) \/ % 0.18/0.47 f b b b (z a (z b $_65)) % 0.18/0.47 |- ~f a a a (z b $_66) \/ f a a a (z a (z b $_66)) \/ % 0.18/0.47 f a a a (z b (z b $_66)) \/ f a b a $_66 % 0.18/0.47 |- ~f a a a (z b $_66) \/ f a a a (z b (z b $_66)) \/ f a b a $_66 \/ % 0.18/0.47 f a b a (z a (z b $_66)) % 0.18/0.47 |- ~f a a a (z b $_66) \/ f a a a (z b (z b $_66)) \/ f a b a $_66 \/ % 0.18/0.47 f b b b (z a (z b $_66)) % 0.18/0.47 |- ~f a a a (z b $_67) \/ f a $_67 b $_67 \/ f a a a (z a (z b $_67)) \/ % 0.18/0.47 f b b b (z b (z b $_67)) % 0.18/0.47 |- ~f a a a (z b $_67) \/ f a $_67 b $_67 \/ f a b a (z a (z b $_67)) \/ % 0.18/0.47 f b b b (z b (z b $_67)) % 0.18/0.47 |- ~f a a a (z b $_67) \/ f a $_67 b $_67 \/ f b b b (z a (z b $_67)) \/ % 0.18/0.47 f b b b (z b (z b $_67)) % 0.18/0.47 |- ~f a a a (z b $_68) \/ f a a a (z a (z b $_68)) \/ f a b a $_68 \/ % 0.18/0.47 f b b b (z b (z b $_68)) % 0.18/0.47 |- ~f a a a (z b $_68) \/ f a b a $_68 \/ f a b a (z a (z b $_68)) \/ % 0.18/0.47 f b b b (z b (z b $_68)) % 0.18/0.47 |- ~f a a a (z b $_68) \/ f a b a $_68 \/ f b b b (z a (z b $_68)) \/ % 0.18/0.47 f b b b (z b (z b $_68)) % 0.18/0.47 |- ~f a a a (z b $_73) \/ f a $_73 b $_73 \/ f a a a (z a (z b $_73)) \/ % 0.18/0.47 f a b a (z b (z b $_73)) % 0.18/0.47 |- ~f a a a (z b $_73) \/ f a $_73 b $_73 \/ f a b a (z a (z b $_73)) \/ % 0.18/0.47 f a b a (z b (z b $_73)) % 0.18/0.47 |- ~f a a a (z b $_73) \/ f a $_73 b $_73 \/ f a b a (z b (z b $_73)) \/ % 0.18/0.47 f b b b (z a (z b $_73)) % 0.18/0.47 |- ~f a a a (z b $_74) \/ f a a a (z a (z b $_74)) \/ f a b a $_74 \/ % 0.18/0.47 f a b a (z b (z b $_74)) % 0.18/0.47 |- ~f a a a (z b $_74) \/ f a b a $_74 \/ f a b a (z a (z b $_74)) \/ % 0.18/0.47 f a b a (z b (z b $_74)) % 0.18/0.47 |- ~f a a a (z b $_74) \/ f a b a $_74 \/ f a b a (z b (z b $_74)) \/ % 0.18/0.47 f b b b (z a (z b $_74)) % 0.18/0.47 |- ~f a b a (z a $_75) \/ f a $_75 a $_75 \/ f a b a (z b (z a $_75)) \/ % 0.18/0.47 f b b b (z a (z a $_75)) % 0.18/0.47 |- ~f a b a (z a $_75) \/ f a $_75 a $_75 \/ f b b b (z a (z a $_75)) \/ % 0.18/0.47 f b b b (z b (z a $_75)) % 0.18/0.47 |- ~f a b a (z a $_75) \/ f a $_75 a $_75 \/ f a a a (z b (z a $_75)) \/ % 0.18/0.47 f b b b (z a (z a $_75)) % 0.18/0.47 |- ~f a b a (z a $_76) \/ f a a a $_76 \/ f a b a (z b (z a $_76)) \/ % 0.18/0.47 f b b b (z a (z a $_76)) % 0.18/0.47 |- ~f a b a (z a $_76) \/ f a a a $_76 \/ f b b b (z a (z a $_76)) \/ % 0.18/0.47 f b b b (z b (z a $_76)) % 0.18/0.47 |- ~f a b a (z a $_76) \/ f a a a $_76 \/ f a a a (z b (z a $_76)) \/ % 0.18/0.47 f b b b (z a (z a $_76)) % 0.18/0.47 |- ~f a b a (z a $_77) \/ f a $_77 a $_77 \/ f a b a (z a (z a $_77)) \/ % 0.18/0.47 f a b a (z b (z a $_77)) % 0.18/0.47 |- ~f a b a (z a $_77) \/ f a $_77 a $_77 \/ f a b a (z a (z a $_77)) \/ % 0.18/0.47 f b b b (z b (z a $_77)) % 0.18/0.47 |- ~f a b a (z a $_77) \/ f a $_77 a $_77 \/ f a a a (z b (z a $_77)) \/ % 0.18/0.47 f a b a (z a (z a $_77)) % 0.18/0.47 |- ~f a b a (z a $_78) \/ f a a a $_78 \/ f a b a (z a (z a $_78)) \/ % 0.18/0.47 f a b a (z b (z a $_78)) % 0.18/0.47 |- ~f a b a (z a $_78) \/ f a a a $_78 \/ f a b a (z a (z a $_78)) \/ % 0.18/0.47 f b b b (z b (z a $_78)) % 0.18/0.47 |- ~f a b a (z a $_78) \/ f a a a $_78 \/ f a a a (z b (z a $_78)) \/ % 0.18/0.47 f a b a (z a (z a $_78)) % 0.18/0.47 |- ~f a b a (z a $_79) \/ f a $_79 a $_79 \/ f a a a (z a (z a $_79)) \/ % 0.18/0.47 f a b a (z b (z a $_79)) % 0.18/0.47 |- ~f a b a (z a $_79) \/ f a $_79 a $_79 \/ f a a a (z a (z a $_79)) \/ % 0.18/0.47 f b b b (z b (z a $_79)) % 0.18/0.47 |- ~f a b a (z a $_79) \/ f a $_79 a $_79 \/ f a a a (z a (z a $_79)) \/ % 0.18/0.47 f a a a (z b (z a $_79)) % 0.18/0.47 |- ~f a b a (z a $_80) \/ f a a a $_80 \/ f a a a (z a (z a $_80)) \/ % 0.18/0.47 f a b a (z b (z a $_80)) % 0.18/0.47 |- ~f a b a (z a $_80) \/ f a a a $_80 \/ f a a a (z a (z a $_80)) \/ % 0.18/0.47 f b b b (z b (z a $_80)) % 0.18/0.47 |- ~f a b a (z a $_80) \/ f a a a $_80 \/ f a a a (z a (z a $_80)) \/ % 0.18/0.47 f a a a (z b (z a $_80)) % 0.18/0.47 |- f $_83 b $_83 (z $_83 (z $_83 $_83)) \/ f a $_83 $_83 $_83 % 0.18/0.47 |- f a $_85 $_85 $_85 \/ f a $_85 a (z $_85 (z $_85 $_85)) % 0.18/0.47 |- f $_87 b $_87 (z $_87 (z $_87 $_87)) \/ f a $_87 a $_87 % 0.18/0.47 |- f a $_89 a $_89 \/ f a $_89 a (z $_89 (z $_89 $_89)) % 0.18/0.47 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.47 %------------------------------------------------------------------------------