%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : PUZ028-1 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n018.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 : Mon Jul 18 18:20:38 EDT 2022 % Result : Satisfiable 0.19s 0.35s % Output : Saturation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : PUZ028-1 : TPTP v8.1.0. Released v1.0.0. % 0.00/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n018.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 : Sat May 28 20:31:55 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.19/0.35 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.35 % 0.19/0.35 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.35 |- person one % 0.19/0.35 |- person two % 0.19/0.35 |- person three % 0.19/0.35 |- person four % 0.19/0.35 |- person five % 0.19/0.35 |- person six % 0.19/0.35 |- after one two % 0.19/0.35 |- after two three % 0.19/0.35 |- after three four % 0.19/0.35 |- after four five % 0.19/0.35 |- after five six % 0.19/0.35 |- ~after $Large $Medium \/ ~after $Medium $Small \/ after $Large $Small % 0.19/0.35 |- ~after $X $Y \/ ~person $X \/ ~person $Y \/ familiar $X $Y \/ % 0.19/0.35 not_familiar $X $Y % 0.19/0.35 |- ~familiar $X1 $X2 \/ ~familiar $X2 $X3 \/ ~familiar $X3 $X1 % 0.19/0.35 |- ~not_familiar $X1 $X2 \/ ~not_familiar $X2 $X3 \/ ~not_familiar $X3 $X1 % 0.19/0.35 |- ~familiar $X1 $X1 % 0.19/0.35 |- ~not_familiar $X1 $X1 % 0.19/0.35 |- ~after five $_4 \/ after four $_4 % 0.19/0.35 |- ~after four $_4 \/ after three $_4 % 0.19/0.35 |- ~after three $_4 \/ after two $_4 % 0.19/0.36 |- ~after $_2 five \/ after $_2 six % 0.19/0.36 |- ~after $_2 four \/ after $_2 five % 0.19/0.36 |- ~after $_2 one \/ after $_2 two % 0.19/0.36 |- ~after $_2 three \/ after $_2 four % 0.19/0.36 |- ~after $_2 two \/ after $_2 three % 0.19/0.36 |- after two four % 0.19/0.36 |- ~after $Large two \/ after $Large four % 0.19/0.36 |- ~after four $Small \/ after two $Small % 0.19/0.36 |- after one three % 0.19/0.36 |- ~after $Large one \/ after $Large three % 0.19/0.36 |- after two five % 0.19/0.36 |- ~after $Large two \/ after $Large five % 0.19/0.36 |- ~after five $Small \/ after two $Small % 0.19/0.36 |- after one four % 0.19/0.36 |- ~after $Large one \/ after $Large four % 0.19/0.36 |- ~after four $Small \/ after one $Small % 0.19/0.36 |- after four six % 0.19/0.36 |- ~after $Large four \/ after $Large six % 0.19/0.36 |- after two six % 0.19/0.36 |- ~after $Large two \/ after $Large six % 0.19/0.36 |- ~after six $Small \/ after two $Small % 0.19/0.36 |- after three five % 0.19/0.36 |- after three six % 0.19/0.36 |- ~after $Large three \/ after $Large five % 0.19/0.36 |- ~after five $Small \/ after three $Small % 0.19/0.36 |- ~after $Large three \/ after $Large six % 0.19/0.36 |- ~after six $Small \/ after three $Small % 0.19/0.36 |- after one five % 0.19/0.36 |- ~after $Large one \/ after $Large five % 0.19/0.36 |- ~after five $Small \/ after one $Small % 0.19/0.36 |- after one six % 0.19/0.36 |- ~after $Large one \/ after $Large six % 0.19/0.36 |- familiar five six \/ not_familiar five six % 0.19/0.36 |- familiar four five \/ not_familiar four five % 0.19/0.36 |- familiar four six \/ not_familiar four six % 0.19/0.36 |- familiar one five \/ not_familiar one five % 0.19/0.36 |- familiar one four \/ not_familiar one four % 0.19/0.36 |- familiar one six \/ not_familiar one six % 0.19/0.36 |- familiar one three \/ not_familiar one three % 0.19/0.36 |- familiar one two \/ not_familiar one two % 0.19/0.36 |- familiar three five \/ not_familiar three five % 0.19/0.36 |- familiar three four \/ not_familiar three four % 0.19/0.36 |- familiar three six \/ not_familiar three six % 0.19/0.36 |- familiar two five \/ not_familiar two five % 0.19/0.36 |- familiar two four \/ not_familiar two four % 0.19/0.36 |- familiar two six \/ not_familiar two six % 0.19/0.36 |- familiar two three \/ not_familiar two three % 0.19/0.36 |- ~not_familiar $X2 one \/ ~not_familiar five $X2 \/ familiar one five % 0.19/0.36 |- ~not_familiar $X2 one \/ ~not_familiar four $X2 \/ familiar one four % 0.19/0.36 |- ~not_familiar $X2 four \/ ~not_familiar five $X2 \/ familiar four five % 0.19/0.36 |- ~not_familiar $X2 three \/ ~not_familiar five $X2 \/ familiar three five % 0.19/0.36 |- ~not_familiar $X2 three \/ ~not_familiar four $X2 \/ familiar three four % 0.19/0.36 |- ~not_familiar $X2 three \/ ~not_familiar six $X2 \/ familiar three six % 0.19/0.36 |- ~not_familiar $X2 two \/ ~not_familiar five $X2 \/ familiar two five % 0.19/0.36 |- ~not_familiar $X2 two \/ ~not_familiar four $X2 \/ familiar two four % 0.19/0.36 |- ~not_familiar $X2 two \/ ~not_familiar six $X2 \/ familiar two six % 0.19/0.36 |- ~not_familiar $X2 two \/ ~not_familiar three $X2 \/ familiar two three % 0.19/0.36 |- ~not_familiar five one \/ familiar four five \/ familiar one four % 0.19/0.36 |- ~not_familiar five three \/ familiar four five \/ familiar three four % 0.19/0.36 |- ~not_familiar five two \/ familiar four five \/ familiar two four % 0.19/0.36 |- ~not_familiar five one \/ familiar one three \/ familiar three five % 0.19/0.36 |- ~not_familiar five two \/ familiar three five \/ familiar two three % 0.19/0.36 |- ~not_familiar four one \/ familiar one three \/ familiar three four % 0.19/0.36 |- ~not_familiar four two \/ familiar three four \/ familiar two three % 0.19/0.36 |- ~not_familiar six two \/ familiar three six \/ familiar two three % 0.19/0.36 |- ~not_familiar five one \/ familiar one two \/ familiar two five % 0.19/0.36 |- ~not_familiar four one \/ familiar one two \/ familiar two four % 0.19/0.36 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.36 %------------------------------------------------------------------------------