%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : PLA028+1 : TPTP v8.1.0. Bugfixed v2.5.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n021.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 : CounterSatisfiable 0.39s 0.57s % Output : Saturation 0.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : PLA028+1 : TPTP v8.1.0. Bugfixed v2.5.0. % 0.04/0.13 % Command : metis --show proof --show saturation %s % 0.13/0.34 % Computer : n021.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue May 31 19:00:45 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.39/0.57 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.57 % 0.39/0.57 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.57 |- ~a_block $Z \/ ~destination $Z $I \/ ~neq $X $Z \/ ~nonfixed $X \/ % 0.39/0.57 ~object $X $I \/ ~time $I \/ on $X $Z (s $I) % 0.39/0.57 |- ~a_block $Y \/ ~neq $X $Y \/ ~nonfixed $X \/ ~object $X $I \/ % 0.39/0.57 ~on $X $Y (s $I) \/ ~source $Y $I \/ ~time $I % 0.39/0.57 |- ~nonfixed $Y \/ ~source $Y $I \/ ~time $I \/ clear $Y (s $I) % 0.39/0.57 |- ~clear $Z (s $I) \/ ~destination $Z $I \/ ~nonfixed $Z \/ ~time $I % 0.39/0.57 |- ~a_block $Y \/ ~neq $X $Y \/ ~nonfixed $X \/ ~object $X $I \/ % 0.39/0.57 ~source $Y $I \/ on $X $Y $I % 0.39/0.57 |- ~nonfixed $X \/ ~object $X $I \/ clear $X $I % 0.39/0.57 |- ~destination $Z $I \/ ~nonfixed $Z \/ clear $Z $I % 0.39/0.57 |- ~clear $W $I \/ ~nonfixed $W \/ ~time $I \/ clear $W (s $I) \/ % 0.39/0.57 destination $W $I % 0.39/0.57 |- ~a_block $W \/ ~neq $V $W \/ ~nonfixed $V \/ ~on $V $W $I \/ ~time $I \/ % 0.39/0.57 object $V $I \/ on $V $W (s $I) % 0.39/0.57 |- ~clear $W (s $I) \/ ~nonfixed $W \/ ~time $I \/ clear $W $I \/ % 0.39/0.57 source $W $I % 0.39/0.57 |- ~a_block $W \/ ~neq $V $W \/ ~nonfixed $V \/ ~on $V $W (s $I) \/ % 0.39/0.57 ~time $I \/ object $V $I \/ on $V $W $I % 0.39/0.57 |- ~a_block $W \/ ~neq $V $W \/ ~nonfixed $V \/ ~on $V $W (s $I) \/ % 0.39/0.57 ~time $I \/ destination $W $I \/ on $V $W $I % 0.39/0.57 |- ~a_block $X2 \/ ~neq $X1 $X2 \/ ~nonfixed $X1 \/ ~object $X1 $I \/ % 0.39/0.57 ~object $X2 $I % 0.39/0.57 |- ~a_block $Y1 \/ ~a_block $Y2 \/ ~neq $Y1 $Y2 \/ ~source $Y1 $I \/ % 0.39/0.57 ~source $Y2 $I % 0.39/0.57 |- ~a_block $Z1 \/ ~a_block $Z2 \/ ~destination $Z1 $I \/ % 0.39/0.57 ~destination $Z2 $I \/ ~neq $Z1 $Z2 % 0.39/0.57 |- ~nonfixed $X \/ ~object $X $I \/ ~source $X $I % 0.39/0.57 |- ~destination $X $I \/ ~nonfixed $X \/ ~object $X $I % 0.39/0.57 |- ~a_block $Y \/ ~destination $Y $I \/ ~source $Y $I % 0.39/0.57 |- ~a_block $X \/ ~a_block $Y \/ ~neq $X $Y \/ ~on $X $Y $I \/ ~on $Y $X $I % 0.39/0.57 |- ~a_block $X \/ ~on $X $X $I % 0.39/0.57 |- ~neq $X $Y \/ ~neq $X $Z \/ ~neq $Y $Z \/ ~nonfixed $X \/ % 0.39/0.57 ~nonfixed $Y \/ ~nonfixed $Z \/ ~on $X $Y $I \/ ~on $Z $Y $I % 0.39/0.57 |- ~a_block $Y \/ ~a_block $Z \/ ~neq $X $Y \/ ~neq $X $Z \/ ~neq $Y $Z \/ % 0.39/0.57 ~nonfixed $X \/ ~on $X $Y $I \/ ~on $X $Z $I % 0.39/0.57 |- ~clear $Y $I \/ ~nonfixed $X \/ ~nonfixed $Y \/ ~on $X $Y $I % 0.39/0.57 |- ~a_block $X \/ ~fixed $Y \/ ~on $Y $X $I % 0.39/0.57 |- ~different $X $Y \/ neq $X $Y % 0.39/0.57 |- ~different $Y $X \/ neq $X $Y % 0.39/0.57 |- different block_1 block_2 % 0.39/0.57 |- different block_1 table % 0.39/0.57 |- different block_2 table % 0.39/0.57 |- a_block block_1 % 0.39/0.57 |- a_block block_2 % 0.39/0.57 |- a_block table % 0.39/0.57 |- fixed table % 0.39/0.57 |- nonfixed block_1 % 0.39/0.57 |- nonfixed block_2 % 0.39/0.57 |- time time_0 % 0.39/0.57 |- time (s time_0) % 0.39/0.57 |- ~time $I \/ source block_1 $I \/ source block_2 $I \/ source table $I % 0.39/0.57 |- ~time $I \/ destination block_1 $I \/ destination block_2 $I \/ % 0.39/0.57 destination table $I % 0.39/0.57 |- ~time $I \/ object block_1 $I \/ object block_2 $I % 0.39/0.57 |- on block_1 table time_0 % 0.39/0.57 |- clear block_1 time_0 % 0.39/0.57 |- on block_2 table time_0 % 0.39/0.57 |- clear block_2 time_0 % 0.39/0.57 |- goal_time (s time_0) % 0.39/0.57 |- ~a_block $X2 \/ ~neq $X2 $X2 \/ ~nonfixed $X2 \/ ~object $X2 $I % 0.39/0.57 |- ~a_block $Y2 \/ ~neq $Y2 $Y2 \/ ~source $Y2 $I % 0.39/0.57 |- ~a_block $Z2 \/ ~destination $Z2 $I \/ ~neq $Z2 $Z2 % 0.39/0.57 |- ~neq $Y $Z \/ ~neq $Z $Y \/ ~neq $Z $Z \/ ~nonfixed $Y \/ % 0.39/0.57 ~nonfixed $Z \/ ~on $Z $Y $I % 0.39/0.57 |- ~a_block $Z \/ ~neq $X $Z \/ ~neq $Z $Z \/ ~nonfixed $X \/ ~on $X $Z $I % 0.39/0.57 |- ~clear block_1 skolemFOFtoCNF_S % 0.39/0.57 |- goal_time skolemFOFtoCNF_S % 0.39/0.57 |- neq block_1 block_2 % 0.39/0.57 |- neq block_1 table % 0.39/0.57 |- neq block_2 table % 0.39/0.57 |- neq block_2 block_1 % 0.39/0.57 |- neq table block_1 % 0.39/0.57 |- neq table block_2 % 0.39/0.57 |- object block_1 (s time_0) \/ object block_2 (s time_0) % 0.39/0.57 |- object block_1 time_0 \/ object block_2 time_0 % 0.39/0.57 |- clear block_2 (s time_0) \/ object block_1 (s time_0) % 0.39/0.57 |- clear block_1 (s time_0) \/ clear block_2 (s time_0) % 0.39/0.57 |- ~destination block_1 (s time_0) \/ clear block_2 (s time_0) % 0.39/0.57 |- ~destination block_2 (s time_0) \/ object block_1 (s time_0) % 0.39/0.57 |- ~destination block_2 time_0 \/ object block_1 time_0 % 0.39/0.57 |- source block_1 (s time_0) \/ source block_2 (s time_0) \/ % 0.39/0.57 source table (s time_0) % 0.39/0.57 |- source block_1 time_0 \/ source block_2 time_0 \/ source table time_0 % 0.39/0.57 |- ~destination table time_0 \/ source block_1 time_0 \/ % 0.39/0.57 source block_2 time_0 % 0.39/0.57 |- ~destination table (s time_0) \/ source block_1 (s time_0) \/ % 0.39/0.57 source block_2 (s time_0) % 0.39/0.57 |- destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.39/0.57 destination table (s time_0) % 0.39/0.57 |- destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.39/0.57 source block_1 (s time_0) \/ source block_2 (s time_0) % 0.39/0.57 |- ~neq block_2 block_2 \/ destination block_1 (s time_0) \/ % 0.39/0.57 destination block_2 (s time_0) \/ source block_1 (s time_0) % 0.39/0.57 |- ~object block_2 (s time_0) \/ destination block_1 (s time_0) \/ % 0.39/0.57 destination block_2 (s time_0) \/ source block_1 (s time_0) % 0.39/0.57 |- ~fixed block_1 % 0.39/0.57 |- ~fixed block_2 % 0.39/0.57 |- destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.39/0.57 object block_1 (s time_0) \/ source block_1 (s time_0) % 0.39/0.57 |- ~neq block_1 block_1 \/ destination block_1 (s time_0) \/ % 0.39/0.57 destination block_2 (s time_0) \/ object block_1 (s time_0) % 0.39/0.57 |- ~neq block_1 block_1 \/ clear block_2 (s time_0) % 0.39/0.57 |- ~neq block_2 block_2 \/ object block_1 (s time_0) % 0.39/0.57 |- ~neq block_2 block_2 \/ object block_1 time_0 % 0.39/0.57 |- clear block_1 (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.39/0.57 destination block_2 (s time_0) \/ object block_1 (s time_0) % 0.41/0.57 |- clear block_2 (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.57 destination block_2 (s time_0) \/ source block_1 (s time_0) % 0.41/0.57 |- ~destination block_2 time_0 \/ clear block_1 (s time_0) % 0.41/0.57 |- ~time (s (s time_0)) \/ clear block_1 (s (s (s time_0))) \/ % 0.41/0.57 destination block_1 (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.57 destination block_2 (s time_0) \/ object block_1 (s time_0) % 0.41/0.57 |- clear block_1 (s time_0) \/ destination block_1 time_0 % 0.41/0.57 |- ~time (s (s time_0)) \/ clear block_2 (s (s (s time_0))) \/ % 0.41/0.57 destination block_1 (s time_0) \/ destination block_2 (s (s time_0)) \/ % 0.41/0.57 destination block_2 (s time_0) \/ source block_1 (s time_0) % 0.41/0.57 |- clear block_1 (s time_0) \/ clear block_2 (s (s time_0)) \/ % 0.41/0.57 destination block_2 (s time_0) % 0.41/0.57 |- clear block_2 (s time_0) \/ destination block_2 time_0 % 0.41/0.57 |- clear block_2 (s (s time_0)) \/ destination block_2 (s time_0) \/ % 0.41/0.57 destination block_2 time_0 % 0.41/0.57 |- clear block_1 (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.57 destination block_1 time_0 % 0.41/0.57 |- ~time (s (s time_0)) \/ clear block_2 (s (s (s time_0))) \/ % 0.41/0.57 destination block_2 (s (s time_0)) \/ destination block_2 (s time_0) \/ % 0.41/0.57 destination block_2 time_0 % 0.41/0.57 |- ~time (s (s time_0)) \/ clear block_1 (s (s (s time_0))) \/ % 0.41/0.57 destination block_1 (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.57 destination block_1 time_0 % 0.41/0.57 |- ~time (s (s time_0)) \/ clear block_1 (s time_0) \/ % 0.41/0.57 clear block_2 (s (s (s time_0))) \/ % 0.41/0.57 destination block_2 (s (s time_0)) \/ destination block_2 (s time_0) % 0.41/0.57 |- ~a_block $_41 \/ ~neq block_1 $_41 \/ ~object $_41 (s time_0) \/ % 0.41/0.57 clear block_2 (s time_0) % 0.41/0.57 |- ~a_block $_41 \/ ~neq block_2 $_41 \/ ~object $_41 (s time_0) \/ % 0.41/0.57 object block_1 (s time_0) % 0.41/0.57 |- ~a_block $_41 \/ ~neq block_2 $_41 \/ ~object $_41 time_0 \/ % 0.41/0.57 object block_1 time_0 % 0.41/0.57 |- ~neq $_40 block_1 \/ ~nonfixed $_40 \/ ~object $_40 (s time_0) \/ % 0.41/0.57 clear block_2 (s time_0) % 0.41/0.57 |- ~neq $_40 block_2 \/ ~nonfixed $_40 \/ ~object $_40 (s time_0) \/ % 0.41/0.57 object block_1 (s time_0) % 0.41/0.57 |- ~neq $_40 block_2 \/ ~nonfixed $_40 \/ ~object $_40 time_0 \/ % 0.41/0.57 object block_1 time_0 % 0.41/0.57 |- ~a_block $_50 \/ ~neq block_1 $_50 \/ ~source $_50 (s time_0) \/ % 0.41/0.57 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.57 object block_1 (s time_0) % 0.41/0.58 |- ~a_block $_50 \/ ~neq block_2 $_50 \/ ~source $_50 (s time_0) \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 source block_1 (s time_0) % 0.41/0.58 |- ~a_block $_50 \/ ~neq table $_50 \/ ~source $_50 (s time_0) \/ % 0.41/0.58 source block_1 (s time_0) \/ source block_2 (s time_0) % 0.41/0.58 |- ~a_block $_50 \/ ~neq table $_50 \/ ~source $_50 time_0 \/ % 0.41/0.58 source block_1 time_0 \/ source block_2 time_0 % 0.41/0.58 |- ~a_block $_49 \/ ~neq $_49 block_1 \/ ~source $_49 (s time_0) \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_1 (s time_0) % 0.41/0.58 |- ~a_block $_49 \/ ~neq $_49 block_2 \/ ~source $_49 (s time_0) \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 source block_1 (s time_0) % 0.41/0.58 |- ~a_block $_49 \/ ~neq $_49 table \/ ~source $_49 (s time_0) \/ % 0.41/0.58 source block_1 (s time_0) \/ source block_2 (s time_0) % 0.41/0.58 |- ~a_block $_49 \/ ~neq $_49 table \/ ~source $_49 time_0 \/ % 0.41/0.58 source block_1 time_0 \/ source block_2 time_0 % 0.41/0.58 |- ~a_block $_57 \/ ~destination $_57 (s time_0) \/ ~neq table $_57 \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 (s time_0) % 0.41/0.58 |- ~a_block $_56 \/ ~destination $_56 (s time_0) \/ ~neq $_56 table \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 (s time_0) % 0.41/0.58 |- ~destination block_1 $_55 \/ ~destination block_2 $_55 % 0.41/0.58 |- ~destination block_1 $_55 \/ ~destination table $_55 % 0.41/0.58 |- ~destination block_2 $_55 \/ ~destination table $_55 % 0.41/0.58 |- ~neq table table % 0.41/0.58 |- ~neq $_74 block_1 \/ ~nonfixed $_74 \/ ~object $_74 (s time_0) \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_1 (s time_0) \/ on $_74 block_1 (s time_0) % 0.41/0.58 |- ~neq $_74 block_2 \/ ~nonfixed $_74 \/ ~object $_74 (s time_0) \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 on $_74 block_2 (s time_0) \/ source block_1 (s time_0) % 0.41/0.58 |- ~neq $_74 table \/ ~nonfixed $_74 \/ ~object $_74 (s time_0) \/ % 0.41/0.58 on $_74 table (s time_0) \/ source block_1 (s time_0) \/ % 0.41/0.58 source block_2 (s time_0) % 0.41/0.58 |- ~neq $_74 table \/ ~nonfixed $_74 \/ ~object $_74 time_0 \/ % 0.41/0.58 on $_74 table time_0 \/ source block_1 time_0 \/ source block_2 time_0 % 0.41/0.58 |- clear block_2 (s time_0) \/ on block_1 table (s time_0) \/ % 0.41/0.58 source block_1 (s time_0) \/ source block_2 (s time_0) % 0.41/0.58 |- object block_1 (s time_0) \/ on block_2 table (s time_0) \/ % 0.41/0.58 source block_1 (s time_0) \/ source block_2 (s time_0) % 0.41/0.58 |- destination block_1 time_0 \/ destination block_2 time_0 % 0.41/0.58 |- destination block_1 time_0 \/ object block_1 time_0 % 0.41/0.58 |- ~neq $X1 block_1 \/ ~nonfixed $X1 \/ ~object $X1 time_0 \/ % 0.41/0.58 destination block_1 time_0 % 0.41/0.58 |- ~a_block $X2 \/ ~neq block_1 $X2 \/ ~object $X2 time_0 \/ % 0.41/0.58 destination block_1 time_0 % 0.41/0.58 |- ~neq block_1 block_1 \/ destination block_1 time_0 % 0.41/0.58 |- destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_1 (s time_0) \/ on block_2 block_1 (s time_0) % 0.41/0.58 |- ~on block_1 block_2 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_2 (s time_0) \/ object block_1 (s time_0) % 0.41/0.58 |- ~clear block_1 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_2 (s time_0) \/ object block_1 (s time_0) % 0.41/0.58 |- destination block_1 (s time_0) \/ destination block_1 time_0 \/ % 0.41/0.58 destination block_2 (s time_0) \/ object block_1 (s time_0) % 0.41/0.58 |- ~neq $X1 block_1 \/ ~nonfixed $X1 \/ ~object $X1 (s time_0) \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_1 time_0 \/ % 0.41/0.58 destination block_2 (s time_0) % 0.41/0.58 |- ~a_block $X2 \/ ~neq block_1 $X2 \/ ~object $X2 (s time_0) \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_1 time_0 \/ % 0.41/0.58 destination block_2 (s time_0) % 0.41/0.58 |- clear block_2 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_2 (s time_0) \/ on block_1 block_2 (s time_0) \/ % 0.41/0.58 source block_1 (s time_0) % 0.41/0.58 |- ~a_block $_97 \/ ~destination $_97 (s time_0) \/ ~neq block_1 $_97 \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_1 time_0 \/ % 0.41/0.58 destination block_2 (s time_0) \/ on block_1 $_97 (s (s time_0)) % 0.41/0.58 |- ~a_block $_97 \/ ~destination $_97 (s time_0) \/ ~neq block_1 $_97 \/ % 0.41/0.58 clear block_2 (s time_0) \/ on block_1 $_97 (s (s time_0)) % 0.41/0.58 |- ~a_block $_97 \/ ~destination $_97 time_0 \/ ~neq block_1 $_97 \/ % 0.41/0.58 destination block_1 time_0 \/ on block_1 $_97 (s time_0) % 0.41/0.58 |- ~a_block $_97 \/ ~destination $_97 (s time_0) \/ ~neq block_2 $_97 \/ % 0.41/0.58 object block_1 (s time_0) \/ on block_2 $_97 (s (s time_0)) % 0.41/0.58 |- ~a_block $_97 \/ ~destination $_97 time_0 \/ ~neq block_2 $_97 \/ % 0.41/0.58 object block_1 time_0 \/ on block_2 $_97 (s time_0) % 0.41/0.58 |- ~destination table time_0 \/ destination block_1 time_0 \/ % 0.41/0.58 on block_1 table (s time_0) % 0.41/0.58 |- destination block_1 time_0 \/ on block_1 block_2 (s time_0) % 0.41/0.58 |- ~neq block_2 block_2 \/ destination block_1 time_0 % 0.41/0.58 |- ~clear block_2 (s time_0) \/ destination block_1 time_0 % 0.41/0.58 |- ~destination block_1 time_0 \/ object block_1 time_0 \/ % 0.41/0.58 on block_2 block_1 (s time_0) % 0.41/0.58 |- ~destination table time_0 \/ object block_1 time_0 \/ % 0.41/0.58 on block_2 table (s time_0) % 0.41/0.58 |- clear block_2 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_2 (s time_0) \/ on block_1 table (s (s time_0)) % 0.41/0.58 |- destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_1 (s time_0) \/ on block_2 table (s (s time_0)) % 0.41/0.58 |- destination block_1 (s time_0) \/ destination block_1 time_0 \/ % 0.41/0.58 destination block_2 (s time_0) \/ on block_1 table (s (s time_0)) % 0.41/0.58 |- ~object block_1 time_0 \/ ~source block_2 time_0 \/ % 0.41/0.58 destination block_1 time_0 % 0.41/0.58 |- ~object block_1 time_0 \/ ~source block_2 time_0 \/ % 0.41/0.58 clear block_2 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_2 (s time_0) \/ source block_1 (s time_0) % 0.41/0.58 |- ~object block_1 (s time_0) \/ ~source table (s time_0) \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_1 time_0 \/ % 0.41/0.58 destination block_2 (s time_0) % 0.41/0.58 |- ~object block_1 (s time_0) \/ ~source table (s time_0) \/ % 0.41/0.58 clear block_2 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_2 (s time_0) % 0.41/0.58 |- ~object block_1 time_0 \/ ~source table time_0 \/ % 0.41/0.58 clear block_2 (s time_0) \/ source block_1 (s time_0) \/ % 0.41/0.58 source block_2 (s time_0) % 0.41/0.58 |- ~object block_2 time_0 \/ ~source block_1 time_0 \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_1 (s time_0) % 0.41/0.58 |- ~object block_2 (s time_0) \/ ~source table (s time_0) \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_1 (s time_0) % 0.41/0.58 |- ~object block_2 time_0 \/ ~source table time_0 \/ % 0.41/0.58 object block_1 (s time_0) \/ source block_1 (s time_0) \/ % 0.41/0.58 source block_2 (s time_0) % 0.41/0.58 |- ~object block_1 time_0 \/ clear block_2 (s time_0) \/ % 0.41/0.58 source block_1 (s time_0) \/ source block_1 time_0 \/ % 0.41/0.58 source block_2 (s time_0) \/ source block_2 time_0 % 0.41/0.58 |- ~object block_2 time_0 \/ object block_1 (s time_0) \/ % 0.41/0.58 source block_1 (s time_0) \/ source block_1 time_0 \/ % 0.41/0.58 source block_2 (s time_0) \/ source block_2 time_0 % 0.41/0.58 |- object block_1 (s time_0) \/ object block_1 time_0 \/ % 0.41/0.58 source block_1 (s time_0) \/ source block_1 time_0 \/ % 0.41/0.58 source block_2 time_0 % 0.41/0.58 |- ~neq $X block_1 \/ ~nonfixed $X \/ ~object $X (s time_0) \/ % 0.41/0.58 object block_1 (s time_0) \/ object block_1 time_0 \/ % 0.41/0.58 on $X block_1 (s time_0) \/ source block_1 time_0 \/ % 0.41/0.58 source block_2 time_0 % 0.41/0.58 |- ~a_block $Y1 \/ ~neq $Y1 block_1 \/ ~source $Y1 (s time_0) \/ % 0.41/0.58 object block_1 (s time_0) \/ object block_1 time_0 \/ % 0.41/0.58 source block_1 time_0 \/ source block_2 time_0 % 0.41/0.58 |- ~a_block $Y2 \/ ~neq block_1 $Y2 \/ ~source $Y2 (s time_0) \/ % 0.41/0.58 object block_1 (s time_0) \/ object block_1 time_0 \/ % 0.41/0.58 source block_1 time_0 \/ source block_2 time_0 % 0.41/0.58 |- clear block_1 (s (s time_0)) \/ object block_1 (s time_0) \/ % 0.41/0.58 object block_1 time_0 \/ source block_1 time_0 \/ source block_2 time_0 % 0.41/0.58 |- ~neq block_1 block_1 \/ object block_1 (s time_0) \/ % 0.41/0.58 object block_1 time_0 \/ source block_1 time_0 \/ source block_2 time_0 % 0.41/0.58 |- ~destination block_1 (s time_0) \/ object block_1 (s time_0) \/ % 0.41/0.58 object block_1 time_0 \/ source block_1 time_0 \/ source block_2 time_0 % 0.41/0.58 |- ~time (s (s time_0)) \/ clear block_1 (s (s (s time_0))) \/ % 0.41/0.58 destination block_1 (s (s time_0)) \/ object block_1 (s time_0) \/ % 0.41/0.58 object block_1 time_0 \/ source block_1 time_0 \/ source block_2 time_0 % 0.41/0.58 |- destination block_1 time_0 \/ object block_1 (s time_0) \/ % 0.41/0.58 on block_1 block_2 (s (s time_0)) % 0.41/0.58 |- ~time (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_1 time_0 \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_1 (s (s time_0)) \/ on block_1 table (s (s (s time_0))) % 0.41/0.58 |- ~time (s (s time_0)) \/ clear block_2 (s time_0) \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_1 (s (s time_0)) \/ on block_1 table (s (s (s time_0))) % 0.41/0.58 |- object block_1 time_0 \/ on block_1 table (s time_0) % 0.41/0.58 |- ~time (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_2 (s time_0) \/ object block_1 (s time_0) \/ % 0.41/0.58 object block_2 (s (s time_0)) \/ on block_2 table (s (s (s time_0))) % 0.41/0.58 |- object block_2 time_0 \/ on block_2 table (s time_0) % 0.41/0.58 |- object block_1 (s time_0) \/ object block_1 time_0 \/ % 0.41/0.58 on block_1 table (s (s time_0)) % 0.41/0.58 |- object block_2 (s time_0) \/ object block_2 time_0 \/ % 0.41/0.58 on block_2 table (s (s time_0)) % 0.41/0.58 |- ~time (s (s time_0)) \/ destination block_1 time_0 \/ % 0.41/0.58 object block_1 (s (s time_0)) \/ object block_1 (s time_0) \/ % 0.41/0.58 on block_1 block_2 (s (s (s time_0))) % 0.41/0.58 |- ~clear block_2 (s (s time_0)) \/ destination block_1 time_0 \/ % 0.41/0.58 object block_1 (s time_0) % 0.41/0.58 |- ~time (s (s time_0)) \/ object block_1 (s (s time_0)) \/ % 0.41/0.58 object block_1 (s time_0) \/ object block_1 time_0 \/ % 0.41/0.58 on block_1 table (s (s (s time_0))) % 0.41/0.58 |- ~time (s (s time_0)) \/ object block_2 (s (s time_0)) \/ % 0.41/0.58 object block_2 (s time_0) \/ object block_2 time_0 \/ % 0.41/0.58 on block_2 table (s (s (s time_0))) % 0.41/0.58 |- destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_1 (s time_0) \/ object block_2 time_0 % 0.41/0.58 |- ~a_block $Z \/ ~destination $Z (s time_0) \/ ~neq block_1 $Z \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_2 time_0 \/ on block_1 $Z (s (s time_0)) % 0.41/0.58 |- ~neq $X1 block_1 \/ ~nonfixed $X1 \/ ~object $X1 (s time_0) \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_2 time_0 % 0.41/0.58 |- ~a_block $X2 \/ ~neq block_1 $X2 \/ ~object $X2 (s time_0) \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_2 time_0 % 0.41/0.58 |- ~neq block_1 block_1 \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_2 (s time_0) \/ object block_2 time_0 % 0.41/0.58 |- destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_2 time_0 \/ on block_1 block_2 (s time_0) \/ % 0.41/0.58 source block_1 (s time_0) % 0.41/0.58 |- clear block_1 (s time_0) \/ object block_2 time_0 % 0.41/0.58 |- clear block_1 (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.58 object block_2 time_0 % 0.41/0.58 |- ~destination block_1 time_0 \/ object block_2 time_0 % 0.41/0.58 |- ~time (s (s time_0)) \/ clear block_1 (s (s (s time_0))) \/ % 0.41/0.58 destination block_1 (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.58 object block_2 time_0 % 0.41/0.58 |- clear block_2 (s time_0) \/ object block_1 time_0 % 0.41/0.58 |- clear block_2 (s (s time_0)) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_1 time_0 % 0.41/0.58 |- ~time (s (s time_0)) \/ clear block_2 (s (s (s time_0))) \/ % 0.41/0.58 destination block_2 (s (s time_0)) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_1 time_0 % 0.41/0.58 |- ~clear block_2 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_2 (s time_0) \/ object block_2 time_0 \/ % 0.41/0.58 source block_1 (s time_0) % 0.41/0.58 |- ~object block_1 time_0 \/ ~source block_2 time_0 \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_2 time_0 \/ source block_1 (s time_0) % 0.41/0.58 |- destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 destination block_2 time_0 \/ object block_2 time_0 % 0.41/0.58 |- ~a_block $Z1 \/ ~destination $Z1 (s time_0) \/ ~neq $Z1 block_2 \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 time_0 \/ % 0.41/0.58 object block_2 time_0 % 0.41/0.58 |- ~a_block $Z2 \/ ~destination $Z2 (s time_0) \/ ~neq block_2 $Z2 \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 time_0 \/ % 0.41/0.58 object block_2 time_0 % 0.41/0.58 |- ~neq block_2 block_2 \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_2 time_0 \/ object block_2 time_0 % 0.41/0.58 |- destination block_1 (s time_0) \/ destination block_2 time_0 \/ % 0.41/0.58 object block_1 (s time_0) \/ object block_2 time_0 % 0.41/0.58 |- ~a_block $Z \/ ~destination $Z (s time_0) \/ ~neq block_1 $Z \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 time_0 \/ % 0.41/0.58 object block_2 time_0 \/ on block_1 $Z (s (s time_0)) % 0.41/0.58 |- ~neq $X1 block_1 \/ ~nonfixed $X1 \/ ~object $X1 (s time_0) \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 time_0 \/ % 0.41/0.58 object block_2 time_0 % 0.41/0.58 |- ~a_block $X2 \/ ~neq block_1 $X2 \/ ~object $X2 (s time_0) \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 time_0 \/ % 0.41/0.58 object block_2 time_0 % 0.41/0.58 |- ~neq block_1 block_1 \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_2 time_0 \/ object block_2 time_0 % 0.41/0.58 |- destination block_1 (s time_0) \/ destination block_2 time_0 \/ % 0.41/0.58 object block_2 time_0 \/ on block_1 table (s time_0) \/ % 0.41/0.58 source block_1 (s time_0) \/ source block_2 (s time_0) % 0.41/0.58 |- ~object block_1 time_0 \/ ~source table time_0 \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 time_0 \/ % 0.41/0.58 object block_2 time_0 \/ source block_1 (s time_0) \/ % 0.41/0.58 source block_2 (s time_0) % 0.41/0.58 |- ~object block_1 time_0 \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_2 time_0 \/ object block_2 time_0 \/ % 0.41/0.58 source block_1 (s time_0) \/ source block_1 time_0 \/ % 0.41/0.58 source block_2 (s time_0) \/ source block_2 time_0 % 0.41/0.58 |- destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_2 time_0 \/ on block_1 table (s (s time_0)) % 0.41/0.58 |- ~time (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_2 (s time_0) \/ object block_1 (s (s time_0)) \/ % 0.41/0.58 object block_2 time_0 \/ on block_1 table (s (s (s time_0))) % 0.41/0.58 |- ~object block_1 (s time_0) \/ ~source table (s time_0) \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 object block_2 time_0 % 0.41/0.58 |- ~neq block_1 $_129 \/ ~neq block_2 $_129 \/ ~nonfixed $_129 \/ % 0.41/0.58 ~on $_129 block_2 (s (s time_0)) \/ destination block_1 time_0 \/ % 0.41/0.58 object block_1 (s time_0) % 0.41/0.58 |- ~neq block_1 $_129 \/ ~neq block_2 $_129 \/ ~nonfixed $_129 \/ % 0.41/0.58 ~on $_129 block_2 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_2 (s time_0) \/ object block_2 time_0 \/ % 0.41/0.58 source block_1 (s time_0) % 0.41/0.58 |- ~neq block_1 $_129 \/ ~neq block_2 $_129 \/ ~nonfixed $_129 \/ % 0.41/0.58 ~on $_129 block_2 (s time_0) \/ destination block_1 time_0 % 0.41/0.58 |- ~neq block_1 $_129 \/ ~neq block_2 $_129 \/ ~nonfixed $_129 \/ % 0.41/0.58 ~on $_129 block_2 (s time_0) \/ clear block_2 (s time_0) \/ % 0.41/0.58 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.58 source block_1 (s time_0) % 0.41/0.58 |- ~neq block_1 $_129 \/ ~neq block_2 $_129 \/ ~nonfixed $_129 \/ % 0.41/0.58 ~on $_129 block_1 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_2 (s time_0) \/ object block_1 (s time_0) % 0.41/0.58 |- ~neq $_127 block_1 \/ ~neq $_127 block_2 \/ ~nonfixed $_127 \/ % 0.41/0.58 ~on $_127 block_2 (s (s time_0)) \/ destination block_1 time_0 \/ % 0.41/0.58 object block_1 (s time_0) % 0.41/0.58 |- ~neq $_127 block_1 \/ ~neq $_127 block_2 \/ ~nonfixed $_127 \/ % 0.41/0.58 ~on $_127 block_2 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.58 destination block_2 (s time_0) \/ object block_2 time_0 \/ % 0.41/0.58 source block_1 (s time_0) % 0.41/0.59 |- ~neq $_127 block_1 \/ ~neq $_127 block_2 \/ ~nonfixed $_127 \/ % 0.41/0.59 ~on $_127 block_2 (s time_0) \/ destination block_1 time_0 % 0.41/0.59 |- ~neq $_127 block_1 \/ ~neq $_127 block_2 \/ ~nonfixed $_127 \/ % 0.41/0.59 ~on $_127 block_2 (s time_0) \/ clear block_2 (s time_0) \/ % 0.41/0.59 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.59 source block_1 (s time_0) % 0.41/0.59 |- ~neq $_127 block_1 \/ ~neq $_127 block_2 \/ ~nonfixed $_127 \/ % 0.41/0.59 ~on $_127 block_1 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 (s time_0) \/ object block_1 (s time_0) % 0.41/0.59 |- ~nonfixed table % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_1 $_144 \/ ~neq block_2 $_144 \/ % 0.41/0.59 ~on block_1 $_144 (s (s time_0)) \/ destination block_1 time_0 \/ % 0.41/0.59 object block_1 (s time_0) % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_1 $_144 \/ ~neq block_2 $_144 \/ % 0.41/0.59 ~on block_1 $_144 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 (s time_0) \/ object block_2 time_0 \/ % 0.41/0.59 source block_1 (s time_0) % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_1 $_144 \/ ~neq block_2 $_144 \/ % 0.41/0.59 ~on block_1 $_144 (s time_0) \/ destination block_1 time_0 % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_1 $_144 \/ ~neq block_2 $_144 \/ % 0.41/0.59 ~on block_1 $_144 (s time_0) \/ clear block_2 (s time_0) \/ % 0.41/0.59 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.59 source block_1 (s time_0) % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_1 $_144 \/ ~neq table $_144 \/ % 0.41/0.59 ~on block_1 $_144 (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 (s time_0) \/ object block_2 time_0 % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_1 $_144 \/ ~neq table $_144 \/ % 0.41/0.59 ~on block_1 $_144 (s (s time_0)) \/ object block_1 (s time_0) \/ % 0.41/0.59 object block_1 time_0 % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_1 $_144 \/ ~neq table $_144 \/ % 0.41/0.59 ~on block_1 $_144 (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_1 time_0 \/ destination block_2 (s time_0) % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_1 $_144 \/ ~neq table $_144 \/ % 0.41/0.59 ~on block_1 $_144 (s (s time_0)) \/ clear block_2 (s time_0) \/ % 0.41/0.59 destination block_1 (s time_0) \/ destination block_2 (s time_0) % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_1 $_144 \/ ~neq table $_144 \/ % 0.41/0.59 ~on block_1 $_144 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 time_0 \/ object block_2 time_0 \/ % 0.41/0.59 source block_1 (s time_0) \/ source block_2 (s time_0) % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_1 $_144 \/ ~neq table $_144 \/ % 0.41/0.59 ~on block_1 $_144 (s time_0) \/ object block_1 time_0 % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_1 $_144 \/ ~neq table $_144 \/ % 0.41/0.59 ~on block_1 $_144 (s time_0) \/ clear block_2 (s time_0) \/ % 0.41/0.59 source block_1 (s time_0) \/ source block_2 (s time_0) % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_1 $_144 \/ ~neq table $_144 \/ % 0.41/0.59 ~on block_1 $_144 time_0 % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_1 $_144 \/ ~neq block_2 $_144 \/ % 0.41/0.59 ~on block_2 $_144 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 (s time_0) \/ object block_1 (s time_0) % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_2 $_144 \/ ~neq table $_144 \/ % 0.41/0.59 ~on block_2 $_144 (s (s time_0)) \/ object block_2 (s time_0) \/ % 0.41/0.59 object block_2 time_0 % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_2 $_144 \/ ~neq table $_144 \/ % 0.41/0.59 ~on block_2 $_144 (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 (s time_0) \/ object block_1 (s time_0) % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_2 $_144 \/ ~neq table $_144 \/ % 0.41/0.59 ~on block_2 $_144 (s time_0) \/ object block_2 time_0 % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_2 $_144 \/ ~neq table $_144 \/ % 0.41/0.59 ~on block_2 $_144 (s time_0) \/ object block_1 (s time_0) \/ % 0.41/0.59 source block_1 (s time_0) \/ source block_2 (s time_0) % 0.41/0.59 |- ~a_block $_144 \/ ~neq block_2 $_144 \/ ~neq table $_144 \/ % 0.41/0.59 ~on block_2 $_144 time_0 % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 block_2 \/ ~neq block_1 $_143 \/ % 0.41/0.59 ~on block_1 $_143 (s (s time_0)) \/ destination block_1 time_0 \/ % 0.41/0.59 object block_1 (s time_0) % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 block_2 \/ ~neq block_1 $_143 \/ % 0.41/0.59 ~on block_1 $_143 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 (s time_0) \/ object block_2 time_0 \/ % 0.41/0.59 source block_1 (s time_0) % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 block_2 \/ ~neq block_1 $_143 \/ % 0.41/0.59 ~on block_1 $_143 (s time_0) \/ destination block_1 time_0 % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 block_2 \/ ~neq block_1 $_143 \/ % 0.41/0.59 ~on block_1 $_143 (s time_0) \/ clear block_2 (s time_0) \/ % 0.41/0.59 destination block_1 (s time_0) \/ destination block_2 (s time_0) \/ % 0.41/0.59 source block_1 (s time_0) % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 table \/ ~neq block_1 $_143 \/ % 0.41/0.59 ~on block_1 $_143 (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 (s time_0) \/ object block_2 time_0 % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 table \/ ~neq block_1 $_143 \/ % 0.41/0.59 ~on block_1 $_143 (s (s time_0)) \/ object block_1 (s time_0) \/ % 0.41/0.59 object block_1 time_0 % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 table \/ ~neq block_1 $_143 \/ % 0.41/0.59 ~on block_1 $_143 (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_1 time_0 \/ destination block_2 (s time_0) % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 table \/ ~neq block_1 $_143 \/ % 0.41/0.59 ~on block_1 $_143 (s (s time_0)) \/ clear block_2 (s time_0) \/ % 0.41/0.59 destination block_1 (s time_0) \/ destination block_2 (s time_0) % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 table \/ ~neq block_1 $_143 \/ % 0.41/0.59 ~on block_1 $_143 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 time_0 \/ object block_2 time_0 \/ % 0.41/0.59 source block_1 (s time_0) \/ source block_2 (s time_0) % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 table \/ ~neq block_1 $_143 \/ % 0.41/0.59 ~on block_1 $_143 (s time_0) \/ object block_1 time_0 % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 table \/ ~neq block_1 $_143 \/ % 0.41/0.59 ~on block_1 $_143 (s time_0) \/ clear block_2 (s time_0) \/ % 0.41/0.59 source block_1 (s time_0) \/ source block_2 (s time_0) % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 table \/ ~neq block_1 $_143 \/ % 0.41/0.59 ~on block_1 $_143 time_0 % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 block_1 \/ ~neq block_2 $_143 \/ % 0.41/0.59 ~on block_2 $_143 (s time_0) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 (s time_0) \/ object block_1 (s time_0) % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 table \/ ~neq block_2 $_143 \/ % 0.41/0.59 ~on block_2 $_143 (s (s time_0)) \/ object block_2 (s time_0) \/ % 0.41/0.59 object block_2 time_0 % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 table \/ ~neq block_2 $_143 \/ % 0.41/0.59 ~on block_2 $_143 (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 (s time_0) \/ object block_1 (s time_0) % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 table \/ ~neq block_2 $_143 \/ % 0.41/0.59 ~on block_2 $_143 (s time_0) \/ object block_2 time_0 % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 table \/ ~neq block_2 $_143 \/ % 0.41/0.59 ~on block_2 $_143 (s time_0) \/ object block_1 (s time_0) \/ % 0.41/0.59 source block_1 (s time_0) \/ source block_2 (s time_0) % 0.41/0.59 |- ~a_block $_143 \/ ~neq $_143 table \/ ~neq block_2 $_143 \/ % 0.41/0.59 ~on block_2 $_143 time_0 % 0.41/0.59 |- clear block_2 (s time_0) \/ destination block_1 time_0 \/ % 0.41/0.59 source block_1 (s time_0) \/ source block_2 (s time_0) % 0.41/0.59 |- ~neq $X block_2 \/ ~nonfixed $X \/ ~object $X (s time_0) \/ % 0.41/0.59 clear block_2 (s time_0) \/ destination block_1 time_0 \/ % 0.41/0.59 on $X block_2 (s time_0) \/ source block_1 (s time_0) % 0.41/0.59 |- ~a_block $Y1 \/ ~neq $Y1 block_2 \/ ~source $Y1 (s time_0) \/ % 0.41/0.59 clear block_2 (s time_0) \/ destination block_1 time_0 \/ % 0.41/0.59 source block_1 (s time_0) % 0.41/0.59 |- ~a_block $Y2 \/ ~neq block_2 $Y2 \/ ~source $Y2 (s time_0) \/ % 0.41/0.59 clear block_2 (s time_0) \/ destination block_1 time_0 \/ % 0.41/0.59 source block_1 (s time_0) % 0.41/0.59 |- clear block_2 (s (s time_0)) \/ clear block_2 (s time_0) \/ % 0.41/0.59 destination block_1 time_0 \/ source block_1 (s time_0) % 0.41/0.59 |- ~destination block_2 (s time_0) \/ clear block_2 (s time_0) \/ % 0.41/0.59 destination block_1 time_0 \/ source block_1 (s time_0) % 0.41/0.59 |- ~object block_2 (s time_0) \/ clear block_2 (s time_0) \/ % 0.41/0.59 destination block_1 time_0 \/ source block_1 (s time_0) % 0.41/0.59 |- ~time (s (s time_0)) \/ clear block_2 (s (s (s time_0))) \/ % 0.41/0.59 clear block_2 (s time_0) \/ destination block_1 time_0 \/ % 0.41/0.59 destination block_2 (s (s time_0)) \/ source block_1 (s time_0) % 0.41/0.59 |- object block_1 (s time_0) \/ object block_1 time_0 \/ % 0.41/0.59 on block_2 block_1 (s time_0) \/ source block_1 time_0 \/ % 0.41/0.59 source block_2 time_0 % 0.41/0.59 |- ~a_block $Y \/ ~neq $Y block_1 \/ ~neq block_2 $Y \/ % 0.41/0.59 ~on block_2 $Y (s time_0) \/ object block_1 (s time_0) \/ % 0.41/0.59 object block_1 time_0 \/ source block_1 time_0 \/ source block_2 time_0 % 0.41/0.59 |- ~a_block $Z \/ ~neq block_1 $Z \/ ~neq block_2 $Z \/ % 0.41/0.59 ~on block_2 $Z (s time_0) \/ object block_1 (s time_0) \/ % 0.41/0.59 object block_1 time_0 \/ source block_1 time_0 \/ source block_2 time_0 % 0.41/0.59 |- ~neq $X block_1 \/ ~neq $X block_2 \/ ~nonfixed $X \/ % 0.41/0.59 ~on $X block_1 (s time_0) \/ object block_1 (s time_0) \/ % 0.41/0.59 object block_1 time_0 \/ source block_1 time_0 \/ source block_2 time_0 % 0.41/0.59 |- ~neq block_1 $Z \/ ~neq block_2 $Z \/ ~nonfixed $Z \/ % 0.41/0.59 ~on $Z block_1 (s time_0) \/ object block_1 (s time_0) \/ % 0.41/0.59 object block_1 time_0 \/ source block_1 time_0 \/ source block_2 time_0 % 0.41/0.59 |- ~on block_1 block_2 (s time_0) \/ object block_1 (s time_0) \/ % 0.41/0.59 object block_1 time_0 \/ source block_1 time_0 \/ source block_2 time_0 % 0.41/0.59 |- ~clear block_1 (s time_0) \/ object block_1 (s time_0) \/ % 0.41/0.59 object block_1 time_0 \/ source block_1 time_0 \/ source block_2 time_0 % 0.41/0.59 |- destination block_1 (s time_0) \/ destination block_2 time_0 \/ % 0.41/0.59 object block_2 time_0 \/ on block_1 block_2 (s (s time_0)) % 0.41/0.59 |- ~a_block $Y \/ ~neq $Y block_2 \/ ~neq block_1 $Y \/ % 0.41/0.59 ~on block_1 $Y (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 time_0 \/ object block_2 time_0 % 0.41/0.59 |- ~a_block $Z \/ ~neq block_1 $Z \/ ~neq block_2 $Z \/ % 0.41/0.59 ~on block_1 $Z (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 time_0 \/ object block_2 time_0 % 0.41/0.59 |- ~neq $X block_1 \/ ~neq $X block_2 \/ ~nonfixed $X \/ % 0.41/0.59 ~on $X block_2 (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 time_0 \/ object block_2 time_0 % 0.41/0.59 |- ~neq block_1 $Z \/ ~neq block_2 $Z \/ ~nonfixed $Z \/ % 0.41/0.59 ~on $Z block_2 (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 time_0 \/ object block_2 time_0 % 0.41/0.59 |- ~time (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 time_0 \/ object block_1 (s (s time_0)) \/ % 0.41/0.59 object block_2 time_0 \/ on block_1 block_2 (s (s (s time_0))) % 0.41/0.59 |- ~clear block_2 (s (s time_0)) \/ destination block_1 (s time_0) \/ % 0.41/0.59 destination block_2 time_0 \/ object block_2 time_0 % 0.41/0.59 |- ~object block_1 (s time_0) \/ ~source block_2 (s time_0) \/ % 0.41/0.59 destination block_1 (s time_0) \/ destination block_2 time_0 \/ % 0.41/0.59 object block_2 time_0 % 0.41/0.59 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.41/0.59 %------------------------------------------------------------------------------