%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : PLA029+2 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n020.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 17:26:21 EDT 2022 % Result : Satisfiable 0.12s 0.35s % Output : Saturation 0.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : PLA029+2 : TPTP v8.1.0. Released v2.5.0. % 0.10/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n020.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 : Tue May 31 18:12:38 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.12/0.35 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.12/0.35 % 0.12/0.35 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.12/0.35 |- ~a_block $Z \/ ~destination $Z $I \/ ~neq $X $Z \/ ~nonfixed $X \/ % 0.12/0.35 ~object $X $I \/ ~time $I \/ on $X $Z (s $I) % 0.12/0.35 |- ~a_block $Y \/ ~neq $X $Y \/ ~nonfixed $X \/ ~object $X $I \/ % 0.12/0.35 ~on $X $Y (s $I) \/ ~source $Y $I \/ ~time $I % 0.12/0.35 |- ~nonfixed $Y \/ ~source $Y $I \/ ~time $I \/ clear $Y (s $I) % 0.12/0.35 |- ~clear $Z (s $I) \/ ~destination $Z $I \/ ~nonfixed $Z \/ ~time $I % 0.12/0.35 |- ~a_block $Y \/ ~neq $X $Y \/ ~nonfixed $X \/ ~object $X $I \/ % 0.12/0.35 ~source $Y $I \/ on $X $Y $I % 0.12/0.35 |- ~nonfixed $X \/ ~object $X $I \/ clear $X $I % 0.12/0.35 |- ~destination $Z $I \/ ~nonfixed $Z \/ clear $Z $I % 0.12/0.35 |- ~clear $W $I \/ ~nonfixed $W \/ ~time $I \/ clear $W (s $I) \/ % 0.12/0.35 destination $W $I % 0.12/0.35 |- ~a_block $W \/ ~neq $V $W \/ ~nonfixed $V \/ ~on $V $W $I \/ ~time $I \/ % 0.12/0.35 object $V $I \/ on $V $W (s $I) % 0.12/0.35 |- ~clear $W (s $I) \/ ~nonfixed $W \/ ~time $I \/ clear $W $I \/ % 0.12/0.35 source $W $I % 0.12/0.35 |- ~a_block $W \/ ~neq $V $W \/ ~nonfixed $V \/ ~on $V $W (s $I) \/ % 0.12/0.35 ~time $I \/ object $V $I \/ on $V $W $I % 0.12/0.35 |- ~a_block $W \/ ~neq $V $W \/ ~nonfixed $V \/ ~on $V $W (s $I) \/ % 0.12/0.35 ~time $I \/ destination $W $I \/ on $V $W $I % 0.12/0.35 |- ~a_block $X2 \/ ~neq $X1 $X2 \/ ~nonfixed $X1 \/ ~object $X1 $I \/ % 0.12/0.35 ~object $X2 $I % 0.12/0.35 |- ~a_block $Y1 \/ ~a_block $Y2 \/ ~neq $Y1 $Y2 \/ ~source $Y1 $I \/ % 0.12/0.35 ~source $Y2 $I % 0.12/0.35 |- ~a_block $Z1 \/ ~a_block $Z2 \/ ~destination $Z1 $I \/ % 0.12/0.35 ~destination $Z2 $I \/ ~neq $Z1 $Z2 % 0.12/0.35 |- ~nonfixed $X \/ ~object $X $I \/ ~source $X $I % 0.12/0.35 |- ~destination $X $I \/ ~nonfixed $X \/ ~object $X $I % 0.12/0.35 |- ~a_block $Y \/ ~destination $Y $I \/ ~source $Y $I % 0.12/0.35 |- ~a_block $X \/ ~a_block $Y \/ ~neq $X $Y \/ ~on $X $Y $I \/ ~on $Y $X $I % 0.12/0.35 |- ~a_block $X \/ ~on $X $X $I % 0.12/0.35 |- ~neq $X $Y \/ ~neq $X $Z \/ ~neq $Y $Z \/ ~nonfixed $X \/ % 0.12/0.35 ~nonfixed $Y \/ ~nonfixed $Z \/ ~on $X $Y $I \/ ~on $Z $Y $I % 0.12/0.35 |- ~a_block $Y \/ ~a_block $Z \/ ~neq $X $Y \/ ~neq $X $Z \/ ~neq $Y $Z \/ % 0.12/0.35 ~nonfixed $X \/ ~on $X $Y $I \/ ~on $X $Z $I % 0.12/0.35 |- ~clear $Y $I \/ ~nonfixed $X \/ ~nonfixed $Y \/ ~on $X $Y $I % 0.12/0.35 |- ~a_block $X \/ ~fixed $Y \/ ~on $Y $X $I % 0.12/0.35 |- ~a_block $X2 \/ ~neq $X2 $X2 \/ ~nonfixed $X2 \/ ~object $X2 $I % 0.12/0.35 |- ~a_block $Y2 \/ ~neq $Y2 $Y2 \/ ~source $Y2 $I % 0.12/0.35 |- ~a_block $Z2 \/ ~destination $Z2 $I \/ ~neq $Z2 $Z2 % 0.12/0.35 |- ~neq $Y $Z \/ ~neq $Z $Y \/ ~neq $Z $Z \/ ~nonfixed $Y \/ % 0.12/0.35 ~nonfixed $Z \/ ~on $Z $Y $I % 0.12/0.35 |- ~a_block $Z \/ ~neq $X $Z \/ ~neq $Z $Z \/ ~nonfixed $X \/ ~on $X $Z $I % 0.12/0.35 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.12/0.35 %------------------------------------------------------------------------------